English
If p = ∞ and f_n → g in eLpNorm on the top ENNReal, then f → g in measure.
Русский
Если p = ∞ и f_n сходится по норме eLp в топе ENNReal к g, то f сходится по мере к g.
LaTeX
$$$p = \infty \Rightarrow Tendsto(f_n - g) \text{ в top eLpNorm} \Rightarrow TendstoInMeasure μ f l g$$$
Lean4
/-- See also `MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm` which work for general
Lp-convergence for all `p ≠ 0`. -/
theorem tendstoInMeasure_of_tendsto_eLpNorm_top {E} [NormedAddCommGroup E] {f : ι → α → E} {g : α → E} {l : Filter ι}
(hfg : Tendsto (fun n => eLpNorm (f n - g) ∞ μ) l (𝓝 0)) : TendstoInMeasure μ f l g :=
by
refine tendstoInMeasure_of_ne_top fun δ hδ hδ_top ↦ ?_
simp only [eLpNorm_exponent_top, eLpNormEssSup] at hfg
rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
intro ε hε
specialize hfg (δ / 2) (ENNReal.div_pos_iff.2 ⟨hδ.ne', ENNReal.ofNat_ne_top⟩)
refine hfg.mono fun n hn => ?_
simp only [Pi.sub_apply] at *
have : essSup (fun x : α => ‖f n x - g x‖ₑ) μ < δ := hn.trans_lt (ENNReal.half_lt_self hδ.ne' hδ_top)
refine ((le_of_eq ?_).trans (ae_lt_of_essSup_lt this).le).trans hε.le
congr with x
simp [edist_eq_enorm_sub]
