Commit 2025-03-21 16:27 2e460a0c

View on Github →

feat: lemmas about Measure.dirac (#23071)

Estimated changes

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

added theorem MeasureTheory.integrable_dirac'

added theorem MeasureTheory.integrable_dirac

modified theorem MeasureTheory.integrable_zero_measure

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean

added theorem aestronglyMeasurable_dirac

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

added theorem MeasureTheory.aemeasurable_dirac

Modified Mathlib/Probability/Moments/Basic.lean

added theorem ProbabilityTheory.mgf_dirac'