# Continuity of the action of `Mᵈᵐᵃ`

on `MeasureSpace.Lp E p μ`

#

In this file we prove that under certain conditions,
the action of `Mᵈᵐᵃ`

on `MeasureTheory.Lp E p μ`

is continuous in both variables.

Recall that `Mᵈᵐᵃ`

acts on `MeasureTheory.Lp E p μ`

by `mk c • f = MeasureTheory.Lp.compMeasurePreserving (c • ·) _ f`

.
This action is defined, if `M`

acts on `X`

by mesaure preserving maps.

If `M`

acts on `X`

by continuous maps
preserving a locally finite measure
which is inner regular for finite measure sets with respect to compact sets,
then the action of `Mᵈᵐᵃ`

on `Lp E p μ`

described above, `1 ≤ p < ∞`

,
is continuous in both arguments.

In particular, it applies to the case when `X = M`

is a locally compact topological group,
and `μ`

is the Haar measure.

## Tags #

measure theory, group action, domain action, continuous action, Lp space

instance
MeasureTheory.Lp.instContinuousVAddDomAddAct
{X : Type u_1}
{M : Type u_2}
{E : Type u_3}
[TopologicalSpace X]
[R1Space X]
[MeasurableSpace X]
[BorelSpace X]
[TopologicalSpace M]
[MeasurableSpace M]
[OpensMeasurableSpace M]
[VAdd M X]
[ContinuousVAdd M X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
[μ.InnerRegularCompactLTTop]
[MeasureTheory.VAddInvariantMeasure M X μ]
{p : ENNReal}
[Fact (1 ≤ p)]
[hp : Fact (p ≠ ⊤)]
:

ContinuousVAdd Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)

## Equations

- ⋯ = ⋯

instance
MeasureTheory.Lp.instContinuousSMulDomMulAct
{X : Type u_1}
{M : Type u_2}
{E : Type u_3}
[TopologicalSpace X]
[R1Space X]
[MeasurableSpace X]
[BorelSpace X]
[TopologicalSpace M]
[MeasurableSpace M]
[OpensMeasurableSpace M]
[SMul M X]
[ContinuousSMul M X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
[μ.InnerRegularCompactLTTop]
[MeasureTheory.SMulInvariantMeasure M X μ]
{p : ENNReal}
[Fact (1 ≤ p)]
[hp : Fact (p ≠ ⊤)]
:

ContinuousSMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

## Equations

- ⋯ = ⋯