Experimentation.Design­Based

theorem tendstoInProb_of_var (D : ∀ m, FiniteDesign (Ω m)) (X : ∀ m, Ω m → ℝ) (hvar : Tendsto (fun m => (D m).Var (X m)) atTop (𝓝 0)) : TendstoInProb D X (fun m => (D m).E (X m)) := by intro ε hε have hε2 : (0 : ℝ) < ε ^ 2 := pow_pos hε 2 have hupper : Tendsto (fun m => (D m).Var (X m) / ε ^ 2) atTop (𝓝 0) := by simpa using hvar.div_const (ε ^ 2) refine squeeze_zero (fun m => ?_) (fun m => ?_) hupper · exact (D m).Pr_nonneg _ · exact (D m).chebyshev (X m) hε

theorem tendstoInProb_div_one (D : ∀ m, FiniteDesign (Ω m)) (X Y : ∀ m, Ω m → ℝ) (a : ℕ → ℝ) (M : ℝ) (ha : ∀ m, |a m| ≤ M) (hX : TendstoInProb D X a) (hY : TendstoInProb D Y (fun _ => 1)) : TendstoInProb D (fun m z => X m z / Y m z) a := by intro ε hε -- `M' := M + 1` is a strictly positive bound on `|a m|`, avoiding division by zero. set M' : ℝ := M + 1 with hM'def have hMnn : 0 ≤ M := le_trans (abs_nonneg _) (ha 0) have hM' : 0 < M' := by rw [hM'def]; linarith have haM' : ∀ m, |a m| ≤ M' := fun m => le_trans (ha m) (by rw [hM'def]; linarith) have hε4 : (0 : ℝ) < ε / 4 := by linarith have hε4M' : (0 : ℝ) < ε / (4 * M') := by positivity have hhalf : (0 : ℝ) < 1 / 2 := by norm_num -- Pointwise inclusion: the ratio-far event is contained in the union of three deviation events. have hbound : ∀ m, (D m).Pr (fun z => ε ≤ |X m z / Y m z - a m|) ≤ (D m).Pr (fun z => (1 : ℝ) / 2 ≤ |Y m z - 1|) + ((D m).Pr (fun z => ε / 4 ≤ |X m z - a m|) + (D m).Pr (fun z => ε / (4 * M') ≤ |Y m z - 1|)) := by intro m have hmono : (D m).Pr (fun z => ε ≤ |X m z / Y m z - a m|) ≤ (D m).Pr (fun z => ((1 : ℝ) / 2 ≤ |Y m z - 1|) ∨ ((ε / 4 ≤ |X m z - a m|) ∨ (ε / (4 * M') ≤ |Y m z - 1|))) := by apply (D m).Pr_mono intro z hz -- Split on whether the denominator is close to one. by_cases hYclose : (1 : ℝ) / 2 ≤ |Y m z - 1| · exact inl hYclose · push_neg at hYclose refine inr ?_ -- On `|Y - 1| < 1/2` we have `|Y| ≥ 1/2 > 0`. have hYlb : (1 : ℝ) / 2 ≤ |Y m z| := by have htri : |Y m z - 1| ≥ |1| - |Y m z| := by have := abs_sub_abs_le_abs_sub (1 : ℝ) (Y m z) rw [abs_sub_comm] at this simpa [abs_sub_comm] using this have h1 : |(1 : ℝ)| = 1 := by norm_num rw [h1] at htri linarith have hYpos : (0 : ℝ) < |Y m z| := lt_of_lt_of_le (by norm_num) hYlb have hYne : Y m z ≠ 0 := by intro h; rw [h] at hYpos; simp at hYpos -- `|X/Y - a| = |X - a·Y| / |Y| ≤ 2·|X - a·Y|`. have hratio : |X m z / Y m z - a m| = |X m z - a m * Y m z| / |Y m z| := by rw [← abs_div] congr 1 field_simp have hle2 : |X m z / Y m z - a m| ≤ 2 * |X m z - a m * Y m z| := by rw [hratio] rw [div_le_iff₀ hYpos] calc |X m z - a m * Y m z| = |X m z - a m * Y m z| * 1 := by ring _ ≤ |X m z - a m * Y m z| * (2 * |Y m z|) := by apply mul_le_mul_of_nonneg_left _ (abs_nonneg _) linarith _ = 2 * |X m z - a m * Y m z| * |Y m z| := by ring -- `|X - a·Y| ≤ |X - a| + |a|·|Y - 1|`. have hsplit : |X m z - a m * Y m z| ≤ |X m z - a m| + |a m| * |Y m z - 1| := by have heq : X m z - a m * Y m z = (X m z - a m) + a m * (1 - Y m z) := by ring calc |X m z - a m * Y m z| = |(X m z - a m) + a m * (1 - Y m z)| := by rw [heq] _ ≤ |X m z - a m| + |a m * (1 - Y m z)| := abs_add_le _ _ _ = |X m z - a m| + |a m| * |1 - Y m z| := by rw [abs_mul] _ = |X m z - a m| + |a m| * |Y m z - 1| := by rw [abs_sub_comm (1 : ℝ)] -- Combine: `ε ≤ |X/Y - a| ≤ 2|X-a| + 2M'|Y-1|`. have hcombine : ε ≤ 2 * |X m z - a m| + 2 * M' * |Y m z - 1| := by have haY : |a m| * |Y m z - 1| ≤ M' * |Y m z - 1| := mul_le_mul_of_nonneg_right (haM' m) (abs_nonneg _) have : ε ≤ 2 * (|X m z - a m| + |a m| * |Y m z - 1|) := le_trans hz (le_trans hle2 (by linarith [hsplit])) nlinarith [haY, abs_nonneg (Y m z - 1)] -- Hence one of the two half-bounds holds. by_contra hcon push_neg at hcon obtain ⟨h1, h2⟩ := hcon -- `2|X-a| < ε/2` and `2M'|Y-1| < ε/2`, contradicting `hcombine`. have hb1 : 2 * |X m z - a m| < ε / 2 := by linarith have hb2 : 2 * M' * |Y m z - 1| < ε / 2 := by have : |Y m z - 1| < ε / (4 * M') := h2 have h4M' : (0 : ℝ) < 4 * M' := by linarith rw [lt_div_iff₀ h4M'] at this nlinarith [this] linarith refine le_trans hmono ?_ refine le_trans ((D m).Pr_or_le _ _) ?_ have := (D m).Pr_or_le (fun z => ε / 4 ≤ |X m z - a m|) (fun z => ε / (4 * M') ≤ |Y m z - 1|) linarith [this] -- The upper bound tends to zero (three vanishing tails). have hupper : Tendsto (fun m => (D m).Pr (fun z => (1 : ℝ) / 2 ≤ |Y m z - 1|) + ((D m).Pr (fun z => ε / 4 ≤ |X m z - a m|) + (D m).Pr (fun z => ε / (4 * M') ≤ |Y m z - 1|))) atTop (𝓝 0) := by have t1 := hY (1 / 2) hhalf have t2 := hX (ε / 4) hε4 have t3 := hY (ε / (4 * M')) hε4M' have := t1.add (t2.add t3) simpa using this refine squeeze_zero (fun m => (D m).Pr_nonneg _) hbound hupper

theorem TendstoInProb.mul_boundedInProb {D : ∀ m, FiniteDesign (Ω m)} {U V : ∀ m, Ω m → ℝ} (hU : TendstoInProb D U (fun _ => 0)) (hV : BoundedInProb D V) : TendstoInProb D (fun m z => U m z * V m z) (fun _ => 0) := by intro ε hε simp only [sub_zero] apply tendsto_order.2 constructor · intro a ha filter_upwards [] with m exact lt_of_lt_of_le ha ((D m).Pr_nonneg _) · intro a ha have ha2 : (0 : ℝ) < a / 2 := by linarith obtain ⟨M, hM⟩ := hV (a / 2) ha2 set M' : ℝ := |M| + 1 with hM'def have hM' : 0 < M' := by rw [hM'def] positivity have hMle : M ≤ M' := by rw [hM'def] linarith [le_abs_self M] have hMbound : ∀ᶠ m in atTop, (D m).Pr (fun z => M' ≤ |V m z|) ≤ a / 2 := by filter_upwards [hM] with m hmm refine le_trans ?_ hmm apply (D m).Pr_mono intro z hz exact le_trans hMle hz have hbound : ∀ m, (D m).Pr (fun z => ε ≤ |U m z * V m z|) ≤ (D m).Pr (fun z => M' ≤ |V m z|) + (D m).Pr (fun z => ε / M' ≤ |U m z|) := by intro m refine le_trans ?_ (Pr_or_le (D m) _ _) apply (D m).Pr_mono intro z hz by_cases hVlarge : M' ≤ |V m z| · exact inl hVlarge · right push_neg at hVlarge rw [div_le_iff₀ hM'] rw [abs_mul] at hz have hUpos : 0 < |U m z| := by by_contra hUpos have hUzero : |U m z| = 0 := le_antisymm (le_of_not_gt hUpos) (abs_nonneg _) rw [hUzero, zero_mul] at hz linarith exact le_of_lt (lt_of_le_of_lt hz (mul_lt_mul_of_pos_left hVlarge hUpos)) have hU' : Tendsto (fun m => (D m).Pr (fun z => ε / M' ≤ |U m z|)) atTop (𝓝 0) := by have hεM' : (0 : ℝ) < ε / M' := by positivity simpa using hU (ε / M') hεM' have htail : ∀ᶠ m in atTop, (D m).Pr (fun z => ε / M' ≤ |U m z|) < a / 2 := (tendsto_order.mp hU').2 (a / 2) ha2 filter_upwards [htail, hMbound] with m hm hmb calc (D m).Pr (fun z => ε ≤ |U m z * V m z|) ≤ (D m).Pr (fun z => M' ≤ |V m z|) + (D m).Pr (fun z => ε / M' ≤ |U m z|) := hbound m _ < a := by linarith [hmb]

lemma Cov_expoInd_same (D : FiniteDesign Ω) (f : Ω → Θ → Δ) (θ : ι → Θ) (i j : ι) (d : Δ) : D.Cov (expoInd f θ i d) (expoInd f θ j d) = propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d := by unfold propPairSame rw [FiniteDesign.Cov_eq, E_expoInd, E_expoInd]

lemma Cov_expoInd_cross (D : FiniteDesign Ω) (f : Ω → Θ → Δ) (θ : ι → Θ) (i j : ι) (d d' : Δ) : D.Cov (expoInd f θ i d) (expoInd f θ j d') = propPairCross D f θ i j d d' - prop D f θ i d * prop D f θ j d' := by unfold propPairCross rw [FiniteDesign.Cov_eq, E_expoInd, E_expoInd]

lemma mse_eq_var_add_bias_sq (est : Ω → ℝ) (μ : ℝ) : D.mse est μ = D.Var est + (D.bias est μ) ^ 2 := by unfold mse bias rw [Var_eq] have h : (fun z => (est z - μ) ^ 2) = (fun z => (est z) ^ 2 + ((-(2 * μ)) * est z + μ ^ 2)) := by funext z; ring rw [h, E_add, E_add, E_const_mul, E_const]; ring

theorem sampleVariance_tendstoInProb (n : ℕ → ℕ) (hn2 : ∀ k, 2 ≤ n k) (hnle : ∀ k, n k ≤ card (U k)) (y : ∀ k, U k → ℝ) (v : ℝ) (hnTop : Tendsto n atTop atTop) (hvar : Tendsto (fun k => popVar (y k)) atTop (𝓝 v)) (hmax : Tendsto (fun k => popMaxSqDev (y k) / (n k : ℝ)) atTop (𝓝 0)) : FiniteDesign.TendstoInProb (fun k => completeRandomization (n k) (hnle k)) (fun k => sampleVariance (n k) (y k)) (fun k => popVar (y k)) := by classical letI hsampleNonempty : ∀ k, Nonempty {S : Finset (U k) // S.card = n k} := fun k => by obtain ⟨S, _hsub, hS⟩ := Finset.exists_subset_card_eq (s := univ) (by simpa using hnle k) exact ⟨⟨S, hS⟩⟩ have hn0 : ∀ k, 0 < n k := fun k => lt_of_lt_of_le (by norm_num) (hn2 k) have hz := centeredSq_sampleMean_tendstoInProb n hn2 hnle y v hvar hmax have hzCentered : FiniteDesign.TendstoInProb (fun k => completeRandomization (n k) (hnle k)) (fun k S => sampleMean (n k) (fun i => (y k i - popMean (y k)) ^ 2) S - popMean (fun i => (y k i - popMean (y k)) ^ 2)) (fun _ => 0) := by intro ε hε simpa using hz ε hε have hx := centered_sampleMean_tendstoInProb n hn2 hnle y v hnTop hvar have hxSq : FiniteDesign.TendstoInProb (fun k => completeRandomization (n k) (hnle k)) (fun k S => (sampleMean (n k) (fun i => y k i - popMean (y k)) S) ^ 2) (fun _ => 0) := by exact FiniteDesign.TendstoInProb.sq_zero hx have hscaleBdd : ∀ k, |(n k : ℝ) / ((n k : ℝ) - 1)| ≤ (2 : ℝ) := by intro k have hnR : (2 : ℝ) ≤ (n k : ℝ) := by exact_mod_cast hn2 k have hden : (0 : ℝ) < (n k : ℝ) - 1 := by linarith rw [abs_of_nonneg (div_nonneg (by positivity) hden.le)] rw [div_le_iff₀ hden] linarith have hzScaled := FiniteDesign.TendstoInProb.mul_deterministic_of_bounded (fun k => (n k : ℝ) / ((n k : ℝ) - 1)) 2 hscaleBdd hzCentered have hxScaled := FiniteDesign.TendstoInProb.mul_deterministic_of_bounded (fun k => (n k : ℝ) / ((n k : ℝ) - 1)) 2 hscaleBdd hxSq have hdet := scaled_popMean_centeredSq_sub_popVar_tendsto n hn2 hnle y v hnTop hvar have hdetProb := FiniteDesign.deterministic_tendstoInProb (fun k => completeRandomization (n k) (hnle k)) (fun k => ((n k : ℝ) / ((n k : ℝ) - 1)) * popMean (fun i => (y k i - popMean (y k)) ^ 2) - popVar (y k)) 0 hdet have hsum : FiniteDesign.TendstoInProb (fun k => completeRandomization (n k) (hnle k)) (fun k S => sampleVariance (n k) (y k) S - popVar (y k)) (fun _ => 0) := by convert (hzScaled.sub hxScaled).add hdetProb using 1 · funext k S rw [sampleVariance_eq_centered (n k) (hn0 k) (y k) S] ring · funext k ring intro ε hε simpa using hsum ε hε

theorem permutationNextMean_eq_remainingMean {N : ℕ} (y : Fin N → ℝ) (k : ℕ) (hk : k < N) (π : PermutationSampleSpace N) : permutationNextMean y k hk π = permutationRemainingSum y k hk.le π / ((N - k : ℕ) : ℝ) := by classical let D := uniformPermutationDesign N let c : ℝ := 1 / (card (PermutationSampleSpace N) : ℝ) let b := permutationPrefix k π have hcard : (card (PermutationSampleSpace N) : ℝ) ≠ 0 := by exact_mod_cast (Fintype.card_ne_zero : card (PermutationSampleSpace N) ≠ 0) have hc : c ≠ 0 := one_div_ne_zero hcard have hp : D.p π ≠ 0 := by change c ≠ 0 exact hc have hmass : fiberMass D (permutationPrefix k) b ≠ 0 := by intro hzero exact hp (p_eq_zero_of_mem_fiberMass_eq_zero D (permutationPrefix k) b hzero π rfl) have hnum : fiberNumerator D (permutationPrefix k) (fun σ (_ : Unit) => permutationDraw y k hk σ) b () = c * (∑ σ : PermutationSampleSpace N, if permutationPrefix k σ = b then permutationDraw y k hk σ else 0) := by unfold fiberNumerator rw [Finset.mul_sum] apply Finset.sum_congr rfl intro σ _ by_cases hσ : permutationPrefix k σ = b <;> simp [D, c, uniformPermutationDesign, hσ] have hmass' : fiberMass D (permutationPrefix k) b = c * (∑ σ : PermutationSampleSpace N, if permutationPrefix k σ = b then (1 : ℝ) else 0) := by unfold fiberMass rw [Finset.mul_sum] apply Finset.sum_congr rfl intro σ _ by_cases hσ : permutationPrefix k σ = b <;> simp [D, c, uniformPermutationDesign, hσ] have hcount : ((N - k : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (Nat.sub_pos_of_lt hk).ne' have hraw := remainingCount_mul_sum_prefixFiber_permutationDraw y k hk π have hweighted : ((N - k : ℕ) : ℝ) * fiberNumerator D (permutationPrefix k) (fun σ (_ : Unit) => permutationDraw y k hk σ) b () = fiberMass D (permutationPrefix k) b * permutationRemainingSum y k hk.le π := by rw [hnum, hmass'] dsimp only [b] calc ((N - k : ℕ) : ℝ) * (c * ∑ σ : PermutationSampleSpace N, if permutationPrefix k σ = permutationPrefix k π then permutationDraw y k hk σ else 0) = c * (((N - k : ℕ) : ℝ) * ∑ σ : PermutationSampleSpace N, if permutationPrefix k σ = permutationPrefix k π then permutationDraw y k hk σ else 0) := by ring _ = c * ((∑ σ : PermutationSampleSpace N, if permutationPrefix k σ = permutationPrefix k π then (1 : ℝ) else 0) * permutationRemainingSum y k hk.le π) := by rw [hraw] _ = (c * ∑ σ : PermutationSampleSpace N, if permutationPrefix k σ = permutationPrefix k π then (1 : ℝ) else 0) * permutationRemainingSum y k hk.le π := by ring unfold permutationNextMean finiteConditionalMean conditionalMeanAlongMap simp only [D, b, hmass, if_false] apply (div_eq_div_iff hmass hcount).2 calc fiberNumerator D (permutationPrefix k) (fun σ (_ : Unit) => permutationDraw y k hk σ) b () * ((N - k : ℕ) : ℝ) = ((N - k : ℕ) : ℝ) * fiberNumerator D (permutationPrefix k) (fun σ (_ : Unit) => permutationDraw y k hk σ) b () := mul_comm _ _ _ = fiberMass D (permutationPrefix k) b * permutationRemainingSum y k hk.le π := hweighted _ = permutationRemainingSum y k hk.le π * fiberMass D (permutationPrefix k) b := mul_comm _ _

theorem permutationCenteredDraw_condExp_zero {N : ℕ} (y : Fin N → ℝ) (k : ℕ) (hk : k < N) : ((uniformPermutationDesign N).toMeasure)[ fun π => permutationDraw y k hk π - permutationNextMean y k hk π | (permutationRevealFiltration N) k] =ᵐ[(uniformPermutationDesign N).toMeasure] 0 := by let μ := (uniformPermutationDesign N).toMeasure let m := (permutationRevealFiltration N) k have hsub := condExp_sub (Integrable.of_finite : Integrable (permutationDraw y k hk) μ) (Integrable.of_finite : Integrable (permutationNextMean y k hk) μ) m have hdraw := permutationNextMean_ae_eq_condExp y k hk have hmean : μ[permutationNextMean y k hk | m] = permutationNextMean y k hk := condExp_of_stronglyMeasurable ((permutationRevealFiltration N).le k) (permutationNextMean_stronglyMeasurable y k hk) Integrable.of_finite change μ[permutationDraw y k hk - permutationNextMean y k hk | m] =ᵐ[μ] 0 filter_upwards [hsub, hdraw] with π hsubπ hdrawπ change permutationNextMean y k hk π = μ[permutationDraw y k hk | m] π at hdrawπ rw [hsubπ] change μ[permutationDraw y k hk | m] π - μ[permutationNextMean y k hk | m] π = 0 rw [hmean, ← hdrawπ] simp

theorem permutationNextVariance_eq_remainingVariance {N : ℕ} (y : Fin N → ℝ) (k : ℕ) (hk : k < N) (π : PermutationSampleSpace N) : permutationNextVariance y k hk π = (∑ j : Fin (N - k), (y (π (permutationRemainingPosition k hk.le j)) - permutationNextMean y k hk π) ^ 2) / ((N - k : ℕ) : ℝ) := by classical let m := permutationNextMean y k hk π let z : Fin N → ℝ := fun i => (y i - m) ^ 2 have hfiber : finiteConditionalMean (uniformPermutationDesign N) (permutationPrefix k) (fun σ => (permutationDraw y k hk σ - permutationNextMean y k hk σ) ^ 2) (permutationPrefix k π) = finiteConditionalMean (uniformPermutationDesign N) (permutationPrefix k) (permutationDraw z k hk) (permutationPrefix k π) := by unfold finiteConditionalMean conditionalMeanAlongMap split_ifs with hmass · rfl · congr 1 unfold fiberNumerator apply Finset.sum_congr rfl intro σ _ by_cases hprefix : permutationPrefix k σ = permutationPrefix k π · have hremain := permutationRemainingSum_eq_of_prefix_eq y k hk.le σ π hprefix have hmean : permutationNextMean y k hk σ = m := by dsimp only [m] rw [permutationNextMean_eq_remainingMean, permutationNextMean_eq_remainingMean, hremain] simp [hprefix, permutationDraw, z, hmean, m] · simp [hprefix] unfold permutationNextVariance rw [hfiber] change permutationNextMean z k hk π = _ rw [permutationNextMean_eq_remainingMean, ← sum_remainingPositions_eq_permutationRemainingSum]

lemma E_compound (D₁ : FiniteDesign Ω₁) (D₂ : Ω₁ → ∀ i, FiniteDesign (α i)) (X : (Ω₁ × ∀ i, α i) → ℝ) : (compound D₁ D₂).E X = ∑ s, ∑ w : ∀ i, α i, D₁.p s * (∏ i, (D₂ s i).p (w i)) * X (s, w) := by simp only [FiniteDesign.E, compound, compoundCore, prodDesign_p] rw [Fintype.sum_prod_type]

lemma E_compound_factor (D₁ : FiniteDesign Ω₁) (D₂ : Ω₁ → ∀ i, FiniteDesign (α i)) (h : Ω₁ → ℝ) (j : ι) (g : α j → ℝ) : (compound D₁ D₂).E (fun sw => h sw.1 * g (sw.2 j)) = D₁.E (fun s => h s * (D₂ s j).E g) := by rw [E_compound] conv_rhs => rw [FiniteDesign.E] apply Finset.sum_congr rfl intro s _ rw [show (∑ w : ∀ i, α i, D₁.p s * (∏ i, (D₂ s i).p (w i)) * (h s * g (w j))) = D₁.p s * h s * ((prodDesign (D₂ s)).E (fun w => g (w j))) from by rw [FiniteDesign.E, Finset.mul_sum] apply Finset.sum_congr rfl intro w _ simp only [prodDesign_p] ring] rw [FiniteDesign.E_prod_apply] ring

lemma Var_compound_eq_tower (D₁ : FiniteDesign Ω₁) (D₂ : Ω₁ → ∀ i, FiniteDesign (α i)) (X : (Ω₁ × ∀ i, α i) → ℝ) : (compound D₁ D₂).Var X = D₁.E (fun s => (prodDesign (D₂ s)).Var (fun w => X (s, w))) + D₁.Var (fun s => (prodDesign (D₂ s)).E (fun w => X (s, w))) := by -- stage-2 conditional mean and variance set m : Ω₁ → ℝ := fun s => (prodDesign (D₂ s)).E (fun w => X (s, w)) with hm set v : Ω₁ → ℝ := fun s => (prodDesign (D₂ s)).Var (fun w => X (s, w)) with hv -- Var X = E[X²] − (E X)² rw [Var_eq] -- E[X²] = E_s[ E_{D₂ s}[ X(s,·)² ] ] = E_s[ v s + (m s)² ] (inner Var_eq) have hEsq : (compound D₁ D₂).E (fun sw => X sw ^ 2) = D₁.E (fun s => v s + (m s) ^ 2) := by rw [E_compound_tower] apply D₁.E_congr intro s have hinner : (prodDesign (D₂ s)).E (fun w => X (s, w) ^ 2) = v s + (m s) ^ 2 := by rw [hv, hm] simp only rw [Var_eq] ring -- the goal's inner expectation is over `fun w => (fun sw => X sw ^ 2) (s, w)` simpa using hinner -- E X = E_s[ m s ] have hEX : (compound D₁ D₂).E X = D₁.E m := by rw [E_compound_tower] rw [hEsq, hEX, E_add] -- now: D₁.E v + D₁.E (fun s => (m s)²) − (D₁.E m)² = D₁.E v + D₁.Var m rw [Var_eq] ring

theorem bernstein_abs_ge (X : Ω → ℝ) {c v ε : ℝ} (hc : 0 ≤ c) (hmean : D.E X = 0) (hbound : ∀ z, |X z| ≤ c) (hvar : D.Var X ≤ v) (hε : 0 ≤ ε) : D.Pr (fun z => ε ≤ |X z|) ≤ 2 * exp (-ε ^ 2 / (2 * (2 * v + c * ε))) := by have hvarneg : D.Var (fun z => -X z) = D.Var X := by have he : (fun z => -X z) = (fun z => (-1 : ℝ) * X z) := by funext z; ring rw [he, D.Var_const_mul]; ring have hsub := D.hasSubexponentialMGF_of_bounded X hc hmean hbound hvar have hpos := D.hasSubexponentialMGF_of_bounded (v := v) (fun z => -X z) hc (by rw [D.E_neg, hmean, neg_zero]) (fun z => by simpa [abs_neg] using hbound z) (by simpa only [hvarneg] using hvar) have hup : D.toMeasure.real {ω | ε ≤ X ω - 0} ≤ exp (-ε ^ 2 / (2 * (2 * v + c * ε))) := by simp only [sub_zero] exact hsub.measure_ge_le hε have hlow : D.toMeasure.real {ω | ε ≤ -X ω + 0} ≤ exp (-ε ^ 2 / (2 * (2 * v + c * ε))) := by simp only [add_zero] exact hpos.measure_ge_le hε have h := measureReal_abs_dev_le_two_sided (μ := D.toMeasure) X 0 (exp (-ε ^ 2 / (2 * (2 * v + c * ε)))) (exp (-ε ^ 2 / (2 * (2 * v + c * ε)))) ε hup hlow rw [D.Pr_eq_measureReal (fun z => ε ≤ |X z|)] simpa only [sub_zero, two_mul] using h

theorem bernstein_sum_ge_of_iIndepFun {n : ℕ} (hn : 0 < n) (X : Fin n → Ω → ℝ) {b sigma2 ε : ℝ} (hb : 0 ≤ b) (hsigma2 : 0 < sigma2) (hε : 0 ≤ ε) (hindep : iIndepFun X D.toMeasure) (hmean : ∀ i, D.E (X i) = 0) (hupper : ∀ i z, X i z ≤ b) (hsecond : ∀ i, D.E (fun z => X i z ^ 2) ≤ sigma2) : D.Pr (fun z => (n : ℝ) * ε ≤ ∑ i, X i z) ≤ exp (-(n : ℝ) * ε ^ 2 / (2 * (sigma2 + b * ε / 3))) := by rw [D.Pr_eq_measureReal] apply bernstein_sum_ge hn hb hsigma2 hε hindep (fun i => measurable_of_finite (X i)) (fun i => (D.memLp_toMeasure (X i) 1).integrable (by simp)) (fun i => (D.memLp_toMeasure (fun z => X i z ^ 2) 1).integrable (by simp)) · intro i rw [D.integral_toMeasure] exact hmean i · intro i exact Filter.Eventually.of_forall (hupper i) · intro i rw [D.integral_toMeasure] exact hsecond i

theorem dependency_studentized_cdf {Ω : ℕ → Type*} [∀ n, Fintype (Ω n)] [∀ n, MeasurableSpace (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (D : ∀ n, FiniteDesign (Ω n)) {ι : ℕ → Type*} [∀ n, Fintype (ι n)] (X : ∀ n, ι n → Ω n → ℝ) (Dep : ∀ n, DepGraph (X n) (D n).toMeasure) (Dmax : ℕ) (hdeg : ∀ n i, ((Dep n).nbhd i).card ≤ Dmax) (M : ℝ) (hM : 0 ≤ M) (hbound : ∀ n i ω, |X n i ω| ≤ M) (hmean : ∀ n i, (D n).E (X n i) = 0) (v : ℕ → ℝ) (hv : ∀ n, (D n).E (fun ω => depSum (X n) ω ^ 2) = 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 => (D n).Pr (fun ω => depSum (X n) ω / sqrt (v n) ≤ s)) atTop (𝓝 (stdNormalCdf s)) := by classical have hmean' : ∀ n i, ∫ ω, X n i ω ∂((D n).toMeasure) = 0 := by intro n i exact ((D n).integral_toMeasure (X n i)).trans (hmean n i) have hv' : ∀ n, ∫ ω, (depSum (X n) ω) ^ 2 ∂((D n).toMeasure) = v n := by intro n exact ((D n).integral_toMeasure (fun ω => (depSum (X n) ω) ^ 2)).trans (hv n) have hengine := bounded_degree_dependency_clt (fun n => (D n).toMeasure) X Dep Dmax hdeg M hM hbound hmean' v hv' c hc hvc hcard s rw [show stdNormalCdf s = (gaussianReal 0 1).real (Iic s) from rfl] refine hengine.congr (fun n => ?_) rw [← (D n).toMeasure_real_setOf, MeasureTheory.map_measureReal_apply (measurable_of_finite _) measurableSet_Iic] rfl

theorem var_edge_sum_le {ι : Type*} [Fintype ι] (b : ι → ι → Ω → ℝ) (G : ι → ι → Prop) [DecidableRel G] {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i j, G i j → ∀ z, |b i j z| ≤ M) (hsymm : ∀ i j, G i j → G j i) {m : ℕ} (hdeg : ∀ i, (Finset.univ.filter (fun j => G i j)).card ≤ m) (hvanish : ∀ i j, ¬ G i j → b i j = fun _ => 0) (hcov0 : ∀ i j k l, ¬ (G i k ∨ G i l ∨ G j k ∨ G j l) → D.Cov (b i j) (b k l) = 0) : D.Var (fun z => ∑ i, ∑ j, b i j z) ≤ 8 * M ^ 2 * ((m : ℝ) ^ 3 * (Fintype.card ι : ℝ)) := by classical -- local indicator set χ : Prop → ℝ := fun p => if p then (1 : ℝ) else 0 with hχdef have χ_nonneg : ∀ p, 0 ≤ χ p := by intro p; by_cases h : p <;> simp [hχdef, h] have χ_le_one : ∀ p, χ p ≤ 1 := by intro p; by_cases h : p <;> simp [hχdef, h] -- degree-sum bound: ∑ j χ(G i j) ≤ m have hdegsum : ∀ i : ι, (∑ j, χ (G i j)) ≤ (m : ℝ) := by intro i have : (∑ j, χ (G i j)) = ((Finset.univ.filter (fun j => G i j)).card : ℝ) := by convert Finset.sum_boole (fun j => G i j) Finset.univ using 3 rw [this] exact_mod_cast hdeg i -- out-degree via symmetry: ∑ k χ(G k l) ≤ m have hdegsum' : ∀ l : ι, (∑ k, χ (G k l)) ≤ (m : ℝ) := by intro l have hcong : (∑ k, χ (G k l)) = (∑ k, χ (G l k)) := by apply Finset.sum_congr rfl intro k _ have : G k l ↔ G l k := ⟨hsymm k l, hsymm l k⟩ simp only [this] rw [hcong] exact hdegsum l -- (a) expand the variance as a quadruple sum of covariances have hexpand : D.Var (fun z => ∑ i, ∑ j, b i j z) = ∑ i, ∑ j, ∑ k, ∑ l, D.Cov (b i j) (b k l) := by have hrw : (fun z => ∑ i, ∑ j, b i j z) = (fun z => ∑ p ∈ (Finset.univ : Finset (ι × ι)), (1 : ℝ) * b p.1 p.2 z) := by funext z rw [Fintype.sum_prod_type] apply Finset.sum_congr rfl; intro i _ apply Finset.sum_congr rfl; intro j _ rw [one_mul] rw [hrw, D.Var_linear_comb (Finset.univ : Finset (ι × ι)) (fun _ => 1) (fun p z => b p.1 p.2 z)] rw [Fintype.sum_prod_type] apply Finset.sum_congr rfl; intro i _ apply Finset.sum_congr rfl; intro j _ rw [Fintype.sum_prod_type] apply Finset.sum_congr rfl; intro k _ apply Finset.sum_congr rfl; intro l _ rw [one_mul, one_mul] rw [hexpand] -- (b) termwise bound: Cov ≤ |Cov| ≤ (2M²)·bracket set bracket : ι → ι → ι → ι → ℝ := fun i j k l => χ (G i j) * χ (G k l) * (χ (G i k) + χ (G i l) + χ (G j k) + χ (G j l)) with hbracketdef have bracket_nonneg : ∀ i j k l, 0 ≤ bracket i j k l := by intro i j k l rw [hbracketdef] apply mul_nonneg (mul_nonneg (χ_nonneg _) (χ_nonneg _)) have h1 := χ_nonneg (G i k); have h2 := χ_nonneg (G i l) have h3 := χ_nonneg (G j k); have h4 := χ_nonneg (G j l) linarith have htermwise : ∀ i j k l, D.Cov (b i j) (b k l) ≤ (2 * M ^ 2) * bracket i j k l := by intro i j k l -- Cov = 0 in the "otherwise" cases, and bracket ≥ 1 in the "all hold" case by_cases hij : G i j · by_cases hkl : G k l · by_cases hconn : G i k ∨ G i l ∨ G j k ∨ G j l · -- all hold: bracket ≥ 1, Cov ≤ |Cov| ≤ 2M² have hb1 : (1 : ℝ) ≤ bracket i j k l := by simp only [hbracketdef] have hχij : χ (G i j) = 1 := by simp [hχdef, hij] have hχkl : χ (G k l) = 1 := by simp [hχdef, hkl] rw [hχij, hχkl, one_mul, one_mul] have n1 := χ_nonneg (G i k); have n2 := χ_nonneg (G i l) have n3 := χ_nonneg (G j k); have n4 := χ_nonneg (G j l) rcases hconn with h | h | h | h · have : χ (G i k) = 1 := by simp [hχdef, h] linarith · have : χ (G i l) = 1 := by simp [hχdef, h] linarith · have : χ (G j k) = 1 := by simp [hχdef, h] linarith · have : χ (G j l) = 1 := by simp [hχdef, h] linarith have hcov : D.Cov (b i j) (b k l) ≤ 2 * M ^ 2 := (le_abs_self _).trans (by simpa [sq, mul_assoc] using D.abs_Cov_le_two_sq hM (hbound i j hij) (hbound k l hkl)) have h2M2 : 0 ≤ 2 * M ^ 2 := by positivity calc D.Cov (b i j) (b k l) ≤ 2 * M ^ 2 := hcov _ = (2 * M ^ 2) * 1 := by ring _ ≤ (2 * M ^ 2) * bracket i j k l := mul_le_mul_of_nonneg_left hb1 h2M2 · -- ¬ connected: Cov = 0, bracket ≥ 0 rw [hcov0 i j k l hconn] exact mul_nonneg (by positivity) (bracket_nonneg i j k l) · -- ¬ G k l: b k l = 0 so Cov = 0 have : D.Cov (b i j) (b k l) = 0 := by rw [D.Cov_congr (X := b i j) (Y := b k l) (X' := b i j) (Y' := fun _ => 0) (fun z => rfl) (fun z => by rw [hvanish k l hkl])] rw [D.Cov_comm, D.Cov_zero_left] rw [this] exact mul_nonneg (by positivity) (bracket_nonneg i j k l) · -- ¬ G i j: b i j = 0 so Cov = 0 have : D.Cov (b i j) (b k l) = 0 := by rw [D.Cov_congr (X := b i j) (Y := b k l) (X' := fun _ => 0) (Y' := b k l) (fun z => by rw [hvanish i j hij]) (fun z => rfl)] rw [D.Cov_zero_left] rw [this] exact mul_nonneg (by positivity) (bracket_nonneg i j k l) -- sum the termwise bound over the quadruple have hsumbound : (∑ i, ∑ j, ∑ k, ∑ l, D.Cov (b i j) (b k l)) ≤ ∑ i, ∑ j, ∑ k, ∑ l, (2 * M ^ 2) * bracket i j k l := by apply Finset.sum_le_sum; intro i _ apply Finset.sum_le_sum; intro j _ apply Finset.sum_le_sum; intro k _ apply Finset.sum_le_sum; intro l _ exact htermwise i j k l refine hsumbound.trans ?_ -- (c) pull out 2M² and split the bracket into four sums have hpull : (∑ i, ∑ j, ∑ k, ∑ l, (2 * M ^ 2) * bracket i j k l) = (2 * M ^ 2) * (∑ i, ∑ j, ∑ k, ∑ l, bracket i j k l) := by rw [Finset.mul_sum] apply Finset.sum_congr rfl; intro i _ rw [Finset.mul_sum] apply Finset.sum_congr rfl; intro j _ rw [Finset.mul_sum] apply Finset.sum_congr rfl; intro k _ rw [Finset.mul_sum] rw [hpull] -- split bracket into S1+S2+S3+S4 set S : (ι → ι → ι → ι → ℝ) → ℝ := fun f => ∑ i, ∑ j, ∑ k, ∑ l, f i j k l with hSdef have hsplit : (∑ i, ∑ j, ∑ k, ∑ l, bracket i j k l) = S (fun i j k l => χ (G i j) * χ (G k l) * χ (G i k)) + S (fun i j k l => χ (G i j) * χ (G k l) * χ (G i l)) + S (fun i j k l => χ (G i j) * χ (G k l) * χ (G j k)) + S (fun i j k l => χ (G i j) * χ (G k l) * χ (G j l)) := by simp only [hSdef] simp only [← Finset.sum_add_distrib] apply Finset.sum_congr rfl; intro i _ apply Finset.sum_congr rfl; intro j _ apply Finset.sum_congr rfl; intro k _ apply Finset.sum_congr rfl; intro l _ rw [hbracketdef]; ring rw [hsplit] -- Each of S1..S4 ≤ N·m³. We prove a generic factorization helper. -- Helper: ∑ over a slot of χ(edge) * (nonneg) ≤ m * sup, using degree bounds. -- We just prove the four bounds directly. have h2M2nn : (0 : ℝ) ≤ 2 * M ^ 2 := by positivity have hmnn : (0 : ℝ) ≤ (m : ℝ) := by positivity -- S1 = ∑i ∑j ∑k ∑l χ(Gij) χ(Gkl) χ(Gik) -- factor: ∑i (∑j χ(Gij)) * (∑k χ(Gik) * (∑l χ(Gkl))) have hS1 : S (fun i j k l => χ (G i j) * χ (G k l) * χ (G i k)) ≤ (Fintype.card ι : ℝ) * (m : ℝ) ^ 3 := by simp only [hSdef] have hcard : (Fintype.card ι : ℝ) * (m : ℝ) ^ 3 = ∑ _i : ι, (m : ℝ) ^ 3 := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] rw [hcard] apply Finset.sum_le_sum; intro i _ -- bound ∑j∑k∑l χ(Gij)χ(Gkl)χ(Gik) ≤ m^3 -- = (∑j χ(Gij)) * (∑k χ(Gik) * (∑l χ(Gkl))) have hfact : (∑ j, ∑ k, ∑ l, χ (G i j) * χ (G k l) * χ (G i k)) = (∑ j, χ (G i j)) * (∑ k, χ (G i k) * (∑ l, χ (G k l))) := by rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun j _ => ?_) rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun k _ => ?_) rw [Finset.mul_sum, Finset.mul_sum] refine Finset.sum_congr rfl (fun l _ => ?_) ring rw [hfact] -- inner: ∑k χ(Gik) * (∑l χ(Gkl)) ≤ ∑k χ(Gik) * m ≤ m * m have hinner : (∑ k, χ (G i k) * (∑ l, χ (G k l))) ≤ (m : ℝ) ^ 2 := by have h1 : (∑ k, χ (G i k) * (∑ l, χ (G k l))) ≤ ∑ k, χ (G i k) * (m : ℝ) := by apply Finset.sum_le_sum; intro k _ exact mul_le_mul_of_nonneg_left (hdegsum k) (χ_nonneg _) have h2 : (∑ k, χ (G i k) * (m : ℝ)) = (∑ k, χ (G i k)) * (m : ℝ) := by rw [Finset.sum_mul] have h3 : (∑ k, χ (G i k)) * (m : ℝ) ≤ (m : ℝ) * (m : ℝ) := mul_le_mul_of_nonneg_right (hdegsum i) hmnn calc (∑ k, χ (G i k) * (∑ l, χ (G k l))) ≤ (∑ k, χ (G i k)) * (m : ℝ) := by rw [← h2]; exact h1 _ ≤ (m : ℝ) * (m : ℝ) := h3 _ = (m : ℝ) ^ 2 := by ring have hjsum : (∑ j, χ (G i j)) ≤ (m : ℝ) := hdegsum i have hinner_nn : (0 : ℝ) ≤ ∑ k, χ (G i k) * (∑ l, χ (G k l)) := Finset.sum_nonneg (fun k _ => mul_nonneg (χ_nonneg _) (Finset.sum_nonneg (fun l _ => χ_nonneg _))) have hjsum_nn : (0 : ℝ) ≤ ∑ j, χ (G i j) := Finset.sum_nonneg (fun j _ => χ_nonneg _) calc (∑ j, χ (G i j)) * (∑ k, χ (G i k) * (∑ l, χ (G k l))) ≤ (m : ℝ) * (m : ℝ) ^ 2 := mul_le_mul hjsum hinner hinner_nn hmnn _ = (m : ℝ) ^ 3 := by ring -- S2 = ∑i∑j∑k∑l χ(Gij)χ(Gkl)χ(Gil) -- factor: ∑i (∑j χ(Gij)) * (∑l χ(Gil) * (∑k χ(Gkl))) -- middle edge i–l have hS2 : S (fun i j k l => χ (G i j) * χ (G k l) * χ (G i l)) ≤ (Fintype.card ι : ℝ) * (m : ℝ) ^ 3 := by simp only [hSdef] have hcard : (Fintype.card ι : ℝ) * (m : ℝ) ^ 3 = ∑ _i : ι, (m : ℝ) ^ 3 := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] rw [hcard] apply Finset.sum_le_sum; intro i _ -- ∑j∑k∑l χ(Gij)χ(Gkl)χ(Gil) = (∑j χ(Gij)) * (∑l χ(Gil) * (∑k χ(Gkl))) have hfact : (∑ j, ∑ k, ∑ l, χ (G i j) * χ (G k l) * χ (G i l)) = (∑ j, χ (G i j)) * (∑ l, χ (G i l) * (∑ k, χ (G k l))) := by rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun j _ => ?_) rw [Finset.sum_comm, Finset.mul_sum] refine Finset.sum_congr rfl (fun l _ => ?_) rw [Finset.mul_sum, Finset.mul_sum] refine Finset.sum_congr rfl (fun k _ => ?_) ring rw [hfact] have hinner : (∑ l, χ (G i l) * (∑ k, χ (G k l))) ≤ (m : ℝ) ^ 2 := by have h1 : (∑ l, χ (G i l) * (∑ k, χ (G k l))) ≤ ∑ l, χ (G i l) * (m : ℝ) := by apply Finset.sum_le_sum; intro l _ exact mul_le_mul_of_nonneg_left (hdegsum' l) (χ_nonneg _) have h2 : (∑ l, χ (G i l) * (m : ℝ)) = (∑ l, χ (G i l)) * (m : ℝ) := by rw [Finset.sum_mul] have h3 : (∑ l, χ (G i l)) * (m : ℝ) ≤ (m : ℝ) * (m : ℝ) := mul_le_mul_of_nonneg_right (hdegsum i) hmnn calc (∑ l, χ (G i l) * (∑ k, χ (G k l))) ≤ (∑ l, χ (G i l)) * (m : ℝ) := by rw [← h2]; exact h1 _ ≤ (m : ℝ) * (m : ℝ) := h3 _ = (m : ℝ) ^ 2 := by ring have hjsum : (∑ j, χ (G i j)) ≤ (m : ℝ) := hdegsum i have hinner_nn : (0 : ℝ) ≤ ∑ l, χ (G i l) * (∑ k, χ (G k l)) := Finset.sum_nonneg (fun l _ => mul_nonneg (χ_nonneg _) (Finset.sum_nonneg (fun k _ => χ_nonneg _))) have hjsum_nn : (0 : ℝ) ≤ ∑ j, χ (G i j) := Finset.sum_nonneg (fun j _ => χ_nonneg _) calc (∑ j, χ (G i j)) * (∑ l, χ (G i l) * (∑ k, χ (G k l))) ≤ (m : ℝ) * (m : ℝ) ^ 2 := mul_le_mul hjsum hinner hinner_nn hmnn -- … truncated; follow the source link for the rest …