Experimentation.Two­Stage­Interference

Formalization of Hudgens & Halloran (2008), "Toward Causal Inference With Interference" (JASA), building on the paper-agnostic design-based substrate Experimentation.DesignBased.

Asymptotic 29 core · 19 supporting · 8 submodules Asymptotic theory for two-stage interference experiments: setup, consistency, CLT discharge, studentized direct effects, and Wald intervals.
Basic 15 core · 0 supporting This file formalizes the design layer for Hudgens & Halloran (2008), "Toward Causal Inference With Interference." The population is partitioned into groups; each unit's potential outcome may depend on treatment assignmen ★ jointDesign★ CE_direct★ CE_indirect★ CE_total★ estDirect

Hudgens–Halloran (2008): two-stage interference setup, estimands, estimators

This file formalizes the design layer for Hudgens & Halloran (2008), "Toward Causal Inference With Interference." The population is partitioned into groups; each unit's potential outcome may depend on treatment assignments within its own group, but not on assignments in other groups.

Randomization is two-stage (Assumption 1): a first-stage design decides which groups receive allocation strategy ψ versus φ; conditionally, each group is randomized by its assigned within-group design. The joint law combines the first-stage design with the per-group product design, so cross-group independence is structural.

This file fixes the public vocabulary used by the rest of the subtree: assignment spaces WAssign and StratAssign, the compound two-stage design jointDesign, average-potential-outcome estimands indMean, groupMean, popMean, indMarg, and popMarg, causal contrasts CE_direct, CE_indirect, CE_total, and CE_overall, and the estimators groupEst, popEst, and estDirect. The unbiasedness and variance theorems for these definitions live in Unbiased.lean, Effects.lean, BetweenGroup.lean, and Variance.lean.

abbrev WAssign reviewed
Causalean.Experimentation.TwoStageInterference

Within-group assignment space for group i: a {treated/untreated} flag per unit.

Definition (Lean source)
abbrev WAssign (n : ι → ℕ) (i : ι) := Fin (n i) → Bool
Causalean.Experimentation.TwoStageInterference.WAssign · Causalean/Experimentation/TwoStageInterference/Basic.lean:40
abbrev StratAssign reviewed
Causalean.Experimentation.TwoStageInterference

Stage-1 strategy assignment space: each group is flagged ψ (true) or φ (false).

Definition (Lean source)
abbrev StratAssign (ι : Type*) := ι → Bool
Causalean.Experimentation.TwoStageInterference.StratAssign · Causalean/Experimentation/TwoStageInterference/Basic.lean:43
def jointDesign reviewed
Causalean.Experimentation.TwoStageInterference

The joint two-stage design: stage-1 design D₁ over strategy assignments, then, conditionally, group i is randomized by ψ i if assigned ψ and by φ i otherwise.

Definition (Lean source)
noncomputable def jointDesign (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) : FiniteDesign (StratAssign ι × ∀ i, WAssign n i) := compound D₁ (fun s i => if s i then ψ i else φ i)
Causalean.Experimentation.TwoStageInterference.jointDesign · Causalean/Experimentation/TwoStageInterference/Basic.lean:46 · uses FiniteDesign , StratAssign , WAssign
def indMean reviewed
Causalean.Experimentation.TwoStageInterference

Individual average potential outcome ȳ_ij(z;ρ): unit (i,j)'s expected outcome under within-group design ρ, conditional on its own treatment being z.

Definition (Lean source)
noncomputable def indMean (ρ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (i : ι) (j : Fin (n i)) (z : Bool) : ℝ := (ρ i).E (fun w => if w j = z then Y i j w else 0) / (ρ i).Pr (fun w => w j = z)
Causalean.Experimentation.TwoStageInterference.indMean · Causalean/Experimentation/TwoStageInterference/Basic.lean:55 · uses FiniteDesign , WAssign
def groupMean reviewed
Causalean.Experimentation.TwoStageInterference

Group average potential outcome ȳ_i(z;ρ) = (1/nᵢ)∑ⱼ ȳ_ij(z;ρ).

Definition (Lean source)
noncomputable def groupMean (ρ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (i : ι) (z : Bool) : ℝ := (∑ j, indMean ρ Y i j z) / (n i : ℝ)
Causalean.Experimentation.TwoStageInterference.groupMean · Causalean/Experimentation/TwoStageInterference/Basic.lean:61 · uses FiniteDesign , WAssign
def popMean reviewed
Causalean.Experimentation.TwoStageInterference

Population average potential outcome ȳ(z;ρ) = (1/N)∑ᵢ ȳ_i(z;ρ).

Definition (Lean source)
noncomputable def popMean (ρ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (z : Bool) : ℝ := (∑ i, groupMean ρ Y i z) / (Fintype.card ι : ℝ)
Causalean.Experimentation.TwoStageInterference.popMean · Causalean/Experimentation/TwoStageInterference/Basic.lean:66 · uses FiniteDesign , WAssign
def indMarg reviewed
Causalean.Experimentation.TwoStageInterference

Marginal individual average potential outcome ȳ_ij(ρ): expected outcome of (i,j) under design ρ, averaging over its own treatment as well (the overall-effect target).

Definition (Lean source)
noncomputable def indMarg (ρ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (i : ι) (j : Fin (n i)) : ℝ := (ρ i).E (fun w => Y i j w)
Causalean.Experimentation.TwoStageInterference.indMarg · Causalean/Experimentation/TwoStageInterference/Basic.lean:71 · uses FiniteDesign , WAssign
def popMarg reviewed
Causalean.Experimentation.TwoStageInterference

Population marginal average potential outcome ȳ(ρ) = (1/N)∑ᵢ(1/nᵢ)∑ⱼ ȳ_ij(ρ).

Definition (Lean source)
noncomputable def popMarg (ρ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) : ℝ := (∑ i, (∑ j, indMarg ρ Y i j) / (n i : ℝ)) / (Fintype.card ι : ℝ)
Causalean.Experimentation.TwoStageInterference.popMarg · Causalean/Experimentation/TwoStageInterference/Basic.lean:77 · uses FiniteDesign , WAssign
def CE_direct reviewed
Causalean.Experimentation.TwoStageInterference

Hudgens-Halloran direct-effect contrast. This is the population average outcome under treatment minus the population average outcome under control, evaluated under the strategy ψ.

Definition (Lean source)
noncomputable def CE_direct (ψ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) : ℝ := popMean ψ Y true - popMean ψ Y false
Causalean.Experimentation.TwoStageInterference.CE_direct · Causalean/Experimentation/TwoStageInterference/Basic.lean:82 · uses FiniteDesign , WAssign
def CE_indirect reviewed
Causalean.Experimentation.TwoStageInterference

Indirect (spillover) causal effect C̄E^I(φ,ψ) = ȳ(0;φ) − ȳ(0;ψ).

Definition (Lean source)
noncomputable def CE_indirect (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) : ℝ := popMean φ Y false - popMean ψ Y false
Causalean.Experimentation.TwoStageInterference.CE_indirect · Causalean/Experimentation/TwoStageInterference/Basic.lean:88 · uses FiniteDesign , WAssign
def CE_total reviewed
Causalean.Experimentation.TwoStageInterference

Total causal effect C̄E^T(φ,ψ) = ȳ(0;φ) − ȳ(1;ψ).

Definition (Lean source)
noncomputable def CE_total (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) : ℝ := popMean φ Y false - popMean ψ Y true
Causalean.Experimentation.TwoStageInterference.CE_total · Causalean/Experimentation/TwoStageInterference/Basic.lean:93 · uses FiniteDesign , WAssign
def CE_overall reviewed
Causalean.Experimentation.TwoStageInterference

Overall causal effect C̄E^O(φ,ψ) = ȳ(φ) − ȳ(ψ).

Definition (Lean source)
noncomputable def CE_overall (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) : ℝ := popMarg φ Y - popMarg ψ Y
Causalean.Experimentation.TwoStageInterference.CE_overall · Causalean/Experimentation/TwoStageInterference/Basic.lean:101 · uses FiniteDesign , WAssign
def groupEst reviewed
Causalean.Experimentation.TwoStageInterference

Within-group estimator Ŷ_i(z;ρ): the empirical mean outcome among the m units of group i whose own treatment equals z, as a function of the realized within-group assignment w. The denominator m is the (design-fixed) number of such units.

Definition (Lean source)
noncomputable def groupEst (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (i : ι) (z : Bool) (m : ℝ) (w : WAssign n i) : ℝ := (∑ j, if w j = z then Y i j w else 0) / m
Causalean.Experimentation.TwoStageInterference.groupEst · Causalean/Experimentation/TwoStageInterference/Basic.lean:111 · uses WAssign
def popEst reviewed
Causalean.Experimentation.TwoStageInterference

Population estimator Ŷ(z;ρ) on the groups assigned strategy pick: the average of the within-group estimators over the denom groups with s i = pick, as a function of the realized joint assignment (s, w). m i is the design-fixed count of z-units in group i.

Definition (Lean source)
noncomputable def popEst (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (z : Bool) (pick : Bool) (m : ι → ℝ) (denom : ℝ) (sw : StratAssign ι × ∀ i, WAssign n i) : ℝ := (∑ i, if sw.1 i = pick then groupEst Y i z (m i) (sw.2 i) else 0) / denom
Causalean.Experimentation.TwoStageInterference.popEst · Causalean/Experimentation/TwoStageInterference/Basic.lean:118 · uses StratAssign , WAssign
def estDirect reviewed
Causalean.Experimentation.TwoStageInterference

The Horvitz-Thompson estimator of the treatment-minus-control direct-effect contrast on the ψ-groups: the estimated treatment mean minus the estimated control mean.

Definition (Lean source)
noncomputable def estDirect (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (m0 m1 : ι → ℝ) (denom : ℝ) (sw : StratAssign ι × ∀ i, WAssign n i) : ℝ := popEst Y true true m1 denom sw - popEst Y false true m0 denom sw
Causalean.Experimentation.TwoStageInterference.estDirect · Causalean/Experimentation/TwoStageInterference/Basic.lean:126 · uses StratAssign , WAssign
Complete­Randomization 5 core · 8 supporting This file pushes the paper-agnostic complete-randomization design on fixed-size treated sets forward to the Boolean assignment spaces used by the two-stage interference modules. ★ crdOn★ crdOn_pair★ crd

Completely randomized assignment on Boolean vectors

This file pushes the paper-agnostic complete-randomization design on fixed-size treated sets forward to the Boolean assignment spaces used by the two-stage interference modules. It proves the first- and second-order inclusion probabilities and deterministic treated-count support facts needed to instantiate the Hudgens-Halloran variance theorems under actual complete randomization.

The general construction is crdOn for any finite population U; crd is the within-group specialization to Fin n. The exported facts crdOn_mean, crdOn_pair, crdOn_supp, crd_mean, crd_pair, crd_supp, crd_prop_true, and crd_prop_false are the moment and propensity lemmas consumed by the unbiasedness and variance files.

def crdToBoolOn reviewed
Causalean.Experimentation.TwoStageInterference

The treated-set-to-indicator map: a size-K treated set S becomes the Boolean assignment that flags unit i true exactly when i ∈ S.

Definition (Lean source)
def crdToBoolOn (S : {S : Finset U // S.card = K}) : U → Bool := fun i => decide (i ∈ S.val)
Causalean.Experimentation.TwoStageInterference.crdToBoolOn · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:59
def crdOn reviewed
Causalean.Experimentation.TwoStageInterference

The completely randomized design on U → Bool. Exactly K of the N = card U units are treated, with every one of the (N choose K) treated sets equally likely. Realized as the pushforward of completeRandomization K (on size-K treated sets) along the indicator-vector map crdToBoolOn.

Definition (Lean source)
noncomputable def crdOn : FiniteDesign (U → Bool) := (completeRandomization K hK).map (crdToBoolOn K)
Causalean.Experimentation.TwoStageInterference.crdOn · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:64 · uses FiniteDesign
lemma crdOn_pair reviewed
Causalean.Experimentation.TwoStageInterference

Second-order inclusion probability of the completely randomized design. Under the completely randomized design that treats exactly K of the N units in the population uniformly over all size-K treated subsets, if i and j are two distinct units then the probability that both i and j are treated equals K(K−1)/(N(N−1)).

Formal statement
i j :
U
hij :
i ≠ j
(crdOn K hK).E (fun w => (FiniteDesign.ind fun w => w i = true) w * (FiniteDesign.ind fun w => w j = true) w)
= (K * (K - 1) : ℝ) / (Fintype.card U * ((Fintype.card U : ℝ) - 1))
Proof (Lean source)
lemma crdOn_pair (i j : U) (hij : i ≠ j) : (crdOn K hK).E (fun w => (FiniteDesign.ind fun w => w i = true) w * (FiniteDesign.ind fun w => w j = true) w) = (K * (K - 1) : ℝ) / (Fintype.card U * ((Fintype.card U : ℝ) - 1)) := by rw [crdOn, FiniteDesign.E_map] have hfun : (fun S => (FiniteDesign.ind (fun w => w i = true) (crdToBoolOn K S)) * (FiniteDesign.ind (fun w => w j = true) (crdToBoolOn K S))) = FiniteDesign.ind (fun S : {S : Finset U // S.card = K} => i ∈ S.val ∧ j ∈ S.val) := by funext S by_cases hi : i ∈ S.val <;> by_cases hj : j ∈ S.val <;> simp [crdToBoolOn, FiniteDesign.ind, hi, hj] rw [hfun, FiniteDesign.E_ind, completeRandomization_incl_pair _ _ hij]
Causalean.Experimentation.TwoStageInterference.crdOn_pair · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:91 · uses E , ind , crdOn
def crdToBool reviewed
Causalean.Experimentation.TwoStageInterference

The within-group treated-set-to-indicator map (specialization of crdToBoolOn to Fin n).

Definition (Lean source)
def crdToBool (S : {S : Finset (Fin n) // S.card = K}) : Fin n → Bool := crdToBoolOn K S
Causalean.Experimentation.TwoStageInterference.crdToBool · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:140
def crd reviewed
Causalean.Experimentation.TwoStageInterference

The within-group completely randomized design on Fin n → Bool. Exactly K of the n units are treated, uniformly over the (n choose K) treated sets — the U = Fin n specialization of crdOn.

Definition (Lean source)
noncomputable def crd : FiniteDesign (Fin n → Bool) := crdOn K (hK.trans_eq (Fintype.card_fin n).symm)
8 supporting declarations (lemmas, instances)
  • crdOn_mean lemma — First-order inclusion probability: each unit i is treated with probability K/N, i.e. E[Tᵢ] = K/N. Derived from completeRandomization_incl.
    i :
    U
    (crdOn K hK).E (FiniteDesign.ind fun w => w i = true) = (K : ℝ) / card U
    Proof (Lean source)
    lemma crdOn_mean (i : U) : (crdOn K hK).E (FiniteDesign.ind fun w => w i = true) = (K : ℝ) / card U := by rw [crdOn, FiniteDesign.E_map] have hfun : (fun S => FiniteDesign.ind (fun w => w i = true) (crdToBoolOn K S)) = FiniteDesign.ind (fun S : {S : Finset U // S.card = K} => i ∈ S.val) := by funext S; by_cases h : i ∈ S.val <;> simp [crdToBoolOn, FiniteDesign.ind, h] rw [hfun, FiniteDesign.E_ind, completeRandomization_incl]
    Causalean.Experimentation.TwoStageInterference.crdOn_mean · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:71
  • crdOn_mean_compl lemma — Complementary first moment: each unit i is untreated with probability (N−K)/N, i.e. E[1−Tᵢ] = (N−K)/N. The control-arm propensity, from the indicator complement 1 − Tᵢ.
    i :
    U
    (crdOn K hK).E (fun w => 1 - FiniteDesign.ind (fun w => w i = true) w)
    = ((Fintype.card U : ℝ) - K) / Fintype.card U
    Proof (Lean source)
    lemma crdOn_mean_compl (i : U) : (crdOn K hK).E (fun w => 1 - FiniteDesign.ind (fun w => w i = true) w) = ((Fintype.card U : ℝ) - K) / Fintype.card U := by have hNpos : (0 : ℝ) < Fintype.card U := by exact_mod_cast Fintype.card_pos_iff.mpr ⟨i⟩ rw [FiniteDesign.E_sub, FiniteDesign.E_const, crdOn_mean] field_simp
    Causalean.Experimentation.TwoStageInterference.crdOn_mean_compl · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:81
  • crdOn_supp lemma — Deterministic treated count on the design's support: any assignment with positive design weight treats exactly K units, i.e. ∑ᵢ Tᵢ = K.
    w :
    U → Bool
    hw :
    (crdOn K hK).p w ≠ 0
    (∑ i, (FiniteDesign.ind fun w => w i = true) w) = (K : ℝ)
    Proof (Lean source)
    lemma crdOn_supp (w : U → Bool) (hw : (crdOn K hK).p w ≠ 0) : (∑ i, (FiniteDesign.ind fun w => w i = true) w) = (K : ℝ) := by rw [crdOn] at hw simp only [FiniteDesign.map_p] at hw obtain ⟨S, _, hSne⟩ := Finset.exists_ne_zero_of_sum_ne_zero hw have hSw : crdToBoolOn K S = w := by by_contra h; simp [h] at hSne have hiff : ∀ i, (w i = true) ↔ i ∈ S.val := by intro i have : w i = decide (i ∈ S.val) := by rw [← hSw]; rfl rw [this, decide_eq_true_eq] have hstep : (∑ i, (FiniteDesign.ind fun w => w i = true) w) = ∑ i, if i ∈ S.val then (1 : ℝ) else 0 := by refine Finset.sum_congr rfl fun i _ => ?_ unfold FiniteDesign.ind by_cases h : i ∈ S.val <;> simp [hiff i, h] rw [hstep, Finset.sum_ite_mem, Finset.univ_inter, Finset.sum_const, nsmul_eq_mul, mul_one] exact_mod_cast S.property
    Causalean.Experimentation.TwoStageInterference.crdOn_supp · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:111
  • crd_mean lemma — First-order inclusion probability of the within-group design: E[Tⱼ] = K/n.
    j :
    Fin n
    (crd K hK).E (FiniteDesign.ind fun w => w j = true) = (K : ℝ) / n
    Proof (Lean source)
    lemma crd_mean (j : Fin n) : (crd K hK).E (FiniteDesign.ind fun w => w j = true) = (K : ℝ) / n := by rw [crd, crdOn_mean, Fintype.card_fin]
    Causalean.Experimentation.TwoStageInterference.crd_mean · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:149
  • crd_pair lemma — Second-order inclusion probability of the within-group design: E[Tⱼ Tₖ] = K(K−1)/(n(n−1)) for j ≠ k.
    j k :
    Fin n
    hjk :
    j ≠ k
    (crd K hK).E (fun w => (FiniteDesign.ind fun w => w j = true) w * (FiniteDesign.ind fun w => w k = true) w)
    = (K * (K - 1) : ℝ) / (n * (n - 1))
    Proof (Lean source)
    lemma crd_pair (j k : Fin n) (hjk : j ≠ k) : (crd K hK).E (fun w => (FiniteDesign.ind fun w => w j = true) w * (FiniteDesign.ind fun w => w k = true) w) = (K * (K - 1) : ℝ) / (n * (n - 1)) := by rw [crd, crdOn_pair _ _ _ _ hjk, Fintype.card_fin]
    Causalean.Experimentation.TwoStageInterference.crd_pair · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:154
  • crd_supp lemma — Deterministic treated count on the within-group design's support: ∑ⱼ Tⱼ = K.
    w :
    Fin n → Bool
    hw :
    (crd K hK).p w ≠ 0
    (∑ j, (FiniteDesign.ind fun w => w j = true) w) = (K : ℝ)
    Proof (Lean source)
    lemma crd_supp (w : Fin n → Bool) (hw : (crd K hK).p w ≠ 0) : (∑ j, (FiniteDesign.ind fun w => w j = true) w) = (K : ℝ) := by rw [crd] at hw exact crdOn_supp K _ w hw
    Causalean.Experimentation.TwoStageInterference.crd_supp · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:162
  • crd_prop_true lemma — Treatment propensity of the within-group design: each unit j is treated with probability K/n, i.e. Pr[wⱼ = true] = K/n.
    j :
    Fin n
    (crd K hK).Pr (fun w => w j = true) = (K : ℝ) / n
    Proof (Lean source)
    lemma crd_prop_true (j : Fin n) : (crd K hK).Pr (fun w => w j = true) = (K : ℝ) / n := crd_mean K hK j
    Causalean.Experimentation.TwoStageInterference.crd_prop_true · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:168
  • crd_prop_false lemma — Control propensity of the within-group design: each unit j is in control with probability (n−K)/n, i.e. Pr[wⱼ = false] = (n−K)/n.
    j :
    Fin n
    (crd K hK).Pr (fun w => w j = false) = ((n : ℝ) - K) / n
    Proof (Lean source)
    lemma crd_prop_false (j : Fin n) : (crd K hK).Pr (fun w => w j = false) = ((n : ℝ) - K) / n := by have hind : (FiniteDesign.ind fun w : Fin n → Bool => w j = false) = (fun w : Fin n → Bool => 1 - FiniteDesign.ind (fun w => w j = true) w) := by funext w; unfold FiniteDesign.ind; cases hw : w j <;> simp [hw] change (crd K hK).E (FiniteDesign.ind fun w : Fin n → Bool => w j = false) = _ rw [hind, crd, crdOn_mean_compl, Fintype.card_fin]
    Causalean.Experimentation.TwoStageInterference.crd_prop_false · Causalean/Experimentation/TwoStageInterference/CompleteRandomization.lean:174
Stage­One 2 core · 0 supporting Simple-random-sampling selection contributes the finite-population between-group variance term. ★ Var_srs_mean

Stage-one sampling variance

Simple-random-sampling selection contributes the finite-population between-group variance term.

This file defines SmuVar, the N - 1 sample variance of group-level quantities, and proves Var_srs_mean: under simple-random-sampling first- and second-order selection moments, the variance of the selected group mean is (1 - m/N) / m * SmuVar. The result is design-agnostic and is used as the between-group term in the two-stage variance decompositions.

def SmuVar reviewed
Causalean.Experimentation.TwoStageInterference

The population sample variance (Neyman N−1 denominator) of the group-level quantities μ, Sμ² = (∑ᵢ(μᵢ − μ̄)²)/(N−1), where N := card ι and μ̄ = (∑ μ)/N.

Definition (Lean source)
noncomputable def SmuVar (μ : ι → ℝ) : ℝ := (∑ i, (μ i - (∑ i, μ i) / (Fintype.card ι : ℝ)) ^ 2) / ((Fintype.card ι : ℝ) - 1)
Causalean.Experimentation.TwoStageInterference.SmuVar · Causalean/Experimentation/TwoStageInterference/StageOne.lean:46
theorem Var_srs_mean reviewed
Causalean.Experimentation.TwoStageInterference

Stage-1 / between-group SRS variance term (Hudgens–Halloran 2008, the between-group term of Theorems 4 and 6). Under simple random sampling of m of the N := card ι groups, with {0,1} selection indicators U satisfying the SRS first- and second-order selection moments (hmean, hpair) and the Bernoulli diagonal variance (hvar), the sampling variance of the sample mean (∑ᵢ Uᵢ·μᵢ)/m of the group-level quantities μ equals (1 − m/N)/m times the population sample variance SmuVar μ.

Formal statement
D₁.Var (fun s => (∑ i, U i s * μ i) / m) = (1 - m / (Fintype.card ι : ℝ)) / m * SmuVar μ
Proof (Lean source)
theorem Var_srs_mean : D₁.Var (fun s => (∑ i, U i s * μ i) / m) = (1 - m / (Fintype.card ι : ℝ)) / m * SmuVar μ := by set N : ℝ := (Fintype.card ι : ℝ) with hNdef -- Step 1: write the mean as `(1/m) · ∑ᵢ μᵢ · Uᵢ` and pull the constant out of the variance. have hmeanform : (fun s => (∑ i, U i s * μ i) / m) = (fun s => (1 / m) * (∑ i, μ i * U i s)) := by funext s rw [Finset.sum_div, Finset.mul_sum] refine Finset.sum_congr rfl (fun i _ => ?_) rw [mul_comm (μ i) (U i s)]; ring rw [hmeanform, FiniteDesign.Var_const_mul] -- Step 2: `Var(∑ μᵢ Uᵢ) = ∑ᵢ∑ⱼ μᵢμⱼ Cov(Uᵢ,Uⱼ)`. rw [FiniteDesign.Var_linear_comb] -- Step 3: the covariances are two-valued — `vd` on the diagonal, `vo` off it. set vd : ℝ := (m / N) * (1 - m / N) with hvd set vo : ℝ := (m * (m - 1)) / (N * (N - 1)) - (m / N) * (m / N) with hvo have hcov : ∀ i j, D₁.Cov (U i) (U j) = if i = j then vd else vo := by intro i j by_cases h : i = j · subst h; rw [if_pos rfl, hvd, FiniteDesign.Cov_self, hvar i] · rw [if_neg h, hvo, FiniteDesign.Cov_eq, hpair i j h, hmean i, hmean j] have hrw : ∀ i j, μ i * μ j * D₁.Cov (U i) (U j) = μ i * μ j * (if i = j then vd else vo) := fun i j => by rw [hcov i j] simp only [hrw] -- Step 4: collapse the double sum to `vo·(∑μ)² + (vd−vo)·∑μ²`. rw [sum_sum_ite_quadratic univ μ vd vo] -- Step 5: rewrite `∑μ² − (∑μ)²/N` as `∑(μ−μ̄)²` and finish by field algebra. unfold SmuVar rw [← hNdef] -- `∑ᵢ(μᵢ − μ̄)² = ∑μ² − (∑μ)²/N`, the population deviation-sum identity over `ι`. have hNne : N ≠ 0 := hN have hcardN : (∑ _i : ι, ((∑ i, μ i) / N) ^ 2) = (∑ i, μ i) ^ 2 / N := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, ← hNdef] field_simp have hdev : (∑ i, (μ i - (∑ i, μ i) / N) ^ 2) = (∑ i, (μ i) ^ 2) - (∑ i, μ i) ^ 2 / N := by have hexp : ∀ i, (μ i - (∑ i, μ i) / N) ^ 2 = (μ i) ^ 2 - 2 * ((∑ i, μ i) / N) * (μ i) + ((∑ i, μ i) / N) ^ 2 := fun i => by ring simp only [hexp, Finset.sum_add_distrib, Finset.sum_sub_distrib] rw [hcardN, ← Finset.mul_sum] field_simp ring rw [hdev, hvd, hvo] -- Pure field algebra over the raw moment sums; constant `(1−m/N)/m` verified symbolically. have hNsub : N - 1 ≠ 0 := hN1 clear_value N field_simp [hm, hNne, hNsub] ring
Causalean.Experimentation.TwoStageInterference.Var_srs_mean · Causalean/Experimentation/TwoStageInterference/StageOne.lean:62 · uses FiniteDesign , E , Var , SmuVar
Variance 8 core · 5 supporting This file proves the Hudgens-Halloran within-group difference-in-means variance identity. ★ Var_tauHat★ Var_tauHat_CRD

Within-group Neyman variance under complete randomization

This file proves the Hudgens-Halloran within-group difference-in-means variance identity. The generic theorem states the Neyman split S₁/K + S₀/(n−K) − Sτ/n from first- and second-order treatment-indicator moments, then specializes it to the completely randomized within-group design.

The public definitions are the treatment indicator T, the difference-in-means statistic tauHat, the population mean popMeanV, and the sample variances S1, S0, and Stau. Var_tauHat is the moment-conditioned theorem; Var_tauHat_CRD is the corresponding theorem for the actual completely randomized design, with crd_mean and crd_pair supplying the moments.

def T reviewed
Causalean.Experimentation.TwoStageInterference

Treatment indicator of unit j: 1 on within-group assignments that treat j, 0 otherwise. (The indicator does not depend on the design.)

Definition (Lean source)
noncomputable def T (j : Fin n) : (Fin n → Bool) → ℝ := FiniteDesign.ind (fun w => w j = true)
Causalean.Experimentation.TwoStageInterference.T · Causalean/Experimentation/TwoStageInterference/Variance.lean:104
def tauHat reviewed
Causalean.Experimentation.TwoStageInterference

The difference-in-means estimator ȳ(0) − ȳ(1): the mean untreated-state outcome among the n − K control units minus the mean treated-state outcome among the K treated units, as a function of the realized assignment. On the design's support the treated units realize a and the control units realize b, so this is linear in the treatment indicators.

Definition (Lean source)
noncomputable def tauHat : (Fin n → Bool) → ℝ := fun w => (∑ j, b j * (1 - T j w)) / (n - K : ℝ) - (∑ j, a j * T j w) / K
Causalean.Experimentation.TwoStageInterference.tauHat · Causalean/Experimentation/TwoStageInterference/Variance.lean:111
def popMeanV reviewed
Causalean.Experimentation.TwoStageInterference

Population mean of a unit-indexed quantity: (1/n)∑ⱼ x j.

Definition (Lean source)
noncomputable def popMeanV (x : Fin n → ℝ) : ℝ := (∑ j, x j) / n
Causalean.Experimentation.TwoStageInterference.popMeanV · Causalean/Experimentation/TwoStageInterference/Variance.lean:120
def S1 reviewed
Causalean.Experimentation.TwoStageInterference

Population sample variance of the treated-state outcomes a, S₁ = (1/(n−1))∑ⱼ(a j − ā)².

Definition (Lean source)
noncomputable def S1 : ℝ := (∑ j, (a j - popMeanV a) ^ 2) / (n - 1 : ℝ)
Causalean.Experimentation.TwoStageInterference.S1 · Causalean/Experimentation/TwoStageInterference/Variance.lean:123
def S0 reviewed
Causalean.Experimentation.TwoStageInterference

Population sample variance of the untreated-state outcomes b, S₀ = (1/(n−1))∑ⱼ(b j − b̄)².

Definition (Lean source)
noncomputable def S0 : ℝ := (∑ j, (b j - popMeanV b) ^ 2) / (n - 1 : ℝ)
Causalean.Experimentation.TwoStageInterference.S0 · Causalean/Experimentation/TwoStageInterference/Variance.lean:126
def Stau reviewed
Causalean.Experimentation.TwoStageInterference

Population sample variance of the unit-level treatment effects a j − b j, Sτ = (1/(n−1))∑ⱼ((a j − b j) − (ā − b̄))².

Definition (Lean source)
noncomputable def Stau : ℝ := (∑ j, ((a j - b j) - (popMeanV a - popMeanV b)) ^ 2) / (n - 1 : ℝ)
Causalean.Experimentation.TwoStageInterference.Stau · Causalean/Experimentation/TwoStageInterference/Variance.lean:130
theorem Var_tauHat reviewed
Causalean.Experimentation.TwoStageInterference

Hudgens–Halloran (2008), Theorem 5 (within-group / Neyman form). For any within-group design whose treatment indicators have first moment K/n (hmean) and pairwise second moment K(K−1)/(n(n−1)) (hpair) — the moments of the completely randomized (mixed) design of Assumption 1, which treats exactly K of n units — with the two-valued potential outcomes a (treated state) and b (control state), the randomization variance of the difference-in-means estimator is S₁/K + S₀/(n−K) − Sτ/n.

Formal statement
ρ.Var (tauHat K a b) = S1 a / K + S0 b / (n - K) - Stau a b / n
Proof (Lean source)
theorem Var_tauHat : ρ.Var (tauHat K a b) = S1 a / K + S0 b / (n - K) - Stau a b / n := by -- Write the estimator as a linear combination of the indicators plus a constant. set c : Fin n → ℝ := fun j => -(b j / (n - K) + a j / K) with hc have hlin : tauHat K a b = fun w => (∑ j, c j * T j w) + (∑ j, b j) / (n - K) := by funext w; unfold tauHat have e1 : ∑ j, b j * (1 - T j w) = (∑ j, b j) - ∑ j, b j * T j w := by rw [← Finset.sum_sub_distrib]; exact Finset.sum_congr rfl (fun j _ => by ring) have e2 : ∑ j, c j * T j w = -((∑ j, b j * T j w) / (n - K)) - (∑ j, a j * T j w) / K := by rw [Finset.sum_div, Finset.sum_div, ← Finset.sum_neg_distrib, ← Finset.sum_sub_distrib] exact Finset.sum_congr rfl (fun j _ => by rw [hc]; ring) rw [e1, e2]; ring rw [hlin, FiniteDesign.Var_add_const, FiniteDesign.Var_linear_comb] -- The completely-randomized covariances are two-valued: `vd` on the diagonal, `vo` off it. set vd : ℝ := (K / n : ℝ) * (1 - K / n) with hvd set vo : ℝ := (K * (K - 1) : ℝ) / (n * (n - 1)) - (K / n) * (K / n) with hvo have hcov : ∀ i j, ρ.Cov (T i) (T j) = if i = j then vd else vo := by intro i j by_cases h : i = j · subst h; rw [if_pos rfl, hvd]; exact cov_diag K ρ hmean i · rw [if_neg h, hvo]; exact cov_offdiag K ρ hmean hpair i j h have hrw : ∀ i j, c i * c j * ρ.Cov (T i) (T j) = c i * c j * (if i = j then vd else vo) := fun i j => by rw [hcov i j] simp only [hrw] rw [sum_sum_ite_quadratic univ c vd vo] -- Positivity of the denominators. have hKr : (K : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hK.ne' have hKn' : (K : ℝ) < n := by exact_mod_cast hKn have hnKpos : (0 : ℝ) < n - K := by linarith have hnKr : (n - K : ℝ) ≠ 0 := ne_of_gt hnKpos have hn1pos : (1 : ℝ) < n := by exact_mod_cast lt_of_le_of_lt hK hKn have hnpos0 : (0 : ℝ) < n := by linarith have hnr : (n : ℝ) ≠ 0 := ne_of_gt hnpos0 have hn1r : (n - 1 : ℝ) ≠ 0 := by have : (0 : ℝ) < n - 1 := by linarith exact ne_of_gt this -- Linear and quadratic sums of the coefficients in terms of raw moments. have hsumc : (∑ j, c j) = -((∑ j, b j) / (n - K) + (∑ j, a j) / K) := by simp only [hc] rw [Finset.sum_neg_distrib] congr 1 rw [Finset.sum_div, Finset.sum_div, ← Finset.sum_add_distrib] have hsumc2 : (∑ j, c j ^ 2) = (∑ j, b j ^ 2) / (n - K) ^ 2 + 2 * (∑ j, a j * b j) / ((n - K) * K) + (∑ j, a j ^ 2) / K ^ 2 := by simp only [hc] rw [show (∑ j, b j ^ 2) / (↑n - ↑K) ^ 2 + 2 * (∑ j, a j * b j) / ((↑n - ↑K) * ↑K) + (∑ j, a j ^ 2) / ↑K ^ 2 = (∑ j, b j ^ 2) / (↑n - ↑K) ^ 2 + (∑ j, 2 * (a j * b j)) / ((↑n - ↑K) * ↑K) + (∑ j, a j ^ 2) / ↑K ^ 2 from by rw [← Finset.mul_sum]] rw [Finset.sum_div, Finset.sum_div, Finset.sum_div, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib] exact Finset.sum_congr rfl (fun j _ => by field_simp; ring) -- Unfold the sample variances via the deviation-sum identity. have hnpos : 0 < n := lt_of_le_of_lt (zero_le K) hKn unfold S1 S0 Stau popMeanV rw [sum_sub_mean_sq hnpos a, sum_sub_mean_sq hnpos b] -- For Sτ, rewrite the mean of effects as the difference of means, then apply the identity. have hStau : (∑ j, ((a j - b j) - ((∑ i, a i) / n - (∑ i, b i) / n)) ^ 2) = (∑ j, (a j - b j) ^ 2) - (∑ i, (a i - b i)) ^ 2 / n := by have hmean_eq : ((∑ i, a i) / n - (∑ i, b i) / n) = (∑ i, (a i - b i)) / n := by rw [Finset.sum_sub_distrib, sub_div] rw [hmean_eq, sum_sub_mean_sq hnpos (fun j => a j - b j)] rw [hStau, hsumc, hsumc2] -- Expand the effect-sum moments in terms of `a`, `b` raw moments. have hsumab2 : (∑ j, (a j - b j) ^ 2) = (∑ j, a j ^ 2) - 2 * (∑ j, a j * b j) + (∑ j, b j ^ 2) := by have hpt : ∀ j, (a j - b j) ^ 2 = a j ^ 2 - 2 * (a j * b j) + b j ^ 2 := fun j => by ring simp only [hpt, Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.mul_sum] have hsumabsub : (∑ i, (a i - b i)) = (∑ i, a i) - (∑ i, b i) := Finset.sum_sub_distrib a b rw [hsumab2, hsumabsub, hvd, hvo] -- Pure field algebra over the five moment sums; verified symbolically. field_simp ring
theorem Var_tauHat_CRD reviewed
Causalean.Experimentation.TwoStageInterference

Hudgens–Halloran (2008), Theorem 5, for the completely randomized design. For a group of n units with potential outcomes a (treated state) and b (untreated state), consider the completely randomized within-group design that treats exactly K units uniformly at random, where K is positive and strictly less than the group size n. Then the randomization variance of the control-minus-treatment difference-in-means estimator under this design equals S₁/K + S₀/(n−K) − Sτ/n, where S₁ and S₀ are the population sample variances of the treated-state and untreated-state outcomes and is the population sample variance of the unit-level treatment effects.

Formal statement
hK :
0 < K
hKn :
K < n
(crd K hKn.le).Var (tauHat K a b) = S1 a / K + S0 b / (n - K) - Stau a b / n
Proof (Lean source)
theorem Var_tauHat_CRD (hK : 0 < K) (hKn : K < n) : (crd K hKn.le).Var (tauHat K a b) = S1 a / K + S0 b / (n - K) - Stau a b / n := Var_tauHat K a b (crd K hKn.le) hK hKn (fun j => crd_mean K hKn.le j) (fun j k hjk => crd_pair K hKn.le j k hjk)
Causalean.Experimentation.TwoStageInterference.Var_tauHat_CRD · Causalean/Experimentation/TwoStageInterference/Variance.lean:262 · uses Var , S0 , S1 , Stau , crd , tauHat
5 supporting declarations (lemmas, instances)
  • Var_add_const lemma — Variance is invariant under adding a constant: Var(X + c) = Var X.
    Ω :
    Type*
    D :
    X :
    Ω → ℝ
    c :
    D.Var (fun z => X z + c) = D.Var X
    Proof (Lean source)
    lemma FiniteDesign.Var_add_const {Ω : Type*} [Fintype Ω] (D : FiniteDesign Ω) (X : Ω → ℝ) (c : ℝ) : D.Var (fun z => X z + c) = D.Var X := by unfold FiniteDesign.Var have hE : D.E (fun z => X z + c) = D.E X + c := by rw [FiniteDesign.E_add, FiniteDesign.E_const] rw [hE] exact D.E_congr (fun z => by ring)
    Causalean.Experimentation.TwoStageInterference.FiniteDesign.Var_add_const · Causalean/Experimentation/TwoStageInterference/Variance.lean:57
  • sum_sum_ite_quadratic lemma — A double sum of cⱼ cₖ weighted by a two-valued kernel (vd on the diagonal, vo off it) collapses to vo·(∑ c)² + (vd − vo)·∑ c². This is the algebraic core that turns the Var_linear_comb double sum into the Neyman split form.
    α :
    Type*
    s :
    c :
    α → ℝ
    vd vo :
    (∑ j ∈ s, ∑ k ∈ s, c j * c k * (if j = k then vd else vo))
    = vo * (∑ j ∈ s, c j) ^ 2 + (vd - vo) * ∑ j ∈ s, (c j) ^ 2
    Proof (Lean source)
    lemma sum_sum_ite_quadratic {α : Type*} [DecidableEq α] (s : Finset α) (c : α → ℝ) (vd vo : ℝ) : (∑ j ∈ s, ∑ k ∈ s, c j * c k * (if j = k then vd else vo)) = vo * (∑ j ∈ s, c j) ^ 2 + (vd - vo) * ∑ j ∈ s, (c j) ^ 2 := by have hsplit : ∀ j k, c j * c k * (if j = k then vd else vo) = vo * (c j * c k) + (if j = k then (vd - vo) * (c j * c k) else 0) := by intro j k; by_cases h : j = k <;> simp [h] <;> ring simp only [hsplit, Finset.sum_add_distrib] congr 1 · rw [sq, Finset.sum_mul_sum, Finset.mul_sum] refine Finset.sum_congr rfl (fun i _ => ?_) rw [Finset.mul_sum] · rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun i hi => ?_) rw [Finset.sum_ite_eq s i (fun k => (vd - vo) * (c i * c k)), if_pos hi, sq]
    Causalean.Experimentation.TwoStageInterference.sum_sum_ite_quadratic · Causalean/Experimentation/TwoStageInterference/Variance.lean:67
  • sum_sub_mean_sq lemma — The sum of squared deviations equals the raw second moment minus the squared first moment divided by m: ∑ⱼ (xⱼ − x̄)² = ∑ⱼ xⱼ² − (∑ⱼ xⱼ)²/m, where x̄ = (∑ x)/m.
    m :
    hm :
    0 < m
    x :
    Fin m → ℝ
    (∑ j, (x j - (∑ i, x i) / m) ^ 2) = (∑ j, (x j) ^ 2) - (∑ i, x i) ^ 2 / m
    Proof (Lean source)
    lemma sum_sub_mean_sq {m : ℕ} (hm : 0 < m) (x : Fin m → ℝ) : (∑ j, (x j - (∑ i, x i) / m) ^ 2) = (∑ j, (x j) ^ 2) - (∑ i, x i) ^ 2 / m := by have hmne : (m : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hm.ne' have hcard : (∑ _j : Fin m, ((∑ i, x i) / m) ^ 2) = (∑ i, x i) ^ 2 / m := by rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp have hexp : ∀ j, (x j - (∑ i, x i) / m) ^ 2 = (x j) ^ 2 - 2 * ((∑ i, x i) / m) * (x j) + ((∑ i, x i) / m) ^ 2 := fun j => by ring simp only [hexp, Finset.sum_add_distrib, Finset.sum_sub_distrib] rw [hcard, ← Finset.mul_sum] field_simp ring
    Causalean.Experimentation.TwoStageInterference.sum_sub_mean_sq · Causalean/Experimentation/TwoStageInterference/Variance.lean:85
  • cov_diag lemma — The diagonal covariance Cov(Tⱼ, Tⱼ) = Var(Tⱼ) = (K/n)(1 − K/n).
    j :
    Fin n
    ρ.Cov (T j) (T j) = (K / n : ℝ) * (1 - K / n)
    Proof (Lean source)
    lemma cov_diag (j : Fin n) : ρ.Cov (T j) (T j) = (K / n : ℝ) * (1 - K / n) := by rw [FiniteDesign.Cov_self] simp only [T] rw [FiniteDesign.Var_ind] change ρ.E (T j) * (1 - ρ.E (T j)) = _ rw [hmean j]
    Causalean.Experimentation.TwoStageInterference.cov_diag · Causalean/Experimentation/TwoStageInterference/Variance.lean:145
  • cov_offdiag lemma — The off-diagonal covariance Cov(Tⱼ, Tₖ) = K(K−1)/(n(n−1)) − (K/n)² for j ≠ k.
    j k :
    Fin n
    hjk :
    j ≠ k
    ρ.Cov (T j) (T k) = (K * (K - 1) : ℝ) / (n * (n - 1)) - (K / n) * (K / n)
    Proof (Lean source)
    lemma cov_offdiag (j k : Fin n) (hjk : j ≠ k) : ρ.Cov (T j) (T k) = (K * (K - 1) : ℝ) / (n * (n - 1)) - (K / n) * (K / n) := by rw [FiniteDesign.Cov_eq, hpair j k hjk, hmean j, hmean k]
    Causalean.Experimentation.TwoStageInterference.cov_offdiag · Causalean/Experimentation/TwoStageInterference/Variance.lean:155
Between­Group 3 core · 0 supporting Two-stage population-mean variance decomposes into between-group and within-group terms. ★ Var_groupAgg★ Var_popEst★ Var_popEst_CRD

Two-stage between-group variance

Two-stage population-mean variance decomposes into between-group and within-group terms.

The abstract theorem Var_groupAgg proves the decomposition for any per-group statistic: an SRS between-group term over conditional means plus an averaged within-group conditional-variance term. Var_popEst instantiates it for the population estimator popEst, and Var_popEst_CRD specializes the result to the completely randomized mixed two-stage design, using the CRD inclusion and propensity lemmas rather than leaving those moments as assumptions.

theorem Var_groupAgg reviewed
Causalean.Experimentation.TwoStageInterference

Two-stage variance decomposition, abstract per-group statistic. For an arbitrary within-group allocation design ψ and comparison design φ and an arbitrary per-group statistic g, assume the selected-group count C is nonzero, the population has nonzero size and at least two groups, and that the stage-1 selection satisfies first-order inclusion probability C/N for every group and second-order (pairwise) inclusion probability C(C−1)/(N(N−1)) — the moments of a simple random sample of C of the N groups. Then the randomization variance of the aggregate (∑ᵢ 1(Sᵢ=ψ)·g i(wᵢ))/C under the two-stage design jointDesign D₁ ψ φ splits into a between-group SRS term with finite-population correction (1 − C/N)/C applied to the population sample variance of the conditional means (ψ i).E (g i), plus a within-group term (1/(C·N)) times the sum of the conditional variances (ψ i).Var (g i).

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
g :
∀ i
if
then
C :
hC :
C ≠ 0
hN :
(Fintype.card ι : ℝ) ≠ 0
hN1 :
(Fintype.card ι : ℝ) - 1 ≠ 0
hstage1 :
∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)
hstage1pair :
∀ i j
if
i ≠ j
then
D₁.E (fun s => FiniteDesign.ind (fun s => s i = true) s * FiniteDesign.ind (fun s => s j = true) s)
= (C * (C - 1)) / ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) - 1))
(jointDesign D₁ ψ φ).Var (fun sw => (∑ i, if sw.1 i = true then g i (sw.2 i) else 0) / C)
= (1 - C / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => (ψ i).E (g i))
+ (1 / (C * (Fintype.card ι : ℝ))) * ∑ i, (ψ i).Var (g i)
Proof (Lean source)
theorem Var_groupAgg (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (g : ∀ i, WAssign n i → ℝ) (C : ℝ) (hC : C ≠ 0) (hN : (Fintype.card ι : ℝ) ≠ 0) (hN1 : (Fintype.card ι : ℝ) - 1 ≠ 0) (hstage1 : ∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)) (hstage1pair : ∀ i j, i ≠ j → D₁.E (fun s => FiniteDesign.ind (fun s => s i = true) s * FiniteDesign.ind (fun s => s j = true) s) = (C * (C - 1)) / ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) - 1))) : (jointDesign D₁ ψ φ).Var (fun sw => (∑ i, if sw.1 i = true then g i (sw.2 i) else 0) / C) = (1 - C / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => (ψ i).E (g i)) + (1 / (C * (Fintype.card ι : ℝ))) * ∑ i, (ψ i).Var (g i) := by -- Step 0: law of total variance for the compound design. unfold jointDesign rw [FiniteDesign.Var_compound_eq_tower D₁ (fun s i => if s i then ψ i else φ i) (fun sw => (∑ i, if sw.1 i = true then g i (sw.2 i) else 0) / C)] rw [add_comm] congr 1 · -- BETWEEN term: collapse the conditional mean, then `Var_srs_mean`. rw [D₁.Var_congr (between_cond_mean_agg ψ φ g C)] rw [Var_srs_mean D₁ Usel (fun i => (ψ i).E (g i)) C ?_ ?_ ?_ hC hN1 hN] · -- hmean intro i; unfold Usel; rw [FiniteDesign.E_ind, hstage1 i] · -- hpair intro i j hij; unfold Usel; exact hstage1pair i j hij · -- hvar intro i; unfold Usel; rw [FiniteDesign.Var_ind, hstage1 i] · -- WITHIN term. exact within_term_agg D₁ ψ φ g C hC hN hstage1
theorem Var_popEst reviewed
Causalean.Experimentation.TwoStageInterference

Hudgens–Halloran (2008), Theorem 4 (two-stage variance decomposition of Ŷ(z;ψ)). For arbitrary within-group allocation designs ψ and comparison designs φ and potential outcomes Y, assume the treated/control unit counts m i are nonzero, the group sizes n i are nonzero, the population has nonzero size and at least two groups, the selected-group count C is nonzero, that the within-group z-propensity of every unit equals m i / n i, and that the stage-1 selection satisfies first-order inclusion probability C/N and second-order (pairwise) inclusion probability C(C−1)/(N(N−1)) — the moments of a simple random sample of C of the N groups, each then randomized by its within-group design. Then the randomization variance of the population estimator Ŷ(z;ψ) under the two-stage design jointDesign D₁ ψ φ splits into a between-group SRS term with finite-population correction (1 − C/N)/C applied to the population sample variance of the group-level potential outcomes ȳ_i(z;ψ), plus a within-group term (1/(C·N)) times the sum of the per-group conditional variances of the within-group estimator.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
z :
m :
ι → ℝ
C :
hC :
C ≠ 0
hm :
∀ i, m i ≠ 0
hn :
∀ i, (n i : ℝ) ≠ 0
hN :
(Fintype.card ι : ℝ) ≠ 0
hN1 :
(Fintype.card ι : ℝ) - 1 ≠ 0
hprop :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = z) = m i / (n i)
hstage1 :
∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)
hstage1pair :
∀ i j
if
i ≠ j
then
D₁.E (fun s => FiniteDesign.ind (fun s => s i = true) s * FiniteDesign.ind (fun s => s j = true) s)
= (C * (C - 1)) / ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) - 1))
(jointDesign D₁ ψ φ).Var (popEst Y z true m C)
= (1 - C / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean ψ Y i z)
+ (1 / (C * (Fintype.card ι : ℝ))) * ∑ i, (ψ i).Var (groupEst Y i z (m i))
Proof (Lean source)
theorem Var_popEst (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (z : Bool) (m : ι → ℝ) (C : ℝ) (hC : C ≠ 0) (hm : ∀ i, m i ≠ 0) (hn : ∀ i, (n i : ℝ) ≠ 0) (hN : (Fintype.card ι : ℝ) ≠ 0) (hN1 : (Fintype.card ι : ℝ) - 1 ≠ 0) (hprop : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = z) = m i / (n i)) (hstage1 : ∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)) (hstage1pair : ∀ i j, i ≠ j → D₁.E (fun s => FiniteDesign.ind (fun s => s i = true) s * FiniteDesign.ind (fun s => s j = true) s) = (C * (C - 1)) / ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) - 1))) : (jointDesign D₁ ψ φ).Var (popEst Y z true m C) = (1 - C / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean ψ Y i z) + (1 / (C * (Fintype.card ι : ℝ))) * ∑ i, (ψ i).Var (groupEst Y i z (m i)) := by -- `popEst` is the aggregate with `g i = groupEst Y i z (m i)`. have hpop : (popEst Y z true m C) = (fun sw => (∑ i, if sw.1 i = true then groupEst Y i z (m i) (sw.2 i) else 0) / C) := by funext sw; rfl rw [hpop, Var_groupAgg D₁ ψ φ (fun i => groupEst Y i z (m i)) C hC hN hN1 hstage1 hstage1pair] -- Collapse the between-term conditional means `(ψ i).E (groupEst…) = groupMean ψ Y i z`. have hmean : (fun i => (ψ i).E (groupEst Y i z (m i))) = (fun i => groupMean ψ Y i z) := by funext i; exact E_groupEst ψ Y i z (m i) (hm i) (hn i) (hprop i) rw [hmean]
theorem Var_popEst_CRD reviewed
Causalean.Experimentation.TwoStageInterference

Hudgens–Halloran (2008), Theorem 4, for the mixed two-stage design. For arbitrary potential outcomes Y, assume the selected-group count C is positive and strictly less than the number of groups, and that every group's treated-unit count K i is positive and strictly less than the group's size n i. Then, under the mixed two-stage design — stage 1 a simple random sample of C of the groups, each selected group i completely randomized to treat K i of its n i units — Var_popEst's between/within variance decomposition holds for the population estimator Ŷ(z; ·), with all of Var_popEst's design-moment hypotheses discharged by the completely-randomized design's inclusion and propensity facts.

Formal statement
Y :
∀ i
if
Fin (n i)
and
then
z :
K :
ι → ℕ
C :
hC0 :
0 < C
hCN :
C < Fintype.card ι
hK0 :
∀ i, 0 < K i
hKn :
∀ i, K i < n i
(jointDesign (crdOn C hCN.le) (fun i => crd (K i) (hKn i).le) (fun i => crd (K i) (hKn i).le)).Var (popEst Y z true (fun i => bif z then (K i : ℝ) else ((n i : ℝ) - K i)) (C : ℝ))
= (1 - (C : ℝ) / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean (fun i => crd (K i) (hKn i).le) Y i z)
+ (1 / ((C : ℝ) * (Fintype.card ι : ℝ))) * ∑ i, (crd (K i) (hKn i).le).Var (groupEst Y i z (bif z then (K i : ℝ) else ((n i : ℝ) - K i)))
Proof (Lean source)
theorem Var_popEst_CRD (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (z : Bool) (K : ι → ℕ) (C : ℕ) (hC0 : 0 < C) (hCN : C < Fintype.card ι) (hK0 : ∀ i, 0 < K i) (hKn : ∀ i, K i < n i) : (jointDesign (crdOn C hCN.le) (fun i => crd (K i) (hKn i).le) (fun i => crd (K i) (hKn i).le)).Var (popEst Y z true (fun i => bif z then (K i : ℝ) else ((n i : ℝ) - K i)) (C : ℝ)) = (1 - (C : ℝ) / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean (fun i => crd (K i) (hKn i).le) Y i z) + (1 / ((C : ℝ) * (Fintype.card ι : ℝ))) * ∑ i, (crd (K i) (hKn i).le).Var (groupEst Y i z (bif z then (K i : ℝ) else ((n i : ℝ) - K i))) := by have hCN' : (0 : ℝ) < Fintype.card ι := by exact_mod_cast lt_of_le_of_lt (zero_le C) hCN have hNr : (Fintype.card ι : ℝ) ≠ 0 := ne_of_gt hCN' have hN1r : (Fintype.card ι : ℝ) - 1 ≠ 0 := by have h2 : 2 ≤ Fintype.card ι := by omega have : (2 : ℝ) ≤ Fintype.card ι := by exact_mod_cast h2 linarith have hCr : (C : ℝ) ≠ 0 := by exact_mod_cast hC0.ne' have hnr : ∀ i, (n i : ℝ) ≠ 0 := fun i => by have h := hKn i; have : 0 < n i := by omega exact_mod_cast this.ne' have hmr : ∀ i, (bif z then (K i : ℝ) else ((n i : ℝ) - K i)) ≠ 0 := fun i => by cases z with | true => simpa using (by exact_mod_cast (hK0 i).ne' : (K i : ℝ) ≠ 0) | false => simp only [cond_false] exact sub_ne_zero.mpr (ne_of_gt (show (K i : ℝ) < n i by exact_mod_cast hKn i)) have hprop : ∀ i (j : Fin (n i)), (crd (K i) (hKn i).le).Pr (fun w => w j = z) = (bif z then (K i : ℝ) else ((n i : ℝ) - K i)) / n i := fun i j => by cases z with | true => simpa using crd_prop_true (K i) (hKn i).le j | false => simpa using crd_prop_false (K i) (hKn i).le j exact Var_popEst (crdOn C hCN.le) (fun i => crd (K i) (hKn i).le) (fun i => crd (K i) (hKn i).le) Y z (fun i => bif z then (K i : ℝ) else ((n i : ℝ) - K i)) (C : ℝ) hCr hmr hnr hNr hN1r hprop (fun i => crdOn_mean C hCN.le i) (fun i j hij => crdOn_pair C hCN.le i j hij)
Between­Group­Effect 2 core · 0 supporting The treatment-minus-control direct-effect contrast estimator has a two-stage between/within variance decomposition. ★ Var_estDirect★ Var_estDirect_CRD

Direct-contrast variance under two-stage interference

The treatment-minus-control direct-effect contrast estimator has a two-stage between/within variance decomposition.

The theorem Var_estDirect instantiates Var_groupAgg with the per-group treatment-minus-control statistic, yielding Hudgens-Halloran Theorem 6 under explicit stage-one and within-group moment hypotheses. Var_estDirect_CRD specializes the same identity to the completely randomized mixed two-stage design, where crdOn_mean, crdOn_pair, and the within-group crd_prop_* facts discharge those hypotheses.

theorem Var_estDirect reviewed
Causalean.Experimentation.TwoStageInterference

Hudgens–Halloran (2008), Theorem 6 (two-stage variance of the direct-effect contrast estimator). Consider the two-stage design that first allocates each group to strategy ψ or strategy φ and then randomizes the group's units accordingly, with outcomes recorded by the potential-outcome function Y. Assume the target sample size C of selected groups is nonzero, the number N of groups is nonzero, N minus one is nonzero, every group's control-arm unit count m0 is nonzero, every group's treatment-arm unit count m1 is nonzero, and every group's size n is nonzero. Suppose the stage-1 design draws a simple random sample of C of the N groups, so that each group is selected with probability C/N and each pair of distinct groups is jointly selected with probability C(C−1)/(N(N−1)), and that within a selected ψ-group each unit's control propensity is m0/n and each unit's treatment propensity is m1/n. Then the randomization variance of the treatment-minus-control estimator decomposes into a between-group term — the finite-population-corrected sample variance of the group-level treatment-minus-control contrasts, scaled by (1 − C/N)/C — plus a within-group term averaging, over the N groups and scaled by 1/(C·N), the conditional variance of each group's within-group contrast estimator.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
m0 m1 :
ι → ℝ
C :
hC :
C ≠ 0
hN :
(Fintype.card ι : ℝ) ≠ 0
hN1 :
(Fintype.card ι : ℝ) - 1 ≠ 0
hm0 :
∀ i, m0 i ≠ 0
hm1 :
∀ i, m1 i ≠ 0
hn :
∀ i, (n i : ℝ) ≠ 0
hprop0 :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = false) = m0 i / (n i)
hprop1 :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = true) = m1 i / (n i)
hstage1 :
∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)
hstage1pair :
∀ i j
if
i ≠ j
then
D₁.E (fun s => FiniteDesign.ind (fun s => s i = true) s * FiniteDesign.ind (fun s => s j = true) s)
= (C * (C - 1)) / ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) - 1))
(jointDesign D₁ ψ φ).Var (estDirect Y m0 m1 C)
= (1 - C / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean ψ Y i true - groupMean ψ Y i false)
+ (1 / (C * (Fintype.card ι : ℝ))) * ∑ i, (ψ i).Var (fun w => groupEst Y i true (m1 i) w - groupEst Y i false (m0 i) w)
Proof (Lean source)
theorem Var_estDirect (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (m0 m1 : ι → ℝ) (C : ℝ) (hC : C ≠ 0) (hN : (Fintype.card ι : ℝ) ≠ 0) (hN1 : (Fintype.card ι : ℝ) - 1 ≠ 0) (hm0 : ∀ i, m0 i ≠ 0) (hm1 : ∀ i, m1 i ≠ 0) (hn : ∀ i, (n i : ℝ) ≠ 0) (hprop0 : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = false) = m0 i / (n i)) (hprop1 : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = true) = m1 i / (n i)) (hstage1 : ∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)) (hstage1pair : ∀ i j, i ≠ j → D₁.E (fun s => FiniteDesign.ind (fun s => s i = true) s * FiniteDesign.ind (fun s => s j = true) s) = (C * (C - 1)) / ((Fintype.card ι : ℝ) * ((Fintype.card ι : ℝ) - 1))) : (jointDesign D₁ ψ φ).Var (estDirect Y m0 m1 C) = (1 - C / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean ψ Y i true - groupMean ψ Y i false) + (1 / (C * (Fintype.card ι : ℝ))) * ∑ i, (ψ i).Var (fun w => groupEst Y i true (m1 i) w - groupEst Y i false (m0 i) w) := by -- (a) The contrast estimator is the aggregate of the per-group contrast statistic. have hagg : (estDirect Y m0 m1 C) = (fun sw => (∑ i, if sw.1 i = true then (fun w => groupEst Y i true (m1 i) w - groupEst Y i false (m0 i) w) (sw.2 i) else 0) / C) := by funext sw unfold estDirect popEst rw [← sub_div] congr 1 rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) by_cases h : sw.1 i = true · rw [if_pos h, if_pos h, if_pos h] · rw [if_neg h, if_neg h, if_neg h, sub_zero] -- (b) Apply the abstract two-stage decomposition with `g i = dᵢ`. rw [hagg, Var_groupAgg D₁ ψ φ (fun i w => groupEst Y i true (m1 i) w - groupEst Y i false (m0 i) w) C hC hN hN1 hstage1 hstage1pair] -- (c) Collapse the between-term conditional means to the group-level contrasts. have hmean : (fun i => (ψ i).E (fun w => groupEst Y i true (m1 i) w - groupEst Y i false (m0 i) w)) = (fun i => groupMean ψ Y i true - groupMean ψ Y i false) := by funext i rw [FiniteDesign.E_sub (ψ i) (groupEst Y i true (m1 i)) (groupEst Y i false (m0 i))] rw [E_groupEst ψ Y i true (m1 i) (hm1 i) (hn i) (hprop1 i)] rw [E_groupEst ψ Y i false (m0 i) (hm0 i) (hn i) (hprop0 i)] rw [hmean]
theorem Var_estDirect_CRD reviewed
Causalean.Experimentation.TwoStageInterference

Hudgens–Halloran (2008), Theorem 6, for the mixed two-stage design. Consider the completely randomized two-stage design in which stage 1 draws a simple random sample of C groups out of the population of N groups, and each drawn group is completely randomized by treating K of its n units, with outcomes recorded by the potential-outcome function Y. Assume the sample size C is strictly positive, C is strictly less than the number N of groups, every group's treated-unit count K is strictly positive, and every group's treated count K is strictly less than its size n. Then the randomization variance of the treatment-minus-control estimator on this design equals the same between-group/within-group decomposition as Var_estDirect, with control count n−K and treatment count K in each group.

Formal statement
Y :
∀ i
if
Fin (n i)
and
then
K :
ι → ℕ
C :
hC0 :
0 < C
hCN :
C < Fintype.card ι
hK0 :
∀ i, 0 < K i
hKn :
∀ i, K i < n i
(jointDesign (crdOn C hCN.le) (fun i => crd (K i) (hKn i).le) (fun i => crd (K i) (hKn i).le)).Var (estDirect Y (fun i => (n i : ℝ) - K i) (fun i => (K i : ℝ)) (C : ℝ))
= (1 - (C : ℝ) / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean (fun i => crd (K i) (hKn i).le) Y i true - groupMean (fun i => crd (K i) (hKn i).le) Y i false)
+ (1 / ((C : ℝ) * (Fintype.card ι : ℝ))) * ∑ i, (crd (K i) (hKn i).le).Var (fun w => groupEst Y i true (K i : ℝ) w - groupEst Y i false ((n i : ℝ) - K i) w)
Proof (Lean source)
theorem Var_estDirect_CRD (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (K : ι → ℕ) (C : ℕ) (hC0 : 0 < C) (hCN : C < Fintype.card ι) (hK0 : ∀ i, 0 < K i) (hKn : ∀ i, K i < n i) : (jointDesign (crdOn C hCN.le) (fun i => crd (K i) (hKn i).le) (fun i => crd (K i) (hKn i).le)).Var (estDirect Y (fun i => (n i : ℝ) - K i) (fun i => (K i : ℝ)) (C : ℝ)) = (1 - (C : ℝ) / (Fintype.card ι : ℝ)) / C * SmuVar (fun i => groupMean (fun i => crd (K i) (hKn i).le) Y i true - groupMean (fun i => crd (K i) (hKn i).le) Y i false) + (1 / ((C : ℝ) * (Fintype.card ι : ℝ))) * ∑ i, (crd (K i) (hKn i).le).Var (fun w => groupEst Y i true (K i : ℝ) w - groupEst Y i false ((n i : ℝ) - K i) w) := by have hCN' : (0 : ℝ) < Fintype.card ι := by exact_mod_cast lt_of_le_of_lt (zero_le C) hCN have hNr : (Fintype.card ι : ℝ) ≠ 0 := ne_of_gt hCN' have hN1r : (Fintype.card ι : ℝ) - 1 ≠ 0 := by have h2 : 2 ≤ Fintype.card ι := by omega have : (2 : ℝ) ≤ Fintype.card ι := by exact_mod_cast h2 linarith have hCr : (C : ℝ) ≠ 0 := by exact_mod_cast hC0.ne' have hnr : ∀ i, (n i : ℝ) ≠ 0 := fun i => by have h := hKn i; have : 0 < n i := by omega exact_mod_cast this.ne' have hm0 : ∀ i, ((n i : ℝ) - K i) ≠ 0 := fun i => sub_ne_zero.mpr (ne_of_gt (show (K i : ℝ) < n i by exact_mod_cast hKn i)) have hm1 : ∀ i, (K i : ℝ) ≠ 0 := fun i => by exact_mod_cast (hK0 i).ne' have hprop0 : ∀ i (j : Fin (n i)), (crd (K i) (hKn i).le).Pr (fun w => w j = false) = ((n i : ℝ) - K i) / n i := fun i j => crd_prop_false (K i) (hKn i).le j have hprop1 : ∀ i (j : Fin (n i)), (crd (K i) (hKn i).le).Pr (fun w => w j = true) = (K i : ℝ) / n i := fun i j => crd_prop_true (K i) (hKn i).le j exact Var_estDirect (crdOn C hCN.le) (fun i => crd (K i) (hKn i).le) (fun i => crd (K i) (hKn i).le) Y (fun i => (n i : ℝ) - K i) (fun i => (K i : ℝ)) (C : ℝ) hCr hNr hN1r hm0 hm1 hnr hprop0 hprop1 (fun i => crdOn_mean C hCN.le i) (fun i j hij => crdOn_pair C hCN.le i j hij)
Effects 6 core · 0 supporting This file proves unbiasedness for the Hudgens-Halloran direct, indirect, and total effect estimators. ★ E_popEst_pick★ estIndirect★ estTotal★ E_estDirect★ E_estIndirect★ E_estTotal

Two-stage effect estimators and unbiasedness

This file proves unbiasedness for the Hudgens-Halloran direct, indirect, and total effect estimators. The main reusable step is population unbiasedness for either stage-one selection flag, which specializes to the ψ-selected and φ-selected groups used in the three causal-effect contrasts.

The theorem E_popEst_pick generalizes E_popEst to either stage-one flag. The definitions estIndirect and estTotal are the Horvitz-Thompson effect estimators built from the selected population estimators, and E_estDirect, E_estIndirect, and E_estTotal prove their exact finite-sample unbiasedness for CE_direct, CE_indirect, and CE_total.

theorem E_popEst_pick reviewed
Causalean.Experimentation.TwoStageInterference

Population unbiasedness, either selection (generalizing Theorem 1). For the two-stage design that allocates groups to strategy ψ or strategy φ and records outcomes via the potential-outcome function Y, fix an arbitrary selection flag pick together with a within-group design ρ meant to govern every group whose stage-1 flag equals pick, where on the event that a group's stage-1 flag equals pick, its conditional within-group design (ψ if flagged true, φ if flagged false) actually equals ρ. Assume the normalizing group count denom is nonzero, every group's unit count m at treatment level z is nonzero, and every group's size n is nonzero. Suppose that within each group governed by ρ each unit's propensity of being assigned treatment level z is m/n, and that the stage-1 design selects each group flagged pick with probability denom/N. Then the population estimator on the groups selected by pick is unbiased for the population average potential outcome at level z computed under design ρ.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
z :
m :
ι → ℝ
pick :
denom :
ρ :
∀ i, FiniteDesign (WAssign n i)
hdenom :
denom ≠ 0
hm :
∀ i, m i ≠ 0
hn :
∀ i, (n i : ℝ) ≠ 0
hcond :
∀ (s : StratAssign ι) (i : ι)
if
s i = pick
then
(if s i then ψ i else φ i) = ρ i
hprop :
∀ i, ∀ j : Fin (n i), (ρ i).Pr (fun w => w j = z) = m i / (n i)
hstage1 :
∀ i, D₁.Pr (fun s => s i = pick) = denom / (Fintype.card ι : ℝ)
(jointDesign D₁ ψ φ).E (popEst Y z pick m denom) = popMean ρ Y z
Proof (Lean source)
theorem E_popEst_pick (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (z : Bool) (m : ι → ℝ) (pick : Bool) (denom : ℝ) (ρ : ∀ i, FiniteDesign (WAssign n i)) (hdenom : denom ≠ 0) (hm : ∀ i, m i ≠ 0) (hn : ∀ i, (n i : ℝ) ≠ 0) (hcond : ∀ (s : StratAssign ι) (i : ι), s i = pick → (if s i then ψ i else φ i) = ρ i) (hprop : ∀ i, ∀ j : Fin (n i), (ρ i).Pr (fun w => w j = z) = m i / (n i)) (hstage1 : ∀ i, D₁.Pr (fun s => s i = pick) = denom / (Fintype.card ι : ℝ)) : (jointDesign D₁ ψ φ).E (popEst Y z pick m denom) = popMean ρ Y z := by unfold popEst popMean jointDesign have hEsum : (compound D₁ (fun s i => if s i then ψ i else φ i)).E (fun sw => (∑ i, if sw.1 i = pick then groupEst Y i z (m i) (sw.2 i) else 0) / denom) = (∑ i, groupMean ρ Y i z * (denom / (Fintype.card ι : ℝ))) / denom := by rw [show (fun sw : StratAssign ι × ∀ i, WAssign n i => (∑ i, if sw.1 i = pick then groupEst Y i z (m i) (sw.2 i) else 0) / denom) = (fun sw => denom⁻¹ * ∑ i, if sw.1 i = pick then groupEst Y i z (m i) (sw.2 i) else 0) from funext fun sw => by rw [div_eq_inv_mul]] rw [FiniteDesign.E_const_mul, FiniteDesign.E_sum, ← div_eq_inv_mul] congr 1 refine Finset.sum_congr rfl (fun i _ => ?_) -- per-group: E[1(S_i=pick)·Ŷ_i] = ȳ_i(z;ρ) · (denom/N) rw [(compound D₁ (fun s i => if s i then ψ i else φ i)).E_congr (popEst_summand_pick Y z m pick i)] rw [FiniteDesign.E_compound_factor D₁ (fun s i => if s i then ψ i else φ i) (FiniteDesign.ind (fun s : StratAssign ι => s i = pick)) i (groupEst Y i z (m i))] rw [show (fun s : StratAssign ι => FiniteDesign.ind (fun s => s i = pick) s * (if s i then ψ i else φ i).E (groupEst Y i z (m i))) = (fun s => FiniteDesign.ind (fun s => s i = pick) s * groupMean ρ Y i z) from ?_] · rw [FiniteDesign.E_mul_const, FiniteDesign.E_ind, hstage1 i]; ring · funext s unfold FiniteDesign.ind by_cases h : s i = pick · rw [if_pos h, one_mul, hcond s i h, E_groupEst ρ Y i z (m i) (hm i) (hn i) (hprop i), one_mul] · rw [if_neg h, zero_mul, zero_mul] have hcN : (denom / (Fintype.card ι : ℝ)) / denom = 1 / (Fintype.card ι : ℝ) := by rw [div_div, mul_comm (Fintype.card ι : ℝ) denom, ← div_div, div_self hdenom] rw [hEsum, ← Finset.sum_mul, mul_div_assoc, hcN, mul_one_div]
def estIndirect reviewed
Causalean.Experimentation.TwoStageInterference

The HT-effect estimator of the indirect (spillover) effect: Ŷ(0;φ) − Ŷ(0;ψ), the control-treatment population estimators on the φ-groups minus on the ψ-groups.

Definition (Lean source)
noncomputable def estIndirect (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (m0φ m0ψ : ι → ℝ) (dφ dψ : ℝ) (sw : StratAssign ι × ∀ i, WAssign n i) : ℝ := popEst Y false false m0φ dφ sw - popEst Y false true m0ψ dψ sw
Causalean.Experimentation.TwoStageInterference.estIndirect · Causalean/Experimentation/TwoStageInterference/Effects.lean:121 · uses StratAssign , WAssign
def estTotal reviewed
Causalean.Experimentation.TwoStageInterference

The HT-effect estimator of the total effect: Ŷ(0;φ) − Ŷ(1;ψ), the control-treatment population estimator on the φ-groups minus the treatment population estimator on the ψ-groups.

Definition (Lean source)
noncomputable def estTotal (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (m0φ m1ψ : ι → ℝ) (dφ dψ : ℝ) (sw : StratAssign ι × ∀ i, WAssign n i) : ℝ := popEst Y false false m0φ dφ sw - popEst Y true true m1ψ dψ sw
Causalean.Experimentation.TwoStageInterference.estTotal · Causalean/Experimentation/TwoStageInterference/Effects.lean:128 · uses StratAssign , WAssign
theorem E_estDirect reviewed
Causalean.Experimentation.TwoStageInterference

Direct-contrast unbiasedness (Theorem 1 contrast). For the two-stage design that allocates groups to strategy ψ or strategy φ and records outcomes via the potential-outcome function Y, assume the target sample size C of ψ-selected groups is nonzero, every group's control-arm unit count m0 is nonzero, every group's treatment-arm unit count m1 is nonzero, and every group's size n is nonzero. Suppose that within each group randomized by ψ each unit's control propensity is m0/n and each unit's treatment propensity is m1/n, and that the stage-1 design selects each group into the ψ arm with probability C/N. Then the Horvitz–Thompson estimator built from the ψ-selected groups is unbiased for the direct-effect contrast — the population average outcome under treatment minus under control, both evaluated under strategy ψ.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
m0 m1 :
ι → ℝ
C :
hC :
C ≠ 0
hm0 :
∀ i, m0 i ≠ 0
hm1 :
∀ i, m1 i ≠ 0
hn :
∀ i, (n i : ℝ) ≠ 0
hprop0 :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = false) = m0 i / (n i)
hprop1 :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = true) = m1 i / (n i)
hstage1ψ :
∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)
(jointDesign D₁ ψ φ).E (estDirect Y m0 m1 C) = CE_direct ψ Y
Proof (Lean source)
theorem E_estDirect (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (m0 m1 : ι → ℝ) (C : ℝ) (hC : C ≠ 0) (hm0 : ∀ i, m0 i ≠ 0) (hm1 : ∀ i, m1 i ≠ 0) (hn : ∀ i, (n i : ℝ) ≠ 0) (hprop0 : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = false) = m0 i / (n i)) (hprop1 : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = true) = m1 i / (n i)) (hstage1ψ : ∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)) : (jointDesign D₁ ψ φ).E (estDirect Y m0 m1 C) = CE_direct ψ Y := by unfold estDirect CE_direct rw [FiniteDesign.E_sub] rw [E_popEst_pick D₁ ψ φ Y true m1 true C ψ hC hm1 hn (fun s i hs => by simp [hs]) hprop1 hstage1ψ] rw [E_popEst_pick D₁ ψ φ Y false m0 true C ψ hC hm0 hn (fun s i hs => by simp [hs]) hprop0 hstage1ψ]
theorem E_estIndirect reviewed
Causalean.Experimentation.TwoStageInterference

Indirect-effect unbiasedness (Theorem 2 contrast). For the two-stage design that allocates groups to strategy ψ or strategy φ and records outcomes via the potential-outcome function Y, assume the target sample size dφ of φ-selected groups is nonzero, the target sample size dψ of ψ-selected groups is nonzero, every group's φ-arm control unit count m0φ is nonzero, every group's ψ-arm control unit count m0ψ is nonzero, and every group's size n is nonzero. Suppose that within each group randomized by φ each unit's control propensity is m0φ/n, that within each group randomized by ψ each unit's control propensity is m0ψ/n, that the stage-1 design selects each group into the φ arm with probability dφ/N, and that it selects each group into the ψ arm with probability dψ/N. Then the indirect-effect estimator is unbiased for the spillover contrast: the population average control outcome under φ minus the population average control outcome under ψ.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
m0φ m0ψ :
ι → ℝ
dφ dψ :
hdφ :
dφ ≠ 0
hdψ :
dψ ≠ 0
hm0φ :
∀ i, m0φ i ≠ 0
hm0ψ :
∀ i, m0ψ i ≠ 0
hn :
∀ i, (n i : ℝ) ≠ 0
hpropφ :
∀ i, ∀ j : Fin (n i), (φ i).Pr (fun w => w j = false) = m0φ i / (n i)
hpropψ :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = false) = m0ψ i / (n i)
hstage1φ :
∀ i, D₁.Pr (fun s => s i = false) = dφ / (Fintype.card ι : ℝ)
hstage1ψ :
∀ i, D₁.Pr (fun s => s i = true) = dψ / (Fintype.card ι : ℝ)
(jointDesign D₁ ψ φ).E (estIndirect Y m0φ m0ψ dφ dψ) = CE_indirect ψ φ Y
Proof (Lean source)
theorem E_estIndirect (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (m0φ m0ψ : ι → ℝ) (dφ dψ : ℝ) (hdφ : dφ ≠ 0) (hdψ : dψ ≠ 0) (hm0φ : ∀ i, m0φ i ≠ 0) (hm0ψ : ∀ i, m0ψ i ≠ 0) (hn : ∀ i, (n i : ℝ) ≠ 0) (hpropφ : ∀ i, ∀ j : Fin (n i), (φ i).Pr (fun w => w j = false) = m0φ i / (n i)) (hpropψ : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = false) = m0ψ i / (n i)) (hstage1φ : ∀ i, D₁.Pr (fun s => s i = false) = dφ / (Fintype.card ι : ℝ)) (hstage1ψ : ∀ i, D₁.Pr (fun s => s i = true) = dψ / (Fintype.card ι : ℝ)) : (jointDesign D₁ ψ φ).E (estIndirect Y m0φ m0ψ dφ dψ) = CE_indirect ψ φ Y := by unfold estIndirect CE_indirect rw [FiniteDesign.E_sub] rw [E_popEst_pick D₁ ψ φ Y false m0φ false dφ φ hdφ hm0φ hn (fun s i hs => by simp [hs]) hpropφ hstage1φ] rw [E_popEst_pick D₁ ψ φ Y false m0ψ true dψ ψ hdψ hm0ψ hn (fun s i hs => by simp [hs]) hpropψ hstage1ψ]
theorem E_estTotal reviewed
Causalean.Experimentation.TwoStageInterference

Total-effect unbiasedness (Theorem 3 contrast). For the two-stage design that allocates groups to strategy ψ or strategy φ and records outcomes via the potential-outcome function Y, assume the target sample size dφ of φ-selected groups is nonzero, the target sample size dψ of ψ-selected groups is nonzero, every group's φ-arm control unit count m0φ is nonzero, every group's ψ-arm treatment unit count m1ψ is nonzero, and every group's size n is nonzero. Suppose that within each group randomized by φ each unit's control propensity is m0φ/n, that within each group randomized by ψ each unit's treatment propensity is m1ψ/n, that the stage-1 design selects each group into the φ arm with probability dφ/N, and that it selects each group into the ψ arm with probability dψ/N. Then the total-effect estimator is unbiased for the contrast between the population average control outcome under φ and the population average treatment outcome under ψ.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
m0φ m1ψ :
ι → ℝ
dφ dψ :
hdφ :
dφ ≠ 0
hdψ :
dψ ≠ 0
hm0φ :
∀ i, m0φ i ≠ 0
hm1ψ :
∀ i, m1ψ i ≠ 0
hn :
∀ i, (n i : ℝ) ≠ 0
hpropφ :
∀ i, ∀ j : Fin (n i), (φ i).Pr (fun w => w j = false) = m0φ i / (n i)
hpropψ :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = true) = m1ψ i / (n i)
hstage1φ :
∀ i, D₁.Pr (fun s => s i = false) = dφ / (Fintype.card ι : ℝ)
hstage1ψ :
∀ i, D₁.Pr (fun s => s i = true) = dψ / (Fintype.card ι : ℝ)
(jointDesign D₁ ψ φ).E (estTotal Y m0φ m1ψ dφ dψ) = CE_total ψ φ Y
Proof (Lean source)
theorem E_estTotal (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (m0φ m1ψ : ι → ℝ) (dφ dψ : ℝ) (hdφ : dφ ≠ 0) (hdψ : dψ ≠ 0) (hm0φ : ∀ i, m0φ i ≠ 0) (hm1ψ : ∀ i, m1ψ i ≠ 0) (hn : ∀ i, (n i : ℝ) ≠ 0) (hpropφ : ∀ i, ∀ j : Fin (n i), (φ i).Pr (fun w => w j = false) = m0φ i / (n i)) (hpropψ : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = true) = m1ψ i / (n i)) (hstage1φ : ∀ i, D₁.Pr (fun s => s i = false) = dφ / (Fintype.card ι : ℝ)) (hstage1ψ : ∀ i, D₁.Pr (fun s => s i = true) = dψ / (Fintype.card ι : ℝ)) : (jointDesign D₁ ψ φ).E (estTotal Y m0φ m1ψ dφ dψ) = CE_total ψ φ Y := by unfold estTotal CE_total rw [FiniteDesign.E_sub] rw [E_popEst_pick D₁ ψ φ Y false m0φ false dφ φ hdφ hm0φ hn (fun s i hs => by simp [hs]) hpropφ hstage1φ] rw [E_popEst_pick D₁ ψ φ Y true m1ψ true dψ ψ hdψ hm1ψ hn (fun s i hs => by simp [hs]) hpropψ hstage1ψ]
Stratified 4 core · 2 supporting Stratified interference factors outcomes through own treatment and the count of treated peers. ★ exists_strat_factor

Stratified interference

Stratified interference factors outcomes through own treatment and the count of treated peers.

The grouped exposure summary is stratExpo, built from a unit's own treatment and numTreatedOthers. StratifiedInterference states Hudgens-Halloran Assumption 2 as invariance under equality of that exposure summary, StratifiedInterference.elim exposes the two raw conditions, and exists_strat_factor proves that any stratified-interference outcome function factors through the exposure map.

def numTreatedOthers reviewed
Causalean.Experimentation.TwoStageInterference

The number of units k ≠ j in group i that are treated under within-group assignment w (the count of other treated units relevant to unit j).

Definition (Lean source)
def numTreatedOthers (i : ι) (j : Fin (n i)) (w : WAssign n i) : ℕ := (Finset.univ.filter (fun k => k ≠ j ∧ w k = true)).card
Causalean.Experimentation.TwoStageInterference.numTreatedOthers · Causalean/Experimentation/TwoStageInterference/Stratified.lean:49 · uses WAssign
def stratExpo reviewed
Causalean.Experimentation.TwoStageInterference

The stratified-interference exposure of unit (i,j) under within-group assignment w: the pair of its own treatment w j and the number of other treated units in its group. This is the exposure summary through which outcomes are allowed to depend on the assignment.

Definition (Lean source)
def stratExpo (i : ι) (j : Fin (n i)) (w : WAssign n i) : Bool × ℕ := (w j, numTreatedOthers i j w)
Causalean.Experimentation.TwoStageInterference.stratExpo · Causalean/Experimentation/TwoStageInterference/Stratified.lean:54 · uses WAssign
def StratifiedInterference reviewed
Causalean.Experimentation.TwoStageInterference

Assumption 2 (stratified interference). A population of potential outcomes Y satisfies stratified interference when each unit's outcome depends on the within-group assignment only through its stratified exposure: whenever two assignments give a unit the same own treatment and the same count of treated others, the unit's outcome agrees.

Definition (Lean source)
def StratifiedInterference (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) : Prop := ∀ i (j : Fin (n i)) (w w' : WAssign n i), stratExpo i j w = stratExpo i j w' → Y i j w = Y i j w'
Causalean.Experimentation.TwoStageInterference.StratifiedInterference · Causalean/Experimentation/TwoStageInterference/Stratified.lean:60 · uses WAssign
theorem exists_strat_factor reviewed
Causalean.Experimentation.TwoStageInterference

Factorization through the exposure. Under stratified interference of the potential outcomes Y, there is a family g i j : Bool × ℕ → ℝ of exposure-indexed potential outcomes such that every outcome factors as Y i j w = g i j (stratExpo i j w).

Formal statement
Y :
∀ i
if
Fin (n i)
and
then
∃ g : ∀ i
if
Fin (n i)
and
(Bool × ℕ)
then
ℝ, ∀ i (j : Fin (n i)) (w : WAssign n i), Y i j w = g i j (stratExpo i j w)
Proof (Lean source)
theorem exists_strat_factor {Y : ∀ i, Fin (n i) → WAssign n i → ℝ} (h : StratifiedInterference Y) : ∃ g : ∀ i, Fin (n i) → (Bool × ℕ) → ℝ, ∀ i (j : Fin (n i)) (w : WAssign n i), Y i j w = g i j (stratExpo i j w) := by classical refine ⟨fun i j e => if he : ∃ w, stratExpo i j w = e then Y i j (choose he) else 0, ?_⟩ intro i j w have he : ∃ w', stratExpo i j w' = stratExpo i j w := stratExpo_exists i j w simp only [dif_pos he] exact (h i j w (choose he) (Classical.choose_spec he).symm)
Causalean.Experimentation.TwoStageInterference.exists_strat_factor · Causalean/Experimentation/TwoStageInterference/Stratified.lean:85 · uses StratifiedInterference , WAssign , stratExpo
2 supporting declarations (lemmas, instances)
Unbiased 3 core · 0 supporting Hudgens-Halloran within-group, population, and effect estimators are unbiased under known propensities. ★ E_groupEst★ E_popEst★ CE_total_decomp

Two-stage estimator unbiasedness

Hudgens-Halloran within-group, population, and effect estimators are unbiased under known propensities.

The theorem E_groupEst proves within-group unbiasedness from constant treatment propensities, and E_popEst lifts it through the compound design to population means on the ψ-selected groups. The file also records CE_total_decomp, the sign-convention identity relating the direct, indirect, and total contrasts used in this subtree.

theorem E_groupEst reviewed
Causalean.Experimentation.TwoStageInterference

Within-group unbiasedness. Fix a per-group design ρ governing the within-group treatment randomization and an outcome recorded for every group, unit, and realized within-group assignment, together with a group i, a treatment state z, and a nonzero real number m used as the treated-count denominator. Assume group i has a nonzero number of units and that every unit of group i receives treatment state z with the same probability m divided by the group's size. Then the expected value, under ρ, of the empirical mean outcome among the z-treated units of group i equals the group's average potential outcome under z.

Formal statement
ρ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
i :
ι
z :
m :
hm :
m ≠ 0
hn :
(n i : ℝ) ≠ 0
hprop :
∀ j : Fin (n i), (ρ i).Pr (fun w => w j = z) = m / (n i)
(ρ i).E (groupEst Y i z m) = groupMean ρ Y i z
Proof (Lean source)
theorem E_groupEst (ρ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (i : ι) (z : Bool) (m : ℝ) (hm : m ≠ 0) (hn : (n i : ℝ) ≠ 0) (hprop : ∀ j : Fin (n i), (ρ i).Pr (fun w => w j = z) = m / (n i)) : (ρ i).E (groupEst Y i z m) = groupMean ρ Y i z := by unfold groupEst groupMean have hLHS : (ρ i).E (fun w => (∑ j, if w j = z then Y i j w else 0) / m) = (∑ j, (ρ i).E (fun w => if w j = z then Y i j w else 0)) / m := by rw [show (fun w => (∑ j, if w j = z then Y i j w else 0) / m) = (fun w => m⁻¹ * ∑ j, if w j = z then Y i j w else 0) from funext fun w => by rw [div_eq_inv_mul]] rw [FiniteDesign.E_const_mul, FiniteDesign.E_sum, ← div_eq_inv_mul] have key : ∀ j : Fin (n i), indMean ρ Y i j z = (n i / m) * (ρ i).E (fun w => if w j = z then Y i j w else 0) := by intro j rw [indMean, hprop j, div_div_eq_mul_div, mul_div_assoc, mul_comm] rw [hLHS, Finset.sum_congr rfl (fun j _ => key j), ← Finset.mul_sum] field_simp
theorem E_popEst reviewed
Causalean.Experimentation.TwoStageInterference

Population unbiasedness (Theorem 1). Consider the two per-group designs ψ and φ governing the within-group randomization when a group is respectively assigned the ψ-strategy or the φ-strategy at stage 1 and an outcome recorded for every group, unit, and realized within-group assignment. Fix a treatment state z, a nonzero real number C used as the population-estimator denominator, and a family m with every group's value m i nonzero; suppose every group has a nonzero number of units, within every ψ-assigned group every unit receives treatment state z with the same probability m i divided by the group's size, and the marginal probability of each group being assigned the ψ-strategy at stage 1 equals C divided by the number of groups. Then the expected value, under the compound two-stage design, of the population estimator restricted to the ψ-assigned groups equals the population average potential outcome under z computed from the ψ-design.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
z :
m :
ι → ℝ
C :
hC :
C ≠ 0
hm :
∀ i, m i ≠ 0
hn :
∀ i, (n i : ℝ) ≠ 0
hprop :
∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = z) = m i / (n i)
hstage1 :
∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)
(jointDesign D₁ ψ φ).E (popEst Y z true m C) = popMean ψ Y z
Proof (Lean source)
theorem E_popEst (D₁ : FiniteDesign (StratAssign ι)) (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) (z : Bool) (m : ι → ℝ) (C : ℝ) (hC : C ≠ 0) (hm : ∀ i, m i ≠ 0) (hn : ∀ i, (n i : ℝ) ≠ 0) (hprop : ∀ i, ∀ j : Fin (n i), (ψ i).Pr (fun w => w j = z) = m i / (n i)) (hstage1 : ∀ i, D₁.Pr (fun s => s i = true) = C / (Fintype.card ι : ℝ)) : (jointDesign D₁ ψ φ).E (popEst Y z true m C) = popMean ψ Y z := by unfold popEst popMean jointDesign have hEsum : (compound D₁ (fun s i => if s i then ψ i else φ i)).E (fun sw => (∑ i, if sw.1 i = true then groupEst Y i z (m i) (sw.2 i) else 0) / C) = (∑ i, groupMean ψ Y i z * (C / (Fintype.card ι : ℝ))) / C := by rw [show (fun sw : StratAssign ι × ∀ i, WAssign n i => (∑ i, if sw.1 i = true then groupEst Y i z (m i) (sw.2 i) else 0) / C) = (fun sw => C⁻¹ * ∑ i, if sw.1 i = true then groupEst Y i z (m i) (sw.2 i) else 0) from funext fun sw => by rw [div_eq_inv_mul]] rw [FiniteDesign.E_const_mul, FiniteDesign.E_sum, ← div_eq_inv_mul] congr 1 refine Finset.sum_congr rfl (fun i _ => ?_) -- per-group: E[1(S_i=ψ)·Ŷ_i] = ȳ_i · (C/N) rw [(compound D₁ (fun s i => if s i then ψ i else φ i)).E_congr (popEst_summand Y z m i)] rw [FiniteDesign.E_compound_factor D₁ (fun s i => if s i then ψ i else φ i) (FiniteDesign.ind (fun s : StratAssign ι => s i = true)) i (groupEst Y i z (m i))] -- D₁.E (fun s => 1(s i) · (if s i then ψ i else φ i).E (groupEst...)) rw [show (fun s : StratAssign ι => FiniteDesign.ind (fun s => s i = true) s * (if s i then ψ i else φ i).E (groupEst Y i z (m i))) = (fun s => FiniteDesign.ind (fun s => s i = true) s * groupMean ψ Y i z) from ?_] · rw [FiniteDesign.E_mul_const, FiniteDesign.E_ind, hstage1 i]; ring · funext s unfold FiniteDesign.ind by_cases h : s i = true · simp only [h, if_true] rw [E_groupEst ψ Y i z (m i) (hm i) (hn i) (hprop i)] · simp [h] have hcN : (C / (Fintype.card ι : ℝ)) / C = 1 / (Fintype.card ι : ℝ) := by rw [div_div, mul_comm (Fintype.card ι : ℝ) C, ← div_div, div_self hC] rw [hEsum, ← Finset.sum_mul, mul_div_assoc, hcN, mul_one_div]
theorem CE_total_decomp reviewed
Causalean.Experimentation.TwoStageInterference

Mixed-orientation decomposition identity. For per-group two-stage designs ψ (treatment strategy) and φ (control strategy) governing each group's within-group assignment and an outcome recorded for every group, unit, and realized within-group assignment, the total contrast — the population control-state mean under φ minus the population treated-state mean under ψ — equals the indirect contrast — the population control-state mean under φ minus the population control-state mean under ψ — minus the direct contrast — the population treated-state mean under ψ minus the population control-state mean under ψ.

Formal statement
ψ φ :
∀ i, FiniteDesign (WAssign n i)
Y :
∀ i
if
Fin (n i)
and
then
CE_total ψ φ Y = CE_indirect ψ φ Y - CE_direct ψ Y
Proof (Lean source)
theorem CE_total_decomp (ψ φ : ∀ i, FiniteDesign (WAssign n i)) (Y : ∀ i, Fin (n i) → WAssign n i → ℝ) : CE_total ψ φ Y = CE_indirect ψ φ Y - CE_direct ψ Y := by unfold CE_total CE_direct CE_indirect ring
Variance­Conservative 10 core · 4 supporting Within-group sample-variance estimators conservatively estimate direct-effect randomization variance. ★ varHat_nonneg★ E_ShatTreated★ E_ShatControl★ E_varHat_conservative★ E_varHat_conservative_CRD

Conservative two-stage variance estimators

Within-group sample-variance estimators conservatively estimate direct-effect randomization variance.

The definitions obsMeanTreated, obsMeanControl, ShatTreated, ShatControl, and varHat describe the single-assignment sample-variance estimator. The theorem varHat_nonneg proves pointwise nonnegativity, E_ShatTreated and E_ShatControl identify the expected treated and control sample variances with S1 and S0, and E_varHat_conservative proves Var(tauHat) ≤ E[varHat]. E_varHat_conservative_CRD specializes that inequality to the completely randomized within-group design, where the moment and support hypotheses are proved by crd_mean, crd_pair, and crd_supp.

def obsMeanTreated reviewed
Causalean.Experimentation.TwoStageInterference

Empirical mean of the treated-state outcomes among the units observed treated under the realized assignment w: (1/K)∑_{j: wⱼ=1} a j, written with the treatment indicators.

Definition (Lean source)
noncomputable def obsMeanTreated (w : Fin n → Bool) : ℝ := (∑ j, T j w * a j) / K
Causalean.Experimentation.TwoStageInterference.obsMeanTreated · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:56
def obsMeanControl reviewed
Causalean.Experimentation.TwoStageInterference

Empirical mean of the untreated-state outcomes among the units observed in control under the realized assignment w: (1/(n−K))∑_{j: wⱼ=0} b j.

Definition (Lean source)
noncomputable def obsMeanControl (w : Fin n → Bool) : ℝ := (∑ j, (1 - T j w) * b j) / (n - K : ℝ)
Causalean.Experimentation.TwoStageInterference.obsMeanControl · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:61
def ShatTreated reviewed
Causalean.Experimentation.TwoStageInterference

Observed sample variance among the K treated units, Ŝ₁, with K−1 denominator: (1/(K−1))∑_{j: wⱼ=1}(a j − ā_obs)².

Definition (Lean source)
noncomputable def ShatTreated (w : Fin n → Bool) : ℝ := (∑ j, T j w * (a j - obsMeanTreated K a w) ^ 2) / (K - 1 : ℝ)
Causalean.Experimentation.TwoStageInterference.ShatTreated · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:66
def ShatControl reviewed
Causalean.Experimentation.TwoStageInterference

Observed sample variance among the n−K control units, Ŝ₀, with n−K−1 denominator: (1/(n−K−1))∑_{j: wⱼ=0}(b j − b̄_obs)².

Definition (Lean source)
noncomputable def ShatControl (w : Fin n → Bool) : ℝ := (∑ j, (1 - T j w) * (b j - obsMeanControl K b w) ^ 2) / (n - K - 1 : ℝ)
Causalean.Experimentation.TwoStageInterference.ShatControl · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:71
def varHat reviewed
Causalean.Experimentation.TwoStageInterference

Conservative variance estimator v̂ar = Ŝ₁/K + Ŝ₀/(n−K), the empirical analogue of the first two terms of the Neyman variance. Computable from a single realized assignment.

Definition (Lean source)
noncomputable def varHat (w : Fin n → Bool) : ℝ := ShatTreated K a w / K + ShatControl K b w / (n - K : ℝ)
Causalean.Experimentation.TwoStageInterference.varHat · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:76
theorem varHat_nonneg reviewed
Causalean.Experimentation.TwoStageInterference

Pointwise nonnegativity of the conservative variance estimator. For a group of n units with potential outcomes a and b, provided at least one unit is treated and at least one unit remains in control (K + 1 ≤ n) — so both within-group sample-variance denominators K and n − K are positive — then for every realized assignment w, the conservative variance estimator v̂ar is nonnegative, being the sum of two nonnegative sample variances each divided by a positive count.

Formal statement
hK :
1 ≤ K
hKn :
K + 1 ≤ n
w :
Fin n → Bool
0 ≤ varHat K a b w
Proof (Lean source)
theorem varHat_nonneg (hK : 1 ≤ K) (hKn : K + 1 ≤ n) (w : Fin n → Bool) : 0 ≤ varHat K a b w := by unfold varHat have hKpos : (0 : ℝ) < K := by have : (1 : ℝ) ≤ K := by exact_mod_cast hK linarith have hnKpos : (0 : ℝ) < n - K := by have h1 : (K : ℝ) + 1 ≤ n := by exact_mod_cast hKn linarith apply add_nonneg · exact div_nonneg (ShatTreated_nonneg K a hK w) hKpos.le · exact div_nonneg (ShatControl_nonneg K b hKn w) hnKpos.le
Causalean.Experimentation.TwoStageInterference.varHat_nonneg · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:107 · uses varHat
lemma E_ShatTreated reviewed
Causalean.Experimentation.TwoStageInterference

Expected observed treated sample variance. For any within-group design whose treatment indicators satisfy the completely-randomized moment hypotheses — first moment K/n (hmean), pairwise second moment K(K−1)/(n(n−1)) (hpair), and a deterministic treated count K on the support (hsupp) — the expectation of the realized treated-state sample variance equals the population treated-state sample variance S₁: E[Ŝ₁] = S₁.

Formal statement
ρ.E (ShatTreated K a) = S1 a
Proof (Lean source)
lemma E_ShatTreated : ρ.E (ShatTreated K a) = S1 a := by obtain ⟨hnr, hn1r, hKr, hK1r, _, _⟩ := denom_facts K hK2 hKn2 have hidem : ∀ (j : Fin n) (w : Fin n → Bool), T j w * T j w = T j w := by intro j w have := congrFun (FiniteDesign.ind_sq (fun w => w j = true)) w simpa [sq, T] using this -- ShatTreated K a unfolds to the `E_Shat` integrand with U = T, M = K. have hval := E_Shat ρ (K : ℝ) a T hnr hn1r hKr hK1r hidem hmean hpair hsupp unfold ShatTreated obsMeanTreated unfold S1 popMeanV exact hval
lemma E_ShatControl reviewed
Causalean.Experimentation.TwoStageInterference

Expected observed control sample variance. The control analogue: for any design satisfying the same completely-randomized moment hypotheses, the expectation of the realized untreated-state sample variance among the n−K control units equals the population untreated-state sample variance S₀: E[Ŝ₀] = S₀.

Formal statement
ρ.E (ShatControl K b) = S0 b
Proof (Lean source)
lemma E_ShatControl : ρ.E (ShatControl K b) = S0 b := by obtain ⟨hnr, hn1r, _, _, hnKr, hnK1r⟩ := denom_facts K hK2 hKn2 set U : Fin n → (Fin n → Bool) → ℝ := fun j w => 1 - T j w with hU -- idempotence of the control indicator have hidemT : ∀ (j : Fin n) (w : Fin n → Bool), T j w * T j w = T j w := by intro j w have := congrFun (FiniteDesign.ind_sq (fun w => w j = true)) w simpa [sq, T] using this have hidem : ∀ (j : Fin n) (w : Fin n → Bool), U j w * U j w = U j w := by intro j w; simp only [hU] rw [show (1 - T j w) * (1 - T j w) = 1 - 2 * T j w + T j w * T j w from by ring, hidemT j w]; ring -- first moment: E[1 − Tⱼ] = (n−K)/n have hmeanU : ∀ j, ρ.E (U j) = ((n - K : ℝ)) / n := by intro j have : U j = (fun w => 1 - T j w) := rfl rw [this] rw [show (fun w => (1 : ℝ) - T j w) = (fun w => (1 : ℝ) - T j w) from rfl] rw [FiniteDesign.E_sub, FiniteDesign.E_const, hmean j] field_simp -- pairwise second moment: E[(1−Tⱼ)(1−Tₖ)] = (n−K)(n−K−1)/(n(n−1)) have hpairU : ∀ j k, j ≠ k → ρ.E (fun w => U j w * U k w) = ((n - K : ℝ) * ((n - K : ℝ) - 1)) / (n * (n - 1)) := by intro j k hjk have hexp : (fun w => U j w * U k w) = (fun w => 1 - T j w - T k w + T j w * T k w) := by funext w; simp only [hU]; ring rw [hexp] rw [show (fun w => 1 - T j w - T k w + T j w * T k w) = (fun w => (1 - T j w - T k w) + (T j w * T k w)) from by funext w; ring] rw [FiniteDesign.E_add] rw [show (fun w => 1 - T j w - T k w) = (fun w => (1 - T j w) - T k w) from by funext w; ring] rw [FiniteDesign.E_sub, show (fun w => (1 : ℝ) - T j w) = (fun w => (1 : ℝ) - T j w) from rfl, FiniteDesign.E_sub, FiniteDesign.E_const, hmean j, hmean k, hpair j k hjk] field_simp ring -- support total: ∑ⱼ (1 − Tⱼ) = n − K on the support have hsuppU : ∀ w, ρ.p w ≠ 0 → (∑ j, U j w) = ((n - K : ℝ)) := by intro w hw simp only [hU] rw [Finset.sum_sub_distrib] rw [hsupp w hw] simp [Finset.card_univ] have hval := E_Shat ρ ((n : ℝ) - K) b U hnr hn1r hnKr hnK1r hidem hmeanU hpairU hsuppU -- bridge: M − 1 = (n−K) − 1, M = n−K unfold ShatControl obsMeanControl unfold S0 popMeanV simpa only [hU, sub_sub] using hval
theorem E_varHat_conservative reviewed
Causalean.Experimentation.TwoStageInterference

Conservativeness of the within-group variance estimator (Hudgens–Halloran 2008, Eq. 9). For any design satisfying the completely-randomized moment hypotheses (hmean/hpair/hsupp) and treating exactly K of n units (with 2 ≤ K and K + 2 ≤ n, so both sample variances are well defined), the conservative estimator overstates the randomization variance, Var(τ̂) ≤ E[v̂ar].

Formal statement
ρ.Var (tauHat K a b) ≤ ρ.E (varHat K a b)
Proof (Lean source)
theorem E_varHat_conservative : ρ.Var (tauHat K a b) ≤ ρ.E (varHat K a b) := by obtain ⟨hnr, hn1r, _, _, hnKr, _⟩ := denom_facts K hK2 hKn2 have hK : 0 < K := by omega have hKn : K < n := by omega -- E[v̂ar] = S₁/K + S₀/(n−K) have hEvar : ρ.E (varHat K a b) = S1 a / K + S0 b / (n - K) := by unfold varHat rw [show (fun w => ShatTreated K a w / K + ShatControl K b w / (n - K : ℝ)) = (fun w => ShatTreated K a w / K + ShatControl K b w / (n - K : ℝ)) from rfl, FiniteDesign.E_add] rw [show (fun w => ShatTreated K a w / (K : ℝ)) = (fun w => (K : ℝ)⁻¹ * ShatTreated K a w) from by funext w; rw [div_eq_mul_inv]; ring, show (fun w => ShatControl K b w / (n - K : ℝ)) = (fun w => (n - K : ℝ)⁻¹ * ShatControl K b w) from by funext w; rw [div_eq_mul_inv]; ring] rw [FiniteDesign.E_const_mul, FiniteDesign.E_const_mul, E_ShatTreated K a ρ hK2 hKn2 hmean hpair hsupp, E_ShatControl K b ρ hK2 hKn2 hmean hpair hsupp] rw [div_eq_mul_inv (S1 a), div_eq_mul_inv (S0 b)]; ring rw [hEvar, Var_tauHat K a b ρ hK hKn hmean hpair] -- Stau a b / n ≥ 0 (sum of squares over n−1 > 0, divided by n > 0) have hn4 : (4 : ℝ) ≤ n := by exact_mod_cast (by omega : 4 ≤ n) have hStau_nonneg : 0 ≤ Stau a b / n := by apply div_nonneg · unfold Stau apply div_nonneg · exact sum_nonneg (fun j _ => sq_nonneg _) · linarith · linarith linarith
Causalean.Experimentation.TwoStageInterference.E_varHat_conservative · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:228 · uses FiniteDesign , E , Var , T , tauHat , varHat
theorem E_varHat_conservative_CRD reviewed
Causalean.Experimentation.TwoStageInterference

Conservativeness of the within-group variance estimator, for the completely randomized design (Hudgens–Halloran 2008, Eq. 9). For a group of n units with potential outcomes a (treated state) and b (untreated state), consider the completely randomized within-group design that treats exactly K units uniformly at random, where at least two units are treated and at least two units remain in control (K + 2 ≤ n) — so both within-group sample variances are well defined. Then the randomization variance of the control-minus-treatment difference-in-means estimator under this design is at most the expectation, under the same design, of the conservative variance estimator v̂ar.

Formal statement
hK2 :
2 ≤ K
hKn2 :
K + 2 ≤ n
(crd K (le_trans (le_add_right K 2) hKn2)).Var (tauHat K a b)
≤ (crd K (le_trans (le_add_right K 2) hKn2)).E (varHat K a b)
Proof (Lean source)
theorem E_varHat_conservative_CRD (hK2 : 2 ≤ K) (hKn2 : K + 2 ≤ n) : (crd K (le_trans (le_add_right K 2) hKn2)).Var (tauHat K a b) ≤ (crd K (le_trans (le_add_right K 2) hKn2)).E (varHat K a b) := E_varHat_conservative K a b (crd K (le_trans (le_add_right K 2) hKn2)) hK2 hKn2 (fun j => crd_mean K _ j) (fun j k hjk => crd_pair K _ j k hjk) (fun w hw => crd_supp K _ w hw)
Causalean.Experimentation.TwoStageInterference.E_varHat_conservative_CRD · Causalean/Experimentation/TwoStageInterference/VarianceConservative.lean:271 · uses E , Var , crd , tauHat , varHat
4 supporting declarations (lemmas, instances)
Variance­Moments 1 core · 1 supporting Observed within-group sample variance has the correct finite-population expectation under fixed-count randomization with completely-randomized first and second moments. ★ E_Shat

Within-group sample-variance moments

Observed within-group sample variance has the correct finite-population expectation under fixed-count randomization with completely-randomized first and second moments.

The main lemma is E_Shat. For a {0,1}-valued selection family U with deterministic support total M, first moment M/n, and pairwise moment M(M-1)/(n(n-1)), it proves that the expected realized sample variance (1/(M-1)) * sum_j U_j * (x_j - xbar_U)^2 equals the population sample variance with denominator n-1. This paper-agnostic moment calculation is instantiated by the treated and control selection families in the Hudgens-Halloran two-stage-interference variance estimator. The support-congruence helper E_congr_supp lets the proof rewrite the statistic only on assignments that have positive design mass.

lemma E_Shat reviewed
Causalean.Experimentation.TwoStageInterference

Expectation of an observed sample variance. Let U be a {0,1}-valued selection family over a design ρ on length-n binary assignments, so that every Uⱼ is idempotent, taking only the values 0 and 1, and suppose the group size n and n − 1 are both nonzero, as are the real-valued selection count M and M − 1. If each Uⱼ has first moment M/n, every two distinct units j and k have second moment M(M−1)/(n(n−1)) for the product Uⱼ·Uₖ, and exactly M units are selected on every assignment the design gives positive weight, then the expectation of the realized sample variance of x over the selected units — (1/(M−1))∑ⱼ Uⱼ(xⱼ − x̄_U)² with x̄_U = (∑ Uⱼxⱼ)/M — equals the population sample variance (1/(n−1))∑ⱼ(xⱼ − x̄)².

Formal statement
ρ :
M :
x :
Fin n → ℝ
U :
Fin n → (Fin n → Bool) → ℝ
hnr :
(n : ℝ) ≠ 0
hn1r :
(n - 1 : ℝ) ≠ 0
hmr :
M ≠ 0
hm1r :
(M - 1 : ℝ) ≠ 0
hidem :
∀ j w, U j w * U j w = U j w
hmean :
∀ j, ρ.E (U j) = M / n
hpair :
∀ j k
if
j ≠ k
then
ρ.E (fun w => U j w * U k w) = (M * (M - 1) : ℝ) / (n * (n - 1))
hsupp :
∀ w
if
ρ.p w ≠ 0
then
(∑ j, U j w) = M
ρ.E (fun w => (∑ j, U j w * (x j - (∑ i, U i w * x i) / M) ^ 2) / (M - 1))
= (∑ j, (x j - (∑ i, x i) / n) ^ 2) / (n - 1)
Proof (Lean source)
lemma E_Shat (ρ : FiniteDesign (Fin n → Bool)) (M : ℝ) (x : Fin n → ℝ) (U : Fin n → (Fin n → Bool) → ℝ) (hnr : (n : ℝ) ≠ 0) (hn1r : (n - 1 : ℝ) ≠ 0) (hmr : M ≠ 0) (hm1r : (M - 1 : ℝ) ≠ 0) (hidem : ∀ j w, U j w * U j w = U j w) (hmean : ∀ j, ρ.E (U j) = M / n) (hpair : ∀ j k, j ≠ k → ρ.E (fun w => U j w * U k w) = (M * (M - 1) : ℝ) / (n * (n - 1))) (hsupp : ∀ w, ρ.p w ≠ 0 → (∑ j, U j w) = M) : ρ.E (fun w => (∑ j, U j w * (x j - (∑ i, U i w * x i) / M) ^ 2) / (M - 1)) = (∑ j, (x j - (∑ i, x i) / n) ^ 2) / (n - 1) := by -- Step 1: support-expansion of the numerator into raw moments. -- On the support, ∑ⱼ Uⱼ(xⱼ − m_U)² = (∑ⱼ Uⱼxⱼ²) − (∑ⱼ Uⱼxⱼ)²/M. have hnum : ρ.E (fun w => ∑ j, U j w * (x j - (∑ i, U i w * x i) / M) ^ 2) = ρ.E (fun w => (∑ j, U j w * x j ^ 2) - M⁻¹ * (∑ i, U i w * x i) ^ 2) := by refine E_congr_supp ρ (fun w hw => ?_) set S1w : ℝ := ∑ i, U i w * x i with hS1w -- expand the square (xⱼ − m_U)² = xⱼ² − 2 m_U xⱼ + m_U² have hexp : ∀ j, U j w * (x j - S1w / M) ^ 2 = U j w * x j ^ 2 - 2 * (S1w / M) * (U j w * x j) + (S1w / M) ^ 2 * U j w := by intro j; ring simp only [hexp, Finset.sum_add_distrib, Finset.sum_sub_distrib] -- pull the sum-independent factors out of the second and third sums rw [← Finset.mul_sum (Finset.univ : Finset (Fin n)) (fun j => U j w * x j) (2 * (S1w / M)), ← Finset.mul_sum (Finset.univ : Finset (Fin n)) (fun j => U j w) ((S1w / M) ^ 2)] -- ∑ⱼ Uⱼxⱼ = S1w, ∑ⱼ Uⱼ = M on support have hUx : (∑ j, U j w * x j) = S1w := rfl rw [hUx, hsupp w hw] field_simp ring rw [show (fun w => (∑ j, U j w * (x j - (∑ i, U i w * x i) / M) ^ 2) / (M - 1)) = (fun w => (∑ j, U j w * (x j - (∑ i, U i w * x i) / M) ^ 2) * ((M - 1)⁻¹)) from by funext w; rw [div_eq_mul_inv]] rw [FiniteDesign.E_mul_const, hnum, FiniteDesign.E_sub, FiniteDesign.E_const_mul] -- Step 2: the two raw-moment expectations. -- E[∑ⱼ Uⱼxⱼ²] = (m/n)∑ⱼxⱼ². have hE1 : ρ.E (fun w => ∑ j, U j w * x j ^ 2) = (M / n : ℝ) * ∑ j, x j ^ 2 := by rw [FiniteDesign.E_sum] rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun j _ => ?_) rw [FiniteDesign.E_mul_const, hmean j] -- E[(∑ⱼ Uⱼxⱼ)²] = (m/n)∑xⱼ² + m(m−1)/(n(n−1)) · ((∑x)² − ∑x²). have hE2 : ρ.E (fun w => (∑ i, U i w * x i) ^ 2) = (M / n : ℝ) * (∑ j, x j ^ 2) + (M * (M - 1) : ℝ) / (n * (n - 1)) * ((∑ j, x j) ^ 2 - ∑ j, x j ^ 2) := by -- expand the square into a double sum have hsq : ∀ w, (∑ i, U i w * x i) ^ 2 = ∑ j, ∑ k, (x j * x k) * (U j w * U k w) := by intro w rw [sq, Finset.sum_mul_sum] refine Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => by ring)) simp only [hsq] rw [FiniteDesign.E_sum] -- now ∑ⱼ E[∑ₖ (xⱼxₖ)(Uⱼ Uₖ)] have hinner : ∀ j, ρ.E (fun w => ∑ k, (x j * x k) * (U j w * U k w)) = ∑ k, (x j * x k) * ρ.E (fun w => U j w * U k w) := by intro j rw [FiniteDesign.E_sum] refine Finset.sum_congr rfl (fun k _ => ?_) rw [FiniteDesign.E_const_mul] simp only [hinner] -- split the inner sum at the diagonal k = j have hdiag : ∀ j, ρ.E (fun w => U j w * U j w) = (M / n : ℝ) := by intro j rw [show (fun w => U j w * U j w) = U j from by funext w; rw [hidem j w]] exact hmean j have hsplit : ∀ j, (∑ k, (x j * x k) * ρ.E (fun w => U j w * U k w)) = (x j ^ 2) * (M / n : ℝ) + (M * (M - 1) : ℝ) / (n * (n - 1)) * (x j * (∑ k, x k) - x j ^ 2) := by intro j rw [← Finset.sum_erase_add _ _ (Finset.mem_univ j)] rw [hdiag j] -- off-diagonal terms use hpair have hoff : (∑ k ∈ Finset.univ.erase j, (x j * x k) * ρ.E (fun w => U j w * U k w)) = (M * (M - 1) : ℝ) / (n * (n - 1)) * (∑ k ∈ Finset.univ.erase j, x j * x k) := by rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun k hk => ?_) have hjk : j ≠ k := (Finset.ne_of_mem_erase hk).symm rw [hpair j k hjk]; ring rw [hoff] -- ∑_{k≠j} xⱼxₖ = xⱼ(∑x) − xⱼxⱼ have herase : (∑ k ∈ Finset.univ.erase j, x j * x k) = x j * (∑ k, x k) - x j * x j := by rw [← Finset.mul_sum, ← Finset.sum_erase_add _ _ (Finset.mem_univ j)] ring rw [herase]; ring simp only [hsplit, Finset.sum_add_distrib] rw [← Finset.sum_mul, ← Finset.mul_sum] -- ∑ⱼ xⱼ(∑x) − xⱼ² = (∑x)² − ∑x² have hcollapse : (∑ j, (x j * (∑ k, x k) - x j ^ 2)) = (∑ j, x j) ^ 2 - ∑ j, x j ^ 2 := by rw [Finset.sum_sub_distrib, ← Finset.sum_mul] congr 1 rw [sq] rw [hcollapse] ring rw [hE1, hE2] -- Step 3: algebra collapses E[num]·(m−1)⁻¹ to the population sample variance. rw [sum_sub_mean_sq (by rcases Nat.eq_zero_or_pos n with h | h · simp [h] at hnr · exact h) x] -- Let P = ∑x², Q = (∑x)². Goal is a pure field identity in P, Q, n, m. set P : ℝ := ∑ j, x j ^ 2 set Q : ℝ := (∑ j, x j) ^ 2 field_simp ring
Causalean.Experimentation.TwoStageInterference.E_Shat · Causalean/Experimentation/TwoStageInterference/VarianceMoments.lean:64 · uses FiniteDesign , E
1 supporting declaration (lemmas, instances)
  • E_congr_supp lemma — Support congruence for expectation. Two random variables that agree on every assignment the design gives positive weight have equal expectation, since the off-support assignments contribute 0 = p w · _ to the finite sum either way.
    ρ :
    f g :
    (Fin n → Bool) → ℝ
    h :
    ∀ w
    if
    ρ.p w ≠ 0
    then
    f w = g w
    ρ.E f = ρ.E g
    Proof (Lean source)
    lemma E_congr_supp (ρ : FiniteDesign (Fin n → Bool)) {f g : (Fin n → Bool) → ℝ} (h : ∀ w, ρ.p w ≠ 0 → f w = g w) : ρ.E f = ρ.E g := by unfold FiniteDesign.E refine Finset.sum_congr rfl (fun w _ => ?_) by_cases hw : ρ.p w = 0 · rw [hw]; ring · rw [h w hw]
    Causalean.Experimentation.TwoStageInterference.E_congr_supp · Causalean/Experimentation/TwoStageInterference/VarianceMoments.lean:53