eLpNorm_exponent_top_lim_eq_essSup_liminf

English

Alternative formulation relating eLpNorm with essSup of liminf for p = ∞.

Русский

Альтернативная формулировка связи eLpNorm и essSup-лиминф для p = ∞.

LaTeX

$$$eLpNorm_{\infty}(f_{lim}) = \operatorname{essSup}_{a} \left(\liminf_{m} \|f_m(a)\|\right)$$$

Lean4

theorem eLpNorm_exponent_top_lim_eq_essSup_liminf {ι} [Nonempty ι] [LinearOrder ι] {f : ι → α → E} {f_lim : α → E}
    (h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
    eLpNorm f_lim ∞ μ = essSup (fun x => atTop.liminf fun m => ‖f m x‖ₑ) μ :=
  by
  rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
  refine essSup_congr_ae (h_lim.mono fun x hx => ?_)
  dsimp only
  apply (Tendsto.liminf_eq ..).symm
  exact (continuous_enorm.tendsto (f_lim x)).comp hx

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