English
Let X, Y be R1 spaces with Borel σ-algebras and measures μ on X and ν on Y. If μ is inner regular for finite measure sets and ν is locally finite, and 1 ≤ p < ∞, then the map (g,f) ↦ g ∘ f, from Lp(E,p,ν) × C(X,Y) to Lp(E,p,μ) given by composing a function g with a measure-preserving continuous map f, is continuous in both arguments.
Русский
Пусть X, Y — топологические пространства R1 с борелевскими σ-алгебрами, μ — мера на X, ν — мера на Y, μ внутренне регулярна по конечным множествам, ν локально конечна, и 1 ≤ p < ∞. Тогда композиция g ∘ f с MeasurePreserving f и непрерывной характеристикой f непрерывна в обе стороны как отображение Lp(E,p,ν) × C(X,Y) → Lp(E,p,μ).
LaTeX
$$$\\text{Let } X,Y \\text{ be R1 spaces with Borel σ-algebras } μ,ν \\text{ measures with } μ\\text{ inner regular for finite measure sets and } ν \\text{ locally finite. For } 1 \\le p < \\infty,\\; g \\in L^p(E,p,ν),\\; f \\in C(X,Y)\\text{ measure-preserving, the map } (g,f) \\mapsto g \\circ f \\text{ is continuous in both arguments.}$$$
Lean4
/-- 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 compMeasurePreserving_continuous (hp : p ≠ ∞) :
Continuous fun gf : Lp E p ν × { f : C(X, Y) // MeasurePreserving f μ ν } ↦
compMeasurePreserving gf.2.1 gf.2.2 gf.1 :=
by
have hp₀ : p ≠ 0 := (one_pos.trans_le Fact.out).ne'
refine
continuous_prod_of_dense_continuous_lipschitzWith _ 1 (MeasureTheory.Lp.simpleFunc.dense hp) ?_ fun f ↦
(isometry_compMeasurePreserving f.2).lipschitz
intro f hf
lift f to Lp.simpleFunc E p ν using hf
induction f using Lp.simpleFunc.induction hp₀ hp with
| add hfp hgp _ ihf ihg => exact ihf.add ihg
| @indicatorConst c s hs
hνs =>
dsimp only [Lp.simpleFunc.coe_indicatorConst, Lp.indicatorConstLp_compMeasurePreserving]
refine continuous_indicatorConstLp_set hp fun f ↦ ?_
apply tendsto_measure_symmDiff_preimage_nhds_zero continuousAt_subtype_val _ f.2 hs.nullMeasurableSet hνs.ne
exact .of_forall Subtype.property
