Central limit theorems and Poisson approximation

Convergence in law of normalized sums and their error terms: central limit theorems (Lindeberg–Feller, lacunary and infinite-variance variants), Berry–Esseen bounds and constants, global and local de Moivre–Laplace theorems, Edgeworth expansions, Donsker's invariance principle, and Poisson limit theorems for binomial and urn models.

TheoremConverse of Poisson's theorem for urns#●ready to prove

Let \((\Omega, \mu)\) be a probability space, let \((p_n)_{n \ge 0}\) be real numbers in \([0, 1]\), and let \((X_n)_{n \ge 0}\) be pairwise independent measurable real random variables on \(\Omega\) such that each \(X_n\) almost surely takes only the values \(0\) and \(1\), and \(\mu(X_n = 1) = p_n\). Then for every real number \(L\) and almost every \(\omega \in \Omega\): if \(\frac{1}{n} \sum_{i=0}^{n-1} X_i(\omega) \to L\) as \(n \to \infty\), then \(\frac{1}{n} \sum_{i=0}^{n-1} p_i \to L\) as \(n \to \infty\).

Here \(X_n\) records one draw from the \(n\)-th of a sequence of urns of unknown composition, a white ball as \(1\) and a black ball as \(0\), and \(p_n\) is the probability of drawing a white ball from the \(n\)-th urn. Only pairwise independence is assumed: for uncorrelated variables with uniformly bounded variances the strong law of large numbers still holds.

theorem_wanted urnConversePoisson :
    ∀ (Ω : Type) [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
      [MeasureTheory.IsProbabilityMeasure μ] (prob : ℕ → ℝ) (X : ℕ → Ω → ℝ) (L : ℝ),
      (∀ n, 0 ≤ prob n ∧ prob n ≤ 1) →
      (∀ n, Measurable (X n)) →
      (∀ n, ∀ᵐ ω ∂μ, X n ω = 0 ∨ X n ω = 1) →
      (∀ n, μ {ω | X n ω = 1} = ENNReal.ofReal (prob n)) →
      (∀ i j, i ≠ j → ProbabilityTheory.IndepFun (X i) (X j) μ) →
      ∀ᵐ ω ∂μ, Filter.Tendsto (fun n : ℕ => (∑ i ∈ Finset.range n, X i ω) / (n : ℝ))
          Filter.atTop (nhds L) →
        Filter.Tendsto (fun n : ℕ => (∑ i ∈ Finset.range n, prob i) / (n : ℝ))
          Filter.atTop (nhds L)
Sources
  • S. Ulam, Problem 17 of the Scottish Book. The proof is Kolmogorov's strong law of large numbers for independent bounded variables (1933).

TheoremKac's Scottish Book Problem 126#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be a measurable function that is integrable on \([0, 1]\) and satisfies \(\int_0^1 f(x)\,dx = 0\) and \(\int_0^1 f(x)^2\,dx = \infty\). Then the complex numbers \(\left(\int_0^1 \exp\left(i f(x) / \sqrt{n}\right) dx\right)^n\) tend to \(0\) as \(n \to \infty\) through the natural numbers.

theorem_wanted khintchine_infinite_variance_limit :
    ∀ f : ℝ → ℝ,
      Measurable f →
      MeasureTheory.IntegrableOn f (Set.Icc (0 : ℝ) 1) MeasureTheory.volume →
      (∫ x in Set.Icc (0 : ℝ) 1, f x ∂MeasureTheory.volume) = 0 →
      (∫⁻ x in Set.Icc (0 : ℝ) 1,
        ENNReal.ofReal ((f x) ^ 2) ∂MeasureTheory.volume) = ⊤ →
      Filter.Tendsto
        (fun n : ℕ =>
          (∫ x in Set.Icc (0 : ℝ) 1,
            Complex.exp (Complex.I * (f x : ℂ) / (Real.sqrt (n : ℝ) : ℂ))
              ∂MeasureTheory.volume) ^ n)
        Filter.atTop (nhds (0 : ℂ))
Sources
  • M. Kac, Problem 126 of the Scottish Book; solved affirmatively by A. Khintchine, fourth communique on dependent functions, Studia Mathematicae 6 or 7, as cited in the typescript addendum Ad 126. The typescript parenthetical states the finite-variance case as e ^ (-1 / 2) where e ^ (-A / 2) for A = ∫_0^1 f^2 would be expected; that parenthetical is not used here.

TheoremLocal Edgeworth expansion for the Ewens distribution#●ready to prove

Let \(r \ge 0\) be an integer and let \(L \subseteq (0, \infty)\) be compact. For \(\theta > 0\) and integers \(n \ge 2\) and \(1 \le k \le n\), let \(s(n, k)\) be the unsigned Stirling number of the first kind (the number of permutations of \(n\) elements with exactly \(k\) cycles), let \(p_n(k; \theta) = \theta^k s(n, k) / (\theta (\theta + 1) \cdots (\theta + n - 1))\) be the probability that an Ewens permutation with parameter \(\theta\) has exactly \(k\) cycles, and let \(x_n(k; \theta) = (k - \theta \log n) / \sqrt{\theta \log n}\). Then there are functions \(H_0, H_1, \dots : \mathbb{R} \times \mathbb{R} \to \mathbb{R}\) such that for every \(\varepsilon > 0\) there is an \(N \ge 2\) with the following property: for all \(n \ge N\), all \(\theta \in L\) and all integers \(1 \le k \le n\), writing \(x = x_n(k; \theta)\),

\[(\log n)^{(r+1)/2} \left| p_n(k; \theta) - \frac{e^{-x^2/2}}{\sqrt{2 \pi \theta \log n}} \sum_{j=0}^{r} \frac{H_j(x, \theta)}{(\theta \log n)^{j/2}} \right| < \varepsilon.\]

The functions \(H_j\) are bound existentially and may depend on both \(r\) and \(L\); nothing requires them to be polynomials.

MetaMathlibExt.stirling_edgeworth_expansion · 17 lines 
public theorem_wanted stirling_edgeworth_expansion
    (r : ℕ)
    (L : Set ℝ)
    (hL_compact : IsCompact L)
    (hL_positive : L ⊆ Set.Ioi 0) :
    ∃ H : ℕ → ℝ → ℝ → ℝ, ∀ ε : ℝ, 0 < ε →
      ∀ᶠ n : ℕ in atTop, ∀ θ ∈ L, ∀ k ∈ Finset.Icc 1 n,
        Real.rpow (Real.log n) (((r : ℝ) + 1) / 2) *
            |θ ^ k * (Nat.stirlingFirst n k : ℝ) /
                (∏ i ∈ Finset.range n, (θ + (i : ℝ))) -
              Real.exp (-(((((k : ℝ) - θ * Real.log n) /
                  Real.sqrt (θ * Real.log n)) ^ 2) / 2)) /
                Real.sqrt (2 * Real.pi * θ * Real.log n) *
                ∑ j ∈ Finset.range (r + 1),
                  H j (((k : ℝ) - θ * Real.log n) /
                    Real.sqrt (θ * Real.log n)) θ /
                    Real.rpow (θ * Real.log n) ((j : ℝ) / 2)| < ε
Sources
  • Zakhar Kabluchko, Alexander Marynych, and Henning Sulzbach, "Mode and Edgeworth Expansion for the Ewens Distribution and the Stirling Numbers," Journal of Integer Sequences 19 (2016), Article 16.8.8, Theorem, lines 207–226 (Ewens probability mass function at lines 143–146), https://cs.uwaterloo.ca/journals/JIS/VOL19/Kabluchko/kabl2.tex

TheoremMean absolute sum over the unit cube#●ready to prove

For \(n \in \mathbb{N}\) let

\[ I_n = \int_{[-1/2,\, 1/2]^n} \left| \sum_{i=1}^n x_i \right| dx. \]

Then \(I_n / \sqrt{n} \to 1 / \sqrt{6\pi}\) as \(n \to \infty\).

public theorem_wanted tendsto_integral_abs_sum_cube_div_sqrt
    (I : ℕ → ℝ)
    (hI : ∀ n : ℕ,
      I n = ∫ x in (Set.Icc
          (fun _ : Fin n => (-1 / 2 : ℝ))
          (fun _ : Fin n => (1 / 2 : ℝ))),
        |∑ i : Fin n, x i|) :
    Tendsto (fun n : ℕ => I n / Real.sqrt (n : ℝ)) atTop
      (𝓝 (1 / Real.sqrt (6 * Real.pi)))
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_95.
4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.