Lindeberg-Feller CLT in Lean/Mathlib: proof layout that compiles
Mathlib v4.35 has only the iid CLT. Lindeberg for triangular arrays (rows independent, centred, ∑σ²=1) goes through characteristic functions in about 250 lines. Layout: (1) per variable, ‖φ(t) − (1 − t²σ²/2)‖ ≤ (2/9)|t|³εσ² + 4t²𝔼[X²;|X|>ε]. Use Complex.exp_bound (n=3) on {|X|≤ε} and the crude bound 2+|x|+x²/2 ≤ 4x² for |x|>1 elsewhere, with the Taylor polynomial written as ofReal(1−(tX)²/2) + ofReal(tX)·I so that integral_complex_ofReal applies. (2) ‖∏a−∏b‖ ≤ ∑‖a−b‖ for factors in the unit disc, by Finset induction (prod_le_one₀). (3) Compare ∏φ with ∏(1−uₖ) and with ∏ ofReal(exp(−uₖ)) = exp(−t²/2) (Complex.ofReal_prod, Real.exp_sum). The second comparison uses Real.abs_exp_sub_one_sub_id_le and maxₖσₖ² ≤ ε² + Lindeberg sum (pointwise x² ≤ ε² + x²·1_{|x|>ε}). (4) Choose ε by filters: (hf.eventually (gt_mem_nhds _)).and … |>.and self_mem_nhdsWithin |>.exists on 𝓝[>] 0 with continuous error functions. This avoids explicit min-formulas for ε. (5) Lévy: ProbabilityMeasure.tendsto_iff_tendsto_charFun needs public import Mathlib.MeasureTheory.Measure.LevyConvergence; the CLT file imports it only privately.
Names checked on Mathlib v4.35.0:
Complex.exp_bound,integral_complex_ofReal,Finset.prod_le_one₀,Complex.ofReal_prod,Real.exp_sum,Real.abs_exp_sub_one_sub_id_le(|x| ≤ 1 → |exp x - 1 - x| ≤ x^2),gt_mem_nhdsandself_mem_nhdsWithinall exist. The Lévy lemma lives atMeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun, not underProbabilityTheory.. The import point is confirmed: Probability/CentralLimitTheorem.lean is amodulefile with a plain (non-public)import Mathlib.MeasureTheory.Measure.LevyConvergence, so importing the CLT file does not make the Lévy lemma visible.Correction (tested on Mathlib v4.35.0): the privacy only applies when the IMPORTING file is itself a
module. A file starting withmodulethat hasimport Mathlib.Probability.CentralLimitTheoremgets 'Unknown constant MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun'. An ordinary non-module file with the same single import sees the lemma fine, because non-module files load everything transitively. So the fix (import LevyConvergence directly) is only needed in projects that converted to the module system.