English
If μ is finite, f_n are AES-trongly-measurable, and f_n(x) converges to g(x) almost everywhere, then f converges in measure to g along atTop.
Русский
Если μ конечна, f_n ультраа.е. измеримы и f_n(x) сходится к g(x) почти каждая точка, тогда f сходится по мере к g вдоль atTop.
LaTeX
$$$[IsFiniteMeasure\;\mu] \ (\forall n, AEStronglyMeasurable(f_n)) \Rightarrow (AEStronglyMeasurable(g)) \\Rightarrow (\forall^{?} x, Tendsto (f_n(x)) atTop (\mathcal{N}(g(x)))) \\Rightarrow TendstoInMeasure\;\mu\;f\;atTop\;g$$
Lean4
/-- Convergence a.e. implies convergence in measure in a finite measure space. -/
theorem tendstoInMeasure_of_tendsto_ae [IsFiniteMeasure μ] (hf : ∀ n, AEStronglyMeasurable (f n) μ)
(hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) : TendstoInMeasure μ f atTop g :=
by
have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg
refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
refine
tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable (fun i => (hf i).stronglyMeasurable_mk)
hg.stronglyMeasurable_mk ?_
have hf_eq_ae : ∀ᵐ x ∂μ, ∀ n, (hf n).mk (f n) x = f n x := ae_all_iff.mpr fun n => (hf n).ae_eq_mk.symm
filter_upwards [hf_eq_ae, hg.ae_eq_mk, hfg] with x hxf hxg hxfg
rw [← hxg, funext fun n => hxf n]
exact hxfg
