Step 0 of the martingale CLT: truncation at level 2 is asymptotically harmless
ProvedMartingale.clt_truncation_matches_of_ltFirst step of the proof of the martingale CLT. Replace the difference array by its truncation
The indicator depends only on for , so it is measurable with respect to the past and is again a martingale difference array — that is exactly why the sum inside the indicator stops before . The claim is that this substitution does not change the limit: the difference of the two row sums tends to in probability.
The reason is that the two row sums coincide on the event that the running sum of squares never exceeds the threshold, and under the limiting-variance hypothesis with that event has probability tending to one. The purpose of the truncation is to make the increments bounded, so that the expansion of the characteristic function in the main argument converges.
The hypothesis is necessary, not cosmetic. If the limiting variance exceeded the truncation level the indicator would switch off with asymptotically positive probability and the two row sums would genuinely differ. The classical presentations take without loss of generality — one may always rescale — and the threshold is then simply a fixed constant comfortably above ; stating the lemma for general requires carrying that inequality explicitly. This supersedes an earlier version of this statement which omitted it and is therefore false for .
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_truncation_matches_of_lt {Ω : Type*} {m0 : MeasurableSpace Ω}
(P : Measure Ω) [IsProbabilityMeasure P] (D : ℕ → ℕ → Ω → ℝ)
(hmeas : ∀ n k, Measurable (D n k))
(σ : ℝ) (hσ2 : σ ^ 2 < 2)
(hvar : TendstoInMeasure P
(fun (n : ℕ) ω => ∑ k ∈ Finset.range n, D n k ω ^ 2) atTop (fun _ => σ ^ 2)) :
TendstoInMeasure P
(fun (n : ℕ) ω => (∑ k ∈ Finset.range n, D n k ω)
- ∑ k ∈ Finset.range n, (Set.indicator
{ω' | ∑ j ∈ Finset.range k, D n j ω' ^ 2 ≤ 2} (D n k) ω))
atTop (fun _ => 0) := by sorry