haveLebesgueDecomposition_smul — Mathlib

English

If s has Lebesgue decomposition with μ, then r • s also has one for any r ≥ 0, with the positive/negative parts scaled accordingly.

Русский

Если s имеет разложение Лебега по μ, то r • s тоже имеет разложение для любого r ≥ 0; части масштабируются соответственно.

LaTeX

$$$s.HaveLebesgueDecomposition μ \Rightarrow (r \cdot s).HaveLebesgueDecomposition μ$ with posPart = r • s.posPart and negPart = r • s.negPart$$

Lean4

instance haveLebesgueDecomposition_smul (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    (r : ℝ≥0) : (r • s).HaveLebesgueDecomposition μ
    where
  posPart := by
    rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart]
    infer_instance
  negPart := by
    rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart]
    infer_instance

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