eLpNormEssSup_lt_top_of_ae_nnnorm_bound

English

If a function f is essentially bounded by a finite NNReal bound C almost everywhere, then its eLp norm ess sup is finite.

Русский

Если функция f почти всюду ограничена конечной границей C в NNReal, то её eLp-норма ess sup конечна.

LaTeX

$$$\text{Let } f:\alpha\to F \text{ and } C\in\mathbb{R}_{\ge 0}.\; (\forall^{\mathrm{a}} x\,\partial\mu,\; \|f(x)\|_{+}\le C) \Rightarrow eLpNormEssSup\; f\; \mu < \infty.$$$

Lean4

theorem eLpNormEssSup_lt_top_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) :
    eLpNormEssSup f μ < ∞ :=
  (eLpNormEssSup_le_of_ae_nnnorm_bound hfC).trans_lt ENNReal.coe_lt_top

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