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.
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 f : α → C(X, Y) be a family of continuous maps
that converges to a continuous map g : C(X, Y) in the compact-open topology along a filter l.
Suppose that g is a measure preserving map
and f a is a measure preserving map eventually along l.
Then for any finite measure measurable set s,
the preimages f a ⁻¹' s tend to the preimage g ⁻¹' s in measure.
More precisely, the measure of the symmetric difference of these two sets tends to zero.
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.