singularPart_smul_nnreal — Mathlib

English

For s with μ, scalar multiply by NNReal r commutes with taking the singular part: (r • s).singularPart μ = r • s.singularPart μ.

Русский

При умножении на NNReal r сначала берем сингулярную часть, затем домножаем, т.е. (r • s).singularPart μ = r • s.singularPart μ.

LaTeX

$$$ (r \cdot s).singularPart μ = r \cdot s.singularPart μ $$$

Lean4

theorem singularPart_smul_nnreal (s : SignedMeasure α) (μ : Measure α) (r : ℝ≥0) :
    (r • s).singularPart μ = r • s.singularPart μ :=
  by
  rw [singularPart, singularPart, smul_sub, ← toSignedMeasure_smul, ← toSignedMeasure_smul]
  conv_lhs =>
    congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

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