noncomputable def ProbabilityTheory.binomProbHalf (n k : ℕ) : ℝ

The point mass P(S_n = k) = C(n,k) / 2ⁿ for a Binomial(n, 1/2) random variable S_n.

noncomputable def ProbabilityTheory.gaussianApproxHalf (n k : ℕ) : ℝ

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

noncomputable def ProbabilityTheory.localDMLIndex (x : ℝ) (n : ℕ) : ℕ

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.

theorem ProbabilityTheory.localDMLIndex_tendsto_atTop (x : ℝ) : Filter.Tendsto (localDMLIndex x) Filter.atTop Filter.atTop

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

theorem ProbabilityTheory.n_sub_localDMLIndex_tendsto_atTop (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => n - localDMLIndex x n) Filter.atTop Filter.atTop

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

theorem ProbabilityTheory.localDMLIndex_ratio_half (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => ↑(localDMLIndex x n) / ↑n) Filter.atTop (nhds (1 / 2))

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

theorem ProbabilityTheory.factorial_eq_stirlingSeq_mul (m : ℕ) (hm : 0 < m) : ↑m.factorial = Stirling.stirlingSeq m * √(2 * ↑m) * (↑m / Real.exp 1) ^ m

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

theorem ProbabilityTheory.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.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))

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.

theorem ProbabilityTheory.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

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.

theorem ProbabilityTheory.localDMLIndex_deviation_bound (x : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, |2 * ↑(localDMLIndex x n) - ↑n| ≤ |x| * √↑n + 2

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

theorem ProbabilityTheory.log_power_factor_formula (n k : ℕ) (hk : 0 < k) (hkn : k < n) : have 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)

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.

theorem ProbabilityTheory.dml_power_factor_tendsto_one (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => have k := localDMLIndex x n; ↑n ^ n / (↑k ^ k * ↑(n - k) ^ (n - k) * 2 ^ n) * Real.exp ((↑k - ↑n / 2) ^ 2 / (↑n / 2))) Filter.atTop (nhds 1)

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.

theorem ProbabilityTheory.n_sub_localDMLIndex_ratio_half (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => ↑(n - localDMLIndex x n) / ↑n) Filter.atTop (nhds (1 / 2))

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

theorem ProbabilityTheory.binomProbHalf_isEquivalent_gaussianApproxHalf (x : ℝ) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => binomProbHalf n (localDMLIndex x n)) fun (n : ℕ) => gaussianApproxHalf n (localDMLIndex x n)

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 ProbabilityTheory.local_deMoivreLaplace_half (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => binomProbHalf n (localDMLIndex x n) / gaussianApproxHalf n (localDMLIndex x n)) Filter.atTop (nhds 1)

Local DeMoivre–Laplace limit theorem (p = 1/2 case).

If 2k/√(2n) → x, then P(S_{2n} = 2k) ∼ (π n)^{-1/2} e^{-x²/2} for a fair-coin random walk S_n. Equivalently, for any x ∈ ℝ, the ratio binomProbHalf n (localDMLIndex x n) / gaussianApproxHalf n (localDMLIndex x n) → 1.