norm_le_of_ae_bound — Mathlib

English

If μ is finite, and ‖f x‖ ≤ c consistently a.e., then ‖f‖ ≤ c · ‖g‖ for appropriate f,g.

Русский

Если μ конечна и ‖f x‖ ≤ c · ‖g x‖ почти всюду, то ‖f‖ ≤ c · ‖g‖.

LaTeX

$$$[IsFiniteMeasure μ] \Rightarrow (hfC: ∀^{\mathrm{ae}} x, \|f(x)\| ≤ C) \Rightarrow \|f\| ≤ (μ(\mathrm{univ}))^{1/p} · C$$$

Lean4

theorem norm_le_of_ae_bound [IsFiniteMeasure μ] {f : Lp E p μ} {C : ℝ} (hC : 0 ≤ C) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
    ‖f‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C :=
  by
  lift C to ℝ≥0 using hC
  have := nnnorm_le_of_ae_bound hfC
  rwa [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_rpow] at this

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