Commit 2021-08-18 00:41 ce965a55

View on Github →

feat(measure_theory/decomposition/lebesgue): the Lebesgue decomposition theorem (#8687) This PR proves the existence and uniqueness of the Lebesgue decompositions theorem which is the last step before proving the Radon-Nikodym theorem 🎉

Estimated changes

Created src/measure_theory/decomposition/lebesgue.lean

added theorem measure_theory.measure.eq_radon_nikodym_deriv

added theorem measure_theory.measure.eq_singular_part

added theorem measure_theory.measure.exists_positive_of_not_mutually_singular

added def measure_theory.measure.have_lebesgue_decomposition

added theorem measure_theory.measure.have_lebesgue_decomposition_add

added theorem measure_theory.measure.have_lebesgue_decomposition_of_finite_measure

added theorem measure_theory.measure.have_lebesgue_decomposition_spec

added theorem measure_theory.measure.lebesgue_decomposition.max_measurable_le

added def measure_theory.measure.lebesgue_decomposition.measurable_le

added def measure_theory.measure.lebesgue_decomposition.measurable_le_eval

added theorem measure_theory.measure.lebesgue_decomposition.sup_mem_measurable_le

added theorem measure_theory.measure.lebesgue_decomposition.supr_le_le

added theorem measure_theory.measure.lebesgue_decomposition.supr_mem_measurable_le'

added theorem measure_theory.measure.lebesgue_decomposition.supr_mem_measurable_le

added theorem measure_theory.measure.lebesgue_decomposition.supr_monotone'

added theorem measure_theory.measure.lebesgue_decomposition.supr_monotone

added theorem measure_theory.measure.lebesgue_decomposition.supr_succ_eq_sup

added theorem measure_theory.measure.lebesgue_decomposition.zero_mem_measurable_le

added theorem measure_theory.measure.measurable_radon_nikodym_deriv

added theorem measure_theory.measure.mutually_singular_singular_part

added def measure_theory.measure.radon_nikodym_deriv

added def measure_theory.measure.singular_part

added theorem measure_theory.measure.singular_part_le

added theorem measure_theory.measure.with_density_radon_nikodym_deriv_le

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.with_density_zero

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.finite_measure_of_le

added theorem measure_theory.measure.sigma_finite_of_le

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.exists_measure_pos_of_not_measure_Union_null