Commit 2024-01-16 12:23 92f863e4

View on Github →

Feat : Add geometric distribution (#9561) Adds the geometric probability distribution

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Distributions/Geometric.lean

added def ProbabilityTheory.geometricMeasure

added def ProbabilityTheory.geometricPMF

added def ProbabilityTheory.geometricPMFReal

added theorem ProbabilityTheory.geometricPMFRealSum

added theorem ProbabilityTheory.geometricPMFReal_nonneg

added theorem ProbabilityTheory.geometricPMFReal_pos

added theorem ProbabilityTheory.isProbabilityMeasureGeometric

added theorem ProbabilityTheory.measurable_geometricPMFReal

added theorem ProbabilityTheory.stronglyMeasurable_geometricPMFReal