English
If f is a sequence of uniformly integrable functions, converging μ-a.e. to g, then eLpNorm(f_n−g) → 0; hence convergence in Lp holds.
Русский
Если f — последовательность униформно интегрируемых функций, сходящаяся μ-почти к g, тогда eLpNorm(f_n−g) → 0; следовательно, сходится в Lp.
LaTeX
$$$\forall ε>0,\ ∃N:\n f_n \to g\text{ in } Lp: \ eLpNorm(f_n−g) p μ → 0$$$
Lean4
/-- A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp. -/
theorem tendsto_Lp_finite_of_tendsto_ae_of_meas [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ℕ → α → β}
{g : α → β} (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g) (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
rw [ENNReal.tendsto_atTop_zero]
intro ε hε
by_cases h : ε < ∞; swap
· rw [not_lt, top_le_iff] at h
exact ⟨0, fun n _ => by simp [h]⟩
by_cases hμ : μ = 0
· exact ⟨0, fun n _ => by simp [hμ]⟩
have hε' : 0 < ε.toReal / 3 := div_pos (ENNReal.toReal_pos hε.ne' h.ne) (by simp)
have hdivp : 0 ≤ 1 / p.toReal := by positivity
have hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal) := Real.rpow_pos_of_pos (measureUnivNNReal_pos hμ) _
obtain ⟨δ₁, hδ₁, heLpNorm₁⟩ := hui hε'
obtain ⟨δ₂, hδ₂, heLpNorm₂⟩ := hg'.eLpNorm_indicator_le hp hp' hε'
obtain ⟨t, htm, ht₁, ht₂⟩ := tendstoUniformlyOn_of_ae_tendsto' hf hg hfg (lt_min hδ₁ hδ₂)
rw [Metric.tendstoUniformlyOn_iff] at ht₂
specialize
ht₂ (ε.toReal / (3 * measureUnivNNReal μ ^ (1 / p.toReal)))
(div_pos (ENNReal.toReal_pos (gt_iff_lt.1 hε).ne.symm h.ne) (mul_pos (by simp) hpow))
obtain ⟨N, hN⟩ := eventually_atTop.1 ht₂; clear ht₂
refine ⟨N, fun n hn => ?_⟩
rw [← t.indicator_self_add_compl (f n - g)]
refine
le_trans
(eLpNorm_add_le (((hf n).sub hg).indicator htm).aestronglyMeasurable
(((hf n).sub hg).indicator htm.compl).aestronglyMeasurable hp)
?_
rw [sub_eq_add_neg, Set.indicator_add' t, Set.indicator_neg']
refine
le_trans
(add_le_add_right
(eLpNorm_add_le ((hf n).indicator htm).aestronglyMeasurable (hg.indicator htm).neg.aestronglyMeasurable hp) _)
?_
have hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3) :=
by
refine heLpNorm₁ n t htm (le_trans ht₁ ?_)
rw [ENNReal.ofReal_le_ofReal_iff hδ₁.le]
exact min_le_left _ _
have hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3) :=
by
refine heLpNorm₂ t htm (le_trans ht₁ ?_)
rw [ENNReal.ofReal_le_ofReal_iff hδ₂.le]
exact min_le_right _ _
have hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3) :=
by
specialize hN n hn
have : 0 ≤ ε.toReal / (3 * measureUnivNNReal μ ^ (1 / p.toReal)) := by positivity
have :=
eLpNorm_sub_le_of_dist_bdd μ hp' htm.compl this fun x hx =>
(dist_comm (g x) (f n x) ▸ (hN x hx).le :
dist (f n x) (g x) ≤ ε.toReal / (3 * measureUnivNNReal μ ^ (1 / p.toReal)))
refine le_trans this ?_
rw [div_mul_eq_div_mul_one_div, ← ENNReal.ofReal_toReal (measure_lt_top μ tᶜ).ne,
ENNReal.ofReal_rpow_of_nonneg ENNReal.toReal_nonneg hdivp, ← ENNReal.ofReal_mul, mul_assoc]
· refine ENNReal.ofReal_le_ofReal (mul_le_of_le_one_right hε'.le ?_)
rw [mul_comm, mul_one_div, div_le_one]
· refine
Real.rpow_le_rpow ENNReal.toReal_nonneg (ENNReal.toReal_le_of_le_ofReal (measureUnivNNReal_pos hμ).le ?_)
hdivp
rw [ENNReal.ofReal_coe_nnreal, coe_measureUnivNNReal]
exact measure_mono (Set.subset_univ _)
· exact Real.rpow_pos_of_pos (measureUnivNNReal_pos hμ) _
· positivity
have : ENNReal.ofReal (ε.toReal / 3) = ε / 3 :=
by
rw [ENNReal.ofReal_div_of_pos (show (0 : ℝ) < 3 by simp), ENNReal.ofReal_toReal h.ne]
simp
rw [this] at hnf hng hlt
rw [eLpNorm_neg, ← ENNReal.add_thirds ε, ← sub_eq_add_neg]
gcongr
