def ProbabilityTheory.LindebergConditionTriangular {Ω : Type u_1} [MeasurableSpace Ω] (X : ℕ → ℕ → Ω → ℝ) (μ : MeasureTheory.Measure Ω) : Prop

The Lindeberg condition for a triangular array X n k of random variables on (Ω, μ): for every ε > 0, the truncated second moment ∑ₖ ∫ (X n k)² · 𝟙{|X n k| > ε} dμ tends to 0 as n → ∞. This is the key hypothesis of the Lindeberg–Feller central limit theorem.

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

Helper bound: for any real x, ‖e^{ix} - 1 - ix‖ ≤ x². This is the standard second-order Taylor estimate for the complex exponential along the imaginary axis.

theorem ProbabilityTheory.norm_charFun_sub_one_le_sq_mul_variance {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → ℝ) (hmeas : Measurable X) (hmean : ∫ (ω : Ω), X ω ∂μ = 0) (hint2 : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) (t : ℝ) : ‖MeasureTheory.charFun (MeasureTheory.Measure.map X μ) t - 1‖ ≤ t ^ 2 * ∫ (ω : Ω), X ω ^ 2 ∂μ

For a mean-zero random variable X with finite second moment, the deviation of its characteristic function from 1 is controlled by the variance: ‖φ_X(t) - 1‖ ≤ t² · 𝔼[X²].

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

Under the Lindeberg hypothesis, the product of characteristic functions of the rows of a mean-zero triangular array converges to the characteristic function of a N(0, σ²) Gaussian, exp(-σ² t²/2). This is the analytic core of the Lindeberg–Feller theorem.

theorem ProbabilityTheory.lindeberg_feller_clt_triangular {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → ℕ → Ω → ℝ) (hind : ∀ (n : ℕ), iIndepFun (X n) μ) (hmeas : ∀ (n k : ℕ), Measurable (X n k)) (hmean : ∀ (n k : ℕ), ∫ (ω : Ω), X n k ω ∂μ = 0) (σ : ℝ) (hσ : 0 < σ) (hvar : Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, ∫ (ω : Ω), X n k ω ^ 2 ∂μ) Filter.atTop (nhds (σ ^ 2))) (hL : LindebergConditionTriangular X μ) (f : BoundedContinuousFunction ℝ ℝ) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), f x ∂MeasureTheory.Measure.map (fun (ω : Ω) => ∑ k ∈ Finset.range n, X n k ω) μ) Filter.atTop (nhds (∫ (x : ℝ), f x ∂gaussianReal 0 ⟨σ ^ 2, ⋯⟩))

Lindeberg–Feller central limit theorem (triangular array form).

Suppose X n k, for 1 ≤ k ≤ n, is a triangular array of independent, mean-zero random variables on (Ω, μ). If

• the row variances ∑ₖ 𝔼[X n k²] converge to σ² > 0, and
• the Lindeberg condition LindebergConditionTriangular X μ holds,

then the row sums Sₙ = ∑ₖ X n k converge in distribution to N(0, σ²): for every bounded continuous f : ℝ →ᵇ ℝ, 𝔼[f(Sₙ)] → 𝔼[f(σ · χ)] where χ is a standard normal.