eLpNorm_le_mul_eLpNorm_of_ae_le_mul'

English

If |f| ≤ c|g| a.e., then eLpNorm f p μ ≤ c · eLpNorm g p μ for all p in ENNReal.

Русский

Если |f| ≤ c|g| почти всюду, то eLpNorm f p μ ≤ c · eLpNorm g p μ для всех p в ENNReal.

LaTeX

$$$\text{ae bound: } \|f\| ≤ c \|g\| \Rightarrow eLpNorm f p μ ≤ c \cdot eLpNorm g p μ$$$

Lean4

/-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ`, then `eLpNorm f p μ ≤ c * eLpNorm g p μ`.

This version assumes `c` is finite, but requires no measurability hypothesis on `g`. -/
theorem eLpNorm_le_mul_eLpNorm_of_ae_le_mul' {f : α → ε} {g : α → ε'} {c : ℝ≥0} (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ)
    (p : ℝ≥0∞) : eLpNorm f p μ ≤ c * eLpNorm g p μ := by apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul' h

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