Stat.Nonparametric.HOIF
Higher-order influence-function machinery for localized nonparametric functionals: product remainders, degenerate U-statistic variance, projected-kernel trace identities, and projection-risk assembly.
DegenerateUStatVariance 2 core · 2 supporting Variance bounds for degenerate rank-2 U-statistic terms in higher-order influence-function estimators. ★ degenerate_uStatistic_variance★ degenerate_uStatistic_variance_le
Variance of the degenerate (rank-2) U-statistic: the J/(nh)² term
Variance bounds for degenerate rank-2 U-statistic terms in higher-order influence-function estimators.
The order-m HOIF estimator's stochastic term is dominated by a degenerate order-2
U-statistic whose kernel is a J-dimensional, bandwidth-h localized projection. For such a
kernel g (∫ g(x,·) dP = 0, symmetric, square-integrable) the off-diagonal second-moment
computation of Causalean.Stat.UStatistic.Variance (integral_offDiag_sum_sq) gives the exact
variance
Var[Uₙ] = 2ζ / (n(n−1)), ζ = ∬ g² dP dP.
When the localized projection kernel has L²-energy ζ ≤ C·J/h², this yields the HOIF
degenerate U-statistic variance bound
Var[Uₙ] ≤ 4C·J / (nh)²,
the O(J/(nh)²) term of the projection-risk decomposition. The sibling
HOIF.ProjectedKernelTrace file supplies the algebraic inverse-Gram trace identity ζ = J
for the unlocalized projected kernel; the bandwidth-localized inequality is the hypothesis
passed to degenerate_uStatistic_variance_le.
Exact variance of the degenerate order-2 U-statistic. For an i.i.d. sample S, if the kernel g is symmetric, square-integrable, and doubly degenerate — its conditional expectation given either argument vanishes — and the sample size n is at least 2, then the order-2 U-statistic built from g on n observations has variance Var[Uₙ] = 2ζ / (n(n−1)), where ζ = ∬ g² dP dP.
Formal statement
Proof (Lean source)
HOIF degenerate U-statistic variance bound O(J/(nh)²). For an i.i.d. sample S, if the kernel g is symmetric, square-integrable, and doubly degenerate, the sample size n is at least 2, the bandwidth h is positive, the projection dimension J is nonnegative, the trace constant C is nonnegative, and the localized, J-dimensional projection kernel g has L²-energy ζ = ∬ g² dP dP bounded by C·J/h², then the degenerate order-2 U-statistic's variance satisfies Var[Uₙ] ≤ 4C·J / (nh)².
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
memLp_uStatistictheorem — The degenerate order-2 U-statistic is in L² (rescaling the √n-version).hypothesesconclusionMemLp (uStatistic S g n) 2 μProof (Lean source)
theorem memLp_uStatistic (S : IIDSample Ω X μ P) (hg : DegenKernel P g) {n : ℕ} (hn : 2 ≤ n) : MemLp (uStatistic S g n) 2 μ := by have hn0 : (0 : ℝ) < (n : ℝ) := by exact_mod_cast (by omega : 0 < n) have hsqrt : sqrt (n : ℝ) ≠ 0 := by simp only [ne_eq, Real.sqrt_eq_zero']; push_neg; exact hn0 have hres : MemLp (fun ω => sqrt (n : ℝ) * uStatistic S g n ω) 2 μ := S.memLp_rescaled hg n have hrw : uStatistic S g n = fun ω => (sqrt (n : ℝ))⁻¹ * (sqrt (n : ℝ) * uStatistic S g n ω) := by funext ω; rw [← mul_assoc, inv_mul_cancel₀ hsqrt, one_mul] rw [hrw] exact hres.const_mul _ -
integral_uStatistic_eq_zerotheorem — Mean of the degenerate U-statistic is zero.hypothesesconclusion∫ ω, uStatistic S g n ω ∂μ = 0Proof (Lean source)
theorem integral_uStatistic_eq_zero (S : IIDSample Ω X μ P) (hg : DegenKernel P g) {n : ℕ} (hn : 2 ≤ n) : ∫ ω, uStatistic S g n ω ∂μ = 0 := by have hn0 : (0 : ℝ) < (n : ℝ) := by exact_mod_cast (by omega : 0 < n) have hsqrt : sqrt (n : ℝ) ≠ 0 := by simp only [ne_eq, Real.sqrt_eq_zero']; push_neg; exact hn0 have h := S.integral_rescaled_eq_zero hg n rw [integral_const_mul] at h exact (mul_eq_zero.mp h).resolve_left hsqrt
ProductRemainder 1 core · 2 supporting The order-m higher-order influence function (HOIF) estimator removes the leading nuisance-estimation bias up to a remainder that is a *finite sum of products of m+1 nuisance L²-errors*. ★ hoif_order_choice_negligible
Order-m HOIF estimation bias: the product remainder
The order-m higher-order influence function (HOIF) estimator removes the leading
nuisance-estimation bias up to a remainder that is a finite sum of products of m+1
nuisance L²-errors. Writing δ for the largest of those errors, every term of the
remainder is a product of m+1 factors each ≤ δ, so the whole remainder is bounded by
|T|·δ^{m+1} (with |T| the fixed number of terms), and its squared contribution by
R² ≤ |T|²·δ^{2(m+1)}.
This is the order-m analogue of the second-order doubly-robust remainder
(product of two nuisance errors): pushing to order m buys the higher power δ^{m+1}.
Choosing the order m so that 2(m+1)λ_* > the target risk exponent makes this squared
contribution o(ρ_n) — the rate-selection lemma hoif_order_choice_negligible.
This file is purely elementary (finite products of bounded reals + a power-law limit); it carries no measure theory and is the leaf of the HOIF substrate.
Rate selection: a high-enough HOIF order makes the squared remainder o(ρ_n). For a squared product-remainder bound of the power-law form K·n^{-a} and a target risk rate ρ_n = n^{-κ}, if the remainder's decay exponent a exceeds the target rate's exponent κ, then the ratio (K·n^{-a}) / n^{-κ} = K·n^{κ-a} tends to 0 as n → ∞: the HOIF estimation bias is asymptotically negligible relative to the target rate.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
prod_le_pow_of_factors_letheorem — A product of m+1 factors each in [0, δ] is at most δ^{m+1}. Each nuisance-error factor of a single HOIF remainder term is nonnegative and bounded by the largest error δ; multiplying m+1 of them keeps the product below δ^{m+1}.hypothesesι :Type*e :ι → ℝm :ℕδ :ℝs :Finset ℕidx :ℕ → ιhcard :s.card = m + 1hnn :∀ k ∈ s, 0 ≤ e (idx k)hle :∀ k ∈ s, e (idx k) ≤ δconclusion∏ k ∈ s, e (idx k) ≤ δ ^ (m + 1)Proof (Lean source)
theorem prod_le_pow_of_factors_le {ι : Type*} (e : ι → ℝ) (m : ℕ) (δ : ℝ) (s : Finset ℕ) (idx : ℕ → ι) (hcard : s.card = m + 1) (hnn : ∀ k ∈ s, 0 ≤ e (idx k)) (hle : ∀ k ∈ s, e (idx k) ≤ δ) : ∏ k ∈ s, e (idx k) ≤ δ ^ (m + 1) := by calc ∏ k ∈ s, e (idx k) ≤ ∏ _k ∈ s, δ := Finset.prod_le_prod (fun k hk => hnn k hk) (fun k hk => hle k hk) _ = δ ^ (m + 1) := by rw [Finset.prod_const, hcard] -
hoif_remainder_sq_letheorem — Squared HOIF product-remainder bound. The order-m HOIF estimation-bias remainder R is dominated by a sum, over a finite index set T of terms, of products of m+1 nuisance-error factors e t k; every factor lies in [0, δ], where δ is the largest nuisance L²-error. Then the remainder's squared contribution obeys R² ≤ |T|²·δ^{2(m+1)}. This is the order-m doubly-robust bound: the higher the order, the higher the power of δ.hypothesesι :Type*T :Finset ιe :ι → ℕ → ℝm :ℕδ :ℝR :ℝhnn :∀ t ∈ T, ∀ k ∈ range (m + 1), 0 ≤ e t khle :∀ t ∈ T, ∀ k ∈ range (m + 1), e t k ≤ δhbound :|R| ≤ ∑ t ∈ T, ∏ k ∈ range (m + 1), e t kconclusionR ^ 2 ≤ (T.card : ℝ) ^ 2 * δ ^ (2 * (m + 1))Proof (Lean source)
theorem hoif_remainder_sq_le {ι : Type*} (T : Finset ι) (e : ι → ℕ → ℝ) (m : ℕ) (δ : ℝ) (R : ℝ) (hnn : ∀ t ∈ T, ∀ k ∈ range (m + 1), 0 ≤ e t k) (hle : ∀ t ∈ T, ∀ k ∈ range (m + 1), e t k ≤ δ) (hbound : |R| ≤ ∑ t ∈ T, ∏ k ∈ range (m + 1), e t k) : R ^ 2 ≤ (T.card : ℝ) ^ 2 * δ ^ (2 * (m + 1)) := by -- Each term ≤ δ^{m+1}. have hterm : ∀ t ∈ T, ∏ k ∈ range (m + 1), e t k ≤ δ ^ (m + 1) := by intro t ht calc ∏ k ∈ range (m + 1), e t k ≤ ∏ _k ∈ range (m + 1), δ := Finset.prod_le_prod (fun k hk => hnn t ht k hk) (fun k hk => hle t ht k hk) _ = δ ^ (m + 1) := by rw [Finset.prod_const, Finset.card_range] -- Sum ≤ |T|·δ^{m+1}. have hsum_le : ∑ t ∈ T, ∏ k ∈ range (m + 1), e t k ≤ (T.card : ℝ) * δ ^ (m + 1) := by calc ∑ t ∈ T, ∏ k ∈ range (m + 1), e t k ≤ ∑ _t ∈ T, δ ^ (m + 1) := Finset.sum_le_sum hterm _ = (T.card : ℝ) * δ ^ (m + 1) := by rw [Finset.sum_const, nsmul_eq_mul] -- The sum is nonnegative (sum of products of nonnegatives). have hsum_nn : 0 ≤ ∑ t ∈ T, ∏ k ∈ range (m + 1), e t k := sum_nonneg (fun t ht => Finset.prod_nonneg (fun k hk => hnn t ht k hk)) -- Square the chain |R| ≤ sum ≤ |T|·δ^{m+1}. have hRabs : |R| ≤ (T.card : ℝ) * δ ^ (m + 1) := le_trans hbound hsum_le have hR2 : R ^ 2 ≤ ((T.card : ℝ) * δ ^ (m + 1)) ^ 2 := by rw [← sq_abs R] exact pow_le_pow_left₀ (abs_nonneg R) hRabs 2 calc R ^ 2 ≤ ((T.card : ℝ) * δ ^ (m + 1)) ^ 2 := hR2 _ = (T.card : ℝ) ^ 2 * δ ^ (2 * (m + 1)) := by rw [mul_pow, ← pow_mul, Nat.mul_comm (m + 1) 2]
ProjectedKernelTrace 3 core · 4 supporting Trace and degeneracy identities for projected HOIF kernels, showing that a rank-J projection kernel has L² energy equal to the projection dimension under inverse-Gram weighting. ★ projKernel_L2_eq_dim
The projected localized HOIF kernel: L²-energy equals the projection dimension
Trace and degeneracy identities for projected HOIF kernels, showing that a rank-J projection
kernel has L² energy equal to the projection dimension under inverse-Gram weighting.
The order-2 stochastic term of the order-m HOIF estimator is a degenerate U-statistic whose
kernel is the J-dimensional projection
g(x, y) = ⟨c(x), M c(y)⟩ = ∑_{k,l} c(x)_k · M_{kl} · c(y)_l,
where c : X → ℝ^J is the (bandwidth-localized, residual-weighted) basis evaluated at the
covariate and M is the projection weighting matrix. Writing Σ = 𝔼[c cᵀ] for the
second-moment (Gram) matrix, the L²-energy of the kernel factors, by the independence of the two
sample points, into
ζ = ∬ g² dP dP = ∑_{k,l,k',l'} M_{kl} M_{k'l'} Σ_{kk'} Σ_{ll'} = tr(Σ M Σ Mᵀ).
With the natural HOIF weighting M = Σ⁻¹ this collapses to ζ = J — the projected
degenerate kernel's L²-energy is exactly the projection dimension. In localized analyses this
identity is paired with the separate bandwidth scaling hypothesis ζ ≤ C·J/h² used by
Causalean.Stat.Nonparametric.HOIF.DegenerateUStatVariance
(Var = 2ζ/(n(n−1))), this is the source of the O(J/(nh)²) term in the HOIF projection risk.
projKernel_degen records only the one-sided degeneracy field
∫ g(x,·) dP = 0 when the basis coordinates are centered (∫ c_l dP = 0). It
does not by itself construct a DegenKernel, since that structure also carries
measurability, symmetry, and square-integrability requirements.
The second-moment (Gram) matrix of the basis c: Σ_{kl} = ∫ c(x)_k c(x)_l dP.
The projected HOIF kernel g(x,y) = ∑_{k,l} c(x)_k M_{kl} c(y)_l.
Definition (Lean source)
Projected degenerate-kernel L²-energy equals the dimension: ζ = J. For a feature map c into J-dimensional space, if every coordinate of c is square-integrable under P, the Gram matrix of c under P is invertible, and M is the inverse of that Gram matrix, then the squared L²(P⊗P)-norm of the HOIF projection kernel g(x,y) = ⟨c(x), M·c(y)⟩ equals the projection dimension J.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
projKernel_degentheorem — One-sided degeneracy of the projected kernel. If the basis coordinates are centered (∫ c_l dP = 0 for every l), then ∫ g(x, ·) dP = 0 for every x. This records the zero-integral field only; measurability, symmetry, and square-integrability are separate requirements for packaging the kernel as a degenerate U-statistic kernel.hypothesesconclusion∫ y, projKernel c M x y ∂P = 0Proof (Lean source)
theorem projKernel_degen (c : X → Fin J → ℝ) (M : Matrix (Fin J) (Fin J) ℝ) (hint : ∀ l, Integrable (fun x => c x l) P) (hzero : ∀ l, ∫ x, c x l ∂P = 0) (x : X) : ∫ y, projKernel c M x y ∂P = 0 := by unfold projKernel rw [integral_finset_sum] · refine Finset.sum_eq_zero (fun k _ => ?_) rw [integral_finset_sum] · refine Finset.sum_eq_zero (fun l _ => ?_) have : (fun y => c x k * M k l * c y l) = (fun y => (c x k * M k l) * c y l) := by funext y; ring rw [this, integral_const_mul, hzero l, mul_zero] · intro l _ exact ((hint l).const_mul (c x k * M k l)) · intro k _ apply integrable_finset_sum intro l _ exact ((hint l).const_mul (c x k * M k l)) -
projKernel_L2_eq_sumtheorem — L²-energy of the projected kernel (expanded form). By independence of the two sample points, the double integral of the squared projected kernel factors into Gram entries:hypothesesconclusion∫ p, (projKernel c M p.1 p.2) ^ 2 ∂(P.prod P)= ∑ k, ∑ l, ∑ k', ∑ l', M k l * M k' l' * gram c P k k' * gram c P l l'Proof (Lean source)
theorem projKernel_L2_eq_sum (c : X → Fin J → ℝ) (M : Matrix (Fin J) (Fin J) ℝ) (hc : ∀ k, MemLp (fun x => c x k) 2 P) : ∫ p, (projKernel c M p.1 p.2) ^ 2 ∂(P.prod P) = ∑ k, ∑ l, ∑ k', ∑ l', M k l * M k' l' * gram c P k k' * gram c P l l' := by have hsq : ∀ p : X × X, (projKernel c M p.1 p.2) ^ 2 = ∑ k, ∑ l, ∑ k', ∑ l', (c p.1 k * M k l * c p.2 l) * (c p.1 k' * M k' l' * c p.2 l') := by intro p unfold projKernel rw [sq, Finset.sum_mul_sum] rw [Finset.sum_congr rfl (fun k _ => Finset.sum_congr rfl (fun k' _ => by rw [Finset.sum_mul_sum]))] rw [Finset.sum_congr rfl (fun k _ => Finset.sum_comm)] have hInt : ∀ k l k' l' : Fin J, Integrable (fun p : X × X => (c p.1 k * M k l * c p.2 l) * (c p.1 k' * M k' l' * c p.2 l')) (P.prod P) := by intro k l k' l' have hX : Integrable (fun x => c x k * c x k') P := (hc k).integrable_mul (hc k') have hY : Integrable (fun y => c y l * c y l') P := (hc l).integrable_mul (hc l') have hprod : Integrable (fun p : X × X => (c p.1 k * c p.1 k') * (c p.2 l * c p.2 l')) (P.prod P) := hX.mul_prod hY have hEq : (fun p : X × X => (c p.1 k * M k l * c p.2 l) * (c p.1 k' * M k' l' * c p.2 l')) = (fun p : X × X => (M k l * M k' l') * ((c p.1 k * c p.1 k') * (c p.2 l * c p.2 l'))) := by funext p ring rw [hEq] exact hprod.const_mul (M k l * M k' l') have hEval : ∀ k l k' l' : Fin J, ∫ p, (c p.1 k * M k l * c p.2 l) * (c p.1 k' * M k' l' * c p.2 l') ∂(P.prod P) = M k l * M k' l' * gram c P k k' * gram c P l l' := by intro k l k' l' have hEq : (fun p : X × X => (c p.1 k * M k l * c p.2 l) * (c p.1 k' * M k' l' * c p.2 l')) = (fun p : X × X => (M k l * M k' l') * ((c p.1 k * c p.1 k') * (c p.2 l * c p.2 l'))) := by funext p ring rw [hEq, integral_const_mul, integral_prod_mul (μ := P) (ν := P) (f := fun x => c x k * c x k') (g := fun y => c y l * c y l')] simp only [gram, Matrix.of_apply] ring simp_rw [hsq] rw [integral_finset_sum] · apply Finset.sum_congr rfl intro k _ rw [integral_finset_sum] · apply Finset.sum_congr rfl intro l _ rw [integral_finset_sum] · apply Finset.sum_congr rfl intro k' _ rw [integral_finset_sum] · apply Finset.sum_congr rfl intro l' _ exact hEval k l k' l' · intro l' _ exact hInt k l k' l' · intro k' _ apply integrable_finset_sum intro l' _ exact hInt k l k' l' · intro l _ apply integrable_finset_sum intro k' _ apply integrable_finset_sum intro l' _ exact hInt k l k' l' · intro k _ apply integrable_finset_sum intro l _ apply integrable_finset_sum intro k' _ apply integrable_finset_sum intro l' _ exact hInt k l k' l' -
sum_collapse_dimtheorem — The 4-fold Gram sum collapses to the projection dimension. With the HOIF weighting M = Σ⁻¹ (Σ = gram c P invertible), the expanded L²-energy equals the projection dimension J, because Σ Σ⁻¹ = Σ⁻¹ Σ = 1.hypothesesconclusion∑ k, ∑ l, ∑ k', ∑ l', M k l * M k' l' * S k k' * S l l' = (J : ℝ)Proof (Lean source)
theorem sum_collapse_dim (M S : Matrix (Fin J) (Fin J) ℝ) (hu : IsUnit S.det) (hM : M = S⁻¹) : ∑ k, ∑ l, ∑ k', ∑ l', M k l * M k' l' * S k k' * S l l' = (J : ℝ) := by have hSM : S * M = 1 := by rw [hM]; exact Matrix.mul_nonsing_inv S hu have hMS : M * S = 1 := by rw [hM]; exact Matrix.nonsing_inv_mul S hu -- For fixed k,l, the inner double sum collapses to `M k l * S l k`. have key : ∀ k l : Fin J, (∑ k', ∑ l', M k l * M k' l' * S k k' * S l l') = M k l * S l k := by intro k l rw [Finset.sum_comm] -- ∑ l', ∑ k', M k l * M k' l' * S k k' * S l l' have hinner : ∀ l' : Fin J, (∑ k', M k l * M k' l' * S k k' * S l l') = M k l * S l l' * (S * M) k l' := by intro l' rw [Matrix.mul_apply, Finset.mul_sum] exact Finset.sum_congr rfl (fun k' _ => by ring) rw [Finset.sum_congr rfl (fun l' _ => hinner l'), hSM] simp only [Matrix.one_apply, mul_ite, mul_one, mul_zero] rw [Finset.sum_ite_eq univ k (fun l' => M k l * S l l')] simp rw [Finset.sum_congr rfl (fun k _ => Finset.sum_congr rfl (fun l _ => key k l))] -- ∑ k, ∑ l, M k l * S l k = ∑ k, (M*S) k k = ∑ k, 1 = J have hrow : ∀ k : Fin J, (∑ l, M k l * S l k) = (M * S) k k := fun k => (Matrix.mul_apply).symm rw [Finset.sum_congr rfl (fun k _ => hrow k), hMS] simp only [Matrix.one_apply_eq] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one]
ProjectionRisk 1 core · 0 supporting Risk decompositions for localized HOIF estimators, combining first-order variance, projection bias, degenerate U-statistic variance, and higher-order product remainders. ★ hoif_projection_risk_bound
Order-m HOIF projection-risk decomposition (capstone)
Risk decompositions for localized HOIF estimators, combining first-order variance, projection bias, degenerate U-statistic variance, and higher-order product remainders.
The mean-squared error of an order-m HOIF estimator, using a J-dimensional projection space and
bandwidth h, splits into three statistically distinct pieces plus the higher-order estimation
remainder:
* localized first-order variance V₁ = O((nh)^{-1}) — the AIPW/plug-in stochastic term;
* projection product bias² B² = O(J^{-4s/d}) — the squared series/sieve approximation error of
the J-term projection (Causalean.Stat.Nonparametric.SeriesSieve);
* degenerate U-statistic variance V₂ = Var[Uₙ] ≤ 4C·J/(nh)² — the second-order projected
stochastic term, controlled by HOIF.DegenerateUStatVariance from the supplied localized
L²-energy hypothesis ζ ≤ C·J/h² (the sibling HOIF.ProjectedKernelTrace proves the inverse-Gram
identity ζ = J in the unlocalized case);
* order-m product remainder R² ≤ |T|²·δ^{2(m+1)} — the HOIF estimation bias, a finite sum of
products of m+1 nuisance L²-errors (HOIF.ProductRemainder), made o(ρ_n) by choosing m
large enough (hoif_order_choice_negligible).
hoif_projection_risk_bound assembles these into a single explicit upper bound on the risk: it
takes the bias-variance decomposition as input and discharges the second-order variance term and
the product remainder from the Causalean theorems, leaving only V₁ and B² (supplied by the
sibling local-polynomial / series-sieve substrates) as hypotheses.
Order-m HOIF projection-risk bound. For an i.i.d. sample S and a projection kernel g, suppose g is symmetric, square-integrable, and doubly degenerate, the sample size n is at least 2, and the bandwidth h is positive, the projection dimension J and trace constant C are nonnegative, and the kernel's L²-energy ζ obeys the trace bound ζ ≤ C·J/h². Suppose further that the first-order variance V1 obeys the rate V1 ≤ Cv1/(nh) and the projection bias² Bsq obeys the rate Bsq ≤ Cb·J^{-4s/d}, and that the order-m estimation remainder R is controlled, over a finite index set T, by a sum of products of m+1 nuisance-error factors: every such factor is nonnegative, every factor is at most the largest nuisance error δ, and the absolute value of R is bounded by that sum of products. If, finally, the estimator's risk decomposes as risk ≤ V1 + Bsq + Var[Uₙ] + R², then the risk is bounded by the explicit sum Cv1/(nh) + Cb·J^{-4s/d} + 4C·J/(nh)² + |T|²·δ^{2(m+1)}.