Documentation

Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

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_2} {Y : Type u_3} [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_4) [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_2} {Y : Type u_3} [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_4} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 p)] {α : Type u_5} {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_2} {Y : Type u_3} [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_4} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 p)] {Z : Type u_5} [TopologicalSpace Z] {f : Z(MeasureTheory.Lp E p ν)} {g : ZC(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_2} {Y : Type u_3} [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_4} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 p)] {Z : Type u_5} [TopologicalSpace Z] {f : Z(MeasureTheory.Lp E p ν)} {g : ZC(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_2} {Y : Type u_3} [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_4} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 p)] {Z : Type u_5} [TopologicalSpace Z] {f : Z(MeasureTheory.Lp E p ν)} {g : ZC(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_2} {Y : Type u_3} [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_4} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 p)] {Z : Type u_5} [TopologicalSpace Z] {f : Z(MeasureTheory.Lp E p ν)} {g : ZC(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)