haveLebesgueDecomposition_smul_real

English

If s has Lebesgue decomposition with μ, then r • s has one for any real r, with the sign-adjusted parts handled depending on the sign of r.

Русский

Если s имеет разложение Лебега относительно μ, то r • s имеет разложение для любого действительного r, причём части меняются в зависимости от знака r.

LaTeX

$$$s.HaveLebesgueDecomposition μ \Rightarrow (r \cdot s).HaveLebesgueDecomposition μ$ with appropriate adjustment for sign of r$$

Lean4

instance haveLebesgueDecomposition_smul_real (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    (r : ℝ) : (r • s).HaveLebesgueDecomposition μ :=
  by
  by_cases hr : 0 ≤ r
  · lift r to ℝ≥0 using hr
    exact s.haveLebesgueDecomposition_smul μ _
  · rw [not_le] at hr
    refine
      { posPart := by
          rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_posPart_neg _ _ hr]
          infer_instance
        negPart := by
          rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_negPart_neg _ _ hr]
          infer_instance }

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