eLpNorm_smul_measure_of_ne_zero — Mathlib

English

Let p be a finite or infinite exponent, and c ≠ 0. Then scaling the measure by c scales eLpNorm by c^(1/p).

Русский

Пусть p конечен или бесконечен, и c ≠ 0. Тогда масштабирование меры на c масштабирует eLpNorm на c^(1/p).

LaTeX

$$$c \\neq 0 \\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 ^ (1 / p).toReal • eLpNorm f p μ :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  by_cases hp_top : p = ∞
  · simp [hp_top, eLpNormEssSup_smul_measure hc]
  exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c

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