De Moivre–Laplace theorem

DefinitionStandardized binomial distribution#✓fully proved

For a natural number \(n\) and \(p \in [0, 1]\), the standardized binomial distribution is the measure on \(\mathbb{R}\) given by the law of \((S_n - np)/\sqrt{np(1-p)}\), where \(S_n\) has the binomial distribution with parameters \(n\) and \(p\). When \(np(1-p) = 0\) the division by \(0\) is read as \(0\), so the law is the point mass at \(0\).

This is the standardized sum appearing in the De Moivre–Laplace limit theorem.

noncomputable def standardizedBinomial (n : ℕ) (p : I) : Measure ℝ :=
  Bin(ℝ, n, p).map (fun x : ℝ ↦ (x - ↑n * ↑p) / Real.sqrt (↑n * ↑p * (1 - ↑p)))

Used by 2

Used byCharacteristic function of the standardized binomial · Convergence of characteristic functions in De Moivre–Laplace

TheoremAffine transformation of a characteristic function#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\), let \(a, s, t \in \mathbb{R}\), and let \(\nu\) be the image of \(\mu\) under the map \(x \mapsto (x - a)/s\). Then the characteristic functions satisfy \(\varphi_\nu(t) = \varphi_\mu(t s^{-1}) \, e^{-i a t s^{-1}}\). Here \(s^{-1}\) and division by \(s\) are read as \(0\) when \(s = 0\), so no hypothesis \(s \neq 0\) is needed.

theorem charFun_map_affine (μ : Measure ℝ) (a s t : ℝ) :
    charFun (μ.map (fun x => (x - a) / s)) t =
      charFun μ (t * s⁻¹) * Complex.exp (↑(-(a * (t * s⁻¹))) * Complex.I)

Used by 1

Used byCharacteristic function of the standardized binomial

TheoremCharacteristic function of the real-valued binomial distribution#✓fully proved

For every natural number \(n\), every \(p \in [0, 1]\) and every real \(t\), the characteristic function \(\varphi_{\mathrm{Bin}(n, p)}\) of the binomial distribution \(\mathrm{Bin}(n, p)\), viewed as a measure on \(\mathbb{R}\), satisfies \(\varphi_{\mathrm{Bin}(n, p)}(t) = \left((1 - p) + p e^{it}\right)^n\).

theorem charFun_binomial_real (n : ℕ) (p : I) (t : ℝ) :
    charFun Bin(ℝ, n, p) t =
      ((1 - (p : ℝ)) + (p : ℝ) * Complex.exp (↑t * Complex.I)) ^ n

Used by 2

Used byConvergence of characteristic functions in De Moivre–Laplace · Characteristic function of a binomial law

TheoremSecond-order Taylor remainder bound for the exponential#✓fully proved

For every complex number \(z\) with \(|z| \le 1\), the remainder after the degree-2 Taylor polynomial of the exponential satisfies \(|e^z - 1 - z - z^2/2| \le 2|z|^3\).

theorem exp_taylor2_err (z : ℂ) (hz : ‖z‖ ≤ 1) :
    ‖Complex.exp z - 1 - z - z ^ 2 / 2‖ ≤ 2 * ‖z‖ ^ 3

Used by 1

Used byConvergence of characteristic functions in De Moivre–Laplace

TheoremCharacteristic function of the standardized binomial#✓fully proved

For every natural number \(n\), every \(p \in [0, 1]\) and every real \(t\), put \(s = \sqrt{np(1-p)}\), with \(s^{-1}\) read as \(0\) when \(s = 0\). Let \(\psi\) be the characteristic function of the binomial distribution \(\mathrm{Bin}(n, p)\) viewed as a measure on \(\mathbb{R}\), and \(\varphi\) that of the standardized binomial distribution with parameters \(n\) and \(p\). Then \(\varphi(t) = \psi(t s^{-1}) \, e^{-i n p t s^{-1}}\).

theorem charFun_standardizedBinomial (n : ℕ) (p : I) (t : ℝ) :
    let s := Real.sqrt (↑n * ↑p * (1 - ↑p))
    charFun (standardizedBinomial n p) t =
      charFun Bin(ℝ, n, p) (t * s⁻¹) *
        Complex.exp (↑(-(↑n * (↑p : ℝ) * (t * s⁻¹))) * Complex.I)

Uses 2 · Used by 1

Statement usesStandardized binomial distribution

Proof usesAffine transformation of a characteristic function

Used byConvergence of characteristic functions in De Moivre–Laplace

TheoremConvergence of characteristic functions in De Moivre–Laplace#✓fully proved

Let \(0 < p < 1\) and \(t \in \mathbb{R}\). As \(n \to \infty\), the characteristic function of the standardized binomial distribution with parameters \(n\) and \(p\), evaluated at \(t\), converges to \(e^{-t^2/2}\), the value at \(t\) of the characteristic function of the standard normal distribution.

This is the key analytic step in proving the De Moivre–Laplace theorem via Lévy's continuity theorem.

theorem tendsto_charFun_standardizedBinomial (p : I) (hp₀ : (0 : ℝ) < p) (hp₁ : (p : ℝ) < 1)
    (t : ℝ) :
    Tendsto (fun n ↦ charFun (standardizedBinomial n p) t) atTop
      (𝓝 (Complex.exp (-(t ^ 2 / 2))))

Uses 4

Statement usesStandardized binomial distribution

Proof usesCharacteristic function of the real-valued binomial distribution · Characteristic function of the standardized binomial · Second-order Taylor remainder bound for the exponential

DefinitionStandardized partial sums#✓fully proved

For a sequence \(X_0, X_1, \dots\) of real-valued functions on a set \(\Omega\), a real number \(p\) and \(n \in \mathbb{N}\), the standardized partial sum is the function \(\omega \mapsto (S_n(\omega) - np)/\sqrt{np(1-p)}\) on \(\Omega\), where \(S_n = X_0 + \dots + X_{n-1}\).

The square root of a negative number is taken to be \(0\) and division by \(0\) gives \(0\); in particular the standardized partial sum is \(0\) for \(n = 0\).

noncomputable def deMoivreLaplaceStandardized {Ω : Type*} (X : ℕ → Ω → ℝ)
    (p : ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  ((∑ k ∈ Finset.range n, X k ω) - ↑n * p) / Real.sqrt (↑n * p * (1 - p))

Used by 4

Used byMotif conservation score approximation as a de Moivre–Laplace sum · De Moivre–Laplace for the MCS approximation · De Moivre–Laplace limit theorem, interval form · De Moivre–Laplace limit theorem, convergence in distribution

DefinitionBernoulli standardization map#✓fully proved

For a real number \(p\), the standardization map sends \(x \in \mathbb{R}\) to \((x - p)/\sqrt{p(1-p)}\).

The square root of a negative number is taken to be \(0\) and division by \(0\) gives \(0\), so for \(p \le 0\) or \(p \ge 1\) the map is identically \(0\).

noncomputable def standardizedBernoulli (p : ℝ) (x : ℝ) : ℝ :=
  (x - p) / Real.sqrt (p * (1 - p))

Used by 1

Used byDe Moivre–Laplace limit theorem, convergence in distribution

TheoremAlmost surely \(\{0, 1\}\)-valued random variables are integrable#✓fully proved

Let \(P\) be a probability measure on \(\Omega\) and let \(f : \Omega \to \mathbb{R}\) be almost everywhere measurable with \(f(\omega) \in \{0, 1\}\) for \(P\)-almost every \(\omega\). Then \(f\) is integrable with respect to \(P\).

theorem integrable_of_ae_eq_zero_or_one {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] {f : Ω → ℝ}
    (hf : AEMeasurable f P) (h : ∀ᵐ ω ∂P, f ω = 0 ∨ f ω = 1) :
    Integrable f P

Used by 1

Used byDe Moivre–Laplace limit theorem, convergence in distribution

TheoremSecond moment of a \(\{0, 1\}\)-valued random variable#✓fully proved

Let \(P\) be a probability measure on \(\Omega\) and let \(f : \Omega \to \mathbb{R}\) satisfy \(f(\omega) \in \{0, 1\}\) for \(P\)-almost every \(\omega\). Then \(\int f^2 \, dP = \int f \, dP\).

theorem integral_sq_eq_integral_of_ae_eq_zero_or_one {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] {f : Ω → ℝ}
    (h : ∀ᵐ ω ∂P, f ω = 0 ∨ f ω = 1) :
    ∫ ω, (f ω) ^ 2 ∂P = ∫ ω, f ω ∂P

Used by 1

Used byDe Moivre–Laplace limit theorem, convergence in distribution

TheoremDe Moivre–Laplace limit theorem, convergence in distribution#✓fully proved

Let \(X_0, X_1, \dots\) be independent, identically distributed real random variables on a probability space \((\Omega, P)\), each almost surely equal to \(0\) or \(1\), with mean \(p\) for some \(0 < p < 1\). Write \(S_n = X_0 + \dots + X_{n-1}\). Then the standardized sums \((S_n - np)/\sqrt{np(1-p)}\) converge in distribution to the standard normal distribution \(\mathcal{N}(0, 1)\) as \(n \to \infty\).

theorem deMoivreLaplace_tendstoInDistribution {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] (X : ℕ → Ω → ℝ) {p : ℝ}
    (hp0 : 0 < p) (hp1 : p < 1)
    (h01 : ∀ i, ∀ᵐ ω ∂P, X i ω = 0 ∨ X i ω = 1)
    (hmean : ∀ i, ∫ ω, X i ω ∂P = p)
    (hindep : iIndepFun X P)
    (hident : ∀ i, IdentDistrib (X i) (X 0) P P) :
    TendstoInDistribution
      (fun n ω => deMoivreLaplaceStandardized X p n ω) atTop (id : ℝ → ℝ)
      (fun _ => P) (gaussianReal 0 1)

Uses 4 · Used by 2

Statement usesStandardized partial sums

Proof usesAlmost surely \(\{0, 1\}\)-valued random variables are integrable · Second moment of a \(\{0, 1\}\)-valued random variable · Bernoulli standardization map

Used byDe Moivre–Laplace for the MCS approximation · De Moivre–Laplace limit theorem, interval form

TheoremDe Moivre–Laplace limit theorem, interval form#✓fully proved

Let \(X_0, X_1, \dots\) be independent, identically distributed real random variables on a probability space \((\Omega, P)\), each almost surely equal to \(0\) or \(1\), with mean \(p\) for some \(0 < p < 1\). Write \(S_n = X_0 + \dots + X_{n-1}\). Then for all real numbers \(a \le b\), the probability \(P\left(a \le (S_n - np)/\sqrt{np(1-p)} \le b\right)\) tends, as \(n \to \infty\), to the mass that the standard normal distribution \(\mathcal{N}(0, 1)\) gives to the interval \([a, b]\).

theorem deMoivreLaplace_interval_probability {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] (X : ℕ → Ω → ℝ) {p : ℝ}
    (hp0 : 0 < p) (hp1 : p < 1)
    (h01 : ∀ i, ∀ᵐ ω ∂P, X i ω = 0 ∨ X i ω = 1)
    (hmean : ∀ i, ∫ ω, X i ω ∂P = p)
    (hindep : iIndepFun X P)
    (hident : ∀ i, IdentDistrib (X i) (X 0) P P)
    {a b : ℝ} (hab : a ≤ b) :
    Tendsto (fun n => P.real {ω | a ≤ deMoivreLaplaceStandardized X p n ω
        ∧ deMoivreLaplaceStandardized X p n ω ≤ b}) atTop
      (𝓝 ((gaussianReal 0 1).real (Set.Icc a b)))

Uses 2

Statement usesStandardized partial sums

Proof usesDe Moivre–Laplace limit theorem, convergence in distribution

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.