Experimentation.Super­Population

Super-population network inference: locally dependent fields, network-sum and mean CLTs, HAC variance estimation, and consistency bounds.

HACConsistency 2 core · 3 supporting · 2 submodules This roll-up imports the variance bound for the network-HAC estimator and the Chebyshev consistency theorem. Mean­CLT 5 core · 2 supporting · 3 submodules This roll-up imports the construction of centered, variance-normalized network fields, the hypotheses that make those fields mean-zero and unit-variance, and the final CLT turning the abstract m-dependent network-sum the
Basic 5 core · 0 supporting The design-based experimentation substrate (Experimentation/DesignBased/) fixes the potential outcomes and puts all randomness in the assignment, so its probability space is a finite product measure over the treatment ve ★ mem_nbhd_iff★ self_mem_nbhd

Super-population locally-dependent network field

The design-based experimentation substrate (Experimentation/DesignBased/) fixes the potential outcomes and puts all randomness in the assignment, so its probability space is a finite product measure over the treatment vector. The super-population / model-based route is the opposite: the units (and their outcomes) are themselves drawn from a population, the randomness is the sampling / population draw, and the dependence between units is governed by a network rather than by an assignment mechanism. This file provides the base object for that route.

A NetworkDependence is the model-based sibling of Causalean.Stat.IIDSample: instead of mutual independence (iIndepFun) it carries a bounded-range / m-dependent network — node-level random summands X i : Ω → ℝ on a common ambient space (Ω, μ), together with a reflexive, symmetric adjacency relation such that index sets with no edge between them carry independent summand tuples. This is exactly the data of a dependency graph (Causalean.SteinMethod.DepGraph), so toDepGraph exposes the field to the proved Stein dependency-graph CLT (stein_cdf_clt_of_depGraph), which the CLT file specializes.

This is the m-dependent (exact-independence-beyond-the-network) layer. Decaying-dependence (ψ- or mixing) models, where far-apart nodes are only approximately independent, are a different super-population abstraction and are not part of this module.

structure NetworkDependence reviewed
Causalean.Experimentation.SuperPopulation

A super-population locally-dependent network field: bundles node-level random summands on a common ambient probability space together with a network relation between units that is reflexive and symmetric, requires every summand to be measurable, and requires any two collections of units joined by no edge to carry independent summand tuples (exact m-dependence beyond the network). This is the model-based counterpart of the finite design — the randomness is the population draw, not the assignment — and the m-dependence sibling of an i.i.d. sample.

Definition (Lean source)
μ :
The node-level random summand (one real-valued contribution per unit).
X :
V → Ω → ℝ
The network / dependency relation between units.
adj :
V → V → Prop
Decidability of adjacency (for the neighborhood `Finset`).
decAdj :
Each unit is adjacent to itself.
refl :
∀ i, adj i i
The network is symmetric.
symm :
∀ i j
if
adj i j
then
adj j i
Each node summand is measurable.
meas :
∀ i, Measurable (X i)
Non-adjacent index sets carry independent summand tuples (exact `m`-dependence).
indep :
∀ A B : Finset V
if
(∀ a ∈ A, ∀ b ∈ B, ¬ adj a b)
then
IndepFun (fun ω => fun k : A => X k ω) (fun ω => fun k : B => X k ω) μ
Causalean.Experimentation.SuperPopulation.NetworkDependence · Causalean/Experimentation/SuperPopulation/Basic.lean:39
def toDepGraph reviewed
Causalean.Experimentation.SuperPopulation.NetworkDependence

The network field, viewed as a Stein dependency graph for its summands — a pure field rename, so the proved dependency-graph CLT applies verbatim.

Definition (Lean source)
def toDepGraph : DepGraph F.X μ where G := F.adj decG := F.decAdj refl := F.refl symm := F.symm meas := F.meas indep := F.indep
Causalean.Experimentation.SuperPopulation.NetworkDependence.toDepGraph · Causalean/Experimentation/SuperPopulation/Basic.lean:68 · uses NetworkDependence , DepGraph
def nbhd reviewed
Causalean.Experimentation.SuperPopulation.NetworkDependence

The closed network neighborhood N i = {j | adj i j} of a unit.

Definition (Lean source)
noncomputable def nbhd (i : V) : Finset V := F.toDepGraph.nbhd i
Causalean.Experimentation.SuperPopulation.NetworkDependence.nbhd · Causalean/Experimentation/SuperPopulation/Basic.lean:78 · uses NetworkDependence
theorem mem_nbhd_iff reviewed
Causalean.Experimentation.SuperPopulation.NetworkDependence

Unit j lies in unit i's network neighborhood if and only if i and j are adjacent in the underlying interference network.

Formal statement
i j :
V
j ∈ F.nbhd i ↔ F.adj i j
Proof (Lean source)
theorem mem_nbhd_iff {i j : V} : j ∈ F.nbhd i ↔ F.adj i j := F.toDepGraph.mem_nbhd_iff
Causalean.Experimentation.SuperPopulation.NetworkDependence.mem_nbhd_iff · Causalean/Experimentation/SuperPopulation/Basic.lean:82 · uses NetworkDependence , nbhd
theorem self_mem_nbhd reviewed
Causalean.Experimentation.SuperPopulation.NetworkDependence

Every unit lies in its own network neighborhood.

Formal statement
i :
V
i ∈ F.nbhd i
Proof (Lean source)
theorem self_mem_nbhd (i : V) : i ∈ F.nbhd i := F.toDepGraph.self_mem_nbhd i
Causalean.Experimentation.SuperPopulation.NetworkDependence.self_mem_nbhd · Causalean/Experimentation/SuperPopulation/Basic.lean:87 · uses NetworkDependence , nbhd
HAC 2 core · 0 supporting Inference for a super-population network field needs a variance estimator that is robust to the network dependence — the analog of a HAC / cluster-robust estimator. ★ netHACVarEst★ netHACVarEst_integral_eq_variance

Network-HAC variance estimator

Inference for a super-population network field needs a variance estimator that is robust to the network dependence — the analog of a HAC / cluster-robust estimator. Because far-apart units are independent (m-dependence beyond the network), the variance of the network sum collapses to a sum of within-neighborhood cross-products, so the natural estimator is

V̂ = ∑ᵢ ∑_{j ∈ N i} Xᵢ Xⱼ,

i.e. the empirical sum of products over network-adjacent pairs. This file defines that estimator and records its unbiasedness anchor: under mean-zero summands its expectation is exactly the variance of the network sum. Sequence-level consistency of for the true variance along a growing network is developed in the HACConsistency modules.

def netHACVarEst reviewed
Causalean.Experimentation.SuperPopulation.NetworkDependence

The network-HAC variance estimator for a network field: the empirical sum of summand products over network-adjacent pairs, V̂(ω) = ∑ᵢ ∑_{j ∈ N i} Xᵢ(ω)·Xⱼ(ω). It targets the variance of the network sum, whose cross-terms vanish outside the network neighborhoods.

Definition (Lean source)
noncomputable def NetworkDependence.netHACVarEst (F : NetworkDependence V Ω μ) (ω : Ω) : ℝ := ∑ i, ∑ j ∈ F.nbhd i, F.X i ω * F.X j ω
Causalean.Experimentation.SuperPopulation.NetworkDependence.netHACVarEst · Causalean/Experimentation/SuperPopulation/HAC.lean:33 · uses NetworkDependence
theorem netHACVarEst_integral_eq_variance reviewed
Causalean.Experimentation.SuperPopulation.NetworkDependence

Unbiasedness of the network-HAC estimator. Under a probability measure with square- integrable summands that are mean zero, the expectation of the network-HAC estimator equals the variance of the network sum: E[V̂] = Var(∑ᵢ Xᵢ).

Formal statement
F :
hL2 :
∀ i, MemLp (F.X i) 2 μ
hmean :
∀ i, ∫ ω, F.X i ω ∂μ = 0
∫ ω, F.netHACVarEst ω ∂μ = variance (depSum F.X) μ
Proof (Lean source)
theorem NetworkDependence.netHACVarEst_integral_eq_variance (F : NetworkDependence V Ω μ) [IsProbabilityMeasure μ] (hL2 : ∀ i, MemLp (F.X i) 2 μ) (hmean : ∀ i, ∫ ω, F.X i ω ∂μ = 0) : ∫ ω, F.netHACVarEst ω ∂μ = variance (depSum F.X) μ := by classical have hvar : variance (depSum F.X) μ = ∑ i, ∑ j, covariance (F.X i) (F.X j) μ := by exact variance_fun_sum hL2 have hprod : ∀ i j, ∫ ω, F.X i ω * F.X j ω ∂μ = covariance (F.X i) (F.X j) μ := by intro i j rw [covariance_eq_sub (hL2 i) (hL2 j)] simp [hmean i, hmean j] have hint : ∀ i j, Integrable (fun ω => F.X i ω * F.X j ω) μ := by intro i j exact (hL2 i).integrable_mul (hL2 j) have hzero : ∀ i j, j ∉ F.nbhd i → covariance (F.X i) (F.X j) μ = 0 := by intro i j hj have hsep : ∀ a ∈ ({i} : Finset V), ∀ b ∈ ({j} : Finset V), ¬ F.adj a b := by intro a ha b hb hab rw [mem_singleton] at ha rw [mem_singleton] at hb subst a subst b exact hj ((F.mem_nbhd_iff).mpr hab) have hind := F.indep ({i} : Finset V) ({j} : Finset V) hsep let φ : (({i} : Finset V) → ℝ) → ℝ := fun t => t ⟨i, Finset.mem_singleton.mpr rfl⟩ let ψ : (({j} : Finset V) → ℝ) → ℝ := fun t => t ⟨j, Finset.mem_singleton.mpr rfl⟩ have hφ : Measurable φ := measurable_pi_apply _ have hψ : Measurable ψ := measurable_pi_apply _ have hcomp := hind.comp hφ hψ have h1 : φ ∘ (fun ω => fun k : ({i} : Finset V) => F.X k ω) = F.X i := rfl have h2 : ψ ∘ (fun ω => fun k : ({j} : Finset V) => F.X k ω) = F.X j := rfl rw [h1, h2] at hcomp exact hcomp.covariance_eq_zero (hL2 i) (hL2 j) have hinner : ∀ i, ∑ j ∈ F.nbhd i, covariance (F.X i) (F.X j) μ = ∑ j, covariance (F.X i) (F.X j) μ := by intro i apply Finset.sum_subset (Finset.subset_univ _) intro j _ hj exact hzero i j hj calc ∫ ω, F.netHACVarEst ω ∂μ = ∫ ω, (∑ i, ∑ j ∈ F.nbhd i, F.X i ω * F.X j ω) ∂μ := rfl _ = ∑ i, ∑ j ∈ F.nbhd i, ∫ ω, F.X i ω * F.X j ω ∂μ := by rw [MeasureTheory.integral_finset_sum univ] · congr with i rw [MeasureTheory.integral_finset_sum (F.nbhd i)] intro j _ exact hint i j · intro i _ exact integrable_finset_sum (F.nbhd i) (fun j _ => hint i j) _ = ∑ i, ∑ j ∈ F.nbhd i, covariance (F.X i) (F.X j) μ := by refine Finset.sum_congr rfl ?_ intro i _ refine Finset.sum_congr rfl ?_ intro j _ exact hprod i j _ = ∑ i, ∑ j, covariance (F.X i) (F.X j) μ := by refine Finset.sum_congr rfl ?_ intro i _ exact hinner i _ = variance (depSum F.X) μ := hvar.symm
Causalean.Experimentation.SuperPopulation.NetworkDependence.netHACVarEst_integral_eq_variance · Causalean/Experimentation/SuperPopulation/HAC.lean:39 · uses NetworkDependence , netHACVarEst , depSum
CLT 1 core · 0 supporting For a sequence of super-population network fields (one per population size n) with bounded degree m, uniformly bounded summands |X i| ≤ Bₙ shrinking with Bₙ → 0 and N·Bₙ³ → 0, mean-zero summands, and unit total variance, ★ networkSum_clt

m-dependent CLT for a super-population network field

For a sequence of super-population network fields (one per population size n) with bounded degree m, uniformly bounded summands |X i| ≤ Bₙ shrinking with Bₙ → 0 and N·Bₙ³ → 0, mean-zero summands, and unit total variance, the network sum ∑ᵢ Xᵢ converges in distribution to the standard normal. This is the model-based (super-population, network-dependence) analog of the design-based prodDesign_clt, and is obtained by viewing the field as a Stein dependency graph (NetworkDependence.toDepGraph) and invoking the proved bounded-degree dependency-graph CLT stein_cdf_clt_of_depGraph — the m-dependence (exact independence beyond the network) is exactly its leave-out independence hypothesis.

theorem networkSum_clt reviewed
Causalean.Experimentation.SuperPopulation

m-dependent network CLT (super-population). Consider a sequence of super-population network fields F n, each on a probability space with measure μ n, whose dependency graph has degree at most m, whose summands are uniformly bounded in absolute value by a sequence B n tending to zero fast enough that card(Vₙ)·(Bₙ)³ → 0, and whose summands are mean zero with the network sum having unit total variance for every n. Then the network sum's cumulative distribution function converges pointwise to the standard normal CDF: P[∑ᵢ (F n).X i ≤ s] → Φ(s).

Formal statement
V :
ℕ → Type*
∀ n, Fintype (V n)
∀ n, DecidableEq (V n)
Ω :
ℕ → Type*
∀ n, MeasurableSpace (Ω n)
μ :
∀ n, Measure (Ω n)
∀ n, IsProbabilityMeasure (μ n)
F :
∀ n, NetworkDependence (V n) (Ω n) (μ n)
m :
hdeg :
∀ n i, ((F n).toDepGraph.nbhd i).card ≤ m
B :
ℕ → ℝ
hB :
∀ n, 0 ≤ B n
hbound :
∀ n i ω, |(F n).X i ω| ≤ B n
hB0 :
Tendsto B atTop (𝓝 0)
hNB3 :
Tendsto (fun n => (card (V n) : ℝ) * (B n) ^ 3) atTop (𝓝 0)
hmean :
∀ n i, ∫ ω, (F n).X i ω ∂(μ n) = 0
hvar :
∀ n, ∫ ω, (depSum (F n).X ω) ^ 2 ∂(μ n) = 1
s :
Tendsto (fun n => ((μ n).map (depSum (F n).X)).real (Iic s)) atTop (𝓝 ((gaussianReal 0 1).real (Iic s)))
Proof (Lean source)
theorem networkSum_clt {V : ℕ → Type*} [∀ n, Fintype (V n)] [∀ n, DecidableEq (V n)] {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)] (μ : ∀ n, Measure (Ω n)) [∀ n, IsProbabilityMeasure (μ n)] (F : ∀ n, NetworkDependence (V n) (Ω n) (μ n)) (m : ℕ) (hdeg : ∀ n i, ((F n).toDepGraph.nbhd i).card ≤ m) (B : ℕ → ℝ) (hB : ∀ n, 0 ≤ B n) (hbound : ∀ n i ω, |(F n).X i ω| ≤ B n) (hB0 : Tendsto B atTop (𝓝 0)) (hNB3 : Tendsto (fun n => (card (V n) : ℝ) * (B n) ^ 3) atTop (𝓝 0)) (hmean : ∀ n i, ∫ ω, (F n).X i ω ∂(μ n) = 0) (hvar : ∀ n, ∫ ω, (depSum (F n).X ω) ^ 2 ∂(μ n) = 1) (s : ℝ) : Tendsto (fun n => ((μ n).map (depSum (F n).X)).real (Iic s)) atTop (𝓝 ((gaussianReal 0 1).real (Iic s))) := stein_cdf_clt_of_depGraph μ (fun n => (F n).X) (fun n => (F n).toDepGraph) m hdeg B hB hbound hB0 hNB3 hmean hvar s
Causalean.Experimentation.SuperPopulation.networkSum_clt · Causalean/Experimentation/SuperPopulation/CLT.lean:29 · uses NetworkDependence , toDepGraph , nbhd , depSum