English
Let s be a signed measure on a measurable space. Then there exists a measurable set i such that the signed measure is nonnegative on i, is nonpositive on i^c, and the Jordan decomposition components are exactly the pos- and neg-parts restricted to i and i^c respectively.
Русский
Пусть s — подписанная мера на измеримом пространстве. Существует измеримое множество i такое, что s неотрицальна на i, s неотрицательна на i^c отрицательна, и компоненты разложения Йордана posPart и negPart совпадают с соответствующими ограничениями на i и i^c.
LaTeX
$$$$\exists i\; (i \text{ MeasurableSet})\; (0 \le_{i} s)\; (s \le_{i^{c}} 0)\; \; s^{+} = s^{\mathrm{toMeasureOfZeroLE}} i \; hi_1 \; hi_2 \\; \; s^{-} = s^{\mathrm{toMeasureOfLEZero}} i^{c} \; hi_1.compl \; hi_3.$$$$
Lean4
theorem toJordanDecomposition_spec (s : SignedMeasure α) :
∃ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ hi₁.compl hi₃ :=
by
set i := s.exists_compl_positive_negative.choose
obtain ⟨hi₁, hi₂, hi₃⟩ := s.exists_compl_positive_negative.choose_spec
exact ⟨i, hi₁, hi₂, hi₃, rfl, rfl⟩
