English
Vitali's convergence criterion: convergence in Lp to g is equivalent to uniform integrability plus convergence in measure to g.
Русский
Критерий сходимости в Lp: сходимость в Lp эквивалентна единой встроенной интегрируемости и схождению по мере к g.
LaTeX
$$$\text{TendstoInMeasure } μ f atTop g ∧ UnifIntegrable f p μ \iff \ Tendsto (n \mapsto eLpNorm (f n - g) p μ) atTop (\ NHds 0)$$$
Lean4
/-- **Vitali's convergence theorem**: A sequence of functions `f` converges to `g` in Lp if and
only if it is uniformly integrable and converges to `g` in measure. -/
theorem tendstoInMeasure_iff_tendsto_Lp_finite [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞)
(hf : ∀ n, MemLp (f n) p μ) (hg : MemLp g p μ) :
TendstoInMeasure μ f atTop g ∧ UnifIntegrable f p μ ↔ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0) :=
⟨fun h => tendsto_Lp_finite_of_tendstoInMeasure hp hp' (fun n => (hf n).1) hg h.2 h.1, fun h =>
⟨tendstoInMeasure_of_tendsto_eLpNorm (lt_of_lt_of_le zero_lt_one hp).ne.symm (fun n => (hf n).aestronglyMeasurable)
hg.aestronglyMeasurable h,
unifIntegrable_of_tendsto_Lp hp hp' hf hg h⟩⟩
