Commit 2021-08-28 16:48 1aaff8da

View on Github →

feat(measure_theory/decomposition/lebesgue): Lebesgue decomposition for sigma-finite measures (#8875) This PR shows sigma-finite measures have_lebesgue_decomposition. With this instance, absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq will provide the Radon-Nikodym theorem for sigma-finite measures.

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

added theorem measurable.ennreal_tsum'

Modified src/measure_theory/decomposition/lebesgue.lean

added theorem measure_theory.measure.have_lebesgue_decomposition_of_finite_measure

Modified src/measure_theory/decomposition/radon_nikodym.lean

added theorem measure_theory.measure.absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq

deleted theorem measure_theory.measure.absolutely_continuous_iff_with_density_radon_nikodym_derive_eq

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.with_density_indicator

added theorem measure_theory.with_density_tsum

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.measure.sum_add_sum

added theorem measure_theory.measure.sum_congr