tendsto_Lp_iff_tendsto_eLpNorm — Mathlib

English

Equivalent tendsto results for Lp via eLpNorm.

Русский

Эквивалентные результаты перехода в Lp через eLpNorm.

LaTeX

$$$\text{Tendsto in } Lp \;\Leftrightarrow\; \text{Tendsto via } eLpNorm$$$

Lean4

theorem tendsto_Lp_iff_tendsto_eLpNorm {ι} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → Lp E p μ) (f_lim : α → E)
    (f_lim_ℒp : MemLp f_lim p μ) :
    fi.Tendsto f (𝓝 (f_lim_ℒp.toLp f_lim)) ↔ fi.Tendsto (fun n => eLpNorm (⇑(f n) - f_lim) p μ) (𝓝 0) :=
  by
  rw [tendsto_Lp_iff_tendsto_eLpNorm']
  suffices h_eq :
    (fun n => eLpNorm (⇑(f n) - ⇑(MemLp.toLp f_lim f_lim_ℒp)) p μ) = (fun n => eLpNorm (⇑(f n) - f_lim) p μ) by
    rw [h_eq]
  exact funext fun n => eLpNorm_congr_ae (EventuallyEq.rfl.sub (MemLp.coeFn_toLp f_lim_ℒp))

Похожие утверждения