mathlib

8f863f6b - feat(measure_theory/decomposition/jordan): the Jordan decomposition theorem for signed measures (#8645)

feat(measure_theory/decomposition/jordan): the Jordan decomposition theorem for signed measures (#8645) This PR proves the Jordan decomposition theorem for signed measures, that is, given a signed measure `s`, there exists a unique pair of mutually singular measures `μ` and `ν`, such that `s = μ - ν`.