toSignedMeasure_smul — Mathlib

English

Scaling a Jordan decomposition by a nonnegative NNReal scales its signed measure accordingly.

Русский

Умножение разложения Джордана на неотрицательное NNReal масштабирует сигнальную меру.

LaTeX

$$$ (r \ge 0) \Rightarrow (r \cdot j)^{\mathrm{toSignedMeasure}} = r \cdot j^{\mathrm{toSignedMeasure}} $$$

Lean4

theorem toSignedMeasure_smul (r : ℝ≥0) : (r • j).toSignedMeasure = r • j.toSignedMeasure :=
  by
  ext1 i hi
  rw [VectorMeasure.smul_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, smul_sub, smul_posPart, smul_negPart, measureReal_nnreal_smul_apply,
    measureReal_nnreal_smul_apply]
  rfl

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