eLpNorm_smul_measure_of_ne_top' — Mathlib

English

A variant of the above for NNReal scalars and p as ENNReal, giving the same scaling law with exponent reciprocal.

Русский

Вариант в отношении NNReal-скаляров и p как ENNReal, дающий ту же зависимость масштабирования через обратную дробь.

LaTeX

$$$p \\neq ∞ \\Rightarrow eLpNorm s p (c \\cdot μ) = c^{p^{-1}} \\cdot eLpNorm s p μ,$ where c ∈ NNReal.$$

Lean4

/-- See `eLpNorm_smul_measure_of_ne_top'` for a version with scalar multiplication by `ℝ≥0∞`. -/
theorem eLpNorm_smul_measure_of_ne_top' (hp : p ≠ ∞) (c : ℝ≥0) (f : α → ε) :
    eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ :=
  by
  have : 0 ≤ p.toReal⁻¹ := by positivity
  refine (eLpNorm_smul_measure_of_ne_top hp ..).trans ?_
  simp [ENNReal.smul_def, ENNReal.coe_rpow_of_nonneg, this]

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