Mathlib.Probability.Stein­Method

theorem steinSol_hasDerivAt (h : ℝ → ℝ) (hh : Continuous h) {C : ℝ} (hb : ∀ x, |h x| ≤ C) (w : ℝ) : HasDerivAt (steinSol h) (w * steinSol h w + (h w - gExpect h)) w := by set g := steinIntegrand h with hg_def have hg_cont : Continuous g := steinIntegrand_continuous h hh have hg_int : Integrable g := steinIntegrand_integrable hh hb -- The cumulative integral `G w = ∫ x in Iic w, g x` has derivative `g w`. set G : ℝ → ℝ := fun u => ∫ x in Iic u, g x with hG_def have hG_deriv : HasDerivAt G (g w) w := by -- Base point `a := w - 1`. set a : ℝ := w - 1 with ha_def have hIIc_int : ∀ u : ℝ, IntegrableOn g (Iic u) := fun u => hg_int.integrableOn -- `G u = (∫ x in Iic a, g) + ∫ x in a..u, g`. have hGeq : ∀ u : ℝ, G u = (∫ x in Iic a, g x) + ∫ x in a..u, g x := by intro u have := intervalIntegral.integral_Iic_sub_Iic (hIIc_int a) (hIIc_int u) rw [hG_def]; linarith [this] have hivint : IntervalIntegrable g MeasureTheory.volume a w := hg_int.intervalIntegrable have hd : HasDerivAt (fun u => ∫ x in a..u, g x) (g w) w := intervalIntegral.integral_hasDerivAt_right hivint hg_cont.aestronglyMeasurable.stronglyMeasurableAtFilter hg_cont.continuousAt have hd' : HasDerivAt (fun u => (∫ x in Iic a, g x) + ∫ x in a..u, g x) (g w) w := by simpa using hd.const_add (∫ x in Iic a, g x) exact hd'.congr_of_eventuallyEq (Filter.Eventually.of_forall (fun u => hGeq u)) -- Derivative of `e^{w²/2}`. have hexp_deriv : HasDerivAt (fun u : ℝ => exp (u ^ 2 / 2)) (w * exp (w ^ 2 / 2)) w := by have hpow : HasDerivAt (fun u : ℝ => u ^ 2 / 2) w w := by have := (hasDerivAt_pow 2 w).div_const 2 simpa using this have := hpow.exp simpa [mul_comm] using this -- Product rule. have hprod := hexp_deriv.mul hG_deriv -- Rewrite `steinSol h = fun u => e^{u²/2} * G u`. have hsol_eq : steinSol h = fun u => exp (u ^ 2 / 2) * G u := by funext u; rfl -- Match derivatives: `w * steinSol h w + (h w - gExpect h)`. have hgcancel : exp (w ^ 2 / 2) * g w = h w - gExpect h := by rw [hg_def, steinIntegrand, ← mul_assoc, mul_comm (exp _) (h w - gExpect h), mul_assoc, ← Real.exp_add] rw [show w ^ 2 / 2 + -w ^ 2 / 2 = 0 by ring, Real.exp_zero, mul_one] rw [hsol_eq] refine hprod.congr_deriv ?_ rw [hgcancel]; ring

theorem stein_local_dependence_bound (X : ι → Ω → ℝ) (N : ι → Finset ι) (hmeas : ∀ i, Measurable (X i)) {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ i ω, |X i ω| ≤ B) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hindep : ∀ i, IndepFun (X i) (fun ω => ∑ j ∈ univ \ N i, X j ω) μ) (hvar : ∫ ω, (depSum X ω) ^ 2 ∂μ = 1) (h : ℝ → ℝ) {C L : ℝ} (hb : ∀ x, |h x| ≤ C) (hd : ∀ x, |deriv h x| ≤ L) (hdiff : Differentiable ℝ h) : |(∫ ω, h (depSum X ω) ∂μ) - gExpect h| ≤ 2 * L * sqrt (variance (fun ω => ∑ i, X i ω * nbhdSum X N i ω) μ) + L * ∑ i, ∫ ω, |X i ω| * (nbhdSum X N i ω) ^ 2 ∂μ := by classical have hh : Continuous h := hdiff.continuous -- Abbreviations. set W : Ω → ℝ := depSum X with hW set T : ι → Ω → ℝ := fun i => nbhdSum X N i with hT set S : ι → Ω → ℝ := fun i ω => ∑ j ∈ univ \ N i, X j ω with hS set f : ℝ → ℝ := steinSol h with hf set f' : ℝ → ℝ := deriv (steinSol h) with hf' set Y : Ω → ℝ := fun ω => ∑ i, X i ω * T i ω with hY have hL : 0 ≤ L := le_trans (abs_nonneg (deriv h 0)) (hd 0) -- Continuity / measurability of the Stein solution and its derivative. have hfdiff : Differentiable ℝ f := fun w => (steinSol_hasDerivAt h hh hb w).differentiableAt have hfcont : Continuous f := hfdiff.continuous have hf'cont : Continuous f' := steinSol_deriv_continuous h hh hL hb hd hdiff have hfbd : ∀ w, |f w| ≤ 2 * L := fun w => (steinSol_abs_le h hb hd hdiff w).trans (by linarith) have hf'bd : ∀ w, |f' w| ≤ 2 * L := fun w => steinSol_deriv_abs_le h hb hd hdiff w -- Measurability of the random variables. have hWmeas : Measurable W := by simp only [hW]; exact measurable_sum _ (fun i _ => hmeas i) have hTmeas : ∀ i, Measurable (T i) := by intro i; simp only [hT]; exact measurable_sum _ (fun j _ => hmeas j) have hSmeas : ∀ i, Measurable (S i) := by intro i; rw [hS]; exact measurable_sum _ (fun j _ => hmeas j) have hYmeas : Measurable Y := by rw [hY]; exact measurable_sum _ (fun i _ => (hmeas i).mul (hTmeas i)) -- Boundedness of the sums (by `card · B`). have hWbd : ∀ ω, |W ω| ≤ (Fintype.card ι : ℝ) * B := by intro ω; simp only [hW, depSum] calc |∑ i, X i ω| ≤ ∑ _i : ι, B := by refine (Finset.abs_sum_le_sum_abs _ _).trans ?_ exact Finset.sum_le_sum (fun i _ => hbound i ω) _ = (Fintype.card ι : ℝ) * B := by rw [Finset.sum_const]; simp [mul_comm] have hTbd : ∀ i ω, |T i ω| ≤ (Fintype.card ι : ℝ) * B := by intro i ω; simp only [hT, nbhdSum] calc |∑ j ∈ N i, X j ω| ≤ ∑ _j ∈ N i, B := by refine (Finset.abs_sum_le_sum_abs _ _).trans ?_ exact Finset.sum_le_sum (fun j _ => hbound j ω) _ = ((N i).card : ℝ) * B := by rw [Finset.sum_const]; simp [mul_comm] _ ≤ (Fintype.card ι : ℝ) * B := by apply mul_le_mul_of_nonneg_right _ hB exact_mod_cast Finset.card_le_univ (N i) have hSbd : ∀ i ω, |S i ω| ≤ (Fintype.card ι : ℝ) * B := by intro i ω; rw [hS] calc |∑ j ∈ univ \ N i, X j ω| ≤ ∑ _j ∈ univ \ N i, B := by refine (Finset.abs_sum_le_sum_abs _ _).trans ?_ exact Finset.sum_le_sum (fun j _ => hbound j ω) _ = ((univ \ N i).card : ℝ) * B := by rw [Finset.sum_const]; simp [mul_comm] _ ≤ (Fintype.card ι : ℝ) * B := by apply mul_le_mul_of_nonneg_right _ hB exact_mod_cast Finset.card_le_univ (univ \ N i) -- A helper: a bounded measurable real function is integrable on the probability measure. have hInt_of_bd : ∀ (g : Ω → ℝ) (_ : Measurable g) (c : ℝ) (_ : ∀ ω, |g ω| ≤ c), Integrable g μ := by intro g hg c hgc have hmemlp : MemLp g 1 μ := MemLp.of_bound hg.aestronglyMeasurable c (Filter.Eventually.of_forall (fun ω => by rw [Real.norm_eq_abs]; exact hgc ω)) exact hmemlp.integrable le_rfl -- Integrability facts used throughout. have hXint : ∀ i, Integrable (X i) μ := fun i => hInt_of_bd _ (hmeas i) B (fun ω => hbound i ω) have hfWmeas : Measurable (fun ω => f (W ω)) := hfcont.measurable.comp hWmeas have hf'Wmeas : Measurable (fun ω => f' (W ω)) := hf'cont.measurable.comp hWmeas have hf'Wint : Integrable (fun ω => f' (W ω)) μ := hInt_of_bd _ hf'Wmeas (2 * L) (fun ω => hf'bd (W ω)) have hWfWint : Integrable (fun ω => W ω * f (W ω)) μ := hInt_of_bd _ (hWmeas.mul hfWmeas) ((Fintype.card ι : ℝ) * B * (2 * L)) (fun ω => by rw [abs_mul]; exact mul_le_mul (hWbd ω) (hfbd (W ω)) (abs_nonneg _) (by positivity)) have hhWint : Integrable (fun ω => h (W ω)) μ := hInt_of_bd _ (hh.measurable.comp hWmeas) C (fun ω => hb (W ω)) -- **Step 1.** Stein equation, integrated. have hstein_pt : ∀ ω, f' (W ω) - W ω * f (W ω) = h (W ω) - gExpect h := by intro ω; rw [hf', hf]; exact steinSol_stein_eq h hh hb (W ω) have hStep1 : (∫ ω, h (W ω) ∂μ) - gExpect h = (∫ ω, f' (W ω) ∂μ) - ∫ ω, W ω * f (W ω) ∂μ := by have hpt : (fun ω => h (W ω) - gExpect h) = (fun ω => f' (W ω) - W ω * f (W ω)) := by funext ω; rw [hstein_pt ω] have hlhs : (∫ ω, (h (W ω) - gExpect h) ∂μ) = (∫ ω, h (W ω) ∂μ) - gExpect h := by rw [integral_sub hhWint (integrable_const _), integral_const] simp rw [← hlhs, hpt, integral_sub hf'Wint hWfWint] -- **Step 2.** `W = T i + S i` (split `univ = N i ⊔ (univ \ N i)`). have hWsplit : ∀ i ω, W ω = T i ω + S i ω := by intro i ω simp only [hW, depSum, hT, nbhdSum, hS] rw [← Finset.sum_union (Finset.disjoint_sdiff)] rw [Finset.union_sdiff_of_subset (Finset.subset_univ (N i))] -- Measurability / boundedness / integrability of `f ∘ S i` and the products. have hfSmeas : ∀ i, Measurable (fun ω => f (S i ω)) := fun i => hfcont.measurable.comp (hSmeas i) have hfSint : ∀ i, Integrable (fun ω => f (S i ω)) μ := fun i => hInt_of_bd _ (hfSmeas i) (2 * L) (fun ω => hfbd (S i ω)) have hcardB_nonneg : (0:ℝ) ≤ (Fintype.card ι : ℝ) * B := by positivity have hXfWint : ∀ i, Integrable (fun ω => X i ω * f (W ω)) μ := fun i => hInt_of_bd _ ((hmeas i).mul hfWmeas) (B * (2 * L)) (fun ω => by rw [abs_mul]; exact mul_le_mul (hbound i ω) (hfbd (W ω)) (abs_nonneg _) hB) have hXfSint : ∀ i, Integrable (fun ω => X i ω * f (S i ω)) μ := fun i => hInt_of_bd _ ((hmeas i).mul (hfSmeas i)) (B * (2 * L)) (fun ω => by rw [abs_mul]; exact mul_le_mul (hbound i ω) (hfbd (S i ω)) (abs_nonneg _) hB) -- **Step 3.** Independence kills `∫ Xᵢ·f(Sᵢ) = 0`. have hXfS_zero : ∀ i, ∫ ω, X i ω * f (S i ω) ∂μ = 0 := by intro i have hindep_comp : IndepFun (X i) (fun ω => f (S i ω)) μ := (hindep i).comp (φ := id) (ψ := f) measurable_id hfcont.measurable rw [hindep_comp.integral_fun_mul_eq_mul_integral (hmeas i).aestronglyMeasurable (hfSmeas i).aestronglyMeasurable] rw [hmean i, zero_mul] -- **Step 4 (a).** `∫ W·f(W) = ∑ᵢ ∫ Xᵢ·f(W)`. have hIWf_sum : (∫ ω, W ω * f (W ω) ∂μ) = ∑ i, ∫ ω, X i ω * f (W ω) ∂μ := by have hpt : (fun ω => W ω * f (W ω)) = (fun ω => ∑ i, X i ω * f (W ω)) := by funext ω; rw [← Finset.sum_mul] simp only [hW, depSum] rw [hpt, integral_finset_sum _ (fun i _ => hXfWint i)] -- Each `∫ Xᵢ·f(W) = ∫ Xᵢ·(f(W) − f(Sᵢ))`. have hXfW_sub : ∀ i, (∫ ω, X i ω * f (W ω) ∂μ) = ∫ ω, X i ω * (f (W ω) - f (S i ω)) ∂μ := by intro i have hsplit : (fun ω => X i ω * (f (W ω) - f (S i ω))) = (fun ω => X i ω * f (W ω) - X i ω * f (S i ω)) := by funext ω; ring rw [hsplit, integral_sub (hXfWint i) (hXfSint i), hXfS_zero i, sub_zero] -- The Taylor remainder `R i ω = Tᵢ·f'(W) − (f(W) − f(Sᵢ))`. set R : ι → Ω → ℝ := fun i ω => T i ω * f' (W ω) - (f (W ω) - f (S i ω)) with hR -- Taylor bound: `|R i ω| ≤ L·(Tᵢ ω)²`. have hRbound : ∀ i ω, |R i ω| ≤ L * (T i ω) ^ 2 := by intro i ω have htaylor := steinSol_taylor_right h hb hd hdiff (S i ω) (T i ω) have hWeq : S i ω + T i ω = W ω := by rw [hWsplit i ω]; ring rw [hWeq] at htaylor change |T i ω * f' (W ω) - (f (W ω) - f (S i ω))| ≤ L * (T i ω) ^ 2 have heq : T i ω * f' (W ω) - (f (W ω) - f (S i ω)) = -(f (W ω) - f (S i ω) - T i ω * deriv (steinSol h) (W ω)) := by rw [hf']; ring rw [heq, abs_neg]; exact htaylor -- Measurability / integrability of `R i`, `Xᵢ·Tᵢ·f'(W)`, `Xᵢ·Rᵢ`. have hf'Wcont_meas : Measurable (fun ω => f' (W ω)) := hf'Wmeas have hRmeas : ∀ i, Measurable (R i) := by intro i; rw [hR] exact ((hTmeas i).mul hf'Wmeas).sub (hfWmeas.sub (hfSmeas i)) have hXTf'int : ∀ i, Integrable (fun ω => X i ω * T i ω * f' (W ω)) μ := by intro i refine hInt_of_bd _ (((hmeas i).mul (hTmeas i)).mul hf'Wmeas) (B * ((Fintype.card ι : ℝ) * B) * (2 * L)) (fun ω => ?_) rw [abs_mul, abs_mul] refine mul_le_mul (mul_le_mul (hbound i ω) (hTbd i ω) (abs_nonneg _) hB) (hf'bd (W ω)) (abs_nonneg _) (by positivity) have hXRint : ∀ i, Integrable (fun ω => X i ω * R i ω) μ := by intro i refine hInt_of_bd _ ((hmeas i).mul (hRmeas i)) (B * (L * ((Fintype.card ι : ℝ) * B) ^ 2)) (fun ω => ?_) rw [abs_mul] refine mul_le_mul (hbound i ω) ((hRbound i ω).trans ?_) (abs_nonneg _) hB apply mul_le_mul_of_nonneg_left _ hL calc (T i ω) ^ 2 = |T i ω| ^ 2 := (sq_abs _).symm _ ≤ ((Fintype.card ι : ℝ) * B) ^ 2 := by apply pow_le_pow_left₀ (abs_nonneg _) (hTbd i ω) -- Decomposition of each summand. have hXfW_decomp : ∀ i, (∫ ω, X i ω * f (W ω) ∂μ) = (∫ ω, X i ω * T i ω * f' (W ω) ∂μ) - ∫ ω, X i ω * R i ω ∂μ := by intro i rw [hXfW_sub i] have hpt : (fun ω => X i ω * (f (W ω) - f (S i ω))) = (fun ω => X i ω * T i ω * f' (W ω) - X i ω * R i ω) := by funext ω; rw [hR]; ring rw [hpt, integral_sub (hXTf'int i) (hXRint i)] -- **Step 4 (c).** `∑ᵢ ∫ Xᵢ·Tᵢ·f'(W) = ∫ f'(W)·Y`. have hf'WYint : Integrable (fun ω => f' (W ω) * Y ω) μ := by refine hInt_of_bd _ (hf'Wmeas.mul hYmeas) (2 * L * ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) * B * B))) (fun ω => ?_) rw [abs_mul] refine mul_le_mul (hf'bd (W ω)) ?_ (abs_nonneg _) (by positivity) rw [hY] calc |∑ i, X i ω * T i ω| ≤ ∑ _i : ι, (Fintype.card ι : ℝ) * B * B := by refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum (fun i _ => ?_)) rw [abs_mul, mul_comm ((Fintype.card ι : ℝ) * B) B] exact mul_le_mul (hbound i ω) (hTbd i ω) (abs_nonneg _) hB _ = (Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) * B * B) := by rw [Finset.sum_const]; simp [mul_comm] have hsum_XTf' : (∑ i, ∫ ω, X i ω * T i ω * f' (W ω) ∂μ) = ∫ ω, f' (W ω) * Y ω ∂μ := by rw [← integral_finset_sum _ (fun i _ => hXTf'int i)] congr 1; funext ω rw [hY, Finset.mul_sum] congr 1; funext i; ring -- **Master identity.** `(∫h(W)) − gExpect h = ∫ f'(W)·(1 − Y) + ∑ᵢ ∫ Xᵢ·Rᵢ`. have hYint : Integrable Y μ := by refine hInt_of_bd _ hYmeas ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) * B * B)) (fun ω => ?_) rw [hY] calc |∑ i, X i ω * T i ω| ≤ ∑ _i : ι, (Fintype.card ι : ℝ) * B * B := by refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum (fun i _ => ?_)) rw [abs_mul, mul_comm ((Fintype.card ι : ℝ) * B) B] exact mul_le_mul (hbound i ω) (hTbd i ω) (abs_nonneg _) hB _ = (Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) * B * B) := by rw [Finset.sum_const]; simp [mul_comm] have hmaster : (∫ ω, h (W ω) ∂μ) - gExpect h = (∫ ω, f' (W ω) * (1 - Y ω) ∂μ) + ∑ i, ∫ ω, X i ω * R i ω ∂μ := by rw [hStep1, hIWf_sum] have hsumdecomp : (∑ i, ∫ ω, X i ω * f (W ω) ∂μ) = (∑ i, ∫ ω, X i ω * T i ω * f' (W ω) ∂μ) - ∑ i, ∫ ω, X i ω * R i ω ∂μ := by rw [← Finset.sum_sub_distrib] exact Finset.sum_congr rfl (fun i _ => hXfW_decomp i) rw [hsumdecomp, hsum_XTf'] have h1mY : (∫ ω, f' (W ω) * (1 - Y ω) ∂μ) = (∫ ω, f' (W ω) ∂μ) - ∫ ω, f' (W ω) * Y ω ∂μ := by have hpt : (fun ω => f' (W ω) * (1 - Y ω)) = (fun ω => f' (W ω) - f' (W ω) * Y ω) := by funext ω; ring rw [hpt, integral_sub hf'Wint hf'WYint] rw [h1mY]; ring -- **Step 5 (a).** `∫ Y = ∫ W² = 1`. have hXSint : ∀ i, Integrable (fun ω => X i ω * S i ω) μ := fun i => hInt_of_bd _ ((hmeas i).mul (hSmeas i)) (B * ((Fintype.card ι : ℝ) * B)) (fun ω => by rw [abs_mul]; exact mul_le_mul (hbound i ω) (hSbd i ω) (abs_nonneg _) hB) have hXTint : ∀ i, Integrable (fun ω => X i ω * T i ω) μ := fun i => hInt_of_bd _ ((hmeas i).mul (hTmeas i)) (B * ((Fintype.card ι : ℝ) * B)) (fun ω => by rw [abs_mul]; exact mul_le_mul (hbound i ω) (hTbd i ω) (abs_nonneg _) hB) have hXWint : ∀ i, Integrable (fun ω => X i ω * W ω) μ := fun i => hInt_of_bd _ ((hmeas i).mul hWmeas) (B * ((Fintype.card ι : ℝ) * B)) (fun ω => by rw [abs_mul]; exact mul_le_mul (hbound i ω) (hWbd ω) (abs_nonneg _) hB) have hXS_zero : ∀ i, ∫ ω, X i ω * S i ω ∂μ = 0 := by intro i have hindep_i : IndepFun (X i) (S i) μ := hindep i rw [hindep_i.integral_fun_mul_eq_mul_integral (hmeas i).aestronglyMeasurable (hSmeas i).aestronglyMeasurable, hmean i, zero_mul] have hintY : (∫ ω, Y ω ∂μ) = 1 := by have hYeq : (∫ ω, Y ω ∂μ) = ∑ i, ∫ ω, X i ω * T i ω ∂μ := by rw [hY, integral_finset_sum _ (fun i _ => hXTint i)] have hW2eq : (∫ ω, W ω ^ 2 ∂μ) = ∑ i, ∫ ω, X i ω * W ω ∂μ := by have hpt : (fun ω => W ω ^ 2) = (fun ω => ∑ i, X i ω * W ω) := by funext ω; rw [← Finset.sum_mul, sq] simp only [hW, depSum] rw [hpt, integral_finset_sum _ (fun i _ => hXWint i)] have hXW_eq : ∀ i, (∫ ω, X i ω * W ω ∂μ) = ∫ ω, X i ω * T i ω ∂μ := by intro i -- … truncated; follow the source link for the rest …

theorem stein_cdf_clt_of_depGraph {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)] (μ : ∀ n, Measure (Ω n)) [∀ n, IsProbabilityMeasure (μ n)] {ι : ℕ → Type*} [∀ n, Fintype (ι n)] (X : ∀ n, ι n → Ω n → ℝ) (D : ∀ n, DepGraph (X n) (μ n)) (m : ℕ) (hdeg : ∀ n i, ((D n).nbhd i).card ≤ m) (B : ℕ → ℝ) (hB : ∀ n, 0 ≤ B n) (hbound : ∀ n i ω, |X n i ω| ≤ B n) (hB0 : Tendsto B atTop (𝓝 0)) (hNB3 : Tendsto (fun n => (card (ι n) : ℝ) * (B n) ^ 3) atTop (𝓝 0)) (hmean : ∀ n i, ∫ ω, X n i ω ∂(μ n) = 0) (hvar : ∀ n, ∫ ω, (depSum (X n) ω) ^ 2 ∂(μ n) = 1) (s : ℝ) : Tendsto (fun n => ((μ n).map (depSum (X n))).real (Iic s)) atTop (𝓝 ((gaussianReal 0 1).real (Iic s))) := by classical -- `nbhdSum (X n) (Nₙ) i ω = ∑_{k∈Nₙ i} X n k ω` definitionally. -- Leave-out independence and the self-membership hypothesis come from the dependency graph. have hindep : ∀ n i, IndepFun (X n i) (fun ω => ∑ j ∈ univ \ (D n).nbhd i, X n j ω) (μ n) := fun n i => (D n).indepFun_leaveOut i -- Error term 1: variance of the localized double sum, squeezed via `var_nbhd_prod_le`. have herr1 : Tendsto (fun n => variance (fun ω => ∑ i, X n i ω * nbhdSum (X n) (fun i => (D n).nbhd i) i ω) (μ n)) atTop (𝓝 0) := by -- Upper bound `2 m⁵ · N · B⁴ → 0`. have hub : Tendsto (fun n => 2 * (m : ℝ) ^ 5 * (card (ι n) : ℝ) * (B n) ^ 4) atTop (𝓝 0) := by have hfac : (fun n => 2 * (m : ℝ) ^ 5 * (card (ι n) : ℝ) * (B n) ^ 4) = (fun n => (2 * (m : ℝ) ^ 5) * (((card (ι n) : ℝ) * (B n) ^ 3) * B n)) := by funext n; ring rw [hfac] have h := (hNB3.mul hB0) simpa using (h.const_mul (2 * (m : ℝ) ^ 5)).congr (fun n => by ring) refine squeeze_zero (fun n => variance_nonneg _ _) (fun n => ?_) hub have := (D n).var_nbhd_prod_le (hB n) (hbound n) (hdeg n) simpa only [nbhdSum] using this -- Error term 2: `∑ᵢ E[|Xᵢ|·Tᵢ²]`, squeezed via `sum_E_nbhd_sq_le`. have herr2 : Tendsto (fun n => ∑ i, ∫ ω, |X n i ω| * (nbhdSum (X n) (fun i => (D n).nbhd i) i ω) ^ 2 ∂(μ n)) atTop (𝓝 0) := by have hub : Tendsto (fun n => (m : ℝ) ^ 2 * (card (ι n) : ℝ) * (B n) ^ 3) atTop (𝓝 0) := by have hfac : (fun n => (m : ℝ) ^ 2 * (card (ι n) : ℝ) * (B n) ^ 3) = (fun n => (m : ℝ) ^ 2 * ((card (ι n) : ℝ) * (B n) ^ 3)) := by funext n; ring rw [hfac] simpa using hNB3.const_mul ((m : ℝ) ^ 2) have hnonneg : ∀ n, 0 ≤ ∑ i, ∫ ω, |X n i ω| * (nbhdSum (X n) (fun i => (D n).nbhd i) i ω) ^ 2 ∂(μ n) := by intro n apply sum_nonneg intro i _ apply integral_nonneg intro ω positivity refine squeeze_zero hnonneg (fun n => ?_) hub have := DepGraph.sum_E_nbhd_sq_le (X := X n) (μ := μ n) (fun i => (D n).nbhd i) (fun i => (D n).meas i) (hB n) (hbound n) (hdeg n) simpa only [nbhdSum] using this exact stein_cdf_clt μ X (fun n => (D n).nbhd) (fun n i => (D n).meas i) B hB hbound hmean hindep hvar herr1 herr2 s

theorem steinSol_abs_le (h : ℝ → ℝ) {C L : ℝ} (hb : ∀ x, |h x| ≤ C) (hd : ∀ x, |deriv h x| ≤ L) (hdiff : Differentiable ℝ h) (w : ℝ) : |steinSol h w| ≤ L := by -- Notation for the four building blocks of the weighted identity. set P : ℝ := ∫ x in Ioi w, phi x with hP set Q : ℝ := ∫ x in Iic w, phi x with hQ set A : ℝ := ∫ x in Iic w, (h x - h w) * phi x with hA set B : ℝ := ∫ x in Ioi w, (h x - h w) * phi x with hB set E : ℝ := exp (w ^ 2 / 2) with hE have hPpos : 0 ≤ P := by rw [hP]; exact setIntegral_nonneg measurableSet_Ioi (fun x _ => (phi_pos x).le) have hQpos : 0 ≤ Q := by rw [hQ]; exact setIntegral_nonneg measurableSet_Iic (fun x _ => (phi_pos x).le) have hEpos : 0 < E := Real.exp_pos _ have hKpos : 0 < sqrt (2 * π) := Real.sqrt_pos.mpr (by positivity) -- Bounds on |A| and |B| coming from the Lipschitz estimates. have hAbound : |A| ≤ L * (w * Q + phi w) := by rw [hA, hQ]; exact abs_integral_diff_phi_Iic_le hdiff.continuous hb hd hdiff w have hBbound : |B| ≤ L * (phi w - w * P) := by rw [hB, hP]; exact abs_integral_diff_phi_Ioi_le hdiff.continuous hb hd hdiff w -- The weighted identity, with the cancellation pre-computed. have hid : sqrt (2 * π) * steinSol h w = E * (P * A - Q * B) := by rw [hE, hP, hQ, hA, hB]; exact steinSol_weighted_identity hdiff.continuous hb w -- Bound `√(2π)·|steinSol|`. have hmain : sqrt (2 * π) * |steinSol h w| ≤ sqrt (2 * π) * L := by calc sqrt (2 * π) * |steinSol h w| = |sqrt (2 * π) * steinSol h w| := by rw [abs_mul, abs_of_nonneg hKpos.le] _ = |E * (P * A - Q * B)| := by rw [hid] _ = E * |P * A - Q * B| := by rw [abs_mul, abs_of_nonneg hEpos.le] _ ≤ E * (P * |A| + Q * |B|) := by gcongr calc |P * A - Q * B| ≤ |P * A| + |Q * B| := abs_sub _ _ _ = P * |A| + Q * |B| := by rw [abs_mul, abs_mul, abs_of_nonneg hPpos, abs_of_nonneg hQpos] _ ≤ E * (P * (L * (w * Q + phi w)) + Q * (L * (phi w - w * P))) := by gcongr _ = L * (E * (P * (w * Q + phi w) + Q * (phi w - w * P))) := by ring _ = L * sqrt (2 * π) := by rw [weighted_moment_cancel w] _ = sqrt (2 * π) * L := by ring -- Cancel the positive factor `√(2π)`. exact le_of_mul_le_mul_left hmain hKpos

theorem stein_cdf_clt {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)] (μ : ∀ n, Measure (Ω n)) [∀ n, IsProbabilityMeasure (μ n)] {ι : ℕ → Type*} [∀ n, Fintype (ι n)] [∀ n, DecidableEq (ι n)] (X : ∀ n, ι n → Ω n → ℝ) (N : ∀ n, ι n → Finset (ι n)) (hmeas : ∀ n i, Measurable (X n i)) (B : ℕ → ℝ) (hB : ∀ n, 0 ≤ B n) (hbound : ∀ n i ω, |X n i ω| ≤ B n) (hmean : ∀ n i, ∫ ω, X n i ω ∂(μ n) = 0) (hindep : ∀ n i, IndepFun (X n i) (fun ω => ∑ j ∈ univ \ N n i, X n j ω) (μ n)) (hvar : ∀ n, ∫ ω, (depSum (X n) ω) ^ 2 ∂(μ n) = 1) (herr1 : Tendsto (fun n => variance (fun ω => ∑ i, X n i ω * nbhdSum (X n) (N n) i ω) (μ n)) atTop (𝓝 0)) (herr2 : Tendsto (fun n => ∑ i, ∫ ω, |X n i ω| * (nbhdSum (X n) (N n) i ω) ^ 2 ∂(μ n)) atTop (𝓝 0)) (s : ℝ) : Tendsto (fun n => ((μ n).map (depSum (X n))).real (Iic s)) atTop (𝓝 ((gaussianReal 0 1).real (Iic s))) := by classical -- `W n` is the standardized sum; it is measurable (finite sum of measurable maps). have hWmeas : ∀ n, Measurable (depSum (X n)) := fun n => by unfold depSum; exact measurable_sum _ (fun i _ => hmeas n i) -- The law of `W n` is a probability measure. haveI : ∀ n, IsProbabilityMeasure ((μ n).map (depSum (X n))) := fun n => Measure.isProbabilityMeasure_map (hWmeas n).aemeasurable -- Package the laws. set lawn : ℕ → ProbabilityMeasure ℝ := fun n => ⟨(μ n).map (depSum (X n)), inferInstance⟩ with hlawn -- Reduce to characteristic-function convergence via Theorem 1. have hcoe : ∀ n, (lawn n : Measure ℝ) = (μ n).map (depSum (X n)) := fun n => rfl let ν₀ : ProbabilityMeasure ℝ := ⟨gaussianReal 0 1, inferInstance⟩ letI : NullSingletonClass (ν₀ : Measure ℝ) := nullSingletonClass_gaussianReal one_ne_zero refine cdf_tendsto_of_charFun_tendsto lawn ν₀ ?_ s intro t -- Test functions `cos(t·)` and `sin(t·)`: both bounded by `1` with derivative bounded by `|t|`. have hcos_cont : Continuous (fun x => cos (t * x)) := by fun_prop have hcos_diff : Differentiable ℝ (fun x => cos (t * x)) := by fun_prop have hcos_b : ∀ x, |cos (t * x)| ≤ 1 := fun x => Real.abs_cos_le_one _ have hcos_d : ∀ x, |deriv (fun x => cos (t * x)) x| ≤ |t| := by intro x have hderiv : deriv (fun x => cos (t * x)) x = -(t * sin (t * x)) := by have h := (Real.hasDerivAt_cos (t * x)).comp x ((hasDerivAt_id x).const_mul t) simpa [mul_comm, Function.comp_def] using h.deriv rw [hderiv, abs_neg, abs_mul] calc |t| * |sin (t * x)| ≤ |t| * 1 := mul_le_mul_of_nonneg_left (Real.abs_sin_le_one _) (abs_nonneg _) _ = |t| := mul_one _ have hsin_cont : Continuous (fun x => sin (t * x)) := by fun_prop have hsin_diff : Differentiable ℝ (fun x => sin (t * x)) := by fun_prop have hsin_b : ∀ x, |sin (t * x)| ≤ 1 := fun x => Real.abs_sin_le_one _ have hsin_d : ∀ x, |deriv (fun x => sin (t * x)) x| ≤ |t| := by intro x have hderiv : deriv (fun x => sin (t * x)) x = t * cos (t * x) := by have h := (Real.hasDerivAt_sin (t * x)).comp x ((hasDerivAt_id x).const_mul t) simpa [mul_comm, Function.comp_def] using h.deriv rw [hderiv, abs_mul] calc |t| * |cos (t * x)| ≤ |t| * 1 := mul_le_mul_of_nonneg_left (Real.abs_cos_le_one _) (abs_nonneg _) _ = |t| := mul_one _ -- Stein convergence of the cos- and sin-expectations to the Gaussian expectations. have hcos_tendsto : Tendsto (fun n => ∫ ω, cos (t * depSum (X n) ω) ∂(μ n)) atTop (𝓝 (gExpect (fun x => cos (t * x)))) := stein_expect_tendsto μ X N hmeas B hB hbound hmean hindep hvar herr1 herr2 (fun x => cos (t * x)) hcos_b hcos_d hcos_diff have hsin_tendsto : Tendsto (fun n => ∫ ω, sin (t * depSum (X n) ω) ∂(μ n)) atTop (𝓝 (gExpect (fun x => sin (t * x)))) := stein_expect_tendsto μ X N hmeas B hB hbound hmean hindep hvar herr1 herr2 (fun x => sin (t * x)) hsin_b hsin_d hsin_diff -- Decompose `charFun` of the limit Gaussian into the cos/sin Gaussian expectations. have hgauss : charFun (gaussianReal 0 1) t = (↑(gExpect (fun x => cos (t * x))) : ℂ) + (↑(gExpect (fun x => sin (t * x))) : ℂ) * I := by have hmap : (gaussianReal 0 1).map id = gaussianReal 0 1 := Measure.map_id have := charFun_map_eq_cos_sin (gaussianReal 0 1) id measurable_id t rw [hmap] at this simpa [gExpect, comp] using this -- Decompose `charFun` of each law `lawn n` into the cos/sin sample expectations. have hlaw : ∀ n, charFun (lawn n : Measure ℝ) t = (↑(∫ ω, cos (t * depSum (X n) ω) ∂(μ n)) : ℂ) + (↑(∫ ω, sin (t * depSum (X n) ω) ∂(μ n)) : ℂ) * I := by intro n rw [hcoe n] exact charFun_map_eq_cos_sin (μ n) (depSum (X n)) (hWmeas n) t -- Combine: real and imaginary parts converge, hence the complex char-functions converge. have hν₀ : (ν₀ : Measure ℝ) = gaussianReal 0 1 := rfl rw [hν₀, hgauss] simp_rw [hlaw] refine Tendsto.add ?_ (Tendsto.mul_const I ?_) · exact (Complex.continuous_ofReal.tendsto _).comp hcos_tendsto · exact (Complex.continuous_ofReal.tendsto _).comp hsin_tendsto

theorem bounded_degree_dependency_clt {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)] (μ : ∀ n, Measure (Ω n)) [∀ n, IsProbabilityMeasure (μ n)] {ι : ℕ → Type*} [∀ n, Fintype (ι n)] (X : ∀ n, ι n → Ω n → ℝ) (Dep : ∀ n, DepGraph (X n) (μ n)) (Dmax : ℕ) (hdeg : ∀ n i, ((Dep n).nbhd i).card ≤ Dmax) (M : ℝ) (hM : 0 ≤ M) (hbound : ∀ n i ω, |X n i ω| ≤ M) (hmean : ∀ n i, ∫ ω, X n i ω ∂(μ n) = 0) (v : ℕ → ℝ) (hv : ∀ n, ∫ ω, (depSum (X n) ω) ^ 2 ∂(μ n) = v n) (c : ℝ) (hc : 0 < c) (hvc : ∀ᶠ n in atTop, c * (card (ι n) : ℝ) ≤ v n) (hcard : Tendsto (fun n => card (ι n)) atTop atTop) (s : ℝ) : Tendsto (fun n => ((μ n).map (fun ω => depSum (X n) ω / sqrt (v n))).real (Iic s)) atTop (𝓝 ((gaussianReal 0 1).real (Iic s))) := by classical rcases eventually_atTop.1 hvc with ⟨Nv, hNv⟩ rcases eventually_atTop.1 (hcard.eventually_ge_atTop 1) with ⟨Nc, hNc⟩ let N := max Nv Nc have hvc_tail : ∀ n, c * (card (ι (n + N)) : ℝ) ≤ v (n + N) := by intro n apply hNv omega have hcard_pos_tail : ∀ n, 0 < card (ι (n + N)) := by intro n have hge : 1 ≤ card (ι (n + N)) := hNc (n + N) (by omega) exact Nat.lt_of_lt_of_le Nat.zero_lt_one hge have hcard_tail : Tendsto (fun n => card (ι (n + N))) atTop atTop := hcard.comp (tendsto_add_atTop_nat N) have htail := bounded_degree_dependency_clt_of_variance_floor_all (μ := fun n => μ (n + N)) (X := fun n => X (n + N)) (Dep := fun n => Dep (n + N)) Dmax (fun n i => hdeg (n + N) i) M hM (fun n i ω => hbound (n + N) i ω) (fun n i => hmean (n + N) i) (fun n => v (n + N)) (fun n => hv (n + N)) c hc hvc_tail hcard_pos_tail hcard_tail s exact (tendsto_add_atTop_iff_nat N).1 htail