English
The singular part of (−s) with respect to μ equals the negative of the singular part of s with respect to μ.
Русский
Сингулярная часть (−s) по μ равна −(s.singularPart μ).
LaTeX
$$$(-s).singularPart μ = -s.singularPart μ$$$
Lean4
theorem singularPart_neg (s : SignedMeasure α) (μ : Measure α) : (-s).singularPart μ = -s.singularPart μ :=
by
have h₁ :
((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure :=
by
refine toSignedMeasure_congr ?_
rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]
have h₂ :
((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
(s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure :=
by
refine toSignedMeasure_congr ?_
rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]
rw [singularPart, singularPart, neg_sub, h₁, h₂]
