Commit 2025-06-23 08:19 761f9b55

feat(MeasureTheory/Decomposition): link the clipped sub of positive measures to Jordan decomposition (#23500) This introduces a new file Mathlib/MeasureTheory/Decomposition/JordanSub.lean which develops the Jordan decomposition of the signed measure μ.toSignedMeasure - ν.toSignedMeasure for finite measures μ and ν, expressing it as the pair (μ - ν, ν - μ) of mutually singular finite measures. The key tool is the Hahn decomposition theorem, which yields a measurable partition of the space where μ ≥ ν and ν ≥ μ. Some basic results of VectorMeasure are also provided such as restrict_neg, restrict_sub restrict_add_restrict_compl and Measure.toSignedMeasure_le_iff within the JordanSub.lean file. They could be moved to another more central place (I guess VectorMeasure/Basic.lean). Similarly, Measure.sub_zero could go to Sub.lean.