Commit 2025-06-18 09:18 1fdbaf88

View on Github →

feat: missing API for measure theory (#26066) Grab bag of small useful lemmas in measure theory. Their need showed up in the formalization of Riemannian manifolds.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

added theorem MeasureTheory.setIntegral_measure_zero

deleted theorem MeasureTheory.setIntegral_zero_measure

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem ContinuousOn.aemeasurable₀

added theorem MeasureTheory.IntegrableOn.of_measure_zero

added theorem MeasureTheory.integrableOn_congr_set_ae

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem MeasureTheory.Measure.absolutelyContinuous_restrict

added theorem MeasureTheory.nullMeasurableSet_restrict

added theorem MeasureTheory.nullMeasurableSet_restrict_of_subset

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.withDensity_apply₀

Modified Mathlib/Probability/Kernel/Condexp.lean