Experimentation.Super­Population.Mean­CLT

theorem centeredNormalizedField_sq_integral (hL2 : ∀ i, MemLp (Y i) 2 μ) (s : ℝ) (hs_pos : 0 < s) (hs2 : s ^ 2 = variance (fun ω => ∑ i, Y i ω) μ) : ∫ ω, (depSum (centeredNormalizedField Y adj hrefl hsymm hmeasY hindepY s).X ω) ^ 2 ∂μ = 1 := by let S : Ω → ℝ := fun ω => ∑ i, Y i ω let C : ℝ := ∑ i, ∫ x, Y i x ∂μ have hs_ne : s ≠ 0 := ne_of_gt hs_pos have hS_mem : MemLp S 2 μ := by simpa [S] using (memLp_finset_sum univ (fun i _ => hL2 i)) have hsum_eq : depSum (centeredNormalizedField Y adj hrefl hsymm hmeasY hindepY s).X = fun ω => (S ω - C) / s := by funext ω simp only [depSum, centeredNormalizedField_X] dsimp [S, C] rw [← Finset.sum_div, Finset.sum_sub_distrib] have hS_integral : ∫ ω, S ω ∂μ = C := by dsimp [S, C] rw [integral_finset_sum univ] intro i _ exact (hL2 i).integrable (by norm_num) have hsum_int_zero : ∫ ω, depSum (centeredNormalizedField Y adj hrefl hsymm hmeasY hindepY s).X ω ∂μ = 0 := by rw [hsum_eq, integral_div] rw [integral_sub (hS_mem.integrable (by norm_num)) (integrable_const C)] simp [hS_integral, integral_const, probReal_univ] have hsum_aemeas : AEMeasurable (depSum (centeredNormalizedField Y adj hrefl hsymm hmeasY hindepY s).X) μ := by rw [hsum_eq] exact (hS_mem.aemeasurable.sub_const C).div_const s rw [← variance_of_integral_eq_zero hsum_aemeas hsum_int_zero, hsum_eq] have hscaled_mem : MemLp (fun ω => S ω / s) 2 μ := by convert hS_mem.mul_const (1 / s) using 1 ext ω ring calc variance (fun ω => (S ω - C) / s) μ = variance (fun ω => S ω / s) μ := by calc variance (fun ω => (S ω - C) / s) μ = variance (fun ω => S ω / s + (-C / s)) μ := by congr ext ω ring _ = variance (fun ω => S ω / s) μ := by exact variance_add_const hscaled_mem.aestronglyMeasurable (-C / s) _ = variance S μ / s ^ 2 := by calc variance (fun ω => S ω / s) μ = variance (fun ω => S ω * (1 / s)) μ := by congr ext ω ring _ = variance S μ * (1 / s) ^ 2 := by rw [variance_mul_const] _ = variance S μ / s ^ 2 := by field_simp [hs_ne] _ = 1 := by have hvarS : variance S μ = s ^ 2 := by simpa [S] using hs2.symm rw [hvarS] exact div_self (pow_ne_zero 2 hs_ne)

theorem networkMean_clt {V : ℕ → Type*} [∀ n, Fintype (V n)] {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)] (μ : ∀ n, Measure (Ω n)) [∀ n, IsProbabilityMeasure (μ n)] (Y : ∀ n, V n → Ω n → ℝ) (adj : ∀ n, V n → V n → Prop) [∀ n, DecidableRel (adj n)] (hrefl : ∀ n i, adj n i i) (hsymm : ∀ n i j, adj n i j → adj n j i) (hmeasY : ∀ n i, Measurable (Y n i)) (hindepY : ∀ n, ∀ A B : Finset (V n), (∀ a ∈ A, ∀ b ∈ B, ¬ adj n a b) → IndepFun (fun ω => fun k : A => Y n k ω) (fun ω => fun k : B => Y n k ω) (μ n)) (m : ℕ) (hdeg : ∀ n i, (Finset.univ.filter (fun j => adj n i j)).card ≤ m) (hL2 : ∀ n i, MemLp (Y n i) 2 (μ n)) (s : ℕ → ℝ) (hs_pos : ∀ n, 0 < s n) (hs2 : ∀ n, (s n) ^ 2 = variance (fun ω => ∑ i, Y n i ω) (μ n)) (c : ℕ → ℝ) (hc : ∀ n i ω, |Y n i ω - ∫ x, Y n i x ∂(μ n)| ≤ c n) (hsmall : Tendsto (fun n => (card (V n) : ℝ) * (c n / s n) ^ 3) atTop (𝓝 0)) (t : ℝ) : Tendsto (fun n => (μ n).real {ω | (∑ i, Y n i ω - ∑ i, ∫ x, Y n i x ∂(μ n)) / s n ≤ t}) atTop (𝓝 ((gaussianReal 0 1).real (Iic t))) := by classical let F : ∀ n, NetworkDependence (V n) (Ω n) (μ n) := fun n => centeredNormalizedField (Y n) (adj n) (hrefl n) (hsymm n) (hmeasY n) (hindepY n) (s n) let B : ℕ → ℝ := fun n => 2 * c n / s n have hdeg' : ∀ n i, ((F n).toDepGraph.nbhd i).card ≤ m := by intro n i change (Finset.univ.filter (fun j => adj n i j)).card ≤ m exact hdeg n i have hΩne : ∀ n, Nonempty (Ω n) := by intro n by_contra hΩ haveI : IsEmpty (Ω n) := not_nonempty_iff.mp hΩ have hzero : μ n = 0 := by ext S have hS : S = ∅ := by ext x exact isEmptyElim x simp [hS] exact (MeasureTheory.IsProbabilityMeasure.ne_zero (μ n)) hzero have hne : ∀ n, Nonempty (V n) := by intro n by_contra hV haveI : IsEmpty (V n) := not_nonempty_iff.mp hV have hsum : (fun ω => ∑ i, Y n i ω) = (0 : Ω n → ℝ) := by funext ω exact Fintype.sum_empty (fun i => Y n i ω) have hs2zero : (s n) ^ 2 = 0 := by rw [hs2 n, hsum] exact variance_zero (μ n) have hs2pos : 0 < (s n) ^ 2 := sq_pos_of_pos (hs_pos n) nlinarith have hcard : ∀ n, 1 ≤ card (V n) := by intro n exact Fintype.card_pos_iff.mpr (hne n) have hc_nonneg : ∀ n, 0 ≤ c n := by intro n obtain ⟨i⟩ := hne n obtain ⟨ω⟩ := hΩne n exact le_trans (abs_nonneg _) (hc n i ω) have hB : ∀ n, 0 ≤ B n := by intro n exact div_nonneg (mul_nonneg zero_le_two (hc_nonneg n)) (le_of_lt (hs_pos n)) have hbound : ∀ n i ω, |(F n).X i ω| ≤ B n := by intro n i ω exact centeredNormalizedField_abs_le (Y n) (adj n) (hrefl n) (hsymm n) (hmeasY n) (hindepY n) (s n) (hs_pos n) (c n) (hc n) i ω have hNB3 : Tendsto (fun n => (card (V n) : ℝ) * (B n) ^ 3) atTop (𝓝 0) := by have hfac : (fun n => (card (V n) : ℝ) * (B n) ^ 3) = (fun n => 8 * ((card (V n) : ℝ) * (c n / s n) ^ 3)) := by funext n dsimp [B] ring rw [hfac] simpa using hsmall.const_mul 8 have hB0 : Tendsto B atTop (𝓝 0) := by have hB3_0 : Tendsto (fun n => (B n) ^ 3) atTop (𝓝 0) := by refine squeeze_zero (fun n => pow_nonneg (hB n) 3) (fun n => ?_) hNB3 have hcardR : (1 : ℝ) ≤ (card (V n) : ℝ) := by exact_mod_cast hcard n exact le_mul_of_one_le_left (pow_nonneg (hB n) 3) hcardR have hroot : Tendsto (fun n => ((B n) ^ 3) ^ ((3 : ℕ)⁻¹ : ℝ)) atTop (𝓝 0) := by simpa [Function.comp_def] using (Real.continuousAt_rpow_const 0 ((3 : ℕ)⁻¹ : ℝ) (inr (by positivity))).tendsto.comp hB3_0 exact hroot.congr (fun n => Real.pow_rpow_inv_natCast (hB n) (by norm_num : (3 : ℕ) ≠ 0)) have hmean : ∀ n i, ∫ ω, (F n).X i ω ∂(μ n) = 0 := by intro n i exact centeredNormalizedField_integral_eq_zero (Y n) (adj n) (hrefl n) (hsymm n) (hmeasY n) (hindepY n) (hL2 n) (s n) i have hvar : ∀ n, ∫ ω, (depSum (F n).X ω) ^ 2 ∂(μ n) = 1 := by intro n exact centeredNormalizedField_sq_integral (Y n) (adj n) (hrefl n) (hsymm n) (hmeasY n) (hindepY n) (hL2 n) (s n) (hs_pos n) (hs2 n) have hclt := networkSum_clt μ F m hdeg' B hB hbound hB0 hNB3 hmean hvar t refine hclt.congr (fun n => ?_) have hWmeas : Measurable (depSum (F n).X) := by exact measurable_sum _ (fun i _ => (F n).meas i) have hset : (depSum (F n).X) ⁻¹' Iic t = {ω | (∑ i, Y n i ω - ∑ i, ∫ x, Y n i x ∂(μ n)) / s n ≤ t} := by ext ω simp only [Set.mem_preimage, Set.mem_Iic, Set.mem_setOf_eq] dsimp [depSum, F] have hsum : (∑ i, (Y n i ω - ∫ x, Y n i x ∂(μ n)) / s n) = (∑ i, Y n i ω - ∑ i, ∫ x, Y n i x ∂(μ n)) / s n := by rw [← Finset.sum_sub_distrib, Finset.sum_div] rw [hsum] rw [← hset, MeasureTheory.map_measureReal_apply hWmeas measurableSet_Iic]