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 11 core · 0 supporting The setup for "Average treatment effects in the presence of unknown interference" (Sävje, Aronow & Hudgens, *Annals of Statistics* 49(2), 2021). ★ Interferes★ InterfDep★ dbar★ EATE★ htEst★ y_update_eq_of_not_interferes★ 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.
Interference indicator. Unit ℓ interferes with unit i if changing ℓ's treatment changes i's outcome under some assignment, or if ℓ = i (a unit always interferes with itself). y i z is unit i's outcome under the full assignment z.
Definition (Lean source)
Interference dependence. Units i and j are interference dependent if some unit ℓ interferes with both — i.e. they may be affected by a common treatment. The paper's d̄_{ij}.
Definition (Lean source)
The (unnormalized) count ∑ᵢ ∑ⱼ 1[InterfDep i j] of interference-dependent ordered pairs.
Average interference dependence d̄ = n⁻¹ ∑ᵢ ∑ⱼ 1[InterfDep i j] — the paper's basic measure of the amount of interference. For a nonempty population, d̄ = 1 under no interference; d̄ = n when every pair is interference dependent. "Restricted interference" is the assumption d̄ = o(n).
Assignment-conditional unit-level treatment effect. τ_i(z_{-i}) = y_i(1; z_{-i}) − y_i(0; z_{-i}), the effect of changing unit i's own treatment with all others held at z. Encoded on the full assignment via Function.update; it does not depend on z i.
Assignment-conditional average treatment effect ACATE(z) = n⁻¹ ∑ᵢ τ_i(z_{-i}).
Expected average treatment effect (Definition, Sävje–Aronow–Hudgens 2021): EATE = E[ACATE(Z)], the design average of the assignment-conditional ATE. It generalizes the conventional ATE — under no interference ACATE(z) is constant in z, so the marginalization is inconsequential and EATE = ATE.
Definition (Lean source)
The iᵗʰ Horvitz–Thompson summand Z_i Y_i / p_i − (1 − Z_i) Y_i / (1 − p_i), with Z_i = 1[z i] and Y_i = y i z.
Horvitz–Thompson estimator htEst = n⁻¹ ∑ᵢ [Z_i Y_i / p_i − (1 − Z_i) Y_i / (1 − p_i)], with p i the marginal treatment probability of unit i.
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.
Formal statement
Proof (Lean source)
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)
Bernoulli 4 core · 0 supporting Independent Bernoulli assignment supplies the product-design independence used for Sävje-Aronow-Hudgens unknown-interference results. ★ bernoulliDesign★ bernoulliDesign_E_eval★ bernoulliDesign_E_treat★ bernoulliDesign_E_ctrl
Bernoulli design under unknown interference
Independent Bernoulli assignment supplies the product-design independence used for Sävje-Aronow-Hudgens unknown-interference results.
This file reuses the canonical single-unit coinDesign, builds the product Bernoulli randomization
design bernoulliDesign, and proves the one-coordinate marginal identities used throughout the
Horvitz-Thompson and Hájek arguments. coinDesign_E expands the two-point expectation,
bernoulliDesign_E_eval reduces any function of one unit's assignment to the corresponding coin
expectation, and bernoulliDesign_E_treat / bernoulliDesign_E_ctrl give the marginal treatment
and control probabilities p_i and 1 - p_i.
The Bernoulli randomization design: each unit i is independently assigned treatment with probability p i. Built as the product of the per-unit coin designs.
Definition (Lean source)
Marginalizing the Bernoulli design to a single coordinate. Under the Bernoulli design with per-unit treatment probabilities p taking values in [0, 1], the expected value of any function g of a single unit i's treatment status coincides with its expectation under that unit's own coin design with success probability p i — the Zᵢ ⊥ Z₋ᵢ marginalization.
Formal statement
Proof (Lean source)
Marginal treatment-indicator expectation under the Bernoulli design. Under the Bernoulli design with per-unit treatment probabilities p taking values in [0, 1], the expected value of the indicator that unit i is treated equals p i.
Formal statement
Proof (Lean source)
Marginal control-indicator expectation under the Bernoulli design. Under the Bernoulli design with per-unit treatment probabilities p taking values in [0, 1], the expected value of the indicator that unit i is untreated equals 1 - p i.
Formal statement
Proof (Lean source)
Consistency 8 core · 2 supporting Horvitz-Thompson estimates the expected average treatment effect consistently when average interference is sparse. ★ SAHExperiment★ D_E_htEst★ D_Var_htEst_le★ chebyshev_eate★ htEst_consistent_eate★ root_n_var
Consistency under unknown interference
Horvitz-Thompson estimates the expected average treatment effect consistently when average interference is sparse.
This file packages one Sävje-Aronow-Hudgens Bernoulli experiment as SAHExperiment, including
the finite unit type, treatment probabilities, potential outcomes, overlap bounds, moment bound,
and regularity constant. The namespace-level bundle lemmas D_E_htEst, D_Var_htEst_le, and
chebyshev_eate restate exact unbiasedness, the finite-sample variance bound, and the resulting
Chebyshev tail inequality for the packaged experiment. The main sequence theorem
htEst_consistent_eate proves convergence in probability when k^4 * dbar / n -> 0, and
root_n_var records the root-n variance scaling under bounded average interference.
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)
The Bernoulli design of the experiment.
Definition (Lean source)
The EATE estimand of the experiment.
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)
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.
Proof (Lean source)
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.
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)
2 supporting declarations (lemmas, instances)
-
p_ne_zerolemma — The treatment probabilities are nonzero (from lower overlap).hypothesesi :E.UconclusionE.p i ≠ 0Proof (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).hypothesesi :E.Uconclusion(1 : ℝ) - E.p i ≠ 0Proof (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
Confidence 6 core · 0 supporting Chebyshev confidence statements remain valid under unknown interference when they use proven conservative variance bounds. ★ VhatBer★ E_VhatBer_bias★ var_htEst_le_inflated★ chebyshev_ci_eate★ eate_ci_kbound
Confidence under unknown interference
Chebyshev confidence statements remain valid under unknown interference when they use proven conservative variance bounds.
This file formalizes three finite-sample confidence facts for the Sävje-Aronow-Hudgens
Bernoulli setup. The conventional variance estimator VhatBer has an exact expectation-bias
identity E_VhatBer_bias, showing how off-diagonal covariances from interference can make it
anti-conservative. The degree statistic degDep supports var_htEst_le_inflated, an
in-expectation conservative inflation of VhatBer when each unit has bounded interference
degree. Finally, chebyshev_ci_eate proves coverage for any positive conservative variance
bound, and eate_ci_kbound instantiates it with the finite-sample variance bound
k^4 * dbar / n.
The conventional Horvitz–Thompson variance estimator V̂_Ber = n⁻² ∑ᵢ ĤTᵢ². Pointwise this equals the paper's n⁻²[∑ᵢ ZᵢYᵢ²/pᵢ² + ∑ᵢ(1−Zᵢ)Yᵢ²/(1−pᵢ)²] (the cross term vanishes since Zᵢ(1−Zᵢ)=0).
The interference degree of unit i: the number of units interference-dependent with i (d̄ᵢ = ∑ⱼ 1[InterfDep i j]).
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)
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 − α.
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 significance level α is positive. Then the Chebyshev interval ĤT ± √(k⁴·d̄/(n·α)), where d̄ is the average interference degree and n 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 interference measure d̄.
Formal statement
Proof (Lean source)
Hajek 10 core · 9 supporting The Hájek estimator normalizes treated and control inverse-probability-weighted outcome sums by their realized weight sums. ★ 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. This file defines those numerator and denominator components, proves their mean and variance controls under Bernoulli assignment, and combines them with the finite-design Slutsky tools to prove consistency for the Sävje-Aronow-Hudgens EATE estimand.
Treated Horvitz–Thompson summand Zᵢ Yᵢ / pᵢ.
Definition (Lean source)
Control Horvitz–Thompson summand (1 − Zᵢ) Yᵢ / (1 − pᵢ).
Definition (Lean source)
Treated weight summand Zᵢ / pᵢ.
Definition (Lean source)
Control weight summand (1 − Zᵢ) / (1 − pᵢ).
Definition (Lean source)
The treated numerator average Â₁ = n⁻¹ ∑ᵢ Zᵢ Yᵢ / pᵢ.
Definition (Lean source)
The control numerator average Â₀ = n⁻¹ ∑ᵢ (1−Zᵢ) Yᵢ / (1−pᵢ).
Definition (Lean source)
The treated weight average B̂₁ = n⁻¹ ∑ᵢ Zᵢ / pᵢ.
Definition (Lean source)
The control weight average B̂₀ = n⁻¹ ∑ᵢ (1−Zᵢ) / (1−pᵢ).
Definition (Lean source)
The Hájek estimator ĤA = Â₁/B̂₁ − Â₀/B̂₀, the realized-weight-normalized inverse-probability-weighted estimator.
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.hypothesesconclusion(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) : (bernoulliDesign p hp0 hp1).E (BhatTreat p) = 1 := by set D := 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 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.hypothesesconclusion(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) : (bernoulliDesign p hp0 hp1).E (BhatCtrl p) = 1 := by set D := 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 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).hypothesesp :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, (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, (bernoulliDesign p hp0 hp1).E (fun z => (y i z) ^ 2) ≤ k ^ 2) : (bernoulliDesign p hp0 hp1).Var (AhatTreat p y) ≤ k ^ 4 * dbar y / (Fintype.card U : ℝ) := by classical set D := 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) := Var_nonneg D _ 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.hypothesesp :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, (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, (bernoulliDesign p hp0 hp1).E (fun z => (y i z) ^ 2) ≤ k ^ 2) : (bernoulliDesign p hp0 hp1).Var (AhatCtrl p y) ≤ k ^ 4 * dbar y / (Fintype.card U : ℝ) := by classical set D := 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) := Var_nonneg D _ 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).hypothesesp :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) : (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 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.hypothesesp :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⁻¹) : (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 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).hypothesesp :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1hp0' :∀ i, p i ≠ 0y :U → (U → Bool) → ℝk :ℝhk :1 ≤ khcard :1 ≤ card Uconclusion|(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, (bernoulliDesign p hp0 hp1).E (fun z => |y i (update z i true)|) ≤ k) : |(bernoulliDesign p hp0 hp1).E (AhatTreat p y)| ≤ k := by set D := 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 (abs_E_le_E_abs D _) (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.hypothesesp :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|(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, (bernoulliDesign p hp0 hp1).E (fun z => |y i (update z i false)|) ≤ k) : |(bernoulliDesign p hp0 hp1).E (AhatCtrl p y)| ≤ k := by set D := 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 (abs_E_le_E_abs D _) (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).hypothesesp :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) → ℝ) : (bernoulliDesign p hp0 hp1).E (AhatTreat p y) - (bernoulliDesign p hp0 hp1).E (AhatCtrl p y) = EATE (bernoulliDesign p hp0 hp1) y := by set D := 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.
The per-unit theorem E_htSummand shows that the ith Horvitz-Thompson summand has expectation
equal to the assignment-conditional treatment effect tau y i. Its proof uses product-design
block independence between unit i's own treatment and the remaining assignments that determine
y_i(1; Z_{-i}) or y_i(0; Z_{-i}), plus the Bernoulli marginal identities from Bernoulli.
Summing these identities gives htEst_unbiased, 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 The Horvitz-Thompson variance is bounded by the average amount of interference dependence under Bernoulli assignment. ★ cov_htSummand_zero★ var_htSummand_le★ var_htEst_le
Variance bounds under unknown interference
The Horvitz-Thompson variance is bounded by the average amount of interference dependence under Bernoulli assignment.
This file proves the Sävje-Aronow-Hudgens finite-sample bound
Var(htEst) <= k^4 * dbar / n under overlap and second-moment control. The block
interferers y i records the coordinate support of the ith HT summand;
htSummand_depends_on_interferers and disjoint_interferers_of_not_interfDep connect the
interference graph to product-design disjoint-block independence, and cov_htSummand_zero
eliminates covariance terms off that graph. The per-summand bound var_htSummand_le controls
the remaining covariance terms by k^4, and the headline theorem var_htEst_le sums them over
the dbarCount = n * dbar dependent ordered pairs.
The block of units that interfere with i (its own treatment included): the coordinate support of the iᵗʰ HT summand.
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.hypothesesProof (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⟩