English
Let X,Y be topological spaces with Borel σ-algebras, μ,f etc. If f and g are continuous within a set s and g(z) is measure-preserving for all z, then the map z ↦ Lp.compMeasurePreserving(g z)(f z) is continuous within s, provided p ≠ ∞.
Русский
Пусть f: Z→Lp(E,p,ν) и g: Z→C(X,Y) непрерывны на множестве s; предположим, что для каждого z мером меры ν и μ сохраняются при g(z). Тогда z↦Lp.compMeasurePreserving(g z)(f z) непрерывна на s при p ≠ ∞.
LaTeX
$$$\\text{If } f,g: Z\\to \\cdots,\\; f,g \\text{ continuous, and } \\forall z,\\ MeasurePreserving(g(z),\\mu,\\nu),\\; p\\neq\\infty, \\text{ then } z \\mapsto Lp\\cdot (g(z),f(z)) \\text{ is continuous}. $$$
Lean4
theorem compMeasurePreservingLp (hf : ContinuousWithinAt f s z) (hg : ContinuousWithinAt g s z)
(hgm : ∀ z, MeasurePreserving (g z) μ ν) (hp : p ≠ ∞) :
ContinuousWithinAt (fun z ↦ Lp.compMeasurePreserving (g z) (hgm z) (f z)) s z :=
Tendsto.compMeasurePreservingLp hf hg _ _ hp
