Poisson limit of binomial probabilities

This file proves a Poisson limit theorem.

Fix k : ℕ. Assuming n * p n → r as n → ∞, we show PMF.binomial (p n) (h n) n (Fin.ofNat (n + 1) k) → poissonPMF r k.

Main results

• ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop: if n * p n → r, then n.choose k * (p n)^k * (1 - p n)^(n - k) → exp (-r) * r^k / k!.

• ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop: convergence of PMF.binomial to poissonPMF in ℝ≥0∞ under the natural hypotheses (p n ≤ 1 and n * p n → r).

Tags

binomial distribution, Poisson distribution, asymptotics, limits, probability mass function

theorem ProbabilityTheory.tendsto_zero_of_tendsto_mul_atTop {p : ℕ → ℝ} {r : ℝ} (hr : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop (nhds r)) : Filter.Tendsto p Filter.atTop (nhds 0)

theorem ProbabilityTheory.tendsto_choose_mul_pow_atTop {p : ℕ → ℝ} {r : ℝ} (k : ℕ) (hr : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop (nhds r)) : Filter.Tendsto (fun (n : ℕ) => ↑(n.choose k) * p n ^ k) Filter.atTop (nhds (r ^ k / ↑k.factorial))

theorem ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop {p : ℕ → ℝ} {r : ℝ} (k : ℕ) (hr : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop (nhds r)) : Filter.Tendsto (fun (n : ℕ) => ↑(n.choose k) * p n ^ k * (1 - p n) ^ (n - k)) Filter.atTop (nhds (Real.exp (-r) * r ^ k / ↑k.factorial))

Poisson limit Theorem: If n * p n → r as n → ∞. Then (n.choose k) * (p n)^k * (1 - p n)^(n - k) → exp (-r) * r^k / k!.

theorem ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop (k : ℕ) {r : NNReal} {p : ℕ → NNReal} (h : ∀ (n : ℕ), p n ≤ 1) (hr : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop (nhds r)) : Filter.Tendsto (fun (n : ℕ) => (PMF.binomial (p n) ⋯ n) (Fin.ofNat (n + 1) k)) Filter.atTop (nhds ((poissonPMF r) k))

Another version of Poisson Limit Theorem: convergence of PMF.binomial to poissonPMF in ℝ≥0∞ under the natural hypotheses (∀ n, p n ≤ 1 and r ≥ 0).