eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm

English

When multiplying a scalar function φ with f, the Lp-norm is controlled by the product of the scalar's norm and the top Lp-norm of f.

Русский

При умножении на скаляр φ нормa Lp управляется как произведение нормы φ и верхней нормы Lp f.

LaTeX

$$$eLpNorm (φ \\cdot f) p μ ≤ eLpNorm φ ∞ μ · eLpNorm f p μ$$$

Lean4

theorem eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm (p : ℝ≥0∞) (hf : AEStronglyMeasurable f μ) (φ : α → 𝕜) :
    eLpNorm (φ • f) p μ ≤ eLpNorm φ ∞ μ * eLpNorm f p μ := by
  simpa using
    (eLpNorm_le_eLpNorm_top_mul_eLpNorm p φ hf (· • ·) 1 (.of_forall fun _ => by simpa using nnnorm_smul_le _ _) :)

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