Experimentation.Super­Population.HACConsistency

This roll-up imports the variance bound for the network-HAC estimator and the Chebyshev consistency theorem.

Consistency 1 core · 1 supporting This file proves the variance-estimator consistency input for feasible inference with super-population network dependence: the network-HAC estimator V̂ = ∑ᵢ ∑_{j ∈ N i} Xᵢ Xⱼ converges in probability to the variance of t ★ netHAC_consistent

Consistency of the network-HAC variance estimator

This file proves the variance-estimator consistency input for feasible inference with super-population network dependence: the network-HAC estimator V̂ = ∑ᵢ ∑_{j ∈ N i} Xᵢ Xⱼ converges in probability to the variance of the network sum under bounded-degree and shrinking summand conditions. It supplies a consistency ingredient for future Wald-style conclusions, but does not itself prove a Wald statistic or coverage theorem.

The argument is Chebyshev:

* the estimator is unbiased, E[V̂] = Var(∑ᵢ Xᵢ) (the proved identity NetworkDependence.netHACVarEst_integral_eq_variance), and * its variance tends to zero (netHACVarEst_variance_tendsto_zero),

so for every ε > 0 the deviation probability (μ n)({ω | ε ≤ |V̂ ω − Var(∑ᵢ Xᵢ)|}) ≤ Var(V̂)/ε² → 0.

netHAC_consistent is the resulting convergence-in-probability statement, stated with the real-valued measure Measure.real to match the convergence-mode convention used elsewhere in the library. The bounded-summand MemLp anchor is the auxiliary netHACVarEst_memLp.

theorem netHAC_consistent reviewed
Causalean.Experimentation.SuperPopulation.HACConsistency

HAC consistency (convergence in probability). Consider a sequence of super-population network fields F n over probability spaces with measures μ n, each in the CLT regime — dependency-graph degree at most m, summands uniformly bounded by a sequence B n tending to zero with card(Vₙ)·(Bₙ)³ → 0, and square-integrable, mean-zero summands — and an arbitrary error tolerance ε > 0. Then the network-HAC variance estimator converges in probability to the variance of the network sum: the probability that the estimator deviates from that variance by at least ε tends to zero as n → ∞.

Formal statement
hypotheses
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)
hL2 :
∀ n i, MemLp ((F n).X i) 2 (μ n)
hmean :
∀ n i, ∫ ω, (F n).X i ω ∂(μ n) = 0
ε :
ℝ
hε :
0 < ε
conclusion
Tendsto (fun n => (μ n).real {ω | ε ≤ |(F n).netHACVarEst ω - variance (depSum (F n).X) (μ n)|}) atTop (𝓝 0)
Proof (Lean source)
theorem netHAC_consistent {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)) (hL2 : ∀ n i, MemLp ((F n).X i) 2 (μ n)) (hmean : ∀ n i, ∫ ω, (F n).X i ω ∂(μ n) = 0) (ε : ℝ) (hε : 0 < ε) : Tendsto (fun n => (μ n).real {ω | ε ≤ |(F n).netHACVarEst ω - variance (depSum (F n).X) (μ n)|}) atTop (𝓝 0) := by have hmemLp : ∀ n, MemLp (fun ω => (F n).netHACVarEst ω) 2 (μ n) := fun n => netHACVarEst_memLp (F n) (hB n) (hbound n) (hdeg n) have hEq : ∀ n, ∫ ω, (F n).netHACVarEst ω ∂(μ n) = variance (depSum (F n).X) (μ n) := fun n => (F n).netHACVarEst_integral_eq_variance (hL2 n) (hmean n) have hupper : Tendsto (fun n => variance (fun ω => (F n).netHACVarEst ω) (μ n) / ε ^ 2) atTop (𝓝 0) := by simpa using (netHACVarEst_variance_tendsto_zero μ F m hdeg B hB hbound hB0 hNB3).div_const (ε ^ 2) refine squeeze_zero (fun n => measureReal_nonneg) (fun n => ?_) hupper have hcheb := meas_ge_le_variance_div_sq (hmemLp n) hε rw [hEq n] at hcheb have hnn : (0 : ℝ) ≤ variance (fun ω => (F n).netHACVarEst ω) (μ n) / ε ^ 2 := by exact div_nonneg (variance_nonneg _ _) (sq_nonneg ε) rw [measureReal_def] calc ((μ n) {ω | ε ≤ |(F n).netHACVarEst ω - variance (depSum (F n).X) (μ n)|}).toReal ≤ (ofReal (variance (fun ω => (F n).netHACVarEst ω) (μ n) / ε ^ 2)).toReal := ENNReal.toReal_mono ENNReal.ofReal_ne_top hcheb _ = variance (fun ω => (F n).netHACVarEst ω) (μ n) / ε ^ 2 := ENNReal.toReal_ofReal hnn
Causalean.Experimentation.SuperPopulation.HACConsistency.netHAC_consistent · Causalean/Experimentation/SuperPopulation/HACConsistency/Consistency.lean:85 · uses NetworkDependence , netHACVarEst , toDepGraph , nbhd , depSum
1 supporting declaration (lemmas, instances)
  • netHACVarEst_memLp theorem — The network-HAC estimator is in L². With summands bounded by B and degree ≤ m, the estimator V̂ is pointwise bounded by card(V)·m·B², hence square-integrable; this is the moment hypothesis Chebyshev's inequality needs.
    hypotheses
    F :
    NetworkDependence V Ω μ
    IsProbabilityMeasure μ
    B :
    ℝ
    hB :
    0 ≤ B
    hbound :
    ∀ i ω, |F.X i ω| ≤ B
    m :
    ℕ
    hdeg :
    ∀ i, (F.toDepGraph.nbhd i).card ≤ m
    conclusion
    MemLp (fun ω => F.netHACVarEst ω) 2 μ
    Proof (Lean source)
    theorem netHACVarEst_memLp (F : NetworkDependence V Ω μ) [IsProbabilityMeasure μ] {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ i ω, |F.X i ω| ≤ B) {m : ℕ} (hdeg : ∀ i, (F.toDepGraph.nbhd i).card ≤ m) : MemLp (fun ω => F.netHACVarEst ω) 2 μ := by classical have hmeas : Measurable (fun ω => F.netHACVarEst ω) := by simp only [NetworkDependence.netHACVarEst] exact measurable_sum _ (fun i _ => measurable_sum _ (fun j _ => (F.meas i).mul (F.meas j))) have hpt : ∀ ω, |F.netHACVarEst ω| ≤ (Fintype.card V : ℝ) * ((m : ℝ) * B ^ 2) := by intro ω 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 ω| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ i, ∑ j ∈ F.nbhd i, |F.X i ω * F.X j ω| := Finset.sum_le_sum (fun i _ => Finset.abs_sum_le_sum_abs _ _) _ ≤ ∑ i, ∑ j ∈ F.nbhd i, B * B := Finset.sum_le_sum (fun i _ => Finset.sum_le_sum (fun j _ => by rw [abs_mul] exact mul_le_mul (hbound i ω) (hbound j ω) (abs_nonneg _) hB)) _ = ∑ i, ((F.nbhd i).card : ℝ) * (B * B) := by refine Finset.sum_congr rfl (fun i _ => ?_) rw [Finset.sum_const, nsmul_eq_mul] _ ≤ ∑ _i : V, (m : ℝ) * (B * B) := by refine Finset.sum_le_sum (fun i _ => ?_) apply mul_le_mul_of_nonneg_right _ (by positivity) change ((F.toDepGraph.nbhd i).card : ℝ) ≤ (m : ℝ) exact_mod_cast hdeg i _ = (Fintype.card V : ℝ) * ((m : ℝ) * B ^ 2) := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] ring exact MemLp.of_bound hmeas.aestronglyMeasurable ((Fintype.card V : ℝ) * ((m : ℝ) * B ^ 2)) (Filter.Eventually.of_forall (fun ω => by rw [Real.norm_eq_abs] exact hpt ω))
    Causalean.Experimentation.SuperPopulation.HACConsistency.netHACVarEst_memLp · Causalean/Experimentation/SuperPopulation/HACConsistency/Consistency.lean:42
Variance­Bound 1 core · 2 supporting The network-HAC estimator V̂ = ∑ᵢ ∑_{j ∈ N i} Xᵢ Xⱼ of a super-population locally-dependent network field (Causalean.Experimentation.SuperPopulation.NetworkDependence.netHACVarEst) is *itself* a sum of products over netw ★ netHACVarEst_variance_le

Variance bound for the network-HAC variance estimator

The network-HAC estimator V̂ = ∑ᵢ ∑_{j ∈ N i} Xᵢ Xⱼ of a super-population locally-dependent network field (Causalean.Experimentation.SuperPopulation.NetworkDependence.netHACVarEst) is itself a sum of products over network-adjacent pairs. Rewritten with Finset.mul_sum it is exactly the localized double sum ∑ᵢ Xᵢ · (∑_{j ∈ N i} Xⱼ) whose variance the proved dependency-graph pair-counting bound Causalean.SteinMethod.DepGraph.var_nbhd_prod_le controls.

This file records two facts.

* netHACVarEst_variance_le — the estimator-variance bound: for a single field with bounded summands |Xᵢ| ≤ B and bounded degree m, the variance of V̂ is at most a polynomial in m times card(V)·B⁴, namely 2·m⁵·card(V)·B⁴. This is the substantive lemma: it is derived from the m-dependence (covariances of separated localized products vanish) and the bounded-degree pair counting, not assumed.

* netHACVarEst_variance_tendsto_zero — the variance → 0 corollary: along a CLT-regime sequence with B n → 0 and card(V n)·(B n)³ → 0, the estimator variance tends to zero (squeeze the bound, using card·B⁴ = (card·B³)·B → 0).

The consistency-in-probability statement is assembled in Consistency.lean from this variance limit and the unbiasedness identity netHACVarEst_integral_eq_variance via Chebyshev.

theorem netHACVarEst_variance_le reviewed
Causalean.Experimentation.SuperPopulation.HACConsistency

Estimator-variance bound. For a super-population network field F, given a nonnegative bound B such that every summand is bounded in absolute value by B and every network neighborhood has size at most m, the variance of the network-HAC estimator V̂ = ∑ᵢ ∑_{j∈N i} Xᵢ Xⱼ is at most 2·m⁵·card(V)·B⁴.

Formal statement
hypotheses
F :
NetworkDependence V Ω μ
IsProbabilityMeasure μ
B :
ℝ
hB :
0 ≤ B
hbound :
∀ i ω, |F.X i ω| ≤ B
m :
ℕ
hdeg :
∀ i, (F.toDepGraph.nbhd i).card ≤ m
conclusion
variance (fun ω => F.netHACVarEst ω) μ ≤ 2 * (m : ℝ) ^ 5 * (Fintype.card V : ℝ) * B ^ 4
Proof (Lean source)
theorem netHACVarEst_variance_le (F : NetworkDependence V Ω μ) [IsProbabilityMeasure μ] {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ i ω, |F.X i ω| ≤ B) {m : ℕ} (hdeg : ∀ i, (F.toDepGraph.nbhd i).card ≤ m) : variance (fun ω => F.netHACVarEst ω) μ ≤ 2 * (m : ℝ) ^ 5 * (Fintype.card V : ℝ) * B ^ 4 := by have hrw : (fun ω => F.netHACVarEst ω) = (fun ω => ∑ i, F.X i ω * ∑ k ∈ F.toDepGraph.nbhd i, F.X k ω) := by funext ω; exact netHACVarEst_eq_locProd F ω rw [hrw] exact F.toDepGraph.var_nbhd_prod_le hB hbound hdeg
Causalean.Experimentation.SuperPopulation.HACConsistency.netHACVarEst_variance_le · Causalean/Experimentation/SuperPopulation/HACConsistency/VarianceBound.lean:50 · uses NetworkDependence , netHACVarEst , toDepGraph , nbhd
2 supporting declarations (lemmas, instances)
  • netHACVarEst_eq_locProd theorem — The network-HAC estimator equals the localized double sum ∑ᵢ Xᵢ · (∑_{j ∈ N i} Xⱼ): the pointwise identity that lets the dependency-graph variance bound apply to V̂ verbatim.
    hypotheses
    F :
    NetworkDependence V Ω μ
    ω :
    Ω
    conclusion
    F.netHACVarEst ω = ∑ i, F.X i ω * ∑ k ∈ F.toDepGraph.nbhd i, F.X k ω
    Proof (Lean source)
    theorem netHACVarEst_eq_locProd (F : NetworkDependence V Ω μ) (ω : Ω) : F.netHACVarEst ω = ∑ i, F.X i ω * ∑ k ∈ F.toDepGraph.nbhd i, F.X k ω := by simp only [NetworkDependence.netHACVarEst, NetworkDependence.nbhd, Finset.mul_sum]
    Causalean.Experimentation.SuperPopulation.HACConsistency.netHACVarEst_eq_locProd · Causalean/Experimentation/SuperPopulation/HACConsistency/VarianceBound.lean:44
  • netHACVarEst_variance_tendsto_zero theorem — Estimator variance tends to zero. Along a sequence of super-population network fields F n in the CLT regime — bounded degree m, summands bounded by B n with B n → 0, and card(V n)·(B n)³ → 0 — the variance of the network-HAC estimator tends to zero.
    hypotheses
    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)
    conclusion
    Tendsto (fun n => variance (fun ω => (F n).netHACVarEst ω) (μ n)) atTop (𝓝 0)
    Proof (Lean source)
    theorem netHACVarEst_variance_tendsto_zero {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)) : Tendsto (fun n => variance (fun ω => (F n).netHACVarEst ω) (μ n)) atTop (𝓝 0) := by have hub : Tendsto (fun n => 2 * (m : ℝ) ^ 5 * (card (V n) : ℝ) * (B n) ^ 4) atTop (𝓝 0) := by have hfac : (fun n => 2 * (m : ℝ) ^ 5 * (card (V n) : ℝ) * (B n) ^ 4) = (fun n => (2 * (m : ℝ) ^ 5) * (((card (V n) : ℝ) * (B n) ^ 3) * B n)) := by funext n; ring rw [hfac] have h := (hNB3.mul hB0) simpa using (h.const_mul (2 * (m : ℝ) ^ 5)).congr (fun n => by ring) refine squeeze_zero (fun n => variance_nonneg _ _) (fun n => ?_) hub exact netHACVarEst_variance_le (F n) (hB n) (hbound n) (hdeg n)
    Causalean.Experimentation.SuperPopulation.HACConsistency.netHACVarEst_variance_tendsto_zero · Causalean/Experimentation/SuperPopulation/HACConsistency/VarianceBound.lean:70