Experimentation.Design­Based.HT

Horvitz-Thompson design-based estimators: totals, means, effects, unbiasedness, covariance formulas, and finite-population variance identities.

Estimator 6 core · 0 supporting Horvitz-Thompson estimators use inverse generalized exposure probabilities to estimate finite-population exposure totals, means, and contrasts. ★ htTotal★ htMean★ htEffect★ htTotal_eq

Horvitz-Thompson estimators

Horvitz-Thompson estimators use inverse generalized exposure probabilities to estimate finite-population exposure totals, means, and contrasts.

The main estimator is htTotal, the totalized inverse-probability-weighted estimator for exposure d. Dividing by the number of units gives htMean, and differencing two exposure means gives htEffect. The target functionals are muTrue and tauTrue. The lemma htTotal_eq rewrites the estimator using the exposure-specific potential outcome y i d, a form used by the unbiasedness and variance proofs.

def htTotal reviewed
Causalean.Experimentation.DesignBased

Totalized Horvitz–Thompson estimator of the total potential outcome under exposure d.

Definition (Lean source)
noncomputable def htTotal (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (z : Ω) : ℝ := ∑ i, expoInd f θ i d z * Yobs y f θ i z / prop D f θ i d
Causalean.Experimentation.DesignBased.htTotal · Causalean/Experimentation/DesignBased/HT/Estimator.lean:45 · uses FiniteDesign
def muTrue reviewed
Causalean.Experimentation.DesignBased

Population mean potential outcome under exposure d: μ(d) = (1/N)∑ᵢ y i d.

Definition (Lean source)
noncomputable def muTrue (y : ι → Δ → ℝ) (d : Δ) : ℝ := (∑ i, y i d) / (Fintype.card ι : ℝ)
Causalean.Experimentation.DesignBased.muTrue · Causalean/Experimentation/DesignBased/HT/Estimator.lean:50
def tauTrue reviewed
Causalean.Experimentation.DesignBased

Average causal effect of exposure dk versus dl: τ = μ(dk) − μ(dl).

Definition (Lean source)
noncomputable def tauTrue (y : ι → Δ → ℝ) (dk dl : Δ) : ℝ := muTrue y dk - muTrue y dl
Causalean.Experimentation.DesignBased.tauTrue · Causalean/Experimentation/DesignBased/HT/Estimator.lean:54
def htMean reviewed
Causalean.Experimentation.DesignBased

Horvitz–Thompson estimator of the mean potential outcome under exposure d.

Definition (Lean source)
noncomputable def htMean (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (z : Ω) : ℝ := htTotal D y f θ d z / (Fintype.card ι : ℝ)
Causalean.Experimentation.DesignBased.htMean · Causalean/Experimentation/DesignBased/HT/Estimator.lean:58 · uses FiniteDesign
def htEffect reviewed
Causalean.Experimentation.DesignBased

Horvitz–Thompson estimator of the average causal effect of dk versus dl.

Definition (Lean source)
noncomputable def htEffect (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (dk dl : Δ) (z : Ω) : ℝ := htMean D y f θ dk z - htMean D y f θ dl z
Causalean.Experimentation.DesignBased.htEffect · Causalean/Experimentation/DesignBased/HT/Estimator.lean:63 · uses FiniteDesign
lemma htTotal_eq reviewed
Causalean.Experimentation.DesignBased

For a finite design D, potential outcomes y, exposure map f, assignment θ, exposure level d, and realized assignment z, the Horvitz–Thompson total equals the same sum with the observed outcome replaced termwise by the potential outcome y i d, because on each unit's exposure-indicator term the observed outcome coincides with y i d.

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
z :
Ω
conclusion
htTotal D y f θ d z = ∑ i, expoInd f θ i d z * y i d / prop D f θ i d
Proof (Lean source)
lemma htTotal_eq (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (z : Ω) : htTotal D y f θ d z = ∑ i, expoInd f θ i d z * y i d / prop D f θ i d := by unfold htTotal refine Finset.sum_congr rfl (fun i _ => ?_) rw [expoInd_mul_Yobs]
Causalean.Experimentation.DesignBased.htTotal_eq · Causalean/Experimentation/DesignBased/HT/Estimator.lean:68 · uses FiniteDesign , expoInd , htTotal , prop
Unbiased 3 core · 0 supporting Positive generalized exposure probabilities make the Horvitz-Thompson estimators exactly unbiased under a finite randomization design. ★ E_htTotal★ E_htMean★ E_htEffect

Horvitz-Thompson unbiasedness

Positive generalized exposure probabilities make the Horvitz-Thompson estimators exactly unbiased under a finite randomization design.

The theorem E_htTotal proves the total estimator has expectation ∑ᵢ y i d, because each inverse-probability weight cancels E[1(expo i = d)]. The theorem E_htMean scales this to the population mean muTrue, and E_htEffect proves unbiasedness of the exposure contrast estimator htEffect for tauTrue.

theorem E_htTotal reviewed
Causalean.Experimentation.DesignBased

Lemma 4.1 (expectation). Given a finite design, an outcome function y, an exposure map f, and an assignment θ, suppose every unit has nonzero probability of realizing exposure d. Then the Horvitz–Thompson total estimator has expectation exactly the population total ∑ᵢ y i d.

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
hpos :
∀ i, prop D f θ i d ≠ 0
conclusion
D.E (htTotal D y f θ d) = ∑ i, y i d
Proof (Lean source)
theorem E_htTotal (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (hpos : ∀ i, prop D f θ i d ≠ 0) : D.E (htTotal D y f θ d) = ∑ i, y i d := by have hfun : htTotal D y f θ d = (fun z => ∑ i, (y i d / prop D f θ i d) * expoInd f θ i d z) := by funext z rw [htTotal_eq] exact Finset.sum_congr rfl (fun i _ => by ring) rw [hfun, FiniteDesign.E_sum] refine Finset.sum_congr rfl (fun i _ => ?_) rw [FiniteDesign.E_const_mul, E_expoInd, div_mul_cancel₀ _ (hpos i)]
Causalean.Experimentation.DesignBased.E_htTotal · Causalean/Experimentation/DesignBased/HT/Unbiased.lean:38 · uses FiniteDesign , E , htTotal , prop
theorem E_htMean reviewed
Causalean.Experimentation.DesignBased

Given a finite design, an outcome function y, an exposure map f, and an assignment θ, suppose every unit has nonzero probability of realizing exposure d. Then the Horvitz–Thompson mean estimator has expectation exactly the population mean μ(d).

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
hpos :
∀ i, prop D f θ i d ≠ 0
conclusion
D.E (htMean D y f θ d) = muTrue y d
Proof (Lean source)
theorem E_htMean (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (hpos : ∀ i, prop D f θ i d ≠ 0) : D.E (htMean D y f θ d) = muTrue y d := by have hmean : htMean D y f θ d = (fun z => ((Fintype.card ι : ℝ)⁻¹) * htTotal D y f θ d z) := by funext z; rw [htMean, div_eq_inv_mul] rw [hmean, FiniteDesign.E_const_mul, E_htTotal D y f θ d hpos, muTrue, div_eq_inv_mul]
Causalean.Experimentation.DesignBased.E_htMean · Causalean/Experimentation/DesignBased/HT/Unbiased.lean:54 · uses FiniteDesign , E , htMean , muTrue , prop
theorem E_htEffect reviewed
Causalean.Experimentation.DesignBased

Proposition 4.4 (expectation). Given a finite design, an outcome function y, an exposure map f, and an assignment θ, suppose every unit has nonzero probability of realizing exposure dk and every unit has nonzero probability of realizing exposure dl. Then the Horvitz–Thompson effect estimator contrasting dk against dl has expectation exactly the average causal effect τ(dk,dl).

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
hk :
∀ i, prop D f θ i dk ≠ 0
hl :
∀ i, prop D f θ i dl ≠ 0
conclusion
D.E (htEffect D y f θ dk dl) = tauTrue y dk dl
Proof (Lean source)
theorem E_htEffect (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (dk dl : Δ) (hk : ∀ i, prop D f θ i dk ≠ 0) (hl : ∀ i, prop D f θ i dl ≠ 0) : D.E (htEffect D y f θ dk dl) = tauTrue y dk dl := by have hsub : htEffect D y f θ dk dl = (fun z => htMean D y f θ dk z - htMean D y f θ dl z) := by funext z; rw [htEffect] rw [hsub, FiniteDesign.E_sub, E_htMean D y f θ dk hk, E_htMean D y f θ dl hl, tauTrue]
Causalean.Experimentation.DesignBased.E_htEffect · Causalean/Experimentation/DesignBased/HT/Unbiased.lean:65 · uses FiniteDesign , E , htEffect , prop , tauTrue
Variance 4 core · 0 supporting Horvitz-Thompson randomization variance reduces to finite covariance sums over exposure indicators. ★ Var_htTotal_cov★ Var_htTotal★ Cov_htTotal_cov★ Cov_htTotal

Horvitz-Thompson variance identities

Horvitz-Thompson randomization variance reduces to finite covariance sums over exposure indicators.

The covariance-form theorem Var_htTotal_cov expands the variance of htTotal as a double sum of indicator covariances, and Var_htTotal rewrites those terms into the marginal and joint exposure probabilities. The companion theorems Cov_htTotal_cov and Cov_htTotal give the analogous covariance formulas for two exposure totals, including the diagonal cross-exposure term that appears when one unit cannot occupy two distinct exposures at once.

theorem Var_htTotal_cov reviewed
Causalean.Experimentation.DesignBased

Lemma 4.1 (variance), covariance form. For a finite design, outcome function y, exposure map f, and assignment θ, the randomization variance of the Horvitz–Thompson total under exposure d equals the double sum, over unit pairs, of inverse-probability-weighted indicator covariances.

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
conclusion
D.Var (htTotal D y f θ d)
= ∑ i, ∑ j, (y i d / prop D f θ i d) * (y j d / prop D f θ j d) * D.Cov (expoInd f θ i d) (expoInd f θ j d)
Proof (Lean source)
theorem Var_htTotal_cov (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) : D.Var (htTotal D y f θ d) = ∑ i, ∑ j, (y i d / prop D f θ i d) * (y j d / prop D f θ j d) * D.Cov (expoInd f θ i d) (expoInd f θ j d) := by rw [show D.Var (htTotal D y f θ d) = D.Var (fun z => ∑ i, (y i d / prop D f θ i d) * expoInd f θ i d z) from D.Var_congr (fun z => by rw [htTotal_eq]; exact Finset.sum_congr rfl (fun i _ => by ring))] rw [FiniteDesign.Var_linear_comb]
Causalean.Experimentation.DesignBased.Var_htTotal_cov · Causalean/Experimentation/DesignBased/HT/Variance.lean:42 · uses FiniteDesign , Cov , Var , expoInd , htTotal , prop
theorem Var_htTotal reviewed
Causalean.Experimentation.DesignBased

Lemma 4.1 (variance), expanded form eq:total_variance. For a finite design, outcome function y, exposure map f, and assignment θ, the randomization variance of the Horvitz–Thompson total under exposure d equals the diagonal sum of inverse-probability-weighted indicator variances plus the off-diagonal sum of inverse-probability-weighted indicator covariances.

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
conclusion
D.Var (htTotal D y f θ d)
= (∑ i, prop D f θ i d * (1 - prop D f θ i d) * (y i d / prop D f θ i d) ^ 2)
+ ∑ i, ∑ j ∈ Finset.univ.erase i, (propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d) * ((y i d / prop D f θ i d) * (y j d / prop D f θ j d))
Proof (Lean source)
theorem Var_htTotal (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) : D.Var (htTotal D y f θ d) = (∑ i, prop D f θ i d * (1 - prop D f θ i d) * (y i d / prop D f θ i d) ^ 2) + ∑ i, ∑ j ∈ Finset.univ.erase i, (propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d) * ((y i d / prop D f θ i d) * (y j d / prop D f θ j d)) := by rw [Var_htTotal_cov, ← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.add_sum_erase univ _ (Finset.mem_univ i)] congr 1 · -- diagonal term j = i rw [FiniteDesign.Cov_self, show D.Var (expoInd f θ i d) = prop D f θ i d * (1 - prop D f θ i d) from FiniteDesign.Var_ind (D := D) (fun z => expo f θ i z = d)] ring · -- off-diagonal j ∈ erase i refine Finset.sum_congr rfl (fun j _ => ?_) rw [Cov_expoInd_same]; ring
Causalean.Experimentation.DesignBased.Var_htTotal · Causalean/Experimentation/DesignBased/HT/Variance.lean:57 · uses FiniteDesign , Var , htTotal , prop , propPairSame
theorem Cov_htTotal_cov reviewed
Causalean.Experimentation.DesignBased

For a finite design, outcome function y, exposure map f, and assignment θ, the covariance between two Horvitz-Thompson exposure totals equals the double sum, over ordered unit pairs, of the two inverse-probability outcome weights times the covariance of the corresponding exposure indicators.

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
conclusion
D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl)
= ∑ i, ∑ j, (y i dk / prop D f θ i dk) * (y j dl / prop D f θ j dl) * D.Cov (expoInd f θ i dk) (expoInd f θ j dl)
Proof (Lean source)
theorem Cov_htTotal_cov (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (dk dl : Δ) : D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl) = ∑ i, ∑ j, (y i dk / prop D f θ i dk) * (y j dl / prop D f θ j dl) * D.Cov (expoInd f θ i dk) (expoInd f θ j dl) := by rw [D.Cov_congr (X' := fun z => ∑ i, (y i dk / prop D f θ i dk) * expoInd f θ i dk z) (Y' := fun z => ∑ j, (y j dl / prop D f θ j dl) * expoInd f θ j dl z) (fun z => by rw [htTotal_eq]; exact Finset.sum_congr rfl (fun i _ => by ring)) (fun z => by rw [htTotal_eq]; exact Finset.sum_congr rfl (fun j _ => by ring))] rw [FiniteDesign.Cov_linear_comb]
Causalean.Experimentation.DesignBased.Cov_htTotal_cov · Causalean/Experimentation/DesignBased/HT/Variance.lean:86 · uses FiniteDesign , Cov , expoInd , htTotal , prop
theorem Cov_htTotal reviewed
Causalean.Experimentation.DesignBased

Proposition 4.4 (covariance), expanded form eq:totals_covariance. Given a finite design, an outcome function y, an exposure map f, and an assignment θ, suppose the two exposures dk and dl are distinct, every unit has nonzero probability of realizing exposure dk, and every unit has nonzero probability of realizing exposure dl. Then the covariance of the two Horvitz–Thompson totals equals the off-diagonal double sum of inverse-probability-weighted joint-exposure covariance terms, minus the diagonal term ∑ᵢ y_i(dk)·y_i(dl) — a unit cannot occupy two distinct exposures at once, so the diagonal cross-indicator vanishes and leaves this unidentified term.

Formal statement
hypotheses
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
hne :
dk ≠ dl
hk :
∀ i, prop D f θ i dk ≠ 0
hl :
∀ i, prop D f θ i dl ≠ 0
conclusion
D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl)
= (∑ i, ∑ j ∈ Finset.univ.erase i, (propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) * ((y i dk / prop D f θ i dk) * (y j dl / prop D f θ j dl)))
- ∑ i, y i dk * y i dl
Proof (Lean source)
theorem Cov_htTotal (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (dk dl : Δ) (hne : dk ≠ dl) (hk : ∀ i, prop D f θ i dk ≠ 0) (hl : ∀ i, prop D f θ i dl ≠ 0) : D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl) = (∑ i, ∑ j ∈ Finset.univ.erase i, (propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) * ((y i dk / prop D f θ i dk) * (y j dl / prop D f θ j dl))) - ∑ i, y i dk * y i dl := by rw [Cov_htTotal_cov, ← Finset.sum_sub_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.add_sum_erase univ _ (Finset.mem_univ i)] rw [show (∑ j ∈ Finset.univ.erase i, (propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) * ((y i dk / prop D f θ i dk) * (y j dl / prop D f θ j dl))) = (∑ j ∈ Finset.univ.erase i, (y i dk / prop D f θ i dk) * (y j dl / prop D f θ j dl) * D.Cov (expoInd f θ i dk) (expoInd f θ j dl)) from Finset.sum_congr rfl (fun j _ => by rw [Cov_expoInd_cross]; ring)] -- diagonal: peel the j = i term and reduce it to -(y i dk * y i dl) rw [Cov_expoInd_cross, propPairCross_self_of_ne D f θ i hne] have hki := hk i have hli := hl i field_simp ring
Causalean.Experimentation.DesignBased.Cov_htTotal · Causalean/Experimentation/DesignBased/HT/Variance.lean:102 · uses FiniteDesign , Cov , htTotal , prop , propPairCross