Commit 2026-08-26 08:21 0fa18d49

refactor: change the default value of Measure.map to a Dirac mass (#42322) MeasureTheory.Measure.mapf µ is currently defined to be 0 if f is not a.e.-measurable. This PR changes it to be an arbitrary Dirac mass (except when µ = 0, where it is still defined to be 0 to keep MeasureTheory.Measure.map_zero). This allows to have an instance saying that mapping a probability measure yields a probability measure, which in turns allows to define MeasureTheory.ProbabilityMeasure.map without requiring a measurability hypothesis while still enjoying MeasureTheory.ProbabilityMeasure.toMeasure_map as a simp lemma. In order to do the change Measure.dirac must be available before Measure.map in the import chain. To do that we split the current Measure.Dirac file in two files, one containing the definition and very basic API in order to prove that it is a probability measure, the other containing the remainder. This change also required to add some measurability hypotheses along the way, which is the main part of the diff. The main one is probably MeasureTheory.Measure.map_smul which now requires measurability of the map. We also replaced the definition of MeasureTheory.pdf.IsUniform to use HasLaw, and added an aemeasurable field in HasGaussianLaw.