Commit 2026-03-06 16:20 c542d63b

View on Github →

feat(ProbabilityTheory): add Poisson limit theorem (#33449)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Probability/Distributions/Poisson.lean to Mathlib/Probability/Distributions/Poisson/Basic.lean

added theorem ProbabilityTheory.poissonPMFReal_ofReal_eq_poissonPMF

Created Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean

added theorem ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop

added theorem ProbabilityTheory.tendsto_choose_mul_pow_atTop

added theorem ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop

added theorem ProbabilityTheory.tendsto_zero_of_tendsto_mul_atTop

Modified Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

added theorem PMF.binomial_apply_of_le

Modified docs/1000.yaml