Commit 2026-05-04 13:04 08bae77c

refactor: define the geometric distribution via a sum of Dirac masses (#36378) Change the definition of geometricMeasure p to be Measure.sum (fun n ↦ ENNReal.ofReal ((1 - p) ^ n * p)) • (.dirac n)) instead of using PMF. This allows to directly use API for measures instead of having to develop an API for PMF, which anyway is defined as a sum of Dirac masses. Also add some results about integrals against the geometricMeasure.