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ᵈᵃᵃ { x : X →ₘ[μ] E // x ∈ 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ᵈᵐᵃ { x : X →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }
Equations
- ⋯ = ⋯