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 large-sample inference on the control-minus-treatment direct-effect contrast. ★ LHExperiment★ E_estD★ var_estD
Liu-Hudgens asymptotic setup
LHExperiment packages one Hudgens–Halloran two-stage experiment for large-sample inference on the
control-minus-treatment direct-effect contrast. This is the negative of the treatment-minus-control
estimand used by Liu–Hudgens (2014).
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 two-stage experiment in the Hudgens–Halloran orientation, packaged so that a sequence can be studied using Liu–Hudgens-style large-sample arguments. Its direct contrast is the negative of Liu–Hudgens' treatment-minus-control estimand. It 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 two-stage 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 two-stage experiment, the Horvitz--Thompson estimator of its control-minus-treatment 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 two-stage experiment, the population-average control-minus-treatment direct effect is the mean potential outcome under control minus the mean potential outcome under treatment, with both means evaluated under the experiment's treatment strategy.
Definition (Lean source)
For a two-stage experiment, the closed-form design variance of the control-minus-treatment direct-effect estimator equals (1-C/N) S_μ²/C + (CN)⁻¹ ∑ᵢ Vᵢ, where N is the number of groups, C is the number assigned the treatment strategy, S_μ² is the population sample variance of the group-level contrasts, and Vᵢ is group i's within-group contrast-estimator variance under the treatment strategy.
Definition (Lean source)
Unbiasedness bridge. The Horvitz–Thompson estimator is unbiased for the population average control-minus-treatment direct-effect contrast.
Formal statement
Proof (Lean source)
Variance bridge. The design variance of the control-minus-treatment 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 strongly 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 strongly 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 special-case result. The control-minus-treatment contrast is the negative of Liu–Hudgens' convention.
For a two-stage experiment, one of its groups, and a within-group treatment assignment, the per-group control-minus-treatment direct-effect estimator is the control-strategy group estimator minus the treated-strategy group estimator.
For a two-stage 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)
For a sequence of two-stage experiments, an evaluation threshold, a studentized-statistic family, a common group contrast, a uniform bound, and a within-group variance sequence, the strong homogeneity and regularity bundle records that the statistic has the standardized direct-contrast form; every group contrast equals the common value; every within-group contrast-estimator variance equals the specified value, which is positive; the centered per-group estimator is uniformly bounded; every supported stage-one selection flags exactly C groups; the size-normalized bound tends to zero, together with its cubed Lyapunov rate; and the conditional CDF is selection-independent on the stage-one support. These assumptions force the between-group effect variance to zero, so they are stronger than the heterogeneous regime of Liu–Hudgens Proposition 5.1.
Definition (Lean source)
Estimand reduction. Under the homogeneity and regularity bundle, the population average control-minus-treatment 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 two-stage experiments, an experiment index n, 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 √(C_n v_n).
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 two-stage experiments and an experiment index n, 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 control-minus-treatment 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 false ((Exp n).m0 i) ((Exp n).hm0 i) ((Exp n).hn i) ((Exp n).hprop0 i), 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), 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 An unconditional CDF limit for the control-minus-treatment direct-effect contrast is obtained by averaging uniformly convergent conditional laws across the first-stage strategy assignment. ★ directEffect_cdf_tendsto_of_uniform_conditional
Direct-contrast conditional-to-unconditional CDF transfer
An unconditional CDF limit for the control-minus-treatment direct-effect contrast is obtained by averaging uniformly convergent conditional laws across the first-stage strategy assignment. The contrast is the negative of Liu–Hudgens' treatment-minus-control estimand.
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 theorem directEffect_cdf_tendsto_of_uniform_conditional is a mixture-transfer result: given
the uniform conditional studentized-CDF limit hcond, the joint-design CDF converges to
stdNormalCdf t. It does not derive the conditional limit required in Liu–Hudgens Proposition 5.1.
Conditional-to-unconditional CDF transfer for the direct-effect statistic. Along a sequence of two-stage Hudgens–Halloran experiments, at a fixed threshold t, let stud n be the studentized statistic (D̂E − DE̅)/√directVar for the control-minus-treatment direct-effect contrast, and let cond n s be the within-selection stage-two product design. If the conditional studentized CDFs at t approach Φ(t) uniformly over selections, with a vanishing uniform bound, then the unconditional joint-design studentized CDF at t approaches Φ(t). The contrast is the negative of Liu–Hudgens' treatment-minus-control estimand, and the conditional Gaussian limit is an assumption rather than a conclusion.
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 CLT for a strongly homogeneous control-minus-treatment direct-effect contrast follows from the independent-summands product-design CLT. ★ directEffect_clt_homogeneous
Primitive direct-contrast CLT
The primitive CLT for a strongly homogeneous control-minus-treatment direct-effect contrast follows from the independent-summands product-design CLT. This contrast reverses the Liu–Hudgens convention.
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.
Primitive CLT under strong homogeneity. Under the strong homogeneity and regularity bundle, the studentized control-minus-treatment direct-effect contrast is asymptotically standard normal: its joint-design CDF at t converges to Φ(t). The contrast is the negative of Liu–Hudgens' treatment-minus-control estimand, and the bundle forces its between-group effect variance to zero, so this is a strict special case of their heterogeneous Proposition 5.1.
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 := Finset.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 control-minus-treatment direct-effect contrast is consistent from bounded potential outcomes, fixed within-group allocations on the design support, and a growing number of selected groups. ★ estDirect_consistent_of_bounded_outcomes
Direct-contrast consistency
The two-stage estimator of the control-minus-treatment direct-effect contrast is consistent from bounded potential outcomes, fixed within-group allocations on the design support, and a growing number of selected groups. This contrast is the negative of the Liu–Hudgens treatment-minus-control estimand.
This file proves Chebyshev consistency for the sign-reversed Liu–Hudgens direct contrast along a sequence of two-stage experiments.
Consistency of the direct-effect contrast estimator (Liu–Hudgens 2014). Along a sequence of two-stage experiments, suppose potential outcomes are uniformly bounded by a nonnegative constant, control and treatment allocation counts are positive, every within-group assignment with nonzero design probability has those fixed allocation counts, the number of groups assigned the treatment strategy is positive and no larger than the population, and that number tends to infinity. Then, for every positive tolerance, the control-minus-treatment direct-effect estimator converges in probability to its population contrast. This contrast is the negative of Liu–Hudgens' treatment-minus-control estimand.
Formal statement
Proof (Lean source)
Identical 9 core · 8 supporting This file turns literal group-level symmetry into the homogeneity hypothesis used by the special-case 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 special-case direct-effect CLT. Its control-minus-treatment contrast reverses the Liu–Hudgens sign.
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 two-stage 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 control-minus-treatment contrast estimator is the control-outcome sum divided by the common control count minus the treatment-outcome sum divided by the common treated 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 control-minus-treatment 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 control minus that under treatment.
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 control-minus-treatment 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 (M/√(C_n v_n))^3 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)
Direct-effect CLT under literally identical groups. Along identical-group experiments at a fixed threshold, suppose all group-level control-minus-treatment contrasts equal δ, each common within-group variance is positive, centered per-group contrast estimators are uniformly bounded by M, supported first-stage selections have fixed size C, the normalized bound vanishes, and the Lyapunov cube rate vanishes. Then the studentized contrast is asymptotically standard normal. No analytic homogeneity hypothesis is assumed: it is derived from the concrete identical-groups structure via hhom_of_identical. The contrast is the negative of Liu–Hudgens' treatment-minus-control estimand, and literal identity makes the theorem a strict special case of their heterogeneous Proposition 5.1.
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 the control-minus-treatment direct-effect contrast have asymptotic coverage from assumed Gaussian CDF limits. ★ wald_coverage_oracle
Oracle Wald coverage
Oracle Wald intervals for the control-minus-treatment direct-effect contrast have asymptotic coverage from assumed Gaussian CDF limits. The contrast reverses the Liu–Hudgens sign convention.
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, let stud n be the studentized statistic (D̂E − DE̅)/√directVar for the control-minus-treatment 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 − γ. The contrast is the negative of Liu–Hudgens' treatment-minus-control estimand.
Formal statement
Proof (Lean source)
WaldFeasible 1 core · 0 supporting This file specializes the shared design-based feasible-Wald transfer to the control-minus-treatment estimator, which is the negative of Liu–Hudgens' treatment-minus-control estimator. ★ wald_coverage_feasible
Feasible Wald coverage
This file specializes the shared design-based feasible-Wald transfer to the control-minus-treatment
estimator, which is the negative of Liu–Hudgens' treatment-minus-control estimator. The theorem
wald_coverage_feasible combines a studentized CDF limit with conservative consistency of 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, let stud n be the studentized statistic (D̂E − DE̅)/√directVar for the control-minus-treatment 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 − γ. The contrast is the negative of Liu–Hudgens' treatment-minus-control estimand.