Stat.CLT.Finite­Iid­Triangular

theorem expect_coordinate (n : ℕ) (i : Fin (M.N n)) (g : Y → ℝ) : M.expect n (fun ys => g (ys i)) = ∑ y, M.w n y * g y := by classical let q : Fin (M.N n) → Y → ℝ := fun k y => M.w n y * (if k = i then g y else 1) have hfactor (ys : Fin (M.N n) → Y) : (∏ k, q k (ys k)) = M.mass n ys * g (ys i) := by change (∏ k, M.w n (ys k) * (if k = i then g (ys k) else 1)) = _ rw [Finset.prod_mul_distrib, Fintype.prod_ite_eq'] rfl have hsum (k : Fin (M.N n)) : (∑ y, q k y) = if k = i then ∑ y, M.w n y * g y else 1 := by by_cases hk : k = i <;> simp [q, hk, M.mass_one] calc M.expect n (fun ys => g (ys i)) = ∑ ys : Fin (M.N n) → Y, ∏ k, q k (ys k) := by unfold expect apply Finset.sum_congr rfl intro ys _ exact (hfactor ys).symm _ = ∏ k, ∑ y, q k y := (Fintype.prod_sum q).symm _ = ∑ y, M.w n y * g y := by simp_rw [hsum] simp

theorem expect_coordinate_mul (n : ℕ) (i j : Fin (M.N n)) (hij : i ≠ j) (g h : Y → ℝ) : M.expect n (fun ys => g (ys i) * h (ys j)) = (∑ y, M.w n y * g y) * (∑ y, M.w n y * h y) := by classical let q : Fin (M.N n) → Y → ℝ := fun k y => M.w n y * (if k = i then g y else 1) * (if k = j then h y else 1) have hfactor (ys : Fin (M.N n) → Y) : (∏ k, q k (ys k)) = M.mass n ys * (g (ys i) * h (ys j)) := by change (∏ k, (M.w n (ys k) * (if k = i then g (ys k) else 1)) * (if k = j then h (ys k) else 1)) = _ rw [Finset.prod_mul_distrib, Finset.prod_mul_distrib] rw [Fintype.prod_ite_eq', Fintype.prod_ite_eq'] simp only [mass] ring have hsum (k : Fin (M.N n)) : (∑ y, q k y) = (if k = i then ∑ y, M.w n y * g y else 1) * (if k = j then ∑ y, M.w n y * h y else 1) := by by_cases hik : k = i · by_cases hjk : k = j · exact (hij (hik.symm.trans hjk)).elim · have : i ≠ j := hij subst k simp [q, this] · by_cases hjk : k = j · have : j ≠ i := Ne.symm hij subst k simp [q, this] · simp [q, hik, hjk, M.mass_one] calc M.expect n (fun ys => g (ys i) * h (ys j)) = ∑ ys : Fin (M.N n) → Y, ∏ k, q k (ys k) := by unfold expect apply Finset.sum_congr rfl intro ys _ exact (hfactor ys).symm _ = ∏ k, ∑ y, q k y := (Fintype.prod_sum q).symm _ = (∑ y, M.w n y * g y) * (∑ y, M.w n y * h y) := by simp_rw [hsum] rw [Finset.prod_mul_distrib] simp

theorem expect_prod_coordinate (n : ℕ) (g : Fin (M.N n) → Y → ℝ) : M.expect n (fun ys => ∏ i, g i (ys i)) = ∏ i, ∑ y, M.w n y * g i y := by simpa only [← M.productDesign_expect n, productDesign, coordinateDesign, FiniteDesign.E] using (FiniteDesign.E_prod_prod (fun _ : Fin (M.N n) => M.coordinateDesign n) g)

theorem rowMeasure_independent (n : ℕ) : iIndepFun (fun (i : Fin (M.N n)) (ys : Fin (M.N n) → Y) => ys i) (M.rowMeasure n) := by exact iIndepFun_prodDesign_eval (fun _ : Fin (M.N n) => M.coordinateDesign n)

theorem expect_empiricalSecond (n : ℕ) (hn : 0 < M.N n) : M.expect n (M.empiricalSecond n) = M.oneSecond n := by classical have hN : (M.N n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) calc M.expect n (M.empiricalSecond n) = (M.N n : ℝ)⁻¹ * ∑ i : Fin (M.N n), M.expect n (fun ys => (M.f n (ys i)) ^ 2) := by simp only [expect, empiricalSecond, Finset.mul_sum] rw [Finset.sum_comm] congr 1 ext i congr 1 ext ys ring _ = (M.N n : ℝ)⁻¹ * ∑ _i : Fin (M.N n), M.oneSecond n := by congr 1 apply Finset.sum_congr rfl intro i _ exact M.expect_coordinate n i (fun y => (M.f n y) ^ 2) _ = M.oneSecond n := by simp [hN]

theorem empiricalSecond_mse_le (n : ℕ) (hn : 0 < M.N n) : M.expect n (fun ys => (M.empiricalSecond n ys - M.oneSecond n) ^ 2) ≤ M.B ^ 4 / (M.N n : ℝ) := by classical let μ := M.oneSecond n let z (i : Fin (M.N n)) (ys : Fin (M.N n) → Y) := (M.f n (ys i)) ^ 2 - μ have hN : (M.N n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) have hsum (g : Fin (M.N n) → (Fin (M.N n) → Y) → ℝ) : M.expect n (fun ys => ∑ i, g i ys) = ∑ i, M.expect n (g i) := by simp only [expect, Finset.mul_sum] rw [Finset.sum_comm] have hscale (c : ℝ) (g : (Fin (M.N n) → Y) → ℝ) : M.expect n (fun ys => c * g ys) = c * M.expect n g := by simp only [expect] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro ys _ ring have hpair (i j : Fin (M.N n)) (hij : i ≠ j) : M.expect n (fun ys => z i ys * z j ys) = 0 := by rw [M.expect_coordinate_mul n i j hij (fun y => (M.f n y) ^ 2 - μ) (fun y => (M.f n y) ^ 2 - μ)] simp [μ, oneSecond, mul_sub, Finset.sum_sub_distrib, ← Finset.sum_mul, M.mass_one] have hdiag (i : Fin (M.N n)) : M.expect n (fun ys => (z i ys) ^ 2) ≤ M.B ^ 4 := by have hc := M.expect_coordinate n i (fun y => ((M.f n y) ^ 2 - μ) ^ 2) change M.expect n (fun ys => (z i ys) ^ 2) = _ at hc rw [hc] have hμsq : 0 ≤ μ ^ 2 := sq_nonneg μ have hfourth : (∑ y, M.w n y * (M.f n y) ^ 4) ≤ M.B ^ 4 := by calc _ ≤ ∑ y, M.w n y * M.B ^ 4 := by apply Finset.sum_le_sum intro y _ apply mul_le_mul_of_nonneg_left _ (M.mass_nonneg n y) have hb := M.bound n y have hb4 : (M.f n y) ^ 4 = |M.f n y| ^ 4 := by rw [← abs_pow] exact (abs_of_nonneg (by positivity)).symm rw [hb4] exact pow_le_pow_left₀ (abs_nonneg _) hb _ _ = M.B ^ 4 := by simp [← Finset.sum_mul, M.mass_one] have hv : (∑ y, M.w n y * ((M.f n y) ^ 2 - μ) ^ 2) = (∑ y, M.w n y * (M.f n y) ^ 4) - μ ^ 2 := by calc _ = (∑ y, M.w n y * (M.f n y) ^ 4) - 2 * μ * (∑ y, M.w n y * (M.f n y) ^ 2) + μ ^ 2 * (∑ y, M.w n y) := by simp only [Finset.mul_sum] rw [← Finset.sum_sub_distrib, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro y _ ring _ = _ := by rw [M.mass_one]; dsimp [μ, oneSecond]; ring rw [hv] linarith have hcenter (ys : Fin (M.N n) → Y) : M.empiricalSecond n ys - μ = (M.N n : ℝ)⁻¹ * ∑ i, z i ys := by simp only [empiricalSecond, z, Finset.sum_sub_distrib] simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul] field_simp have hvar : M.expect n (fun ys => (∑ i, z i ys) ^ 2) = ∑ i : Fin (M.N n), M.expect n (fun ys => (z i ys) ^ 2) := by calc _ = ∑ i : Fin (M.N n), ∑ j : Fin (M.N n), M.expect n (fun ys => z i ys * z j ys) := by calc _ = M.expect n (fun ys => ∑ i : Fin (M.N n), ∑ j : Fin (M.N n), z i ys * z j ys) := by congr 1 funext ys rw [← Finset.sum_mul_sum] ring _ = _ := by rw [hsum] apply Finset.sum_congr rfl intro i _ rw [hsum] _ = ∑ i : Fin (M.N n), M.expect n (fun ys => (z i ys) ^ 2) := by apply Finset.sum_congr rfl intro i _ rw [Finset.sum_eq_single i] · simp only [pow_two] · intro j _ hji exact hpair i j (Ne.symm hji) · intro hi exact (hi (Finset.mem_univ i)).elim calc M.expect n (fun ys => (M.empiricalSecond n ys - M.oneSecond n) ^ 2) = ((M.N n : ℝ)⁻¹) ^ 2 * ∑ i : Fin (M.N n), M.expect n (fun ys => (z i ys) ^ 2) := by simp_rw [show M.oneSecond n = μ from rfl, hcenter] rw [← hvar, ← hscale] congr 1 funext ys ring _ ≤ ((M.N n : ℝ)⁻¹) ^ 2 * ((M.N n : ℝ) * M.B ^ 4) := by apply mul_le_mul_of_nonneg_left _ (sq_nonneg _) simpa only [Finset.sum_const_zero, Finset.sum_const, Finset.card_fin, nsmul_eq_mul] using Finset.sum_le_sum (s := univ) (fun i _ => hdiag i) _ = M.B ^ 4 / (M.N n : ℝ) := by field_simp

theorem empiricalMean_mse_le (n : ℕ) (hn : 0 < M.N n) : M.expect n (fun ys => (M.empiricalMean n ys) ^ 2) ≤ M.B ^ 2 / (M.N n : ℝ) := by classical let z (i : Fin (M.N n)) (ys : Fin (M.N n) → Y) := M.f n (ys i) have hN : (M.N n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) have hsum (g : Fin (M.N n) → (Fin (M.N n) → Y) → ℝ) : M.expect n (fun ys => ∑ i, g i ys) = ∑ i, M.expect n (g i) := by simp only [expect, Finset.mul_sum] rw [Finset.sum_comm] have hscale (c : ℝ) (g : (Fin (M.N n) → Y) → ℝ) : M.expect n (fun ys => c * g ys) = c * M.expect n g := by simp only [expect] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro ys _ ring have hpair (i j : Fin (M.N n)) (hij : i ≠ j) : M.expect n (fun ys => z i ys * z j ys) = 0 := by rw [M.expect_coordinate_mul n i j hij (M.f n) (M.f n)] simp [M.centered n] have hdiag (i : Fin (M.N n)) : M.expect n (fun ys => (z i ys) ^ 2) ≤ M.B ^ 2 := by rw [M.expect_coordinate n i (fun y => (M.f n y) ^ 2)] calc (∑ y, M.w n y * (M.f n y) ^ 2) ≤ ∑ y, M.w n y * M.B ^ 2 := by apply Finset.sum_le_sum intro y _ apply mul_le_mul_of_nonneg_left _ (M.mass_nonneg n y) have hb := M.bound n y have hb2 : (M.f n y) ^ 2 = |M.f n y| ^ 2 := by rw [← abs_pow] exact (abs_of_nonneg (by positivity)).symm rw [hb2] exact pow_le_pow_left₀ (abs_nonneg _) hb _ _ = M.B ^ 2 := by simp [← Finset.sum_mul, M.mass_one] have hvar : M.expect n (fun ys => (∑ i, z i ys) ^ 2) = ∑ i : Fin (M.N n), M.expect n (fun ys => (z i ys) ^ 2) := by calc _ = ∑ i : Fin (M.N n), ∑ j : Fin (M.N n), M.expect n (fun ys => z i ys * z j ys) := by calc _ = M.expect n (fun ys => ∑ i : Fin (M.N n), ∑ j : Fin (M.N n), z i ys * z j ys) := by congr 1 funext ys rw [← Finset.sum_mul_sum] ring _ = _ := by rw [hsum] apply Finset.sum_congr rfl intro i _ rw [hsum] _ = ∑ i : Fin (M.N n), M.expect n (fun ys => (z i ys) ^ 2) := by apply Finset.sum_congr rfl intro i _ rw [Finset.sum_eq_single i] · simp only [pow_two] · intro j _ hji exact hpair i j (Ne.symm hji) · intro hi exact (hi (Finset.mem_univ i)).elim calc M.expect n (fun ys => (M.empiricalMean n ys) ^ 2) = ((M.N n : ℝ)⁻¹) ^ 2 * ∑ i : Fin (M.N n), M.expect n (fun ys => (z i ys) ^ 2) := by simp only [empiricalMean, scoreSum] rw [← hvar, ← hscale] congr 1 funext ys ring _ ≤ ((M.N n : ℝ)⁻¹) ^ 2 * ((M.N n : ℝ) * M.B ^ 2) := by apply mul_le_mul_of_nonneg_left _ (sq_nonneg _) simpa only [Finset.sum_const_zero, Finset.sum_const, Finset.card_fin, nsmul_eq_mul] using Finset.sum_le_sum (s := univ) (fun i _ => hdiag i) _ = M.B ^ 2 / (M.N n : ℝ) := by field_simp

theorem empiricalSecond_tendstoInProbability (ε : ℝ) (hε : 0 < ε) : Tendsto (fun n => M.eventProbability n (fun ys => ε ≤ |M.empiricalSecond n ys - (M.v₀ : ℝ)|)) atTop (𝓝 0) := by classical have hhalf : 0 < ε / 2 := by linarith have hN : Tendsto (fun n => (M.N n : ℝ)) atTop atTop := tendsto_natCast_atTop_atTop.comp M.length_tendsto have hsmall : Tendsto (fun n => M.B ^ 4 / (M.N n : ℝ) / (ε / 2) ^ 2) atTop (𝓝 0) := by have h := (tendsto_const_div_atTop_nhds_zero_nat (M.B ^ 4)).comp M.length_tendsto simpa only [Function.comp_def, zero_div] using h.div_const ((ε / 2) ^ 2) have hcenter : ∀ᶠ n in atTop, |M.oneSecond n - (M.v₀ : ℝ)| < ε / 2 := by simpa only [oneSecond, Real.dist_eq] using (Metric.tendsto_nhds.1 M.variance_tendsto (ε / 2) hhalf) have hpositive : ∀ᶠ n in atTop, 0 < M.N n := M.length_tendsto.eventually (eventually_gt_atTop 0) have hnonneg : ∀ᶠ n in atTop, 0 ≤ M.eventProbability n (fun ys => ε ≤ |M.empiricalSecond n ys - (M.v₀ : ℝ)|) := by filter_upwards [] with n rw [M.eventProbability_eq_designPr] exact (M.productDesign n).Pr_nonneg _ have hupper : ∀ᶠ n in atTop, M.eventProbability n (fun ys => ε ≤ |M.empiricalSecond n ys - (M.v₀ : ℝ)|) ≤ M.B ^ 4 / (M.N n : ℝ) / (ε / 2) ^ 2 := by filter_upwards [hcenter, hpositive] with n hn hnN rw [M.eventProbability_eq_designPr] have hE : (M.productDesign n).E (M.empiricalSecond n) = M.oneSecond n := M.expect_empiricalSecond n hnN have htail : (M.productDesign n).Pr (fun ys => ε ≤ |M.empiricalSecond n ys - (M.v₀ : ℝ)|) ≤ (M.productDesign n).Pr (fun ys => ε / 2 ≤ |M.empiricalSecond n ys - M.oneSecond n|) := by apply (M.productDesign n).Pr_mono intro ys hys have ht := abs_sub_le (M.empiricalSecond n ys) (M.oneSecond n) (M.v₀ : ℝ) by_contra hc have hc' : |M.empiricalSecond n ys - M.oneSecond n| < ε / 2 := lt_of_not_ge hc linarith have hcheb := (M.productDesign n).chebyshev (M.empiricalSecond n) hhalf rw [hE] at hcheb have hvar : (M.productDesign n).Var (M.empiricalSecond n) = M.expect n (fun ys => (M.empiricalSecond n ys - M.oneSecond n) ^ 2) := by rw [show (M.productDesign n).Var (M.empiricalSecond n) = M.expect n (fun ys => (M.empiricalSecond n ys - (M.productDesign n).E (M.empiricalSecond n)) ^ 2) from rfl, hE] rw [hvar] at hcheb exact htail.trans (hcheb.trans (div_le_div_of_nonneg_right (M.empiricalSecond_mse_le n hnN) (sq_nonneg _))) exact squeeze_zero' hnonneg hupper hsmall

theorem empiricalMean_tendstoInProbability (ε : ℝ) (hε : 0 < ε) : Tendsto (fun n => M.eventProbability n (fun ys => ε ≤ |M.empiricalMean n ys|)) atTop (𝓝 0) := by classical have hN : Tendsto (fun n => (M.N n : ℝ)) atTop atTop := tendsto_natCast_atTop_atTop.comp M.length_tendsto have hsmall : Tendsto (fun n => M.B ^ 2 / (M.N n : ℝ) / ε ^ 2) atTop (𝓝 0) := by have h := (tendsto_const_div_atTop_nhds_zero_nat (M.B ^ 2)).comp M.length_tendsto simpa only [Function.comp_def, zero_div] using h.div_const (ε ^ 2) have hpositive : ∀ᶠ n in atTop, 0 < M.N n := M.length_tendsto.eventually (eventually_gt_atTop 0) have hnonneg : ∀ᶠ n in atTop, 0 ≤ M.eventProbability n (fun ys => ε ≤ |M.empiricalMean n ys|) := by filter_upwards [] with n rw [M.eventProbability_eq_designPr] exact (M.productDesign n).Pr_nonneg _ have hupper : ∀ᶠ n in atTop, M.eventProbability n (fun ys => ε ≤ |M.empiricalMean n ys|) ≤ M.B ^ 2 / (M.N n : ℝ) / ε ^ 2 := by filter_upwards [hpositive] with n hn rw [M.eventProbability_eq_designPr] have hE : (M.productDesign n).E (M.empiricalMean n) = 0 := by have hNne : (M.N n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) change M.expect n (M.empiricalMean n) = 0 simp only [expect, empiricalMean, scoreSum, Finset.mul_sum] rw [Finset.sum_comm] have hcoord (i : Fin (M.N n)) : ∑ ys : Fin (M.N n) → Y, M.mass n ys * M.f n (ys i) = 0 := by change M.expect n (fun ys => M.f n (ys i)) = 0 rw [M.expect_coordinate] exact M.centered n calc (∑ i : Fin (M.N n), ∑ ys : Fin (M.N n) → Y, M.mass n ys * ((M.N n : ℝ)⁻¹ * M.f n (ys i))) = ∑ i : Fin (M.N n), (M.N n : ℝ)⁻¹ * (∑ ys : Fin (M.N n) → Y, M.mass n ys * M.f n (ys i)) := by apply Finset.sum_congr rfl intro i _ rw [Finset.mul_sum] apply Finset.sum_congr rfl intro ys _ ring _ = 0 := by simp [hcoord] have hcheb := (M.productDesign n).chebyshev (M.empiricalMean n) hε rw [hE] at hcheb simp only [sub_zero] at hcheb have hvar : (M.productDesign n).Var (M.empiricalMean n) = M.expect n (fun ys => (M.empiricalMean n ys) ^ 2) := by rw [show (M.productDesign n).Var (M.empiricalMean n) = M.expect n (fun ys => (M.empiricalMean n ys - (M.productDesign n).E (M.empiricalMean n)) ^ 2) from rfl, hE] simp rw [hvar] at hcheb exact hcheb.trans (div_le_div_of_nonneg_right (M.empiricalMean_mse_le n hn) (sq_nonneg _)) exact squeeze_zero' hnonneg hupper hsmall

theorem fourth_index_sum (k : ℕ) (m₂ m₄ : ℝ) : (∑ p : Fin 4 → Fin k, if fourthHasSingleton p then (0 : ℝ) else if fourthConstant p then m₄ else m₂ ^ 2) = (k : ℝ) * m₄ + 3 * (k : ℝ) * ((k : ℝ) - 1) * m₂ ^ 2 := by classical have hpoint (a b c d : Fin k) : (if fourthHasSingleton (![a,b,c,d] : Fin 4 → Fin k) then 0 else if fourthConstant ![a,b,c,d] then m₄ else m₂^2) = (if a=b ∧ a=c ∧ a=d then m₄ else 0) + (if a=b ∧ c=d ∧ a≠c then m₂^2 else 0) + (if a=c ∧ b=d ∧ a≠b then m₂^2 else 0) + (if a=d ∧ b=c ∧ a≠b then m₂^2 else 0) := by have hc : fourthConstant (![a,b,c,d] : Fin 4 → Fin k) ↔ a=b ∧ a=c ∧ a=d := by simp [fourthConstant, Fin.forall_fin_succ, eq_comm] have hs : fourthHasSingleton (![a,b,c,d] : Fin 4 → Fin k) ↔ (a ≠ b ∧ a ≠ c ∧ a ≠ d) ∨ (b ≠ a ∧ b ≠ c ∧ b ≠ d) ∨ (c ≠ a ∧ c ≠ b ∧ c ≠ d) ∨ (d ≠ a ∧ d ≠ b ∧ d ≠ c) := by have hcard : fourthHasSingleton (![a,b,c,d] : Fin 4 → Fin k) ↔ ∃ i : Fin k, (if a=i then 1 else 0) + (if b=i then 1 else 0) + (if c=i then 1 else 0) + (if d=i then 1 else 0) = (1 : ℕ) := by simp only [fourthHasSingleton, Finset.card_filter, Fin.sum_univ_four] rfl rw [hcard] constructor · rintro ⟨i, hi⟩ by_cases ha : a = i <;> by_cases hb : b = i <;> by_cases hc : c = i <;> by_cases hd : d = i <;> simp_all [eq_comm] · rintro (h | h | h | h) · refine ⟨a, ?_⟩; simp_all [eq_comm] · refine ⟨b, ?_⟩; simp_all [eq_comm] · refine ⟨c, ?_⟩; simp_all [eq_comm] · refine ⟨d, ?_⟩; simp_all [eq_comm] rw [hc, hs] by_cases h₁ : a = b <;> by_cases h₂ : a = c <;> by_cases h₃ : a = d <;> by_cases h₄ : b = c <;> by_cases h₅ : b = d <;> by_cases h₆ : c = d <;> simp_all [eq_comm] have hquad (f : (Fin 4 → Fin k) → ℝ) : (∑ p, f p) = ∑ a, ∑ b, ∑ c, ∑ d, f ![a,b,c,d] := by let e : (Fin 4 → Fin k) ≃ Fin k × Fin k × Fin k × Fin k := { toFun := fun p => (p 0, p 1, p 2, p 3) invFun := fun x => ![x.1, x.2.1, x.2.2.1, x.2.2.2] left_inv := by intro p; funext i; fin_cases i <;> rfl right_inv := by intro ⟨a,b,c,d⟩; rfl } rw [Fintype.sum_equiv e f (fun x => f ![x.1,x.2.1,x.2.2.1,x.2.2.2]) (by intro p have hp : p = ![p 0,p 1,p 2,p 3] := by funext i; fin_cases i <;> rfl simpa [e] using congrArg f hp)] simp only [Fintype.sum_prod_type] have hconst : (∑ a : Fin k, ∑ b : Fin k, ∑ c : Fin k, ∑ d : Fin k, if a=b ∧ a=c ∧ a=d then m₄ else 0) = (k : ℝ) * m₄ := by simp_rw [ite_and] simp have hneq (t : ℝ) : (∑ a : Fin k, ∑ b : Fin k, if a=b then 0 else t) = (k : ℝ) * ((k : ℝ) - 1) * t := by have h (a b : Fin k) : (if a=b then (0:ℝ) else t) = t - (if a=b then t else 0) := by split_ifs <;> ring simp_rw [h, Finset.sum_sub_distrib] simp ring have hpair₁ : (∑ a : Fin k, ∑ b : Fin k, ∑ c : Fin k, ∑ d : Fin k, if a=b ∧ c=d ∧ a≠c then m₂^2 else 0) = (k : ℝ) * ((k : ℝ) - 1) * m₂^2 := by simp_rw [ite_and] simp only [ne_eq, ite_not, Finset.sum_ite_irrel, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Finset.sum_const_zero] exact hneq (m₂^2) have hpair₂ : (∑ a : Fin k, ∑ b : Fin k, ∑ c : Fin k, ∑ d : Fin k, if a=c ∧ b=d ∧ a≠b then m₂^2 else 0) = (k : ℝ) * ((k : ℝ) - 1) * m₂^2 := by simp_rw [ite_and] simp only [ne_eq, ite_not, Finset.sum_ite_irrel, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Finset.sum_const_zero] exact hneq (m₂^2) have hpair₃ : (∑ a : Fin k, ∑ b : Fin k, ∑ c : Fin k, ∑ d : Fin k, if a=d ∧ b=c ∧ a≠b then m₂^2 else 0) = (k : ℝ) * ((k : ℝ) - 1) * m₂^2 := by simp_rw [ite_and] simp only [ne_eq, ite_not, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte] exact hneq (m₂^2) rw [hquad] simp_rw [hpoint] simp_rw [Finset.sum_add_distrib] rw [hconst, hpair₁, hpair₂, hpair₃] ring

theorem expect_four_product_singleton_zero (n : ℕ) (p : Fin 4 → Fin (M.N n)) (hp : fourthHasSingleton p) : M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = 0 := by -- Factor the product by distinct coordinates using `expect_prod_coordinate`. -- The factor at the singleton index is `M.centered n`. classical obtain ⟨i, hi⟩ := hp let g : Fin (M.N n) → Y → ℝ := fun j y => ∏ a ∈ Finset.univ.filter (fun a : Fin 4 => p a = j), M.f n y have hfactor (ys : Fin (M.N n) → Y) : (∏ j, g j (ys j)) = ∏ a : Fin 4, M.f n (ys (p a)) := by simp only [g] calc (∏ j, ∏ a ∈ Finset.univ.filter (fun a : Fin 4 => p a = j), M.f n (ys j)) = ∏ j, ∏ a ∈ Finset.univ.filter (fun a : Fin 4 => p a = j), M.f n (ys (p a)) := by apply Finset.prod_congr rfl intro j _ apply Finset.prod_congr rfl intro a ha rw [(Finset.mem_filter.mp ha).2] _ = ∏ a : Fin 4, M.f n (ys (p a)) := by simpa using (Finset.prod_fiberwise univ p (fun a : Fin 4 => M.f n (ys (p a)))) have hsingle : ∑ y, M.w n y * g i y = 0 := by obtain ⟨a, ha⟩ := Finset.card_eq_one.mp hi simp [g, ha, M.centered n] calc M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = M.expect n (fun ys => ∏ j, g j (ys j)) := by congr 1; funext ys; exact (hfactor ys).symm _ = ∏ j, ∑ y, M.w n y * g j y := M.expect_prod_coordinate n g _ = 0 := Finset.prod_eq_zero (Finset.mem_univ i) hsingle

theorem expect_four_product_constant (n : ℕ) (p : Fin 4 → Fin (M.N n)) (hp : fourthConstant p) : M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = M.oneFourth n := by -- Rewrite the product as `(f n (ys (p 0))) ^ 4` and use `expect_coordinate`. have hprod (ys : Fin (M.N n) → Y) : (∏ a : Fin 4, M.f n (ys (p a))) = (M.f n (ys (p 0))) ^ 4 := by rw [Fin.prod_univ_four] simp only [hp 1, hp 2, hp 3] ring calc M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = M.expect n (fun ys => (M.f n (ys (p 0))) ^ 4) := by congr 1; funext ys; exact hprod ys _ = M.oneFourth n := by rw [M.expect_coordinate n (p 0) (fun y => (M.f n y) ^ 4)] rfl

theorem expect_four_product_two_pairs (n : ℕ) (p : Fin 4 → Fin (M.N n)) (hs : ¬ fourthHasSingleton p) (hc : ¬ fourthConstant p) : M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = (M.oneSecond n) ^ 2 := by -- Four occurrences with no singleton and at least two indices are two pairs. -- Rewrite as `f i ^ 2 * f j ^ 2` and use `expect_coordinate_mul`. classical have hcases : (p 0 = p 1 ∧ p 2 = p 3 ∧ p 0 ≠ p 2) ∨ (p 0 = p 2 ∧ p 1 = p 3 ∧ p 0 ≠ p 1) ∨ (p 0 = p 3 ∧ p 1 = p 2 ∧ p 0 ≠ p 1) := by have hseq : fourthHasSingleton p ↔ (p 0 ≠ p 1 ∧ p 0 ≠ p 2 ∧ p 0 ≠ p 3) ∨ (p 1 ≠ p 0 ∧ p 1 ≠ p 2 ∧ p 1 ≠ p 3) ∨ (p 2 ≠ p 0 ∧ p 2 ≠ p 1 ∧ p 2 ≠ p 3) ∨ (p 3 ≠ p 0 ∧ p 3 ≠ p 1 ∧ p 3 ≠ p 2) := by simp only [fourthHasSingleton, Finset.card_filter, Fin.sum_univ_four] constructor · rintro ⟨i, hi⟩ by_cases h0 : p 0 = i <;> by_cases h1 : p 1 = i <;> by_cases h2 : p 2 = i <;> by_cases h3 : p 3 = i <;> simp_all [eq_comm] · rintro (h | h | h | h) · refine ⟨p 0, ?_⟩; simp_all [eq_comm] · refine ⟨p 1, ?_⟩; simp_all [eq_comm] · refine ⟨p 2, ?_⟩; simp_all [eq_comm] · refine ⟨p 3, ?_⟩; simp_all [eq_comm] have hceq : fourthConstant p ↔ p 0 = p 1 ∧ p 0 = p 2 ∧ p 0 = p 3 := by simp [fourthConstant, Fin.forall_fin_succ] constructor <;> rintro ⟨h1, h2, h3⟩ <;> exact ⟨h1.symm, h2.symm, h3.symm⟩ rw [hseq] at hs rw [hceq] at hc by_cases h01 : p 0 = p 1 <;> by_cases h02 : p 0 = p 2 <;> by_cases h03 : p 0 = p 3 <;> by_cases h12 : p 1 = p 2 <;> by_cases h13 : p 1 = p 3 <;> by_cases h23 : p 2 = p 3 <;> simp_all [eq_comm] rcases hcases with ⟨h01, h23, h02⟩ | ⟨h02, h13, h01⟩ | ⟨h03, h12, h01⟩ · have hprod (ys : Fin (M.N n) → Y) : (∏ a : Fin 4, M.f n (ys (p a))) = (M.f n (ys (p 0))) ^ 2 * (M.f n (ys (p 2))) ^ 2 := by rw [Fin.prod_univ_four, h01, h23] ring calc M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = M.expect n (fun ys => (M.f n (ys (p 0))) ^ 2 * (M.f n (ys (p 2))) ^ 2) := by congr 1; funext ys; exact hprod ys _ = (M.oneSecond n) ^ 2 := by rw [M.expect_coordinate_mul n (p 0) (p 2) h02 (fun y => (M.f n y) ^ 2) (fun y => (M.f n y) ^ 2)] simp only [oneSecond] ring · have hprod (ys : Fin (M.N n) → Y) : (∏ a : Fin 4, M.f n (ys (p a))) = (M.f n (ys (p 0))) ^ 2 * (M.f n (ys (p 1))) ^ 2 := by rw [Fin.prod_univ_four, h02, h13] ring calc M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = M.expect n (fun ys => (M.f n (ys (p 0))) ^ 2 * (M.f n (ys (p 1))) ^ 2) := by congr 1; funext ys; exact hprod ys _ = (M.oneSecond n) ^ 2 := by rw [M.expect_coordinate_mul n (p 0) (p 1) h01 (fun y => (M.f n y) ^ 2) (fun y => (M.f n y) ^ 2)] simp only [oneSecond] ring · have hprod (ys : Fin (M.N n) → Y) : (∏ a : Fin 4, M.f n (ys (p a))) = (M.f n (ys (p 0))) ^ 2 * (M.f n (ys (p 1))) ^ 2 := by rw [Fin.prod_univ_four, h03, h12] ring calc M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = M.expect n (fun ys => (M.f n (ys (p 0))) ^ 2 * (M.f n (ys (p 1))) ^ 2) := by congr 1; funext ys; exact hprod ys _ = (M.oneSecond n) ^ 2 := by rw [M.expect_coordinate_mul n (p 0) (p 1) h01 (fun y => (M.f n y) ^ 2) (fun y => (M.f n y) ^ 2)] simp only [oneSecond] ring

theorem scoreSum_fourth_expansion (n : ℕ) : M.expect n (fun ys => (M.scoreSum n ys) ^ 4) = (M.N n : ℝ) * M.oneFourth n + 3 * (M.N n : ℝ) * ((M.N n : ℝ) - 1) * (M.oneSecond n) ^ 2 := by classical have hpoint (p : Fin 4 → Fin (M.N n)) : M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) = if fourthHasSingleton p then 0 else if fourthConstant p then M.oneFourth n else (M.oneSecond n) ^ 2 := by by_cases hs : fourthHasSingleton p · simp [hs, M.expect_four_product_singleton_zero n p hs] · by_cases hc : fourthConstant p · simp [hs, hc, M.expect_four_product_constant n p hc] · simp [hs, hc, M.expect_four_product_two_pairs n p hs hc] calc M.expect n (fun ys => (M.scoreSum n ys) ^ 4) = M.expect n (fun ys => ∑ p : Fin 4 → Fin (M.N n), ∏ a : Fin 4, M.f n (ys (p a))) := by congr 1 funext ys exact Fintype.sum_pow (fun i : Fin (M.N n) => M.f n (ys i)) 4 _ = ∑ p : Fin 4 → Fin (M.N n), M.expect n (fun ys => ∏ a : Fin 4, M.f n (ys (p a))) := by simp only [expect, Finset.mul_sum] rw [Finset.sum_comm] _ = _ := by simp_rw [hpoint] exact fourth_index_sum (M.N n) (M.oneSecond n) (M.oneFourth n)

theorem iIndepFun_nat_pad {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (d : ℕ) (X : Fin d → Ω → ℝ) (hX : iIndepFun X μ) : iIndepFun (fun k ω => if h : k < d then X ⟨k, h⟩ ω else 0) μ := by have hfun : (fun k ω => if h : k < d then X ⟨k, h⟩ ω else (0 : ℝ)) = (fun k : ℕ => if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) := by funext k ω split_ifs <;> rfl rw [hfun] classical rw [iIndepFun_iff_measure_inter_preimage_eq_mul] intro S sets hsets let T : Finset (Fin d) := Finset.univ.filter (fun j => (j : ℕ) ∈ S) let U : Finset ℕ := S.filter (fun k => k < d) have hTU : T.image val = U := by ext k rw [mem_image] simp only [U, mem_filter] constructor · rintro ⟨j, hj, rfl⟩ exact ⟨(Finset.mem_filter.mp hj).2, j.isLt⟩ · rintro ⟨hkS, hkD⟩ exact ⟨⟨k, hkD⟩, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hkS⟩, rfl⟩ have hprob : μ univ = 1 := by have h := hX.measure_inter_preimage_eq_mul (∅ : Finset (Fin d)) (sets := fun _ => univ) (by simp) simpa using h have hT := hX.measure_inter_preimage_eq_mul T (sets := fun j : Fin d => sets j.val) (by intro j hj; exact hsets j.val ((Finset.mem_filter.mp hj).2)) have hbelow : μ (⋂ k ∈ U, (if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k) = ∏ k ∈ U, μ ((if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k) := by have hI : (⋂ k ∈ U, (if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k) = ⋂ j ∈ T, X j ⁻¹' sets j.val := by ext ω simp only [Set.mem_iInter] constructor · intro h j hj have hjS : j.val ∈ S := (Finset.mem_filter.mp hj).2 have hjU : j.val ∈ U := Finset.mem_filter.mpr ⟨hjS, j.isLt⟩ simpa [j.isLt] using h j.val hjU · intro h k hk have hkD : k < d := (Finset.mem_filter.mp hk).2 have hkS : k ∈ S := (Finset.mem_filter.mp hk).1 simpa [hkD] using h ⟨k, hkD⟩ (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hkS⟩) rw [hI] convert hT using 1 rw [← hTU, Finset.prod_image] · apply Finset.prod_congr rfl intro j hj simp [j.isLt] · exact Fin.val_injective.injOn by_cases hbad : ∃ k ∈ S, ¬ k < d ∧ (0 : ℝ) ∉ sets k · obtain ⟨k, hkS, hkD, hk0⟩ := hbad have hzero : ((if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k) = ∅ := by simp [hkD, hk0] have hmem : (⋂ i ∈ S, (if hi : i < d then X ⟨i, hi⟩ else fun _ => 0) ⁻¹' sets i) = ∅ := by ext ω simp only [Set.mem_empty_iff_false, iff_false] intro hω have := Set.mem_iInter.mp (Set.mem_iInter.mp hω k) hkS simp [hzero] at this rw [hmem, measure_empty, Finset.prod_eq_zero hkS] simp [hzero] · have hout : ∀ k ∈ S, ¬ k < d → (0 : ℝ) ∈ sets k := by intro k hkS hkD by_contra hk0 exact hbad ⟨k, hkS, hkD, hk0⟩ have hI : (⋂ k ∈ S, (if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k) = ⋂ k ∈ U, (if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k := by ext ω simp only [Set.mem_iInter] constructor · intro h k hk exact h k (Finset.mem_filter.mp hk).1 · intro h k hkS by_cases hkD : k < d · exact h k (Finset.mem_filter.mpr ⟨hkS, hkD⟩) · simp [hkD, hout k hkS hkD] rw [hI, hbelow] have hprod : (∏ k ∈ S, μ ((if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k)) = ∏ k ∈ U, μ ((if hk : k < d then X ⟨k, hk⟩ else fun _ => 0) ⁻¹' sets k) := by rw [Finset.prod_filter] apply Finset.prod_congr rfl intro k hkS by_cases hkD : k < d · simp [hkD] · simp [hkD, hout k hkS hkD, hprob] exact hprod.symm

theorem standardizedIncrement_memLp (n k : ℕ) : MemLp (M.standardizedIncrement n k) 2 (M.rowMeasure n) := by have : IsProbabilityMeasure (M.rowMeasure n) := by change IsProbabilityMeasure (M.productDesign n).toMeasure infer_instance exact MemLp.of_discrete

theorem standardizedIncrement_mean_zero (n k : ℕ) (hk : k < M.N n) : ∫ ys, M.standardizedIncrement n k ys ∂M.rowMeasure n = 0 := by rw [M.integral_rowMeasure_eq_expect] have hcoord := M.expect_coordinate n ⟨k, hk⟩ (M.f n) have hcenter := M.centered n calc M.expect n (M.standardizedIncrement n k) = (sqrt (M.N n : ℝ) * sqrt (M.v₀ : ℝ))⁻¹ * M.expect n (fun ys => M.f n (ys ⟨k, hk⟩)) := by simp only [expect, standardizedIncrement, dif_pos hk, Finset.mul_sum] apply Finset.sum_congr rfl intro ys _ ring _ = 0 := by rw [hcoord, hcenter, mul_zero]

theorem standardizedIncrement_independent (n : ℕ) : iIndepFun (M.standardizedIncrement n) (M.rowMeasure n) := by let X : Fin (M.N n) → (Fin (M.N n) → Y) → ℝ := fun i ys => (sqrt (M.N n : ℝ) * sqrt (M.v₀ : ℝ))⁻¹ * M.f n (ys i) have hX : iIndepFun X (M.rowMeasure n) := by apply (M.rowMeasure_independent n).comp (fun _ y => (sqrt (M.N n : ℝ) * sqrt (M.v₀ : ℝ))⁻¹ * M.f n y) intro i exact measurable_of_finite _ have : IsProbabilityMeasure (M.rowMeasure n) := by change IsProbabilityMeasure (M.productDesign n).toMeasure infer_instance have hpad := iIndepFun_nat_pad (M.rowMeasure n) (M.N n) X hX convert hpad using 1 funext k ys simp only [standardizedIncrement, X]

theorem standardizedIncrement_integral_sq (n k : ℕ) (hk : k < M.N n) : (∫ ys, (M.standardizedIncrement n k ys) ^ 2 ∂M.rowMeasure n) = M.oneSecond n / ((M.N n : ℝ) * (M.v₀ : ℝ)) := by -- Rewrite the integral as `expect`, extract the constant square, and use -- `expect_coordinate` for the score square. `hk` and `variance_pos` make -- both denominator factors nonzero. have hscale : ((sqrt (M.N n : ℝ) * sqrt (M.v₀ : ℝ))⁻¹) ^ 2 = ((M.N n : ℝ) * (M.v₀ : ℝ))⁻¹ := by rw [inv_pow, mul_pow, Real.sq_sqrt (Nat.cast_nonneg _), Real.sq_sqrt (show 0 ≤ (M.v₀ : ℝ) by positivity)] rw [M.integral_rowMeasure_eq_expect] calc M.expect n (fun ys => (M.standardizedIncrement n k ys) ^ 2) = ((sqrt (M.N n : ℝ) * sqrt (M.v₀ : ℝ))⁻¹) ^ 2 * M.expect n (fun ys => (M.f n (ys ⟨k, hk⟩)) ^ 2) := by simp only [expect, standardizedIncrement, dif_pos hk, Finset.mul_sum] apply Finset.sum_congr rfl intro ys _ ring _ = M.oneSecond n / ((M.N n : ℝ) * (M.v₀ : ℝ)) := by rw [M.expect_coordinate n ⟨k, hk⟩ (fun y => (M.f n y) ^ 2), ← oneSecond, hscale] ring

theorem standardizedIncrement_integral_fourth_le (n k : ℕ) (hk : k < M.N n) : (∫ ys, (M.standardizedIncrement n k ys) ^ 4 ∂M.rowMeasure n) ≤ M.B ^ 4 / ((M.N n : ℝ) ^ 2 * (M.v₀ : ℝ) ^ 2) := by -- Use `expect_coordinate` after extracting the scale. The mass-weighted -- fourth score moment is at most `B ^ 4` by `bound`, `mass_nonneg`, and -- `mass_one`. Both denominator factors are positive. have hscale : ((sqrt (M.N n : ℝ) * sqrt (M.v₀ : ℝ))⁻¹) ^ 4 = (((M.N n : ℝ) ^ 2) * ((M.v₀ : ℝ) ^ 2))⁻¹ := by rw [show (4 : ℕ) = 2 * 2 by norm_num, pow_mul, inv_pow, mul_pow, Real.sq_sqrt (Nat.cast_nonneg _), Real.sq_sqrt (show 0 ≤ (M.v₀ : ℝ) by positivity)] rw [inv_pow, mul_pow] have hfour : (∑ y, M.w n y * (M.f n y) ^ 4) ≤ M.B ^ 4 := by calc (∑ y, M.w n y * (M.f n y) ^ 4) ≤ ∑ y, M.w n y * M.B ^ 4 := by apply Finset.sum_le_sum intro y _ apply mul_le_mul_of_nonneg_left _ (M.mass_nonneg n y) have hB : 0 ≤ M.B := (abs_nonneg _).trans (M.bound n y) have hf2 : (M.f n y) ^ 2 ≤ M.B ^ 2 := by have hp : 0 ≤ (M.B - |M.f n y|) * (M.B + |M.f n y|) := mul_nonneg (sub_nonneg.mpr (M.bound n y)) (add_nonneg hB (abs_nonneg _)) nlinarith [sq_abs (M.f n y)] calc (M.f n y) ^ 4 = ((M.f n y) ^ 2) ^ 2 := by ring _ ≤ (M.B ^ 2) ^ 2 := pow_le_pow_left₀ (sq_nonneg _) hf2 2 _ = M.B ^ 4 := by ring _ = M.B ^ 4 := by rw [← Finset.sum_mul, M.mass_one n]; ring rw [M.integral_rowMeasure_eq_expect] calc M.expect n (fun ys => (M.standardizedIncrement n k ys) ^ 4) = ((sqrt (M.N n : ℝ) * sqrt (M.v₀ : ℝ))⁻¹) ^ 4 * M.expect n (fun ys => (M.f n (ys ⟨k, hk⟩)) ^ 4) := by simp only [expect, standardizedIncrement, dif_pos hk, Finset.mul_sum] apply Finset.sum_congr rfl intro ys _ ring _ = (∑ y, M.w n y * (M.f n y) ^ 4) / ((M.N n : ℝ) ^ 2 * (M.v₀ : ℝ) ^ 2) := by rw [M.expect_coordinate n ⟨k, hk⟩ (fun y => (M.f n y) ^ 4), hscale] ring _ ≤ M.B ^ 4 / ((M.N n : ℝ) ^ 2 * (M.v₀ : ℝ) ^ 2) := by exact div_le_div_of_nonneg_right hfour (by positivity)

theorem standardizedArray_varianceSum_tendsto : Tendsto M.standardizedArray.varianceSum atTop (𝓝 1) := by have hlim : Tendsto (fun n => M.oneSecond n / (M.v₀ : ℝ)) atTop (𝓝 1) := by have hv : (M.v₀ : ℝ) ≠ 0 := ne_of_gt (by exact_mod_cast M.variance_pos) simpa only [oneSecond, div_self hv] using M.variance_tendsto.div_const (M.v₀ : ℝ) have hpositive : ∀ᶠ n in atTop, 0 < M.N n := M.length_tendsto.eventually (eventually_gt_atTop 0) apply hlim.congr' filter_upwards [hpositive] with n hn symm change (∑ k ∈ range (M.N n), ∫ ys, (M.standardizedIncrement n k ys) ^ 2 ∂M.rowMeasure n) = M.oneSecond n / (M.v₀ : ℝ) rw [Finset.sum_congr rfl (fun k hk => M.standardizedIncrement_integral_sq n k (Finset.mem_range.mp hk))] simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul] have hN : (M.N n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) have hv : (M.v₀ : ℝ) ≠ 0 := ne_of_gt (by exact_mod_cast M.variance_pos) field_simp

theorem standardizedArray_lyapunovSum_two_tendsto : Tendsto (M.standardizedArray.lyapunovSum 2) atTop (𝓝 0) := by have hsmall : Tendsto (fun n => (M.B ^ 4 / (M.v₀ : ℝ) ^ 2) / (M.N n : ℝ)) atTop (𝓝 0) := by simpa only [Function.comp_def] using (tendsto_const_div_atTop_nhds_zero_nat (M.B ^ 4 / (M.v₀ : ℝ) ^ 2)).comp M.length_tendsto have hnonneg : ∀ n, 0 ≤ M.standardizedArray.lyapunovSum 2 n := by intro n change 0 ≤ ∑ k ∈ range (M.N n), ∫ ys, |M.standardizedIncrement n k ys| ^ (2 + (2 : ℝ)) ∂M.rowMeasure n apply Finset.sum_nonneg intro k hk apply integral_nonneg intro ys exact Real.rpow_nonneg (abs_nonneg _) _ have hpositive : ∀ᶠ n in atTop, 0 < M.N n := M.length_tendsto.eventually (eventually_gt_atTop 0) have hbound : ∀ᶠ n in atTop, M.standardizedArray.lyapunovSum 2 n ≤ (M.B ^ 4 / (M.v₀ : ℝ) ^ 2) / (M.N n : ℝ) := by filter_upwards [hpositive] with n hn change (∑ k ∈ range (M.N n), ∫ ys, |M.standardizedIncrement n k ys| ^ (2 + (2 : ℝ)) ∂M.rowMeasure n) ≤ _ calc (∑ k ∈ range (M.N n), ∫ ys, |M.standardizedIncrement n k ys| ^ (2 + (2 : ℝ)) ∂M.rowMeasure n) ≤ ∑ k ∈ range (M.N n), M.B ^ 4 / ((M.N n : ℝ) ^ 2 * (M.v₀ : ℝ) ^ 2) := by apply Finset.sum_le_sum intro k hk calc (∫ ys, |M.standardizedIncrement n k ys| ^ (2 + (2 : ℝ)) ∂M.rowMeasure n) = ∫ ys, (M.standardizedIncrement n k ys) ^ 4 ∂M.rowMeasure n := by congr 1 funext ys rw [show (2 : ℝ) + 2 = (4 : ℕ) by norm_num, Real.rpow_natCast] have hpow : 0 ≤ (M.standardizedIncrement n k ys) ^ 4 := by positivity rw [← abs_pow, abs_of_nonneg hpow] _ ≤ _ := M.standardizedIncrement_integral_fourth_le n k (Finset.mem_range.mp hk) _ = (M.B ^ 4 / (M.v₀ : ℝ) ^ 2) / (M.N n : ℝ) := by simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul] have hN : (M.N n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) have hv : (M.v₀ : ℝ) ≠ 0 := ne_of_gt (by exact_mod_cast M.variance_pos) field_simp exact squeeze_zero' (Filter.Eventually.of_forall hnonneg) hbound hsmall

theorem normalizedCDF_eq_cdf [MeasurableSpace Y] [MeasurableSingletonClass Y] (n : ℕ) (t : ℝ) : M.normalizedCDF n t = cdf (M.normalizedSumLaw n) t := by classical have : IsProbabilityMeasure (M.rowMeasure n) := by change IsProbabilityMeasure (M.productDesign n).toMeasure infer_instance have : IsProbabilityMeasure (M.normalizedSumLaw n) := Measure.isProbabilityMeasure_map (measurable_of_finite (M.normalizedSum n)).aemeasurable rw [cdf_eq_real, normalizedSumLaw, measureReal_def, Measure.map_apply (measurable_of_finite (M.normalizedSum n)) measurableSet_Iic] change M.normalizedCDF n t = (M.rowMeasure n).real (M.normalizedSum n ⁻¹' Iic t) rw [← integral_indicator_one ((measurable_of_finite (M.normalizedSum n)) measurableSet_Iic)] rw [normalizedCDF, ← M.integral_rowMeasure_eq_expect] congr 1

theorem eventually_small_normalized_coordinate (ε : ℝ) (hε : 0 < ε) : ∀ᶠ n in atTop, ∀ y, |(sqrt (M.N n : ℝ))⁻¹ * M.f n y| < ε := by have hsqrt : Tendsto (fun n : ℕ => sqrt (M.N n : ℝ)) atTop atTop := Real.tendsto_sqrt_atTop.comp (tendsto_natCast_atTop_atTop.comp M.length_tendsto) have hinv : Tendsto (fun n : ℕ => (sqrt (M.N n : ℝ))⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_zero.comp hsqrt have hlim : Tendsto (fun n : ℕ => (sqrt (M.N n : ℝ))⁻¹ * max M.B 0) atTop (𝓝 0) := by simpa using hinv.mul_const (max M.B 0) have hsmall : ∀ᶠ n in atTop, (sqrt (M.N n : ℝ))⁻¹ * max M.B 0 < ε := by exact hlim.eventually_lt_const hε filter_upwards [hsmall] with n hn y calc |(sqrt (M.N n : ℝ))⁻¹ * M.f n y| = (sqrt (M.N n : ℝ))⁻¹ * |M.f n y| := by rw [abs_mul, abs_of_nonneg (inv_nonneg.mpr (Real.sqrt_nonneg _))] _ ≤ (sqrt (M.N n : ℝ))⁻¹ * max M.B 0 := by exact mul_le_mul_of_nonneg_left ((M.bound n y).trans (le_max_left _ _)) (inv_nonneg.mpr (Real.sqrt_nonneg _)) _ < ε := hn