Commit 2025-04-04 16:40 d5380c50

View on Github →

chore(IntegrableOn): drop a MeasurableSet assumption (#23672) ... in IntegrableOn.restrict. Also fix a typo in a docstring and golf away some uses of this lemma.

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

modified theorem MeasureTheory.IntegrableOn.restrict

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean