Commit 2024-11-08 16:56 225ff188

View on Github →

feat: any function is integrable on a finset wrt to a finite measure (#18415) Also restate integral_finset in terms of IntegrableOn From PFR

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space.lean

modified theorem MeasureTheory.Integrable.restrict

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

modified theorem MeasureTheory.Integrable.integrableOn

added theorem MeasureTheory.IntegrableOn.finset

added theorem MeasureTheory.IntegrableOn.of_finite

Modified Mathlib/Probability/ProbabilityMassFunction/Integrals.lean