Commit 2024-01-10 17:15 7f983515

View on Github →

Feat : Define the Poisson distribution (#9554) Add the Poisson probability distribution for non-negative rate r

PMF
Measure
Basic API

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Distributions/Poisson.lean

added theorem ProbabilityTheory.measurable_poissonPmfReal

added def ProbabilityTheory.poissonMeasure

added def ProbabilityTheory.poissonPmf

added def ProbabilityTheory.poissonPmfReal

added theorem ProbabilityTheory.poissonPmfRealSum

added theorem ProbabilityTheory.poissonPmfReal_nonneg

added theorem ProbabilityTheory.poissonPmfReal_pos

added theorem ProbabilityTheory.stronglyMeasurable_poissonPmfReal