eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top

English

For 0 < p, eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top provides an upper bound of liminf by eLpNorm.

Русский

При 0 < p верхняя граница лиминф задаётся через eLpNorm.

LaTeX

$$$eLpNorm f_lim^{\,+} \leq \liminf_{n} eLpNorm (f_n)$$$

Lean4

theorem eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top {ι} [Nonempty ι] [Countable ι] [LinearOrder ι]
    {f : ι → α → E} {f_lim : α → E} (h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
    eLpNorm f_lim ∞ μ ≤ atTop.liminf fun n => eLpNorm (f n) ∞ μ :=
  by
  rw [eLpNorm_exponent_top_lim_eq_essSup_liminf h_lim]
  simp_rw [eLpNorm_exponent_top, eLpNormEssSup]
  exact ENNReal.essSup_liminf_le _

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