English
Vitali-type equivalence: under suitable conditions, TendstoInMeasure to g implies Tendsto in Lp of the eLpNorm to 0, and vice versa, given uniform integrability and tightness.
Русский
Эквивалентность Виталий: при подходящих условиях существование и переход в Lp эквивалентны TendstoInMeasure к g.
LaTeX
$$$\\text{TendstoInMeasure}\\; μ\\; f\\; atTop\\; g\\quad\\land\\quad \\operatorname{UnifIntegrable} f p μ \\land \\operatorname{UnifTight} f p μ \\Leftrightarrow \\text{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, uniformly tight functions that converge in
measure to some function `g` in a finite measure space, then `f` converge in Lp to `g`. -/
theorem tendsto_Lp_of_tendstoInMeasure (hp : 1 ≤ p) (hp' : p ≠ ∞) (hf : ∀ n, AEStronglyMeasurable (f n) μ)
(hg : MemLp g p μ) (hui : UnifIntegrable f p μ) (hut : UnifTight 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_of_tendsto_ae hp hp' (fun _ => hf _) hg
(fun ε hε => -- `UnifIntegrable` on a subsequence
let ⟨δ, hδ, hδ'⟩ := hui hε
⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
(fun ε hε => -- `UnifTight` on a subsequence
let ⟨s, hμs, hfε⟩ := hut hε
⟨s, hμs, fun i => hfε _⟩)
hms'⟩
