English
For s a signed measure and μ a measure, the positive and negative parts of the Jordan decomposition, when restricted to μ, are mutually singular with respect to each other.
Русский
Для знаковой меры s и меры μ части положительная и отрицательная от Джордановского разложения, при ограничении к μ, взаимно сингулярны между собой.
LaTeX
$$$s.toJordanDecomposition.posPart.singularPart μ \perp s.toJordanDecomposition.negPart.singularPart μ$$$
Lean4
theorem singularPart_mutuallySingular (s : SignedMeasure α) (μ : Measure α) :
s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ :=
by
by_cases hl : s.HaveLebesgueDecomposition μ
· obtain ⟨i, hi, hpos, hneg⟩ := s.toJordanDecomposition.mutuallySingular
rw [s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ] at hpos
rw [s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ] at hneg
rw [add_apply, add_eq_zero] at hpos hneg
exact ⟨i, hi, hpos.1, hneg.1⟩
· rw [not_haveLebesgueDecomposition_iff] at hl
rcases hl with hp | hn
· rw [Measure.singularPart, dif_neg hp]
exact MutuallySingular.zero_left
· rw [Measure.singularPart, Measure.singularPart, dif_neg hn]
exact MutuallySingular.zero_right
