Experimentation.DesignBased.Estimators
Entry point for paper-agnostic estimators of finite-population causal estimands and their randomization properties.
DifferenceInMeans 6 core · 3 supporting The two-arm difference-in-means estimator is unbiased for the sample average treatment effect under complete randomization. ★ E_diffInMeans_eq_sate
Difference-in-means under complete randomization
The two-arm difference-in-means estimator is unbiased for the sample average treatment effect under complete randomization.
This file defines the finite-population target sateEstimand, the realized arm averages
treatedMean and controlMean, and their contrast diffInMeans. The results
E_treatedMean and E_controlMean prove that each arm mean estimates its finite-population arm
mean, and E_diffInMeans_eq_sate packages the consequence: when 0 < n₁ < N, the expected
difference in means equals sateEstimand. The companion theorem unbiased_diffInMeans states the
same fact using the generic FiniteDesign.Unbiased predicate. The generic finite-population
variance quantities used by downstream variance results are defined in NeymanVariance.
For a finite population of units with potential outcomes under treatment and under control, the sample average treatment effect is the population mean of the unit-level difference between those two potential outcomes.
Definition (Lean source)
For a finite population of units, a number of treated units, the potential outcome under treatment for each unit, and a treated set containing exactly that many units, the treated-arm mean is the average treatment potential outcome among the treated units.
Definition (Lean source)
For a finite population of units, a number of treated units, the potential outcome under control for each unit, and a treated set containing exactly that many units, the control-arm mean is the average control potential outcome among all units outside the treated set.
For a finite population of units, a number of treated units, potential outcomes under treatment and under control, and a treated set containing exactly that many units, the difference-in-means estimator is the treated-arm mean minus the control-arm mean.
Definition (Lean source)
Unbiasedness of difference in means. Under complete randomization in which at least one unit is treated and the treated count n₁ is strictly below the population size N, so at least one unit remains a control, the difference-in-means estimator, computed from the potential outcomes Y1 and Y0, has expectation exactly equal to the sample average treatment effect.
Formal statement
Proof (Lean source)
For a population of n units, a treated count, treated and control potential outcomes, and a treated set, the usual conservative variance estimator for difference in means is the transported sum of the two observed arm sample variances divided by their arm sizes.
3 supporting declarations (lemmas, instances)
-
E_treatedMeantheorem — The treated-arm mean is unbiased for the treated population mean (1/N) ∑ Y1. Each unit enters the treated arm with probability n₁ / N, so its inverse-n₁ weight averages to 1/N.hypothesesU :sharedType u_1n₁ :ℕhn :n₁ ≤ Fintype.card Uhn1 :0 < n₁Y1 :U → ℝconclusion(completeRandomization n₁ hn).E (treatedMean n₁ Y1) = (∑ i, Y1 i) / (Fintype.card U : ℝ)Proof (Lean source)
theorem E_treatedMean (n₁ : ℕ) (hn : n₁ ≤ Fintype.card U) (hn1 : 0 < n₁) (Y1 : U → ℝ) : (completeRandomization n₁ hn).E (treatedMean n₁ Y1) = (∑ i, Y1 i) / (Fintype.card U : ℝ) := by let D := completeRandomization n₁ hn have hn1R : (n₁ : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hn1) have hNpos : 0 < Fintype.card U := lt_of_lt_of_le hn1 hn have hNR : (Fintype.card U : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hNpos) have hterm (i : U) : D.E (fun S : {S : Finset U // S.card = n₁} => if i ∈ S.val then Y1 i else 0) = Y1 i * ((n₁ : ℝ) / (Fintype.card U : ℝ)) := by calc D.E (fun S : {S : Finset U // S.card = n₁} => if i ∈ S.val then Y1 i else 0) = D.E (fun S : {S : Finset U // S.card = n₁} => Y1 i * FiniteDesign.ind (fun T : {S : Finset U // S.card = n₁} => i ∈ T.val) S) := by exact D.E_congr (fun S => by unfold FiniteDesign.ind by_cases h : i ∈ S.val <;> simp [h]) _ = Y1 i * D.E (FiniteDesign.ind (fun T : {S : Finset U // S.card = n₁} => i ∈ T.val)) := by rw [FiniteDesign.E_const_mul] _ = Y1 i * D.Pr (fun T : {S : Finset U // S.card = n₁} => i ∈ T.val) := by rw [FiniteDesign.E_ind] _ = Y1 i * ((n₁ : ℝ) / (Fintype.card U : ℝ)) := by rw [completeRandomization_incl] calc D.E (treatedMean n₁ Y1) = D.E (fun S : {S : Finset U // S.card = n₁} => (∑ i, (if i ∈ S.val then Y1 i else 0)) * (1 / (n₁ : ℝ))) := by exact D.E_congr (fun S => by unfold treatedMean rw [div_eq_mul_inv, one_div]) _ = D.E (fun S : {S : Finset U // S.card = n₁} => ∑ i, (if i ∈ S.val then Y1 i else 0)) * (1 / (n₁ : ℝ)) := by rw [FiniteDesign.E_mul_const] _ = (∑ i, D.E (fun S : {S : Finset U // S.card = n₁} => if i ∈ S.val then Y1 i else 0)) * (1 / (n₁ : ℝ)) := by rw [FiniteDesign.E_sum] _ = (∑ i, Y1 i * ((n₁ : ℝ) / (Fintype.card U : ℝ))) * (1 / (n₁ : ℝ)) := by congr 1 exact Finset.sum_congr rfl (fun i _ => hterm i) _ = (∑ i, Y1 i) / (Fintype.card U : ℝ) := by rw [← Finset.sum_mul] field_simp [hn1R, hNR] -
E_controlMeantheorem — The control-arm mean is unbiased for the control population mean (1/N) ∑ Y0. Each unit enters the control arm with probability n₀ / N.hypothesesU :sharedType u_1n₁ :ℕhn0 :n₁ < Fintype.card UY0 :U → ℝconclusion= (∑ i, Y0 i) / (Fintype.card U : ℝ)Proof (Lean source)
theorem E_controlMean (n₁ : ℕ) (hn0 : n₁ < Fintype.card U) (Y0 : U → ℝ) : (completeRandomization n₁ (le_of_lt hn0)).E (controlMean n₁ Y0) = (∑ i, Y0 i) / (Fintype.card U : ℝ) := by have hn : n₁ ≤ Fintype.card U := le_of_lt hn0 let D := completeRandomization n₁ hn have hNpos : 0 < Fintype.card U := lt_of_le_of_lt (zero_le n₁) hn0 have hNR : (Fintype.card U : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hNpos) have hdenNat : (Fintype.card U - n₁ : ℕ) ≠ 0 := Nat.sub_ne_zero_of_lt hn0 have hdenR : ((Fintype.card U - n₁ : ℕ) : ℝ) ≠ 0 := by exact_mod_cast hdenNat have hdiffR : (Fintype.card U : ℝ) - (n₁ : ℝ) ≠ 0 := by have hlt : (n₁ : ℝ) < (Fintype.card U : ℝ) := by exact_mod_cast hn0 exact ne_of_gt (sub_pos.mpr hlt) have hterm (i : U) : D.E (fun S : {S : Finset U // S.card = n₁} => if i ∈ S.val then 0 else Y0 i) = Y0 i * (1 - (n₁ : ℝ) / (Fintype.card U : ℝ)) := by calc D.E (fun S : {S : Finset U // S.card = n₁} => if i ∈ S.val then 0 else Y0 i) = D.E (fun S : {S : Finset U // S.card = n₁} => Y0 i * (1 - FiniteDesign.ind (fun T : {S : Finset U // S.card = n₁} => i ∈ T.val) S)) := by exact D.E_congr (fun S => by unfold FiniteDesign.ind by_cases h : i ∈ S.val <;> simp [h]) _ = Y0 i * D.E (fun S : {S : Finset U // S.card = n₁} => 1 - FiniteDesign.ind (fun T : {S : Finset U // S.card = n₁} => i ∈ T.val) S) := by rw [FiniteDesign.E_const_mul] _ = Y0 i * (D.E (fun _ : {S : Finset U // S.card = n₁} => 1) - D.E (FiniteDesign.ind (fun T : {S : Finset U // S.card = n₁} => i ∈ T.val))) := by rw [FiniteDesign.E_sub] _ = Y0 i * (1 - D.Pr (fun T : {S : Finset U // S.card = n₁} => i ∈ T.val)) := by rw [FiniteDesign.E_const, FiniteDesign.E_ind] _ = Y0 i * (1 - (n₁ : ℝ) / (Fintype.card U : ℝ)) := by rw [completeRandomization_incl] calc D.E (controlMean n₁ Y0) = D.E (fun S : {S : Finset U // S.card = n₁} => (∑ i, (if i ∈ S.val then 0 else Y0 i)) * (1 / ((Fintype.card U - n₁ : ℕ) : ℝ))) := by exact D.E_congr (fun S => by unfold controlMean rw [div_eq_mul_inv, one_div]) _ = D.E (fun S : {S : Finset U // S.card = n₁} => ∑ i, (if i ∈ S.val then 0 else Y0 i)) * (1 / ((Fintype.card U - n₁ : ℕ) : ℝ)) := by rw [FiniteDesign.E_mul_const] _ = (∑ i, D.E (fun S : {S : Finset U // S.card = n₁} => if i ∈ S.val then 0 else Y0 i)) * (1 / ((Fintype.card U - n₁ : ℕ) : ℝ)) := by rw [FiniteDesign.E_sum] _ = (∑ i, Y0 i * (1 - (n₁ : ℝ) / (Fintype.card U : ℝ))) * (1 / ((Fintype.card U - n₁ : ℕ) : ℝ)) := by congr 1 exact Finset.sum_congr rfl (fun i _ => hterm i) _ = (∑ i, Y0 i) / (Fintype.card U : ℝ) := by rw [← Finset.sum_mul] rw [Nat.cast_sub hn] field_simp [hNR, hdenR, hdiffR] -
unbiased_diffInMeanstheorem — The difference in means is unbiased for the SATE, in the Unbiased predicate form.hypothesesconclusionProof (Lean source)
theorem unbiased_diffInMeans (n₁ : ℕ) (hn1 : 0 < n₁) (hn0 : n₁ < card U) (Y1 Y0 : U → ℝ) : (completeRandomization n₁ (le_of_lt hn0)).Unbiased (diffInMeans n₁ Y1 Y0) (sateEstimand Y1 Y0) := E_diffInMeans_eq_sate n₁ hn1 hn0 Y1 Y0
NeymanVariance 10 core · 0 supporting This module contains the paper-independent finite-population arm variances, unit-effect variance, and observed separate-arm variance estimator used by Neyman's complete-randomization formula.
Generic finite-population variance quantities for two-arm designs
This module contains the paper-independent finite-population arm variances, unit-effect variance, and observed separate-arm variance estimator used by Neyman's complete-randomization formula. They live in the design-based layer so interference models can import them without reversing the library's dependency direction.
For a population of n units and a unit, the treatment indicator is one when the Boolean assignment treats that unit and zero otherwise.
For a population of n units and a real quantity for every unit, the finite-population mean is the unit sum divided by n.
Definition (Lean source)
For a population of n units and treated potential outcomes, the treated finite-population sample variance uses denominator n-1.
For a population of n units and control potential outcomes, the control finite-population sample variance uses denominator n-1.
For a population of n units, treated potential outcomes, and control potential outcomes, the finite-population sample variance of unit treatment effects uses denominator n-1.
For a treated count, treated outcomes, and a Boolean assignment, the observed treated-arm mean averages treated outcomes over the treated count.
For a treated count, control outcomes, and a Boolean assignment, the observed control-arm mean averages control outcomes over the control count.
For a treated count, treated outcomes, and a Boolean assignment, the observed treated-arm sample variance uses denominator K-1.
Definition (Lean source)
For a treated count, control outcomes, and a Boolean assignment, the observed control-arm sample variance uses denominator n-K-1.
Definition (Lean source)
For a treated count, treated and control outcomes, and a Boolean assignment, the usual conservative variance estimator is the sum of the observed arm sample variances divided by their arm sizes.