English
Vitali-type forward direction: if a uniform-integrable sequence converges in measure to g on a finite measure space, then the eLpNorm of the difference tends to 0 along the index set.
Русский
Условная версия теоремы Витали: если униформ-интегрируемая последовательность сходится по мере к g на конечном мере, тогда eLpNorm(f_n−g) → 0.
LaTeX
$$$\text{TendstoInMeasure } μ f atTop g \Rightarrow \ Tendsto (n \mapsto eLpNorm (f n - g) p μ) atTop (\ NHDS 0)$$$
Lean4
/-- A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp. -/
theorem tendsto_Lp_finite_of_tendsto_ae [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ℕ → α → β} {g : α → β}
(hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : MemLp g p μ) (hui : UnifIntegrable f p μ)
(hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0) :=
by
have : ∀ n, eLpNorm (f n - g) p μ = eLpNorm ((hf n).mk (f n) - hg.1.mk g) p μ := fun n =>
eLpNorm_congr_ae ((hf n).ae_eq_mk.sub hg.1.ae_eq_mk)
simp_rw [this]
refine
tendsto_Lp_finite_of_tendsto_ae_of_meas hp hp' (fun n => (hf n).stronglyMeasurable_mk) hg.1.stronglyMeasurable_mk
(hg.ae_eq hg.1.ae_eq_mk) (hui.ae_eq fun n => (hf n).ae_eq_mk) ?_
have h_ae_forall_eq : ∀ᵐ x ∂μ, ∀ n, f n x = (hf n).mk (f n) x :=
by
rw [ae_all_iff]
exact fun n => (hf n).ae_eq_mk
filter_upwards [hfg, h_ae_forall_eq, hg.1.ae_eq_mk] with x hx_tendsto hxf_eq hxg_eq
rw [← hxg_eq]
convert hx_tendsto using 1
ext1 n
exact (hxf_eq n).symm
