Stat.CLT.Martingale­Array

lemma rowSum_aemeasurable (A : MartingaleDifferenceArray Ω μ) (n : ℕ) : AEMeasurable (A.rowSum n) (μ n) := by unfold rowSum apply Finset.aemeasurable_sum intro k hk exact (A.squareIntegrable n k (Finset.mem_range.mp hk)).aemeasurable

theorem norm_expQuadraticRemainder_le_truncated (t x η : ℝ) (hη : 0 < η) (htη : |t| * η ≤ 1) : ‖expQuadraticRemainder (t * x)‖ ≤ |t| ^ 3 * η * x ^ 2 + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * (if η < |x| then x ^ 2 else 0) := by /- Split on `η < |x|`. On the small-increment branch, use `norm_expQuadraticRemainder_le_cube`, `|t*x| ≤ 1`, and `|x|³ ≤ η*x²`. On the large branch, use the global estimate and absorb `2` and `|t*x|` into multiples of `x²` using `0 < η < |x|`. -/ by_cases hx : η < |x| · rw [if_pos hx] have hηsq : 0 < η ^ 2 := sq_pos_of_pos hη have hsq : η ^ 2 ≤ x ^ 2 := by nlinarith [sq_abs x] have htwo : 2 ≤ 2 / η ^ 2 * x ^ 2 := by rw [div_mul_eq_mul_div] exact (le_div_iff₀ hηsq).2 (by nlinarith) have hηabs : η * |x| ≤ x ^ 2 := by have habs : 0 ≤ |x| := abs_nonneg x have hle : η ≤ |x| := hx.le nlinarith [sq_abs x] have hlin : |t * x| ≤ |t| / η * x ^ 2 := by rw [abs_mul, div_mul_eq_mul_div] apply (le_div_iff₀ hη).2 nlinarith [mul_nonneg (abs_nonneg t) (sub_nonneg.mpr hηabs)] have hquad : (t * x) ^ 2 / 2 = (t ^ 2 / 2) * x ^ 2 := by ring have hglobal := norm_expQuadraticRemainder_le_global (t * x) have hcubic : 0 ≤ |t| ^ 3 * η * x ^ 2 := by positivity calc ‖expQuadraticRemainder (t * x)‖ ≤ 2 + |t * x| + (t * x) ^ 2 / 2 := hglobal _ ≤ (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * x ^ 2 := by rw [hquad] nlinarith _ ≤ |t| ^ 3 * η * x ^ 2 + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * x ^ 2 := by linarith · rw [if_neg hx, mul_zero, add_zero] have hxle : |x| ≤ η := le_of_not_gt hx have htx : |t * x| ≤ 1 := by rw [abs_mul] exact (mul_le_mul_of_nonneg_left hxle (abs_nonneg t)).trans htη have hlocal := norm_expQuadraticRemainder_le_cube (t * x) htx have hxcube : |x| ^ 3 ≤ η * x ^ 2 := by calc |x| ^ 3 = |x| * x ^ 2 := by rw [pow_succ, sq_abs] ring _ ≤ η * x ^ 2 := mul_le_mul_of_nonneg_right hxle (sq_nonneg x) calc ‖expQuadraticRemainder (t * x)‖ ≤ |t * x| ^ 3 := hlocal _ = |t| ^ 3 * |x| ^ 3 := by rw [abs_mul, mul_pow] _ ≤ |t| ^ 3 * (η * x ^ 2) := mul_le_mul_of_nonneg_left hxcube (by positivity) _ = |t| ^ 3 * η * x ^ 2 := by ring

theorem norm_integral_compensatedWeight_succ_sub_le [∀ n, IsProbabilityMeasure (μ n)] (A : MartingaleDifferenceArray Ω μ) (n k : ℕ) (hk : k < A.rowLength n) (t K : ℝ) (hK : 0 ≤ K) (hQ : A.partialPredictableQuadraticVariation n (k + 1) ≤ᵐ[μ n] fun _ => K) : ‖(∫ ω, A.compensatedWeight n (k + 1) t ω ∂(μ n)) - ∫ ω, A.compensatedWeight n k t ω ∂(μ n)‖ ≤ exp ((t ^ 2 / 2) * K) * ((∫ ω, ‖expQuadraticRemainder (t * A.increment n k ω)‖ ∂(μ n)) + ((t ^ 2 / 2) ^ 2 / 2) * ∫ ω, (A.conditionalSecondMoment n k ω) ^ 2 ∂(μ n)) := by /- Use `integral_compensatedWeight_succ` and `norm_exp_mul_quadraticFactor_sub_one_le` pointwise. The product of the old correction and `exp(c v_k)` is bounded by `exp(c K)` via `hQ`; control the conditional remainder with `norm_integral_mul_condExp_le_of_ae_bound`. -/ let c : ℝ := t ^ 2 / 2 let v : Ω n → ℝ := A.conditionalSecondMoment n k let rem : Ω n → ℂ := fun ω => expQuadraticRemainder (t * A.increment n k ω) let w : Ω n → ℂ := A.compensatedWeight n k t let g : Ω n → ℂ := fun ω => w ω * ((exp (c * v ω) : ℝ) : ℂ) let euler : Ω n → ℂ := fun ω => w ω * (((exp (c * v ω) : ℝ) : ℂ) * (1 - (((c * v ω : ℝ) : ℂ))) - 1) let B : ℝ := exp (c * K) have hc : 0 ≤ c := by dsimp [c] positivity have hB : 0 ≤ B := by dsimp [B] positivity have hv : StronglyMeasurable[A.filtration n k] v := by exact stronglyMeasurable_condExp have hvNonneg : 0 ≤ᵐ[μ n] v := by dsimp [v, conditionalSecondMoment] exact condExp_nonneg (ae_of_all _ fun ω => sq_nonneg (A.increment n k ω)) have hQkNonneg : 0 ≤ᵐ[μ n] A.partialPredictableQuadraticVariation n k := by have hall : ∀ᵐ ω ∂(μ n), ∀ j, 0 ≤ A.conditionalSecondMoment n j ω := ae_all_iff.mpr fun j => by dsimp [conditionalSecondMoment] exact condExp_nonneg (ae_of_all _ fun ω => sq_nonneg (A.increment n j ω)) filter_upwards [hall] with ω hω unfold partialPredictableQuadraticVariation simp only [Pi.zero_apply, Finset.sum_apply] exact sum_nonneg fun j hj => hω j have hvBound : v ≤ᵐ[μ n] fun _ => K := by filter_upwards [hQ, hQkNonneg] with ω hQω hQkω have hstep := congrFun (A.partialPredictableQuadraticVariation_succ n k hk) ω simp only [Pi.add_apply] at hstep simp only [Pi.zero_apply] at hQkω dsimp [v] linarith have hg : StronglyMeasurable[A.filtration n k] g := by have hS := A.partialRowSum_stronglyMeasurable n k have hQk := A.partialPredictableQuadraticVariation_stronglyMeasurable n k dsimp [g, w, compensatedWeight] fun_prop have hgBound : ∀ᵐ ω ∂(μ n), ‖g ω‖ ≤ B := by filter_upwards [hQ] with ω hQω have hstep := congrFun (A.partialPredictableQuadraticVariation_succ n k hk) ω simp only [Pi.add_apply] at hstep have hexpArg : c * (A.partialPredictableQuadraticVariation n k ω - 1) + c * v ω ≤ c * K := by rw [← mul_add] apply mul_le_mul_of_nonneg_left _ hc dsimp [v] linarith calc ‖g ω‖ = exp (c * (A.partialPredictableQuadraticVariation n k ω - 1) + c * v ω) := by dsimp [g, w, compensatedWeight] rw [norm_mul, norm_mul, Complex.norm_exp, Complex.norm_real, Complex.norm_real] simp [c, v, ← Real.exp_add] _ ≤ B := by dsimp [B] exact Real.exp_le_exp.mpr hexpArg have hw : StronglyMeasurable[A.filtration n k] w := by have hS := A.partialRowSum_stronglyMeasurable n k have hQk := A.partialPredictableQuadraticVariation_stronglyMeasurable n k dsimp only [w] unfold compensatedWeight fun_prop have hwBound : ∀ᵐ ω ∂(μ n), ‖w ω‖ ≤ B := by filter_upwards [hQ, hvNonneg] with ω hQω hvω have hstep := congrFun (A.partialPredictableQuadraticVariation_succ n k hk) ω simp only [Pi.add_apply] at hstep have hQk : A.partialPredictableQuadraticVariation n k ω ≤ K := by dsimp [v] at hvω linarith have hexpArg : c * (A.partialPredictableQuadraticVariation n k ω - 1) ≤ c * K := mul_le_mul_of_nonneg_left (by linarith) hc calc ‖w ω‖ = exp (c * (A.partialPredictableQuadraticVariation n k ω - 1)) := by dsimp [w, compensatedWeight] rw [norm_mul, Complex.norm_exp, Complex.norm_real] simp [c] _ ≤ B := by dsimp [B] exact Real.exp_le_exp.mpr hexpArg have hwInt : Integrable w (μ n) := Integrable.mono' (integrable_const B) (hw.mono ((A.filtration n).le k)).aestronglyMeasurable hwBound have hv2Meas : AEStronglyMeasurable (fun ω => (v ω) ^ 2) (μ n) := by exact (hv.mono ((A.filtration n).le k)).pow 2 |>.aestronglyMeasurable have hv2Int : Integrable (fun ω => (v ω) ^ 2) (μ n) := by refine Integrable.mono' (integrable_const (K ^ 2)) hv2Meas ?_ filter_upwards [hvNonneg, hvBound] with ω hv0 hvK simp only [Pi.zero_apply] at hv0 rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [sq_nonneg (K - v ω)] have hrem : Integrable rem (μ n) := by have hX := (A.squareIntegrable n k hk).integrable (by norm_num) have hX2 := (A.squareIntegrable n k hk).integrable_sq have hexp : Integrable (fun ω => exp (I * ((t * A.increment n k ω : ℝ) : ℂ))) (μ n) := by have hmeas : AEStronglyMeasurable (fun ω => exp (I * ((t * A.increment n k ω : ℝ) : ℂ))) (μ n) := by have := hX.aestronglyMeasurable fun_prop refine Integrable.mono' (integrable_const (1 : ℝ)) hmeas ?_ filter_upwards with ω rw [Complex.norm_exp] simp have hlin : Integrable (fun ω => (I * (t : ℂ)) * (A.increment n k ω : ℂ)) (μ n) := hX.ofReal.const_mul _ have hquad : Integrable (fun ω => ((t ^ 2 / 2 : ℝ) : ℂ) * (((A.increment n k ω) ^ 2 : ℝ) : ℂ)) (μ n) := hX2.ofReal.const_mul _ apply (((hexp.sub (integrable_const (1 : ℂ))).sub hlin).add hquad).congr filter_upwards with ω dsimp [rem] rw [expQuadraticRemainder] push_cast ring have hceInt : Integrable ((μ n)[rem | A.filtration n k]) (μ n) := integrable_condExp have hgAmbient := hg.mono ((A.filtration n).le k) have hgceInt : Integrable (fun ω => g ω * (μ n)[rem | A.filtration n k] ω) (μ n) := hceInt.bdd_mul hgAmbient.aestronglyMeasurable hgBound have heulerMeas : AEStronglyMeasurable euler (μ n) := by have hwAmbient : StronglyMeasurable w := hw.mono ((A.filtration n).le k) have hvAmbient : StronglyMeasurable v := hv.mono ((A.filtration n).le k) dsimp [euler] fun_prop have heulerMajor : ∀ᵐ ω ∂(μ n), ‖euler ω‖ ≤ B * (c ^ 2 / 2 * v ω ^ 2) := by filter_upwards [hvNonneg, hgBound] with ω hvω hgω have hdet := norm_exp_mul_quadraticFactor_sub_one_le c (v ω) 0 hc hvω have hfactor : ‖((exp (c * v ω) : ℝ) : ℂ) * (1 - (((c * v ω : ℝ) : ℂ))) - 1‖ ≤ exp (c * v ω) * ((c * v ω) ^ 2 / 2) := by simpa using hdet calc ‖euler ω‖ = ‖w ω‖ * ‖((exp (c * v ω) : ℝ) : ℂ) * (1 - (((c * v ω : ℝ) : ℂ))) - 1‖ := by dsimp [euler] rw [norm_mul] _ ≤ ‖w ω‖ * (exp (c * v ω) * ((c * v ω) ^ 2 / 2)) := mul_le_mul_of_nonneg_left hfactor (norm_nonneg _) _ = ‖g ω‖ * (c ^ 2 / 2 * v ω ^ 2) := by dsimp [g] rw [norm_mul, Complex.norm_real] simp only [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] ring _ ≤ B * (c ^ 2 / 2 * v ω ^ 2) := by exact mul_le_mul_of_nonneg_right hgω (by positivity) have heulerInt : Integrable euler (μ n) := by apply Integrable.mono' (hv2Int.const_mul (B * (c ^ 2 / 2))) heulerMeas filter_upwards [heulerMajor] with ω hω simpa only [mul_assoc] using hω have heulerNorm : ‖∫ ω, euler ω ∂(μ n)‖ ≤ B * (c ^ 2 / 2) * ∫ ω, v ω ^ 2 ∂(μ n) := by calc ‖∫ ω, euler ω ∂(μ n)‖ ≤ ∫ ω, ‖euler ω‖ ∂(μ n) := norm_integral_le_integral_norm _ _ ≤ ∫ ω, B * (c ^ 2 / 2 * v ω ^ 2) ∂(μ n) := by rw [show (fun ω => B * (c ^ 2 / 2 * v ω ^ 2)) = (fun ω => (B * (c ^ 2 / 2)) * v ω ^ 2) by funext ω ring] apply integral_mono_ae heulerInt.norm (hv2Int.const_mul (B * (c ^ 2 / 2))) filter_upwards [heulerMajor] with ω hω simpa only [mul_assoc] using hω _ = B * (c ^ 2 / 2) * ∫ ω, v ω ^ 2 ∂(μ n) := by rw [show (fun ω => B * (c ^ 2 / 2 * v ω ^ 2)) = (fun ω => (B * (c ^ 2 / 2)) * v ω ^ 2) by funext ω; ring] exact integral_const_mul _ _ have hremNorm : ‖∫ ω, g ω * (μ n)[rem | A.filtration n k] ω ∂(μ n)‖ ≤ B * ∫ ω, ‖rem ω‖ ∂(μ n) := norm_integral_mul_condExp_le_of_ae_bound ((A.filtration n).le k) rem g hrem hg B hB hgBound rw [A.integral_compensatedWeight_succ n k hk t K hQ] change ‖(∫ ω, w ω * (((exp (c * v ω) : ℝ) : ℂ) * (1 - (((c * v ω : ℝ) : ℂ)) + (μ n)[rem | A.filtration n k] ω)) ∂(μ n)) - ∫ ω, w ω ∂(μ n)‖ ≤ B * ((∫ ω, ‖rem ω‖ ∂(μ n)) + (c ^ 2 / 2) * ∫ ω, v ω ^ 2 ∂(μ n)) rw [show (fun ω => w ω * (((exp (c * v ω) : ℝ) : ℂ) * (1 - (((c * v ω : ℝ) : ℂ)) + (μ n)[rem | A.filtration n k] ω))) = (fun ω => w ω + euler ω + g ω * (μ n)[rem | A.filtration n k] ω) by funext ω dsimp [euler, g] ring] change ‖(∫ ω, (w + euler) ω + (fun ω => g ω * (μ n)[rem | A.filtration n k] ω) ω ∂(μ n)) - ∫ ω, w ω ∂(μ n)‖ ≤ B * ((∫ ω, ‖rem ω‖ ∂(μ n)) + (c ^ 2 / 2) * ∫ ω, v ω ^ 2 ∂(μ n)) rw [integral_add (hwInt.add heulerInt) hgceInt] have hwEuler : (∫ ω, (w + euler) ω ∂(μ n)) = (∫ ω, w ω ∂(μ n)) + ∫ ω, euler ω ∂(μ n) := by simpa only [Pi.add_apply] using integral_add hwInt heulerInt rw [hwEuler] have hcancel : ((∫ ω, w ω ∂(μ n)) + (∫ ω, euler ω ∂(μ n)) + ∫ ω, g ω * (μ n)[rem | A.filtration n k] ω ∂(μ n)) - ∫ ω, w ω ∂(μ n) = (∫ ω, euler ω ∂(μ n)) + ∫ ω, g ω * (μ n)[rem | A.filtration n k] ω ∂(μ n) := by ring rw [hcancel] calc ‖(∫ ω, euler ω ∂(μ n)) + ∫ ω, g ω * (μ n)[rem | A.filtration n k] ω ∂(μ n)‖ ≤ ‖∫ ω, euler ω ∂(μ n)‖ + ‖∫ ω, g ω * (μ n)[rem | A.filtration n k] ω ∂(μ n)‖ := norm_add_le _ _ _ ≤ B * (c ^ 2 / 2) * ∫ ω, v ω ^ 2 ∂(μ n) + B * ∫ ω, ‖rem ω‖ ∂(μ n) := add_le_add heulerNorm hremNorm _ = B * ((∫ ω, ‖rem ω‖ ∂(μ n)) + (c ^ 2 / 2) * ∫ ω, v ω ^ 2 ∂(μ n)) := by ring

theorem martingaleArrayCharFun_tendsto [∀ n, IsProbabilityMeasure (μ n)] (A : MartingaleDifferenceArray Ω μ) (hVariance : TendstoInProbability μ A.predictableQuadraticVariation 1) (hLindeberg : ∀ ε : ℝ, 0 < ε → TendstoInProbability μ (A.conditionalLindeberg ε) 0) (t : ℝ) : Tendsto (fun n => charFun ((μ n).map (A.rowSum n)) t) atTop (𝓝 (charFun (gaussianReal 0 1) t)) := by /- Brown--Hall--Heyde characteristic-function argument. 1. For fixed `t` and truncation level `ε`, stop a row when either accumulated predictable variance or accumulated conditional Lindeberg mass leaves a deterministic good set. The two convergence-in-probability hypotheses show that stopping changes the characteristic function by `o(1)`. 2. On the good set, condition successively on `filtration n k`. The linear Taylor term vanishes by `A.condExp_zero`; the quadratic term is the conditional variance, and the Taylor remainder is bounded by the conditional Lindeberg term plus `O(ε)` times predictable variance. 3. Telescope the one-step conditional characteristic functions and compare their product with `exp (-(t^2)/2)`. First let the row index tend to infinity, then let `ε` tend to zero. 4. Rewrite the limit using `charFun_gaussianReal`. The proof uses no independence: every factorization is through conditional expectation at the preceding filtration time. -/ have hPQVMeas (B : MartingaleDifferenceArray Ω μ) (n : ℕ) : AEMeasurable (B.predictableQuadraticVariation n) (μ n) := by unfold MartingaleDifferenceArray.predictableQuadraticVariation apply Finset.aemeasurable_sum intro k _ exact (integrable_condExp : Integrable ((μ n)[fun ω => (B.increment n k ω) ^ 2 | B.filtration n k]) (μ n)).aemeasurable have hPQVNonneg (B : MartingaleDifferenceArray Ω μ) (n : ℕ) : 0 ≤ᵐ[μ n] B.predictableQuadraticVariation n := by have hall : ∀ᵐ ω ∂(μ n), ∀ k, 0 ≤ (μ n)[fun ω => (B.increment n k ω) ^ 2 | B.filtration n k] ω := ae_all_iff.mpr fun k => condExp_nonneg (ae_of_all _ fun ω => sq_nonneg (B.increment n k ω)) filter_upwards [hall] with ω hω unfold MartingaleDifferenceArray.predictableQuadraticVariation simp only [Finset.sum_apply] exact sum_nonneg fun k _ => hω k have hVBad : Tendsto (fun n => (μ n).real {ω | 2 < A.predictableQuadraticVariation n ω}) atTop (𝓝 0) := by apply squeeze_zero (fun _ => measureReal_nonneg) (fun n => ?_) ((ENNReal.tendsto_toReal_zero_iff).2 (hVariance 1 zero_lt_one)) apply measureReal_mono (h₂ := measure_ne_top _ _) intro ω hω change 2 < A.predictableQuadraticVariation n ω at hω change 1 ≤ |A.predictableQuadraticVariation n ω - 1| rw [abs_of_pos (by linarith)] linarith have hLBad (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) : Tendsto (fun n => (μ n).real {ω | δ < A.conditionalLindeberg η n ω}) atTop (𝓝 0) := by apply squeeze_zero (fun _ => measureReal_nonneg) (fun n => ?_) ((ENNReal.tendsto_toReal_zero_iff).2 (hLindeberg η hη δ hδ)) apply measureReal_mono (h₂ := measure_ne_top _ _) intro ω hω change δ ≤ |A.conditionalLindeberg η n ω - 0| rw [sub_zero, abs_of_pos (hδ.trans hω)] exact hω.le have hBad (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) : Tendsto (fun n => (μ n).real ({ω | 2 < A.predictableQuadraticVariation n ω} ∪ {ω | δ < A.conditionalLindeberg η n ω})) atTop (𝓝 0) := by apply squeeze_zero (fun _ => measureReal_nonneg) (fun n => measureReal_union_le _ _) simpa using hVBad.add (hLBad η δ hη hδ) have hStopProb (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) : Tendsto (fun n => (μ n).real {ω | (A.stoppedArray η 2 δ).rowSum n ω ≠ A.rowSum n ω}) atTop (𝓝 0) := by apply squeeze_zero (fun _ => measureReal_nonneg) (fun n => ?_) (hBad η δ hη hδ) rw [measureReal_def, measureReal_def] apply (ENNReal.toReal_le_toReal (measure_ne_top _ _) (measure_ne_top _ _)).2 exact A.measure_stoppedArray_rowSum_ne_le η 2 δ hη n have hStoppedVariance (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) : TendstoInProbability μ (A.stoppedArray η 2 δ).predictableQuadraticVariation 1 := by intro ε hε rw [← ENNReal.tendsto_toReal_zero_iff] apply squeeze_zero (fun _ => measureReal_nonneg) (fun n => ?_) (by have hv := (ENNReal.tendsto_toReal_zero_iff).2 (hVariance ε hε) have hb := hVBad.add (hLBad η δ hη hδ) simpa only [measureReal_def, add_zero] using hv.add hb) let E : Set (Ω n) := {ω | ε ≤ |(A.stoppedArray η 2 δ).predictableQuadraticVariation n ω - 1|} let F : Set (Ω n) := {ω | ε ≤ |A.predictableQuadraticVariation n ω - 1|} let G : Set (Ω n) := {ω | 2 < A.predictableQuadraticVariation n ω} let H : Set (Ω n) := {ω | δ < A.conditionalLindeberg η n ω} have hmono : (μ n).real E ≤ (μ n).real (F ∪ (G ∪ H)) := by rw [measureReal_def, measureReal_def] apply (ENNReal.toReal_le_toReal (measure_ne_top _ _) (measure_ne_top _ _)).2 apply measure_mono_ae filter_upwards [stoppedArray_predictableQuadraticVariation_ae_eq_of_bounds A η 2 δ n] with ω heq intro hω by_cases hF : ω ∈ F · exact Or.inl hF by_cases hG : ω ∈ G · exact inr (Or.inl hG) by_cases hH : ω ∈ H · exact inr (inr hH) exfalso apply hF change ε ≤ |(A.stoppedArray η 2 δ).predictableQuadraticVariation n ω - 1| at hω change ε ≤ |A.predictableQuadraticVariation n ω - 1| change ¬2 < A.predictableQuadraticVariation n ω at hG change ¬δ < A.conditionalLindeberg η n ω at hH rw [heq (le_of_not_gt hG) (le_of_not_gt hH)] at hω exact hω calc (μ n).real {ω | ε ≤ |(A.stoppedArray η 2 δ).predictableQuadraticVariation n ω - 1|} = (μ n).real E := rfl _ ≤ (μ n).real (F ∪ (G ∪ H)) := hmono _ ≤ (μ n).real F + ((μ n).real G + (μ n).real H) := by exact (measureReal_union_le F (G ∪ H)).trans (add_le_add le_rfl (measureReal_union_le G H)) _ = _ := rfl have hStoppedVarianceL1 (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) : Tendsto (fun n => ∫ ω, |(A.stoppedArray η 2 δ).predictableQuadraticVariation n ω - 1| ∂(μ n)) atTop (𝓝 0) := by apply tendsto_integral_abs_sub_of_tendstoInProbability_of_ae_bound (fun n => (A.stoppedArray η 2 δ).predictableQuadraticVariation n) 1 3 (fun n => hPQVMeas (A.stoppedArray η 2 δ) n) (by norm_num) _ (hStoppedVariance η δ hη hδ) intro n filter_upwards [hPQVNonneg (A.stoppedArray η 2 δ) n, A.stoppedArray_predictableQuadraticVariation_le η 2 δ (by norm_num) hδ.le n] with ω h0 h2 simp only [Pi.zero_apply] at h0 rw [abs_le] constructor <;> linarith have hCharIntegral (B : MartingaleDifferenceArray Ω μ) (n : ℕ) : charFun ((μ n).map (B.rowSum n)) t = ∫ ω, exp (I * ((t * B.rowSum n ω : ℝ) : ℂ)) ∂(μ n) := by rw [charFun_apply_real, integral_map (B.rowSum_aemeasurable n) (by fun_prop)] apply integral_congr_ae filter_upwards with ω congr 1 push_cast ring have hStopIntegral (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) : Tendsto (fun n => ‖ (∫ ω, exp (I * ((t * A.rowSum n ω : ℝ) : ℂ)) ∂(μ n)) - ∫ ω, exp (I * ((t * (A.stoppedArray η 2 δ).rowSum n ω : ℝ) : ℂ)) ∂(μ n)‖) atTop (𝓝 0) := by apply squeeze_zero (fun _ => norm_nonneg _) (fun n => ?_) (by have hc : Tendsto (fun _ : ℕ => (2 : ℝ)) atTop (𝓝 2) := tendsto_const_nhds simpa using hc.mul (hStopProb η δ hη hδ)) let g : Ω n → ℂ := fun ω => exp (I * ((t * A.rowSum n ω : ℝ) : ℂ)) let gs : Ω n → ℂ := fun ω => exp (I * ((t * (A.stoppedArray η 2 δ).rowSum n ω : ℝ) : ℂ)) let E : Set (Ω n) := {ω | (A.stoppedArray η 2 δ).rowSum n ω ≠ A.rowSum n ω} have hgMeas : AEStronglyMeasurable g (μ n) := by have hrow := A.rowSum_aemeasurable n dsimp [g] fun_prop have hgsMeas : AEStronglyMeasurable gs (μ n) := by have hrow := (A.stoppedArray η 2 δ).rowSum_aemeasurable n dsimp [gs] fun_prop have hgInt : Integrable g (μ n) := by refine Integrable.mono' (integrable_const (1 : ℝ)) hgMeas ?_ filter_upwards with ω dsimp [g] rw [Complex.norm_exp] simp have hgsInt : Integrable gs (μ n) := by refine Integrable.mono' (integrable_const (1 : ℝ)) hgsMeas ?_ filter_upwards with ω dsimp [gs] rw [Complex.norm_exp] simp have hE : NullMeasurableSet E (μ n) := by have hd := (A.stoppedArray η 2 δ).rowSum_aemeasurable n |>.sub (A.rowSum_aemeasurable n) have hp := hd.nullMeasurableSet_preimage (measurableSet_singleton (0 : ℝ)).compl convert hp using 1 ext ω change ((A.stoppedArray η 2 δ).rowSum n ω ≠ A.rowSum n ω) ↔ (A.stoppedArray η 2 δ).rowSum n ω - A.rowSum n ω ≠ 0 exact (sub_ne_zero : ∀ {a b : ℝ}, a - b ≠ 0 ↔ a ≠ b).symm change ‖(∫ ω, g ω ∂(μ n)) - ∫ ω, gs ω ∂(μ n)‖ ≤ _ rw [← integral_sub hgInt hgsInt] calc ‖∫ ω, g ω - gs ω ∂(μ n)‖ ≤ ∫ ω, ‖g ω - gs ω‖ ∂(μ n) := norm_integral_le_integral_norm _ _ ≤ ∫ ω, E.indicator (fun _ => (2 : ℝ)) ω ∂(μ n) := by apply integral_mono_ae (hgInt.sub hgsInt).norm ((integrable_const (2 : ℝ)).indicator₀ hE) filter_upwards with ω by_cases he : ω ∈ E · rw [Set.indicator_of_mem he] exact (norm_sub_le _ _).trans_eq (by dsimp [g, gs] rw [Complex.norm_exp, Complex.norm_exp] norm_num) · rw [Set.indicator_of_notMem he] have heq : (A.stoppedArray η 2 δ).rowSum n ω = A.rowSum n ω := not_ne_iff.mp he simp [g, gs, heq] _ = 2 * (μ n).real E := by rw [integral_indicator₀ hE, setIntegral_const] simp [mul_comm] _ = 2 * (μ n).real {ω | (A.stoppedArray η 2 δ).rowSum n ω ≠ A.rowSum n ω} := rfl have hGaussian : charFun (gaussianReal 0 1) t = ((exp (-(t ^ 2 / 2)) : ℝ) : ℂ) := by rw [charFun_gaussianReal] rw [show ((1 : NNReal) : ℝ) = 1 by rfl] push_cast congr 1 ring rw [Metric.tendsto_atTop] intro ε hε let R₀ : ℝ → ℝ := fun η => exp ((t ^ 2 / 2) * 2) * (|t| ^ 3 * η * 2 + ((t ^ 2 / 2) ^ 2 / 2) * ((η ^ 2 + 0) * 2)) have hR₀ : Tendsto R₀ (𝓝 0) (𝓝 0) := by have hc : ContinuousAt R₀ 0 := by dsimp [R₀] fun_prop simpa [R₀] using hc.tendsto have hR₀small : ∀ᶠ η in 𝓝 (0 : ℝ), dist (R₀ η) 0 < ε / 4 := Metric.tendsto_nhds.mp hR₀ (ε / 4) (by linarith) rcases Metric.mem_nhds_iff.mp hR₀small with ⟨r, hr, hrsub⟩ let η : ℝ := min (r / 2) (1 / (|t| + 1)) have hη : 0 < η := by dsimp [η] exact lt_min (div_pos hr (by norm_num)) (one_div_pos.mpr (by linarith [abs_nonneg t])) -- … truncated; follow the source link for the rest …

theorem norm_integral_compensatedWeight_rowSum_sub_gaussian_le_of_budgets [∀ n, IsProbabilityMeasure (μ n)] (A : MartingaleDifferenceArray Ω μ) (n : ℕ) (t η K δ : ℝ) (hη : 0 < η) (htη : |t| * η ≤ 1) (hK : 0 ≤ K) (hδ : 0 ≤ δ) (hVariance : A.predictableQuadraticVariation n ≤ᵐ[μ n] fun _ => K) (hLindeberg : A.conditionalLindeberg η n ≤ᵐ[μ n] fun _ => δ) : ‖(∫ ω, A.compensatedWeight n (A.rowLength n) t ω ∂(μ n)) - ((exp (-(t ^ 2 / 2)) : ℝ) : ℂ)‖ ≤ exp ((t ^ 2 / 2) * K) * (|t| ^ 3 * η * K + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * δ + ((t ^ 2 / 2) ^ 2 / 2) * ((η ^ 2 + δ) * K)) := by /- Telescope `norm_integral_compensatedWeight_succ_sub_le`. Nonnegativity of conditional second moments makes every partial predictable variation at most the final one. Sum the one-step bounds, then invoke the closed row remainder and squared-mesh budget lemmas. The time-zero weight integrates to `exp (-(t^2/2))`. -/ let F : ℕ → ℂ := fun r => ∫ ω, A.compensatedWeight n r t ω ∂(μ n) let R : ℕ → ℝ := fun k => ∫ ω, ‖expQuadraticRemainder (t * A.increment n k ω)‖ ∂(μ n) let V₂ : ℕ → ℝ := fun k => ∫ ω, (A.conditionalSecondMoment n k ω) ^ 2 ∂(μ n) let c : ℝ := t ^ 2 / 2 have hvNonneg : ∀ᵐ ω ∂(μ n), ∀ k, 0 ≤ A.conditionalSecondMoment n k ω := ae_all_iff.mpr fun k => by unfold conditionalSecondMoment exact condExp_nonneg (ae_of_all _ fun ω => sq_nonneg (A.increment n k ω)) have hPartial : ∀ k < A.rowLength n, A.partialPredictableQuadraticVariation n (k + 1) ≤ᵐ[μ n] fun _ => K := by intro k hk filter_upwards [hvNonneg, hVariance] with ω hvω hVarianceω apply le_trans _ hVarianceω unfold partialPredictableQuadraticVariation predictableQuadraticVariation rw [Nat.min_eq_left (Nat.succ_le_of_lt hk)] simp only [Finset.sum_apply] change (∑ j ∈ range (k + 1), A.conditionalSecondMoment n j ω) ≤ ∑ j ∈ range (A.rowLength n), A.conditionalSecondMoment n j ω apply Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_mono (Nat.succ_le_of_lt hk)) intro j _ _ exact hvω j have hstep : ∀ k < A.rowLength n, ‖F (k + 1) - F k‖ ≤ exp (c * K) * (R k + (c ^ 2 / 2) * V₂ k) := by intro k hk simpa only [F, R, V₂, c] using A.norm_integral_compensatedWeight_succ_sub_le n k hk t K hK (hPartial k hk) have hF0 : F 0 = ((exp (-c) : ℝ) : ℂ) := by simp [F, compensatedWeight, partialRowSum, partialPredictableQuadraticVariation, c] have hRem := A.sum_integral_norm_expQuadraticRemainder_le_of_budgets n t η K δ hη htη hK hδ hVariance hLindeberg have hV₂ := A.sum_sq_conditionalSecondMoment_le_of_budgets n η K δ hη hK hδ hVariance hLindeberg have hV₂int : (∑ k ∈ range (A.rowLength n), V₂ k) ≤ (η ^ 2 + δ) * K := by have hEach : ∀ k ∈ range (A.rowLength n), Integrable (fun ω => (A.conditionalSecondMoment n k ω) ^ 2) (μ n) := by intro k hk have hce : Integrable (A.conditionalSecondMoment n k) (μ n) := integrable_condExp have hbound : A.conditionalSecondMoment n k ≤ᵐ[μ n] fun _ => K := by filter_upwards [hvNonneg, hPartial k (Finset.mem_range.mp hk)] with ω hvω hpω have hsucc := congrFun (A.partialPredictableQuadraticVariation_succ n k (Finset.mem_range.mp hk)) ω simp only [Pi.add_apply] at hsucc have hpartialNonneg : 0 ≤ A.partialPredictableQuadraticVariation n k ω := by unfold partialPredictableQuadraticVariation simp only [Finset.sum_apply] exact sum_nonneg fun j _ => hvω j linarith refine Integrable.mono' (integrable_const (K ^ 2)) (hce.aestronglyMeasurable.pow 2) ?_ filter_upwards [hvNonneg, hbound] with ω hvω hboundω rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [mul_nonneg (sub_nonneg.mpr hboundω) (add_nonneg hK (hvω k))] calc (∑ k ∈ range (A.rowLength n), V₂ k) = ∫ ω, ∑ k ∈ range (A.rowLength n), (A.conditionalSecondMoment n k ω) ^ 2 ∂(μ n) := by rw [integral_finsetSum _ hEach] _ ≤ ∫ _ω, (η ^ 2 + δ) * K ∂(μ n) := by apply integral_mono_ae · exact integrable_finsetSum _ hEach · exact integrable_const _ · exact hV₂ _ = (η ^ 2 + δ) * K := by simp have htel : F (A.rowLength n) - F 0 = ∑ k ∈ range (A.rowLength n), (F (k + 1) - F k) := by rw [Finset.sum_range_sub] rw [hF0] at htel change ‖F (A.rowLength n) - ((exp (-c) : ℝ) : ℂ)‖ ≤ _ rw [htel] calc ‖∑ k ∈ range (A.rowLength n), (F (k + 1) - F k)‖ ≤ ∑ k ∈ range (A.rowLength n), ‖F (k + 1) - F k‖ := norm_sum_le _ _ _ ≤ ∑ k ∈ range (A.rowLength n), exp (c * K) * (R k + (c ^ 2 / 2) * V₂ k) := by apply Finset.sum_le_sum intro k hk exact hstep k (Finset.mem_range.mp hk) _ = exp (c * K) * ((∑ k ∈ range (A.rowLength n), R k) + (c ^ 2 / 2) * ∑ k ∈ range (A.rowLength n), V₂ k) := by calc (∑ k ∈ range (A.rowLength n), exp (c * K) * (R k + (c ^ 2 / 2) * V₂ k)) = (∑ k ∈ range (A.rowLength n), exp (c * K) * R k) + ∑ k ∈ range (A.rowLength n), exp (c * K) * ((c ^ 2 / 2) * V₂ k) := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro k _ ring _ = exp (c * K) * (∑ k ∈ range (A.rowLength n), R k) + exp (c * K) * (∑ k ∈ range (A.rowLength n), (c ^ 2 / 2) * V₂ k) := by rw [Finset.mul_sum, Finset.mul_sum] _ = _ := by have hscale : (∑ k ∈ range (A.rowLength n), (c ^ 2 / 2) * V₂ k) = (c ^ 2 / 2) * ∑ k ∈ range (A.rowLength n), V₂ k := by rw [Finset.mul_sum] rw [hscale] ring _ ≤ exp (c * K) * ((|t| ^ 3 * η * K + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * δ) + (c ^ 2 / 2) * ((η ^ 2 + δ) * K)) := by gcongr _ = _ := by rfl

theorem integral_norm_expQuadraticRemainder_le (X : Ω → ℝ) (hX : MemLp X 2 μ) (t η : ℝ) (hη : 0 < η) (htη : |t| * η ≤ 1) : (∫ ω, ‖expQuadraticRemainder (t * X ω)‖ ∂μ) ≤ |t| ^ 3 * η * (∫ ω, X ω ^ 2 ∂μ) + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * (∫ ω, if η < |X ω| then X ω ^ 2 else 0 ∂μ) := by /- Integrate `norm_expQuadraticRemainder_le_truncated`. Obtain integrability of `X²`, the truncated square, and the remainder from `hX` and `norm_expQuadraticRemainder_le_global`, then distribute the integral over the two nonnegative constant multiples. -/ have hX2 : Integrable (fun ω => X ω ^ 2) μ := hX.integrable_sq have htrunc : Integrable (fun ω => if η < |X ω| then X ω ^ 2 else 0) μ := by let Y := hX.aestronglyMeasurable.mk X have hXY : X =ᵐ[μ] Y := hX.aestronglyMeasurable.ae_eq_mk have hYmeas : StronglyMeasurable Y := hX.aestronglyMeasurable.stronglyMeasurable_mk have hY2 : Integrable (fun ω => Y ω ^ 2) μ := hX2.congr (hXY.pow_const 2) have hs : MeasurableSet {ω | η < |Y ω|} := measurableSet_lt measurable_const hYmeas.measurable.norm have htruncY : Integrable (fun ω => if η < |Y ω| then Y ω ^ 2 else 0) μ := by apply (hY2.indicator hs).congr filter_upwards with ω rw [indicator] rfl exact htruncY.congr (hXY.mono (fun ω hω => by simp [hω])) let A : ℝ := |t| ^ 3 * η let C : ℝ := 2 / η ^ 2 + |t| / η + t ^ 2 / 2 have hA : Integrable (fun ω => A * X ω ^ 2) μ := hX2.const_mul A have hC : Integrable (fun ω => C * (if η < |X ω| then X ω ^ 2 else 0)) μ := htrunc.const_mul C have hmajor : Integrable (fun ω => A * X ω ^ 2 + C * (if η < |X ω| then X ω ^ 2 else 0)) μ := hA.add hC have hremMeas : AEStronglyMeasurable (fun ω => ‖expQuadraticRemainder (t * X ω)‖) μ := by have hXm := hX.aestronglyMeasurable unfold expQuadraticRemainder fun_prop have hbound : ∀ᵐ ω ∂μ, ‖expQuadraticRemainder (t * X ω)‖ ≤ A * X ω ^ 2 + C * (if η < |X ω| then X ω ^ 2 else 0) := ae_of_all μ fun ω => by simpa only [A, C] using norm_expQuadraticRemainder_le_truncated t (X ω) η hη htη have hrem : Integrable (fun ω => ‖expQuadraticRemainder (t * X ω)‖) μ := by apply hmajor.mono' hremMeas filter_upwards [hbound] with ω hω simpa only [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)] using hω calc (∫ ω, ‖expQuadraticRemainder (t * X ω)‖ ∂μ) ≤ ∫ ω, A * X ω ^ 2 + C * (if η < |X ω| then X ω ^ 2 else 0) ∂μ := integral_mono_ae hrem hmajor hbound _ = A * (∫ ω, X ω ^ 2 ∂μ) + C * (∫ ω, if η < |X ω| then X ω ^ 2 else 0 ∂μ) := by rw [integral_add hA hC, integral_const_mul, integral_const_mul] _ = |t| ^ 3 * η * (∫ ω, X ω ^ 2 ∂μ) + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * (∫ ω, if η < |X ω| then X ω ^ 2 else 0 ∂μ) := by rfl

theorem partialRowSum_stronglyMeasurable (A : MartingaleDifferenceArray Ω μ) (n r : ℕ) : StronglyMeasurable[A.filtration n r] (A.partialRowSum n r) := by unfold partialRowSum apply Finset.stronglyMeasurable_sum intro k hk have hkmin : k < min r (A.rowLength n) := Finset.mem_range.mp hk exact (A.adapted n k (lt_of_lt_of_le hkmin (min_le_right _ _))).mono ((A.filtration n).mono (Nat.succ_le_of_lt (lt_of_lt_of_le hkmin (min_le_left _ _))))

theorem abs_exp_varianceCorrection_sub_one_le (c V K : ℝ) (hc : 0 ≤ c) (hV0 : 0 ≤ V) (hVK : V ≤ K) : |exp (c * (V - 1)) - 1| ≤ exp (c * max K 1) * c * |V - 1| := by have hVabs : |V - 1| ≤ max K 1 := by rw [abs_le] constructor <;> linarith [le_max_left K 1, le_max_right K 1] have harg : |c * (V - 1)| ≤ c * max K 1 := by rw [abs_mul, abs_of_nonneg hc] exact mul_le_mul_of_nonneg_left hVabs hc calc |exp (c * (V - 1)) - 1| ≤ exp |c * (V - 1)| * |c * (V - 1)| := abs_exp_sub_one_le_exp_abs_mul_abs _ _ = exp |c * (V - 1)| * c * |V - 1| := by rw [abs_mul, abs_of_nonneg hc] ring _ ≤ exp (c * max K 1) * c * |V - 1| := by gcongr

theorem conditionalLindeberg_of_fourthMomentSum [∀ n, IsProbabilityMeasure (μ n)] (A : MartingaleDifferenceArray Ω μ) (hFourth : ∀ n k, k < A.rowLength n → MemLp (A.increment n k) 4 (μ n)) (hFourthSum : Tendsto A.fourthMomentSum atTop (𝓝 0)) : ∀ ε : ℝ, 0 < ε → TendstoInProbability μ (A.conditionalLindeberg ε) 0 := by apply conditionalLindeberg_of_conditionalFourthMoment A hFourth exact conditionalFourthMoment_tendstoInProbability_of_fourthMomentSum A hFourth hFourthSum

theorem martingaleArrayCLT [∀ n, IsProbabilityMeasure (μ n)] (A : MartingaleDifferenceArray Ω μ) (hVariance : TendstoInProbability μ A.predictableQuadraticVariation 1) (hLindeberg : ∀ ε : ℝ, 0 < ε → TendstoInProbability μ (A.conditionalLindeberg ε) 0) : TendstoInDistribution μ A.rowSum (gaussianReal 0 1) A.rowSum_aemeasurable := by unfold TendstoInDistribution refine ProbabilityMeasure.tendsto_iff_tendsto_charFun.mpr fun t => ?_ simpa [ProbabilityMeasure.coe_mk] using martingaleArrayCharFun_tendsto A hVariance hLindeberg t

theorem sum_sq_conditionalSecondMoment_le_of_budgets [∀ n, IsProbabilityMeasure (μ n)] (A : MartingaleDifferenceArray Ω μ) (n : ℕ) (η K δ : ℝ) (hη : 0 < η) (hK : 0 ≤ K) (hδ : 0 ≤ δ) (hVariance : A.predictableQuadraticVariation n ≤ᵐ[μ n] fun _ => K) (hLindeberg : A.conditionalLindeberg η n ≤ᵐ[μ n] fun _ => δ) : (fun ω => ∑ k ∈ range (A.rowLength n), ((μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω) ^ 2) ≤ᵐ[μ n] fun _ => (η ^ 2 + δ) * K := by /- On one common full-measure set, every conditional variance and Lindeberg term is nonnegative. The local lemma bounds each variance by `η² + δ`; hence `∑ v_k² ≤ (η²+δ) ∑ v_k ≤ (η²+δ)K`. -/ have hlocal : ∀ᵐ ω ∂(μ n), ∀ k ∈ range (A.rowLength n), (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω ≤ η ^ 2 + A.lindebergTerm η n k ω := (Finset.eventually_all _).mpr fun k hk => A.conditionalSecondMoment_le_sq_add_lindebergTerm n k (Finset.mem_range.mp hk) η hη have hvnonneg : ∀ᵐ ω ∂(μ n), ∀ k ∈ range (A.rowLength n), 0 ≤ (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω := (Finset.eventually_all _).mpr fun k _ => condExp_nonneg (ae_of_all _ fun ω => sq_nonneg (A.increment n k ω)) have hlnonneg : ∀ᵐ ω ∂(μ n), ∀ k ∈ range (A.rowLength n), 0 ≤ A.lindebergTerm η n k ω := (Finset.eventually_all _).mpr fun k _ => by apply condExp_nonneg filter_upwards with ω split_ifs <;> positivity filter_upwards [hlocal, hvnonneg, hlnonneg, hVariance, hLindeberg] with ω hlocalω hvω hlω hVω hLω have hB : 0 ≤ η ^ 2 + δ := add_nonneg (sq_nonneg η) hδ unfold predictableQuadraticVariation at hVω unfold conditionalLindeberg at hLω simp only [Finset.sum_apply] at hVω hLω calc (∑ k ∈ range (A.rowLength n), ((μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω) ^ 2) ≤ ∑ k ∈ range (A.rowLength n), (η ^ 2 + δ) * (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω := by apply Finset.sum_le_sum intro k hk have hlk : A.lindebergTerm η n k ω ≤ δ := (Finset.single_le_sum (fun j hj => hlω j hj) hk).trans hLω rw [pow_two] exact mul_le_mul_of_nonneg_right ((hlocalω k hk).trans (add_le_add_right hlk _)) (hvω k hk) _ = (η ^ 2 + δ) * (∑ k ∈ range (A.rowLength n), (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω) := by rw [Finset.mul_sum] _ ≤ (η ^ 2 + δ) * K := mul_le_mul_of_nonneg_left hVω hB

theorem tendsto_integral_abs_sub_of_tendstoInProbability_of_ae_bound [∀ n, IsProbabilityMeasure (μ n)] (Y : (n : ℕ) → Ω n → ℝ) (c B : ℝ) (hMeas : ∀ n, AEMeasurable (Y n) (μ n)) (hB : 0 ≤ B) (hBound : ∀ n, ∀ᵐ ω ∂(μ n), |Y n ω - c| ≤ B) (hTendsto : TendstoInProbability μ Y c) : Tendsto (fun n => ∫ ω, |Y n ω - c| ∂(μ n)) atTop (𝓝 0) := by /- For a positive tolerance `ε`, split the integral over `{|Y-c| < ε}` and its complement. The first part is at most `ε`; the second is at most `B` times the exceptional probability, which tends to zero by `hTendsto`. `hMeas` and the a.e. bound supply all integrability and measurable set side conditions. Treat `B = 0` directly. -/ let f : (n : ℕ) → Ω n → ℝ := fun n ω => |Y n ω - c| have hfMeas : ∀ n, AEMeasurable (f n) (μ n) := fun n => by simpa only [f, Real.norm_eq_abs] using ((hMeas n).sub_const c).norm have hfInt : ∀ n, Integrable (f n) (μ n) := by intro n apply Integrable.of_bound (hfMeas n).aestronglyMeasurable B filter_upwards [hBound n] with ω hω simpa [f, Real.norm_eq_abs, abs_abs] using hω have hfNonneg : ∀ n, 0 ≤ ∫ ω, f n ω ∂(μ n) := fun n => integral_nonneg_of_ae (Filter.Eventually.of_forall fun ω => abs_nonneg _) rw [Metric.tendsto_atTop] intro ε hε let δ : ℝ := ε / 2 have hδ : 0 < δ := div_pos hε (by norm_num) let s : (n : ℕ) → Set (Ω n) := fun n => {ω | δ ≤ f n ω} have hs : ∀ n, NullMeasurableSet (s n) (μ n) := by intro n exact (hfMeas n).nullMeasurableSet_preimage measurableSet_Ici have hprob : Tendsto (fun n => (μ n (s n)).toReal) atTop (𝓝 0) := by rw [ENNReal.tendsto_toReal_zero_iff] simpa [s, f] using hTendsto δ hδ have hupperTendsto : Tendsto (fun n => δ + B * (μ n (s n)).toReal) atTop (𝓝 δ) := by simpa using tendsto_const_nhds.add (tendsto_const_nhds.mul hprob) have hevUpper : ∀ᶠ n in atTop, δ + B * (μ n (s n)).toReal < ε := by exact (tendsto_order.1 hupperTendsto).2 ε (by dsimp [δ]; linarith) obtain ⟨N, hN⟩ := eventually_atTop.1 hevUpper refine ⟨N, fun n hn => ?_⟩ rw [Real.dist_eq] have hIntUpper : (∫ ω, f n ω ∂(μ n)) ≤ δ + B * (μ n (s n)).toReal := by let g : Ω n → ℝ := fun ω => δ + B * (s n).indicator (fun _ => (1 : ℝ)) ω have hind : Integrable ((s n).indicator (fun _ => (1 : ℝ))) (μ n) := (integrable_const (1 : ℝ)).indicator₀ (hs n) have hg : Integrable g (μ n) := by exact (integrable_const δ).add (hind.const_mul B) calc (∫ ω, f n ω ∂(μ n)) ≤ ∫ ω, g ω ∂(μ n) := by apply integral_mono_ae (hfInt n) hg filter_upwards [hBound n] with ω hω by_cases htail : ω ∈ s n · simp only [g, Set.indicator_of_mem htail] dsimp [δ] linarith [hB] · have hlt : f n ω < δ := lt_of_not_ge htail simp only [g, Set.indicator_of_notMem htail, mul_zero, add_zero] exact hlt.le _ = δ + B * (μ n (s n)).toReal := by rw [integral_add (integrable_const δ) (hind.const_mul B), integral_const_mul] rw [integral_indicator₀ (hs n), setIntegral_one_eq_measureReal] simp [measureReal_def] change |(∫ ω, f n ω ∂(μ n)) - 0| < ε rw [sub_zero, abs_of_nonneg (hfNonneg n)] exact hIntUpper.trans_lt (hN n hn)

theorem sum_integral_norm_expQuadraticRemainder_le_of_budgets [∀ n, IsProbabilityMeasure (μ n)] (A : MartingaleDifferenceArray Ω μ) (n : ℕ) (t η K δ : ℝ) (hη : 0 < η) (htη : |t| * η ≤ 1) (hK : 0 ≤ K) (hδ : 0 ≤ δ) (hVariance : A.predictableQuadraticVariation n ≤ᵐ[μ n] fun _ => K) (hLindeberg : A.conditionalLindeberg η n ≤ᵐ[μ n] fun _ => δ) : (∑ k ∈ range (A.rowLength n), ∫ ω, ‖expQuadraticRemainder (t * A.increment n k ω)‖ ∂(μ n)) ≤ |t| ^ 3 * η * K + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * δ := by /- Sum `integral_norm_expQuadraticRemainder_le` over the active increments. Use `integral_condExp` to identify the two sums of unconditional moments with the integrals of predictable quadratic variation and conditional Lindeberg mass, then integrate the two a.e. budget bounds. -/ have hVint : Integrable (A.predictableQuadraticVariation n) (μ n) := by unfold predictableQuadraticVariation rw [show (∑ k ∈ range (A.rowLength n), (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k]) = (fun ω => ∑ k ∈ range (A.rowLength n), (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω) by funext ω simp only [Finset.sum_apply]] exact integrable_finsetSum (range (A.rowLength n)) (fun k _ => (integrable_condExp : Integrable ((μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k]) (μ n))) have hLint : Integrable (A.conditionalLindeberg η n) (μ n) := by unfold conditionalLindeberg lindebergTerm rw [show (∑ k ∈ range (A.rowLength n), (μ n)[fun ω => if η < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0 | A.filtration n k]) = (fun ω => ∑ k ∈ range (A.rowLength n), (μ n)[fun ω => if η < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0 | A.filtration n k] ω) by funext ω simp only [Finset.sum_apply]] exact integrable_finsetSum (range (A.rowLength n)) (fun k _ => (integrable_condExp : Integrable ((μ n)[fun ω => if η < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0 | A.filtration n k]) (μ n))) have hSecond : (∑ k ∈ range (A.rowLength n), ∫ ω, (A.increment n k ω) ^ 2 ∂(μ n)) = ∫ ω, A.predictableQuadraticVariation n ω ∂(μ n) := by unfold predictableQuadraticVariation simp only [Finset.sum_apply] rw [integral_finsetSum _ (fun k _ => (integrable_condExp : Integrable ((μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k]) (μ n)))] apply Finset.sum_congr rfl intro k _ exact (integral_condExp ((A.filtration n).le k)).symm have hTail : (∑ k ∈ range (A.rowLength n), ∫ ω, (if η < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0) ∂(μ n)) = ∫ ω, A.conditionalLindeberg η n ω ∂(μ n) := by unfold conditionalLindeberg lindebergTerm simp only [Finset.sum_apply] rw [integral_finsetSum _ (fun k _ => (integrable_condExp : Integrable ((μ n)[fun ω => if η < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0 | A.filtration n k]) (μ n)))] apply Finset.sum_congr rfl intro k _ exact (integral_condExp ((A.filtration n).le k)).symm have hVbudget : ∫ ω, A.predictableQuadraticVariation n ω ∂(μ n) ≤ K := by calc (∫ ω, A.predictableQuadraticVariation n ω ∂(μ n)) ≤ ∫ _ω, K ∂(μ n) := integral_mono_ae hVint (integrable_const K) hVariance _ = K := by simp have hLbudget : ∫ ω, A.conditionalLindeberg η n ω ∂(μ n) ≤ δ := by calc (∫ ω, A.conditionalLindeberg η n ω ∂(μ n)) ≤ ∫ _ω, δ ∂(μ n) := integral_mono_ae hLint (integrable_const δ) hLindeberg _ = δ := by simp have hsmall : 0 ≤ |t| ^ 3 * η := mul_nonneg (by positivity) hη.le have hlarge : 0 ≤ 2 / η ^ 2 + |t| / η + t ^ 2 / 2 := by positivity calc (∑ k ∈ range (A.rowLength n), ∫ ω, ‖expQuadraticRemainder (t * A.increment n k ω)‖ ∂(μ n)) ≤ ∑ k ∈ range (A.rowLength n), (|t| ^ 3 * η * (∫ ω, (A.increment n k ω) ^ 2 ∂(μ n)) + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * (∫ ω, if η < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0 ∂(μ n))) := by apply Finset.sum_le_sum intro k hk exact integral_norm_expQuadraticRemainder_le (A.increment n k) (A.squareIntegrable n k (Finset.mem_range.mp hk)) t η hη htη _ = |t| ^ 3 * η * (∑ k ∈ range (A.rowLength n), ∫ ω, (A.increment n k ω) ^ 2 ∂(μ n)) + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * (∑ k ∈ range (A.rowLength n), ∫ ω, if η < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0 ∂(μ n)) := by rw [Finset.sum_add_distrib, Finset.mul_sum, Finset.mul_sum] _ = |t| ^ 3 * η * (∫ ω, A.predictableQuadraticVariation n ω ∂(μ n)) + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * (∫ ω, A.conditionalLindeberg η n ω ∂(μ n)) := by rw [hSecond, hTail] _ ≤ |t| ^ 3 * η * K + (2 / η ^ 2 + |t| / η + t ^ 2 / 2) * δ := add_le_add (mul_le_mul_of_nonneg_left hVbudget hsmall) (mul_le_mul_of_nonneg_left hLbudget hlarge)

theorem measure_stoppedArray_rowSum_ne_le (A : MartingaleDifferenceArray Ω μ) (ε K δ : ℝ) (hε : 0 < ε) (n : ℕ) : (μ n) {ω | (A.stoppedArray ε K δ).rowSum n ω ≠ A.rowSum n ω} ≤ (μ n) {ω | K < A.predictableQuadraticVariation n ω ∨ δ < A.conditionalLindeberg ε n ω} := by /- Convert `stoppedArray_rowSum_ae_eq_of_bounds` to an a.e. inclusion of the disagreement event in the union of the two strict budget violations, then apply `measure_mono_ae`. -/ apply measure_mono_ae filter_upwards [A.stoppedArray_rowSum_ae_eq_of_bounds ε K δ hε n] with ω hω intro hne by_contra hbudgets change ¬(K < A.predictableQuadraticVariation n ω ∨ δ < A.conditionalLindeberg ε n ω) at hbudgets simp only [not_or, not_lt] at hbudgets change (A.stoppedArray ε K δ).rowSum n ω ≠ A.rowSum n ω at hne exact hne (hω hbudgets.1 hbudgets.2)

theorem budgetWeightedSums_le (x y : ℕ → ℝ) (K delta : ℝ) (r : ℕ) (hx : ∀ k < r, 0 ≤ x k) (hy : ∀ k < r, 0 ≤ y k) (hK : 0 ≤ K) (hdelta : 0 ≤ delta) : (∑ k ∈ range r, budgetMultiplier x y K delta k * x k) ≤ K ∧ (∑ k ∈ range r, budgetMultiplier x y K delta k * y k) ≤ delta := by /- Induct on `r`. At the successor step, split on whether the two full prefixes through the new last index satisfy their budgets. If they do, nonnegativity implies every earlier prefix also satisfies its budgets, so all multipliers are one and the selected sums are the full prefix sums. If either full prefix fails, the new multiplier is zero and the induction hypothesis bounds the unchanged selected sums. Useful rewrites are `Finset.sum_range_succ`, `Finset.mem_range`, and `budgetMultiplier`. -/ induction r with | zero => simpa using intro hK hdelta | succ r ih => have hx' : ∀ k < r, 0 ≤ x k := fun k hk => hx k (Nat.lt_succ_of_lt hk) have hy' : ∀ k < r, 0 ≤ y k := fun k hk => hy k (Nat.lt_succ_of_lt hk) have ih_bounds := ih hx' hy' by_cases hfull : (∑ j ∈ range (r + 1), x j) ≤ K ∧ (∑ j ∈ range (r + 1), y j) ≤ delta · have hprefix (k : ℕ) (hk : k < r + 1) : (∑ j ∈ range (k + 1), x j) ≤ K ∧ (∑ j ∈ range (k + 1), y j) ≤ delta := by have hsub : range (k + 1) ⊆ range (r + 1) := Finset.range_mono (Nat.succ_le_succ (Nat.le_of_lt_succ hk)) constructor · exact (Finset.sum_le_sum_of_subset_of_nonneg hsub (fun i hi _ => hx i (Finset.mem_range.mp hi))).trans hfull.1 · exact (Finset.sum_le_sum_of_subset_of_nonneg hsub (fun i hi _ => hy i (Finset.mem_range.mp hi))).trans hfull.2 have hmul (k : ℕ) (hk : k < r + 1) : budgetMultiplier x y K delta k = 1 := by simp [budgetMultiplier, hprefix k hk] constructor · calc (∑ k ∈ range (r + 1), budgetMultiplier x y K delta k * x k) = ∑ k ∈ range (r + 1), x k := by apply Finset.sum_congr rfl intro k hk rw [hmul k (Finset.mem_range.mp hk), one_mul] _ ≤ K := hfull.1 · calc (∑ k ∈ range (r + 1), budgetMultiplier x y K delta k * y k) = ∑ k ∈ range (r + 1), y k := by apply Finset.sum_congr rfl intro k hk rw [hmul k (Finset.mem_range.mp hk), one_mul] _ ≤ delta := hfull.2 · have hlast : budgetMultiplier x y K delta r = 0 := by simp [budgetMultiplier, hfull] simpa [Finset.sum_range_succ, hlast] using ih_bounds