Commit 2023-11-12 17:09 708c4de3

View on Github →

feat(MeasureTheory): integrals of rnDeriv without absolute continuity (#8343) Add Lemmas about Lebesgue and Bochner integrals of rnDeriv without absolute continuity assumptions. Also remove a duplicate lemma I introduced in a previous PR: set_integral_toReal_rnDeriv was already there under the name withDensity_rnDeriv_toReal_eq. I kept the name set_integral_toReal_rnDeriv .

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.Measure.integrableOn_toReal_rnDeriv

modified theorem MeasureTheory.Measure.integral_toReal_rnDeriv

modified theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv

added theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_eq_withDensity

added theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_le

added theorem MeasureTheory.Measure.set_lintegral_rnDeriv_le

deleted theorem MeasureTheory.Measure.withDensity_rnDeriv_toReal_eq