eLpNorm_smul_measure_of_ne_zero' — Mathlib

English

If p ≠ ∞, then scaling the measure by c yields eLpNorm f p (c • μ) = c^(1/p) · eLpNorm f p μ for c ≠ 0.

Русский

Если p ≠ ∞, то умножение меры на c дает eLpNorm f p (c μ) = c^(1/p) · eLpNorm f p μ при c ≠ 0.

LaTeX

$$$p \\neq \\infty \\Rightarrow eLpNorm f p (c \\cdot μ) = c^{1/p} \\cdot eLpNorm f p μ.$$$

Lean4

/-- See `eLpNorm_smul_measure_of_ne_zero` for a version with scalar multiplication by `ℝ≥0∞`. -/
theorem eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0} (hc : c ≠ 0) (f : α → ε) (p : ℝ≥0∞) (μ : Measure α) :
    eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ :=
  (eLpNorm_smul_measure_of_ne_zero (ENNReal.coe_ne_zero.2 hc) ..).trans (by simp; norm_cast)

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