Experimentation.ExposureMappingInterference.Asymptotics
Asymptotics for exposure-mapping interference: HT consistency, local-dependence CLTs, variance-estimator consistency, and Wald coverage.
Consistency 4 core · 1 supporting Along a sequence of nested finite-population experiments, the HT mean (hence effect) estimator converges in probability to its estimand under two conditions: * Condition 1 (boundedness): outcomes and inverse exposure pro ★ Experiment★ htMean_consistent_of_var
Consistency of the Horvitz–Thompson effect estimator (Aronow–Samii 2017, Prop 6.4)
Along a sequence of nested finite-population experiments, the HT mean (hence effect) estimator converges in probability to its estimand under two conditions:
* Condition 1 (boundedness): outcomes and inverse exposure probabilities are bounded,
so each weighted summand y_i(d)/π_i(d) is bounded by a constant c.
* Condition 2 (pairwise dependence): ∑_{i,j} g_{ij} = o(N²), where g_{ij}=0
whenever the exposure indicators of i and j are uncorrelated.
The proof is the lightweight-layer Chebyshev inequality applied to the O((N+∑g)/N²)
variance bound; no central limit theorem is needed.
structure Experiment reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
A design-based experiment on a finite population: a finite assignment space Ω equipped with a randomization design D over it, a finite population of units ι each assigned a trait in a trait space Θ, exposure-indexed potential outcomes y, one real value per unit and exposure in an exposure space Δ, and an exposure mapping f sending each assignment and unit trait to a realized exposure.
Definition (Lean source)
fields
Finite assignment space.
Ω :
Type
Fintype Ω
Finite population of units.
ι :
Unit-trait space.
Θ :
Type
Exposure space.
Δ :
Type
Randomization design.
D :
Exposure-indexed potential outcomes.
y :
ι → Δ → ℝ
Exposure mapping.
f :
Ω → Θ → Δ
Unit traits.
θ :
ι → Θ
def gdep reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference.Experiment
Pairwise dependency indicator: 0 when the exposure indicators of i and j for exposure d are uncorrelated, 1 otherwise.
def N reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference.Experiment
Population size.
Definition (Lean source)
def N : ℕ := card E.ι
theorem htMean_consistent_of_var reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Chebyshev consistency. Along a sequence of experiments with a sequence of treatment assignments d such that every unit's exposure probability under d is nonzero, if the design variance of the Horvitz–Thompson mean estimator tends to 0, then for any positive threshold ε, the estimator is consistent: Pr[|μ̂ − μ| ≥ ε] → 0.
Formal statement
hypotheses
Exp :
ℕ → Experiment
d :
∀ n, (Exp n).Δ
hpos :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (d n) ≠ 0
hvar :
ε :
ℝ
hε :
0 < ε
Proof (Lean source)
theorem htMean_consistent_of_var (Exp : ℕ → Experiment) (d : ∀ n, (Exp n).Δ)
(hpos : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (d n) ≠ 0)
(hvar : Tendsto (fun n => (Exp n).D.Var (htMean (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (d n)))
atTop (𝓝 0)) {ε : ℝ} (hε : 0 < ε) :
Tendsto (fun n => (Exp n).D.Pr
(fun z => ε ≤ |htMean (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (d n) z
- muTrue (Exp n).y (d n)|))
atTop (𝓝 (0 : ℝ)) := by
have hε2 : (0 : ℝ) < ε ^ 2 := pow_pos hε 2
-- Upper bound: `Var_n / ε²`, which tends to `0` by Chebyshev + `hvar`.
refine squeeze_zero (g := fun n =>
(Exp n).D.Var (htMean (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (d n)) / ε ^ 2)
(fun n => ?_) (fun n => ?_) ?_
· -- `0 ≤ Pr_n`: a sum of nonnegative terms.
unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind
refine sum_nonneg (fun z _ => ?_)
exact mul_nonneg ((Exp n).D.p_nonneg z) (by positivity)
· -- `Pr_n ≤ Var_n / ε²` by Chebyshev, using unbiasedness to recenter.
have hcenter : muTrue (Exp n).y (d n)
= (Exp n).D.E (htMean (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (d n)) :=
(E_htMean (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (d n) (hpos n)).symm
rw [hcenter]
exact (Exp n).D.chebyshev (htMean (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (d n)) hε
· -- `Var_n / ε² → 0 / ε² = 0`.
have := hvar.div_const (ε ^ 2)
simpa using this
1 supporting declaration (lemmas, instances)
-
Var_htMean_letheorem — Variance bound. Under a uniform bound c on |y_i(d)/π_i(d)|, the variance of the HT mean estimator is O((N + ∑_{i,j} g_{ij})/N²).hypothesesconclusionE.D.Var (htMean E.D E.y E.f E.θ d)≤ c ^ 2 * ((E.N : ℝ) + ∑ i, ∑ j ∈ Finset.univ.erase i, E.gdep d i j) / (E.N : ℝ) ^ 2Proof (Lean source)
theorem Var_htMean_le (d : E.Δ) {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ i, |E.y i d / prop E.D E.f E.θ i d| ≤ c) : E.D.Var (htMean E.D E.y E.f E.θ d) ≤ c ^ 2 * ((E.N : ℝ) + ∑ i, ∑ j ∈ Finset.univ.erase i, E.gdep d i j) / (E.N : ℝ) ^ 2 := by classical -- Abbreviations. set w : E.ι → ℝ := fun i => E.y i d / prop E.D E.f E.θ i d with hw set Cov : E.ι → E.ι → ℝ := fun i j => E.D.Cov (expoInd E.f E.θ i d) (expoInd E.f E.θ j d) with hCov -- Covariance bound: `|Cov i j| ≤ 1` for all `i, j`. have hCovBound : ∀ i j, |Cov i j| ≤ 1 := by intro i j exact abs_Cov_le_one_of_mem_unit E.D _ _ (fun z => FiniteDesign.ind_nonneg _ z) (fun z => FiniteDesign.ind_le_one _ z) (fun z => FiniteDesign.ind_nonneg _ z) (fun z => FiniteDesign.ind_le_one _ z) -- Termwise bound: `|w i * w j * Cov i j| ≤ c ^ 2`. have hTerm : ∀ i j, |w i * w j * Cov i j| ≤ c ^ 2 := by intro i j rw [abs_mul, abs_mul] have h1 : |w i| * |w j| ≤ c * c := mul_le_mul (hbound i) (hbound j) (abs_nonneg _) hc calc |w i| * |w j| * |Cov i j| ≤ (c * c) * 1 := mul_le_mul h1 (hCovBound i j) (abs_nonneg _) (by positivity) _ = c ^ 2 := by ring -- Off-diagonal termwise bound: `w i * w j * Cov i j ≤ c ^ 2 * gdep d i j`. have hOff : ∀ i, ∀ j ∈ Finset.univ.erase i, w i * w j * Cov i j ≤ c ^ 2 * E.gdep d i j := by intro i j _ unfold Experiment.gdep by_cases hz : E.D.Cov (expoInd E.f E.θ i d) (expoInd E.f E.θ j d) = 0 · rw [if_pos hz, mul_zero] have : Cov i j = 0 := hz rw [this, mul_zero] · rw [if_neg hz, mul_one] exact le_trans (le_abs_self _) (hTerm i j) -- Diagonal termwise bound: `w i * w i * Cov i i ≤ c ^ 2`. have hDiag : ∀ i, w i * w i * Cov i i ≤ c ^ 2 := fun i => le_trans (le_abs_self _) (hTerm i i) -- Bound `Var (htTotal) ≤ c ^ 2 * (N + S)`. set S : ℝ := ∑ i, ∑ j ∈ Finset.univ.erase i, E.gdep d i j with hS have hTotal : E.D.Var (htTotal E.D E.y E.f E.θ d) ≤ c ^ 2 * ((E.N : ℝ) + S) := by rw [Var_htTotal_cov] -- Split each inner sum into the diagonal `j = i` plus the `erase i` remainder. have hsplit : (∑ i, ∑ j, w i * w j * Cov i j) = (∑ i, w i * w i * Cov i i) + ∑ i, ∑ j ∈ Finset.univ.erase i, w i * w j * Cov i j := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.add_sum_erase univ (fun j => w i * w j * Cov i j) (Finset.mem_univ i)] rw [hsplit] have hDiagSum : (∑ i, w i * w i * Cov i i) ≤ c ^ 2 * (E.N : ℝ) := by calc (∑ i, w i * w i * Cov i i) ≤ ∑ _i : E.ι, c ^ 2 := Finset.sum_le_sum (fun i _ => hDiag i) _ = c ^ 2 * (E.N : ℝ) := by rw [Finset.sum_const, nsmul_eq_mul, Experiment.N, Finset.card_univ, mul_comm] have hOffSum : (∑ i, ∑ j ∈ Finset.univ.erase i, w i * w j * Cov i j) ≤ c ^ 2 * S := by rw [hS, Finset.mul_sum] refine Finset.sum_le_sum (fun i _ => ?_) rw [Finset.mul_sum] exact Finset.sum_le_sum (fun j hj => hOff i j hj) rw [mul_add] exact add_le_add hDiagSum hOffSum -- Reduce the HT mean variance to the HT total variance. have hmean : htMean E.D E.y E.f E.θ d = fun z => (Fintype.card E.ι : ℝ)⁻¹ * htTotal E.D E.y E.f E.θ d z := by funext z; rw [htMean, div_eq_inv_mul] rw [hmean, FiniteDesign.Var_const_mul] -- Now: `(card)⁻¹ ^ 2 * Var(htTotal) ≤ c ^ 2 * (N + S) / N ^ 2`. have hNdef : (E.N : ℝ) = (Fintype.card E.ι : ℝ) := by rw [Experiment.N] rw [hNdef] by_cases hN0 : (Fintype.card E.ι : ℝ) = 0 · rw [hN0]; simp · have hpos2 : (0 : ℝ) ≤ ((Fintype.card E.ι : ℝ)⁻¹) ^ 2 := by positivity have hVarNonneg := mul_le_mul_of_nonneg_left hTotal hpos2 refine le_trans hVarNonneg ?_ rw [hNdef] at hTotal ⊢ -- `(card)⁻² * (c²(N+S)) = c²(N+S)/N²`. rw [div_eq_mul_inv, inv_pow] ring_nf rfl
SteinCLT 2 core · 0 supporting Asymptotic normality of the Horvitz–Thompson effect estimator under interference rests on a central limit theorem for locally dependent random fields, proved via Stein's method (Chen & Shao 2004, Thm 2.7). ★ LocalDependenceCLT
Local-dependence CLT interface (Aronow-Samii 2017, via Chen-Shao 2004)
Asymptotic normality of the Horvitz–Thompson effect estimator under interference rests on a
central limit theorem for locally dependent random fields, proved via Stein's method
(Chen & Shao 2004, Thm 2.7). The LocalDependenceCLT structure packages the exact convergence
statement consumed by the interval theorem, while SteinInstance.lean connects this interface to
the dependency-graph Stein CLT developed elsewhere in the library.
def studentizedEffect reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference.Experiment
The studentized HT effect statistic: centered at τ, scaled by the true standard error √Var[τ̂].
Definition (Lean source)
noncomputable def studentizedEffect (dk dl : E.Δ) (z : E.Ω) : ℝ :=
(htEffect E.D E.y E.f E.θ dk dl z - tauTrue E.y dk dl)
/ sqrt (E.D.Var (htEffect E.D E.y E.f E.θ dk dl))
structure LocalDependenceCLT reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Chen-Shao local-dependence CLT interface, bounded-neighborhood case. Along a sequence of experiments Exp with a chosen pair of exposure levels dk, dl at each sample size, this records that the design probability that the studentized Horvitz–Thompson effect statistic falls below any fixed threshold converges, as the sample size grows, to the standard normal CDF at that threshold.
Definition (Lean source)
parameters
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
fields
Convergence in distribution of the studentized statistic to `𝒩(0,1)`, via the CDF.
tendsto_cdf :
∀ t : ℝ,
Tendsto (fun n => (Exp n).D.Pr (fun z => (Exp n).studentizedEffect (dk n) (dl n) z ≤ t)) atTop (𝓝 (stdNormalCdf t))
SteinInstance 7 core · 2 supporting This file bridges the finite-design Horvitz-Thompson effect statistic to the measure-theoretic dependency-graph Stein CLT. ★ localDependenceCLT_of_stein★ wald_coverage_of_stein★ localDependenceCLT_of_conditions★ wald_coverage_of_conditions★ localDependenceCLT_of_paper_conditions
Discharging LocalDependenceCLT via the abstract Stein CLT
This file bridges the finite-design Horvitz-Thompson effect statistic to the measure-theoretic dependency-graph Stein CLT. The studentized effect statistic is written as a sum of per-unit summands
Xₙᵢ = (rawᵢ − E[rawᵢ]) / (N · σₙ), σₙ = √(Var[τ̂]),
where rawᵢ = 1(Dᵢ=dk)Yᵢ/πᵢ(dk) − 1(Dᵢ=dl)Yᵢ/πᵢ(dl) is unit i's contribution to N·τ̂.
Then ∑ᵢ Xₙᵢ = studentizedEffect, the summands are mean-zero with Var(∑Xₙᵢ)=1, and the
abstract dependency-graph CLT stein_cdf_clt yields P[studentizedEffect ≤ t] → Φ(t), i.e.
LocalDependenceCLT.
The main public results are localDependenceCLT_of_stein, which assumes the Stein negligibility
limits directly, localDependenceCLT_of_conditions, which derives those limits from a bounded
dependency graph and uniformly negligible summands, and localDependenceCLT_of_paper_conditions,
which packages the Aronow-Samii boundedness, positive-propensity, population-growth, and
variance-growth conditions. The corresponding wald_coverage_of_* theorems compose these CLT
discharges with the oracle Wald-coverage theorem.
def effRaw reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference.Experiment
This is one unit's inverse-propensity-weighted contribution to the unnormalized Horvitz-Thompson effect estimator.
def effSummand reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference.Experiment
This is the centered and standardized per-unit summand used to form the studentized Horvitz-Thompson effect statistic.
Definition (Lean source)
noncomputable def effSummand (dk dl : E.Δ) (i : E.ι) (z : E.Ω) : ℝ :=
(effRaw E dk dl i z - E.D.E (effRaw E dk dl i))
/ ((Fintype.card E.ι : ℝ) * sqrt (E.D.Var (htEffect E.D E.y E.f E.θ dk dl)))
theorem localDependenceCLT_of_stein reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Local-dependence CLT from the abstract Stein conditions. For a pair of treatment sequences dk, dl and a choice of dependency neighbourhoods N n i, suppose the design variance of the Horvitz–Thompson effect estimator is everywhere positive, every unit has nonzero exposure probability under dk and under dl, and the per-unit effect summands are pointwise bounded by a nonnegative sequence B n. If each summand is independent of the sum of summands outside its neighbourhood, and the two Stein negligibility limits hold — the design variance of the neighbourhood cross-term sum tends to 0 and the summed third-moment-type error term tends to 0 — then the studentized Horvitz–Thompson effect statistic converges in distribution to a standard normal.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
N :
∀ n
if
(Exp n).ι
then
Finset ((Exp n).ι)
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
hposk :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0
hposl :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0
B :
ℕ → ℝ
hB :
∀ n, 0 ≤ B n
hbound :
∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n
hindep :
∀ n i,
IndepFun ((Exp n).effSummand (dk n) (dl n) i) (fun z => ∑ j ∈ univ \ N n i, (Exp n).effSummand (dk n) (dl n) j z) (Exp n).D.toMeasure
herr1 :
Tendsto (fun n => (Exp n).D.Var (fun z => ∑ i, (Exp n).effSummand (dk n) (dl n) i z * ∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z)) atTop (𝓝 0)
herr2 :
Tendsto (fun n => ∑ i, (Exp n).D.E (fun z => |(Exp n).effSummand (dk n) (dl n) i z| * (∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z) ^ 2)) atTop (𝓝 0)
conclusion
LocalDependenceCLT Exp dk dl
Proof (Lean source)
theorem localDependenceCLT_of_stein (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(N : ∀ n, (Exp n).ι → Finset ((Exp n).ι))
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(hposk : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0)
(hposl : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0)
(B : ℕ → ℝ) (hB : ∀ n, 0 ≤ B n)
(hbound : ∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n)
(hindep : ∀ n i, IndepFun
((Exp n).effSummand (dk n) (dl n) i)
(fun z => ∑ j ∈ univ \ N n i, (Exp n).effSummand (dk n) (dl n) j z)
(Exp n).D.toMeasure)
(herr1 : Tendsto (fun n => (Exp n).D.Var
(fun z => ∑ i, (Exp n).effSummand (dk n) (dl n) i z
* ∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z)) atTop (𝓝 0))
(herr2 : Tendsto (fun n => ∑ i, (Exp n).D.E
(fun z => |(Exp n).effSummand (dk n) (dl n) i z|
* (∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z) ^ 2)) atTop (𝓝 0)) :
LocalDependenceCLT Exp dk dl := by
classical
-- Abbreviations matching `stein_cdf_clt`.
set μ : ∀ n, Measure (Exp n).Ω := fun n => (Exp n).D.toMeasure with hμ
set X : ∀ n, (Exp n).ι → (Exp n).Ω → ℝ :=
fun n i => (Exp n).effSummand (dk n) (dl n) i with hX
-- Each summand is measurable (the assignment space carries the top σ-algebra).
have hmeas : ∀ n i, Measurable (X n i) := fun n i => measurable_from_top
-- Mean-zero: `∫ Xₙᵢ ∂μₙ = D.E (effSummand) = 0`.
have hmean : ∀ n i, ∫ z, X n i z ∂(μ n) = 0 := by
intro n i
rw [hμ, hX, FiniteDesign.integral_toMeasure, Experiment.E_effSummand]
-- `depSum (Xₙ) = studentizedEffect`.
have hdep : ∀ n, SteinMethod.depSum (X n) = (Exp n).studentizedEffect (dk n) (dl n) :=
fun n => Experiment.depSum_effSummand _ _ _ (hposk n) (hposl n)
-- Unit total variance: `∫ (depSum Xₙ)² ∂μₙ = 1`.
have hvar : ∀ n, ∫ z, (SteinMethod.depSum (X n) z) ^ 2 ∂(μ n) = 1 := by
intro n
rw [hdep n, hμ, FiniteDesign.integral_toMeasure,
Experiment.E_studentizedEffect_sq _ _ _ (hVar n) (hposk n) (hposl n)]
-- The two Stein error limits, transported through the measure bridge.
have herr1' : Tendsto
(fun n => variance
(fun z => ∑ i, X n i z * SteinMethod.nbhdSum (X n) (N n) i z) (μ n)) atTop (𝓝 0) := by
refine herr1.congr (fun n => ?_)
rw [hμ, FiniteDesign.variance_toMeasure]
rfl
have herr2' : Tendsto
(fun n => ∑ i, ∫ z, |X n i z| * (SteinMethod.nbhdSum (X n) (N n) i z) ^ 2 ∂(μ n)) atTop
(𝓝 0) := by
refine herr2.congr (fun n => ?_)
refine Finset.sum_congr rfl (fun i _ => ?_)
rw [hμ, FiniteDesign.integral_toMeasure]
rfl
-- Assemble the abstract Stein CLT, evaluated at each threshold.
refine ⟨fun t => ?_⟩
have hclt := SteinMethod.stein_cdf_clt μ X N hmeas B hB hbound hmean hindep hvar
herr1' herr2' t
-- Rewrite the limit point: `Φ(t) = (gaussianReal 0 1).real (Iic t)` by definition.
rw [show stdNormalCdf t = (gaussianReal 0 1).real (Iic t) from rfl]
-- Match the prelimit sequences pointwise.
refine hclt.congr (fun n => ?_)
-- `D.Pr {studentized ≤ t} = (μₙ.map (depSum Xₙ)).real (Iic t)`.
have hWmeas : Measurable (SteinMethod.depSum (X n)) := by
rw [hdep n]; exact measurable_from_top
have hset : {z | (Exp n).studentizedEffect (dk n) (dl n) z ≤ t}
= (SteinMethod.depSum (X n)) ⁻¹' Iic t := by
rw [hdep n]; rfl
rw [hμ] at *
rw [← FiniteDesign.toMeasure_real_setOf, hset,
MeasureTheory.map_measureReal_apply hWmeas measurableSet_Iic]
theorem wald_coverage_of_stein reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Aronow–Samii oracle Wald coverage from primitive Stein-discharge conditions. For a pair of treatment sequences dk, dl and a choice of dependency neighbourhoods N n i, suppose the design variance of the Horvitz–Thompson effect estimator is everywhere positive, every unit has nonzero exposure probability under dk and under dl, and the per-unit effect summands are pointwise bounded by a nonnegative sequence B n. If each summand is independent of the sum of summands outside its neighbourhood and the two Stein negligibility limits hold — the design variance of the neighbourhood cross-term sum tends to 0 and the summed third-moment-type error term tends to 0 — and zq is a nonnegative quantile satisfying Φ(zq) = 1 − α/2, then the oracle Wald interval τ̂ ± zq·√Var[τ̂] attains asymptotic (liminf) coverage at least 1 − α.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
N :
∀ n
if
(Exp n).ι
then
Finset ((Exp n).ι)
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
hposk :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0
hposl :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0
B :
ℕ → ℝ
hB :
∀ n, 0 ≤ B n
hbound :
∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n
hindep :
∀ n i,
IndepFun ((Exp n).effSummand (dk n) (dl n) i) (fun z => ∑ j ∈ univ \ N n i, (Exp n).effSummand (dk n) (dl n) j z) (Exp n).D.toMeasure
herr1 :
Tendsto (fun n => (Exp n).D.Var (fun z => ∑ i, (Exp n).effSummand (dk n) (dl n) i z * ∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z)) atTop (𝓝 0)
herr2 :
Tendsto (fun n => ∑ i, (Exp n).D.E (fun z => |(Exp n).effSummand (dk n) (dl n) i z| * (∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z) ^ 2)) atTop (𝓝 0)
α :
ℝ
zq :
ℝ
hzq0 :
0 ≤ zq
hzq :
stdNormalCdf zq = 1 - α / 2
Proof (Lean source)
theorem wald_coverage_of_stein (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(N : ∀ n, (Exp n).ι → Finset ((Exp n).ι))
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(hposk : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0)
(hposl : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0)
(B : ℕ → ℝ) (hB : ∀ n, 0 ≤ B n)
(hbound : ∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n)
(hindep : ∀ n i, IndepFun
((Exp n).effSummand (dk n) (dl n) i)
(fun z => ∑ j ∈ univ \ N n i, (Exp n).effSummand (dk n) (dl n) j z)
(Exp n).D.toMeasure)
(herr1 : Tendsto (fun n => (Exp n).D.Var
(fun z => ∑ i, (Exp n).effSummand (dk n) (dl n) i z
* ∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z)) atTop (𝓝 0))
(herr2 : Tendsto (fun n => ∑ i, (Exp n).D.E
(fun z => |(Exp n).effSummand (dk n) (dl n) i z|
* (∑ j ∈ N n i, (Exp n).effSummand (dk n) (dl n) j z) ^ 2)) atTop (𝓝 0))
{α : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - α / 2) :
1 - α ≤ liminf
(fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * sqrt ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))))
atTop :=
wald_coverage Exp dk dl
(localDependenceCLT_of_stein Exp dk dl N hVar hposk hposl B hB hbound hindep
herr1 herr2)
hVar zq hzq0 hzq
theorem localDependenceCLT_of_conditions reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Local-dependence CLT from a bounded-degree dependency graph. For a pair of treatment sequences dk, dl, suppose the per-unit effect summands admit a dependency graph Dg whose neighbourhoods have cardinality at most m, the design variance of the Horvitz–Thompson effect estimator is everywhere positive, every unit has nonzero exposure probability under dk and under dl, and the summands are pointwise bounded by a nonnegative sequence B n with B n → 0 and population size times B n cubed tending to 0. Then the studentized Horvitz–Thompson effect statistic satisfies the local-dependence central limit theorem.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
Dg :
∀ n,
SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i) (Exp n).D.toMeasure
m :
ℕ
hdeg :
∀ n i, ((Dg n).nbhd i).card ≤ m
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
hposk :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0
hposl :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0
B :
ℕ → ℝ
hB :
∀ n, 0 ≤ B n
hbound :
∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n
conclusion
LocalDependenceCLT Exp dk dl
Proof (Lean source)
theorem localDependenceCLT_of_conditions (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(Dg : ∀ n, SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i)
(Exp n).D.toMeasure)
(m : ℕ) (hdeg : ∀ n i, ((Dg n).nbhd i).card ≤ m)
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(hposk : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0)
(hposl : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0)
(B : ℕ → ℝ) (hB : ∀ n, 0 ≤ B n)
(hbound : ∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n)
(hB0 : Tendsto B atTop (𝓝 0))
(hNB3 : Tendsto (fun n => (card (Exp n).ι : ℝ) * (B n) ^ 3) atTop (𝓝 0)) :
LocalDependenceCLT Exp dk dl := by
classical
-- Abbreviations matching `stein_cdf_clt_of_depGraph`.
set μ : ∀ n, Measure (Exp n).Ω := fun n => (Exp n).D.toMeasure with hμ
set X : ∀ n, (Exp n).ι → (Exp n).Ω → ℝ :=
fun n i => (Exp n).effSummand (dk n) (dl n) i with hX
-- Each summand is measurable (the assignment space carries the top σ-algebra).
have hmeas : ∀ n i, Measurable (X n i) := fun n i => measurable_from_top
-- Mean-zero: `∫ Xₙᵢ ∂μₙ = D.E (effSummand) = 0`.
have hmean : ∀ n i, ∫ z, X n i z ∂(μ n) = 0 := by
intro n i
rw [hμ, hX, FiniteDesign.integral_toMeasure, Experiment.E_effSummand]
-- `depSum (Xₙ) = studentizedEffect`.
have hdep : ∀ n, SteinMethod.depSum (X n) = (Exp n).studentizedEffect (dk n) (dl n) :=
fun n => Experiment.depSum_effSummand _ _ _ (hposk n) (hposl n)
-- Unit total variance: `∫ (depSum Xₙ)² ∂μₙ = 1`.
have hvar : ∀ n, ∫ z, (SteinMethod.depSum (X n) z) ^ 2 ∂(μ n) = 1 := by
intro n
rw [hdep n, hμ, FiniteDesign.integral_toMeasure,
Experiment.E_studentizedEffect_sq _ _ _ (hVar n) (hposk n) (hposl n)]
-- Assemble the dependency-graph Stein CLT (negligibility derived internally), at each threshold.
refine ⟨fun t => ?_⟩
have hclt := SteinMethod.stein_cdf_clt_of_depGraph μ X Dg m hdeg B hB hbound hB0 hNB3
hmean hvar t
-- Rewrite the limit point: `Φ(t) = (gaussianReal 0 1).real (Iic t)` by definition.
rw [show stdNormalCdf t = (gaussianReal 0 1).real (Iic t) from rfl]
-- Match the prelimit sequences pointwise.
refine hclt.congr (fun n => ?_)
-- `D.Pr {studentized ≤ t} = (μₙ.map (depSum Xₙ)).real (Iic t)`.
have hWmeas : Measurable (SteinMethod.depSum (X n)) := by
rw [hdep n]; exact measurable_from_top
have hset : {z | (Exp n).studentizedEffect (dk n) (dl n) z ≤ t}
= (SteinMethod.depSum (X n)) ⁻¹' Iic t := by
rw [hdep n]; rfl
rw [hμ] at *
rw [← FiniteDesign.toMeasure_real_setOf, hset,
MeasureTheory.map_measureReal_apply hWmeas measurableSet_Iic]
theorem wald_coverage_of_conditions reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Aronow–Samii oracle Wald coverage from bounded-degree primitive conditions. For a pair of treatment sequences dk, dl, suppose the per-unit effect summands admit a dependency graph Dg whose neighbourhoods have cardinality at most m, the design variance of the Horvitz–Thompson effect estimator is everywhere positive, and every unit has nonzero exposure probability under dk and under dl. If the summands are pointwise bounded by a nonnegative sequence B n with B n → 0 and population size times B n cubed tending to 0, and zq is a nonnegative quantile satisfying Φ(zq) = 1 − α/2, then the oracle Wald interval τ̂ ± zq·√Var[τ̂] attains asymptotic (liminf) coverage at least 1 − α.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
Dg :
∀ n,
SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i) (Exp n).D.toMeasure
m :
ℕ
hdeg :
∀ n i, ((Dg n).nbhd i).card ≤ m
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
hposk :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0
hposl :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0
B :
ℕ → ℝ
hB :
∀ n, 0 ≤ B n
hbound :
∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n
α :
ℝ
zq :
ℝ
hzq0 :
0 ≤ zq
hzq :
stdNormalCdf zq = 1 - α / 2
Proof (Lean source)
theorem wald_coverage_of_conditions (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(Dg : ∀ n, SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i)
(Exp n).D.toMeasure)
(m : ℕ) (hdeg : ∀ n i, ((Dg n).nbhd i).card ≤ m)
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(hposk : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0)
(hposl : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0)
(B : ℕ → ℝ) (hB : ∀ n, 0 ≤ B n)
(hbound : ∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n)
(hB0 : Tendsto B atTop (𝓝 0))
(hNB3 : Tendsto (fun n => (card (Exp n).ι : ℝ) * (B n) ^ 3) atTop (𝓝 0))
{α : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - α / 2) :
1 - α ≤ liminf
(fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * sqrt ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))))
atTop :=
wald_coverage Exp dk dl
(localDependenceCLT_of_conditions Exp dk dl Dg m hdeg hVar hposk hposl B hB hbound hB0 hNB3)
hVar zq hzq0 hzq
theorem localDependenceCLT_of_paper_conditions reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Local-dependence CLT from the literal Aronow–Samii conditions. For a pair of treatment sequences dk, dl, suppose the per-unit effect summands admit a bounded-degree dependency graph Dg, potential outcomes under dk and under dl are uniformly bounded by a constant c1, and the exposure propensities under dk and under dl are bounded away from 0 by a positive constant c2. If the population size diverges, the design variance of the Horvitz–Thompson effect estimator is everywhere positive, and population size times that variance converges to a positive limit cVar, then the studentized Horvitz–Thompson effect statistic satisfies the local-dependence central limit theorem.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
Dg :
∀ n,
SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i) (Exp n).D.toMeasure
m :
ℕ
hdeg :
∀ n i, ((Dg n).nbhd i).card ≤ m
c1 :
ℝ
hyk :
∀ n i, |(Exp n).y i (dk n)| ≤ c1
hyl :
∀ n i, |(Exp n).y i (dl n)| ≤ c1
c2 :
ℝ
hc2 :
0 < c2
hπk :
∀ n i, 1 / c2 ≤ prop (Exp n).D (Exp n).f (Exp n).θ i (dk n)
hπl :
∀ n i, 1 / c2 ≤ prop (Exp n).D (Exp n).f (Exp n).θ i (dl n)
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
cVar :
ℝ
hcVar :
0 < cVar
conclusion
LocalDependenceCLT Exp dk dl
Proof (Lean source)
theorem localDependenceCLT_of_paper_conditions (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(Dg : ∀ n, SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i)
(Exp n).D.toMeasure)
(m : ℕ) (hdeg : ∀ n i, ((Dg n).nbhd i).card ≤ m)
(c1 : ℝ) (hyk : ∀ n i, |(Exp n).y i (dk n)| ≤ c1) (hyl : ∀ n i, |(Exp n).y i (dl n)| ≤ c1)
(c2 : ℝ) (hc2 : 0 < c2)
(hπk : ∀ n i, 1 / c2 ≤ prop (Exp n).D (Exp n).f (Exp n).θ i (dk n))
(hπl : ∀ n i, 1 / c2 ≤ prop (Exp n).D (Exp n).f (Exp n).θ i (dl n))
(hN : Tendsto (fun n => (card (Exp n).ι : ℝ)) atTop atTop)
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(cVar : ℝ) (hcVar : 0 < cVar)
(hCond4 : Tendsto (fun n => (card (Exp n).ι : ℝ)
* (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
atTop (𝓝 cVar)) :
LocalDependenceCLT Exp dk dl := by
classical
-- Abbreviations.
set card : ℕ → ℝ := fun n => (card (Exp n).ι : ℝ) with hcard
set Var : ℕ → ℝ := fun n =>
(Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) with hVardef
set σ : ℕ → ℝ := fun n => sqrt (Var n) with hσdef
set B : ℕ → ℝ := fun n => 4 * c1 * c2 / (card n * σ n) with hBdef
-- Basic positivity facts.
have hcard_nonneg : ∀ n, 0 ≤ card n := fun n => by positivity
have hσ_nonneg : ∀ n, 0 ≤ σ n := fun n => Real.sqrt_nonneg _
have hden_nonneg : ∀ n, 0 ≤ card n * σ n := fun n => mul_nonneg (hcard_nonneg n) (hσ_nonneg n)
-- `0 ≤ c1` whenever the population is nonempty (an outcome witness exists).
have hc1_of : ∀ n (i : (Exp n).ι), 0 ≤ c1 := fun n i => le_trans (abs_nonneg _) (hyk n i)
-- `hposk`/`hposl`: positive propensities ⇒ nonzero.
have hposk : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0 := by
intro n i
exact ne_of_gt (lt_of_lt_of_le (by positivity) (hπk n i))
have hposl : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0 := by
intro n i
exact ne_of_gt (lt_of_lt_of_le (by positivity) (hπl n i))
-- `hB`: `0 ≤ B n`. Nonempty population gives `c1 ≥ 0`; empty gives `card n = 0` so `B n = 0`.
have hB : ∀ n, 0 ≤ B n := by
intro n
rcases isEmpty_or_nonempty (Exp n).ι with he | hne
· have hc0 : card n = 0 := by
rw [hcard]; simp [Fintype.card_eq_zero]
simp [hBdef, hc0]
· obtain ⟨i⟩ := hne
exact div_nonneg (by have := hc1_of n i; positivity) (hden_nonneg n)
-- `hbound`: each centered standardized summand is bounded by `B n`.
have hbound : ∀ n i z, |(Exp n).effSummand (dk n) (dl n) i z| ≤ B n := by
intro n i z
have hraw : ∀ z', |(Exp n).effRaw (dk n) (dl n) i z'| ≤ 2 * c1 * c2 := fun z' =>
abs_effRaw_le (Exp n) (dk n) (dl n) i z' c1 (hyk n i) (hyl n i) c2 hc2 (hπk n i) (hπl n i)
have hEraw : |(Exp n).D.E ((Exp n).effRaw (dk n) (dl n) i)| ≤ 2 * c1 * c2 :=
abs_E_le (Exp n).D hraw
have hnum : |(Exp n).effRaw (dk n) (dl n) i z
- (Exp n).D.E ((Exp n).effRaw (dk n) (dl n) i)| ≤ 4 * c1 * c2 := by
calc |(Exp n).effRaw (dk n) (dl n) i z
- (Exp n).D.E ((Exp n).effRaw (dk n) (dl n) i)|
≤ |(Exp n).effRaw (dk n) (dl n) i z|
+ |(Exp n).D.E ((Exp n).effRaw (dk n) (dl n) i)| := abs_sub _ _
_ ≤ 2 * c1 * c2 + 2 * c1 * c2 := add_le_add (hraw z) hEraw
_ = 4 * c1 * c2 := by ring
change |((Exp n).effRaw (dk n) (dl n) i z - (Exp n).D.E ((Exp n).effRaw (dk n) (dl n) i))
/ (card n * σ n)| ≤ 4 * c1 * c2 / (card n * σ n)
rw [abs_div, abs_of_nonneg (hden_nonneg n)]
gcongr
-- `card n * σ n = √(card n ^ 2 * Var n)`: the denominator as one square root.
have hdenom_sqrt : ∀ n, card n * σ n = sqrt (card n ^ 2 * Var n) := by
intro n
rw [hσdef, Real.sqrt_mul (by positivity), Real.sqrt_sq (hcard_nonneg n)]
-- `card n ^ 2 * Var n → atTop` (from `card → ∞` and `card·Var → cVar > 0`).
have hcard2Var : Tendsto (fun n => card n ^ 2 * Var n) atTop atTop := by
have heq : (fun n => card n ^ 2 * Var n) = fun n => card n * (card n * Var n) := by
funext n; ring
rw [heq]
exact hN.atTop_mul_pos hcVar hCond4
-- `card n * σ n → atTop`.
have hdenom_atTop : Tendsto (fun n => card n * σ n) atTop atTop := by
have : (fun n => card n * σ n) = fun n => sqrt (card n ^ 2 * Var n) := funext hdenom_sqrt
rw [this]
exact Real.tendsto_sqrt_atTop.comp hcard2Var
-- `hB0`: `B → 0`.
have hB0 : Tendsto B atTop (𝓝 0) := hdenom_atTop.const_div_atTop (4 * c1 * c2)
-- `card n * B n ^ 3 = (4 c1 c2)^3 / (card n ^ 2 * σ n ^ 3)`.
have hNB3eq : ∀ n, card n * B n ^ 3
= (4 * c1 * c2) ^ 3 / (card n ^ 2 * σ n ^ 3) := by
intro n
by_cases hd : card n * σ n = 0
· -- degenerate: `card = 0` or `σ = 0`, both sides vanish.
rcases mul_eq_zero.mp hd with hc0 | hs0
· simp [hBdef, hc0]
· simp [hBdef, hs0]
· rw [hBdef]
field_simp
-- `card n ^ 2 * σ n ^ 3 = (√(card n * Var n)) ^ 3 * √(card n)`.
have hpow_sqrt : ∀ n, card n ^ 2 * σ n ^ 3
= (sqrt (card n * Var n)) ^ 3 * sqrt (card n) := by
intro n
rw [hσdef]
rw [Real.sqrt_mul (hcard_nonneg n)]
have hcs : sqrt (card n) ^ 2 = card n := Real.sq_sqrt (hcard_nonneg n)
rw [mul_pow]
ring_nf
rw [show sqrt (card n) ^ 4 = (sqrt (card n) ^ 2) ^ 2 by ring, hcs]
ring
-- `card n ^ 2 * σ n ^ 3 → atTop`.
have hpow_atTop : Tendsto (fun n => card n ^ 2 * σ n ^ 3) atTop atTop := by
have heq : (fun n => card n ^ 2 * σ n ^ 3)
= fun n => (sqrt (card n * Var n)) ^ 3 * sqrt (card n) := funext hpow_sqrt
rw [heq]
have hsqrtcardVar : Tendsto (fun n => sqrt (card n * Var n)) atTop
(𝓝 (sqrt cVar)) := (Real.continuous_sqrt.tendsto cVar).comp hCond4
have hcube : Tendsto (fun n => (sqrt (card n * Var n)) ^ 3) atTop
(𝓝 ((sqrt cVar) ^ 3)) := hsqrtcardVar.pow 3
have hcubepos : 0 < (sqrt cVar) ^ 3 := by positivity
have hsqrtcard : Tendsto (fun n => sqrt (card n)) atTop atTop :=
Real.tendsto_sqrt_atTop.comp hN
exact hcube.pos_mul_atTop hcubepos hsqrtcard
-- `hNB3`: `card · B³ → 0`.
have hNB3 : Tendsto (fun n => card n * B n ^ 3) atTop (𝓝 0) := by
have heq : (fun n => card n * B n ^ 3)
= fun n => (4 * c1 * c2) ^ 3 / (card n ^ 2 * σ n ^ 3) := funext hNB3eq
rw [heq]
exact hpow_atTop.const_div_atTop ((4 * c1 * c2) ^ 3)
-- Assemble.
exact localDependenceCLT_of_conditions Exp dk dl Dg m hdeg hVar hposk hposl B hB hbound hB0 hNB3
2 supporting declarations (lemmas, instances)
-
instMeasurableSpaceΩinstance — Equip a finite assignment space with the top σ-algebra (every set measurable), so the design measure and the measure-theoretic CLT machinery apply with no extra hypotheses. -
instMeasurableSingletonΩinstance — The top sigma-algebra on a finite assignment space makes every singleton measurable.instance instMeasurableSingletonΩ (E : Experiment) : MeasurableSingletonClass E.Ω := ⟨fun _ => trivial⟩
VarEstQuadBound 9 core · 3 supporting The feasible Wald-coverage theorem reduces, via relVar_of_NsqVar_tendsto, to Var[N·V̂] → 0. ★ var_htEdgeStat_le
Quadruple-sum variance bound for the conservative variance estimator (Aronow–Samii Prop 6.6)
The feasible Wald-coverage theorem reduces, via relVar_of_NsqVar_tendsto, to Var[N·V̂] → 0.
This file establishes the per-population core of that limit, the appendix quadruple-sum bound
Var[ V̂_raw ] ≤ 8·M²·m³·N, V̂_raw = ŷVar(dk) + ŷVar(dl) − 2·Ĉov,
where V̂ = N⁻²·V̂_raw (so Var[N·V̂] = N⁻²·Var[V̂_raw] ≤ 8M²m³/N). The estimator V̂_raw is
rewritten as a single edge-sum ∑_{i,j} vb i j over ordered pairs (diagonal i=j folds in
the three single-index sums; off-diagonal folds the three pairwise sums), and the abstract
var_edge_sum_le is applied with:
* boundedness |vb i j z| ≤ M from Condition 1 (bounded outcomes/inverse-propensities) plus
the explicit joint-overlap bound Condition 1' (1/π_{ij} ≤ c₃ on all ordered pairs — the
quantitative input the paper's appendix uses implicitly);
* off-edge vanishing vb i j = 0 for non-adjacent i ≠ j, since then the exposures are
independent and the centered-cross factors π_{ij} − π_iπ_j = Cov[1ᵢ,1ⱼ] vanish;
* edge-covariance vanishing Cov[vb i j, vb k l] = 0 for graph-unlinked edge pairs — the
Condition 3 (local dependence / dependency graph) input, in the form the appendix uses.
def diagVar reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Diagonal (variance) summand of ŷVar(d): 1ᵢ(d)·(1−πᵢ)·(Yᵢ/πᵢ)².
def offVar reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Off-diagonal (variance) summand of ŷVar(d).
Definition (Lean source)
noncomputable def offVar (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ)
(d : Δ) (i j : ι) (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))
def offCov reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Off-diagonal summand of the covariance estimator Ĉov.
Definition (Lean source)
noncomputable def offCov (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ)
(dk dl : Δ) (i j : ι) (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))
def diagCov reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Diagonal (Young) correction summand of Ĉov.
def vbDiag reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Diagonal edge term: diagVar(dk) + diagVar(dl) + 2·diagCov.
Definition (Lean source)
noncomputable def vbDiag (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ)
(dk dl : Δ) (i : ι) (z : Ω) : ℝ :=
diagVar D y f θ dk i z + diagVar D y f θ dl i z + 2 * diagCov D y f θ dk dl i z
def vbOff reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Off-diagonal edge term: offVar(dk) + offVar(dl) − 2·offCov.
Definition (Lean source)
noncomputable def vbOff (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ)
(dk dl : Δ) (i j : ι) (z : Ω) : ℝ :=
offVar D y f θ dk i j z + offVar D y f θ dl i j z - 2 * offCov D y f θ dk dl i j z
def vb reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
The edge-function for V̂_raw: diagonal term on i = j, off-diagonal term otherwise.
Definition (Lean source)
noncomputable def vb (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ)
(dk dl : Δ) (i j : ι) (z : Ω) : ℝ :=
if i = j then vbDiag D y f θ dk dl i z else vbOff D y f θ dk dl i j z
def vbBound reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Uniform pointwise bound on the edge-function, from Conditions 1 and 1'. Chosen large enough to dominate both the squared inverse-propensity terms (∝ c₂²) and the Young-correction terms (∝ c₂), uniformly in the joint-overlap constant c₃.
Definition (Lean source)
noncomputable def vbBound (c₁ c₂ c₃ : ℝ) : ℝ :=
4 * (1 + c₃) * c₁ ^ 2 * (c₂ ^ 2 + c₂)
theorem var_htEdgeStat_le reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Per-population quadruple-sum bound (Aronow–Samii appendix, Prop 6.6). Suppose the two treatment arms are distinct and outcomes are uniformly bounded by a nonnegative constant c₁ (Condition 1). Suppose the marginal exposure propensities under each arm are positive with inverses uniformly bounded by a nonnegative constant c₂, and the same-arm and cross-arm pairwise joint exposure propensities have inverses uniformly bounded by a nonnegative constant c₃ (Condition 1'). Suppose further a symmetric, reflexive dependency relation G of degree at most m makes every non-adjacent pair's joint exposure propensities factor as if independent and gives every quadruple with no adjacent index pair zero covariance between the variance-estimator kernel terms (Condition 3). Then the variance of the raw conservative variance estimator is linear in the population size: Var[ŷVar(dk)+ŷVar(dl)−2Ĉov] ≤ 8·(vbBound c₁ c₂ c₃)²·m³·N.
Formal statement
hypotheses
D :
y :
ι → Δ → ℝ
f :
Ω → Θ → Δ
θ :
ι → Θ
dk dl :
Δ
hne :
dk ≠ dl
c₁ c₂ c₃ :
ℝ
hc₁ :
0 ≤ c₁
hc₂ :
0 ≤ c₂
hc₃ :
0 ≤ c₃
hy :
∀ i d, |y i d| ≤ c₁
hπk :
∀ i, 0 < prop D f θ i dk
hπl :
∀ i, 0 < prop D f θ i dl
hπinvk :
∀ i, 1 / prop D f θ i dk ≤ c₂
hπinvl :
∀ i, 1 / prop D f θ i dl ≤ c₂
hjk :
∀ i j, 1 / propPairSame D f θ i j dk ≤ c₃
hjl :
∀ i j, 1 / propPairSame D f θ i j dl ≤ c₃
hjc :
∀ i j, 1 / propPairCross D f θ i j dk dl ≤ c₃
G :
ι → ι → Prop
hrefl :
∀ i, G i i
hsymm :
∀ i j
if
G i j
then
G j i
m :
ℕ
hdeg :
∀ i, (Finset.univ.filter (fun j => G i j)).card ≤ m
hGindep :
∀ i j
if
¬ G i j
then
Proof (Lean source)
theorem var_htEdgeStat_le (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ)
(dk dl : Δ) (hne : dk ≠ dl)
{c₁ c₂ c₃ : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hc₃ : 0 ≤ c₃)
(hy : ∀ i d, |y i d| ≤ c₁)
(hπk : ∀ i, 0 < prop D f θ i dk) (hπl : ∀ i, 0 < prop D f θ i dl)
(hπinvk : ∀ i, 1 / prop D f θ i dk ≤ c₂) (hπinvl : ∀ i, 1 / prop D f θ i dl ≤ c₂)
(hjk : ∀ i j, 1 / propPairSame D f θ i j dk ≤ c₃)
(hjl : ∀ i j, 1 / propPairSame D f θ i j dl ≤ c₃)
(hjc : ∀ i j, 1 / propPairCross D f θ i j dk dl ≤ c₃)
(G : ι → ι → Prop) [DecidableRel G] (hrefl : ∀ i, G i i) (hsymm : ∀ i j, G i j → G j i)
{m : ℕ} (hdeg : ∀ i, (Finset.univ.filter (fun j => G i j)).card ≤ m)
(hGindep : ∀ i j, ¬ G i j →
propPairSame D f θ i j dk = prop D f θ i dk * prop D f θ j dk ∧
propPairSame D f θ i j dl = prop D f θ i dl * prop D f θ j dl ∧
propPairCross D f θ i j dk dl = prop D f θ i dk * prop D f θ j dl)
(hcov0 : ∀ i j k l, ¬ (G i k ∨ G i l ∨ G j k ∨ G j l) →
D.Cov (vb D y f θ dk dl i j) (vb D y f θ dk dl k l) = 0) :
D.Var (fun z => htVarEst D y f θ dk z + htVarEst D y f θ dl z
- 2 * htCovEst D y f θ dk dl z)
≤ 8 * vbBound c₁ c₂ c₃ ^ 2 * ((m : ℝ) ^ 3 * (Fintype.card ι : ℝ)) := by
rw [htVarEst_add_sub_eq_edgeSum]
have hMnn : 0 ≤ vbBound c₁ c₂ c₃ := by
unfold vbBound
exact mul_nonneg (mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (sq_nonneg c₁))
(add_nonneg (sq_nonneg c₂) hc₂)
refine D.var_edge_sum_le (vb D y f θ dk dl) G hMnn ?_ hsymm hdeg ?_ hcov0
· exact fun i j _ z => abs_vb_le D y f θ dk dl hne hc₁ hc₂ hc₃ hy hπk hπl hπinvk hπinvl
hjk hjl hjc i j z
· intro i j hGij
rcases eq_or_ne i j with rfl | hij
· exact absurd (hrefl i) hGij
· obtain ⟨hsk, hsl, hc⟩ := hGindep i j hGij
exact vb_eq_zero_of_indep D y f θ dk dl i j hij hsk hsl hc
3 supporting declarations (lemmas, instances)
-
htVarEst_add_sub_eq_edgeSumtheorem — Edge-sum identity. V̂_raw = ∑_{i,j} vb i j: the three single-index sums of ŷVar(dk), ŷVar(dl), Ĉov fold into the diagonal i = j, and the three pairwise sums into the off-diagonal i ≠ j.hypothesesProof (Lean source)
theorem htVarEst_add_sub_eq_edgeSum (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (dk dl : Δ) : (fun z => htVarEst D y f θ dk z + htVarEst D y f θ dl z - 2 * htCovEst D y f θ dk dl z) = (fun z => ∑ i, ∑ j, vb D y f θ dk dl i j z) := by funext z -- Split each inner edge-sum into the diagonal term (`i = j`) plus the off-diagonal remainder. have hRHS : (∑ i, ∑ j, vb D y f θ dk dl i j z) = (∑ i, vbDiag D y f θ dk dl i z) + (∑ i, ∑ j ∈ Finset.univ.erase i, vbOff D y f θ dk dl i j z) := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [← Finset.add_sum_erase univ (fun j => vb D y f θ dk dl i j z) (mem_univ i)] congr 1 · rw [vb, if_pos rfl] · refine Finset.sum_congr rfl (fun j hj => ?_) rw [vb, if_neg ((Finset.mem_erase.mp hj).1).symm] rw [hRHS] unfold htVarEst htCovEst vbDiag vbOff diagVar offVar offCov diagCov simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.mul_sum] ring -
abs_vb_letheorem — Boundedness of the edge-function (Conditions 1 + 1'): |vb i j z| ≤ vbBound c₁ c₂ c₃.hypothesesD :y :ι → Δ → ℝf :Ω → Θ → Δθ :ι → Θdk dl :Δ_hne :dk ≠ dlc₁ c₂ c₃ :ℝ_hc₁ :0 ≤ c₁hc₂ :0 ≤ c₂hc₃ :0 ≤ c₃hy :∀ i d, |y i d| ≤ c₁hπk :∀ i, 0 < prop D f θ i dkhπl :∀ i, 0 < prop D f θ i dlhπinvk :∀ i, 1 / prop D f θ i dk ≤ c₂hπinvl :∀ i, 1 / prop D f θ i dl ≤ c₂hjk :∀ i j, 1 / propPairSame D f θ i j dk ≤ c₃hjl :∀ i j, 1 / propPairSame D f θ i j dl ≤ c₃hjc :∀ i j, 1 / propPairCross D f θ i j dk dl ≤ c₃i j :ιz :ΩProof (Lean source)
theorem abs_vb_le (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (dk dl : Δ) (_hne : dk ≠ dl) {c₁ c₂ c₃ : ℝ} (_hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hc₃ : 0 ≤ c₃) (hy : ∀ i d, |y i d| ≤ c₁) (hπk : ∀ i, 0 < prop D f θ i dk) (hπl : ∀ i, 0 < prop D f θ i dl) (hπinvk : ∀ i, 1 / prop D f θ i dk ≤ c₂) (hπinvl : ∀ i, 1 / prop D f θ i dl ≤ c₂) (hjk : ∀ i j, 1 / propPairSame D f θ i j dk ≤ c₃) (hjl : ∀ i j, 1 / propPairSame D f θ i j dl ≤ c₃) (hjc : ∀ i j, 1 / propPairCross D f θ i j dk dl ≤ c₃) (i j : ι) (z : Ω) : |vb D y f θ dk dl i j z| ≤ vbBound c₁ c₂ c₃ := by -- Marginal propensities are at most `1` (used to bound `1 - π` and `πᵢ·πⱼ`). have hπk1 : ∀ a, prop D f θ a dk ≤ 1 := fun a => (prop_mem_unit D f θ a dk).2 have hπl1 : ∀ a, prop D f θ a dl ≤ 1 := fun a => (prop_mem_unit D f θ a dl).2 unfold vb split_ifs with hij · -- Diagonal case `i = j`. unfold vbDiag have hbk := abs_diagVar_le D y f θ dk i z hy (hπk i) (hπk1 i) (hπinvk i) have hbl := abs_diagVar_le D y f θ dl i z hy (hπl i) (hπl1 i) (hπinvl i) have hbc := abs_diagCov_le D y f θ dk dl i z hy (hπk i) (hπl i) (hπinvk i) (hπinvl i) have htri : |diagVar D y f θ dk i z + diagVar D y f θ dl i z + 2 * diagCov D y f θ dk dl i z| ≤ |diagVar D y f θ dk i z| + |diagVar D y f θ dl i z| + 2 * |diagCov D y f θ dk dl i z| := by refine le_trans (abs_add_le _ _) ?_ gcongr · exact abs_add_le _ _ · rw [abs_mul]; simp refine le_trans htri ?_ -- `c₁²c₂² + c₁²c₂² + 2·(2c₁²c₂) = 2c₁²c₂² + 4c₁²c₂ ≤ vbBound`. have hsum : |diagVar D y f θ dk i z| + |diagVar D y f θ dl i z| + 2 * |diagCov D y f θ dk dl i z| ≤ c₁ ^ 2 * c₂ ^ 2 + c₁ ^ 2 * c₂ ^ 2 + 2 * (2 * c₁ ^ 2 * c₂) := by gcongr refine le_trans hsum ?_ unfold vbBound nlinarith [sq_nonneg c₁, hc₂, hc₃, mul_nonneg (sq_nonneg c₁) hc₂, mul_nonneg (mul_nonneg (sq_nonneg c₁) hc₂) hc₃, mul_nonneg (mul_nonneg (sq_nonneg c₁) hc₂) hc₂, mul_nonneg (mul_nonneg (mul_nonneg (sq_nonneg c₁) hc₂) hc₂) hc₃] · -- Off-diagonal case `i ≠ j`. unfold vbOff have hvk := abs_offVar_le D y f θ dk i j z hc₃ hy (hπk i) (hπk j) (hπk1 i) (hπk1 j) (hπinvk i) (hπinvk j) (hjk i j) have hvl := abs_offVar_le D y f θ dl i j z hc₃ hy (hπl i) (hπl j) (hπl1 i) (hπl1 j) (hπinvl i) (hπinvl j) (hjl i j) have hcv := abs_offCov_le D y f θ dk dl i j z hc₃ hy (hπk i) (hπl j) (hπk1 i) (hπl1 j) (hπinvk i) (hπinvl j) (hjc i j) have htri : |offVar D y f θ dk i j z + offVar D y f θ dl i j z - 2 * offCov D y f θ dk dl i j z| ≤ |offVar D y f θ dk i j z| + |offVar D y f θ dl i j z| + 2 * |offCov D y f θ dk dl i j z| := by refine le_trans (abs_sub _ _) ?_ gcongr · exact abs_add_le _ _ · rw [abs_mul]; simp refine le_trans htri ?_ have hsum : |offVar D y f θ dk i j z| + |offVar D y f θ dl i j z| + 2 * |offCov D y f θ dk dl i j z| ≤ (1 + c₃) * c₁ ^ 2 * c₂ ^ 2 + (1 + c₃) * c₁ ^ 2 * c₂ ^ 2 + 2 * ((1 + c₃) * c₁ ^ 2 * c₂ ^ 2) := by gcongr refine le_trans hsum ?_ unfold vbBound nlinarith [sq_nonneg c₁, hc₂, hc₃, mul_nonneg (sq_nonneg c₁) hc₂, mul_nonneg (mul_nonneg (sq_nonneg c₁) hc₂) hc₃, mul_nonneg (mul_nonneg (sq_nonneg c₁) (sq_nonneg c₂)) (by linarith : (0:ℝ) ≤ 1 + c₃)] -
vb_eq_zero_of_indeptheorem — Off-edge vanishing. If the same-exposure and cross-exposure pair propensities factor as products for an off-diagonal pair i ≠ j, then the centered-cross factors vanish and vb i j = 0; Condition 3 supplies these factorization hypotheses for non-adjacent pairs.hypothesesD :y :ι → Δ → ℝf :Ω → Θ → Δθ :ι → Θdk dl :Δi j :ιhij :i ≠ jhsame_k :hsame_l :hcross :conclusionvb D y f θ dk dl i j = fun _ => 0Proof (Lean source)
theorem vb_eq_zero_of_indep (D : FiniteDesign Ω) (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (dk dl : Δ) (i j : ι) (hij : i ≠ j) (hsame_k : propPairSame D f θ i j dk = prop D f θ i dk * prop D f θ j dk) (hsame_l : propPairSame D f θ i j dl = prop D f θ i dl * prop D f θ j dl) (hcross : propPairCross D f θ i j dk dl = prop D f θ i dk * prop D f θ j dl) : vb D y f θ dk dl i j = fun _ => 0 := by funext z rw [vb, if_neg hij, vbOff, offVar, offVar, offCov, hsame_k, hsame_l, hcross] ring
Intervals 2 core · 0 supporting Given the local-dependence CLT interface and a nonzero limiting variance (Condition 4), the Wald interval τ̂ ± z_{1−α/2}·√Var[τ̂] attains asymptotic coverage at least 1 − α (the paper's claim), formalized as 1 − α ≤ limi ★ wald_coverage★ wald_coverage_feasible
Asymptotic confidence intervals (Aronow–Samii 2017, Prop 6.5)
Given the local-dependence CLT interface and a nonzero limiting variance (Condition 4), the
Wald interval τ̂ ± z_{1−α/2}·√Var[τ̂] attains asymptotic coverage at least 1 − α
(the paper's claim), formalized as 1 − α ≤ liminf of the coverage probabilities.
The proof uses only the lower half of the CLT: the event |τ̂ − τ| ≤ z·√Var contains
{−z < W ≤ z} (with W the studentized statistic), whose probability is
Pr[W ≤ z] − Pr[W ≤ −z] → Φ(z) − Φ(−z) = 1 − α by the interface plus CDF symmetry
Φ(−z) = 1 − Φ(z). (The matching upper bound — exact convergence to 1 − α — would need
Gaussian-CDF continuity; the paper only claims "at least", so it is not pursued here.)
theorem wald_coverage reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Proposition 6.5 (asymptotic coverage, true standard error). For a pair of treatment sequences dk, dl, suppose the studentized Horvitz–Thompson effect statistic satisfies the local-dependence central limit theorem and the design variance of the effect estimator is everywhere positive — the operative form of Condition 4 (nonzero limiting variance). Then with zq a nonnegative quantile satisfying Φ(zq) = 1 − α/2, the Wald interval centered at the Horvitz–Thompson effect estimator, using its true standard error, attains asymptotic (liminf) coverage at least 1 − α.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
hclt :
LocalDependenceCLT Exp dk dl
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
α :
ℝ
zq :
ℝ
hzq0 :
0 ≤ zq
hzq :
stdNormalCdf zq = 1 - α / 2
Proof (Lean source)
theorem wald_coverage (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(hclt : LocalDependenceCLT Exp dk dl)
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
{α : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - α / 2) :
1 - α ≤ liminf
(fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * sqrt ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))))
atTop := by
-- The studentized lower-CDF probabilities at `zq` and `-zq`.
set S : ℕ → ℝ := fun n =>
(Exp n).D.Pr (fun z => (Exp n).studentizedEffect (dk n) (dl n) z ≤ zq) with hSdef
set Lo : ℕ → ℝ := fun n =>
(Exp n).D.Pr (fun z => (Exp n).studentizedEffect (dk n) (dl n) z ≤ -zq) with hLodef
set I : ℕ → ℝ := fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * sqrt ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))) with hIdef
-- (1) Limit of `S - Lo`.
have hS : Tendsto S atTop (𝓝 (stdNormalCdf zq)) := hclt.tendsto_cdf zq
have hLo : Tendsto Lo atTop (𝓝 (stdNormalCdf (-zq))) := hclt.tendsto_cdf (-zq)
have hlim : Tendsto (fun n => S n - Lo n) atTop (𝓝 (1 - α)) := by
have h := hS.sub hLo
rw [stdNormalCdf_neg zq, hzq] at h
have he : (1 - α / 2) - (1 - (1 - α / 2)) = 1 - α := by ring
rwa [he] at h
-- (2) Pointwise lower bound `S - Lo ≤ I`.
have hbound : ∀ n, S n - Lo n ≤ I n := by
intro n
-- Abbreviate the studentized statistic.
set W : (Exp n).Ω → ℝ := fun z => (Exp n).studentizedEffect (dk n) (dl n) z with hWdef
-- Split `S` by the event `W ≤ -zq`.
have hsplit := (Exp n).D.Pr_split (fun z => W z ≤ zq) (fun z => W z ≤ -zq)
-- The first piece equals `Lo`.
have hfirst : (Exp n).D.Pr (fun z => W z ≤ zq ∧ W z ≤ -zq) = Lo n := by
apply (Exp n).D.Pr_congr
intro z
constructor
· exact fun h => h.2
· intro h2
exact ⟨le_trans h2 (by linarith [hzq0]), h2⟩
-- So `S - Lo` is the probability of the second piece.
have hSLo : S n - Lo n =
(Exp n).D.Pr (fun z => W z ≤ zq ∧ ¬ W z ≤ -zq) := by
have : S n = (Exp n).D.Pr (fun z => W z ≤ zq ∧ W z ≤ -zq)
+ (Exp n).D.Pr (fun z => W z ≤ zq ∧ ¬ W z ≤ -zq) := hsplit
rw [this, hfirst]; ring
rw [hSLo]
-- That second piece is contained in `I`'s event.
apply (Exp n).D.Pr_mono
intro z hz
obtain ⟨hz1, hz2⟩ := hz
rw [not_le] at hz2
-- `|W z| ≤ zq`.
have habs : |W z| ≤ zq := abs_le.mpr ⟨le_of_lt hz2, hz1⟩
-- Unfold the studentized statistic.
set s : ℝ := sqrt ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) with hsdef
have hs : 0 < s := Real.sqrt_pos.mpr (hVar n)
rw [hWdef] at habs
simp only [Experiment.studentizedEffect] at habs
rw [← hsdef] at habs
rw [abs_div, abs_of_pos hs, div_le_iff₀ hs] at habs
exact habs
-- (3) Conclude with liminf.
have hbdd : IsBoundedUnder (· ≥ ·) atTop (fun n => S n - Lo n) :=
hlim.isBoundedUnder_ge
have hcobdd : IsCoboundedUnder (· ≥ ·) atTop I :=
isCoboundedUnder_ge_of_le atTop (x := (1 : ℝ))
(fun n => (Exp n).D.Pr_le_one _)
calc 1 - α = liminf (fun n => S n - Lo n) atTop := hlim.liminf_eq.symm
_ ≤ liminf I atTop :=
Filter.liminf_le_liminf (Filter.Eventually.of_forall hbound) hbdd hcobdd
theorem wald_coverage_feasible reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Proposition 6.5 (asymptotic coverage, feasible/estimated standard error — the paper's actual interval). For a pair of treatment sequences dk, dl, suppose the studentized effect statistic satisfies the local-dependence central limit theorem, the design variance of the effect estimator is everywhere positive, and the conservative variance estimator V̂ undershoots the true variance only with vanishing probability. Then with zq a nonnegative quantile satisfying Φ(zq) = 1 − α/2, the Wald interval τ̂ ± zq·√(V̂[τ̂]), using the estimated variance htEffectVarEst exactly as in Aronow–Samii Prop 6.5, attains asymptotic (liminf) coverage at least 1 − α.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
hclt :
LocalDependenceCLT Exp dk dl
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
hVhat :
∀ ε : ℝ
if
0 < ε
then
Tendsto (fun n => (Exp n).D.Pr (fun z => htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z < (1 - ε) * (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))) atTop (𝓝 0)
α :
ℝ
zq :
ℝ
hzq0 :
0 ≤ zq
hzq :
stdNormalCdf zq = 1 - α / 2
Proof (Lean source)
theorem wald_coverage_feasible (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(hclt : LocalDependenceCLT Exp dk dl)
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(hVhat : ∀ ε : ℝ, 0 < ε → Tendsto (fun n => (Exp n).D.Pr (fun z =>
htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
< (1 - ε) * (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))))
atTop (𝓝 0))
{α : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - α / 2) :
1 - α ≤ liminf
(fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * Real.sqrt
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z)))
atTop := by
-- The coverage probability sequence.
set I : ℕ → ℝ := fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * Real.sqrt
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z)) with hIdef
-- `I` is coboundedly below (always ≤ 1).
have hIcobdd : IsCoboundedUnder (· ≥ ·) atTop I :=
isCoboundedUnder_ge_of_le atTop (x := (1 : ℝ)) (fun n => (Exp n).D.Pr_le_one _)
have hIbdd : IsBoundedUnder (· ≤ ·) atTop I :=
isBoundedUnder_of ⟨1, fun n => (Exp n).D.Pr_le_one _⟩
-- For each `ε ∈ (0,1)`, `liminf I ≥ 2·Φ(zq·√(1-ε)) - 1`.
have key : ∀ ε : ℝ, 0 < ε → ε < 1 →
2 * stdNormalCdf (zq * Real.sqrt (1 - ε)) - 1 ≤ liminf I atTop := by
intro ε hε0 hε1
set c : ℝ := zq * Real.sqrt (1 - ε) with hcdef
have h1mε : (0 : ℝ) < 1 - ε := by linarith
have hc0 : 0 ≤ c := mul_nonneg hzq0 (Real.sqrt_nonneg _)
-- The CLT interval probability and the "bad variance" probability.
set B : ℕ → ℝ := fun n => (Exp n).D.Pr (fun z =>
-c ≤ (Exp n).studentizedEffect (dk n) (dl n) z ∧
(Exp n).studentizedEffect (dk n) (dl n) z ≤ c) with hBdef
set A : ℕ → ℝ := fun n => (Exp n).D.Pr (fun z =>
htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
< (1 - ε) * (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) with hAdef
have hA0 : Tendsto A atTop (𝓝 0) := hVhat ε hε0
-- STEP 2: pointwise `B n - A n ≤ I n`.
have hstep2 : ∀ n, B n - A n ≤ I n := by
intro n
set Vr : ℝ := (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) with hVrdef
set σ : ℝ := Real.sqrt Vr with hσdef
have hσpos : 0 < σ := Real.sqrt_pos.mpr (hVar n)
have hσ2 : σ ^ 2 = Vr := Real.sq_sqrt (hVar n).le
set W : (Exp n).Ω → ℝ := fun z => (Exp n).studentizedEffect (dk n) (dl n) z with hWdef
-- Split `B` by the bad-variance event.
set Abad : (Exp n).Ω → Prop := fun z =>
htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z < (1 - ε) * Vr
with hAbaddef
set Bev : (Exp n).Ω → Prop := fun z => -c ≤ W z ∧ W z ≤ c with hBevdef
have hsplit := (Exp n).D.Pr_split Bev Abad
-- `Pr(Bev ∧ Abad) ≤ A n`.
have hBA : (Exp n).D.Pr (fun z => Bev z ∧ Abad z) ≤ A n := by
apply (Exp n).D.Pr_mono; intro z hz; exact hz.2
-- So `B n - A n ≤ Pr(Bev ∧ ¬Abad)`.
have hBmA : B n - A n ≤ (Exp n).D.Pr (fun z => Bev z ∧ ¬ Abad z) := by
have hBeq : B n = (Exp n).D.Pr (fun z => Bev z ∧ Abad z)
+ (Exp n).D.Pr (fun z => Bev z ∧ ¬ Abad z) := hsplit
linarith [hBeq, hBA]
refine le_trans hBmA ?_
-- `Pr(Bev ∧ ¬Abad) ≤ I n` by event inclusion.
apply (Exp n).D.Pr_mono
intro z hz
obtain ⟨⟨hzlo, hzhi⟩, hznotbad⟩ := hz
rw [hAbaddef, not_lt] at hznotbad
-- `|W z| ≤ c`.
have habsW : |W z| ≤ c := abs_le.mpr ⟨hzlo, hzhi⟩
-- `htEffect - tauTrue = W z * σ`.
have hWσ : htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n) = W z * σ := by
rw [hWdef]
simp only [Experiment.studentizedEffect]
rw [← hVrdef, ← hσdef]
field_simp
rw [hWσ, abs_mul, abs_of_pos hσpos]
-- `|W z| * σ ≤ c * σ = zq * √((1-ε)*Vr) ≤ zq * √(V̂)`.
calc |W z| * σ ≤ c * σ := by
apply mul_le_mul_of_nonneg_right habsW hσpos.le
_ = zq * Real.sqrt ((1 - ε) * Vr) := by
rw [hcdef, hσdef, mul_assoc, ← Real.sqrt_mul h1mε.le]
_ ≤ zq * Real.sqrt
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z) := by
apply mul_le_mul_of_nonneg_left _ hzq0
exact Real.sqrt_le_sqrt hznotbad
-- STEP 3: liminf chain.
-- `liminf B ≤ liminf (B - A)` since `A → 0`.
have hBAliminf : liminf B atTop ≤ liminf (fun n => B n - A n) atTop := by
have hnegA : Tendsto (fun n => -A n) atTop (𝓝 0) := by
simpa using hA0.neg
have hBbdd_ge : IsBoundedUnder (· ≥ ·) atTop B :=
isBoundedUnder_of ⟨0, fun n => (Exp n).D.Pr_nonneg _⟩
have hBbdd_le : IsBoundedUnder (· ≤ ·) atTop B :=
isBoundedUnder_of ⟨1, fun n => (Exp n).D.Pr_le_one _⟩
have hnegAbdd_ge : IsBoundedUnder (· ≥ ·) atTop (fun n => -A n) :=
hnegA.isBoundedUnder_ge
have hnegAcobdd : IsCoboundedUnder (· ≥ ·) atTop (fun n => -A n) :=
hnegA.isBoundedUnder_le.isCoboundedUnder_ge
have h := le_liminf_add (u := B) (v := fun n => -A n)
hBbdd_ge hBbdd_le hnegAbdd_ge hnegAcobdd
rw [hnegA.liminf_eq] at h
simp only [add_zero] at h
have hsub : (B + fun n => -A n) = fun n => B n - A n := by
funext n; simp [sub_eq_add_neg]
rwa [hsub] at h
-- `liminf (B - A) ≤ liminf I` by pointwise bound.
have hABI : liminf (fun n => B n - A n) atTop ≤ liminf I atTop := by
have hBAbelow : IsBoundedUnder (· ≥ ·) atTop (fun n => B n - A n) := by
refine isBoundedUnder_of ⟨-1, fun n => ?_⟩
have hBn : 0 ≤ B n := by rw [hBdef]; exact (Exp n).D.Pr_nonneg _
have hAn : A n ≤ 1 := by rw [hAdef]; exact (Exp n).D.Pr_le_one _
change (-1 : ℝ) ≤ B n - A n
linarith
exact Filter.liminf_le_liminf (Filter.Eventually.of_forall hstep2) hBAbelow hIcobdd
-- STEP 1 gives `Φ(c) - Φ(-c) ≤ liminf B`.
have hstep1 := clt_interval_liminf_lb Exp dk dl hclt c hc0
-- Chain and rewrite `Φ(c) - Φ(-c) = 2·Φ(c) - 1`.
have hΦ : stdNormalCdf c - stdNormalCdf (-c) = 2 * stdNormalCdf c - 1 := by
rw [stdNormalCdf_neg c]; ring
calc 2 * stdNormalCdf (zq * Real.sqrt (1 - ε)) - 1
= stdNormalCdf c - stdNormalCdf (-c) := by rw [hcdef, hΦ]
_ ≤ liminf B atTop := hstep1
_ ≤ liminf (fun n => B n - A n) atTop := hBAliminf
_ ≤ liminf I atTop := hABI
-- STEP 4: let `ε → 0⁺` along `ε = 1/(k+1)`.
-- The RHS bound tends to `1 - α`.
set g : ℝ → ℝ := fun ε => 2 * stdNormalCdf (zq * Real.sqrt (1 - ε)) - 1 with hgdef
have hgcont : Tendsto g (𝓝 0) (𝓝 (1 - α)) := by
have hsqrt : Tendsto (fun ε : ℝ => Real.sqrt (1 - ε)) (𝓝 0) (𝓝 1) := by
have : Tendsto (fun ε : ℝ => (1 - ε)) (𝓝 0) (𝓝 (1 - 0)) :=
(tendsto_const_nhds.sub tendsto_id)
rw [sub_zero] at this
have hc := (Real.continuous_sqrt.tendsto (1 : ℝ)).comp this
rw [Real.sqrt_one] at hc
exact hc
have hzqsqrt : Tendsto (fun ε : ℝ => zq * Real.sqrt (1 - ε)) (𝓝 0) (𝓝 zq) := by
have := tendsto_const_nhds (x := zq) |>.mul hsqrt
simpa using this
have hΦc : Tendsto (fun ε : ℝ => stdNormalCdf (zq * Real.sqrt (1 - ε))) (𝓝 0)
(𝓝 (stdNormalCdf zq)) :=
(continuous_stdNormalCdf.tendsto zq).comp hzqsqrt
have : Tendsto g (𝓝 0) (𝓝 (2 * stdNormalCdf zq - 1)) := by
rw [hgdef]
exact (tendsto_const_nhds.mul hΦc).sub tendsto_const_nhds
have heq : 2 * stdNormalCdf zq - 1 = 1 - α := by rw [hzq]; ring
rwa [heq] at this
-- Evaluate along `ε_k = 1/(k+1) → 0`, eventually in `(0,1)`.
have hseq : Tendsto (fun k : ℕ => (1 : ℝ) / (k + 1)) atTop (𝓝 0) :=
tendsto_one_div_add_atTop_nhds_zero_nat
have hgseq : Tendsto (fun k : ℕ => g (1 / (k + 1))) atTop (𝓝 (1 - α)) :=
hgcont.comp hseq
-- `g (1/(k+1)) ≤ liminf I` eventually (for `k ≥ 1`, so `1/(k+1) ≤ 1/2 < 1`).
have hev : ∀ᶠ k : ℕ in atTop, g (1 / (k + 1)) ≤ liminf I atTop := by
rw [Filter.eventually_atTop]
refine ⟨1, fun k hk => ?_⟩
have hk1 : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
have hden : (0 : ℝ) < (k : ℝ) + 1 := by linarith
have hpos : (0 : ℝ) < 1 / (k + 1) := by positivity
have hlt1 : (1 : ℝ) / (k + 1) < 1 := by
rw [div_lt_one hden]; linarith
exact key _ hpos hlt1
exact le_of_tendsto hgseq hev
VarEstConsistencyConditions 2 core · 0 supporting Assembles the per-population quadruple-sum bound (var_htEdgeStat_le) into the asymptotic limit N²·Var[V̂_n] → 0 along a sequence of growing experiments, under uniform boundedness, single-propensity overlap, inverse joint ★ var_NsqVhat_tendsto_zero_of_conditions★ wald_coverage_feasible_of_conditions
Variance-estimator consistency from boundedness and dependency-graph conditions
Assembles the per-population quadruple-sum bound (var_htEdgeStat_le) into the asymptotic limit
N²·Var[V̂_n] → 0 along a sequence of growing experiments, under uniform boundedness,
single-propensity overlap, inverse joint-propensity bounds, and dependency-graph covariance
conditions. Combined with the Stein dependency-graph CLT discharge, the Chebyshev reduction
(relVar_of_NsqVar_tendsto), and the feasible-coverage capstone
(wald_coverage_feasible_of_relVar), this proves feasible Wald coverage from primitive
boundedness, overlap, dependency-graph, and variance-growth conditions.
N²·Var[V̂_n] = N⁻²·Var[V̂_raw,n] ≤ N⁻²·(8·M²·m³·N) = 8·M²·m³/N → 0 as N → ∞.
theorem var_NsqVhat_tendsto_zero_of_conditions reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Scaled variance-estimator variance vanishes (Aronow–Samii Prop 6.6 core). Along a sequence of experiments with distinct treatment arms dk ≠ dl whose outcomes are uniformly bounded by a nonnegative constant c₁ (Condition 1), suppose the marginal exposure propensities under dk and dl are positive with inverses uniformly bounded by a nonnegative constant c₂, and the same-arm and cross-arm pairwise joint exposure propensities have inverses uniformly bounded by a nonnegative constant c₃ (Condition 1'). Suppose further a symmetric, reflexive dependency relation G of degree at most m such that every non-adjacent pair's joint exposure propensities factor as if independent and every quadruple with no adjacent index pair has zero covariance between the corresponding variance-estimator kernel terms (Condition 3), and the population size diverges. Then the scaled variance of the conservative variance estimator vanishes: N²·Var[V̂_n] → 0.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
hne :
∀ n, dk n ≠ dl n
c₁ c₂ c₃ :
ℝ
hc₁ :
0 ≤ c₁
hc₂ :
0 ≤ c₂
hc₃ :
0 ≤ c₃
hy :
∀ n i d, |(Exp n).y i d| ≤ c₁
hπk :
∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dk n)
hπl :
∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dl n)
hπinvk :
∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≤ c₂
hπinvl :
∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≤ c₂
hjk :
∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≤ c₃
hjl :
∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≤ c₃
hjc :
∀ n i j, 1 / propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≤ c₃
G :
∀ n
if
(Exp n).ι
and
(Exp n).ι
then
Prop
decG :
∀ n, DecidableRel (G n)
hrefl :
∀ n i, G n i i
hsymm :
∀ n i j
if
G n i j
then
G n j i
m :
ℕ
hdeg :
∀ n i, (Finset.univ.filter (fun j => G n i j)).card ≤ m
hGindep :
∀ n i j
if
¬ G n i j
then
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n)
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n)
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n)
hcov0 :
conclusion
Tendsto (fun n => (card (Exp n).ι : ℝ) ^ 2 * (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) atTop (𝓝 0)
Proof (Lean source)
theorem var_NsqVhat_tendsto_zero_of_conditions
(Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ) (hne : ∀ n, dk n ≠ dl n)
{c₁ c₂ c₃ : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hc₃ : 0 ≤ c₃)
(hy : ∀ n i d, |(Exp n).y i d| ≤ c₁)
(hπk : ∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dk n))
(hπl : ∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dl n))
(hπinvk : ∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≤ c₂)
(hπinvl : ∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≤ c₂)
(hjk : ∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≤ c₃)
(hjl : ∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≤ c₃)
(hjc : ∀ n i j, 1 / propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≤ c₃)
(G : ∀ n, (Exp n).ι → (Exp n).ι → Prop) (decG : ∀ n, DecidableRel (G n))
(hrefl : ∀ n i, G n i i) (hsymm : ∀ n i j, G n i j → G n j i)
{m : ℕ} (hdeg : ∀ n i, (Finset.univ.filter (fun j => G n i j)).card ≤ m)
(hGindep : ∀ n i j, ¬ G n i j →
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n)
= prop (Exp n).D (Exp n).f (Exp n).θ i (dk n)
* prop (Exp n).D (Exp n).f (Exp n).θ j (dk n) ∧
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n)
= prop (Exp n).D (Exp n).f (Exp n).θ i (dl n)
* prop (Exp n).D (Exp n).f (Exp n).θ j (dl n) ∧
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n)
= prop (Exp n).D (Exp n).f (Exp n).θ i (dk n)
* prop (Exp n).D (Exp n).f (Exp n).θ j (dl n))
(hcov0 : ∀ n i j k l, ¬ (G n i k ∨ G n i l ∨ G n j k ∨ G n j l) →
(Exp n).D.Cov (vb (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) i j)
(vb (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) k l) = 0)
(hN : Tendsto (fun n => (card (Exp n).ι : ℝ)) atTop atTop) :
Tendsto (fun n => (card (Exp n).ι : ℝ) ^ 2 *
(Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
atTop (𝓝 0) := by
set C : ℝ := 8 * vbBound c₁ c₂ c₃ ^ 2 * (m : ℝ) ^ 3 with hCdef
refine squeeze_zero (g := fun n => C * (card (Exp n).ι : ℝ)⁻¹)
(fun n => ?_) (fun n => ?_) ?_
· exact mul_nonneg (sq_nonneg _) (Var_nonneg _ _)
· letI := decG n
exact NsqVar_htEffectVarEst_le (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)
(hne n) hc₁ hc₂ hc₃ (hy n) (hπk n) (hπl n) (hπinvk n) (hπinvl n)
(hjk n) (hjl n) (hjc n) (G n) (hrefl n) (hsymm n) (hdeg n) (hGindep n) (hcov0 n)
· have hinv : Tendsto (fun n => (card (Exp n).ι : ℝ)⁻¹) atTop (𝓝 0) :=
tendsto_inv_atTop_zero.comp hN
have := tendsto_const_nhds (x := C) |>.mul hinv
simpa using this
theorem wald_coverage_feasible_of_conditions reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Feasible Wald coverage from primitive boundedness, overlap, dependency-graph, and variance-growth conditions. Along a sequence of experiments with distinct treatment arms dk ≠ dl whose outcomes are uniformly bounded by a nonnegative constant c₁, suppose the marginal exposure propensities under dk and dl are positive with inverses uniformly bounded by a nonnegative constant c₂ — taken strictly positive — and the same-arm and cross-arm pairwise joint exposure propensities have inverses uniformly bounded by a nonnegative constant c₃, with all off-diagonal joint propensities strictly positive. Suppose a symmetric, reflexive dependency relation G of degree at most m makes every non-adjacent pair's joint exposure propensities factor as if independent and gives every quadruple with no adjacent index pair zero covariance between the variance-estimator kernel terms; suppose also the per-unit effect summands admit a Stein dependency graph Dg of degree at most m, that the population size diverges while population size times the true effect-estimator variance converges to a positive constant cVar and that variance is everywhere positive, and that zq is a nonnegative quantile satisfying Φ(zq) = 1 − α/2. Then the feasible Wald interval τ̂ ± zq·√V̂ attains asymptotic (liminf) coverage at least 1 − α.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
m :
ℕ
Dg :
∀ n,
SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i) (Exp n).D.toMeasure
hSteinDeg :
∀ n i, ((Dg n).nbhd i).card ≤ m
hne :
∀ n, dk n ≠ dl n
c₁ c₂ c₃ :
ℝ
hc₁ :
0 ≤ c₁
hc₂ :
0 ≤ c₂
hc₃ :
0 ≤ c₃
hc₂pos :
0 < c₂
hy :
∀ n i d, |(Exp n).y i d| ≤ c₁
hπk :
∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dk n)
hπl :
∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dl n)
hπinvk :
∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≤ c₂
hπinvl :
∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≤ c₂
hjk :
∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≤ c₃
hjl :
∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≤ c₃
hjc :
∀ n i j, 1 / propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≤ c₃
G :
∀ n
if
(Exp n).ι
and
(Exp n).ι
then
Prop
decG :
∀ n, DecidableRel (G n)
hrefl :
∀ n i, G n i i
hsymm :
∀ n i j
if
G n i j
then
G n j i
hdeg :
∀ n i, (Finset.univ.filter (fun j => G n i j)).card ≤ m
hGindep :
∀ n i j
if
¬ G n i j
then
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n)
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n)
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n)
hcov0 :
hjointk :
∀ n i j
if
i ≠ j
then
0 < propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n)
hjointl :
∀ n i j
if
i ≠ j
then
0 < propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n)
hjointc :
∀ n i j
if
i ≠ j
then
0 < propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n)
cVar :
ℝ
hcVar :
0 < cVar
hCond4 :
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
α :
ℝ
zq :
ℝ
hzq0 :
0 ≤ zq
hzq :
stdNormalCdf zq = 1 - α / 2
Proof (Lean source)
theorem wald_coverage_feasible_of_conditions
(Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
{m : ℕ}
(Dg : ∀ n, SteinMethod.DepGraph (fun i => (Exp n).effSummand (dk n) (dl n) i)
(Exp n).D.toMeasure)
(hSteinDeg : ∀ n i, ((Dg n).nbhd i).card ≤ m)
(hne : ∀ n, dk n ≠ dl n)
{c₁ c₂ c₃ : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hc₃ : 0 ≤ c₃)
(hc₂pos : 0 < c₂)
(hy : ∀ n i d, |(Exp n).y i d| ≤ c₁)
(hπk : ∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dk n))
(hπl : ∀ n i, 0 < prop (Exp n).D (Exp n).f (Exp n).θ i (dl n))
(hπinvk : ∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≤ c₂)
(hπinvl : ∀ n i, 1 / prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≤ c₂)
(hjk : ∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≤ c₃)
(hjl : ∀ n i j, 1 / propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≤ c₃)
(hjc : ∀ n i j, 1 / propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≤ c₃)
(G : ∀ n, (Exp n).ι → (Exp n).ι → Prop) (decG : ∀ n, DecidableRel (G n))
(hrefl : ∀ n i, G n i i) (hsymm : ∀ n i j, G n i j → G n j i)
(hdeg : ∀ n i, (Finset.univ.filter (fun j => G n i j)).card ≤ m)
(hGindep : ∀ n i j, ¬ G n i j →
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n)
= prop (Exp n).D (Exp n).f (Exp n).θ i (dk n)
* prop (Exp n).D (Exp n).f (Exp n).θ j (dk n) ∧
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n)
= prop (Exp n).D (Exp n).f (Exp n).θ i (dl n)
* prop (Exp n).D (Exp n).f (Exp n).θ j (dl n) ∧
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n)
= prop (Exp n).D (Exp n).f (Exp n).θ i (dk n)
* prop (Exp n).D (Exp n).f (Exp n).θ j (dl n))
(hcov0 : ∀ n i j k l, ¬ (G n i k ∨ G n i l ∨ G n j k ∨ G n j l) →
(Exp n).D.Cov (vb (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) i j)
(vb (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) k l) = 0)
(hN : Tendsto (fun n => (card (Exp n).ι : ℝ)) atTop atTop)
(hjointk : ∀ n i j, i ≠ j →
0 < propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n))
(hjointl : ∀ n i j, i ≠ j →
0 < propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n))
(hjointc : ∀ n i j, i ≠ j →
0 < propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n))
{cVar : ℝ} (hcVar : 0 < cVar)
(hCond4 : Tendsto (fun n => (card (Exp n).ι : ℝ)
* (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
atTop (𝓝 cVar))
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
{α : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - α / 2) :
1 - α ≤ liminf
(fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * sqrt
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z)))
atTop := by
have hclt : LocalDependenceCLT Exp dk dl :=
localDependenceCLT_of_paper_conditions Exp dk dl Dg m hSteinDeg c₁
(fun n i => hy n i (dk n)) (fun n i => hy n i (dl n)) c₂ hc₂pos
(fun n i => by
have hπinv := hπinvk n i
rw [one_div] at hπinv
rw [one_div]
exact (inv_le_comm₀ hc₂pos (hπk n i)).mpr hπinv)
(fun n i => by
have hπinv := hπinvl n i
rw [one_div] at hπinv
rw [one_div]
exact (inv_le_comm₀ hc₂pos (hπl n i)).mpr hπinv)
hN hVar cVar hcVar hCond4
have hVN := var_NsqVhat_tendsto_zero_of_conditions Exp dk dl hne hc₁ hc₂ hc₃ hy hπk hπl
hπinvk hπinvl hjk hjl hjc G decG hrefl hsymm hdeg hGindep hcov0 hN
have hrel := relVar_of_NsqVar_tendsto Exp dk dl hcVar hCond4 hVN
exact wald_coverage_feasible_of_relVar Exp dk dl hclt hne
(fun n i => (hπk n i).ne') (fun n i => (hπl n i).ne')
(fun n i j hij => (hjointk n i j hij).ne')
(fun n i j hij => (hjointl n i j hij).ne')
(fun n i j hij => (hjointc n i j hij).ne') hVar hrel
zq hzq0 hzq
VarianceConsistency 2 core · 1 supporting The feasible Wald interval of Aronow–Samii (Prop 6.5) uses the *estimated* variance Vh (htEffectVarEst). ★ htEffectVarEst_undershoot_tendsto_zero★ wald_coverage_feasible_of_relVar
Consistency of the conservative variance estimator (Aronow–Samii 2017)
The feasible Wald interval of Aronow–Samii (Prop 6.5) uses the estimated variance Vh
(htEffectVarEst). Its asymptotic coverage (wald_coverage_feasible) consumes a single
analytic input: the conservative estimate undershoots the true variance only with vanishing
probability,
∀ ε > 0, Pr[ Vh < (1−ε)·Var[τ̂] ] → 0.
This file reduces that input to one clean L²-relative-consistency limit
Var[Vh] / Var[τ̂]² → 0
via the finite Chebyshev inequality and the already-proven conservativeness
Var[τ̂] ≤ E[Vh] (E_htEffectVarEst_ge, Prop 5.x):
{ Vh < (1−ε)·Var } ⊆ { ε·Var ≤ |Vh − E Vh| } (using E Vh ≥ Var),
Pr[ ε·Var ≤ |Vh − E Vh| ] ≤ Var[Vh]/(ε·Var)² = (1/ε²)·(Var[Vh]/Var²),
and the right side tends to 0. The hypothesis Var[Vh]/Var² → 0 is the precise,
isolated remaining input — the quantitative content of the paper's appendix
variance-estimator-consistency bound under Conditions 1/3/4. Note that under Condition 4
(N·Var → c > 0, so Var ∼ c/N) this relative limit is equivalent to Var[N·Vh] → 0.
theorem htEffectVarEst_undershoot_tendsto_zero reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Reduction of feasible-interval variance consistency to L²-relative consistency. For a pair of treatment sequences dk, dl with dk n ≠ dl n for every n, suppose every unit has nonzero exposure propensity under dk and under dl, and every off-diagonal pair has nonzero same-arm and nonzero cross-arm joint exposure propensities — the standing overlap conditions giving the conservativeness Var[τ̂] ≤ E[V̂]. If the true effect-estimator variance is everywhere positive and the L²-relative-consistency limit Var[V̂]/Var[τ̂]² → 0 holds, then the conservative variance estimator undershoots the true variance only with vanishing probability: for every ε > 0, Pr[Vh < (1−ε)·Var[τ̂]] → 0.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
hne :
∀ n, dk n ≠ dl n
hk :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0
hl :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0
hjk :
∀ n i j
if
i ≠ j
then
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≠ 0
hjl :
∀ n i j
if
i ≠ j
then
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≠ 0
hjc :
∀ n i j
if
i ≠ j
then
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≠ 0
hVarpos :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
hrel :
Tendsto (fun n => (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) / ((Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) ^ 2) atTop (𝓝 0)
conclusion
∀ ε : ℝ
if
0 < ε
then
Tendsto (fun n => (Exp n).D.Pr (fun z => htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z < (1 - ε) * (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))) atTop (𝓝 0)
Proof (Lean source)
theorem htEffectVarEst_undershoot_tendsto_zero
(Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(hne : ∀ n, dk n ≠ dl n)
(hk : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0)
(hl : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0)
(hjk : ∀ n i j, i ≠ j →
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≠ 0)
(hjl : ∀ n i j, i ≠ j →
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≠ 0)
(hjc : ∀ n i j, i ≠ j →
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≠ 0)
(hVarpos : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(hrel : Tendsto (fun n =>
(Exp n).D.Var
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
/ ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) ^ 2)
atTop (𝓝 0)) :
∀ ε : ℝ, 0 < ε → Tendsto (fun n => (Exp n).D.Pr (fun z =>
htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
< (1 - ε) * (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))))
atTop (𝓝 0) := by
intro ε hε0
have hεne : ε ≠ 0 := hε0.ne'
-- Squeeze the coverage-defect probability between `0` and `(1/ε²)·(Var[Vh]/Var²)`.
refine squeeze_zero (g := fun n => (1 / ε ^ 2) *
((Exp n).D.Var
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
/ ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) ^ 2))
(fun n => (Exp n).D.Pr_nonneg _) (fun n => ?_) ?_
· -- Per-`n` upper bound via event inclusion + Chebyshev.
set Vh : (Exp n).Ω → ℝ :=
htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) with hVh
set Vr : ℝ := (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) with hVr
have hVrpos : 0 < Vr := hVarpos n
have hVrne : Vr ≠ 0 := hVrpos.ne'
-- Conservativeness: `E[Vh] ≥ Var[τ̂]`.
have hEge : Vr ≤ (Exp n).D.E Vh :=
E_htEffectVarEst_ge (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)
(hne n) (hk n) (hl n) (hjk n) (hjl n) (hjc n)
have haε : 0 < ε * Vr := mul_pos hε0 hVrpos
-- `{ Vh < (1−ε)Vr } ⊆ { ε·Vr ≤ |Vh − E Vh| }`.
have hsub : ∀ z, Vh z < (1 - ε) * Vr → ε * Vr ≤ |Vh z - (Exp n).D.E Vh| := by
intro z hz
have hexpand : (1 - ε) * Vr = Vr - ε * Vr := by ring
have hz' : Vh z < Vr - ε * Vr := by rw [hexpand] at hz; exact hz
have h1 : Vh z - (Exp n).D.E Vh < -(ε * Vr) := by linarith [hz', hEge]
have h2 : -(Vh z - (Exp n).D.E Vh) ≤ |Vh z - (Exp n).D.E Vh| :=
neg_le_abs _
linarith
have hmono := (Exp n).D.Pr_mono
(fun z => Vh z < (1 - ε) * Vr)
(fun z => ε * Vr ≤ |Vh z - (Exp n).D.E Vh|) hsub
have hcheb := (Exp n).D.chebyshev Vh haε
calc (Exp n).D.Pr (fun z => Vh z < (1 - ε) * Vr)
≤ (Exp n).D.Pr (fun z => ε * Vr ≤ |Vh z - (Exp n).D.E Vh|) := hmono
_ ≤ (Exp n).D.Var Vh / (ε * Vr) ^ 2 := hcheb
_ = (1 / ε ^ 2) * ((Exp n).D.Var Vh / Vr ^ 2) := by
rw [mul_pow]; field_simp
· -- `(1/ε²)·(Var[Vh]/Var²) → (1/ε²)·0 = 0`.
have h := hrel.const_mul (1 / ε ^ 2)
simpa using h
theorem wald_coverage_feasible_of_relVar reviewed
⚑ flagged
Causalean.Experimentation.ExposureMappingInterference
Feasible Wald coverage from L²-relative variance consistency (capstone). For a pair of treatment sequences dk, dl with dk n ≠ dl n for every n, suppose the studentized effect statistic satisfies the local-dependence central limit theorem, every unit has nonzero exposure propensity under dk and under dl, and every off-diagonal pair has nonzero same-arm and nonzero cross-arm joint exposure propensities. If the true effect-estimator variance is everywhere positive and the L²-relative-consistency limit Var[V̂]/Var[τ̂]² → 0 holds, with zq a nonnegative quantile satisfying Φ(zq) = 1 − α/2, then the paper's actual interval τ̂ ± zq·√V̂ attains asymptotic (liminf) coverage at least 1 − α.
Formal statement
hypotheses
Exp :
ℕ → Experiment
dk dl :
∀ n, (Exp n).Δ
hclt :
LocalDependenceCLT Exp dk dl
hne :
∀ n, dk n ≠ dl n
hk :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0
hl :
∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0
hjk :
∀ n i j
if
i ≠ j
then
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≠ 0
hjl :
∀ n i j
if
i ≠ j
then
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≠ 0
hjc :
∀ n i j
if
i ≠ j
then
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≠ 0
hVar :
∀ n, 0 < (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
hrel :
Tendsto (fun n => (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) / ((Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) ^ 2) atTop (𝓝 0)
α :
ℝ
zq :
ℝ
hzq0 :
0 ≤ zq
hzq :
stdNormalCdf zq = 1 - α / 2
Proof (Lean source)
theorem wald_coverage_feasible_of_relVar
(Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ)
(hclt : LocalDependenceCLT Exp dk dl)
(hne : ∀ n, dk n ≠ dl n)
(hk : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dk n) ≠ 0)
(hl : ∀ n i, prop (Exp n).D (Exp n).f (Exp n).θ i (dl n) ≠ 0)
(hjk : ∀ n i j, i ≠ j →
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dk n) ≠ 0)
(hjl : ∀ n i j, i ≠ j →
propPairSame (Exp n).D (Exp n).f (Exp n).θ i j (dl n) ≠ 0)
(hjc : ∀ n i j, i ≠ j →
propPairCross (Exp n).D (Exp n).f (Exp n).θ i j (dk n) (dl n) ≠ 0)
(hVar : ∀ n, 0 < (Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)))
(hrel : Tendsto (fun n =>
(Exp n).D.Var
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))
/ ((Exp n).D.Var
(htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) ^ 2)
atTop (𝓝 0))
{α : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - α / 2) :
1 - α ≤ liminf
(fun n => (Exp n).D.Pr (fun z =>
|htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z
- tauTrue (Exp n).y (dk n) (dl n)|
≤ zq * sqrt
(htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n) z)))
atTop :=
wald_coverage_feasible Exp dk dl hclt hVar
(htEffectVarEst_undershoot_tendsto_zero Exp dk dl hne hk hl hjk hjl hjc hVar hrel)
zq hzq0 hzq
1 supporting declaration (lemmas, instances)
-
relVar_of_NsqVar_tendstotheorem — Bridge from Var[N·V̂] → 0 to L²-relative consistency. The paper's appendix establishes Var[N·V̂_n] → 0 (here as N²·Var[V̂_n] → 0); together with Condition 4 (N·Var[τ̂_n] → c > 0) this yields the relative limit Var[V̂_n]/Var[τ̂_n]² → 0, via the identity Var[V̂]/Var² = (N²·Var[V̂])/(N·Var)² and Tendsto.div (numerator → 0, denominator → c² > 0).hypothesesExp :ℕ → Experimentdk dl :∀ n, (Exp n).Δc :ℝhc :0 < chCond4 :hVN :Tendsto (fun n => (card (Exp n).ι : ℝ) ^ 2 * (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) atTop (𝓝 0)conclusionTendsto (fun n => (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) / ((Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) ^ 2) atTop (𝓝 0)Proof (Lean source)
theorem relVar_of_NsqVar_tendsto (Exp : ℕ → Experiment) (dk dl : ∀ n, (Exp n).Δ) {c : ℝ} (hc : 0 < c) (hCond4 : Tendsto (fun n => (card (Exp n).ι : ℝ) * (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) atTop (𝓝 c)) (hVN : Tendsto (fun n => (card (Exp n).ι : ℝ) ^ 2 * (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) atTop (𝓝 0)) : Tendsto (fun n => (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) / ((Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n))) ^ 2) atTop (𝓝 0) := by set card : ℕ → ℝ := fun n => (card (Exp n).ι : ℝ) with hcard set Vr : ℕ → ℝ := fun n => (Exp n).D.Var (htEffect (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) with hVrdef set Vh : ℕ → ℝ := fun n => (Exp n).D.Var (htEffectVarEst (Exp n).D (Exp n).y (Exp n).f (Exp n).θ (dk n) (dl n)) with hVhdef -- `(N·Vr)² → c² ≠ 0`, and `N²·Vh → 0`, so the quotient tends to `0/c² = 0`. have hf : Tendsto (fun n => card n ^ 2 * Vh n / (card n * Vr n) ^ 2) atTop (𝓝 0) := by have h := hVN.div (hCond4.pow 2) (pow_ne_zero 2 hc.ne') rw [zero_div] at h exact h -- Eventually `N·Vr > 0`, hence `N ≠ 0` and `Vr ≠ 0`, giving the algebraic identity. have hpos : ∀ᶠ n in atTop, 0 < card n * Vr n := hCond4.eventually (eventually_gt_nhds hc) have hev : (fun n => card n ^ 2 * Vh n / (card n * Vr n) ^ 2) =ᶠ[atTop] (fun n => Vh n / Vr n ^ 2) := by filter_upwards [hpos] with n hn have hne : card n * Vr n ≠ 0 := hn.ne' have hcardn : card n ≠ 0 := fun h => hne (by rw [h, zero_mul]) rw [mul_pow, mul_div_mul_left _ _ (pow_ne_zero 2 hcardn)] exact hf.congr' hev