English
If p ≠ 0 and p ≠ ∞ and f_n are AEStronglyMeasurable, g AEStronglyMeasurable, and Tendsto eLpNorm(f_n − g) p μ to 0, then TendstoInMeasure μ f l g.
Русский
Если p не 0 и не ∞, f_n AESтронно измеримы, g AES измерима, и Tendsto eLpNorm(f_n − g) к 0, то TendstoInMeasure μ f l g.
LaTeX
$$$p ≠ 0 \Rightarrow p ≠ ∞ \Rightarrow (\forall n, AEStronglyMeasurable(f_n)) \Rightarrow AEStronglyMeasurable(g) \Rightarrow \nabla Tendsto(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 = ∞`. -/
theorem tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
(hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : AEStronglyMeasurable g μ) {l : Filter ι}
(hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)) : TendstoInMeasure μ f l g :=
by
refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
refine
tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable hp_ne_zero hp_ne_top
(fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk ?_
have : (fun n => eLpNorm ((hf n).mk (f n) - hg.mk g) p μ) = fun n => eLpNorm (f n - g) p μ := by ext1 n;
refine eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)
rw [this]
exact hfg
