tendsto_Lp_of_tendsto_eLpNorm — Mathlib

English

If eLpNorm tends to 0, then the original Lp-functions tend to their limit in Lp.

Русский

Если eLpNorm стремится к 0, то функции в Lp стремятся к пределу в Lp.

LaTeX

$$$\text{If } eLpNorm(f_n - f) \to 0, \; f_n \to f \text{ in } Lp$$$

Lean4

theorem tendsto_Lp_of_tendsto_eLpNorm {ι} {fi : Filter ι} [Fact (1 ≤ p)] {f : ι → Lp E p μ} (f_lim : α → E)
    (f_lim_ℒp : MemLp f_lim p μ) (h_tendsto : fi.Tendsto (fun n => eLpNorm (⇑(f n) - f_lim) p μ) (𝓝 0)) :
    fi.Tendsto f (𝓝 (f_lim_ℒp.toLp f_lim)) :=
  (tendsto_Lp_iff_tendsto_eLpNorm f f_lim f_lim_ℒp).mpr h_tendsto

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