Experimentation.Exposure­Mapping­Interference.Asymptotics

Horvitz–Thompson exposure-mean consistency

Along a sequence of nested finite-population experiments, the HT exposure-mean estimator converges in probability to its estimand under versions of the two assumptions used for Aronow–Samii (2017), Proposition 6.1:

* Condition 3 (boundedness): outcomes and inverse exposure probabilities are bounded, so each weighted summand y_i(d)/π_i(d) is bounded by a constant c. * Condition 4 (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. The theorem is the one-exposure component used to obtain the paper's effect-estimator conclusion, rather than Proposition 6.1 itself.

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.

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_bounded_degree_scaled_variance, which packages bounded outcomes, positive propensities, population growth, a bounded-degree dependency graph, and an assumed positive scaled-variance limit. These are alternative sufficient conditions, not a derivation of Aronow–Samii's exact Conditions 3, 5, and 6. The corresponding wald_coverage_of_* theorems compose these CLT discharges with the oracle Wald-coverage theorem.

Finite-grid variance bound for the conservative variance estimator

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 the bounded outcomes and inverse propensities in Aronow–Samii's Condition 3, plus an explicit additional joint-overlap bound 1/π_{ij} ≤ c₃ on all ordered pairs; * 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 last two assumptions are explicit factorization and covariance conditions for this finite-grid argument. Together with bounded degree, they are an alternative sufficient-condition route toward the variance consistency used in the paper's Proposition 6.2, not a formalization of its exact Conditions 3, 5, and 6.

Wald-coverage transfer lemmas

Given the local-dependence CLT interface and rowwise positive variances, this module transfers asymptotic normality into oracle Wald coverage. It also gives the corresponding feasible transfer when variance-estimator undershoot probabilities vanish. These lemmas assume the main analytic inputs; they do not by themselves formalize Aronow–Samii (2017), Proposition 6.2 or its Conditions 3, 5, and 6. An alternative finite-grid sufficient-condition result, based on explicit bounded-degree, factorization, covariance-vanishing, and scaled-variance hypotheses, is wald_coverage_feasible_of_bounded_degree_factorization_covariance in VarEstConsistencyConditions.lean.

The oracle theorem 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.)

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 → ∞.

Consistency of the conservative variance estimator

The feasible Wald interval in Aronow–Samii (2017), Proposition 6.2, 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, a positive-joint-probability specialization of Proposition 5.6):

{ 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. Under the separately assumed scaled-variance limit N·Var → c > 0, this relative limit follows from Var[N·Vh] → 0. The bounded-degree, factorization, and covariance-vanishing hypotheses used elsewhere in this development are alternative sufficient conditions, not a restatement of the paper's Conditions 3, 5, and 6.