eLpNorm_smul_measure_of_ne_top — Mathlib

English

If p ≠ ∞, then for c ∈ ℝ≥0, eLpNorm f p (c • μ) = c^(p.toReal)⁻¹ · eLpNorm f p μ.

Русский

Если p ≠ ∞, то при c ∈ ℝ≥0: eLpNorm f p (c μ) = c^{p^{-1}} · eLpNorm f p μ.

LaTeX

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

Lean4

/-- See `eLpNorm_smul_measure_of_ne_top'` for a version with scalar multiplication by `ℝ≥0`. -/
theorem eLpNorm_smul_measure_of_ne_top {p : ℝ≥0∞} (hp_ne_top : p ≠ ∞) (f : α → ε) (c : ℝ≥0∞) :
    eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  · exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_ne_top c

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