English
Forward Vitali: if a sequence f is uniformly integrable and converges in measure to g, then f converges to g in Lp; hence eLpNorm(f−g)→0.
Русский
Витали: если f UniformIntegrable и сходится по мере к g, тогда f→g в Lp; eLpNorm(f−g)→0.
LaTeX
$$$\text{TendstoInMeasure } μ f atTop g ∧ \text{UnifIntegrable } f p μ \Rightarrow \ Tendsto (n \mapsto eLpNorm (f n - g) p μ) atTop (\ NHds 0)$$$
Lean4
/-- Forward direction of Vitali's convergence theorem: if `f` is a sequence of uniformly integrable
functions that converge in measure to some function `g` in a finite measure space, then `f`
converge in Lp to `g`. -/
theorem tendsto_Lp_finite_of_tendstoInMeasure [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞)
(hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : MemLp g p μ) (hui : UnifIntegrable f p μ)
(hfg : TendstoInMeasure μ f atTop g) : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0) :=
by
refine tendsto_of_subseq_tendsto fun ns hns => ?_
obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns
exact
⟨ms,
tendsto_Lp_finite_of_tendsto_ae hp hp' (fun _ => hf _) hg
(fun ε hε =>
let ⟨δ, hδ, hδ'⟩ := hui hε
⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
hms'⟩
