English
In a non-finite measure space, a sequence converging to g in measure, together with uniform integrability and tightness, converges in Lp to g, if p is finite and at least 1.
Русский
В недопустимом по размеру мере пространстве последовательность, сходящаяся в мере к g вместе с униформной интегрируемостью и ограниченностью, сходится в Lp к g, если p конечна и ≥ 1.
LaTeX
$$$1\\le p,\\ p\\neq \\infty \\Rightarrow (TendstoInMeasure μ f atTop g \\land UnifIntegrable f p μ \\land UnifTight f p μ) \\iff Tendsto (n \\mapsto eLpNorm (f n - g) p μ) atTop (nhds 0)$$$
Lean4
/-- **Vitali's convergence theorem** (non-finite measure version).
A sequence of functions `f` converges to `g` in Lp
if and only if it is uniformly integrable, uniformly tight and converges to `g` in measure. -/
theorem tendstoInMeasure_iff_tendsto_Lp (hp : 1 ≤ p) (hp' : p ≠ ∞) (hf : ∀ n, MemLp (f n) p μ) (hg : MemLp g p μ) :
TendstoInMeasure μ f atTop g ∧ UnifIntegrable f p μ ∧ UnifTight f p μ ↔
Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
where
mp h := tendsto_Lp_of_tendstoInMeasure hp hp' (fun n => (hf n).1) hg h.2.1 h.2.2 h.1
mpr
h :=
⟨tendstoInMeasure_of_tendsto_eLpNorm (lt_of_lt_of_le zero_lt_one hp).ne' (fun n => (hf n).aestronglyMeasurable)
hg.aestronglyMeasurable h,
unifIntegrable_of_tendsto_Lp hp hp' hf hg h, unifTight_of_tendsto_Lp hp' hf hg h⟩
