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 measure-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.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] {μ : Measure X} [IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] [SMulInvariantMeasure M X μ] {p : ENNReal} [Fact (1 ≤ p)] [hp : Fact (p ≠ ⊤)] : ContinuousSMul Mᵈᵐᵃ ↥(Lp E p μ)

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] {μ : Measure X} [IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] [VAddInvariantMeasure M X μ] {p : ENNReal} [Fact (1 ≤ p)] [hp : Fact (p ≠ ⊤)] : ContinuousVAdd Mᵈᵃᵃ ↥(Lp E p μ)