English
Forward Vitali-type direction: if a sequence f_n converges a.e. to g and is uniformly integrable and tight, and each f_n is AEStronglyMeasurable with a suitable limit g, then the Lp distance eLpNorm(f_n − g) tends to 0.
Русский
Переходная формулировка Витали типа: если f_n сходится almost everywhere к g и является униформно интегрируемым и сжимаемым, и каждое f_n совместимо с g, тогда расстояние в Lp между f_n и g сходится к нулю.
LaTeX
$$$hp\\ge1, hp'\\neq∞, haef, hg, hui, hut, hfg \\Rightarrow Tendsto (n \\mapsto eLpNorm (f n - g) p μ) atTop (nhds 0)$$$
Lean4
/-- Forward direction of Vitali's convergence theorem, with a.e. instead of `InMeasure`
convergence -/
theorem tendsto_Lp_of_tendsto_ae (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ℕ → α → β} {g : α → β}
(haef : ∀ n, AEStronglyMeasurable (f n) μ) (hg' : MemLp g p μ) (hui : UnifIntegrable f p μ) (hut : UnifTight f p μ)
(hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0) :=
by
-- come up with an a.e. equal strongly measurable replacement `f` for `g`
have hf := fun n => (haef n).stronglyMeasurable_mk
have hff' := fun n => (haef n).ae_eq_mk (μ := μ)
have hui' := hui.ae_eq hff'
have hut' := hut.aeeq hff'
have hg := hg'.aestronglyMeasurable.stronglyMeasurable_mk
have hgg' := hg'.aestronglyMeasurable.ae_eq_mk (μ := μ)
have hg'' := hg'.ae_eq hgg'
have haefg' := ae_tendsto_ae_congr hff' hgg' hfg
set f' := fun n => (haef n).mk (μ := μ)
set g' := hg'.aestronglyMeasurable.mk (μ := μ)
have haefg (n : ℕ) : f n - g =ᵐ[μ] f' n - g' := (hff' n).sub hgg'
have hsnfg (n : ℕ) := eLpNorm_congr_ae (p := p) (haefg n)
apply Filter.Tendsto.congr (fun n => (hsnfg n).symm)
exact tendsto_Lp_of_tendsto_ae_of_meas hp hp' hf hg hg'' hui' hut' haefg'
