eLpNorm'_smul_measure — Mathlib

English

For p ≥ 0, and c ≥ 0, the norm eLpNorm' scales under scalar measure multiplication by c: eLpNorm' f p (c • μ) = c^(1/p) · eLpNorm' f p μ.

Русский

При p ≥ 0 и c ≥ 0 норма eLpNorm' масштабируется при умножении меры на c: eLpNorm' f p (c • μ) = c^(1/p) · eLpNorm' f p μ.

LaTeX

$$$p \\ge 0 \\Rightarrow eLpNorm'(f,p, c\\cdot\\mu) = c^{1/p} \\cdot eLpNorm'(f,p, \\mu).$$$

Lean4

theorem eLpNorm'_smul_measure {p : ℝ} (hp : 0 ≤ p) {f : α → ε} (c : ℝ≥0∞) :
    eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ := by simp [eLpNorm', ENNReal.mul_rpow_of_nonneg, hp]

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