Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-27 14:02 7cfc9872

View on Github →

feat(measure_theory/decomposition/radon_nikodym): the Radon-Nikodym theorem (#8763) The Radon-Nikodym theorem 🎉

Estimated changes

Modified src/measure_theory/decomposition/lebesgue.lean

deleted def measure_theory.measure.have_lebesgue_decomposition

modified theorem measure_theory.measure.have_lebesgue_decomposition_add

deleted theorem measure_theory.measure.have_lebesgue_decomposition_of_finite_measure

modified theorem measure_theory.measure.have_lebesgue_decomposition_spec

Created src/measure_theory/decomposition/radon_nikodym.lean

added theorem measure_theory.measure.absolutely_continuous_iff_with_density_radon_nikodym_derive_eq

added theorem measure_theory.measure.with_density_radon_nikodym_deriv_eq