of_nnnorm_le_mul — Mathlib

English

For any p, if g is AEStronglyMeasurable and |f| ≤ c|g| a.e., then eLpNorm' f p μ ≤ c · eLpNorm' g p μ, including p=0,∞ cases handled by special lemmas.

Русский

Для любого p, если g AEStronglyMeasurable и |f| ≤ c|g| почти везде, тогда eLpNorm' f p μ ≤ c · eLpNorm' g p μ, включая покрытие случаев p=0 и p=∞.

LaTeX

$$$\text{AEStronglyMeasurable}(g,μ) \land (∀^{\ast} x, \|f(x)\| ≤ c \|g(x)\|) \Rightarrow eLpNorm'(f,p,μ) ≤ c · eLpNorm'(g,p,μ)$$$

Lean4

theorem of_nnnorm_le_mul {f : α → E} {g : α → F} {c : ℝ≥0} (hg : MemLp g p μ) (hf : AEStronglyMeasurable f μ)
    (hfg : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) : MemLp f p μ :=
  ⟨hf,
    (eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul hfg p).trans_lt <|
      ENNReal.mul_lt_top ENNReal.coe_lt_top hg.eLpNorm_lt_top⟩

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