Commit 2024-03-13 15:40 2731f819

View on Github →

feat: add set_lintegral variants of lintegral lemmas (#11274)

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.set_lintegral_rnDeriv_mul

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.set_lintegral_withDensity_eq_lintegral_mul₀'

added theorem MeasureTheory.set_lintegral_withDensity_eq_lintegral_mul₀