Poisson limit theorem

TheoremAnalytic core of Poisson convergence#✓fully proved

Let \(\lambda \ge 0\) be a real number, let \(k : \mathbb{N} \to \mathbb{N}\), and for each \(n\) let \(p_{n,i}\), \(0 \le i < k(n)\), be real numbers. Suppose that \(p_{n,i} \ge 0\) for all \(n\) and \(i\), that for every \(\varepsilon > 0\) we have \(p_{n,i} < \varepsilon\) for all \(i < k(n)\) once \(n\) is large enough, and that \(\sum_{i < k(n)} p_{n,i} \to \lambda\) as \(n \to \infty\). Then for every natural number \(j\), as \(n \to \infty\) the Poisson-binomial mass

\[\sum_{|A| = j} \prod_{i \in A} p_{n,i} \prod_{i \notin A} (1 - p_{n,i})\]

tends to \(e^{-\lambda} \lambda^j / j!\), where \(A\) runs over the \(j\)-element subsets of \(\{0, \dots, k(n) - 1\}\) and \(i \notin A\) ranges over the elements of that set not in \(A\).

Without the hypothesis \(p_{n,i} \ge 0\) the conclusion can fail.

theorem elem_symm_poly_tendsto_poisson
    (hp_nonneg : ∀ n i, 0 ≤ p n i)
    (hMaxTendsto : ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop, ∀ i : Fin (k n), p n i < ε)
    (hSumTendsto : Filter.Tendsto (fun n => ∑ i : Fin (k n), p n i) atTop (𝓝 (lam : ℝ)))
    (j : ℕ) :
    Filter.Tendsto (fun n => ∑ A ∈ (Finset.univ : Finset (Fin (k n))).powersetCard j,
        (∏ i ∈ A, p n i) * (∏ i ∈ Finset.univ \ A, (1 - p n i)))
      atTop (𝓝 (Real.exp (-(lam : ℝ)) * (lam : ℝ) ^ j / (Nat.factorial j : ℝ)))

DefinitionBinomial law as a probability measure#✓fully proved

The binomial law Bin(n, p) on ℝ, bundled as a probability measure.

noncomputable def binomialProbMeasure (n : ℕ) (p : I) : ProbabilityMeasure ℝ :=
  ⟨Bin(ℝ, n, p), inferInstance⟩

Used by 3

Used byBinomial approximation to the Poisson law · Characteristic function of a binomial law · Convergence of characteristic functions to the Poisson law

DefinitionPoisson law as a probability measure#✓fully proved

The Poisson law of rate λ on ℝ, bundled as a probability measure.

noncomputable def poissonProbMeasure (lam : ℝ≥0) : ProbabilityMeasure ℝ :=
  ⟨Po(ℝ, lam), inferInstance⟩

Used by 3

Used byCharacteristic function of a Poisson law · Poisson convergence in law (binomial approximation) · Convergence of characteristic functions to the Poisson law

DefinitionSuccess probability of the binomial approximation to Poisson#✓fully proved

The success probability λ / (n + λ) used in the binomial approximation to the Poisson law. It lies in [0, 1] for every n, and n * pₙ → λ.

noncomputable def poissonApproxProb (lam : ℝ≥0) (n : ℕ) : I :=
  ⟨(lam : ℝ) / ((n : ℝ) + (lam : ℝ)),
    ⟨div_nonneg lam.coe_nonneg (by positivity),
     div_le_one_of_le₀ (by
       have h : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
       linarith) (by positivity)⟩⟩

Used by 3

Used byBinomial approximation to the Poisson law · Convergence of characteristic functions to the Poisson law · Mean of the binomial approximation tends to the Poisson rate

DefinitionBinomial approximation to the Poisson law#✓fully proved

The binomial law Bin(n, λ / (n + λ)) on ℝ.

noncomputable def binomialPoissonApprox (lam : ℝ≥0) (n : ℕ) : ProbabilityMeasure ℝ :=
  binomialProbMeasure n (poissonApproxProb lam n)

Uses 2 · Used by 2

Statement usesBinomial law as a probability measure · Success probability of the binomial approximation to Poisson

Used byPoisson convergence in law (binomial approximation) · Convergence of characteristic functions to the Poisson law

TheoremCharacteristic function of a binomial law#✓fully proved

φ_{Bin(n, p)}(t) = ((1 - p) + p * e^{it})ⁿ.

theorem charFun_binomialProbMeasure (n : ℕ) (p : I) (t : ℝ) :
    charFun (binomialProbMeasure n p : Measure ℝ) t =
      ((1 - (p : ℝ)) + (p : ℝ) * Complex.exp (↑t * Complex.I)) ^ n

Uses 2 · Used by 1

Statement usesBinomial law as a probability measure

Proof usesCharacteristic function of the real-valued binomial distribution

Used byConvergence of characteristic functions to the Poisson law

TheoremCharacteristic function of a Poisson law#✓fully proved

φ_{Poisson(λ)}(t) = exp(λ * (e^{it} - 1)).

theorem charFun_poissonProbMeasure (lam : ℝ≥0) (t : ℝ) :
    charFun (poissonProbMeasure lam : Measure ℝ) t =
      Complex.exp (↑lam * (Complex.exp (↑t * Complex.I) - 1))

Uses 1 · Used by 1

Statement usesPoisson law as a probability measure

Used byConvergence of characteristic functions to the Poisson law

TheoremMean of the binomial approximation tends to the Poisson rate#✓fully proved

The expected number of successes tends to the rate: n * (λ / (n + λ)) → λ.

theorem tendsto_mul_poissonApproxProb (lam : ℝ≥0) :
    Tendsto (fun n : ℕ => (n : ℝ) * (poissonApproxProb lam n : ℝ)) atTop
      (𝓝 (lam : ℝ))

Uses 1 · Used by 1

Statement usesSuccess probability of the binomial approximation to Poisson

Used byConvergence of characteristic functions to the Poisson law

TheoremConvergence of characteristic functions to the Poisson law#✓fully proved

The characteristic functions of the approximating binomial laws converge pointwise to the characteristic function of the Poisson law.

theorem tendsto_charFun_binomialPoissonApprox (lam : ℝ≥0) (t : ℝ) :
    Tendsto (fun n => charFun (binomialPoissonApprox lam n : Measure ℝ) t) atTop
      (𝓝 (charFun (poissonProbMeasure lam : Measure ℝ) t))

Uses 7 · Used by 1

Statement usesBinomial approximation to the Poisson law · Poisson law as a probability measure

Proof usesBinomial law as a probability measure · Characteristic function of a binomial law · Characteristic function of a Poisson law · Success probability of the binomial approximation to Poisson · Mean of the binomial approximation tends to the Poisson rate

Used byPoisson convergence in law (binomial approximation)

TheoremPoisson convergence in law (binomial approximation)#✓fully proved

The binomial laws Bin(n, λ / (n + λ)) converge weakly to the Poisson law of rate λ.

theorem tendsto_binomialPoissonApprox (lam : ℝ≥0) :
    Tendsto (fun n => binomialPoissonApprox lam n) atTop
      (𝓝 (poissonProbMeasure lam))

Uses 3

Statement usesBinomial approximation to the Poisson law · Poisson law as a probability measure

Proof usesConvergence of characteristic functions to the Poisson law

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.