English
The total variation of the singular part of a signed measure equals the sum of the singular parts of its positive and negative Jordan components.
Русский
Полная вариация сингулярной части знаковой меры равна сумме сингулярных частей положительной и отрицательной частей Джорданового разложения.
LaTeX
$$$(s.singularPart μ).totalVariation = s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ$$
Lean4
theorem singularPart_totalVariation (s : SignedMeasure α) (μ : Measure α) :
(s.singularPart μ).totalVariation =
s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ :=
by
have :
(s.singularPart μ).toJordanDecomposition =
⟨s.toJordanDecomposition.posPart.singularPart μ, s.toJordanDecomposition.negPart.singularPart μ,
singularPart_mutuallySingular s μ⟩ :=
by
refine JordanDecomposition.toSignedMeasure_injective ?_
rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
rw [totalVariation, this]
