Commit 2026-03-31 14:02 f7b9474b

refactor: define the Poisson measure via a sum of Dirac masses (#36374) Change the definition of poissonMeasure r to be Measure.sum (fun n ↦ ENNReal.ofReal (exp (-r) * r ^ n / (n)!) • (.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 poissonMeasure.