Continuity of MeasureTheory.Lp.compMeasurePreserving #
In this file we prove that the composition of an L^p function g
with a continuous measure-preserving map f is continuous in both arguments.
First, we prove it for indicator functions,
in terms of convergence of μ ((f a ⁻¹' s) ∆ (g ⁻¹' s)) to zero.
Then we prove the continuity of the function of two arguments
defined on MeasureTheory.Lp E p ν × {f : C(X, Y) // MeasurePreserving f μ ν}.
Finally, we provide dot notation convenience lemmas.
theorem
MeasureTheory.Lp.compMeasurePreserving_continuous
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
[R1Space X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[R1Space Y]
(μ : MeasureTheory.Measure X)
(ν : MeasureTheory.Measure Y)
[μ.InnerRegularCompactLTTop]
[MeasureTheory.IsLocallyFiniteMeasure ν]
(E : Type u_3)
[NormedAddCommGroup E]
{p : ENNReal}
[Fact (1 ≤ p)]
(hp : p ≠ ⊤)
:
Continuous fun (gf : ↥(MeasureTheory.Lp E p ν) × { f : C(X, Y) // MeasureTheory.MeasurePreserving (⇑f) μ ν }) =>
(MeasureTheory.Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1
Let X and Y be R₁ topological spaces
with Borel σ-algebras and measures μ and ν, respectively.
Suppose that μ is inner regular for finite measure sets with respect to compact sets
and ν is a locally finite measure.
Let 1 ≤ p < ∞ be an extended nonnegative real number.
Then the composition of a function g : Lp E p ν
and a measure preserving continuous function f : C(X, Y)
is continuous in both variables.
theorem
Filter.Tendsto.compMeasurePreservingLp
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
[R1Space X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[R1Space Y]
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
[μ.InnerRegularCompactLTTop]
[MeasureTheory.IsLocallyFiniteMeasure ν]
{E : Type u_3}
[NormedAddCommGroup E]
{p : ENNReal}
[Fact (1 ≤ p)]
{α : Type u_4}
{l : Filter α}
{f : α → ↥(MeasureTheory.Lp E p ν)}
{f₀ : ↥(MeasureTheory.Lp E p ν)}
{g : α → C(X, Y)}
{g₀ : C(X, Y)}
(hf : Filter.Tendsto f l (nhds f₀))
(hg : Filter.Tendsto g l (nhds g₀))
(hgm : ∀ (a : α), MeasureTheory.MeasurePreserving (⇑(g a)) μ ν)
(hgm₀ : MeasureTheory.MeasurePreserving (⇑g₀) μ ν)
(hp : p ≠ ⊤)
:
Filter.Tendsto (fun (a : α) => (MeasureTheory.Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l
(nhds ((MeasureTheory.Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
theorem
ContinuousWithinAt.compMeasurePreservingLp
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
[R1Space X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[R1Space Y]
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
[μ.InnerRegularCompactLTTop]
[MeasureTheory.IsLocallyFiniteMeasure ν]
{E : Type u_3}
[NormedAddCommGroup E]
{p : ENNReal}
[Fact (1 ≤ p)]
{Z : Type u_4}
[TopologicalSpace Z]
{f : Z → ↥(MeasureTheory.Lp E p ν)}
{g : Z → C(X, Y)}
{s : Set Z}
{z : Z}
(hf : ContinuousWithinAt f s z)
(hg : ContinuousWithinAt g s z)
(hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν)
(hp : p ≠ ⊤)
:
ContinuousWithinAt (fun (z : Z) => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s z
theorem
ContinuousAt.compMeasurePreservingLp
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
[R1Space X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[R1Space Y]
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
[μ.InnerRegularCompactLTTop]
[MeasureTheory.IsLocallyFiniteMeasure ν]
{E : Type u_3}
[NormedAddCommGroup E]
{p : ENNReal}
[Fact (1 ≤ p)]
{Z : Type u_4}
[TopologicalSpace Z]
{f : Z → ↥(MeasureTheory.Lp E p ν)}
{g : Z → C(X, Y)}
{z : Z}
(hf : ContinuousAt f z)
(hg : ContinuousAt g z)
(hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν)
(hp : p ≠ ⊤)
:
ContinuousAt (fun (z : Z) => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) z
theorem
ContinuousOn.compMeasurePreservingLp
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
[R1Space X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[R1Space Y]
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
[μ.InnerRegularCompactLTTop]
[MeasureTheory.IsLocallyFiniteMeasure ν]
{E : Type u_3}
[NormedAddCommGroup E]
{p : ENNReal}
[Fact (1 ≤ p)]
{Z : Type u_4}
[TopologicalSpace Z]
{f : Z → ↥(MeasureTheory.Lp E p ν)}
{g : Z → C(X, Y)}
{s : Set Z}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
(hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν)
(hp : p ≠ ⊤)
:
ContinuousOn (fun (z : Z) => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s
theorem
Continuous.compMeasurePreservingLp
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
[R1Space X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[R1Space Y]
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
[μ.InnerRegularCompactLTTop]
[MeasureTheory.IsLocallyFiniteMeasure ν]
{E : Type u_3}
[NormedAddCommGroup E]
{p : ENNReal}
[Fact (1 ≤ p)]
{Z : Type u_4}
[TopologicalSpace Z]
{f : Z → ↥(MeasureTheory.Lp E p ν)}
{g : Z → C(X, Y)}
(hf : Continuous f)
(hg : Continuous g)
(hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν)
(hp : p ≠ ⊤)
:
Continuous fun (z : Z) => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)