Experimentation.TwoStageInterference
Formalization of Hudgens & Halloran (2008), "Toward Causal Inference With Interference" (JASA), building on the paper-agnostic design-based substrate Experimentation.DesignBased.
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.
Within-group assignment space for group i: a {treated/untreated} flag per unit.
Stage-1 strategy assignment space: each group is flagged ψ (true) or φ (false).
Definition (Lean source)
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)
Individual average potential outcome ȳ_ij(z;ρ): unit (i,j)'s expected outcome under within-group design ρ, conditional on its own treatment being z.
Group average potential outcome ȳ_i(z;ρ) = (1/nᵢ)∑ⱼ ȳ_ij(z;ρ).
Population average potential outcome ȳ(z;ρ) = (1/N)∑ᵢ ȳ_i(z;ρ).
Marginal individual average potential outcome ȳ_ij(ρ): expected outcome of (i,j) under design ρ, averaging over its own treatment as well (the overall-effect target).
Population marginal average potential outcome ȳ(ρ) = (1/N)∑ᵢ(1/nᵢ)∑ⱼ ȳ_ij(ρ).
Hudgens-Halloran direct-effect contrast. This is the population average outcome under treatment minus the population average outcome under control, evaluated under the strategy ψ.
Indirect (spillover) causal effect C̄E^I(φ,ψ) = ȳ(0;φ) − ȳ(0;ψ).
Definition (Lean source)
Total causal effect C̄E^T(φ,ψ) = ȳ(0;φ) − ȳ(1;ψ).
Overall causal effect C̄E^O(φ,ψ) = ȳ(φ) − ȳ(ψ).
Definition (Lean source)
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.
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.
The Horvitz-Thompson estimator of the treatment-minus-control direct-effect contrast on the ψ-groups: the estimated treatment mean minus the estimated control mean.
CompleteRandomization 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.
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)
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)
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
Proof (Lean source)
The within-group treated-set-to-indicator map (specialization of crdToBoolOn to Fin n).
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)
8 supporting declarations (lemmas, instances)
-
crdOn_meanlemma — First-order inclusion probability: each unit i is treated with probability K/N, i.e. E[Tᵢ] = K/N. Derived from completeRandomization_incl.hypothesesi :UProof (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] -
crdOn_mean_compllemma — 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ᵢ.hypothesesi :UProof (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 -
crdOn_supplemma — Deterministic treated count on the design's support: any assignment with positive design weight treats exactly K units, i.e. ∑ᵢ Tᵢ = K.hypothesesconclusion(∑ 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 -
crd_meanlemma — First-order inclusion probability of the within-group design: E[Tⱼ] = K/n. -
crd_pairlemma — Second-order inclusion probability of the within-group design: E[Tⱼ Tₖ] = K(K−1)/(n(n−1)) for j ≠ k.hypothesesj k :Fin nhjk :j ≠ k -
crd_supplemma — Deterministic treated count on the within-group design's support: ∑ⱼ Tⱼ = K.hypothesesconclusion(∑ j, (FiniteDesign.ind fun w => w j = true) w) = (K : ℝ) -
crd_prop_truelemma — Treatment propensity of the within-group design: each unit j is treated with probability K/n, i.e. Pr[wⱼ = true] = K/n. -
crd_prop_falselemma — 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.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]
StageOne 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.
The population sample variance (Neyman N−1 denominator) of the group-level quantities μ, Sμ² = (∑ᵢ(μᵢ − μ̄)²)/(N−1), where N := card ι and μ̄ = (∑ μ)/N.
Definition (Lean source)
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
Proof (Lean source)
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.
Treatment indicator of unit j: 1 on within-group assignments that treat j, 0 otherwise. (The indicator does not depend on the design.)
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.
Population mean of a unit-indexed quantity: (1/n)∑ⱼ x j.
Population sample variance of the treated-state outcomes a, S₁ = (1/(n−1))∑ⱼ(a j − ā)².
Definition (Lean source)
Population sample variance of the untreated-state outcomes b, S₀ = (1/(n−1))∑ⱼ(b j − b̄)².
Definition (Lean source)
Population sample variance of the unit-level treatment effects a j − b j, Sτ = (1/(n−1))∑ⱼ((a j − b j) − (ā − b̄))².
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.
Proof (Lean source)
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 Sτ is the population sample variance of the unit-level treatment effects.
Formal statement
5 supporting declarations (lemmas, instances)
-
Var_add_constlemma — Variance is invariant under adding a constant: Var(X + c) = Var X.hypothesesconclusionD.Var (fun z => X z + c) = D.Var XProof (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) -
sum_sum_ite_quadraticlemma — 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.hypothesesconclusion(∑ 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) ^ 2Proof (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] -
sum_sub_mean_sqlemma — 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.hypothesesconclusion(∑ j, (x j - (∑ i, x i) / m) ^ 2) = (∑ j, (x j) ^ 2) - (∑ i, x i) ^ 2 / mProof (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 -
cov_diaglemma — The diagonal covariance Cov(Tⱼ, Tⱼ) = Var(Tⱼ) = (K/n)(1 − K/n). -
cov_offdiaglemma — The off-diagonal covariance Cov(Tⱼ, Tₖ) = K(K−1)/(n(n−1)) − (K/n)² for j ≠ k.hypothesesj k :Fin nhjk :j ≠ kconclusionρ.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]
BetweenGroup 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.
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
Proof (Lean source)
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
Proof (Lean source)
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
Proof (Lean source)
BetweenGroupEffect 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.
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
Proof (Lean source)
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
Proof (Lean source)
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.
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
Proof (Lean source)
The HT-effect estimator of the indirect (spillover) effect: Ŷ(0;φ) − Ŷ(0;ψ), the control-treatment population estimators on the φ-groups minus on the ψ-groups.
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.
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
Proof (Lean source)
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
Proof (Lean source)
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
Proof (Lean source)
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.
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)
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)
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.
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
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
elimlemma — Restatement of stratified interference in terms of the two raw summaries: equal own treatment and equal count of treated others force equal outcomes.hypothesesh :i :ιj :Fin (n i)w w' :WAssign n ihown :w j = w' jhcount :numTreatedOthers i j w = numTreatedOthers i j w'conclusionY i j w = Y i j w'Proof (Lean source)
lemma StratifiedInterference.elim {Y : ∀ i, Fin (n i) → WAssign n i → ℝ} (h : StratifiedInterference Y) (i : ι) (j : Fin (n i)) (w w' : WAssign n i) (hown : w j = w' j) (hcount : numTreatedOthers i j w = numTreatedOthers i j w') : Y i j w = Y i j w' := h i j w w' (by rw [stratExpo, stratExpo, hown, hcount]) -
stratExpo_existslemma — The exposure summary of unit (i,j) is always realized — namely by w itself; so every stratified exposure value reachable from some assignment has a witnessing assignment.Proof (Lean source)
lemma stratExpo_exists (i : ι) (j : Fin (n i)) (w : WAssign n i) : ∃ w', stratExpo i j w' = stratExpo i j w := ⟨w, rfl⟩
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.
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
Proof (Lean source)
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
Proof (Lean source)
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
Proof (Lean source)
VarianceConservative 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.
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)
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)
Observed sample variance among the K treated units, Ŝ₁, with K−1 denominator: (1/(K−1))∑_{j: wⱼ=1}(a j − ā_obs)².
Definition (Lean source)
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)
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)
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
Proof (Lean source)
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
Proof (Lean source)
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
Proof (Lean source)
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].
Proof (Lean source)
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
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
ShatTreated_nonneglemma — The observed treated sample variance is nonnegative, provided 1 ≤ K (so the denominator K−1 ≥ 0): it is a nonnegative-weighted sum of squares divided by a nonnegative number.Proof (Lean source)
lemma ShatTreated_nonneg (hK : 1 ≤ K) (w : Fin n → Bool) : 0 ≤ ShatTreated K a w := by unfold ShatTreated apply div_nonneg · exact sum_nonneg (fun j _ => mul_nonneg (T_nonneg j w) (sq_nonneg _)) · have : (1 : ℝ) ≤ K := by exact_mod_cast hK linarith -
ShatControl_nonneglemma — The observed control sample variance is nonnegative, provided K + 1 ≤ n (so the denominator n−K−1 ≥ 0).Proof (Lean source)
lemma ShatControl_nonneg (hKn : K + 1 ≤ n) (w : Fin n → Bool) : 0 ≤ ShatControl K b w := by unfold ShatControl apply div_nonneg · exact sum_nonneg (fun j _ => mul_nonneg (one_sub_T_nonneg j w) (sq_nonneg _)) · have : (K : ℝ) + 1 ≤ n := by exact_mod_cast hKn linarith
VarianceMoments 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.
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
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
E_congr_supplemma — 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.hypothesesconclusionρ.E f = ρ.E gProof (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]