Local de Moivre–Laplace theorem

DefinitionBinomial point mass with success probability one half#✓fully proved

The point mass P(B_n = k) = C(n,k) / 2ⁿ for a Binomial(n, 1/2) success count B_n.

def binomProbHalf (n k : ℕ) : ℝ :=
  (Nat.choose n k : ℝ) / (2 : ℝ) ^ n

Used by 5

Used byStirling decomposition of the binomial-to-Gaussian ratio · Binomial point mass is equivalent to a fixed Gaussian value · Binomial point mass is equivalent to its Gaussian approximation · Local De Moivre–Laplace theorem for \(p = 1/2\) · Local limit theorem for the simple random walk

DefinitionGaussian approximation to the symmetric binomial point mass#✓fully proved

The Gaussian (local CLT) approximation to binomProbHalf n k, √(2/(π n)) · exp(-(k - n/2)² / (n/2)).

def gaussianApproxHalf (n : ℕ) (k : ℕ) : ℝ :=
  Real.sqrt (2 / (Real.pi * (n : ℝ))) *
    Real.exp (-(((k : ℝ) - (n : ℝ) / 2) ^ 2 / ((n : ℝ) / 2)))

Used by 4

Used byStirling decomposition of the binomial-to-Gaussian ratio · Binomial point mass is equivalent to a fixed Gaussian value · Binomial point mass is equivalent to its Gaussian approximation · Local De Moivre–Laplace theorem for \(p = 1/2\)

DefinitionLattice index in the local De Moivre–Laplace theorem#✓fully proved

The integer index k = ⌊n/2 + x·√n/2⌋ corresponding to the parameter x in the local DeMoivre–Laplace statement: it picks the lattice point near n/2 + x √n / 2, so that (2k - n)/√n ≈ x.

def localDMLIndex (x : ℝ) (n : ℕ) : ℕ :=
  ⌊(n : ℝ) / 2 + x * Real.sqrt (n : ℝ) / 2⌋₊

Used by 9

Used byBinomial point mass is equivalent to its Gaussian approximation · The corrected binomial power factor tends to one · Local De Moivre–Laplace theorem for \(p = 1/2\) · Deviation bound for the De Moivre–Laplace index · The De Moivre–Laplace index over n tends to one half · Standardized displacement of the rounded index converges · The De Moivre–Laplace index tends to infinity · The complementary index over n tends to one half · The complementary De Moivre–Laplace index tends to infinity

LemmaThe De Moivre–Laplace index tends to infinity#✓fully proved

The index localDMLIndex x n tends to infinity as n → ∞, for any fixed x : ℝ.

lemma localDMLIndex_tendsto_atTop (x : ℝ) :
    Tendsto (localDMLIndex x) atTop atTop

Uses 1 · Used by 1

Statement usesLattice index in the local De Moivre–Laplace theorem

Used byStandardized displacement of the rounded index converges

LemmaThe complementary De Moivre–Laplace index tends to infinity#✓fully proved

The complementary index n - localDMLIndex x n also tends to infinity, so both k and n - k are eventually arbitrarily large.

lemma n_sub_localDMLIndex_tendsto_atTop (x : ℝ) :
    Tendsto (fun n => n - localDMLIndex x n) atTop atTop

Uses 1 · Used by 1

Statement usesLattice index in the local De Moivre–Laplace theorem

Used byThe complementary index over n tends to one half

LemmaThe De Moivre–Laplace index over n tends to one half#✓fully proved

The ratio localDMLIndex x n / n tends to 1/2 as n → ∞, because the correction x √n / 2 is o(n).

lemma localDMLIndex_ratio_half (x : ℝ) :
    Tendsto (fun n => (localDMLIndex x n : ℝ) / (n : ℝ)) atTop (nhds (1/2))

Uses 1 · Used by 1

Statement usesLattice index in the local De Moivre–Laplace theorem

Used byThe complementary index over n tends to one half

LemmaFactorial in terms of the Stirling sequence#✓fully proved

Rewriting of m! in terms of Mathlib's Stirling.stirlingSeq: m! = stirlingSeq(m) · √(2m) · (m/e)^m.

lemma factorial_eq_stirlingSeq_mul (m : ℕ) (hm : 0 < m) :
    (m ! : ℝ) = Stirling.stirlingSeq m * Real.sqrt (2 * (m : ℝ)) *
      ((m : ℝ) / Real.exp 1) ^ m

Used by 1

Used byStirling decomposition of the binomial-to-Gaussian ratio

LemmaStirling decomposition of the binomial-to-Gaussian ratio#✓fully proved

Algebraic rewriting of the ratio binomProbHalf n k / gaussianApproxHalf n k using Stirling's formula, separating it into a Stirling-sequence factor, a square-root factor, a power-of-n factor, and an exponential correction.

lemma binomProb_div_gaussianApprox_eq (n k : ℕ) (hn : 0 < n) (hk : 0 < k) (hkn : k < n) :
    binomProbHalf n k / gaussianApproxHalf n k =
    (Stirling.stirlingSeq n / (Stirling.stirlingSeq k * Stirling.stirlingSeq (n - k))) *
    Real.sqrt (Real.pi * (n : ℝ) ^ 2 / (4 * (k : ℝ) * ((n - k : ℕ) : ℝ))) *
    ((n : ℝ) ^ n / ((k : ℝ) ^ k * ((n - k : ℕ) : ℝ) ^ (n - k) * 2 ^ n)) *
    Real.exp (((k : ℝ) - (n : ℝ) / 2) ^ 2 / ((n : ℝ) / 2))

Uses 3 · Used by 2

Statement usesBinomial point mass with success probability one half · Gaussian approximation to the symmetric binomial point mass

Proof usesFactorial in terms of the Stirling sequence

Used byBinomial point mass is equivalent to a fixed Gaussian value · Binomial point mass is equivalent to its Gaussian approximation

LemmaCubic bound on the symmetric entropy residual#✓fully proved

Third-order Taylor bound for the symmetric entropy expansion: |(1+u) log(1+u) + (1-u) log(1-u) - u²| ≤ 6 |u|³ whenever |u| < 1/2. Used to control the deviation of the binomial coefficient from its Gaussian approximation.

lemma entropy_residual_bound {u : ℝ} (hu : |u| < 1 / 2) :
    |(1 + u) * Real.log (1 + u) + (1 - u) * Real.log (1 - u) - u ^ 2| ≤ 6 * |u| ^ 3

Used by 3

Used byBinomial point mass is equivalent to a fixed Gaussian value · Binomial point mass is equivalent to its Gaussian approximation · The corrected binomial power factor tends to one

LemmaDeviation bound for the De Moivre–Laplace index#✓fully proved

Eventually, the deviation |2k - n| for k = localDMLIndex x n is at most |x| √n + 2, since k = ⌊n/2 + x √n / 2⌋.

lemma localDMLIndex_deviation_bound (x : ℝ) :
    ∀ᶠ n in atTop, |(2 : ℝ) * (localDMLIndex x n : ℝ) - (n : ℝ)| ≤ |x| * Real.sqrt n + 2

Uses 1

Statement usesLattice index in the local De Moivre–Laplace theorem

LemmaLogarithm of the binomial power factor#✓fully proved

Identity rewriting the logarithm of the power factor nⁿ / (kᵏ (n-k)^{n-k} 2ⁿ) plus the Gaussian exponent (k - n/2)² / (n/2) as -(n/2) · ((1+u) log(1+u) + (1-u) log(1-u) - u²), where u = (2k - n)/n. This combines the log-binomial expansion with the Gaussian correction.

lemma log_power_factor_formula (n k : ℕ) (hk : 0 < k) (hkn : k < n) :
    let u := ((2 : ℝ) * k - n) / n
    Real.log ((↑n : ℝ) ^ n / ((↑k : ℝ) ^ k * ((n - k : ℕ) : ℝ) ^ (n - k) * 2 ^ n)) +
      ((↑k : ℝ) - (↑n : ℝ) / 2) ^ 2 / ((↑n : ℝ) / 2) =
    -((↑n : ℝ) / 2) * ((1 + u) * Real.log (1 + u) + (1 - u) * Real.log (1 - u) - u ^ 2)

Used by 3

Used byBinomial point mass is equivalent to a fixed Gaussian value · Binomial point mass is equivalent to its Gaussian approximation · The corrected binomial power factor tends to one

TheoremBinomial point mass is equivalent to a fixed Gaussian value#✓fully proved

For any binomial success-index sequence whose standardized displacement converges to x, the point mass is equivalent to the Gaussian expression evaluated at the fixed limit x. The number of trials may follow any natural-valued sequence tending to infinity.

theorem binomProbHalf_isEquivalent_fixedGaussian {m j : ℕ → ℕ} {x : ℝ}
    (hm : Tendsto m atTop atTop)
    (hz : Tendsto (fun n => (2 * (j n : ℝ) - (m n : ℝ)) / Real.sqrt (m n : ℝ))
      atTop (𝓝 x)) :
    (fun n => binomProbHalf (m n) (j n)) ~[atTop]
      (fun n => Real.sqrt (2 / (Real.pi * (m n : ℝ))) * Real.exp (-(x ^ 2 / 2)))

Uses 5 · Used by 1

Statement usesBinomial point mass with success probability one half

Proof usesStirling decomposition of the binomial-to-Gaussian ratio · Cubic bound on the symmetric entropy residual · Gaussian approximation to the symmetric binomial point mass · Logarithm of the binomial power factor

Used byLocal limit theorem for the simple random walk

TheoremLocal limit theorem for the simple random walk#✓fully proved

The source's random-walk local limit theorem: every integer displacement sequence with 2 kₙ / √(2n) → x has point mass equivalent to (√(π n))⁻¹ exp(-x²/2). The scaling hypothesis itself implies that n + kₙ is a valid success index eventually.

theorem local_deMoivreLaplace_half_of_tendsto {k : ℕ → ℤ} {x : ℝ}
    (hk : Tendsto (fun n => 2 * (k n : ℝ) / Real.sqrt (2 * (n : ℝ))) atTop (𝓝 x)) :
    (fun n => binomProbHalf (2 * n) (((n : ℤ) + k n).toNat)) ~[atTop]
      (fun n => (Real.sqrt (Real.pi * (n : ℝ)))⁻¹ * Real.exp (-(x ^ 2 / 2)))

Uses 2

Statement usesBinomial point mass with success probability one half

Proof usesBinomial point mass is equivalent to a fixed Gaussian value

LemmaStandardized displacement of the rounded index converges#✓fully proved

The rounded success index has standardized displacement converging to x.

lemma localDMLIndex_standardized_tendsto (x : ℝ) :
    Tendsto (fun n => (2 * (localDMLIndex x n : ℝ) - (n : ℝ)) / Real.sqrt (n : ℝ))
      atTop (𝓝 x)

Uses 2 · Used by 2

Statement usesLattice index in the local De Moivre–Laplace theorem

Proof usesThe De Moivre–Laplace index tends to infinity

Used byBinomial point mass is equivalent to its Gaussian approximation · The corrected binomial power factor tends to one

LemmaThe corrected binomial power factor tends to one#✓fully proved

The product of the power factor nⁿ / (kᵏ (n-k)^{n-k} 2ⁿ) with the Gaussian correction exp((k - n/2)² / (n/2)), evaluated at k = localDMLIndex x n, tends to 1 as n → ∞. This is the key analytic estimate behind the local DeMoivre–Laplace limit theorem.

lemma dml_power_factor_tendsto_one (x : ℝ) :
    Tendsto (fun n =>
      let k := localDMLIndex x n
      ((n : ℝ) ^ n / ((k : ℝ) ^ k * ((n - k : ℕ) : ℝ) ^ (n - k) * 2 ^ n)) *
      Real.exp (((k : ℝ) - (n : ℝ) / 2) ^ 2 / ((n : ℝ) / 2)))
    atTop (nhds 1)

Uses 4

Statement usesLattice index in the local De Moivre–Laplace theorem

Proof usesCubic bound on the symmetric entropy residual · Standardized displacement of the rounded index converges · Logarithm of the binomial power factor

LemmaThe complementary index over n tends to one half#✓fully proved

Companion to localDMLIndex_ratio_half: the ratio (n - k) / n for k = localDMLIndex x n also tends to 1/2.

lemma n_sub_localDMLIndex_ratio_half (x : ℝ) :
    Tendsto (fun n => ((n - localDMLIndex x n : ℕ) : ℝ) / (n : ℝ)) atTop (nhds (1/2))

Uses 3

Statement usesLattice index in the local De Moivre–Laplace theorem

Proof usesThe De Moivre–Laplace index over n tends to one half · The complementary De Moivre–Laplace index tends to infinity

TheoremBinomial point mass is equivalent to its Gaussian approximation#✓fully proved

The binomial point mass and its Gaussian approximation are asymptotically equivalent along the sequence k = localDMLIndex x n: binomProbHalf n k ~ gaussianApproxHalf n k as n → ∞. Combines Stirling's formula with the power-factor and entropy estimates.

theorem binomProbHalf_isEquivalent_gaussianApproxHalf (x : ℝ) :
    (fun n => binomProbHalf n (localDMLIndex x n)) ~[atTop]
    (fun n => gaussianApproxHalf n (localDMLIndex x n))

Uses 7 · Used by 1

Statement usesBinomial point mass with success probability one half · Gaussian approximation to the symmetric binomial point mass · Lattice index in the local De Moivre–Laplace theorem

Proof usesStirling decomposition of the binomial-to-Gaussian ratio · Cubic bound on the symmetric entropy residual · Standardized displacement of the rounded index converges · Logarithm of the binomial power factor

Used byLocal De Moivre–Laplace theorem for \(p = 1/2\)

TheoremLocal De Moivre–Laplace theorem for \(p = 1/2\)#✓fully proved

Canonical rounded-sequence corollary of the local De Moivre–Laplace theorem: for any x ∈ ℝ, the binomial point mass divided by its moving Gaussian approximation along localDMLIndex x tends to 1. The arbitrary integer-displacement statement with the fixed Gaussian value at x is local_deMoivreLaplace_half_of_tendsto.

theorem local_deMoivreLaplace_half (x : ℝ) :
    Tendsto (fun n => binomProbHalf n (localDMLIndex x n) /
      gaussianApproxHalf n (localDMLIndex x n))
    atTop (nhds 1)

Uses 4

Statement usesBinomial point mass with success probability one half · Gaussian approximation to the symmetric binomial point mass · Lattice index in the local De Moivre–Laplace theorem

Proof usesBinomial point mass is equivalent to its Gaussian approximation

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.