Experimentation

theorem isTestSupermartingale_capital [IsProbabilityMeasure μ] {X lam : ℕ → Ω → ℝ} {m : ℝ} (hadapt : Adapted ℱ (capital X lam m)) (hlam : ∀ n, StronglyMeasurable[ℱ n] (lam n)) (hint : ∀ n, Integrable (capital X lam m n) μ) (hintX : ∀ n, Integrable (fun ω => X n ω - m) μ) (hintInc : ∀ n, Integrable (fun ω => lam n ω * (X n ω - m)) μ) (hbet : ∀ n ω, 0 ≤ 1 + lam n ω * (X n ω - m)) (hfair : ∀ n, μ[fun ω => X n ω - m | ℱ n] =ᵐ[μ] 0) : IsTestSupermartingale (capital X lam m) ℱ μ := by refine ⟨?super, capital_nonneg hbet, ?init⟩ · refine (martingale_nat hadapt.stronglyAdapted hint ?_).supermartingale intro n -- `Kₙ₊₁ = Kₙ · (1 + lamₙ(Xₙ−m))`; pull the `ℱn`-measurable factors `Kₙ`, `lamₙ` out of the -- conditional expectation and use the fair-bet condition `μ[Xₙ−m | ℱn] = 0`. have hcap : StronglyMeasurable[ℱ n] (capital X lam m n) := hadapt.stronglyAdapted n have hgint : Integrable (fun ω => 1 + lam n ω * (X n ω - m)) μ := (integrable_const (1 : ℝ)).add (hintInc n) have hcapsucc : capital X lam m (n + 1) = capital X lam m n * (fun ω => 1 + lam n ω * (X n ω - m)) := by rw [capital_succ]; rfl have hfgint : Integrable (capital X lam m n * (fun ω => 1 + lam n ω * (X n ω - m))) μ := by rw [← hcapsucc]; exact hint (n + 1) have hpull : μ[capital X lam m (n + 1) | ℱ n] =ᵐ[μ] capital X lam m n * μ[(fun ω => 1 + lam n ω * (X n ω - m)) | ℱ n] := by rw [hcapsucc] exact condExp_mul_of_stronglyMeasurable_left hcap hfgint hgint have hinc : μ[(fun ω => 1 + lam n ω * (X n ω - m)) | ℱ n] =ᵐ[μ] (fun _ => (1 : ℝ)) := by have hsplit : (fun ω => 1 + lam n ω * (X n ω - m)) = (fun _ => (1 : ℝ)) + (fun ω => lam n ω * (X n ω - m)) := by funext ω; rfl rw [hsplit] refine (condExp_add (integrable_const (1 : ℝ)) (hintInc n) (ℱ n)).trans ?_ have hc1 : μ[(fun _ => (1 : ℝ)) | ℱ n] = (fun _ => (1 : ℝ)) := condExp_const (ℱ.le n) 1 have hlampull : μ[(fun ω => lam n ω * (X n ω - m)) | ℱ n] =ᵐ[μ] lam n * μ[(fun ω => X n ω - m) | ℱ n] := condExp_mul_of_stronglyMeasurable_left (hlam n) (hintInc n) (hintX n) rw [hc1] filter_upwards [hlampull, hfair n] with ω h1 h2 simp only [Pi.add_apply, Pi.mul_apply, h1, h2] simp refine (hpull.trans ?_).symm filter_upwards [hinc] with ω hω simp only [Pi.mul_apply, hω, mul_one] · rw [capital_zero] simp [integral_const]

theorem E_htClusterEffect (p : C → ℝ) (n : C → ℕ) (y1 y0 : C → ℝ) (hp0 : ∀ c, 0 ≤ p c) (hp1 : ∀ c, p c ≤ 1) (hppos : ∀ c, 0 < p c) (hp1' : ∀ c, p c < 1) (hNpos : 0 < totalUnits n) : (clusterDesign p hp0 hp1).E (htClusterEffect p n y1 y0) = totalEffect n y1 y0 := by unfold htClusterEffect totalEffect have hNne : totalUnits n ≠ 0 := ne_of_gt hNpos rw [show (fun z => (htTreatedTotal p y1 z - htControlTotal p y0 z) / totalUnits n) = (fun z => (htTreatedTotal p y1 z - htControlTotal p y0 z) * (totalUnits n)⁻¹) from funext (fun z => by rw [div_eq_mul_inv])] rw [FiniteDesign.E_mul_const, FiniteDesign.E_sub, E_htTreatedTotal p y1 hp0 hp1 hppos, E_htControlTotal p y0 hp0 hp1 hp1', ← Finset.sum_sub_distrib, div_eq_mul_inv]

theorem Var_sampleMean (n : ℕ) (hn : n ≤ Fintype.card U) (hn0 : 0 < n) (hN : 2 ≤ Fintype.card U) (y : U → ℝ) : (completeRandomization n hn).Var (sampleMean n y) = (1 / (n : ℝ) - 1 / (Fintype.card U : ℝ)) * popVar y := by classical set D := completeRandomization n hn with hDdef -- the per-unit sampling indicator `1(i ∈ S)` set I : U → ({S : Finset U // S.card = n}) → ℝ := fun i => FiniteDesign.ind (fun S => i ∈ S.val) with hIdef have hNnat : 0 < Fintype.card U := lt_of_lt_of_le (by norm_num) hN have hNR : (Fintype.card U : ℝ) ≠ 0 := by exact_mod_cast hNnat.ne' have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast hn0.ne' have hN1R : (Fintype.card U : ℝ) - 1 ≠ 0 := by have h1 : (1 : ℝ) < Fintype.card U := by exact_mod_cast hN exact sub_ne_zero.mpr h1.ne' -- first-order and second-order inclusion probabilities have hπ : ∀ i, D.Pr (fun S => i ∈ S.val) = (n : ℝ) / Fintype.card U := fun i => completeRandomization_incl n hn i -- diagonal covariance: `Var(1ᵢ) = π(1−π)` have hdiag : ∀ i, D.Cov (I i) (I i) = (n : ℝ) / Fintype.card U * (1 - (n : ℝ) / Fintype.card U) := by intro i; rw [hIdef, FiniteDesign.Cov_self, FiniteDesign.Var_ind, hπ i] -- off-diagonal covariance: `Cov(1ᵢ,1ⱼ) = π_ij − π²` (i ≠ j) have hoff : ∀ i j, i ≠ j → D.Cov (I i) (I j) = (n : ℝ) * ((n : ℝ) - 1) / (Fintype.card U * ((Fintype.card U : ℝ) - 1)) - (n : ℝ) / Fintype.card U * ((n : ℝ) / Fintype.card U) := by intro i j hij rw [hIdef, FiniteDesign.Cov_eq] have hprod : (fun S : {S : Finset U // S.card = n} => FiniteDesign.ind (fun S => i ∈ S.val) S * FiniteDesign.ind (fun S => j ∈ S.val) S) = FiniteDesign.ind (fun S : {S : Finset U // S.card = n} => i ∈ S.val ∧ j ∈ S.val) := by funext S; simp only [FiniteDesign.ind] by_cases hi : i ∈ S.val <;> by_cases hj : j ∈ S.val <;> simp [hi, hj] rw [hprod, FiniteDesign.E_ind, FiniteDesign.E_ind, FiniteDesign.E_ind, completeRandomization_incl_pair n hn hij, hπ i, hπ j] -- `sampleMean = (1/n) · ∑ᵢ yᵢ · 1ᵢ` have hsm : sampleMean n y = fun S => (1 / (n : ℝ)) * ∑ i, y i * I i S := by funext S have hterm : (∑ i, if i ∈ S.val then y i else 0) = ∑ i, y i * I i S := by refine Finset.sum_congr rfl fun i _ => ?_ rw [hIdef]; simp only [FiniteDesign.ind]; by_cases h : i ∈ S.val <;> simp [h] change (∑ i, if i ∈ S.val then y i else 0) / (n : ℝ) = (1 / (n : ℝ)) * ∑ i, y i * I i S rw [hterm]; ring rw [hsm] rw [show (D.Var (fun S => 1 / (n : ℝ) * ∑ i, y i * I i S)) = (1 / (n : ℝ)) ^ 2 * D.Var (fun S => ∑ i, y i * I i S) from D.Var_const_mul (1 / (n : ℝ)) (fun S => ∑ i, y i * I i S)] rw [D.Var_linear_comb univ y I] -- collapse the double sum using `Cov(1ᵢ,1ⱼ) = off + 1{i=j}(diag − off)` set off : ℝ := (n : ℝ) * ((n : ℝ) - 1) / (Fintype.card U * ((Fintype.card U : ℝ) - 1)) - (n : ℝ) / Fintype.card U * ((n : ℝ) / Fintype.card U) with hoffdef set diag : ℝ := (n : ℝ) / Fintype.card U * (1 - (n : ℝ) / Fintype.card U) with hdiagdef have hcov : ∀ i j, y i * y j * D.Cov (I i) (I j) = y i * y j * off + (if i = j then y i * y j * (diag - off) else 0) := by intro i j by_cases hij : i = j · subst hij; rw [hdiag i, if_pos rfl]; ring · rw [hoff i j hij, if_neg hij]; ring simp_rw [hcov] -- collapse the double sum: `off·(∑y)² + (diag−off)·∑y²` have hsumsq : (∑ i, ∑ j, y i * y j) = (∑ i, y i) ^ 2 := by rw [sq, Finset.sum_mul_sum] have hsplit : (∑ i, ∑ j, (y i * y j * off + if i = j then y i * y j * (diag - off) else 0)) = off * (∑ i, y i) ^ 2 + (diag - off) * ∑ i, (y i) ^ 2 := by rw [show (∑ i, ∑ j, (y i * y j * off + if i = j then y i * y j * (diag - off) else 0)) = (∑ i, ∑ j, y i * y j * off) + (∑ i, ∑ j, (if i = j then y i * y j * (diag - off) else 0)) from by rw [← Finset.sum_add_distrib] exact Finset.sum_congr rfl fun i _ => Finset.sum_add_distrib] have hA : (∑ i, ∑ j, y i * y j * off) = off * (∑ i, y i) ^ 2 := by rw [← hsumsq, Finset.mul_sum] exact Finset.sum_congr rfl fun i _ => by rw [Finset.mul_sum]; exact Finset.sum_congr rfl fun j _ => by ring have hB : (∑ i, ∑ j, (if i = j then y i * y j * (diag - off) else 0)) = (diag - off) * ∑ i, (y i) ^ 2 := by rw [Finset.mul_sum] refine Finset.sum_congr rfl fun i _ => ?_ rw [Finset.sum_ite_eq univ i (fun j => y i * y j * (diag - off))] simp only [Finset.mem_univ, if_true]; ring rw [hA, hB] rw [hsplit, hoffdef, hdiagdef, popVar, popMean] -- computational variance formula `∑(yᵢ−ȳ)² = ∑yᵢ² − (∑y)²/N` have hexp : (∑ i, (y i - (∑ k, y k) / (Fintype.card U : ℝ)) ^ 2) = (∑ i, (y i) ^ 2) - (∑ i, y i) ^ 2 / (Fintype.card U : ℝ) := by have hpt : ∀ i, (y i - (∑ k, y k) / (Fintype.card U : ℝ)) ^ 2 = (y i) ^ 2 - 2 * ((∑ k, y k) / (Fintype.card U : ℝ)) * y i + ((∑ k, y k) / (Fintype.card U : ℝ)) ^ 2 := fun i => by ring simp_rw [hpt] rw [Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.mul_sum, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] field_simp ring rw [hexp] field_simp ring