English
If p ≠ 0 and p ≠ ∞ and f_n are AEStronglyMeasurable and g is AEStronglyMeasurable, and eLpNorm(f_n − g) tends to 0 in l, then f converges in measure to g.
Русский
Если p не 0 и не ∞, f_n а.е.-измеримы и g а.е.-измеримы, и eLpNorm(f_n − g) стремится к 0 по l, то f сходится по мере к g.
LaTeX
$$$p ≠ 0, p ≠ ∞ \Rightarrow (\forall n, AEStronglyMeasurable(f_n)) \wedge AEStronglyMeasurable(g) \wedge Tendsto(\lambda n, eLpNorm(f_n - g) p μ) l (\ nhds 0) \Rightarrow TendstoInMeasure μ f l g$$$
Lean4
/-- This lemma is superseded by `MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm` where we
allow `p = ∞` and only require `AEStronglyMeasurable`. -/
theorem tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
(hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g) {l : Filter ι}
(hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)) : TendstoInMeasure μ f l g :=
by
refine tendstoInMeasure_of_ne_top fun ε hε hε_top ↦ ?_
replace hfg :=
ENNReal.Tendsto.const_mul (a := 1 / ε ^ p.toReal) (Tendsto.ennrpow_const p.toReal hfg) (Or.inr <| by simp [hε.ne'])
simp only [mul_zero, ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)] at hfg
rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
intro δ hδ
refine (hfg δ hδ).mono fun n hn => ?_
refine le_trans ?_ hn
rw [one_div, ← ENNReal.inv_mul_le_iff, inv_inv]
· convert mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top ((hf n).sub hg).aestronglyMeasurable ε using 6
simp [edist_eq_enorm_sub]
· simp [hε_top]
· simp [hε.ne']
