Experimentation.Exposure­Mapping­Interference.Variance

Design-based variance estimators for exposure-mapping HT means and effects, including conservative estimators under pairwise exposure conditions.

Conservative 9 core · 5 supporting Design-based variance estimators for Var[ŷᵀ(d)] and Var[τ̂(dk,dl)]. ★ E_htEffectVarEst_ge★ E_htVarEst_eq_addBias★ E_htEffectVarEstA_ge

Conservative variance estimators (Aronow–Samii 2017, §5)

Design-based variance estimators for Var[ŷᵀ(d)] and Var[τ̂(dk,dl)]. In the positive-joint regime (π_{ij}(d) > 0, π_{ij}(d,d') > 0 for i ≠ j) the variance estimator htVarEst is exactly unbiased (Lemma 5.1, varun). The covariance Cov[ŷᵀ(dk),ŷᵀ(dl)] is unidentified, so its estimator htCovEst is only nonpositively biased (Prop 5.3, ncov, via Young's inequality 2ab ≤ a²+b² for the diagonal term). Assembling these gives the conservative effect-variance estimator htEffectVarEst with nonnegative bias (a positive-joint specialization of Prop 5.6, consvar) — the input the interval result consumes.

The zero-pairwise refinements handle the π_{ij} = 0 corner cases. Prop 5.1 (E_htVarEst_eq_addBias, varbias) characterizes the bias of htVarEst as the explicit correction A = ∑_{π_{ij}=0} y_i y_j; the Young correction htA2 (Â₂) restores conservativeness (Prop 5.2, E_htVarEst_add_htA2_ge, a2). Prop 5.4 (E_htCovEst_eq_of_noEffect, no_bias_cov) shows htCovEst is exactly unbiased under no effect. The general covariance estimator htCovEstA (Ĉov_A, eq:ht_cov_general_estimator) is nonpositively biased with no positive-cross-joint assumption (Prop 5.5, E_htCovEstA_le, cova); its Young correction ranges over all j ∈ U with π_{ij}(d_k,d_l)=0 (faithful to the paper — the diagonal j=i, always zero since d_k ≠ d_l, subsumes the unidentified −∑ᵢ y_i(d_k)y_i(d_l) term). Assembling these gives the general conservative effect-variance estimator htEffectVarEstA with nonnegative bias (Prop 5.6, consvar, E_htEffectVarEstA_ge).

def htVarEst reviewed
Causalean.Experimentation.ExposureMappingInterference

For a finite assignment space, a finite unit population, a unit-trait space, an exposure space, a randomization design, exposure-indexed potential outcomes, an exposure mapping, unit traits, an exposure level, and an assignment, the Horvitz--Thompson variance estimator is the sum of its single-unit inverse-propensity terms and its ordered-pair terms over distinct units.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
z :
Ω
def
htVarEst D y f θ d z :
ℝ
given by
(∑ i, expoInd f θ i d z * (1 - prop D f θ i d) * (Yobs y f θ i z / prop D f θ i d) ^ 2)
+ ∑ i, ∑ j ∈ Finset.univ.erase i, expoInd f θ i d z * expoInd f θ j d z * ((propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d) / propPairSame D f θ i j d) * ((Yobs y f θ i z / prop D f θ i d) * (Yobs y f θ j z / prop D f θ j d))
Causalean.Experimentation.ExposureMappingInterference.htVarEst · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:50 · uses FiniteDesign
def htCovEst reviewed
Causalean.Experimentation.ExposureMappingInterference

For a finite assignment space, a finite unit population, a unit-trait space, an exposure space, a randomization design, exposure-indexed potential outcomes, an exposure mapping, unit traits, two exposure levels, and an assignment, the Horvitz--Thompson covariance estimator is its ordered-pair cross-exposure term over distinct units minus its single-unit Young correction.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
z :
Ω
def
htCovEst D y f θ dk dl z :
ℝ
given by
(∑ i, ∑ j ∈ Finset.univ.erase i, expoInd f θ i dk z * expoInd f θ j dl z * ((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((Yobs y f θ i z / prop D f θ i dk) * (Yobs y f θ j z / prop D f θ j dl)))
- ∑ i, (expoInd f θ i dk z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dk) + expoInd f θ i dl z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dl))
Causalean.Experimentation.ExposureMappingInterference.htCovEst · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:68 · uses FiniteDesign
def htEffectVarEst reviewed
Causalean.Experimentation.ExposureMappingInterference

For a finite assignment space, a finite unit population, a unit-trait space, an exposure space, a randomization design, exposure-indexed potential outcomes, an exposure mapping, unit traits, two exposure levels, and an assignment, the conservative effect-variance estimator is the sum of the two variance estimators minus twice the covariance estimator, divided by the square of the population size.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
z :
Ω
def
htEffectVarEst D y f θ dk dl z :
ℝ
given by
(htVarEst D y f θ dk z + htVarEst D y f θ dl z - 2 * htCovEst D y f θ dk dl z) / (Fintype.card ι : ℝ) ^ 2
Causalean.Experimentation.ExposureMappingInterference.htEffectVarEst · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:87 · uses FiniteDesign
theorem E_htEffectVarEst_ge reviewed
Causalean.Experimentation.ExposureMappingInterference

Positive-joint specialization of Proposition 5.6 (consvar). For a design and exposure model, suppose the two treatment arms are distinct, every unit has nonzero dk propensity, every unit has nonzero dl propensity, and every off-diagonal pair has nonzero dk same-arm joint propensity, nonzero dl same-arm joint propensity, and nonzero cross-arm joint propensity. Then the effect-variance estimator has nonnegative bias.

Formal statement
hypotheses
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
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
hjk :
∀ i j
if
i ≠ j
then
propPairSame D f θ i j dk ≠ 0
hjl :
∀ i j
if
i ≠ j
then
propPairSame D f θ i j dl ≠ 0
hjc :
∀ i j
if
i ≠ j
then
propPairCross D f θ i j dk dl ≠ 0
conclusion
D.Var (htEffect D y f θ dk dl) ≤ D.E (htEffectVarEst D y f θ dk dl)
Proof (Lean source)
theorem E_htEffectVarEst_ge (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) (hjk : ∀ i j, i ≠ j → propPairSame D f θ i j dk ≠ 0) (hjl : ∀ i j, i ≠ j → propPairSame D f θ i j dl ≠ 0) (hjc : ∀ i j, i ≠ j → propPairCross D f θ i j dk dl ≠ 0) : D.Var (htEffect D y f θ dk dl) ≤ D.E (htEffectVarEst D y f θ dk dl) := by set N : ℝ := (Fintype.card ι : ℝ) with hN -- Variance of the effect estimator in terms of the totals' moments. have hVar : D.Var (htEffect D y f θ dk dl) = N⁻¹ ^ 2 * (D.Var (htTotal D y f θ dk) + D.Var (htTotal D y f θ dl) - 2 * D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl)) := by rw [D.Var_congr (Y := fun z => N⁻¹ * (htTotal D y f θ dk z - htTotal D y f θ dl z)) (fun z => by unfold htEffect htMean; rw [div_eq_mul_inv, div_eq_mul_inv]; ring)] rw [FiniteDesign.Var_const_mul, FiniteDesign.Var_sub] -- Expectation of the variance estimator in terms of the same moments. have hE : D.E (htEffectVarEst D y f θ dk dl) = N⁻¹ ^ 2 * (D.Var (htTotal D y f θ dk) + D.Var (htTotal D y f θ dl) - 2 * D.E (htCovEst D y f θ dk dl)) := by rw [D.E_congr (Y := fun z => N⁻¹ ^ 2 * (htVarEst D y f θ dk z + htVarEst D y f θ dl z - 2 * htCovEst D y f θ dk dl z)) (fun z => by unfold htEffectVarEst; rw [div_eq_mul_inv, mul_comm, ← hN]; ring)] rw [D.E_const_mul] congr 1 rw [D.E_sub, D.E_add, D.E_const_mul, E_htVarEst D y f θ dk hk hjk, E_htVarEst D y f θ dl hl hjl] rw [hVar, hE] -- N⁻² ≥ 0, and E[htCovEst] ≤ Cov gives the bracket inequality. have hCov := E_htCovEst_le D y f θ dk dl hne hk hl hjc have hsq : (0 : ℝ) ≤ N⁻¹ ^ 2 := sq_nonneg _ apply mul_le_mul_of_nonneg_left _ hsq -- a + b - 2 Cov ≤ a + b - 2 E[htCovEst] since E[htCovEst] ≤ Cov have h2 : (2 : ℝ) * D.E (htCovEst D y f θ dk dl) ≤ 2 * D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl) := by apply mul_le_mul_of_nonneg_left hCov norm_num exact sub_le_sub_left h2 (D.Var (htTotal D y f θ dk) + D.Var (htTotal D y f θ dl))
Causalean.Experimentation.ExposureMappingInterference.E_htEffectVarEst_ge · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:272 · uses FiniteDesign , E , Var , htEffect , prop , propPairCross , propPairSame , htEffectVarEst
theorem E_htVarEst_eq_addBias reviewed
Causalean.Experimentation.ExposureMappingInterference

Proposition 5.1 (varbias). For a design and exposure model, an exposure level, and nonzero marginal exposure propensities, the expected estimator equals the true variance plus its zero-joint correction.

Formal statement
hypotheses
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
hpos :
∀ i, prop D f θ i d ≠ 0
conclusion
D.E (htVarEst D y f θ d)
= D.Var (htTotal D y f θ d)
+ ∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairSame D f θ i j d = 0 then (1:ℝ) else 0) * (y i d * y j d)
Proof (Lean source)
theorem E_htVarEst_eq_addBias (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (hpos : ∀ i, prop D f θ i d ≠ 0) : D.E (htVarEst D y f θ d) = D.Var (htTotal D y f θ d) + ∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairSame D f θ i j d = 0 then (1:ℝ) else 0) * (y i d * y j d) := by rw [Var_htTotal] unfold htVarEst rw [D.E_add, D.E_sum, D.E_sum] -- The diagonal sums coincide; the off-diagonal sums differ by the zero-joint correction. rw [add_assoc] congr 1 · -- diagonal sum (identical to `E_htVarEst`) refine Finset.sum_congr rfl (fun i _ => ?_) have key : (fun z => expoInd f θ i d z * (1 - prop D f θ i d) * (Yobs y f θ i z / prop D f θ i d) ^ 2) = (fun z => ((1 - prop D f θ i d) * (prop D f θ i d)⁻¹ ^ 2) * (expoInd f θ i d z * (Yobs y f θ i z) ^ 2)) := by funext z; rw [div_pow]; ring rw [key, D.E_const_mul] rw [D.E_congr (Y := fun z => expoInd f θ i d z * (y i d) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i d z)] rw [D.E_mul_const, E_expoInd] ring · -- off-diagonal: combine the estimator's off-diagonal expectation with the bias term, -- and show the result equals the true off-diagonal sum. rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_sum, ← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun j hj => ?_) have hji : j ≠ i := (Finset.mem_erase.mp hj).1 have hij : i ≠ j := fun h => hji h.symm have hi := hpos i have hjp := hpos j -- compute the expectation of the estimator's off-diagonal term have key : (fun z => expoInd f θ i d z * expoInd f θ j d z * ((propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d) / propPairSame D f θ i j d) * ((Yobs y f θ i z / prop D f θ i d) * (Yobs y f θ j z / prop D f θ j d))) = (fun z => (((propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d) / propPairSame D f θ i j d) * ((prop D f θ i d)⁻¹ * (prop D f θ j d)⁻¹)) * (expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z * Yobs y f θ j z)) := by funext z; ring rw [key, D.E_const_mul] have hprod : D.E (fun z => expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z * Yobs y f θ j z) = y i d * y j d * propPairSame D f θ i j d := by rw [D.E_congr (Y := fun z => (y i d * y j d) * (expoInd f θ i d z * expoInd f θ j d z)) (fun z => ?_)] · rw [D.E_const_mul]; rfl · have h1 : expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z = expoInd f θ i d z * expoInd f θ j d z * y i d := expoInd₂_mul_Yobs y f θ i d (expoInd f θ j d) z have h2 : expoInd f θ j d z * expoInd f θ i d z * Yobs y f θ j z = expoInd f θ j d z * expoInd f θ i d z * y j d := expoInd₂_mul_Yobs y f θ j d (expoInd f θ i d) z calc expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z * Yobs y f θ j z = (expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z) * Yobs y f θ j z := by ring _ = (expoInd f θ i d z * expoInd f θ j d z * y i d) * Yobs y f θ j z := by rw [h1] _ = y i d * (expoInd f θ j d z * expoInd f θ i d z * Yobs y f θ j z) := by ring _ = y i d * (expoInd f θ j d z * expoInd f θ i d z * y j d) := by rw [h2] _ = (y i d * y j d) * (expoInd f θ i d z * expoInd f θ j d z) := by ring rw [hprod] -- now case split on whether the joint probability vanishes by_cases hz : propPairSame D f θ i j d = 0 · rw [if_pos hz, hz] -- estimator term vanishes (the `* (yᵢyⱼ * 0)` factor); true off-diagonal term is `−yᵢyⱼ`, -- the bias term `+ yᵢyⱼ` exactly cancels it, both sides equal `0`. rw [mul_zero, mul_zero, zero_sub, one_mul] field_simp ring · rw [if_neg hz, zero_mul, add_zero] -- estimator term equals true off-diagonal term (positive-joint cancellation) rw [div_mul_eq_mul_div, div_mul_eq_mul_div, div_mul_eq_mul_div, mul_div_assoc, mul_div_assoc, mul_div_assoc, div_self hz] ring
Causalean.Experimentation.ExposureMappingInterference.E_htVarEst_eq_addBias · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:319 · uses FiniteDesign , E , Var , htTotal , prop , propPairSame , htVarEst
def htA2 reviewed
Causalean.Experimentation.ExposureMappingInterference

For a finite assignment space, a finite unit population, a unit-trait space, an exposure space, a randomization design, exposure-indexed potential outcomes, an exposure mapping, unit traits, an exposure level, and an assignment, the Young-inequality correction adds, over every ordered pair of distinct units with zero same-exposure joint probability, the two corresponding half-weighted squared observed-outcome terms.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
d :
Δ
z :
Ω
def
htA2 D y f θ d z :
ℝ
given by
∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairSame D f θ i j d = 0 then (1:ℝ) else 0) * (expoInd f θ i d z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i d) + expoInd f θ j d z * (Yobs y f θ j z) ^ 2 / (2 * prop D f θ j d))
Causalean.Experimentation.ExposureMappingInterference.htA2 · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:404 · uses FiniteDesign
def htCovEstA reviewed
Causalean.Experimentation.ExposureMappingInterference

For a finite assignment space, a finite unit population, a unit-trait space, an exposure space, a randomization design, exposure-indexed potential outcomes, an exposure mapping, unit traits, two exposure levels, and an assignment, the general Horvitz--Thompson covariance estimator is its distinct-unit cross-exposure sum minus a Young correction over every ordered pair with zero cross-exposure joint probability.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
z :
Ω
def
htCovEstA D y f θ dk dl z :
ℝ
given by
(∑ i, ∑ j ∈ Finset.univ.erase i, expoInd f θ i dk z * expoInd f θ j dl z * ((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((Yobs y f θ i z / prop D f θ i dk) * (Yobs y f θ j z / prop D f θ j dl)))
- ∑ i, ∑ j, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * (expoInd f θ i dk z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dk) + expoInd f θ j dl z * (Yobs y f θ j z) ^ 2 / (2 * prop D f θ j dl))
Causalean.Experimentation.ExposureMappingInterference.htCovEstA · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:582 · uses FiniteDesign
def htEffectVarEstA reviewed
Causalean.Experimentation.ExposureMappingInterference

For a finite assignment space, a finite unit population, a unit-trait space, an exposure space, a randomization design, exposure-indexed potential outcomes, an exposure mapping, unit traits, two exposure levels, and an assignment, the general conservative effect-variance estimator is the two variance estimators and their Young corrections, minus twice the general covariance estimator, divided by the square of the population size.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
D :
FiniteDesign Ω
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
z :
Ω
def
htEffectVarEstA D y f θ dk dl z :
ℝ
given by
(htVarEst D y f θ dk z + htA2 D y f θ dk z + htVarEst D y f θ dl z + htA2 D y f θ dl z - 2 * htCovEstA D y f θ dk dl z) / (Fintype.card ι : ℝ) ^ 2
Causalean.Experimentation.ExposureMappingInterference.htEffectVarEstA · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:785 · uses FiniteDesign
theorem E_htEffectVarEstA_ge reviewed
Causalean.Experimentation.ExposureMappingInterference

Proposition 5.6 (consvar). For a design and exposure model, suppose the two treatment arms are distinct, every unit has nonzero dk propensity, and every unit has nonzero dl propensity, without any positive-joint assumption. Then the general effect-variance estimator has nonnegative bias.

Formal statement
hypotheses
Ω :
Type u_1
shared
ι :
Type u_2
shared
Θ :
Type u_3
shared
Δ :
Type u_4
shared
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.Var (htEffect D y f θ dk dl) ≤ D.E (htEffectVarEstA D y f θ dk dl)
Proof (Lean source)
theorem E_htEffectVarEstA_ge (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.Var (htEffect D y f θ dk dl) ≤ D.E (htEffectVarEstA D y f θ dk dl) := by set N : ℝ := (Fintype.card ι : ℝ) with hN -- Variance of the effect estimator in terms of the totals' moments. have hVar : D.Var (htEffect D y f θ dk dl) = N⁻¹ ^ 2 * (D.Var (htTotal D y f θ dk) + D.Var (htTotal D y f θ dl) - 2 * D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl)) := by rw [D.Var_congr (Y := fun z => N⁻¹ * (htTotal D y f θ dk z - htTotal D y f θ dl z)) (fun z => by unfold htEffect htMean; rw [div_eq_mul_inv, div_eq_mul_inv]; ring)] rw [FiniteDesign.Var_const_mul, FiniteDesign.Var_sub] -- Expectation of the variance estimator in terms of the corrected moments. have hE : D.E (htEffectVarEstA D y f θ dk dl) = N⁻¹ ^ 2 * (D.E (fun z => htVarEst D y f θ dk z + htA2 D y f θ dk z) + D.E (fun z => htVarEst D y f θ dl z + htA2 D y f θ dl z) - 2 * D.E (htCovEstA D y f θ dk dl)) := by rw [D.E_congr (Y := fun z => N⁻¹ ^ 2 * ((htVarEst D y f θ dk z + htA2 D y f θ dk z) + (htVarEst D y f θ dl z + htA2 D y f θ dl z) - 2 * htCovEstA D y f θ dk dl z)) (fun z => by unfold htEffectVarEstA; rw [div_eq_mul_inv, mul_comm, ← hN]; ring)] rw [D.E_const_mul] congr 1 rw [D.E_sub, D.E_add, D.E_const_mul] rw [hVar, hE] -- N⁻² ≥ 0; Prop 5.2 twice and Prop 5.5 bound the bracket. have hsq : (0 : ℝ) ≤ N⁻¹ ^ 2 := sq_nonneg _ apply mul_le_mul_of_nonneg_left _ hsq have hAk := E_htVarEst_add_htA2_ge D y f θ dk hk have hAl := E_htVarEst_add_htA2_ge D y f θ dl hl have hCov := E_htCovEstA_le D y f θ dk dl hne hk hl have h2 : (2 : ℝ) * D.E (htCovEstA D y f θ dk dl) ≤ 2 * D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl) := mul_le_mul_of_nonneg_left hCov (by norm_num) -- Var dk + Var dl - 2 Cov ≤ E[V̂dk+Â₂dk] + E[V̂dl+Â₂dl] - 2 E[Ĉov_A] exact sub_le_sub (add_le_add hAk hAl) h2
Causalean.Experimentation.ExposureMappingInterference.E_htEffectVarEstA_ge · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:800 · uses FiniteDesign , E , Var , htEffect , prop , htEffectVarEstA
5 supporting declarations (lemmas, instances)
  • E_htVarEst theorem — Lemma 5.1 (varun). In the positive-joint regime — every unit has nonzero exposure propensity under d and every off-diagonal pair has nonzero same-arm joint exposure propensity under d — the Horvitz–Thompson variance estimator is exactly unbiased for the true design variance of the HT total.
    hypotheses
    Ω :
    Type u_1
    shared
    ι :
    Type u_2
    shared
    Θ :
    Type u_3
    shared
    Δ :
    Type u_4
    shared
    D :
    FiniteDesign Ω
    y :
    ι → Δ → ℝ
    f :
    Ω → Θ → Δ
    θ :
    ι → Θ
    d :
    Δ
    hpos :
    ∀ i, prop D f θ i d ≠ 0
    hjoint :
    ∀ i j
    if
    i ≠ j
    then
    propPairSame D f θ i j d ≠ 0
    conclusion
    D.E (htVarEst D y f θ d) = D.Var (htTotal D y f θ d)
    Proof (Lean source)
    theorem E_htVarEst (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (hpos : ∀ i, prop D f θ i d ≠ 0) (hjoint : ∀ i j, i ≠ j → propPairSame D f θ i j d ≠ 0) : D.E (htVarEst D y f θ d) = D.Var (htTotal D y f θ d) := by rw [Var_htTotal] unfold htVarEst rw [D.E_add, D.E_sum, D.E_sum] congr 1 · -- diagonal sum refine Finset.sum_congr rfl (fun i _ => ?_) have key : (fun z => expoInd f θ i d z * (1 - prop D f θ i d) * (Yobs y f θ i z / prop D f θ i d) ^ 2) = (fun z => ((1 - prop D f θ i d) * (prop D f θ i d)⁻¹ ^ 2) * (expoInd f θ i d z * (Yobs y f θ i z) ^ 2)) := by funext z; rw [div_pow]; ring rw [key, D.E_const_mul] rw [D.E_congr (Y := fun z => expoInd f θ i d z * (y i d) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i d z)] rw [D.E_mul_const, E_expoInd] ring · -- off-diagonal sum refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_sum] refine Finset.sum_congr rfl (fun j hj => ?_) have hji : j ≠ i := (Finset.mem_erase.mp hj).1 have hij : i ≠ j := fun h => hji h.symm have hjoint_ij := hjoint i j hij have hi := hpos i have hjp := hpos j -- factor constants out of the expectation have key : (fun z => expoInd f θ i d z * expoInd f θ j d z * ((propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d) / propPairSame D f θ i j d) * ((Yobs y f θ i z / prop D f θ i d) * (Yobs y f θ j z / prop D f θ j d))) = (fun z => (((propPairSame D f θ i j d - prop D f θ i d * prop D f θ j d) / propPairSame D f θ i j d) * ((prop D f θ i d)⁻¹ * (prop D f θ j d)⁻¹)) * (expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z * Yobs y f θ j z)) := by funext z; ring rw [key, D.E_const_mul] -- now evaluate E of the product of indicators times both observed outcomes have hprod : D.E (fun z => expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z * Yobs y f θ j z) = y i d * y j d * propPairSame D f θ i j d := by rw [D.E_congr (Y := fun z => (y i d * y j d) * (expoInd f θ i d z * expoInd f θ j d z)) (fun z => ?_)] · rw [D.E_const_mul]; rfl · -- force both outcomes via expoInd₂_mul_Yobs and its symmetric use have h1 : expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z = expoInd f θ i d z * expoInd f θ j d z * y i d := expoInd₂_mul_Yobs y f θ i d (expoInd f θ j d) z have h2 : expoInd f θ j d z * expoInd f θ i d z * Yobs y f θ j z = expoInd f θ j d z * expoInd f θ i d z * y j d := expoInd₂_mul_Yobs y f θ j d (expoInd f θ i d) z calc expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z * Yobs y f θ j z = (expoInd f θ i d z * expoInd f θ j d z * Yobs y f θ i z) * Yobs y f θ j z := by ring _ = (expoInd f θ i d z * expoInd f θ j d z * y i d) * Yobs y f θ j z := by rw [h1] _ = y i d * (expoInd f θ j d z * expoInd f θ i d z * Yobs y f θ j z) := by ring _ = y i d * (expoInd f θ j d z * expoInd f θ i d z * y j d) := by rw [h2] _ = (y i d * y j d) * (expoInd f θ i d z * expoInd f θ j d z) := by ring rw [hprod] rw [div_mul_eq_mul_div, div_mul_eq_mul_div, div_mul_eq_mul_div, mul_div_assoc, mul_div_assoc, mul_div_assoc, div_self hjoint_ij] ring
    Causalean.Experimentation.ExposureMappingInterference.E_htVarEst · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:100
  • E_htCovEst_le theorem — Proposition 5.3 (ncov). For a design and exposure model, suppose the two treatment arms are distinct, every unit has nonzero dk propensity, every unit has nonzero dl propensity, and every off-diagonal pair has nonzero cross-arm joint propensity. Then the covariance estimator is nonpositively biased for the true covariance.
    hypotheses
    Ω :
    Type u_1
    shared
    ι :
    Type u_2
    shared
    Θ :
    Type u_3
    shared
    Δ :
    Type u_4
    shared
    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
    hjoint :
    ∀ i j
    if
    i ≠ j
    then
    propPairCross D f θ i j dk dl ≠ 0
    conclusion
    D.E (htCovEst D y f θ dk dl) ≤ D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl)
    Proof (Lean source)
    theorem E_htCovEst_le (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) (hjoint : ∀ i j, i ≠ j → propPairCross D f θ i j dk dl ≠ 0) : D.E (htCovEst D y f θ dk dl) ≤ D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl) := by rw [Cov_htTotal D y f θ dk dl hne hk hl] -- compute the expectation of the covariance estimator have hE : D.E (htCovEst D y f θ dk 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) ^ 2 / 2 + (y i dl) ^ 2 / 2) := by unfold htCovEst rw [D.E_sub, D.E_sum, D.E_sum] congr 1 · -- off-diagonal sum (same cancellation as the variance case) refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_sum] refine Finset.sum_congr rfl (fun j hj => ?_) have hji : j ≠ i := (Finset.mem_erase.mp hj).1 have hij : i ≠ j := fun h => hji h.symm have hjoint_ij := hjoint i j hij have hidk := hk i have hjdl := hl j have key : (fun z => expoInd f θ i dk z * expoInd f θ j dl z * ((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((Yobs y f θ i z / prop D f θ i dk) * (Yobs y f θ j z / prop D f θ j dl))) = (fun z => (((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((prop D f θ i dk)⁻¹ * (prop D f θ j dl)⁻¹)) * (expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z)) := by funext z; ring rw [key, D.E_const_mul] have hprod : D.E (fun z => expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z) = y i dk * y j dl * propPairCross D f θ i j dk dl := by rw [D.E_congr (Y := fun z => (y i dk * y j dl) * (expoInd f θ i dk z * expoInd f θ j dl z)) (fun z => ?_)] · rw [D.E_const_mul]; rfl · have h1 : expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z = expoInd f θ i dk z * expoInd f θ j dl z * y i dk := expoInd₂_mul_Yobs y f θ i dk (expoInd f θ j dl) z have h2 : expoInd f θ j dl z * expoInd f θ i dk z * Yobs y f θ j z = expoInd f θ j dl z * expoInd f θ i dk z * y j dl := expoInd₂_mul_Yobs y f θ j dl (expoInd f θ i dk) z calc expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z = (expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z) * Yobs y f θ j z := by ring _ = (expoInd f θ i dk z * expoInd f θ j dl z * y i dk) * Yobs y f θ j z := by rw [h1] _ = y i dk * (expoInd f θ j dl z * expoInd f θ i dk z * Yobs y f θ j z) := by ring _ = y i dk * (expoInd f θ j dl z * expoInd f θ i dk z * y j dl) := by rw [h2] _ = (y i dk * y j dl) * (expoInd f θ i dk z * expoInd f θ j dl z) := by ring rw [hprod] rw [div_mul_eq_mul_div, div_mul_eq_mul_div, div_mul_eq_mul_div, mul_div_assoc, mul_div_assoc, mul_div_assoc, div_self hjoint_ij] ring · -- diagonal correction sum refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_add] have hidk := hk i have hidl := hl i congr 1 · have key : (fun z => expoInd f θ i dk z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dk)) = (fun z => (2 * prop D f θ i dk)⁻¹ * (expoInd f θ i dk z * (Yobs y f θ i z) ^ 2)) := by funext z; rw [div_eq_mul_inv]; ring rw [key, D.E_const_mul, D.E_congr (Y := fun z => expoInd f θ i dk z * (y i dk) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i dk z), D.E_mul_const, E_expoInd] rw [mul_inv, show (2:ℝ)⁻¹ * (prop D f θ i dk)⁻¹ * (prop D f θ i dk * y i dk ^ 2) = (2:ℝ)⁻¹ * y i dk ^ 2 * ((prop D f θ i dk)⁻¹ * prop D f θ i dk) by ring, inv_mul_cancel₀ hidk] ring · have key : (fun z => expoInd f θ i dl z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dl)) = (fun z => (2 * prop D f θ i dl)⁻¹ * (expoInd f θ i dl z * (Yobs y f θ i z) ^ 2)) := by funext z; rw [div_eq_mul_inv]; ring rw [key, D.E_const_mul, D.E_congr (Y := fun z => expoInd f θ i dl z * (y i dl) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i dl z), D.E_mul_const, E_expoInd] rw [mul_inv, show (2:ℝ)⁻¹ * (prop D f θ i dl)⁻¹ * (prop D f θ i dl * y i dl ^ 2) = (2:ℝ)⁻¹ * y i dl ^ 2 * ((prop D f θ i dl)⁻¹ * prop D f θ i dl) by ring, inv_mul_cancel₀ hidl] ring rw [hE] -- now: offdiag - ∑ ((y dk)²+(y dl)²)/2 ≤ offdiag - ∑ y dk y dl apply sub_le_sub_left -- ∑ y dk y dl ≤ ∑ ((y dk)²+(y dl)²)/2, termwise via Young's inequality rw [← sub_nonneg, ← Finset.sum_sub_distrib] refine Finset.sum_induction _ (0 ≤ ·) (fun a b ha hb => add_nonneg ha hb) le_rfl (fun i _ => ?_) rw [show y i dk ^ 2 / 2 + y i dl ^ 2 / 2 - y i dk * y i dl = (y i dk - y i dl) ^ 2 / 2 by ring] exact div_nonneg (sq_nonneg _) (by norm_num)
    Causalean.Experimentation.ExposureMappingInterference.E_htCovEst_le · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:169
  • E_htVarEst_add_htA2_ge theorem — Proposition 5.2 (a2). For a design and exposure model, an exposure level, and nonzero marginal exposure propensities, adding the Young correction to the variance estimator gives nonnegative bias.
    hypotheses
    Ω :
    Type u_1
    shared
    ι :
    Type u_2
    shared
    Θ :
    Type u_3
    shared
    Δ :
    Type u_4
    shared
    D :
    FiniteDesign Ω
    y :
    ι → Δ → ℝ
    f :
    Ω → Θ → Δ
    θ :
    ι → Θ
    d :
    Δ
    hpos :
    ∀ i, prop D f θ i d ≠ 0
    conclusion
    D.Var (htTotal D y f θ d) ≤ D.E (fun z => htVarEst D y f θ d z + htA2 D y f θ d z)
    Proof (Lean source)
    theorem E_htVarEst_add_htA2_ge (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (d : Δ) (hpos : ∀ i, prop D f θ i d ≠ 0) : D.Var (htTotal D y f θ d) ≤ D.E (fun z => htVarEst D y f θ d z + htA2 D y f θ d z) := by rw [D.E_add, E_htVarEst_eq_addBias D y f θ d hpos] -- E[Â₂] = ∑_{π_{ij}=0} (y_i²/2 + y_j²/2) have hEA2 : D.E (htA2 D y f θ d) = ∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairSame D f θ i j d = 0 then (1:ℝ) else 0) * ((y i d) ^ 2 / 2 + (y j d) ^ 2 / 2) := by unfold htA2 rw [D.E_sum] refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_sum] refine Finset.sum_congr rfl (fun j hj => ?_) have hi := hpos i have hjp := hpos j have key : (fun z => (if propPairSame D f θ i j d = 0 then (1:ℝ) else 0) * (expoInd f θ i d z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i d) + expoInd f θ j d z * (Yobs y f θ j z) ^ 2 / (2 * prop D f θ j d))) = (fun z => (if propPairSame D f θ i j d = 0 then (1:ℝ) else 0) * ((2 * prop D f θ i d)⁻¹ * (expoInd f θ i d z * (Yobs y f θ i z) ^ 2) + (2 * prop D f θ j d)⁻¹ * (expoInd f θ j d z * (Yobs y f θ j z) ^ 2))) := by funext z; rw [div_eq_mul_inv, div_eq_mul_inv]; ring rw [key, D.E_const_mul, D.E_add, D.E_const_mul, D.E_const_mul, D.E_congr (Y := fun z => expoInd f θ i d z * (y i d) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i d z), D.E_congr (X := fun z => expoInd f θ j d z * (Yobs y f θ j z) ^ 2) (Y := fun z => expoInd f θ j d z * (y j d) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ j d z), D.E_mul_const, D.E_mul_const, E_expoInd, E_expoInd] rw [mul_inv, mul_inv] congr 1 rw [show (2:ℝ)⁻¹ * (prop D f θ i d)⁻¹ * (prop D f θ i d * y i d ^ 2) = (2:ℝ)⁻¹ * y i d ^ 2 * ((prop D f θ i d)⁻¹ * prop D f θ i d) by ring, inv_mul_cancel₀ hi, show (2:ℝ)⁻¹ * (prop D f θ j d)⁻¹ * (prop D f θ j d * y j d ^ 2) = (2:ℝ)⁻¹ * y j d ^ 2 * ((prop D f θ j d)⁻¹ * prop D f θ j d) by ring, inv_mul_cancel₀ hjp] ring rw [hEA2] -- Var + A + E[Â₂] = Var + ∑_{zero}(y_i+y_j)²/2 ≥ Var rw [add_assoc] apply le_add_of_nonneg_right rw [← Finset.sum_add_distrib] refine Finset.sum_nonneg (fun i _ => ?_) rw [← Finset.sum_add_distrib] refine Finset.sum_nonneg (fun j _ => ?_) by_cases hz : propPairSame D f θ i j d = 0 · rw [if_pos hz, one_mul, one_mul, show y i d * y j d + (y i d ^ 2 / 2 + y j d ^ 2 / 2) = (y i d + y j d) ^ 2 / 2 by ring] exact div_nonneg (sq_nonneg _) (by norm_num) · rw [if_neg hz, zero_mul, zero_mul, add_zero]
    Causalean.Experimentation.ExposureMappingInterference.E_htVarEst_add_htA2_ge · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:422
  • E_htCovEst_eq_of_noEffect theorem — Proposition 5.4 (no_bias_cov). For a design and exposure model, suppose the two treatment arms are distinct, every unit has nonzero dk propensity, every unit has nonzero dl propensity, every off-diagonal pair has nonzero cross-arm joint propensity, and the two exposures share the same potential outcomes. Then the covariance estimator is exactly unbiased for the true covariance: the Young diagonal correction (y_i²/2 + y_i²/2) = y_i² = y_i(dk)y_i(dl) is exact, so the nonpositive bias of Proposition 5.3 vanishes.
    hypotheses
    Ω :
    Type u_1
    shared
    ι :
    Type u_2
    shared
    Θ :
    Type u_3
    shared
    Δ :
    Type u_4
    shared
    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
    hjc :
    ∀ i j
    if
    i ≠ j
    then
    propPairCross D f θ i j dk dl ≠ 0
    heq :
    ∀ i, y i dk = y i dl
    conclusion
    D.E (htCovEst D y f θ dk dl) = D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl)
    Proof (Lean source)
    theorem E_htCovEst_eq_of_noEffect (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) (hjc : ∀ i j, i ≠ j → propPairCross D f θ i j dk dl ≠ 0) (heq : ∀ i, y i dk = y i dl) : D.E (htCovEst D y f θ dk dl) = D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl) := by rw [Cov_htTotal D y f θ dk dl hne hk hl] have hE : D.E (htCovEst D y f θ dk 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) ^ 2 / 2 + (y i dl) ^ 2 / 2) := by unfold htCovEst rw [D.E_sub, D.E_sum, D.E_sum] congr 1 · refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_sum] refine Finset.sum_congr rfl (fun j hj => ?_) have hji : j ≠ i := (Finset.mem_erase.mp hj).1 have hij : i ≠ j := fun h => hji h.symm have hjoint_ij := hjc i j hij have hidk := hk i have hjdl := hl j have key : (fun z => expoInd f θ i dk z * expoInd f θ j dl z * ((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((Yobs y f θ i z / prop D f θ i dk) * (Yobs y f θ j z / prop D f θ j dl))) = (fun z => (((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((prop D f θ i dk)⁻¹ * (prop D f θ j dl)⁻¹)) * (expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z)) := by funext z; ring rw [key, D.E_const_mul] have hprod : D.E (fun z => expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z) = y i dk * y j dl * propPairCross D f θ i j dk dl := by rw [D.E_congr (Y := fun z => (y i dk * y j dl) * (expoInd f θ i dk z * expoInd f θ j dl z)) (fun z => ?_)] · rw [D.E_const_mul]; rfl · have h1 : expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z = expoInd f θ i dk z * expoInd f θ j dl z * y i dk := expoInd₂_mul_Yobs y f θ i dk (expoInd f θ j dl) z have h2 : expoInd f θ j dl z * expoInd f θ i dk z * Yobs y f θ j z = expoInd f θ j dl z * expoInd f θ i dk z * y j dl := expoInd₂_mul_Yobs y f θ j dl (expoInd f θ i dk) z calc expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z = (expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z) * Yobs y f θ j z := by ring _ = (expoInd f θ i dk z * expoInd f θ j dl z * y i dk) * Yobs y f θ j z := by rw [h1] _ = y i dk * (expoInd f θ j dl z * expoInd f θ i dk z * Yobs y f θ j z) := by ring _ = y i dk * (expoInd f θ j dl z * expoInd f θ i dk z * y j dl) := by rw [h2] _ = (y i dk * y j dl) * (expoInd f θ i dk z * expoInd f θ j dl z) := by ring rw [hprod] rw [div_mul_eq_mul_div, div_mul_eq_mul_div, div_mul_eq_mul_div, mul_div_assoc, mul_div_assoc, mul_div_assoc, div_self hjoint_ij] ring · refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_add] have hidk := hk i have hidl := hl i congr 1 · have key : (fun z => expoInd f θ i dk z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dk)) = (fun z => (2 * prop D f θ i dk)⁻¹ * (expoInd f θ i dk z * (Yobs y f θ i z) ^ 2)) := by funext z; rw [div_eq_mul_inv]; ring rw [key, D.E_const_mul, D.E_congr (Y := fun z => expoInd f θ i dk z * (y i dk) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i dk z), D.E_mul_const, E_expoInd] rw [mul_inv, show (2:ℝ)⁻¹ * (prop D f θ i dk)⁻¹ * (prop D f θ i dk * y i dk ^ 2) = (2:ℝ)⁻¹ * y i dk ^ 2 * ((prop D f θ i dk)⁻¹ * prop D f θ i dk) by ring, inv_mul_cancel₀ hidk] ring · have key : (fun z => expoInd f θ i dl z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dl)) = (fun z => (2 * prop D f θ i dl)⁻¹ * (expoInd f θ i dl z * (Yobs y f θ i z) ^ 2)) := by funext z; rw [div_eq_mul_inv]; ring rw [key, D.E_const_mul, D.E_congr (Y := fun z => expoInd f θ i dl z * (y i dl) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i dl z), D.E_mul_const, E_expoInd] rw [mul_inv, show (2:ℝ)⁻¹ * (prop D f θ i dl)⁻¹ * (prop D f θ i dl * y i dl ^ 2) = (2:ℝ)⁻¹ * y i dl ^ 2 * ((prop D f θ i dl)⁻¹ * prop D f θ i dl) by ring, inv_mul_cancel₀ hidl] ring rw [hE] -- the diagonal correction equals ∑ y_i(dk) y_i(dl) exactly under `heq` congr 1 refine Finset.sum_congr rfl (fun i _ => ?_) rw [heq i]; ring
    Causalean.Experimentation.ExposureMappingInterference.E_htCovEst_eq_of_noEffect · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:481
  • E_htCovEstA_le theorem — Proposition 5.5 (cova). For a design and exposure model, suppose the two treatment arms are distinct, every unit has nonzero dk propensity, and every unit has nonzero dl propensity, without a positive-cross-joint assumption. Then the general covariance estimator is nonpositively biased for the true covariance: zero-cross-joint off-diagonal pairs drop from the first sum, while the Young correction (summing over every j with π_{ij}(dk,dl)=0, including the diagonal) dominates the corresponding −y_i(dk)y_j(dl) covariance contributions termwise via y_i(dk)y_j(dl) ≤ y_i(dk)²/2 + y_j(dl)²/2.
    hypotheses
    Ω :
    Type u_1
    shared
    ι :
    Type u_2
    shared
    Θ :
    Type u_3
    shared
    Δ :
    Type u_4
    shared
    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.E (htCovEstA D y f θ dk dl) ≤ D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl)
    Proof (Lean source)
    theorem E_htCovEstA_le (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.E (htCovEstA D y f θ dk dl) ≤ D.Cov (htTotal D y f θ dk) (htTotal D y f θ dl) := by rw [Cov_htTotal D y f θ dk dl hne hk hl] -- expectation of the general covariance estimator have hE : D.E (htCovEstA D y f θ dk dl) = (∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (0:ℝ) else 1) * ((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, ∑ j, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * ((y i dk) ^ 2 / 2 + (y j dl) ^ 2 / 2) := by unfold htCovEstA rw [D.E_sub, D.E_sum, D.E_sum] congr 1 · -- first (off-diagonal) sum refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_sum] refine Finset.sum_congr rfl (fun j hj => ?_) have hji : j ≠ i := (Finset.mem_erase.mp hj).1 have hij : i ≠ j := fun h => hji h.symm have hidk := hk i have hjdl := hl j have key : (fun z => expoInd f θ i dk z * expoInd f θ j dl z * ((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((Yobs y f θ i z / prop D f θ i dk) * (Yobs y f θ j z / prop D f θ j dl))) = (fun z => (((propPairCross D f θ i j dk dl - prop D f θ i dk * prop D f θ j dl) / propPairCross D f θ i j dk dl) * ((prop D f θ i dk)⁻¹ * (prop D f θ j dl)⁻¹)) * (expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z)) := by funext z; ring rw [key, D.E_const_mul] have hprod : D.E (fun z => expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z) = y i dk * y j dl * propPairCross D f θ i j dk dl := by rw [D.E_congr (Y := fun z => (y i dk * y j dl) * (expoInd f θ i dk z * expoInd f θ j dl z)) (fun z => ?_)] · rw [D.E_const_mul]; rfl · have h1 : expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z = expoInd f θ i dk z * expoInd f θ j dl z * y i dk := expoInd₂_mul_Yobs y f θ i dk (expoInd f θ j dl) z have h2 : expoInd f θ j dl z * expoInd f θ i dk z * Yobs y f θ j z = expoInd f θ j dl z * expoInd f θ i dk z * y j dl := expoInd₂_mul_Yobs y f θ j dl (expoInd f θ i dk) z calc expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z * Yobs y f θ j z = (expoInd f θ i dk z * expoInd f θ j dl z * Yobs y f θ i z) * Yobs y f θ j z := by ring _ = (expoInd f θ i dk z * expoInd f θ j dl z * y i dk) * Yobs y f θ j z := by rw [h1] _ = y i dk * (expoInd f θ j dl z * expoInd f θ i dk z * Yobs y f θ j z) := by ring _ = y i dk * (expoInd f θ j dl z * expoInd f θ i dk z * y j dl) := by rw [h2] _ = (y i dk * y j dl) * (expoInd f θ i dk z * expoInd f θ j dl z) := by ring rw [hprod] by_cases hz : propPairCross D f θ i j dk dl = 0 · rw [if_pos hz, zero_mul, hz, mul_zero, mul_zero] · rw [if_neg hz, one_mul] rw [div_mul_eq_mul_div, div_mul_eq_mul_div, div_mul_eq_mul_div, mul_div_assoc, mul_div_assoc, mul_div_assoc, div_self hz] ring · -- Young correction sum (over all j) refine Finset.sum_congr rfl (fun i _ => ?_) rw [D.E_sum] refine Finset.sum_congr rfl (fun j _ => ?_) have hidk := hk i have hjdl := hl j have key : (fun z => (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * (expoInd f θ i dk z * (Yobs y f θ i z) ^ 2 / (2 * prop D f θ i dk) + expoInd f θ j dl z * (Yobs y f θ j z) ^ 2 / (2 * prop D f θ j dl))) = (fun z => (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * ((2 * prop D f θ i dk)⁻¹ * (expoInd f θ i dk z * (Yobs y f θ i z) ^ 2) + (2 * prop D f θ j dl)⁻¹ * (expoInd f θ j dl z * (Yobs y f θ j z) ^ 2))) := by funext z; rw [div_eq_mul_inv, div_eq_mul_inv]; ring rw [key, D.E_const_mul, D.E_add, D.E_const_mul, D.E_const_mul, D.E_congr (Y := fun z => expoInd f θ i dk z * (y i dk) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ i dk z), D.E_congr (X := fun z => expoInd f θ j dl z * (Yobs y f θ j z) ^ 2) (Y := fun z => expoInd f θ j dl z * (y j dl) ^ 2) (fun z => expoInd_mul_Yobs_sq y f θ j dl z), D.E_mul_const, D.E_mul_const, E_expoInd, E_expoInd] rw [mul_inv, mul_inv] congr 1 rw [show (2:ℝ)⁻¹ * (prop D f θ i dk)⁻¹ * (prop D f θ i dk * y i dk ^ 2) = (2:ℝ)⁻¹ * y i dk ^ 2 * ((prop D f θ i dk)⁻¹ * prop D f θ i dk) by ring, inv_mul_cancel₀ hidk, show (2:ℝ)⁻¹ * (prop D f θ j dl)⁻¹ * (prop D f θ j dl * y j dl ^ 2) = (2:ℝ)⁻¹ * y j dl ^ 2 * ((prop D f θ j dl)⁻¹ * prop D f θ j dl) by ring, inv_mul_cancel₀ hjdl] ring rw [hE] -- Compare to eq:totals_covariance: it suffices to show -- Cov - E[htCovEstA] = ∑_diag Young-gap + ∑_offdiag Young-gap ≥ 0. rw [← sub_nonneg] -- Rewrite the goal's Cov first sum (full off-diagonal) by splitting on π_{ij}=0. have hsplit : (∑ 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, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (0:ℝ) else 1) * ((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, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * (- (y i dk * y j dl)) := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun j hj => ?_) have hji : j ≠ i := (Finset.mem_erase.mp hj).1 have hidk := hk i have hjdl := hl j by_cases hz : propPairCross D f θ i j dk dl = 0 · rw [if_pos hz, if_pos hz, zero_mul, zero_add, one_mul, hz] field_simp ring · rw [if_neg hz, if_neg hz, one_mul, zero_mul, add_zero] rw [hsplit] -- Split the all-j Young sum into diagonal (j=i) and off-diagonal (j≠i). have hYoung : (∑ i, ∑ j, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * ((y i dk) ^ 2 / 2 + (y j dl) ^ 2 / 2)) = (∑ i, ((y i dk) ^ 2 / 2 + (y i dl) ^ 2 / 2)) + ∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * ((y i dk) ^ 2 / 2 + (y j dl) ^ 2 / 2) := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.add_sum_erase univ _ (Finset.mem_univ i)] congr 1 -- diagonal j = i: indicator is 1 since π_{ii}(dk,dl)=0 rw [propPairCross_self_of_ne D f θ i hne, if_pos rfl, one_mul] rw [hYoung] -- Name the off-diagonal positive-joint sum `P` (it cancels) and reduce to a gap of -- nonnegative diagonal + off-diagonal Young corrections. set P : ℝ := ∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (0:ℝ) else 1) * ((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))) with hP -- Goal: 0 ≤ (P + Negyy) - (Diagyy + (P - (Diagyoung + Offyoung))) rw [show P + (∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * (- (y i dk * y j dl))) - (∑ i, y i dk * y i dl) - (P - (∑ i, ((y i dk) ^ 2 / 2 + (y i dl) ^ 2 / 2) + ∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * ((y i dk) ^ 2 / 2 + (y j dl) ^ 2 / 2))) = (∑ i, ((y i dk) ^ 2 / 2 + (y i dl) ^ 2 / 2) - ∑ i, y i dk * y i dl) + (∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * ((y i dk) ^ 2 / 2 + (y j dl) ^ 2 / 2) + ∑ i, ∑ j ∈ Finset.univ.erase i, (if propPairCross D f θ i j dk dl = 0 then (1:ℝ) else 0) * (- (y i dk * y j dl))) by ring] apply add_nonneg · -- diagonal gaps: ∑ᵢ (yᵢdk²/2 + yᵢdl²/2) - ∑ᵢ yᵢdkyᵢdl ≥ 0 rw [← Finset.sum_sub_distrib] refine Finset.sum_nonneg (fun i _ => ?_) rw [show (y i dk) ^ 2 / 2 + (y i dl) ^ 2 / 2 - y i dk * y i dl = (y i dk - y i dl) ^ 2 / 2 by ring] exact div_nonneg (sq_nonneg _) (by norm_num) · -- off-diagonal gaps rw [← Finset.sum_add_distrib] refine Finset.sum_nonneg (fun i _ => ?_) rw [← Finset.sum_add_distrib] refine Finset.sum_nonneg (fun j _ => ?_) by_cases hz : propPairCross D f θ i j dk dl = 0 · rw [if_pos hz, one_mul, one_mul, show (y i dk) ^ 2 / 2 + (y j dl) ^ 2 / 2 + - (y i dk * y j dl) = (y i dk - y j dl) ^ 2 / 2 by ring] exact div_nonneg (sq_nonneg _) (by norm_num) · rw [if_neg hz, zero_mul, zero_mul, add_zero]
    Causalean.Experimentation.ExposureMappingInterference.E_htCovEstA_le · Causalean/Experimentation/ExposureMappingInterference/Variance/Conservative.lean:605