English
Let s be a signed measure, μ a measure, and r a real number. Then the singular part of r times s with respect to μ is r times the singular part of s with respect to μ.
Русский
Пусть s — знаковая мера, μ — мера, а r — вещественное число. Тогда сингулярная часть от r·s по отношению к μ равна r·(s сингулярная часть μ).
LaTeX
$$$ (r \\cdot s).singularPart \\mu = r \\cdot (s.singularPart \\mu) $$$
Lean4
nonrec theorem singularPart_smul (s : SignedMeasure α) (μ : Measure α) (r : ℝ) :
(r • s).singularPart μ = r • s.singularPart μ := by
cases le_or_gt 0 r with
| inl hr =>
lift r to ℝ≥0 using hr
exact singularPart_smul_nnreal s μ r
| inr hr =>
rw [singularPart, singularPart]
conv_lhs =>
congr
· congr
· rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
· congr
· rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def, ← neg_smul,
Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]
