eLpNorm_le_of_ae_bound — Mathlib

English

If f is bounded by a real constant C almost everywhere, then the eLp norm is bounded by μ(univ)^{1/p} times ENNReal.ofReal C.

Русский

Если f ограничена до действительного числа C, тогда eLpNorm f ≤ μ(univ)^{1/p} · ENNReal.ofReal(C).

LaTeX

$$$\text{If } hfC:\forall^{\mathrm{a}} x\partial\mu,\; \|f(x)\| ≤ C, \text{ then } eLpNorm\; f\; p\; μ ≤ μ(\mathrm{Set.univ})^{\frac{1}{p}} \cdot ENNReal.ofReal(C).$$$

Lean4

theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
    eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C :=
  by
  rw [← mul_comm]
  exact eLpNorm_le_of_ae_nnnorm_bound (hfC.mono fun x hx => hx.trans C.le_coe_toNNReal)

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