Experimentation.TwoStageInterference.Asymptotic
Asymptotic theory for two-stage interference experiments: setup, consistency, CLT discharge, studentized direct effects, and Wald intervals.
Setup 7 core · 0 supporting LHExperiment packages one Hudgens-Halloran two-stage experiment for Liu-Hudgens large-sample inference on the treatment-minus-control direct-effect contrast. ★ LHExperiment★ E_estD★ var_estD
Liu-Hudgens asymptotic setup
LHExperiment packages one Hudgens-Halloran two-stage experiment for Liu-Hudgens large-sample
inference on the treatment-minus-control direct-effect contrast.
The structure carries the group population, group sizes, stage-1 strategy design, within-group
strategies ψ and φ, partial-interference potential outcomes, fixed treated/control counts,
the number C of ψ-selected groups, and the known design propensities needed by the finite-sample
unbiasedness and variance theorems. Its namespace defines the joint two-stage design jointD, the
Horvitz-Thompson direct-effect estimator estD, the estimand DEbar, and the closed-form variance
directVar.
The main theorems are the reusable bridges E_estD and var_estD: they specialize the
finite-sample Hudgens-Halloran unbiasedness and variance results to each packaged experiment, so
later consistency, CLT, and Wald arguments can reason through LHExperiment alone.
A single Liu–Hudgens (2014) two-stage experiment, packaged so that a sequence of them can be studied for large-sample inference. Carries a finite population of groups with per-group sizes, a stage-1 design assigning each group a strategy, the per-group allocation strategies ψ and φ, partial-interference potential outcomes, and design-fixed control and treatment unit counts per group, together with the regularity conditions that the number C of ψ-selected groups is nonzero, every group has nonzero control and treatment counts and nonzero size, the population has at least one group and at least two groups, every unit's within-group control propensity equals m0 i / nᵢ and its treatment propensity equals m1 i / nᵢ, every group's stage-1 selection propensity equals C/N, and every pair's joint selection propensity equals C(C−1)/(N(N−1)) — exactly the hypothesis lists of E_estDirect and Var_estDirect.
Definition (Lean source)
For a Liu--Hudgens experiment, the joint two-stage randomization design first draws the group-level strategy assignment and then draws each group's within-group assignment from the design corresponding to its assigned strategy.
Definition (Lean source)
For a Liu--Hudgens experiment, the Horvitz--Thompson estimator of its treatment-minus-control direct effect assigns a real-valued estimate to every joint realization of the group-level strategy assignment and all within-group assignments.
Definition (Lean source)
For a Liu--Hudgens experiment, the population-average treatment-minus-control direct effect is the mean potential outcome under treatment minus the mean potential outcome under control, with both means evaluated under the experiment's treatment strategy.
Definition (Lean source)
For a Liu--Hudgens experiment, the closed-form two-stage design variance of the treatment-minus-control direct-effect estimator equals , where is the number of groups, is the number assigned the treatment strategy, is the population sample variance of the group-level direct-effect contrasts, and is the variance of group 's within-group contrast estimator under the treatment strategy.
Definition (Lean source)
Unbiasedness bridge. The Horvitz–Thompson estimator is unbiased for the population average treatment-minus-control direct-effect contrast.
Formal statement
Proof (Lean source)
Variance bridge. The design variance of the treatment-minus-control direct-effect contrast estimator equals the closed-form two-stage variance directVar.
Formal statement
Proof (Lean source)
CLTDischarge 8 core · 8 supporting This file develops the conditional-design ingredients for a central limit theorem for the studentized direct-effect estimator in homogeneous two-stage interference experiments. ★ DEbar_eq_of_homogeneous★ directVar_eq_of_homogeneous★ stud_eq_sum_of_homogeneous
Ingredients for the homogeneous two-stage central limit theorem
This file develops the conditional-design ingredients for a central limit theorem for the studentized direct-effect estimator in homogeneous two-stage interference experiments. It defines group-level contrasts, conditional assignment designs, normalized summands, and a reference selection, and derives the estimand and variance reductions needed for the final asymptotic result.
For a Liu--Hudgens experiment, one of its groups, and a within-group treatment assignment, the per-group treatment-minus-control direct-effect estimator is the treated-strategy group estimator minus the control-strategy group estimator.
For a Liu--Hudgens experiment and a stage-one strategy assignment, the conditional stage-two design independently assigns each group according to its treatment design when that group is assigned treatment and according to its control design otherwise.
Definition (Lean source)
Homogeneity and regularity bundle for a sequence of Liu–Hudgens experiments. Faithfully encodes the hypotheses of Proposition 5.1 for the Hudgens-Halloran orientation: the studentized statistic is the standardized contrast estimator; every group-level direct-effect contrast equals a common value δ (homogeneity); every within-group contrast-estimator variance equals a common value v(n) that is positive; the centered per-group contrast estimator is uniformly bounded; every stage-1 selection supported by the design flags exactly C groups; the resulting rate sequence tends to zero together with its cubed Lyapunov rate (the many-groups asymptotic regime); and the conditional distribution of the studentized statistic does not depend on which stage-1 selection occurred, the analytic form of homogeneity that lifts the conditional CLT to the average.
Definition (Lean source)
Estimand reduction. Under the homogeneity and regularity bundle, the population average treatment-minus-control direct-effect contrast collapses to the common group-level contrast δ.
Formal statement
Proof (Lean source)
Variance reduction. Under the homogeneity and regularity bundle, the two-stage design variance of the direct-effect contrast collapses to v n / C: the between-group term vanishes since the population variance of a constant is zero, and the within-group term averages to v n / C.
Formal statement
Proof (Lean source)
For a sequence of Liu--Hudgens experiments, an experiment index , a common group-level contrast , a sequence of within-group variances, a stage-one strategy assignment, a group, and that group's within-group treatment assignment, the scaled per-coordinate summand of the conditional studentized statistic is the selected-group indicator times the centered group contrast estimator, divided by .
Definition (Lean source)
Studentized = independent sum. For a stage-1 stratified assignment s that the design supports with positive probability, then, under homogeneity, for every within-group assignment pattern w, the conditional studentized statistic decomposes as the normalized independent sum stud(s,w) = ∑ᵢ cltSummand n δ v s i (w i).
Formal statement
Proof (Lean source)
For a sequence of Liu--Hudgens experiments and an experiment index , the reference stage-one selection is a fixed strategy assignment having positive probability under that experiment's stage-one design.
Definition (Lean source)
8 supporting declarations (lemmas, instances)
-
Var_sub_constlemma — Shifting a random variable by a constant leaves its variance unchanged.hypothesesconclusionD.Var (fun z => X z - c) = D.Var XProof (Lean source)
lemma Var_sub_const (X : Ω → ℝ) (c : ℝ) : D.Var (fun z => X z - c) = D.Var X := by rw [Var_eq, Var_eq, E_sub, E_const] have h : (fun z => (X z - c) ^ 2) = (fun z => (X z) ^ 2 + ((-(2 * c)) * X z + c ^ 2)) := by funext z; ring rw [h, E_add, E_add, E_const_mul, E_const]; ring -
tendsto_E_of_uniformBound_aetheorem — Design expectations converge to a constant when the random variables converge uniformly on the support of each design.hypothesesΩ :ℕ → Type*∀ n, Fintype (Ω n)D :∀ n, FiniteDesign (Ω n)F :∀ nifΩ nthenℝL :ℝB :ℕ → ℝhbound :∀ n sif(D n).p s ≠ 0then|F n s - L| ≤ B nProof (Lean source)
theorem tendsto_E_of_uniformBound_ae {Ω : ℕ → Type*} [∀ n, Fintype (Ω n)] (D : ∀ n, FiniteDesign (Ω n)) (F : ∀ n, Ω n → ℝ) (L : ℝ) (B : ℕ → ℝ) (hbound : ∀ n s, (D n).p s ≠ 0 → |F n s - L| ≤ B n) (hB : Tendsto B atTop (𝓝 0)) : Tendsto (fun n => (D n).E (F n)) atTop (𝓝 L) := by rw [tendsto_iff_norm_sub_tendsto_zero] refine squeeze_zero (fun n => norm_nonneg _) (fun n => ?_) hB have hrecenter : (D n).E (F n) - L = (D n).E (fun s => F n s - L) := by rw [(D n).E_sub (F n) (fun _ => L), (D n).E_const] rw [Real.norm_eq_abs, hrecenter] -- `|∑ p s (F s − L)| ≤ ∑ p s |F s − L| ≤ ∑ p s · B n = B n` on the support. unfold FiniteDesign.E calc |∑ s, (D n).p s * (F n s - L)| ≤ ∑ s, |(D n).p s * (F n s - L)| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ _s, (D n).p _s * B n := by refine Finset.sum_le_sum (fun s _ => ?_) rw [abs_mul, abs_of_nonneg ((D n).p_nonneg s)] by_cases hps : (D n).p s = 0 · simp [hps] · exact mul_le_mul_of_nonneg_left (hbound n s hps) ((D n).p_nonneg s) _ = B n := by rw [← Finset.sum_mul, (D n).p_sum, one_mul] -
estD_eq_agglemma — The experiment-level contrast estimator is the mean of the selected groups' per-group treatment-minus-control contrast estimators.hypothesesconclusionE.estD (s, w) = (∑ i, (if s i then (1 : ℝ) else 0) * groupDiff E i (w i)) / E.CProof (Lean source)
lemma estD_eq_agg (E : LHExperiment) (s : StratAssign E.ι) (w : ∀ i, Fin (E.gsize i) → Bool) : E.estD (s, w) = (∑ i, (if s i then (1 : ℝ) else 0) * groupDiff E i (w i)) / E.C := by simp only [LHExperiment.estD, estDirect, popEst, groupDiff] rw [← sub_div] congr 1 rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) by_cases h : s i = true · simp only [h, if_pos, one_mul] · simp [h] -
E_groupDiff_eq_of_homogeneouslemma — The conditional mean of the per-group contrast estimator under the ψ-design is the common group-level contrast: (ψ i).E (dᵢ) = δ. Immediate from E_groupEst (twice) and homogeneity.hypothesest :sharedℝδ :sharedℝM :sharedℝv :sharedℕ → ℝstud :sharedh :Homogeneous Exp t stud δ M vn :ℕi :(Exp n).ιconclusion((Exp n).ψ i).E (groupDiff (Exp n) i) = δProof (Lean source)
lemma E_groupDiff_eq_of_homogeneous (h : Homogeneous Exp t stud δ M v) (n : ℕ) (i : (Exp n).ι) : ((Exp n).ψ i).E (groupDiff (Exp n) i) = δ := by unfold groupDiff rw [FiniteDesign.E_sub, E_groupEst (Exp n).ψ (Exp n).Y i true ((Exp n).m1 i) ((Exp n).hm1 i) ((Exp n).hn i) ((Exp n).hprop1 i), E_groupEst (Exp n).ψ (Exp n).Y i false ((Exp n).m0 i) ((Exp n).hm0 i) ((Exp n).hn i) ((Exp n).hprop0 i), h.hδ n i] -
M_nonneg_of_homogeneouslemma — Nonnegativity of the bound constant M, available whenever the experiment has at least one group.hypothesest :sharedℝδ :sharedℝM :sharedℝv :sharedℕ → ℝstud :sharedh :Homogeneous Exp t stud δ M vn :ℕNonempty (Exp n).ιconclusion0 ≤ MProof (Lean source)
lemma M_nonneg_of_homogeneous (h : Homogeneous Exp t stud δ M v) (n : ℕ) [Nonempty (Exp n).ι] : 0 ≤ M := by obtain ⟨i⟩ := (inferInstance : Nonempty (Exp n).ι) exact le_trans (abs_nonneg _) (h.hMbound n i (fun _ => false)) -
exists_support_selectionlemma — Some stage-1 selection lies in the support of D₁ (its probabilities sum to one).Proof (Lean source)
lemma exists_support_selection (E : LHExperiment) : ∃ s, E.D₁.p s ≠ 0 := by by_contra hcon push_neg at hcon have : ∑ s, E.D₁.p s = 0 := Finset.sum_eq_zero (fun s _ => hcon s) rw [E.D₁.p_sum] at this exact one_ne_zero this -
refSel_memlemma — The fixed reference selection has positive stage-one design probability.Proof (Lean source)
lemma refSel_mem (Exp : ℕ → LHExperiment) (n : ℕ) : (Exp n).D₁.p (refSel Exp n) ≠ 0 := (exists_support_selection (Exp n)).choose_spec -
nonempty_of_refSellemma — The reference selection flags at least one group, so the group index type is nonempty.hypothesest :sharedℝδ :sharedℝM :sharedℝv :sharedℕ → ℝstud :sharedh :Homogeneous Exp t stud δ M vn :ℕconclusionNonempty (Exp n).ιProof (Lean source)
lemma nonempty_of_refSel (h : Homogeneous Exp t stud δ M v) (n : ℕ) : Nonempty (Exp n).ι := by by_contra hcon rw [not_nonempty_iff] at hcon have h0 : (∑ i, if refSel Exp n i then (1 : ℝ) else 0) = 0 := by rw [Finset.univ_eq_empty, Finset.sum_empty] rw [h.hcount n (refSel Exp n) (refSel_mem Exp n)] at h0 exact (Exp n).hC h0
CLT 1 core · 2 supporting The unconditional CLT for the treatment-minus-control direct-effect contrast is obtained by averaging uniformly convergent conditional laws across the first-stage strategy assignment. ★ directEffect_clt
Direct-contrast central limit theorem
The unconditional CLT for the treatment-minus-control direct-effect contrast is obtained by averaging uniformly convergent conditional laws across the first-stage strategy assignment.
The design-level lemmas are FiniteDesign.tendsto_E_of_uniformBound, which says expectations
preserve a uniform limit over finite assignment spaces, and FiniteDesign.Pr_compound_eq_E_condPr,
the tower bridge rewriting a compound-design probability as the stage-1 average of stage-2
conditional probabilities.
The headline theorem directEffect_clt proves Liu-Hudgens Proposition 5.1 conditional on the
uniform conditional studentized CDF hypothesis hcond: the joint-design CDF of the studentized
direct-effect contrast converges to stdNormalCdf t.
Proposition 5.1 (Liu–Hudgens 2014), asymptotic normality of the treatment-minus-control direct-effect contrast — conditional on the uniform conditional CLT. Along a sequence of two-stage Hudgens–Halloran experiments Exp : ℕ → LHExperiment, let stud n be the studentized statistic (D̂E − DE̅)/√directVar for the treatment-minus-control direct-effect contrast and cond n s the within-selection (stage-2 product) design when stage 1 selects the strategy assignment s. Assume the conditional studentized CDFs at t converge to the standard normal CDF Φ(t) uniformly over selections s, with a vanishing uniform bound. Then the unconditional (joint-design) studentized CDF at t converges to Φ(t):
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
tendsto_E_of_uniformBoundtheorem — Mixture-lifting lemma. If a sequence of design random variables F n : Ω n → ℝ converges to a constant L *uniformly* over the assignment space — |F n s − L| ≤ B n for every s, with B n → 0 — then their expectations converge to L: (D n).E (F n) → L. Averaging a uniformly convergent family preserves the limit, since the expectation of a B n-bounded deviation is itself B n-bounded. This is the abstract content of the two-stage mixture-lifting argument: the joint law is the stage-1 average of conditional laws, and a uniform conditional limit lifts to the average.hypothesesΩ :ℕ → Type*∀ n, Fintype (Ω n)D :∀ n, FiniteDesign (Ω n)F :∀ nifΩ nthenℝL :ℝB :ℕ → ℝhbound :∀ n s, |F n s - L| ≤ B nProof (Lean source)
theorem tendsto_E_of_uniformBound {Ω : ℕ → Type*} [∀ n, Fintype (Ω n)] (D : ∀ n, FiniteDesign (Ω n)) (F : ∀ n, Ω n → ℝ) (L : ℝ) (B : ℕ → ℝ) (hbound : ∀ n s, |F n s - L| ≤ B n) (hB : Tendsto B atTop (𝓝 0)) : Tendsto (fun n => (D n).E (F n)) atTop (𝓝 L) := by -- It suffices that `|(D n).E (F n) − L| → 0`. rw [tendsto_iff_norm_sub_tendsto_zero] -- Squeeze `‖(D n).E (F n) − L‖` between `0` and `B n → 0`. refine squeeze_zero (fun n => norm_nonneg _) (fun n => ?_) hB -- `(D n).E (F n) − L = (D n).E (fun s => F n s − L)` by linearity (`E_sub` + `E_const`). have hrecenter : (D n).E (F n) - L = (D n).E (fun s => F n s - L) := by rw [(D n).E_sub (F n) (fun _ => L), (D n).E_const] -- `|(D n).E (fun s => F n s − L)| ≤ B n` by the pointwise bound `hbound`. rw [Real.norm_eq_abs, hrecenter] exact (D n).abs_E_le (fun s => hbound n s) -
Pr_compound_eq_E_condPrlemma — Tower bridge for probabilities. Under the two-stage compound design, the unconditional probability of an event P equals the stage-1 expectation of its stage-2 conditional probability:hypothesesΩ₁ ι :∀ i, Fintype (α i)D₁ :FiniteDesign Ω₁D₂ :Ω₁ → ∀ i, FiniteDesign (α i)P :(Ω₁ × ∀ i, α i) → PropconclusionProof (Lean source)
lemma Pr_compound_eq_E_condPr {Ω₁ ι : Type*} [Fintype Ω₁] [Fintype ι] [DecidableEq ι] {α : ι → Type*} [∀ i, Fintype (α i)] (D₁ : FiniteDesign Ω₁) (D₂ : Ω₁ → ∀ i, FiniteDesign (α i)) (P : (Ω₁ × ∀ i, α i) → Prop) [DecidablePred P] : (compound D₁ D₂).Pr P = D₁.E (fun s => (prodDesign (D₂ s)).Pr (fun w => P (s, w))) := by -- `Pr P = E (ind P)`, then push `E` through the tower. rw [FiniteDesign.Pr, E_compound_tower] -- The inner stage-2 expectation of `ind P (s, ·)` is exactly the conditional probability. apply D₁.E_congr intro s rw [FiniteDesign.Pr] -- `ind P (s, w) = ind (fun w => P (s, w)) w` definitionally (both `if … then 1 else 0`). apply (prodDesign (D₂ s)).E_congr intro w rfl
CLTDischargeMain 1 core · 1 supporting The primitive Liu-Hudgens treatment-minus-control direct-effect CLT follows from the independent-summands product-design CLT. ★ directEffect_clt_homogeneous
Primitive direct-contrast CLT
The primitive Liu-Hudgens treatment-minus-control direct-effect CLT follows from the independent-summands product-design CLT.
The lemma condCLT_ref applies prodDesign_clt to the homogeneity-reduced per-coordinate summands
at the reference first-stage selection. The theorem directEffect_clt_homogeneous then uses
selection homogeneity and the support-restricted mixture-lifting lemma to prove that the joint
studentized direct-effect CDF converges to stdNormalCdf t.
Proposition 5.1 (Liu–Hudgens 2014), fully primitive. Under the homogeneity and regularity bundle, the studentized treatment-minus-control direct-effect contrast is asymptotically standard normal: its joint-design CDF at t converges to Φ(t).
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
condCLT_reflemma — Conditional CLT for the reference selection. Applying the independent-summands CLT prodDesign_clt to the per-coordinate summands gₛ₀,ᵢ over the conditional product design gives the conditional studentized CDF at the reference selection refSel Exp n converging to Φ(t).hypothesest :sharedℝδ :sharedℝM :sharedℝv :sharedℕ → ℝstud :sharedh :Homogeneous Exp t stud δ M vconclusionTendsto (fun n => (condDesign (Exp n) (refSel Exp n)).Pr (fun w => stud n (refSel Exp n, w) ≤ t)) atTop (𝓝 (stdNormalCdf t))Proof (Lean source)
lemma condCLT_ref (h : Homogeneous Exp t stud δ M v) : Tendsto (fun n => (condDesign (Exp n) (refSel Exp n)).Pr (fun w => stud n (refSel Exp n, w) ≤ t)) atTop (𝓝 (stdNormalCdf t)) := by classical set s₀ : ∀ n, StratAssign (Exp n).ι := fun n => refSel Exp n with hs₀ -- Coordinate designs and per-coordinate summands. set D : ∀ n, ∀ i : (Exp n).ι, FiniteDesign (Fin ((Exp n).gsize i) → Bool) := fun n i => if s₀ n i then (Exp n).ψ i else (Exp n).φ i with hD set g : ∀ n, ∀ i : (Exp n).ι, (Fin ((Exp n).gsize i) → Bool) → ℝ := fun n i => cltSummand n δ v (s₀ n) i with hg set B : ℕ → ℝ := fun n => M / sqrt ((Exp n).C * v n) with hBdef -- Positivity facts. have hCpos : ∀ n, 0 < (Exp n).C := by intro n have := nonempty_of_refSel h n rcases lt_or_gt_of_ne (Exp n).hC with h0 | h0 · exfalso have hnn : (0 : ℝ) ≤ ∑ i, if s₀ n i then (1 : ℝ) else 0 := sum_nonneg (fun i _ => by positivity) rw [h.hcount n (s₀ n) (refSel_mem Exp n)] at hnn; linarith · exact h0 have hsqrt : ∀ n, 0 < sqrt ((Exp n).C * v n) := fun n => Real.sqrt_pos.mpr (mul_pos (hCpos n) (h.hvpos n)) -- `0 ≤ B n`. have hB : ∀ n, 0 ≤ B n := by intro n have := nonempty_of_refSel h n exact div_nonneg (M_nonneg_of_homogeneous h n) (hsqrt n).le -- Uniform bound `|g n i a| ≤ B n`. have hbound : ∀ n i a, |g n i a| ≤ B n := by intro n i a rw [hg, hBdef] change |cltSummand n δ v (s₀ n) i a| ≤ M / sqrt ((Exp n).C * v n) unfold cltSummand rw [abs_div, abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)] rw [div_le_div_iff_of_pos_right (hsqrt n)] calc |if s₀ n i then (1:ℝ) else 0| * |groupDiff (Exp n) i a - δ| ≤ 1 * |groupDiff (Exp n) i a - δ| := by apply mul_le_mul_of_nonneg_right _ (abs_nonneg _) by_cases hh : s₀ n i = true <;> simp [hh] _ = |groupDiff (Exp n) i a - δ| := one_mul _ _ ≤ M := h.hMbound n i a -- Mean-zero summands. have hmean : ∀ n i, (D n i).E (g n i) = 0 := by intro n i change (if s₀ n i then (Exp n).ψ i else (Exp n).φ i).E (cltSummand n δ v (s₀ n) i) = 0 rw [show cltSummand n δ v (s₀ n) i = (fun a => ((if s₀ n i then (1:ℝ) else 0) / sqrt ((Exp n).C * v n)) * (groupDiff (Exp n) i a - δ)) from funext fun a => by unfold cltSummand; ring] rw [FiniteDesign.E_const_mul] by_cases hh : s₀ n i = true · rw [if_pos hh, if_pos hh] have : ((Exp n).ψ i).E (fun a => groupDiff (Exp n) i a - δ) = 0 := by rw [FiniteDesign.E_sub, FiniteDesign.E_const, E_groupDiff_eq_of_homogeneous h, sub_self] rw [this, mul_zero] · rw [if_neg hh]; ring -- Unit total variance. have hvar : ∀ n, (prodDesign (D n)).Var (fun w => ∑ i, g n i (w i)) = 1 := by intro n have := nonempty_of_refSel h n -- Write `g n i a = c i * gtil i a`. set c : (Exp n).ι → ℝ := fun i => (if s₀ n i then (1:ℝ) else 0) / sqrt ((Exp n).C * v n) with hc set gtil : ∀ i : (Exp n).ι, (Fin ((Exp n).gsize i) → Bool) → ℝ := fun i a => groupDiff (Exp n) i a - δ with hgtil rw [show (fun w : ∀ i, Fin ((Exp n).gsize i) → Bool => ∑ i, g n i (w i)) = (fun w => ∑ i, c i * gtil i (w i)) from funext fun w => by refine Finset.sum_congr rfl (fun i _ => ?_) rw [hg, hc, hgtil]; simp only [cltSummand]; ring] rw [FiniteDesign.Var_prod_linear_comb] -- Each term: `(c i)² · Var(gtil i) = if s₀ᵢ then v/(C·v) else 0`. have hterm : ∀ i, (c i) ^ 2 * (D n i).Var (gtil i) = (if s₀ n i then (1:ℝ) else 0) * (v n / ((Exp n).C * v n)) := by intro i change ((if s₀ n i then (1:ℝ) else 0) / sqrt ((Exp n).C * v n)) ^ 2 * (if s₀ n i then (Exp n).ψ i else (Exp n).φ i).Var (fun a => groupDiff (Exp n) i a - δ) = (if s₀ n i then (1:ℝ) else 0) * (v n / ((Exp n).C * v n)) by_cases hh : s₀ n i = true · rw [if_pos hh, if_pos hh, FiniteDesign.Var_sub_const, h.hv n i] rw [div_pow, one_pow, Real.sq_sqrt (mul_pos (hCpos n) (h.hvpos n)).le, one_mul, one_div, inv_mul_eq_div] · rw [if_neg hh, if_neg hh]; simp rw [Finset.sum_congr rfl (fun i _ => hterm i), ← Finset.sum_mul, h.hcount n (s₀ n) (refSel_mem Exp n)] rw [mul_div_assoc', div_eq_one_iff_eq (mul_ne_zero (ne_of_gt (hCpos n)) (ne_of_gt (h.hvpos n)))] -- Assemble `prodDesign_clt`. have hclt := DesignBased.prodDesign_clt D g B hB h.hB0 hbound h.hNB3 hmean hvar t -- Rewrite the prelimit to the conditional studentized CDF. refine hclt.congr (fun n => ?_) rw [condDesign] congr 1 funext w rw [stud_eq_sum_of_homogeneous h n (s₀ n) (refSel_mem Exp n) w]
Consistency 1 core · 0 supporting The two-stage estimator of the treatment-minus-control direct-effect contrast is consistent when its design variance vanishes. ★ estDirect_consistent
Direct-contrast consistency
The two-stage estimator of the treatment-minus-control direct-effect contrast is consistent when its design variance vanishes.
This file proves Chebyshev consistency for the Liu-Hudgens direct-contrast estimator along a sequence of two-stage experiments.
Consistency of the direct-effect contrast estimator (Liu–Hudgens 2014). Along a sequence of two-stage experiments, if the closed-form design variance directVar tends to zero as the number of groups grows, then for every positive tolerance ε, the Horvitz-Thompson estimator is consistent for the population average treatment-minus-control direct-effect contrast: the probability that the deviation exceeds ε tends to zero.
Formal statement
Proof (Lean source)
Identical 9 core · 8 supporting This file turns literal group-level symmetry into the homogeneity hypothesis used by the Liu-Hudgens direct-effect CLT. ★ IdenticalRef★ directEffect_clt_identical
Identical-groups discharge for the direct-effect CLT
This file turns literal group-level symmetry into the homogeneity hypothesis used by the Liu-Hudgens direct-effect CLT.
The reference bundle IdenticalRef stores one identical-groups experiment: a common group size,
common within-group strategies, common potential outcomes, common treated/control counts, the
stage-1 design, and the propensities/nondegeneracy hypotheses needed to build `toExp :
LHExperiment. It also defines the common per-group contrast groupDiff₀`, the concrete
studentized statistic studId, the common group effect refDelta, and the common within-group
variance refVar.
The theorem hhom_of_identical proves the selection-symmetry hypothesis by relabeling equal-size
selected sets with exists_equiv_selection and prodDesign_Pr_reindex. The definition
homogeneous_of_identical assembles the resulting Homogeneous bundle, and
directEffect_clt_identical derives asymptotic normality without assuming analytic homogeneity as a
separate premise.
Reference data for one identical-groups experiment. All groups in the population share a common size K, a common pair of within-group allocation strategies ψ₀ and φ₀, common potential outcomes Y₀, and common control and treatment unit counts, each assumed nonzero, as is the group size K. A stage-1 design D₁ assigns each group a strategy, selecting a nonzero number C of groups for ψ, out of a population of at least two groups; every unit's within-group control propensity equals m0₀/K and its treatment propensity equals m1₀/K, every group's stage-1 selection propensity equals C/N, and every pair's joint selection propensity equals C(C−1)/(N(N−1)). Together these assemble the constant LHExperiment toExp.
Definition (Lean source)
Given reference data for one identical-groups experiment, the constant Liu--Hudgens experiment assigns every group the common size, two common within-group randomization designs, common potential outcomes, and common treated and control counts in that reference data. Thus its conditional within-group randomization is a product across groups.
Definition (Lean source)
Given reference data for one identical-groups experiment and a realized assignment within its common-size group, the common per-group treatment-minus-control contrast estimator is the sum of potential outcomes for treated units divided by the common treated count minus the analogous sum for control units divided by the common control count.
Definition (Lean source)
Given reference data for one identical-groups experiment and a realized first-stage strategy assignment together with a realized within-group assignment for every group, the studentized treatment-minus-control contrast statistic is the aggregate direct-effect estimator minus its population direct effect, divided by the square root of its direct-effect variance.
Definition (Lean source)
Given reference data for one identical-groups experiment and a treatment status, the common group-average potential outcome is the arithmetic mean over units in the common group of their expected potential outcomes under the reference allocation strategy, conditional on their own treatment having that status.
Definition (Lean source)
Given reference data for one identical-groups experiment, the common group-level direct-effect contrast is its common group-average potential outcome under treatment minus that under control.
Definition (Lean source)
Given reference data for one identical-groups experiment, the common within-group contrast-estimator variance is the variance, under the reference first allocation strategy, of the common per-group treatment-minus-control contrast estimator.
Definition (Lean source)
Given a sequence of identical-groups reference experiments, a real evaluation threshold, a real common direct-effect contrast, a real uniform bound, the assumption that every reference direct-effect contrast equals that common contrast, the assumption that every reference within-group contrast variance is positive, the assumption that, for every experiment, group, and within-group assignment, the absolute difference between the realized group contrast and the common contrast is at most the uniform bound, the assumption that every first-stage assignment with positive probability selects exactly its prescribed number of groups, the assumption that, as the sequence index grows, converges to zero, where is the prescribed selected-group count and the reference within-group variance, and the assumption that the number of groups times converges to zero, the homogeneity bundle for this sequence has the stated threshold, studentized statistics, common contrast, bound, and reference within-group variances. Its conditional-distribution homogeneity follows from literal identity of the groups.
Definition (Lean source)
Proposition 5.1 under literally identical groups. Along a sequence of identical-groups experiments R — common size, allocation strategies, potential outcomes, and unit counts — sharing one group-level treatment-minus-control direct-effect contrast δ with a positive common within-group variance, a uniform bound M on the centered per-group contrast estimator, every supported stage-1 selection flagging exactly C groups, and the many-groups rate M/√(C·v) → 0 together with its Lyapunov cube card·(M/√(C·v))³ → 0 — the studentized contrast statistic is asymptotically standard normal. No analytic homogeneity hypothesis is assumed: it is derived from the concrete identical-groups structure via hhom_of_identical.
Formal statement
Proof (Lean source)
8 supporting declarations (lemmas, instances)
-
exists_equiv_selectionlemma — Selection-symmetry permutation. Given two Boolean selections s, s' on a finite type ι that flag the same number of indices (card {i | s i} = card {i | s' i}), there is a permutation σ : ι ≃ ι aligning their patterns: s' i = s (σ i) for every i. Built by gluing a bijection of the selected sets (equal cardinality) with a bijection of their complements (equal cardinality, since the total is fixed) through Equiv.sumCompl.Proof (Lean source)
lemma exists_equiv_selection {ι : Type*} [Fintype ι] (s s' : ι → Bool) (hcard : (Finset.univ.filter (fun i => s i = true)).card = (Finset.univ.filter (fun i => s' i = true)).card) : ∃ σ : ι ≃ ι, ∀ i, s' i = s (σ i) := by classical -- Predicates with the carried `Fintype`/`DecidablePred` instances. -- True-sets have equal cardinality (`hcard`); complements then also (total `card ι` fixed). have hcardT : card {i // s' i = true} = card {i // s i = true} := by simp only [Fintype.card_subtype] exact hcard.symm have hcardF : card {i // ¬ s' i = true} = card {i // ¬ s i = true} := by have h1 := Fintype.card_subtype_compl (fun i => s' i = true) have h2 := Fintype.card_subtype_compl (fun i => s i = true) rw [h1, h2, hcardT] -- Bijections of selected sets and of complements. let eT : {i // s' i = true} ≃ {i // s i = true} := Fintype.equivOfCardEq hcardT let eF : {i // ¬ s' i = true} ≃ {i // ¬ s i = true} := Fintype.equivOfCardEq hcardF -- Glue via `sumCompl` on both sides. let σ : ι ≃ ι := (Equiv.sumCompl (fun i => s' i = true)).symm.trans ((eT.sumCongr eF).trans (Equiv.sumCompl (fun i => s i = true))) refine ⟨σ, fun i => ?_⟩ -- Compute `σ i` explicitly: it is the underlying element of the image of `i` under the glued -- bijection, which by construction lies in the matching set of `s`. have hσ : ∀ i, σ i = (Equiv.sumCompl (fun i => s i = true)) ((eT.sumCongr eF) ((Equiv.sumCompl (fun i => s' i = true)).symm i)) := fun i => rfl rw [hσ] -- Case on `s' i`; in each branch `σ i` lands in the matching set of `s`. by_cases hi : s' i = true · rw [Equiv.sumCompl_symm_apply_of_pos (p := fun i => s' i = true) hi] rw [Equiv.sumCongr_apply, Sum.map_inl, Equiv.sumCompl_apply_inl] exact hi.trans ((eT ⟨i, hi⟩).2).symm · rw [Equiv.sumCompl_symm_apply_of_neg (p := fun i => s' i = true) hi] rw [Equiv.sumCongr_apply, Sum.map_inr, Equiv.sumCompl_apply_inr] have hF : s (↑(eF ⟨i, hi⟩)) = false := Bool.not_eq_true _ ▸ (eF ⟨i, hi⟩).2 rw [hF]; simpa using hi -
groupDiff_toExplemma — In the constant experiment, every group's contrast estimator equals the common groupDiff₀.Proof (Lean source)
-
condDesign_toExplemma — The conditional design of the constant experiment is the genuine product, over the non-dependent space R.ι → (Fin K → Bool), of the per-group strategy designs.hypothesess :StratAssign R.ιconclusioncondDesign R.toExp s = prodDesign (fun i => if s i then R.ψ₀ else R.φ₀)Proof (Lean source)
lemma condDesign_toExp (s : StratAssign R.ι) : condDesign R.toExp s = prodDesign (fun i => if s i then R.ψ₀ else R.φ₀) := rfl -
estD_equivariantlemma — Estimator equivariance. Because all groups are identical, the aggregate contrast estimator sees a selection only through its pattern: if σ aligns the patterns of s' and s (s' i = s (σ i)), then evaluating at s' and the relabeled assignment w ∘ σ equals the value at s and w.hypothesesconclusionR.toExp.estD (s', fun i => w (σ i)) = R.toExp.estD (s, w)Proof (Lean source)
lemma estD_equivariant (s s' : StratAssign R.ι) (σ : R.ι ≃ R.ι) (hσ : ∀ i, s' i = s (σ i)) (w : R.ι → (Fin R.K → Bool)) : R.toExp.estD (s', fun i => w (σ i)) = R.toExp.estD (s, w) := by rw [estD_eq_agg R.toExp s' (fun i => w (σ i)), estD_eq_agg R.toExp s w] congr 1 refine Fintype.sum_equiv σ (fun i => (if s' i then (1 : ℝ) else 0) * groupDiff R.toExp i (w (σ i))) (fun i => (if s i then (1 : ℝ) else 0) * groupDiff R.toExp i (w i)) (fun i => ?_) simp only [groupDiff_toExp, hσ i] -
studId_equivariantlemma — Studentized equivariance. The studentized statistic is likewise selection-pattern equivariant, since DEbar and directVar are scalars and the estimator is equivariant.hypothesesconclusionR.studId (s', fun i => w (σ i)) = R.studId (s, w)Proof (Lean source)
lemma studId_equivariant (s s' : StratAssign R.ι) (σ : R.ι ≃ R.ι) (hσ : ∀ i, s' i = s (σ i)) (w : R.ι → (Fin R.K → Bool)) : R.studId (s', fun i => w (σ i)) = R.studId (s, w) := by unfold studId congr 2 exact estD_equivariant R s s' σ hσ w -
hhom_of_identicallemma — Derived homogeneity hypothesis under identical groups. For two stage-1 selections each flagging exactly C groups, the conditional studentized CDF is the same. This is exactly the analytic homogeneity hypothesis hhom, now a theorem: the selection-symmetry permutation σ (exists_equiv_selection) relabels the conditional product design (prodDesign_Pr_reindex) while carrying the studentized statistic (studId_equivariant), so the two CDFs coincide.hypothesest :ℝs s' :StratAssign R.ιhs :(∑ i, if s i then (1 : ℝ) else 0) = R.Chs' :(∑ i, if s' i then (1 : ℝ) else 0) = R.Cconclusion(condDesign R.toExp s).Pr (fun w => R.studId (s, w) ≤ t)= (condDesign R.toExp s').Pr (fun w => R.studId (s', w) ≤ t)Proof (Lean source)
lemma hhom_of_identical (t : ℝ) (s s' : StratAssign R.ι) (hs : (∑ i, if s i then (1 : ℝ) else 0) = R.C) (hs' : (∑ i, if s' i then (1 : ℝ) else 0) = R.C) : (condDesign R.toExp s).Pr (fun w => R.studId (s, w) ≤ t) = (condDesign R.toExp s').Pr (fun w => R.studId (s', w) ≤ t) := by -- The two selections flag the same number of groups, so their selected sets have equal card. have hsum : (∑ i, if s i then (1 : ℝ) else 0) = (∑ i, if s' i then (1 : ℝ) else 0) := by rw [hs, hs'] have hcardℝ : ((Finset.univ.filter (fun i => s i = true)).card : ℝ) = ((Finset.univ.filter (fun i => s' i = true)).card : ℝ) := by have e : ∀ u : StratAssign R.ι, (∑ i, if u i then (1 : ℝ) else 0) = ((Finset.univ.filter (fun i => u i = true)).card : ℝ) := by intro u rw [Finset.sum_ite, Finset.sum_const, Finset.sum_const_zero, add_zero, nsmul_eq_mul, mul_one] rw [← e s, ← e s', hsum] have hcard : (Finset.univ.filter (fun i => s i = true)).card = (Finset.univ.filter (fun i => s' i = true)).card := by exact_mod_cast hcardℝ -- The selection-symmetry permutation aligning `s'` to `s`. obtain ⟨σ, hσ⟩ := exists_equiv_selection s s' hcard -- Relabel `condDesign s'` to `condDesign s` via `prodDesign_Pr_reindex`, carrying the statistic. rw [condDesign_toExp, condDesign_toExp] -- The permuted product `D ∘ σ` equals the conditional design at `s'` (since `s' i = s (σ i)`). have hdesign : (fun i => if s (σ i) then R.ψ₀ else R.φ₀) = (fun i => if s' i then R.ψ₀ else R.φ₀) := by funext i; rw [hσ i] calc (prodDesign (fun i => if s i then R.ψ₀ else R.φ₀)).Pr (fun w => R.studId (s, w) ≤ t) = (prodDesign (fun i => if s i then R.ψ₀ else R.φ₀)).Pr (fun w => R.studId (s', fun i => w (σ i)) ≤ t) := FiniteDesign.Pr_congr _ _ _ (fun w => by rw [studId_equivariant R s s' σ hσ w]) _ = (prodDesign (fun i => (fun i => if s i then R.ψ₀ else R.φ₀) (σ i))).Pr (fun w => R.studId (s', w) ≤ t) := FiniteDesign.prodDesign_Pr_reindex σ (fun i => if s i then R.ψ₀ else R.φ₀) (fun w => R.studId (s', w) ≤ t) _ = (prodDesign (fun i => if s' i then R.ψ₀ else R.φ₀)).Pr (fun w => R.studId (s', w) ≤ t) := by rw [hdesign] -
hδ_toExplemma — In the constant experiment every group's level contrast equals the common refDelta.hypothesesi :R.ι -
hv_toExplemma — In the constant experiment every group's within-group variance equals the common refVar.hypothesesi :R.ι
Wald 1 core · 0 supporting Oracle Wald intervals for Liu-Hudgens treatment-minus-control direct-effect contrasts have asymptotic coverage from the CLT. ★ wald_coverage_oracle
Oracle Wald coverage
Oracle Wald intervals for Liu-Hudgens treatment-minus-control direct-effect contrasts have asymptotic coverage from the CLT.
The public theorem wald_coverage_oracle proves the lower-coverage result for intervals using
the true design variance. It takes the two one-sided studentized CLT limits at the normal
quantile and its negative as inputs, then converts the event |stud| ≤ zq into coverage of
DEbar by multiplying through the positive square-root design variance.
Asymptotic oracle Wald coverage (Liu–Hudgens 2014). Along a sequence of two-stage Hudgens–Halloran experiments Exp, let stud n be the studentized statistic (D̂E − DE̅)/√directVar for the treatment-minus-control direct-effect contrast, and assume the design variance is everywhere positive. Let zq ≥ 0 be the standard-normal upper quantile at level γ, i.e. Φ(zq) = 1 − γ/2, and assume the two studentized-CDF limits of stud at zq and −zq converge to Φ(zq) and Φ(−zq) — exactly the conclusion of the direct-contrast CLT. Then the oracle Wald interval D̂E ± zq·√directVar attains asymptotic coverage of DE̅ at least 1 − γ.
Formal statement
Proof (Lean source)
WaldFeasible 1 core · 0 supporting Feasible Wald intervals retain asymptotic coverage when the estimated variance does not undershoot. ★ wald_coverage_feasible
Feasible Wald coverage
Feasible Wald intervals retain asymptotic coverage when the estimated variance does not undershoot.
The helper lemma clt_interval_liminf_lb turns per-threshold CLT limits into a lower bound for
two-sided studentized bands. The public theorem wald_coverage_feasible then combines that band
bound with a conservative-consistency hypothesis on the variance estimator Vh, proving
asymptotic lower coverage for intervals of the form estD ± zq * sqrt (Vh).
Asymptotic feasible Wald coverage (Liu–Hudgens 2014). Along a sequence of two-stage Hudgens–Halloran experiments Exp, let stud n be the studentized statistic (D̂E − DE̅)/√directVar for the treatment-minus-control direct-effect contrast, and assume its per-threshold CDF converges to the standard normal CDF at every threshold and the design variance is everywhere positive. Let Vh n be an arbitrary variance estimator that is conservative-consistent — for every slack ε > 0 the probability it undershoots (1−ε) times the true variance tends to zero, and let zq ≥ 0 be the standard-normal upper quantile at level γ, Φ(zq) = 1 − γ/2. Then the feasible Wald interval D̂E ± zq·√(Vh) attains asymptotic coverage of DE̅ at least 1 − γ.