English
Consider a net (f) in Lp(E,p,ν) and a net (g) in C(X,Y) with appropriate measure-preserving properties. If f and g converge to f0 and g0 respectively, then the composed elements Lp.compMeasurePreserving(g a)(f a) converge to Lp.compMeasurePreserving(g0)(f0).
Русский
Пусть (f_i) в Lp(E,p,ν) и (g_i) в C(X,Y) сходятся к f0 и g0 соответственно, и g_i сохраняют меру. Тогда для их композиции выполняется сходимость: Lp.compMeasurePreserving(g_i, f_i) → Lp.compMeasurePreserving(g0, f0).
LaTeX
$$$\\text{If } f_i \\to f_0 \\text{ in } L^p(E,p,ν),\\; g_i \\to g_0 \\text{ in } C(X,Y),\\; \\text{and } g_i \\text{ preserve measures, then } Lp\\text{ composition is continuous: } \n\\lim_i Lp\\text{(g_i,f_i)} = Lp\\text{(g_0,f_0)}.$$$
Lean4
theorem compMeasurePreservingLp {α : Type*} {l : Filter α} {f : α → Lp E p ν} {f₀ : Lp E p ν} {g : α → C(X, Y)}
{g₀ : C(X, Y)} (hf : Tendsto f l (𝓝 f₀)) (hg : Tendsto g l (𝓝 g₀)) (hgm : ∀ a, MeasurePreserving (g a) μ ν)
(hgm₀ : MeasurePreserving g₀ μ ν) (hp : p ≠ ∞) :
Tendsto (fun a ↦ Lp.compMeasurePreserving (g a) (hgm a) (f a)) l (𝓝 (Lp.compMeasurePreserving g₀ hgm₀ f₀)) :=
by
have := (Lp.compMeasurePreserving_continuous μ ν E hp).tendsto ⟨f₀, g₀, hgm₀⟩
replace hg : Tendsto (fun a ↦ ⟨g a, hgm a⟩ : α → { g : C(X, Y) // MeasurePreserving g μ ν }) l (𝓝 ⟨g₀, hgm₀⟩) :=
tendsto_subtype_rng.2 hg
convert this.comp (hf.prodMk_nhds hg)
