mathlib3

7b27f461 - feat(measure_theory/vector_measure): a signed measure restricted on a positive set is a unsigned measure (#8597)

feat(measure_theory/vector_measure): a signed measure restricted on a positive set is a unsigned measure (#8597) This PR defines `signed_measure.to_measure` which is the measure corresponding to a signed measure restricted on some positive set. This definition is useful for the Jordan decomposition theorem.