Experimentation.UnknownInterference
Formalization of the Bernoulli-design core of Sävje, Aronow & Hudgens (2021), "Average treatment effects in the presence of unknown interference," *Annals of Statistics* 49(2):673–701 (arXiv:1711.06399).
Basic 10 core · 2 supporting The setup for "Average treatment effects in the presence of unknown interference" (Sävje, Aronow & Hudgens, *Annals of Statistics* 49(2), 2021). ★ Interferes★ EATE★ y_eq_of_agree_on_interferers
Sävje–Aronow–Hudgens (2021): EATE estimand and the Horvitz–Thompson estimator
The setup for "Average treatment effects in the presence of unknown interference"
(Sävje, Aronow & Hudgens, Annals of Statistics 49(2), 2021). A finite sample of units U
is assigned a binary treatment vector z : U → Bool by a randomization design. Each unit's
outcome y i z may depend on the entire assignment z — units interfere — but the form of
the interference is unknown.
This file fixes the primitives:
* the interference indicator Interferes y ℓ i (changing ℓ's treatment changes i's
outcome under some assignment, plus the reflexive case ℓ = i), its symmetric closure
InterfDep y i j (some ℓ interferes with both i and j), and the average interference
dependence dbar (the paper's d̄, the basis for the "restricted interference" assumption);
* the assignment-conditional unit-level effect `tau y i z = y i (z with iᵗʰ coord 1) −
y i (z with iᵗʰ coord 0), its average ACATE` (assignment-conditional ATE), and the
expected average treatment effect EATE = E[ACATE(Z)] (Definition: the design average of
the assignment-conditional ATE);
* the Horvitz–Thompson estimator htEst.
The key structural fact proven here is y_eq_of_agree_on_interferers: a unit's outcome depends
only on the treatments of the units that interfere with it — the bridge that turns
"InterfDep fails" into "the two HT summands depend on disjoint coordinate blocks", which the
disjoint-block independence lemma then turns into a vanishing covariance.
For a population of units, a potential-outcome schedule, and two units, the potential source unit and the affected unit, the interference indicator holds exactly when the units are identical or there is an assignment under which reversing the source unit's treatment changes the affected unit's outcome.
For a population of units, a potential-outcome schedule, and two units, the interference-dependence relation holds exactly when some unit's treatment interferes with both units' outcomes; equivalently, the two outcomes may be affected by a common treatment.
Definition (Lean source)
For a finite population of units and a potential-outcome schedule, the unnormalized interference-dependence count is the number of ordered pairs of units that are interference dependent.
For a finite population of units and a potential-outcome schedule, the average interference dependence is the unnormalized count of interference-dependent ordered pairs divided by the population size. For a nonempty population it equals one under no interference and the population size when every ordered pair is interference dependent; restricted interference is the condition that it is of smaller order than the population size.
For a population of units, a potential-outcome schedule, a unit, and an assignment of treatments to all units, the assignment-conditional unit-level treatment effect is that unit's outcome when its own treatment is set to treated minus its outcome when its own treatment is set to control, with every other unit's assignment held fixed.
For a finite population of units, a potential-outcome schedule, and an assignment of treatments to all units, the assignment-conditional average treatment effect is the average, over all units, of their own-treatment effects with the remaining assignments held fixed.
For a finite population of units, a randomization design over treatment assignments, and a potential-outcome schedule, the expected average treatment effect is the design expectation of the assignment-conditional average treatment effect. Under no interference this quantity equals the conventional average treatment effect because the assignment-conditional effect is then constant across assignments.
Definition (Lean source)
For a population of units, marginal treatment probabilities, a potential-outcome schedule, a unit, and a realized treatment assignment, the unit-level Horvitz--Thompson summand is its observed outcome weighted by the reciprocal of its treatment probability if treated, minus the same outcome weighted by the reciprocal of its control probability if untreated.
For a finite population of units, marginal treatment probabilities, a potential-outcome schedule, and a realized treatment assignment, the Horvitz--Thompson estimator is the average of the units' treated-minus-control inverse-probability-weighted outcome summands.
A unit's outcome depends only on the units that interfere with it. If two treatment assignments z and z' agree on every unit that interferes with unit i, then unit i's outcome is the same under both assignments: y i z = y i z'.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
one_le_dbartheorem — For a nonempty finite population, average interference dependence is at least one, because every unit is interference-dependent with itself.hypothesesconclusion(1 : ℝ) ≤ dbar yProof (Lean source)
theorem one_le_dbar (y : U → (U → Bool) → ℝ) (hcard : 1 ≤ Fintype.card U) : (1 : ℝ) ≤ dbar y := by classical have hn0 : (0 : ℝ) < (Fintype.card U : ℝ) := by exact_mod_cast lt_of_lt_of_le zero_lt_one hcard have hdiag : ∀ i : U, InterfDep y i i := fun i => ⟨i, Or.inl rfl, Or.inl rfl⟩ have hcount : (Fintype.card U : ℝ) ≤ dbarCount y := by rw [dbarCount] calc (Fintype.card U : ℝ) = ∑ _i : U, (1 : ℝ) := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one] _ = ∑ i : U, (if InterfDep y i i then (1 : ℝ) else 0) := by refine Finset.sum_congr rfl (fun i _ => ?_) rw [if_pos (hdiag i)] _ ≤ ∑ i : U, ∑ j : U, (if InterfDep y i j then (1 : ℝ) else 0) := by refine Finset.sum_le_sum (fun i _ => ?_) refine Finset.single_le_sum (f := fun j => if InterfDep y i j then (1 : ℝ) else 0) (fun j _ => ?_) (Finset.mem_univ i) by_cases h : InterfDep y i j <;> simp [h] rw [dbar, le_div_iff₀ hn0, one_mul] exact hcount -
y_update_eq_of_not_interfereslemma — When unit ℓ does not interfere with unit i, flipping ℓ's treatment while holding every other unit's assignment fixed never changes i's realized outcome.hypothesesconclusiony i z = y i (update z ℓ (! z ℓ))Proof (Lean source)
lemma y_update_eq_of_not_interferes {y : U → (U → Bool) → ℝ} {ℓ i : U} (h : ¬ Interferes y ℓ i) (z : U → Bool) : y i z = y i (update z ℓ (! z ℓ)) := by by_contra hne exact h (inr ⟨z, hne⟩)
Consistency 6 core · 4 supporting Horvitz-Thompson estimates the expected average treatment effect consistently when average interference is sparse. ★ D_E_htEst★ htEst_consistent_eate★ root_n_var
Consistency under unknown interference
Horvitz-Thompson estimates the expected average treatment effect consistently when average interference is sparse.
The SAHExperiment structure packages one Sävje-Aronow-Hudgens Bernoulli experiment, including
overlap, moment, and regularity bounds. Exact unbiasedness and the variance bound
Var(ĤT) ≤ k^4 * dbar / n give a Chebyshev tail bound. Along a sequence of experiments, this
proves convergence in probability whenever that upper bound tends to zero, without requiring the
interference graph itself to be known.
The file also records root-n variance control when average interference and the regularity constant are uniformly bounded.
A single Sävje–Aronow–Hudgens Bernoulli experiment, packaged so that a sequence of them models the growing-sample regime. Carries a finite population of units, marginal treatment probabilities, and potential outcomes indexed by the full assignment vector, together with an overlap regularity constant k at least one; the conditions that there is at least one unit, every treatment probability lies between 0 and 1, is bounded below by 1/k and above by 1 − 1/k (overlap); and every unit's potential outcome has second moment at most k² under the resulting Bernoulli design.
Definition (Lean source)
For a packaged Sävje--Aronow--Hudgens experiment, the experiment's Bernoulli randomization design independently assigns each unit treatment according to that experiment's stated marginal treatment probabilities.
Definition (Lean source)
For a packaged Sävje--Aronow--Hudgens experiment, the experiment's expected average treatment-effect estimand is the expectation, under its Bernoulli randomization design, of the assignment-conditional average treatment effect determined by its potential outcomes.
Definition (Lean source)
Unbiasedness (bundle form). The Horvitz–Thompson estimator's expectation under the experiment's Bernoulli design equals the experiment's EATE estimand.
Formal statement
Proof (Lean source)
Consistency of Horvitz–Thompson for EATE under unknown interference (Sävje–Aronow–Hudgens 2021). Along a sequence of Bernoulli experiments along which k⁴·d̄/n → 0 — restricted interference with a controlled regularity constant, for every fixed deviation threshold ε > 0, the probability that the Horvitz–Thompson estimator deviates from the EATE by at least ε tends to zero along the sequence, i.e. the HT estimator converges in probability to the EATE.
Formal statement
Proof (Lean source)
Root-n variance scaling under bounded interference (Sävje–Aronow–Hudgens 2021). In one bundled experiment, if the average interference degree d̄ is bounded above by a constant C, then the sample size n times the variance of the Horvitz–Thompson estimator is at most k⁴·C, where k is the experiment's regularity constant — the finite-sample variance inequality that supports a root-n rate in bounded-interference sequences.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
p_ne_zerolemma — The treatment probabilities are nonzero (from lower overlap).Proof (Lean source)
lemma p_ne_zero (i : E.U) : E.p i ≠ 0 := by have hkpos : (0 : ℝ) < E.k := lt_of_lt_of_le zero_lt_one E.hk have : (0 : ℝ) < E.p i := lt_of_lt_of_le (by positivity) (E.hplo i) exact ne_of_gt this -
one_sub_p_ne_zerolemma — One minus the treatment probability is nonzero (from upper overlap).Proof (Lean source)
lemma one_sub_p_ne_zero (i : E.U) : (1 : ℝ) - E.p i ≠ 0 := by have hkpos : (0 : ℝ) < E.k := lt_of_lt_of_le zero_lt_one E.hk have hkinv : (0 : ℝ) < E.k⁻¹ := by positivity have : (0 : ℝ) < 1 - E.p i := by have := E.hphi i linarith exact ne_of_gt this -
D_Var_htEst_letheorem — Variance bound (bundle form). The Horvitz–Thompson estimator's variance is at most the fourth power of the regularity constant times the average interference degree, divided by the population size.hypothesesProof (Lean source)
theorem D_Var_htEst_le : E.D.Var (htEst E.p E.y) ≤ E.k ^ 4 * dbar E.y / (Fintype.card E.U : ℝ) := by unfold SAHExperiment.D exact var_htEst_le E.p E.hp0 E.hp1 E.y E.k E.hk E.hcard E.hplo E.hphi E.hmom -
chebyshev_eatetheorem — Chebyshev tail bound. For any deviation threshold ε > 0, the probability that the Horvitz–Thompson estimator deviates from the EATE by at least ε is at most (k⁴·d̄/n)/ε², where k is the experiment's regularity constant, d̄ is the average interference degree, and n is the population size.hypothesesProof (Lean source)
theorem chebyshev_eate {ε : ℝ} (hε : 0 < ε) : E.D.Pr (fun z => ε ≤ |htEst E.p E.y z - E.eate|) ≤ (E.k ^ 4 * dbar E.y / (Fintype.card E.U : ℝ)) / ε ^ 2 := by have hcheb := FiniteDesign.chebyshev E.D (htEst E.p E.y) hε rw [E.D_E_htEst] at hcheb have hε2 : (0 : ℝ) < ε ^ 2 := pow_pos hε 2 refine le_trans hcheb ?_ exact div_le_div_of_nonneg_right E.D_Var_htEst_le hε2.le
Confidence 5 core · 1 supporting Under unknown interference, off-diagonal covariance can make the conventional Horvitz–Thompson variance estimator anti-conservative. ★ E_VhatBer_bias★ var_htEst_le_inflated★ eate_ci_kbound
Confidence under unknown interference
Under unknown interference, off-diagonal covariance can make the conventional Horvitz–Thompson variance estimator anti-conservative. This file gives its exact finite-sample expectation-bias identity and proves that degree-based inflation is conservative in expectation when every unit has bounded interference degree.
The confidence results use Chebyshev's inequality rather than a normal approximation. Any positive
deterministic upper bound on the estimator variance yields a finite-sample interval with coverage
at least 1 − α; the final theorem uses the bound k^4 * dbar / n. These results do not claim
that a data-dependent variance estimator is asymptotically conservative in probability, which
would additionally require concentration of that estimator.
For a finite population of units, marginal treatment probabilities, a potential-outcome schedule, and a realized treatment assignment, the conventional Horvitz--Thompson variance estimator is the population-size-squared-normalized sum of squared unit-level Horvitz--Thompson summands. Pointwise it equals the sum of the treated and control squared inverse-probability-weighted outcome terms because their cross product is zero.
For a finite population of units, a potential-outcome schedule, and a unit, the interference degree is the number of units that are interference dependent with that unit.
The anti-conservativeness mechanism (Sävje–Aronow–Hudgens 2021). Under the Bernoulli design with per-unit treatment probabilities p taking values in [0, 1], the conventional variance estimator's expected value equals Var(ĤT) + n⁻²·(∑ᵢ(E ĤTᵢ)² − ∑ᵢ∑_{j≠i} Cov(ĤTᵢ,ĤTⱼ)): the true sampling variance of the Horvitz–Thompson estimator, plus the average squared per-unit mean, minus the off-diagonal covariances between units' Horvitz–Thompson summands.
Formal statement
Proof (Lean source)
Conservative inflation (Sävje–Aronow–Hudgens 2021). Under the Bernoulli design with per-unit treatment probabilities p taking values in [0, 1], if every unit's interference degree — the number of units it is interference-dependent with — is at most a bound D, then inflating the conventional variance estimator's expectation by a factor 1 + D gives a conservative bound on the Horvitz–Thompson estimator's true variance: Var(ĤT) ≤ (1 + D)·E[V̂_Ber].
Formal statement
Proof (Lean source)
A concrete finite-sample confidence interval for EATE (Sävje–Aronow–Hudgens 2021). Suppose the Bernoulli design has treatment probabilities p that lie in [0, 1], are never exactly zero or one, and in fact stay within [1/k, 1 - 1/k] for some regularity constant k ≥ 1; suppose also that the population is nonempty, every unit's outcome has second moment at most k², and the analyst supplies an upper bound D₀ on the average interference degree, while the significance level α is positive. Then the Chebyshev interval ĤT ± √(k⁴·D₀/(n·α)), where n is the population size, covers the EATE estimand with probability at least 1 − α — a valid (conservative) interval that needs only the regularity constant k and the supplied interference bound D₀.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
chebyshev_ci_eatetheorem — Chebyshev confidence interval for EATE. For the Bernoulli design with per-unit treatment probabilities p that take values in [0, 1] and are never exactly zero or one, for any value V that is positive and bounds the Horvitz–Thompson estimator's true sampling variance from above, and for any positive significance level α, the interval ĤT ± √(V/α) covers the EATE estimand with probability at least 1 − α.hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1hp0' :∀ i, p i ≠ 0hp1' :∀ i, (1 : ℝ) - p i ≠ 0y :U → (U → Bool) → ℝV α :ℝhV0 :0 < Vhα :0 < αProof (Lean source)
theorem chebyshev_ci_eate (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (hp0' : ∀ i, p i ≠ 0) (hp1' : ∀ i, (1 : ℝ) - p i ≠ 0) (y : U → (U → Bool) → ℝ) {V α : ℝ} (hV0 : 0 < V) (hV : (DesignBased.bernoulliDesign p hp0 hp1).Var (htEst p y) ≤ V) (hα : 0 < α) : 1 - α ≤ (DesignBased.bernoulliDesign p hp0 hp1).Pr (fun z => |htEst p y z - EATE (DesignBased.bernoulliDesign p hp0 hp1) y| ≤ sqrt (V / α)) := by classical set D := DesignBased.bernoulliDesign p hp0 hp1 with hD set t : ℝ := sqrt (V / α) with ht have hVα : 0 < V / α := div_pos hV0 hα have ht0 : 0 < t := Real.sqrt_pos.mpr hVα have ht2 : t ^ 2 = V / α := by rw [ht, Real.sq_sqrt (le_of_lt hVα)] have hμ : D.E (htEst p y) = EATE D y := htEst_unbiased p hp0 hp1 hp0' hp1' y -- Chebyshev: Pr(t ≤ |htEst - EATE|) ≤ Var / t² have hcheb := D.chebyshev (htEst p y) ht0 rw [hμ] at hcheb set A : (U → Bool) → Prop := fun z => |htEst p y z - EATE D y| ≤ t with hA set B : (U → Bool) → Prop := fun z => t ≤ |htEst p y z - EATE D y| with hB -- Pr B ≤ α. have hVt : D.Var (htEst p y) / t ^ 2 ≤ α := by rw [ht2] have hstep : D.Var (htEst p y) / (V / α) ≤ V / (V / α) := div_le_div_of_nonneg_right hV (by positivity) have hVdiv : V / (V / α) = α := by field_simp rw [hVdiv] at hstep; exact hstep have hPrB : D.Pr B ≤ α := le_trans hcheb hVt -- A and B cover everything: ind A + ind B ≥ 1 pointwise. have hcover : ∀ z, (1 : ℝ) ≤ FiniteDesign.ind A z + FiniteDesign.ind B z := by intro z rcases le_total (|htEst p y z - EATE D y|) t with h | h · have hi : FiniteDesign.ind A z = 1 := by unfold FiniteDesign.ind A; simp [h] have hBn : 0 ≤ FiniteDesign.ind B z := FiniteDesign.ind_nonneg B z rw [hi]; linarith · have hi : FiniteDesign.ind B z = 1 := by unfold FiniteDesign.ind B; simp [h] have hAn : 0 ≤ FiniteDesign.ind A z := FiniteDesign.ind_nonneg A z rw [hi]; linarith -- 1 = E[1] ≤ E[ind A + ind B] = Pr A + Pr B. have h1le : (1 : ℝ) ≤ D.Pr A + D.Pr B := by have hEmono : D.E (fun _ => (1 : ℝ)) ≤ D.E (fun z => FiniteDesign.ind A z + FiniteDesign.ind B z) := by unfold FiniteDesign.E exact Finset.sum_le_sum (fun z _ => mul_le_mul_of_nonneg_left (hcover z) (D.p_nonneg z)) rw [D.E_const, D.E_add] at hEmono change (1 : ℝ) ≤ D.E (FiniteDesign.ind A) + D.E (FiniteDesign.ind B) exact hEmono linarith [hPrB, h1le]
Hajek 10 core · 9 supporting The Hájek estimator normalizes treated and control inverse-probability-weighted outcome sums by their realized weight sums rather than by population size. ★ hajekEst★ hajek_consistent_eate
Hájek estimation under unknown interference
The Hájek estimator normalizes treated and control inverse-probability-weighted outcome sums by their realized weight sums rather than by population size. This file defines the treated and control numerators and denominators and proves their mean and variance controls under Bernoulli assignment.
Under vanishing interference variance, the two numerators converge to their population targets and the two weight denominators converge to one. A finite-design Slutsky argument then gives consistency for the Sävje-Aronow-Hudgens expected average treatment effect. The result also assumes uniform regularity and absolute potential-outcome moment bounds needed to control the ratio limits.
For a population of units, marginal treatment probabilities, a potential-outcome schedule, a unit, and a realized treatment assignment, the treated Horvitz--Thompson summand is that unit's observed outcome multiplied by its treatment indicator and divided by its treatment probability.
For a population of units, marginal treatment probabilities, a potential-outcome schedule, a unit, and a realized treatment assignment, the control Horvitz--Thompson summand is that unit's observed outcome multiplied by its control indicator and divided by its control probability.
For a population of units, marginal treatment probabilities, a unit, and a realized treatment assignment, the treated inverse-probability weight summand is the unit's treatment indicator divided by its treatment probability.
Definition (Lean source)
For a population of units, marginal treatment probabilities, a unit, and a realized treatment assignment, the control inverse-probability weight summand is the unit's control indicator divided by its control probability.
Definition (Lean source)
For a finite population of units, marginal treatment probabilities, a potential-outcome schedule, and a realized treatment assignment, the treated numerator average is the population average of the treated Horvitz--Thompson summands.
Definition (Lean source)
For a finite population of units, marginal treatment probabilities, a potential-outcome schedule, and a realized treatment assignment, the control numerator average is the population average of the control Horvitz--Thompson summands.
Definition (Lean source)
For a finite population of units, marginal treatment probabilities, and a realized treatment assignment, the treated weight average is the population average of the treated inverse-probability weight summands.
Definition (Lean source)
For a finite population of units, marginal treatment probabilities, and a realized treatment assignment, the control weight average is the population average of the control inverse-probability weight summands.
Definition (Lean source)
For a finite population of units, marginal treatment probabilities, a potential-outcome schedule, and a realized treatment assignment, the Hájek estimator is the treated numerator average divided by the treated weight average, minus the control numerator average divided by the control weight average.
Consistency of the Hájek estimator for EATE (Sävje–Aronow–Hudgens 2021). Along a sequence of Bernoulli experiments for which the regularity constants are uniformly bounded above by a constant M, k⁴·d̄/n → 0 along the sequence — restricted interference, and the mean absolute treated and control potential outcomes are each bounded by that experiment's own regularity constant k (the paper's Assumption C), the Hájek estimator converges in probability to the EATE.
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
E_BhatTreattheorem — With nonzero treatment propensities and a nonempty population, the treated weight average has mean exactly one: E[B̂₁] = 1.hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1hp0' :∀ i, p i ≠ 0hcard :1 ≤ card Uconclusion(DesignBased.bernoulliDesign p hp0 hp1).E (BhatTreat p) = 1Proof (Lean source)
theorem E_BhatTreat (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (hp0' : ∀ i, p i ≠ 0) (hcard : 1 ≤ Fintype.card U) : (DesignBased.bernoulliDesign p hp0 hp1).E (BhatTreat p) = 1 := by set D := DesignBased.bernoulliDesign p hp0 hp1 with hD set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : n ≠ 0 := by rw [hn]; exact_mod_cast Nat.one_le_iff_ne_zero.mp hcard have h1 : D.E (BhatTreat p) = (1 / n) * ∑ i : U, D.E (weightTreatSummand p i) := by have hcongr : ∀ z, BhatTreat p z = (1 / n) * ∑ i : U, weightTreatSummand p i z := by intro z; rw [BhatTreat, hn]; ring rw [D.E_congr hcongr, D.E_const_mul, D.E_sum] have h2 : ∀ i : U, D.E (weightTreatSummand p i) = 1 := by intro i have hc : ∀ z, weightTreatSummand p i z = (1 / p i) * (if z i then (1 : ℝ) else 0) := by intro z; rw [weightTreatSummand]; ring rw [D.E_congr hc, D.E_const_mul] have : D.E (fun z => if z i then (1 : ℝ) else 0) = p i := by rw [hD]; exact DesignBased.bernoulliDesign_E_treat p hp0 hp1 i rw [this]; field_simp [hp0' i] rw [h1] simp only [h2, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one] rw [← hn]; field_simp -
E_BhatCtrltheorem — With nonzero control propensities and a nonempty population, the control weight average has mean exactly one: E[B̂₀] = 1.hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1hp1' :∀ i, (1 : ℝ) - p i ≠ 0hcard :1 ≤ card Uconclusion(DesignBased.bernoulliDesign p hp0 hp1).E (BhatCtrl p) = 1Proof (Lean source)
theorem E_BhatCtrl (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (hp1' : ∀ i, (1 : ℝ) - p i ≠ 0) (hcard : 1 ≤ Fintype.card U) : (DesignBased.bernoulliDesign p hp0 hp1).E (BhatCtrl p) = 1 := by set D := DesignBased.bernoulliDesign p hp0 hp1 with hD set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : n ≠ 0 := by rw [hn]; exact_mod_cast Nat.one_le_iff_ne_zero.mp hcard have h1 : D.E (BhatCtrl p) = (1 / n) * ∑ i : U, D.E (weightCtrlSummand p i) := by have hcongr : ∀ z, BhatCtrl p z = (1 / n) * ∑ i : U, weightCtrlSummand p i z := by intro z; rw [BhatCtrl, hn]; ring rw [D.E_congr hcongr, D.E_const_mul, D.E_sum] have h2 : ∀ i : U, D.E (weightCtrlSummand p i) = 1 := by intro i have hc : ∀ z, weightCtrlSummand p i z = (1 / (1 - p i)) * (if z i then (0 : ℝ) else 1) := by intro z; rw [weightCtrlSummand]; ring rw [D.E_congr hc, D.E_const_mul] have : D.E (fun z => if z i then (0 : ℝ) else 1) = 1 - p i := by rw [hD]; exact DesignBased.bernoulliDesign_E_ctrl p hp0 hp1 i rw [this]; field_simp [hp1' i] rw [h1] simp only [h2, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one] rw [← hn]; field_simp -
var_AhatTreat_letheorem — Variance bound for the treated numerator average: Var(Â₁) ≤ k⁴·d̄/n (same disjoint-block argument as the HT estimator).hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1y :U → (U → Bool) → ℝk :ℝhk :1 ≤ khcard :1 ≤ Fintype.card Uhplo :∀ i, k⁻¹ ≤ p ihmom :∀ i, (DesignBased.bernoulliDesign p hp0 hp1).E (fun z => (y i z) ^ 2) ≤ k ^ 2Proof (Lean source)
theorem var_AhatTreat_le (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (y : U → (U → Bool) → ℝ) (k : ℝ) (hk : 1 ≤ k) (hcard : 1 ≤ Fintype.card U) (hplo : ∀ i, k⁻¹ ≤ p i) (hmom : ∀ i, (DesignBased.bernoulliDesign p hp0 hp1).E (fun z => (y i z) ^ 2) ≤ k ^ 2) : (DesignBased.bernoulliDesign p hp0 hp1).Var (AhatTreat p y) ≤ k ^ 4 * dbar y / (Fintype.card U : ℝ) := by classical set D := DesignBased.bernoulliDesign p hp0 hp1 with hD set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : (0 : ℝ) < n := by rw [hn]; exact_mod_cast lt_of_lt_of_le zero_lt_one hcard have hcov : ∀ i j, D.Cov (htTreatSummand p y i) (htTreatSummand p y j) ≤ (if InterfDep y i j then (k ^ 4 : ℝ) else 0) := by intro i j by_cases hdep : InterfDep y i j · rw [if_pos hdep] have hVsub : 0 ≤ D.Var (fun z => htTreatSummand p y i z - htTreatSummand p y j z) := D.Var_nonneg _ rw [D.Var_sub] at hVsub have hVi : D.Var (htTreatSummand p y i) ≤ k ^ 4 := var_htTreatSummand_le p hp0 hp1 y k hk hplo hmom i have hVj : D.Var (htTreatSummand p y j) ≤ k ^ 4 := var_htTreatSummand_le p hp0 hp1 y k hk hplo hmom j linarith · rw [if_neg hdep] exact le_of_eq (cov_htTreatSummand_zero p hp0 hp1 y hdep) have hEstEq : AhatTreat p y = fun z => n⁻¹ * ∑ i : U, (1 : ℝ) * htTreatSummand p y i z := by funext z; unfold AhatTreat; rw [hn, div_eq_inv_mul]; congr 1 exact Finset.sum_congr rfl (fun i _ => (one_mul _).symm) have hVarEst : D.Var (AhatTreat p y) = (n⁻¹) ^ 2 * ∑ i : U, ∑ j : U, D.Cov (htTreatSummand p y i) (htTreatSummand p y j) := by rw [hEstEq, D.Var_const_mul, D.Var_linear_comb univ (fun _ => (1 : ℝ)) (htTreatSummand p y)] congr 1 refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_)) rw [one_mul, one_mul] have hsumle : (∑ i : U, ∑ j : U, D.Cov (htTreatSummand p y i) (htTreatSummand p y j)) ≤ k ^ 4 * dbarCount y := by have hstep : (∑ i : U, ∑ j : U, D.Cov (htTreatSummand p y i) (htTreatSummand p y j)) ≤ ∑ i : U, ∑ j : U, (if InterfDep y i j then (k ^ 4 : ℝ) else 0) := Finset.sum_le_sum (fun i _ => Finset.sum_le_sum (fun j _ => hcov i j)) refine le_trans hstep ?_ rw [dbarCount, Finset.mul_sum] refine Finset.sum_le_sum (fun i _ => ?_) rw [Finset.mul_sum] refine Finset.sum_le_sum (fun j _ => ?_) by_cases hdep : InterfDep y i j <;> simp [hdep] rw [hVarEst] have hninv2 : (0 : ℝ) ≤ (n⁻¹) ^ 2 := sq_nonneg _ calc (n⁻¹) ^ 2 * ∑ i : U, ∑ j : U, D.Cov (htTreatSummand p y i) (htTreatSummand p y j) ≤ (n⁻¹) ^ 2 * (k ^ 4 * dbarCount y) := mul_le_mul_of_nonneg_left hsumle hninv2 _ = k ^ 4 * dbar y / n := by rw [dbar, hn]; ring -
var_AhatCtrl_letheorem — Variance bound for the control numerator average: Var(Â₀) ≤ k⁴·d̄/n.hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1y :U → (U → Bool) → ℝk :ℝhk :1 ≤ khcard :1 ≤ Fintype.card Uhphi :∀ i, p i ≤ 1 - k⁻¹hmom :∀ i, (DesignBased.bernoulliDesign p hp0 hp1).E (fun z => (y i z) ^ 2) ≤ k ^ 2Proof (Lean source)
theorem var_AhatCtrl_le (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (y : U → (U → Bool) → ℝ) (k : ℝ) (hk : 1 ≤ k) (hcard : 1 ≤ Fintype.card U) (hphi : ∀ i, p i ≤ 1 - k⁻¹) (hmom : ∀ i, (DesignBased.bernoulliDesign p hp0 hp1).E (fun z => (y i z) ^ 2) ≤ k ^ 2) : (DesignBased.bernoulliDesign p hp0 hp1).Var (AhatCtrl p y) ≤ k ^ 4 * dbar y / (Fintype.card U : ℝ) := by classical set D := DesignBased.bernoulliDesign p hp0 hp1 with hD set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : (0 : ℝ) < n := by rw [hn]; exact_mod_cast lt_of_lt_of_le zero_lt_one hcard have hcov : ∀ i j, D.Cov (htCtrlSummand p y i) (htCtrlSummand p y j) ≤ (if InterfDep y i j then (k ^ 4 : ℝ) else 0) := by intro i j by_cases hdep : InterfDep y i j · rw [if_pos hdep] have hVsub : 0 ≤ D.Var (fun z => htCtrlSummand p y i z - htCtrlSummand p y j z) := D.Var_nonneg _ rw [D.Var_sub] at hVsub have hVi : D.Var (htCtrlSummand p y i) ≤ k ^ 4 := var_htCtrlSummand_le p hp0 hp1 y k hk hphi hmom i have hVj : D.Var (htCtrlSummand p y j) ≤ k ^ 4 := var_htCtrlSummand_le p hp0 hp1 y k hk hphi hmom j linarith · rw [if_neg hdep] exact le_of_eq (cov_htCtrlSummand_zero p hp0 hp1 y hdep) have hEstEq : AhatCtrl p y = fun z => n⁻¹ * ∑ i : U, (1 : ℝ) * htCtrlSummand p y i z := by funext z; unfold AhatCtrl; rw [hn, div_eq_inv_mul]; congr 1 exact Finset.sum_congr rfl (fun i _ => (one_mul _).symm) have hVarEst : D.Var (AhatCtrl p y) = (n⁻¹) ^ 2 * ∑ i : U, ∑ j : U, D.Cov (htCtrlSummand p y i) (htCtrlSummand p y j) := by rw [hEstEq, D.Var_const_mul, D.Var_linear_comb univ (fun _ => (1:ℝ)) (htCtrlSummand p y)] congr 1 refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_)) rw [one_mul, one_mul] have hsumle : (∑ i : U, ∑ j : U, D.Cov (htCtrlSummand p y i) (htCtrlSummand p y j)) ≤ k ^ 4 * dbarCount y := by have hstep : (∑ i : U, ∑ j : U, D.Cov (htCtrlSummand p y i) (htCtrlSummand p y j)) ≤ ∑ i : U, ∑ j : U, (if InterfDep y i j then (k ^ 4 : ℝ) else 0) := Finset.sum_le_sum (fun i _ => Finset.sum_le_sum (fun j _ => hcov i j)) refine le_trans hstep ?_ rw [dbarCount, Finset.mul_sum] refine Finset.sum_le_sum (fun i _ => ?_) rw [Finset.mul_sum] refine Finset.sum_le_sum (fun j _ => ?_) by_cases hdep : InterfDep y i j <;> simp [hdep] rw [hVarEst] have hninv2 : (0 : ℝ) ≤ (n⁻¹) ^ 2 := sq_nonneg _ calc (n⁻¹) ^ 2 * ∑ i : U, ∑ j : U, D.Cov (htCtrlSummand p y i) (htCtrlSummand p y j) ≤ (n⁻¹) ^ 2 * (k ^ 4 * dbarCount y) := mul_le_mul_of_nonneg_left hsumle hninv2 _ = k ^ 4 * dbar y / n := by rw [dbar, hn]; ring -
var_BhatTreat_letheorem — Variance bound for the treated weight average: Var(B̂₁) ≤ k²/n (single-coordinate independence — the weight summands Zᵢ/pᵢ depend on disjoint singletons).hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1k :ℝhk :1 ≤ khcard :1 ≤ Fintype.card Uhplo :∀ i, k⁻¹ ≤ p iProof (Lean source)
theorem var_BhatTreat_le (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (k : ℝ) (hk : 1 ≤ k) (hcard : 1 ≤ Fintype.card U) (hplo : ∀ i, k⁻¹ ≤ p i) : (DesignBased.bernoulliDesign p hp0 hp1).Var (BhatTreat p) ≤ k ^ 2 / (Fintype.card U : ℝ) := by set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : (0 : ℝ) < n := by rw [hn]; exact_mod_cast lt_of_lt_of_le zero_lt_one hcard have hk0 : (0 : ℝ) < k := lt_of_lt_of_le zero_lt_one hk have hkinv0 : (0 : ℝ) < k⁻¹ := inv_pos.mpr hk0 -- single-coordinate function `g_i b = (if b then 1 else 0)/p i` set g : U → Bool → ℝ := fun i b => (if b then (1 : ℝ) else 0) / p i with hg -- `BhatTreat = fun z => ∑ i, (n⁻¹) * g i (z i)` have hBeq : BhatTreat p = fun z => ∑ i : U, n⁻¹ * g i (z i) := by funext z; unfold BhatTreat weightTreatSummand rw [hn, Finset.sum_div] refine Finset.sum_congr rfl (fun i _ => ?_) rw [hg]; ring -- per-coordinate variance bound `Var(g i) ≤ k²` have hVcoord : ∀ i, (coinDesign (p i) (hp0 i) (hp1 i)).Var (g i) ≤ k ^ 2 := by intro i have hpi0 : (0 : ℝ) < p i := lt_of_lt_of_le hkinv0 (hplo i) have hrecp : 1 / p i ≤ k := by rw [div_le_iff₀ hpi0] nlinarith [mul_le_mul_of_nonneg_right (hplo i) (le_of_lt hk0), inv_mul_cancel₀ (ne_of_gt hk0)] have hEsq : (coinDesign (p i) (hp0 i) (hp1 i)).E (fun b => (g i b) ^ 2) = 1 / p i := by have h0 : p i ≠ 0 := ne_of_gt hpi0 rw [coinDesign_E]; simp only [hg]; norm_num; field_simp have hVle : (coinDesign (p i) (hp0 i) (hp1 i)).Var (g i) ≤ (coinDesign (p i) (hp0 i) (hp1 i)).E (fun b => (g i b) ^ 2) := by rw [(coinDesign (p i) (hp0 i) (hp1 i)).Var_eq] linarith [sq_nonneg ((coinDesign (p i) (hp0 i) (hp1 i)).E (g i))] have hk2 : (1 : ℝ) / p i ≤ k ^ 2 := by nlinarith [hrecp, hk] linarith [le_trans hVle (le_of_eq hEsq)] -- apply the product-design linear-combination variance identity rw [hBeq] unfold DesignBased.bernoulliDesign rw [FiniteDesign.Var_prod_linear_comb (fun i => coinDesign (p i) (hp0 i) (hp1 i)) (fun _ => n⁻¹) g] -- `∑ i, (n⁻¹)² · Var(g i) ≤ ∑ i, (n⁻¹)² · k² = n · (n⁻¹)² · k² = k²/n` have hninv2 : (0 : ℝ) ≤ (n⁻¹) ^ 2 := sq_nonneg _ have hstep : (∑ i : U, (n⁻¹) ^ 2 * (coinDesign (p i) (hp0 i) (hp1 i)).Var (g i)) ≤ ∑ _i : U, (n⁻¹) ^ 2 * k ^ 2 := Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_left (hVcoord i) hninv2) refine le_trans hstep ?_ rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, ← hn] rw [show (n : ℝ) * ((n⁻¹) ^ 2 * k ^ 2) = (n * n⁻¹) * (n⁻¹ * k ^ 2) by ring] rw [mul_inv_cancel₀ (ne_of_gt hn0), one_mul, inv_mul_eq_div] -
var_BhatCtrl_letheorem — Variance bound for the control weight average: Var(B̂₀) ≤ k²/n.hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1k :ℝhk :1 ≤ khcard :1 ≤ Fintype.card Uhphi :∀ i, p i ≤ 1 - k⁻¹Proof (Lean source)
theorem var_BhatCtrl_le (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (k : ℝ) (hk : 1 ≤ k) (hcard : 1 ≤ Fintype.card U) (hphi : ∀ i, p i ≤ 1 - k⁻¹) : (DesignBased.bernoulliDesign p hp0 hp1).Var (BhatCtrl p) ≤ k ^ 2 / (Fintype.card U : ℝ) := by set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : (0 : ℝ) < n := by rw [hn]; exact_mod_cast lt_of_lt_of_le zero_lt_one hcard have hk0 : (0 : ℝ) < k := lt_of_lt_of_le zero_lt_one hk have hkinv0 : (0 : ℝ) < k⁻¹ := inv_pos.mpr hk0 -- single-coordinate function `g_i b = (if b then 0 else 1)/(1 - p i)` set g : U → Bool → ℝ := fun i b => (if b then (0 : ℝ) else 1) / (1 - p i) with hg have hBeq : BhatCtrl p = fun z => ∑ i : U, n⁻¹ * g i (z i) := by funext z; unfold BhatCtrl weightCtrlSummand rw [hn, Finset.sum_div] refine Finset.sum_congr rfl (fun i _ => ?_) rw [hg]; ring have hVcoord : ∀ i, (coinDesign (p i) (hp0 i) (hp1 i)).Var (g i) ≤ k ^ 2 := by intro i have hpi1 : (0 : ℝ) < 1 - p i := lt_of_lt_of_le hkinv0 (by linarith [hphi i]) have hrecq : 1 / (1 - p i) ≤ k := by rw [div_le_iff₀ hpi1] nlinarith [mul_le_mul_of_nonneg_right (by linarith [hphi i] : k⁻¹ ≤ 1 - p i) (le_of_lt hk0), inv_mul_cancel₀ (ne_of_gt hk0)] have hEsq : (coinDesign (p i) (hp0 i) (hp1 i)).E (fun b => (g i b) ^ 2) = 1 / (1 - p i) := by have h1 : (1 : ℝ) - p i ≠ 0 := ne_of_gt hpi1 rw [coinDesign_E]; simp only [hg]; norm_num; field_simp have hVle : (coinDesign (p i) (hp0 i) (hp1 i)).Var (g i) ≤ (coinDesign (p i) (hp0 i) (hp1 i)).E (fun b => (g i b) ^ 2) := by rw [(coinDesign (p i) (hp0 i) (hp1 i)).Var_eq] linarith [sq_nonneg ((coinDesign (p i) (hp0 i) (hp1 i)).E (g i))] have hk2 : (1 : ℝ) / (1 - p i) ≤ k ^ 2 := by nlinarith [hrecq, hk] linarith [le_trans hVle (le_of_eq hEsq)] rw [hBeq] unfold DesignBased.bernoulliDesign rw [FiniteDesign.Var_prod_linear_comb (fun i => coinDesign (p i) (hp0 i) (hp1 i)) (fun _ => n⁻¹) g] have hninv2 : (0 : ℝ) ≤ (n⁻¹) ^ 2 := sq_nonneg _ have hstep : (∑ i : U, (n⁻¹) ^ 2 * (coinDesign (p i) (hp0 i) (hp1 i)).Var (g i)) ≤ ∑ _i : U, (n⁻¹) ^ 2 * k ^ 2 := Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_left (hVcoord i) hninv2) refine le_trans hstep ?_ rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, ← hn] rw [show (n : ℝ) * ((n⁻¹) ^ 2 * k ^ 2) = (n * n⁻¹) * (n⁻¹ * k ^ 2) by ring] rw [mul_inv_cancel₀ (ne_of_gt hn0), one_mul, inv_mul_eq_div] -
abs_E_AhatTreat_letheorem — The treated numerator mean is the average treated potential outcome, uniformly bounded by k via the potential-outcome moment bound (Assumption C).hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1hp0' :∀ i, p i ≠ 0y :U → (U → Bool) → ℝk :ℝhk :1 ≤ khcard :1 ≤ card Uconclusion|(DesignBased.bernoulliDesign p hp0 hp1).E (AhatTreat p y)| ≤ kProof (Lean source)
theorem abs_E_AhatTreat_le (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (hp0' : ∀ i, p i ≠ 0) (y : U → (U → Bool) → ℝ) (k : ℝ) (hk : 1 ≤ k) (hcard : 1 ≤ Fintype.card U) (hpo : ∀ i, (DesignBased.bernoulliDesign p hp0 hp1).E (fun z => |y i (update z i true)|) ≤ k) : |(DesignBased.bernoulliDesign p hp0 hp1).E (AhatTreat p y)| ≤ k := by set D := DesignBased.bernoulliDesign p hp0 hp1 with hD set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : (0 : ℝ) < n := by rw [hn]; exact_mod_cast lt_of_lt_of_le Nat.zero_lt_one hcard -- `E[Â₁] = (1/n) * ∑ i E[htTreatSummand i]`. have h1 : D.E (AhatTreat p y) = (1 / n) * ∑ i : U, D.E (htTreatSummand p y i) := by have hcongr : ∀ z, AhatTreat p y z = (1 / n) * ∑ i : U, htTreatSummand p y i z := by intro z; rw [AhatTreat, hn]; ring rw [D.E_congr hcongr, D.E_const_mul, D.E_sum] -- Each summand's expectation is bounded by `k`. have hbound : ∀ i : U, |D.E (htTreatSummand p y i)| ≤ k := by intro i rw [E_htTreatSummand p hp0 hp1 hp0' y i] exact le_trans (D.abs_E_le_E_abs _) (hpo i) rw [h1, abs_mul] have hpos : |1 / n| = 1 / n := abs_of_pos (by positivity) rw [hpos] calc (1 / n) * |∑ i : U, D.E (htTreatSummand p y i)| ≤ (1 / n) * ∑ i : U, |D.E (htTreatSummand p y i)| := mul_le_mul_of_nonneg_left (Finset.abs_sum_le_sum_abs _ _) (by positivity) _ ≤ (1 / n) * ∑ i : U, k := mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun i _ => hbound i)) (by positivity) _ = k := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, ← hn] field_simp -
abs_E_AhatCtrl_letheorem — The control numerator mean is the average control potential outcome, uniformly bounded by k.hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1hp1' :∀ i, (1 : ℝ) - p i ≠ 0y :U → (U → Bool) → ℝk :ℝhk :1 ≤ khcard :1 ≤ card Uconclusion|(DesignBased.bernoulliDesign p hp0 hp1).E (AhatCtrl p y)| ≤ kProof (Lean source)
theorem abs_E_AhatCtrl_le (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (hp1' : ∀ i, (1 : ℝ) - p i ≠ 0) (y : U → (U → Bool) → ℝ) (k : ℝ) (hk : 1 ≤ k) (hcard : 1 ≤ Fintype.card U) (hpo : ∀ i, (DesignBased.bernoulliDesign p hp0 hp1).E (fun z => |y i (update z i false)|) ≤ k) : |(DesignBased.bernoulliDesign p hp0 hp1).E (AhatCtrl p y)| ≤ k := by set D := DesignBased.bernoulliDesign p hp0 hp1 with hD set n : ℝ := (Fintype.card U : ℝ) with hn have hn0 : (0 : ℝ) < n := by rw [hn]; exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one hcard have h1 : D.E (AhatCtrl p y) = (1 / n) * ∑ i : U, D.E (htCtrlSummand p y i) := by have hcongr : ∀ z, AhatCtrl p y z = (1 / n) * ∑ i : U, htCtrlSummand p y i z := by intro z; rw [AhatCtrl, hn]; ring rw [D.E_congr hcongr, D.E_const_mul, D.E_sum] have hbound : ∀ i : U, |D.E (htCtrlSummand p y i)| ≤ k := by intro i rw [E_htCtrlSummand p hp0 hp1 hp1' y i] exact le_trans (D.abs_E_le_E_abs _) (hpo i) rw [h1, abs_mul] have hpos : |1 / n| = 1 / n := abs_of_pos (by positivity) rw [hpos] calc (1 / n) * |∑ i : U, D.E (htCtrlSummand p y i)| ≤ (1 / n) * ∑ i : U, |D.E (htCtrlSummand p y i)| := mul_le_mul_of_nonneg_left (Finset.abs_sum_le_sum_abs _ _) (by positivity) _ ≤ (1 / n) * ∑ i : U, k := mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun i _ => hbound i)) (by positivity) _ = k := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, ← hn] field_simp -
E_AhatTreat_sub_E_AhatCtrltheorem — The difference of the numerator means is EATE: E[Â₁] − E[Â₀] = EATE (the HT estimator is Â₁ − Â₀, and it is unbiased).hypothesesU :sharedType u_1p :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1hp0' :∀ i, p i ≠ 0hp1' :∀ i, (1 : ℝ) - p i ≠ 0y :U → (U → Bool) → ℝProof (Lean source)
theorem E_AhatTreat_sub_E_AhatCtrl (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (hp0' : ∀ i, p i ≠ 0) (hp1' : ∀ i, (1 : ℝ) - p i ≠ 0) (y : U → (U → Bool) → ℝ) : (DesignBased.bernoulliDesign p hp0 hp1).E (AhatTreat p y) - (DesignBased.bernoulliDesign p hp0 hp1).E (AhatCtrl p y) = EATE (DesignBased.bernoulliDesign p hp0 hp1) y := by set D := DesignBased.bernoulliDesign p hp0 hp1 with hD rw [← D.E_sub] -- Pointwise `AhatTreat - AhatCtrl = htEst`. have hpt : ∀ z, AhatTreat p y z - AhatCtrl p y z = htEst p y z := by intro z rw [AhatTreat, AhatCtrl, htEst, ← sub_div] congr 1 rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [htSummand, htTreatSummand, htCtrlSummand] rw [D.E_congr hpt] rw [hD] exact htEst_unbiased p hp0 hp1 hp0' hp1' y
Unbiased 2 core · 0 supporting Bernoulli Horvitz-Thompson estimators are exactly unbiased for the expected average treatment effect even when outcomes may depend on other units' assignments. ★ E_htSummand★ htEst_unbiased
Unbiasedness under unknown interference
Bernoulli Horvitz-Thompson estimators are exactly unbiased for the expected average treatment effect even when outcomes may depend on other units' assignments.
For each unit, its own Bernoulli treatment is independent of the remaining assignment coordinates
that determine its treated and control potential outcomes. Product-design block factorization and
the Bernoulli marginal identities therefore show that the unit's Horvitz-Thompson summand has
expectation equal to its assignment-conditional treatment effect. Summing these identities proves
the exact equality E[htEst] = EATE.
Per-unit unbiasedness. Under a Bernoulli design in which every unit's treatment probability lies in [0,1] and is neither exactly zero nor exactly one, so both the treatment and control propensities are nonzero, the i-th Horvitz–Thompson summand has the same expectation as unit i's assignment-conditional treatment effect τ_i.
Formal statement
Proof (Lean source)
Horvitz–Thompson unbiasedness for EATE (Sävje–Aronow–Hudgens 2021). Under a Bernoulli design in which every unit's treatment probability lies in [0,1] and is neither exactly zero nor exactly one, so both the treatment and control propensities are nonzero, the Horvitz–Thompson estimator is exactly unbiased for the expected average treatment effect.
Formal statement
Proof (Lean source)
VarianceBound 4 core · 2 supporting Under Bernoulli assignment, overlap and second-moment control bound the Horvitz-Thompson variance by the average amount of interference dependence: Var(ĤT) ≤ k⁴ · d̄ / n. ★ cov_htSummand_zero★ var_htSummand_le★ var_htEst_le
Variance bounds under unknown interference
Under Bernoulli assignment, overlap and second-moment control bound the Horvitz-Thompson variance by the average amount of interference dependence:
Var(ĤT) ≤ k⁴ · d̄ / n.
This file identifies the assignment-coordinate support of each unit's summand. Summands with
disjoint supports have zero covariance by product-design independence; every remaining covariance
is bounded by k⁴. Summing over the n * dbar interference-dependent ordered pairs gives the
finite-sample bound used by the consistency development.
For every finite population of units whose members can be compared for equality, every schedule of potential outcomes indexed by a unit and a complete binary treatment assignment, and every unit in that population, the interferer set is the finite set consisting of that unit and every other unit whose treatment can affect that unit's potential outcome.
Definition (Lean source)
No covariance off the interference-dependence graph. Under a Bernoulli design in which each unit i is treated independently with probability p i, where every p i lies in the unit interval, if units i and j are not interference dependent — no unit's treatment affects both units' outcomes — then their Horvitz–Thompson summands have zero covariance under this design.
Formal statement
Proof (Lean source)
Per-summand variance bound. Fix a regularity constant k at least 1 and a Bernoulli design with per-unit treatment probabilities lying in the unit interval and further satisfying the overlap bounds k⁻¹ ≤ p i ≤ 1 − k⁻¹ for every unit. If the outcome function's second moment E[(y i)²] is at most k² for every unit under this design, then the variance of the iᵗʰ Horvitz–Thompson summand is at most k⁴.
Formal statement
Proof (Lean source)
The Horvitz–Thompson variance bound (Sävje–Aronow–Hudgens 2021). Fix a regularity constant k at least 1 over a nonempty finite unit population, with a Bernoulli design whose per-unit treatment probabilities lie in the unit interval and further satisfy the overlap bounds k⁻¹ ≤ p i ≤ 1 − k⁻¹ for every unit. If the outcome function's second moment E[(y i)²] is at most k² for every unit under this design, then the Horvitz–Thompson estimator's variance is at most k⁴ · d̄ / n, where d̄ is the average interference-dependence degree and n the number of units.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
htSummand_depends_on_interfererstheorem — The iᵗʰ HT summand depends only on the treatments of the units interfering with i.hypothesesU :sharedType u_1p :U → ℝy :U → (U → Bool) → ℝi :Uz z' :U → Boolh :∀ ℓ ∈ interferers y i, z ℓ = z' ℓProof (Lean source)
theorem htSummand_depends_on_interferers (p : U → ℝ) (y : U → (U → Bool) → ℝ) (i : U) (z z' : U → Bool) (h : ∀ ℓ ∈ interferers y i, z ℓ = z' ℓ) : htSummand p y i z = htSummand p y i z' := by classical have hmem : ∀ ℓ : U, Interferes y ℓ i → ℓ ∈ interferers y i := by intro ℓ hℓ exact Finset.mem_filter.mpr ⟨Finset.mem_univ ℓ, hℓ⟩ -- `i` interferes with itself, so `z i = z' i`. have hzi : z i = z' i := h i (hmem i (inl rfl)) -- The outcome agrees because `z, z'` agree on all interferers of `i`. have hyi : y i z = y i z' := y_eq_of_agree_on_interferers y i z z' (fun ℓ hℓ => h ℓ (hmem ℓ hℓ)) unfold htSummand rw [hzi, hyi] -
disjoint_interferers_of_not_interfDeptheorem — If i and j are not interference dependent, their interferer blocks are disjoint.hypothesesconclusionProof (Lean source)
theorem disjoint_interferers_of_not_interfDep (y : U → (U → Bool) → ℝ) {i j : U} (h : ¬ InterfDep y i j) : Disjoint (interferers y i) (interferers y j) := by classical rw [Finset.disjoint_left] intro ℓ hℓi hℓj have hi : Interferes y ℓ i := (Finset.mem_filter.mp hℓi).2 have hj : Interferes y ℓ j := (Finset.mem_filter.mp hℓj).2 exact h ⟨ℓ, hi, hj⟩