The martingale central limit theorem for uniformly bounded arrays (Brown–McLeish)
ProvedMartingale.clt_of_bounded_mds_arrayLet be a filtration on a probability space and let be a triangular array which, for each fixed , is an adapted, integrable martingale difference sequence: a.s. and . Suppose
- uniform negligibility: everywhere, with ;
- uniformly bounded squared variation: along every path;
- convergence of the squared variation in : .
Then
What this is. This is the martingale central limit theorem in the bounded-array form — the theorem of Brown (1971) and McLeish (1974) that replaces independence by the martingale-difference property. Independence is not assumed anywhere: the summands may depend on the entire past in an essentially arbitrary way, provided each is conditionally centred given what came before. It is the engine behind central limit theorems for Markov chains (through the Poisson-equation/Gordin martingale approximation), for stochastic approximation and MCMC, and for a large part of asymptotic statistics, where score functions and estimating equations are naturally martingales rather than sums of independent terms.
On the hypotheses. The three assumptions are the pathwise-bounded specialisation of McLeish's conditions.
- Condition 1 is the negligibility of individual increments. Without it a single summand could carry a non-vanishing share of the total and the limit would fail to be Gaussian. Here it is imposed in the strong uniform form , which is what truncation arguments deliver in practice.
- Condition 2 replaces McLeish's uniform integrability of . It is what makes the comparison factor uniformly bounded, by .
- Condition 3 is the identification of the limiting variance. It is stated in ; combined with condition 2 this is equivalent to convergence in probability, since the integrands are uniformly bounded by .
No sign condition on is required — only enters, and the degenerate case is allowed, where the conclusion is convergence in probability to .
Proof. By Lévy's continuity theorem it suffices to show for each fixed . McLeish's master inequality, applied with the constant , bounds
valid as soon as , hence for all large . The first term is at most , because , and vanishes by condition 1. The second is at most , because for , and vanishes by condition 3. A squeeze argument on the eventual filter concludes.
import Mathlib.Probability.Martingale.Basic import Mathlib.MeasureTheory.Function.ConvergenceInDistribution import Mathlib.MeasureTheory.Function.ConvergenceInMeasure import Mathlib.Probability.Distributions.Gaussian.Real open MeasureTheory ProbabilityTheory Filter open scoped ENNReal NNReal Topology ProbabilityTheory
theorem Martingale.clt_of_bounded_mds_array {Ω : Type*} {m0 : MeasurableSpace Ω}
(P : Measure Ω) [IsProbabilityMeasure P] (ℱ : Filtration ℕ m0)
(D : ℕ → ℕ → Ω → ℝ)
(hmeas : ∀ n k, Measurable (D n k))
(hadapt : ∀ n k, Measurable[ℱ k] (D n k))
(hint : ∀ n k, Integrable (D n k) P)
(hmds : ∀ n k, P[D n (k + 1) | ℱ k] =ᵐ[P] 0)
(hcent : ∀ n, ∫ ω, D n 0 ω ∂P = 0)
(C : ℕ → ℝ) (hCbdd : ∀ n k ω, |D n k ω| ≤ C n)
(hC0 : Tendsto C atTop (𝓝 0))
(M : ℝ) (hM : ∀ n ω, ∑ k ∈ Finset.range n, D n k ω ^ 2 ≤ M)
(σ : ℝ)
(hvar : Tendsto (fun n : ℕ => ∫ ω, |(∑ k ∈ Finset.range n, D n k ω ^ 2) - σ ^ 2| ∂P)
atTop (𝓝 0)) :
TendstoInDistribution (fun (n : ℕ) ω => ∑ k ∈ Finset.range n, D n k ω)
atTop (id : ℝ → ℝ) (fun _ => P) (gaussianReal 0 (σ ^ 2).toNNReal) := by sorry