English
The map from a Jordan decomposition to the corresponding signed measure is injective.
Русский
Отображение разложения Йордана в соответствующую подписанную меру инъективно.
LaTeX
$$$$ \forall j_1\; j_2:\text{JordanDecomposition}(\alpha),\; j_1.toSignedMeasure = j_2.toSignedMeasure \Rightarrow j_1 = j_2. $$$$
Lean4
/-- The Jordan decomposition of a signed measure is unique. -/
theorem toSignedMeasure_injective : Injective <| @JordanDecomposition.toSignedMeasure α _ := by
/- The main idea is that two Jordan decompositions of a signed measure provide two
Hahn decompositions for that measure. Then, from `of_symmDiff_compl_positive_negative`,
the symmetric difference of the two Hahn decompositions has measure zero, thus, allowing us to
show the equality of the underlying measures of the Jordan decompositions. -/
intro j₁ j₂ hj
obtain ⟨S, hS₁, hS₂, hS₃, hS₄, hS₅⟩ := j₁.exists_compl_positive_negative
obtain ⟨T, hT₁, hT₂, hT₃, hT₄, hT₅⟩ := j₂.exists_compl_positive_negative
rw [← hj] at hT₂ hT₃
obtain ⟨hST₁, -⟩ :=
of_symmDiff_compl_positive_negative hS₁.compl hT₁.compl ⟨hS₃, (compl_compl S).symm ▸ hS₂⟩
⟨hT₃, (compl_compl T).symm ▸ hT₂⟩
-- it suffices to show the Jordan decompositions have the same positive parts
refine eq_of_posPart_eq_posPart ?_ hj
ext1 i hi
have hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ) :=
by
rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hS₁.compl), measureReal_def (μ := j₁.negPart),
show j₁.negPart (i ∩ Sᶜ) = 0 from nonpos_iff_eq_zero.1 (hS₅ ▸ measure_mono Set.inter_subset_right),
ENNReal.toReal_zero, sub_zero]
conv_lhs => rw [← Set.inter_union_compl i S]
rw [measureReal_union, measureReal_def,
show j₁.posPart (i ∩ S) = 0 from nonpos_iff_eq_zero.1 (hS₄ ▸ measure_mono Set.inter_subset_right),
ENNReal.toReal_zero, zero_add]
·
refine
Set.disjoint_of_subset_left Set.inter_subset_right
(Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)
· exact hi.inter hS₁.compl
have hμ₂ : j₂.posPart.real i = j₂.toSignedMeasure (i ∩ Tᶜ) :=
by
rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hT₁.compl), measureReal_def (μ := j₂.negPart),
show j₂.negPart (i ∩ Tᶜ) = 0 from nonpos_iff_eq_zero.1 (hT₅ ▸ measure_mono Set.inter_subset_right),
ENNReal.toReal_zero, sub_zero]
conv_lhs => rw [← Set.inter_union_compl i T]
rw [measureReal_union, measureReal_def,
show j₂.posPart (i ∩ T) = 0 from nonpos_iff_eq_zero.1 (hT₄ ▸ measure_mono Set.inter_subset_right),
ENNReal.toReal_zero, zero_add]
·
exact
Set.disjoint_of_subset_left Set.inter_subset_right
(Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)
· exact hi.inter hT₁.compl
rw [← measureReal_eq_measureReal_iff, hμ₁, hμ₂, ← hj]
exact of_inter_eq_of_symmDiff_eq_zero_positive hS₁.compl hT₁.compl hi hS₃ hT₃ hST₁
