English
A Hahn decomposition exists with observable sign on i and its complement, illustrating the split of μ into positive and negative parts.
Русский
Существование разложения Хана с явной сигнатурой на i и его дополнении, демонстрирующее разложение меры на положительную и отрицательную части.
LaTeX
$$$\exists i,j, \ MeasurableSet i, \; MeasurableSet j, \ 0 \le[i] s, \ s \le[i^c] 0, \ 0 \le[j] s, \ s \le[j^c] 0, \ IsCompl i j$$$
Lean4
/-- A Jordan decomposition provides a Hahn decomposition. -/
theorem exists_compl_positive_negative :
∃ S : Set α,
MeasurableSet S ∧ j.toSignedMeasure ≤[S] 0 ∧ 0 ≤[Sᶜ] j.toSignedMeasure ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0 :=
by
obtain ⟨S, hS₁, hS₂, hS₃⟩ := j.mutuallySingular
refine ⟨S, hS₁, ?_, ?_, hS₂, hS₃⟩
· refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_
rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def,
show j.posPart A = 0 from nonpos_iff_eq_zero.1 (hS₂ ▸ measure_mono hA₁), ENNReal.toReal_zero, zero_sub, neg_le,
zero_apply, neg_zero]
exact ENNReal.toReal_nonneg
· refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_
rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def (μ := j.negPart),
show j.negPart A = 0 from nonpos_iff_eq_zero.1 (hS₃ ▸ measure_mono hA₁), ENNReal.toReal_zero, sub_zero]
exact ENNReal.toReal_nonneg
