Commit 2021-08-10 18:08 32735ca2

View on Github →

feat(measure_theory/measure_space): add mutually singular measures (#8605) This PR defines mutually_singular for measures. This is useful for Jordan and Lebesgue decomposition.

Estimated changes

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure.mutually_singular.add

added theorem measure_theory.measure.mutually_singular.smul

added theorem measure_theory.measure.mutually_singular.symm

added theorem measure_theory.measure.mutually_singular.zero

added def measure_theory.measure.mutually_singular