Stat.Nonparametric.HigherOrderInfluence
Two ingredients of the risk analysis of second-order U-statistic corrections built from a J-dimensional projection.
DegenerateUStatVariance 2 core · 2 supporting Variance bounds for degenerate rank-2 U-statistic terms used in higher-order influence function (HOIF) projection-kernel risk algebra. ★ 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 used in higher-order influence function (HOIF) projection-kernel risk algebra.
For a degenerate order-2 U-statistic whose kernel is a J-dimensional,
bandwidth-h localized projection, the
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
degenerate U-statistic variance bound
Var[Uₙ] ≤ 4C·J / (nh)²,
the O(J/(nh)²) term of the projection-risk decomposition. The sibling
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)
Projection-kernel 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).hypothesesΩ :sharedType u_1X :sharedType u_2g :sharedX → X → ℝS :IIDSample Ω X μ Phg :DegenKernel P gn :ℕhn :2 ≤ nconclusionMemLp (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 — A degenerate order-2 U-statistic has mean zero.hypothesesΩ :sharedType u_1X :sharedType u_2g :sharedX → X → ℝS :IIDSample Ω X μ Phg :DegenKernel P gn :ℕhn :2 ≤ nconclusion∫ ω, 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 This file supplies the product-remainder algebra for a higher-order influence function (HOIF) estimator whose remainder is a *finite sum of products of m+1 nonnegative factors*. ★ const_mul_natCast_rpow_sub_tendsto_zero
Finite product-remainder algebra
This file supplies the product-remainder algebra for a higher-order influence function (HOIF)
estimator whose remainder is a finite sum of products of m+1 nonnegative factors.
Writing δ for the largest factor, 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)}.
The final theorem is a separate generic power-law fact: K n^{κ-a} tends to zero whenever
κ < a. Connecting its exponent a to an order m, nuisance rates, or a product remainder
requires an additional argument not supplied here.
This file is purely elementary (finite products of bounded reals + a power-law limit); it carries no measure theory and is a reusable risk-algebra building block.
A negative power vanishes asymptotically. For a real constant K and real exponents a and κ, if κ < a, then K n^{κ-a} tends to zero as n tends to infinity. The statement does not choose a remainder order or connect a to the product-remainder bound above.
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 factor of a remainder term is nonnegative and bounded by the largest factor δ; 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] -
productRemainder_sq_letheorem — Squared finite-product remainder bound. The order-m 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 productRemainder_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 := Finset.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 centering identities for the projected kernels used by higher-order influence function (HOIF) estimators, showing that a rank-J projection kernel has L² energy equal to the projection dimension under inverse-Gr ★ projKernel_L2_eq_dim
Projected-kernel L²-energy equals the projection dimension
Trace and centering identities for the projected kernels used by higher-order influence
function (HOIF) estimators, showing that a rank-J projection kernel has L² energy equal to
the projection dimension under inverse-Gram weighting.
The rank-2 projection kernel associated with the J-dimensional projection is
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 inverse-Gram weighting M = Σ⁻¹ this collapses to ζ = J — the projection
kernel's L²-energy is exactly the projection dimension. In applications where degeneracy is
established separately, this identity can be paired with the bandwidth scaling hypothesis
ζ ≤ C·J/h² used by
Causalean.Stat.Nonparametric.HigherOrderInfluence.DegenerateUStatVariance
(Var = 2ζ/(n(n−1))) as an input to a projection-kernel risk bound.
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.
For a measurable sample space, a nonnegative integer giving the number of basis functions, a real-valued basis evaluated at each sample point, and a measure on that sample space, the second-moment, or Gram, matrix of the basis has entry equal to .
For a sample space, a nonnegative integer giving the number of basis functions, a real-valued basis evaluated at each sample point, and a real square weighting matrix indexed by those basis functions, the projected higher-order influence-function kernel assigns to two sample points the value .
Projection-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 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)
-
gram_symmtheorem — The Gram matrix is symmetric.hypothesesconclusion(gram c P)ᵀ = gram c P -
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.hypothesesJ :sharedℕc :X → Fin J → ℝhint :∀ l, Integrable (fun x => c x l) Phzero :∀ l, ∫ x, c x l ∂P = 0x :Xconclusion∫ 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 inverse-Gram 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 Algebraic risk bounds for higher-order influence function (HOIF) calculations, combining assumed first-order variance and projection bias with proved degenerate U-statistic variance and finite-product remainder bounds. ★ projectionKernel_risk_bound
Projection-kernel risk-bound algebra
Algebraic risk bounds for higher-order influence function (HOIF) calculations, combining assumed first-order variance and projection bias with proved degenerate U-statistic variance and finite-product remainder bounds.
Given a risk decomposition with a J-dimensional projection space and bandwidth h, this module
combines its four component bounds:
* localized first-order variance V₁ = O((nh)^{-1}) — an assumed 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 HigherOrderInfluence.DegenerateUStatVariance from the supplied localized
L²-energy hypothesis ζ ≤ C·J/h² (the sibling HigherOrderInfluence.ProjectedKernelTrace proves the inverse-Gram
identity ζ = J in the unlocalized case);
* order-m product remainder R² ≤ |T|²·δ^{2(m+1)} — a finite sum of products of
m+1 bounded factors (HigherOrderInfluence.ProductRemainder). A separate theorem,
const_mul_natCast_rpow_sub_tendsto_zero proves only a generic negative-power limit; relating
its exponent comparison to m and nuisance rates requires an additional argument.
projectionKernel_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.
Conditional projection-kernel risk algebra. For an i.i.d. sample and a symmetric, square-integrable, doubly degenerate kernel, sample size at least two, positive bandwidth, and nonnegative projection dimension and trace constant, this theorem assumes the estimator's risk decomposition into first-order variance, projection bias, degenerate U-statistic variance, and squared remainder, as well as the stated bounds on the first-order variance, projection bias, kernel energy, and remainder; it only combines those inputs into the displayed risk bound. It is not a theorem deriving a higher-order influence function (HOIF) risk decomposition or its first-order and approximation terms.