Lindeberg–Feller central limit theorem

DefinitionLindeberg condition for a triangular array#✓fully proved

A triangular array of real random variables \(X_{n,k}\) (\(n \in \mathbb{N}\), \(0 \le k < n\)) on a measure space \((\Omega, \mu)\) satisfies the Lindeberg condition if for every \(\varepsilon > 0\) the truncated second moments

\[\sum_{k < n} \int_\Omega X_{n,k}^2 \, \mathbf{1}\{|X_{n,k}| > \varepsilon\} \, d\mu\]

tend to \(0\) as \(n \to \infty\). This is the key hypothesis of the Lindeberg–Feller central limit theorem.

def LindebergConditionTriangular {Ω : Type*} [MeasurableSpace Ω]
    (X : ℕ → ℕ → Ω → ℝ) (μ : Measure Ω) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    Tendsto (fun n => ∑ k ∈ Finset.range n,
      ∫ ω, (X n k ω) ^ 2 * Set.indicator {ω' | ε < |X n k ω'|} 1 ω ∂μ)
    atTop (𝓝 0)

Used by 2

Used byAnalytic core of the Lindeberg–Feller theorem · Lindeberg–Feller central limit theorem

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

For every real \(x\) with \(|x| \le 1\), \(|e^{ix} - 1 - ix| \le x^2\).

theorem norm_exp_ofReal_mul_I_sub_one_sub_le {x : ℝ} (hx : ‖x‖ ≤ 1) :
    ‖Complex.exp (↑x * Complex.I) - 1 - ↑x * Complex.I‖ ≤ x ^ 2

TheoremComparing a finite product with the exponential of a sum#✓fully proved

Let \(s\) be a finite index set and let \(u_i \in \mathbb{C}\) for \(i \in s\). If \(|u_i| \le 1/2\) for every \(i \in s\), then

\[ \Bigl|\prod_{i \in s} (1 + u_i) - \exp\Bigl(\sum_{i \in s} u_i\Bigr)\Bigr| \le \Bigl(\sum_{i \in s} |u_i|^2\Bigr) \exp\Bigl(\sum_{i \in s} |u_i|\Bigr). \]

This is the estimate that turns the second-order expansion of each characteristic function into convergence of the product.

theorem prod_one_add_sub_exp_sum_le {ι : Type*} [DecidableEq ι] (s : Finset ι) (u : ι → ℂ)
    (hu : ∀ i ∈ s, ‖u i‖ ≤ 1 / 2) :
    ‖∏ i ∈ s, (1 + u i) - Complex.exp (∑ i ∈ s, u i)‖ ≤
      (∑ i ∈ s, ‖u i‖ ^ 2) * Real.exp (∑ i ∈ s, ‖u i‖)

Used by 1

Used byAnalytic core of the Lindeberg–Feller theorem

TheoremAnalytic core of the Lindeberg–Feller theorem#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\) and let \(X_{n,k}\) (\(n \in \mathbb{N}\), \(0 \le k < n\)) be real random variables on \(\Omega\) such that each \(X_{n,k}\) has mean \(0\) and each \(X_{n,k}^2\) is integrable (expectations are taken under \(\mu\)). Suppose that for some \(\sigma > 0\) the row variances \(\sum_{k < n} \mathbb{E}[X_{n,k}^2]\) converge to \(\sigma^2\) and that the array satisfies the Lindeberg condition. Then for every real \(t\) the product \(\prod_{k < n} \varphi_{n,k}(t)\) of the characteristic functions \(\varphi_{n,k}\) of the laws of the \(X_{n,k}\) converges to \(e^{-\sigma^2 t^2 / 2}\) as \(n \to \infty\).

theorem lindeberg_charFun_product_tendsto
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : ℕ → ℕ → Ω → ℝ)
    (hmeas : ∀ n, ∀ k ∈ Finset.range n, Measurable (X n k))
    (hmean : ∀ n, ∀ k ∈ Finset.range n, ∫ ω, X n k ω ∂μ = 0)
    (hint2 : ∀ n, ∀ k ∈ Finset.range n, Integrable (fun ω => (X n k ω) ^ 2) μ)
    (σ : ℝ) (hσ : 0 < σ)
    (hvar : Tendsto (fun n => ∑ k ∈ Finset.range n,
              ∫ ω, (X n k ω) ^ 2 ∂μ) atTop (𝓝 (σ ^ 2)))
    (hL : LindebergConditionTriangular X μ)
    (t : ℝ) :
    Tendsto (fun n => ∏ k ∈ Finset.range n, charFun (μ.map (X n k)) t)
      atTop (𝓝 (Complex.exp (-(↑(σ ^ 2) * ↑t ^ 2 / 2))))

Uses 2 · Used by 1

Statement usesLindeberg condition for a triangular array

Proof usesComparing a finite product with the exponential of a sum

Used byLindeberg–Feller central limit theorem

TheoremLindeberg–Feller central limit theorem#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\) and let \(X_{n,k}\) (\(n \in \mathbb{N}\), \(0 \le k < n\)) be a triangular array of real random variables on \(\Omega\) such that for each \(n\) the variables \(X_{n,0}, \dots, X_{n,n-1}\) are independent, each \(X_{n,k}\) has mean \(0\), and each \(X_{n,k}^2\) is integrable (expectations are taken under \(\mu\)). Suppose that for some \(\sigma > 0\) the row variances \(\sum_{k < n} \mathbb{E}[X_{n,k}^2]\) converge to \(\sigma^2\) and that the array satisfies the Lindeberg condition. Then the row sums \(S_n = \sum_{k < n} X_{n,k}\) converge in distribution to the Gaussian law \(N(0, \sigma^2)\): for every bounded continuous \(f : \mathbb{R} \to \mathbb{R}\), \(\mathbb{E}[f(S_n)] \to \int_{\mathbb{R}} f \, dN(0, \sigma^2)\) as \(n \to \infty\).

ProbabilityTheory.lindeberg_feller_clt_triangular · 15 lines

theorem lindeberg_feller_clt_triangular
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : ℕ → ℕ → Ω → ℝ)
    (hind : ∀ n, iIndepFun (m := fun _ => inferInstance)
      ((Finset.range n).restrict (X n)) μ)
    (hmeas : ∀ n, ∀ k ∈ Finset.range n, Measurable (X n k))
    (hmean : ∀ n, ∀ k ∈ Finset.range n, ∫ ω, X n k ω ∂μ = 0)
    (hint2 : ∀ n, ∀ k ∈ Finset.range n, Integrable (fun ω => (X n k ω) ^ 2) μ)
    (σ : ℝ) (hσ : 0 < σ)
    (hvar : Tendsto (fun n => ∑ k ∈ Finset.range n,
              ∫ ω, (X n k ω) ^ 2 ∂μ) atTop (𝓝 (σ ^ 2)))
    (hL : LindebergConditionTriangular X μ) :
    ∀ f : ℝ →ᵇ ℝ,
      Tendsto (fun n => ∫ x, f x ∂(Measure.map (fun ω => ∑ k ∈ Finset.range n, X n k ω) μ))
        atTop (𝓝 (∫ x, f x ∂(gaussianReal 0 ⟨σ ^ 2, sq_nonneg σ⟩)))

Uses 2

Statement usesLindeberg condition for a triangular array

Proof usesAnalytic core of the Lindeberg–Feller theorem

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.