tendsto_Lp_iff_tendsto_eLpNorm' — Mathlib

English

For f: ι → Lp, Tendsto f ↦ f_lim in Lp is equivalent to Tendsto eLpNorm( f - f_lim) to 0.

Русский

При переходе в Lp эквивалентно: непрерывность по норме эквивалентна Tendsto по норме eLp.

LaTeX

$$$\mathrm{Tendsto}_f (f) \leftrightarrow \mathrm{Tendsto}_f (eLpNorm(f- f_{lim}) )$$$

Lean4

theorem tendsto_Lp_iff_tendsto_eLpNorm' {ι} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → Lp E p μ) (f_lim : Lp E p μ) :
    fi.Tendsto f (𝓝 f_lim) ↔ fi.Tendsto (fun n => eLpNorm (⇑(f n) - ⇑f_lim) p μ) (𝓝 0) :=
  by
  rw [tendsto_iff_dist_tendsto_zero]
  simp_rw [dist_def]
  rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]
  rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
  exact Lp.eLpNorm_ne_top _

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