eLpNorm_lim_le_liminf_eLpNorm — Mathlib

English

The limit inferior of Lp-norms controls the norm of the limit in Lp.

Русский

Границы лимина в Lp управляют нормой предела в Lp.

LaTeX

$$$eLpNorm( f_{lim}) \le \liminf_{n} eLpNorm(f_n)$$$

Lean4

theorem eLpNorm_lim_le_liminf_eLpNorm {f : ℕ → α → E} (hf : ∀ n, AEStronglyMeasurable (f n) μ) (f_lim : α → E)
    (h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
    eLpNorm f_lim p μ ≤ atTop.liminf fun n => eLpNorm (f n) p μ :=
  by
  obtain rfl | hp0 := eq_or_ne p 0
  · simp
  by_cases hp_top : p = ∞
  · simp_rw [hp_top]
    exact eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top h_lim
  simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
  have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
  exact eLpNorm'_lim_le_liminf_eLpNorm' hp_pos hf h_lim

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