Theorem MeasureTheory.Measure.set_lintegral_rnDeriv

Modification history

2024-06-29 15:21
Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
chore: rename set_lintegral to setLIntegral throughout mathlib (#14260) …
Deleted MeasureTheory.Measure.set_lintegral_rnDerivView on Github →
2023-11-14 12:32
Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
feat: generalize some lemmas using `withDensity_apply'` (#8383) …
Modified MeasureTheory.Measure.set_lintegral_rnDerivView on Github →
2023-11-02 08:18
Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
feat: properties of rnDeriv (#7675) …
Added MeasureTheory.Measure.set_lintegral_rnDerivView on Github →