English
The Jordan decomposition-to-signed-measure construction is inverse to the signed-measure-to-Jordan-decomposition construction; i.e., applying toJordanDecomposition followed by toSignedMeasure recovers the original signed measure.
Русский
Пусть для данного подписанного измерения s берется разложение Йордана, затем восстанавливается знаковая мера; полученная мера равна исходной.
LaTeX
$$$$ (s^{\mathrm{toJordanDecomposition}})^{\mathrm{toSignedMeasure}} = s. $$$$
Lean4
/-- **The Jordan decomposition theorem**: Given a signed measure `s`, there exists a pair of
mutually singular measures `μ` and `ν` such that `s = μ - ν`. In this case, the measures `μ`
and `ν` are given by `s.toJordanDecomposition.posPart` and
`s.toJordanDecomposition.negPart` respectively.
Note that we use `MeasureTheory.JordanDecomposition.toSignedMeasure` to represent the
signed measure corresponding to
`s.toJordanDecomposition.posPart - s.toJordanDecomposition.negPart`. -/
@[simp]
theorem toSignedMeasure_toJordanDecomposition (s : SignedMeasure α) : s.toJordanDecomposition.toSignedMeasure = s :=
by
obtain ⟨i, hi₁, hi₂, hi₃, hμ, hν⟩ := s.toJordanDecomposition_spec
simp only [JordanDecomposition.toSignedMeasure, hμ, hν]
ext k hk
rw [toSignedMeasure_sub_apply hk, toMeasureOfZeroLE_real_apply _ hi₂ hi₁ hk,
toMeasureOfLEZero_real_apply _ hi₃ hi₁.compl hk]
simp only [sub_neg_eq_add]
rw [← of_union _ (MeasurableSet.inter hi₁ hk) (MeasurableSet.inter hi₁.compl hk), Set.inter_comm i, Set.inter_comm iᶜ,
Set.inter_union_compl _ _]
exact (disjoint_compl_right.inf_left _).inf_right _
