eLpNorm_le_mul_eLpNorm_of_ae_le_mul

English

If |f| ≤ c|g| a.e., then eLpNorm f p μ ≤ c · eLpNorm g p μ for any p≥0, including cases with c ∈ ENNReal.

Русский

Если |f| ≤ c|g| почти всюду, то eLpNorm f p μ ≤ c · eLpNorm g p μ для любого p≥0, включая случаи с c ∈ ENNReal.

LaTeX

$$$\forall p,\; (\forall^{\ast} x, \|f(x)\| ≤ c \|g(x)\|) \Rightarrow eLpNorm f p μ ≤ c \cdot eLpNorm g p μ$$$

Lean4

theorem eLpNorm_le_mul_eLpNorm_of_ae_le_mul {f : α → F} {g : α → G} {c : ℝ} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ c * ‖g x‖)
    (p : ℝ≥0∞) : eLpNorm f p μ ≤ ENNReal.ofReal c * eLpNorm g p μ :=
  eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
    (h.mono fun _x hx => hx.trans <| mul_le_mul_of_nonneg_right c.le_coe_toNNReal (norm_nonneg _))
    _
      -- TODO: eventually, deprecate and remove the nnnorm version

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