Stat.Nonparametric.LocalPoly
Finite-sample analysis of the degree-p local-polynomial estimator at an interior point.
EstimatorRisk 12 core · 12 supporting · 6 submodules Given the design, the degree-p local-polynomial intercept of a β-Hölder regression function has bias at most Cbias · h^β and stochastic L² error at most Cvar · (Nh)^(−1/2), with the leverage constants expressed through l RandomDesignRate 30 core · 44 supporting · 7 submodules For independent pairs (X_i, Y_i) with a design density bounded above and below by positive constants near an interior point x₀, the degree-p local-polynomial estimator of the regression function at x₀, clipped to [−M, M] Rate 5 core · 7 supporting · 2 submodules One-sided leverage upper bounds for the local-polynomial design inverse, derived from deterministic entrywise perturbation and population scaling hypotheses.
Weights 3 core · 5 supporting Equivalent-kernel weights for local-polynomial weighted least squares and their polynomial-reproduction property. ★ equivKernelWeight_reproduces
Polynomial reproduction of the local-polynomial equivalent kernel
Equivalent-kernel weights for local-polynomial weighted least squares and their polynomial-reproduction property.
The degree-p local-polynomial weighted least-squares fit at a point has, when the
weighted design moment matrix is invertible, an explicit equivalent-kernel weight
Sᵢ = ∑ₖ (M⁻¹)₀ₖ wᵢ xᵢᵏ, where M_{jk} = ∑ᵢ wᵢ xᵢʲ xᵢᵏ is the weighted design moment
matrix (xᵢ = aᵢ − t). This file proves the defining polynomial-reproduction
property of these weights:
∑ᵢ Sᵢ xᵢᵐ = [m = 0] for m ≤ p,
i.e. the equivalent kernel reproduces polynomials up to degree p. This is exactly the
hypothesis hrep consumed by linearSmoother_bias_of_reproduces, so it converts the
abstract bias bound into the concrete local-polynomial bias estimate. The reproduction is
pure linear algebra: ∑ᵢ Sᵢ xᵢᵐ = ∑ₖ (M⁻¹)₀ₖ M_{km} = (M⁻¹ M)₀ₘ = I₀ₘ (Fan–Gijbels 1996
§3.1).
def designMatrix reviewed
⚑ flagged
Causalean.Stat.Nonparametric
Given a nonnegative polynomial degree, a sample indexed by a nonnegative number of observations, real-valued centered design coordinates for those observations, and real-valued observation weights, the weighted design moment matrix is the matrix whose entry is .
def equivKernelWeight reviewed
⚑ flagged
Causalean.Stat.Nonparametric
Given a nonnegative polynomial degree, a sample indexed by a nonnegative number of observations, real-valued centered design coordinates, real-valued observation weights, and an observation in that sample, the local-polynomial equivalent-kernel weight for that observation is , where is the corresponding weighted design moment matrix. This weight extracts the fitted intercept: the degree- weighted least-squares intercept is the outcome-weighted sum of these weights.
Definition (Lean source)
parameters
def
equivKernelWeight p x w i :
ℝ
given by
∑ k, (designMatrix p x w)⁻¹ 0 k * (w i * x i ^ (k : ℕ))
theorem equivKernelWeight_reproduces reviewed
⚑ flagged
Causalean.Stat.Nonparametric
Polynomial reproduction of the equivalent kernel. If the weighted design moment matrix is invertible, then the local-polynomial equivalent-kernel weights reproduce polynomials up to degree p: ∑ᵢ Sᵢ xᵢᵐ = [m = 0] for every m ≤ p. This discharges the reproduction hypothesis of linearSmoother_bias_of_reproduces.
Formal statement
hypotheses
conclusion
(∑ i, equivKernelWeight p x w i * x i ^ m) = if m = 0 then 1 else 0
Proof (Lean source)
theorem equivKernelWeight_reproduces {N p : ℕ} {x w : Fin N → ℝ}
(hM : IsUnit (designMatrix p x w).det) :
∀ m : ℕ, m ≤ p →
(∑ i, equivKernelWeight p x w i * x i ^ m) = if m = 0 then 1 else 0 := by
intro m hm
let M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := designMatrix p x w
let m' : Fin (p + 1) := ⟨m, Nat.lt_succ_of_le hm⟩
calc
(∑ i, equivKernelWeight p x w i * x i ^ m)
= ∑ i, (∑ k, M⁻¹ 0 k * (w i * x i ^ (k : ℕ))) * x i ^ m := by
simp only [equivKernelWeight, M]
_ = ∑ k, M⁻¹ 0 k * M k m' := by
simp only [Finset.sum_mul]
rw [Finset.sum_comm]
apply Finset.sum_congr rfl
intro k hk
calc
(∑ i, M⁻¹ 0 k * (w i * x i ^ (k : ℕ)) * x i ^ m)
= ∑ i, M⁻¹ 0 k * (w i * x i ^ (k : ℕ) * x i ^ m) := by
apply Finset.sum_congr rfl
intro i hi
ring
_ = M⁻¹ 0 k * (∑ i, w i * x i ^ (k : ℕ) * x i ^ m) := by
rw [Finset.mul_sum]
_ = M⁻¹ 0 k * M k m' := by
simp only [M, m', designMatrix]
_ = (M⁻¹ * M) 0 m' := by
rw [Matrix.mul_apply]
_ = (1 : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ) 0 m' := by
rw [Matrix.nonsing_inv_mul]
simpa only [M] using hM
_ = if m = 0 then 1 else 0 := by
by_cases hm0 : m = 0
· subst m
have hfin : (0 : Fin (p + 1)) = m' := by
ext
simp only [Fin.val_zero, m']
simp only [Matrix.one_apply, hfin, ↓reduceIte]
· simp only [Matrix.one_apply, hm0, ↓reduceIte]
rw [if_neg]
intro h
apply hm0
have hval := congrArg val h
simpa only [Fin.val_zero, m', Fin.val_mk] using hval.symm
5 supporting declarations (lemmas, instances)
-
wls_normal_equationstheorem — Normal equations for weighted polynomial least squares (the Vandermonde design Φᵢⱼ = xᵢʲ). The weighted least-squares minimizer of ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ xᵢʲ)² has residual orthogonal to every design monomial: ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ xᵢʲ) xᵢᵏ = 0.hypotheseshw :∀ i, 0 ≤ w ihmin :∀ c' : Fin (p + 1) → ℝ,(∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) ^ 2)≤ ∑ i, w i * (Y i - ∑ j, c' j * x i ^ (j : ℕ)) ^ 2k :Fin (p + 1)conclusion∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) * x i ^ (k : ℕ) = 0Proof (Lean source)
theorem wls_normal_equations {N p : ℕ} {x w Y : Fin N → ℝ} {c : Fin (p + 1) → ℝ} (hw : ∀ i, 0 ≤ w i) (hmin : ∀ c' : Fin (p + 1) → ℝ, (∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) ^ 2) ≤ ∑ i, w i * (Y i - ∑ j, c' j * x i ^ (j : ℕ)) ^ 2) : ∀ k : Fin (p + 1), ∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) * x i ^ (k : ℕ) = 0 := by have hmin' : ∀ c' : Fin (p + 1) → ℝ, lstsqObjective (fun (i : Fin N) (j : Fin (p + 1)) => x i ^ (j : ℕ)) w Y c ≤ lstsqObjective (fun (i : Fin N) (j : Fin (p + 1)) => x i ^ (j : ℕ)) w Y c' := by intro c' simpa [lstsqObjective, lstsqResidual] using hmin c' intro k have hk := lstsq_normal_equations (Φ := fun (i : Fin N) (j : Fin (p + 1)) => x i ^ (j : ℕ)) hw hmin' k simpa [lstsqResidual] using hk -
wls_intercept_eq_equivKernelSmoothertheorem — The local-polynomial WLS intercept is the equivalent-kernel linear smoother. If the weighted design moment matrix is invertible and c minimizes the weighted sum of squares, then the fitted intercept c 0 equals the linear smoother ∑ᵢ Sᵢ Yᵢ with the equivalent-kernel weights Sᵢ = equivKernelWeight p x w i. Combined with equivKernelWeight_reproduces and linearSmoother_bias_of_reproduces, this yields the interior local-polynomial bias estimate.hypotheseshw :∀ i, 0 ≤ w ihM :IsUnit (designMatrix p x w).dethmin :∀ c' : Fin (p + 1) → ℝ,(∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) ^ 2)≤ ∑ i, w i * (Y i - ∑ j, c' j * x i ^ (j : ℕ)) ^ 2conclusionc 0 = ∑ i, equivKernelWeight p x w i * Y iProof (Lean source)
theorem wls_intercept_eq_equivKernelSmoother {N p : ℕ} {x w Y : Fin N → ℝ} {c : Fin (p + 1) → ℝ} (hw : ∀ i, 0 ≤ w i) (hM : IsUnit (designMatrix p x w).det) (hmin : ∀ c' : Fin (p + 1) → ℝ, (∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) ^ 2) ≤ ∑ i, w i * (Y i - ∑ j, c' j * x i ^ (j : ℕ)) ^ 2) : c 0 = ∑ i, equivKernelWeight p x w i * Y i := by let M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := designMatrix p x w let b : Fin (p + 1) → ℝ := fun k => ∑ i, w i * x i ^ (k : ℕ) * Y i have hnormal_scalar : ∀ k : Fin (p + 1), b k = ∑ i, w i * x i ^ (k : ℕ) * (∑ j, c j * x i ^ (j : ℕ)) := by intro k have hne := wls_normal_equations (x := x) (w := w) (Y := Y) (c := c) hw hmin k have hdiff : b k - ∑ i, w i * x i ^ (k : ℕ) * (∑ j, c j * x i ^ (j : ℕ)) = 0 := by rw [← Finset.sum_sub_distrib] calc (∑ i, (w i * x i ^ (k : ℕ) * Y i - w i * x i ^ (k : ℕ) * (∑ j, c j * x i ^ (j : ℕ)))) = ∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) * x i ^ (k : ℕ) := by apply Finset.sum_congr rfl intro i hi ring _ = 0 := hne exact sub_eq_zero.mp hdiff have hnormal : M *ᵥ c = b := by funext k calc (M *ᵥ c) k = ∑ j, M k j * c j := by simp [mulVec, dotProduct] _ = ∑ j : Fin (p + 1), (∑ i, w i * x i ^ (k : ℕ) * x i ^ (j : ℕ)) * c j := by simp only [M, designMatrix] _ = ∑ i, w i * x i ^ (k : ℕ) * (∑ j : Fin (p + 1), c j * x i ^ (j : ℕ)) := by simp_rw [Finset.sum_mul] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro i hi rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring _ = b k := (hnormal_scalar k).symm have hMinv : M⁻¹ * M = 1 := by rw [Matrix.nonsing_inv_mul] simpa only [M] using hM have hc_eq : c = M⁻¹ *ᵥ b := by calc c = (1 : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ) *ᵥ c := by simp _ = (M⁻¹ * M) *ᵥ c := by simp only [hMinv] _ = M⁻¹ *ᵥ (M *ᵥ c) := by rw [Matrix.mulVec_mulVec] _ = M⁻¹ *ᵥ b := by rw [hnormal] calc c 0 = (M⁻¹ *ᵥ b) 0 := by rw [hc_eq] _ = ∑ k, M⁻¹ 0 k * b k := by simp [mulVec, dotProduct] _ = ∑ k, M⁻¹ 0 k * (∑ i, w i * x i ^ (k : ℕ) * Y i) := by simp only [b] _ = ∑ i, (∑ k, M⁻¹ 0 k * (w i * x i ^ (k : ℕ))) * Y i := by simp_rw [Finset.mul_sum] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro i hi rw [Finset.sum_mul] apply Finset.sum_congr rfl intro k hk ring _ = ∑ i, equivKernelWeight p x w i * Y i := by simp only [equivKernelWeight, M] -
equivKernel_weighted_sq_sumtheorem — Leverage identity for the equivalent kernel. Writing the equivalent-kernel weight as Sᵢ = wᵢ · gᵢ with gᵢ = ∑ₖ (M⁻¹)₀ₖ xᵢᵏ the unweighted kernel, the weighted leverage equals the (0,0) entry of the inverse moment matrix: ∑ᵢ wᵢ gᵢ² = (M⁻¹)₀₀. (Algebraically e₀ᵀ M⁻¹ M M⁻¹ e₀ = e₀ᵀ M⁻¹ e₀.)hypothesesN p :ℕFin N → ℝhM :IsUnit (designMatrix p x w).detconclusion(∑ i, w i * (∑ k, (designMatrix p x w)⁻¹ 0 k * x i ^ (k : ℕ)) ^ 2)= (designMatrix p x w)⁻¹ 0 0Proof (Lean source)
theorem equivKernel_weighted_sq_sum {N p : ℕ} {x w : Fin N → ℝ} (hM : IsUnit (designMatrix p x w).det) : (∑ i, w i * (∑ k, (designMatrix p x w)⁻¹ 0 k * x i ^ (k : ℕ)) ^ 2) = (designMatrix p x w)⁻¹ 0 0 := by let M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := designMatrix p x w have hMinv : M⁻¹ * M = 1 := by rw [Matrix.nonsing_inv_mul] simpa only [M] using hM calc (∑ i, w i * (∑ k, (designMatrix p x w)⁻¹ 0 k * x i ^ (k : ℕ)) ^ 2) = ∑ i, w i * ((∑ k, M⁻¹ 0 k * x i ^ (k : ℕ)) * (∑ l, M⁻¹ 0 l * x i ^ (l : ℕ))) := by simp only [M] apply Finset.sum_congr rfl intro i hi rw [sq] _ = ∑ k, ∑ l, M⁻¹ 0 k * M⁻¹ 0 l * M k l := by calc (∑ i, w i * ((∑ k, M⁻¹ 0 k * x i ^ (k : ℕ)) * (∑ l, M⁻¹ 0 l * x i ^ (l : ℕ)))) = ∑ i, ∑ k, ∑ l, w i * ((M⁻¹ 0 k * x i ^ (k : ℕ)) * (M⁻¹ 0 l * x i ^ (l : ℕ))) := by apply Finset.sum_congr rfl intro i hi rw [Finset.sum_mul_sum] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k hk rw [Finset.mul_sum] _ = ∑ k, ∑ i, ∑ l, w i * ((M⁻¹ 0 k * x i ^ (k : ℕ)) * (M⁻¹ 0 l * x i ^ (l : ℕ))) := by rw [Finset.sum_comm] _ = ∑ k, ∑ l, ∑ i, w i * ((M⁻¹ 0 k * x i ^ (k : ℕ)) * (M⁻¹ 0 l * x i ^ (l : ℕ))) := by apply Finset.sum_congr rfl intro k hk rw [Finset.sum_comm] _ = ∑ k, ∑ l, M⁻¹ 0 k * M⁻¹ 0 l * M k l := by apply Finset.sum_congr rfl intro k hk apply Finset.sum_congr rfl intro l hl calc (∑ i, w i * ((M⁻¹ 0 k * x i ^ (k : ℕ)) * (M⁻¹ 0 l * x i ^ (l : ℕ)))) = ∑ i, (M⁻¹ 0 k * M⁻¹ 0 l) * (w i * x i ^ (k : ℕ) * x i ^ (l : ℕ)) := by apply Finset.sum_congr rfl intro i hi ring _ = (M⁻¹ 0 k * M⁻¹ 0 l) * (∑ i, w i * x i ^ (k : ℕ) * x i ^ (l : ℕ)) := by rw [Finset.mul_sum] _ = M⁻¹ 0 k * M⁻¹ 0 l * M k l := by simp only [M, designMatrix] _ = ∑ l, (∑ k, M⁻¹ 0 k * M k l) * M⁻¹ 0 l := by rw [Finset.sum_comm] apply Finset.sum_congr rfl intro l hl rw [Finset.sum_mul] apply Finset.sum_congr rfl intro k hk ring _ = ∑ l, (M⁻¹ * M) 0 l * M⁻¹ 0 l := by apply Finset.sum_congr rfl intro l hl rw [Matrix.mul_apply] _ = ∑ l, (1 : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ) 0 l * M⁻¹ 0 l := by simp only [hMinv] _ = M⁻¹ 0 0 := by simp [Matrix.one_apply] -
equivKernelWeight_sq_sum_letheorem — Leverage bound for the equivalent kernel. With nonnegative weights bounded by W, the local-polynomial equivalent-kernel weights satisfy ∑ᵢ Sᵢ² ≤ W · (M⁻¹)₀₀. Combined with linearSmoother_variance_le, this reduces the interior O((Nh)^{−1/2}) stochastic-error rate to the single concentration bound (M⁻¹)₀₀ = O(1/(Nh)).hypothesesconclusion(∑ i, equivKernelWeight p x w i ^ 2) ≤ W * (designMatrix p x w)⁻¹ 0 0Proof (Lean source)
theorem equivKernelWeight_sq_sum_le {N p : ℕ} {x w : Fin N → ℝ} {W : ℝ} (hM : IsUnit (designMatrix p x w).det) (hw : ∀ i, 0 ≤ w i) (hwW : ∀ i, w i ≤ W) : (∑ i, equivKernelWeight p x w i ^ 2) ≤ W * (designMatrix p x w)⁻¹ 0 0 := by let M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := designMatrix p x w let g : Fin N → ℝ := fun i => ∑ k, M⁻¹ 0 k * x i ^ (k : ℕ) have hfactor : ∀ i, equivKernelWeight p x w i = w i * g i := by intro i calc equivKernelWeight p x w i = ∑ k, M⁻¹ 0 k * (w i * x i ^ (k : ℕ)) := by simp only [equivKernelWeight, M] _ = ∑ k, w i * (M⁻¹ 0 k * x i ^ (k : ℕ)) := by apply Finset.sum_congr rfl intro k hk ring _ = w i * g i := by simp only [g] rw [Finset.mul_sum] have hterm : ∀ i, equivKernelWeight p x w i ^ 2 ≤ W * (w i * g i ^ 2) := by intro i have hsq_le : w i ^ 2 ≤ W * w i := by nlinarith [hw i, hwW i] have hg_nonneg : 0 ≤ g i ^ 2 := sq_nonneg (g i) calc equivKernelWeight p x w i ^ 2 = (w i * g i) ^ 2 := by rw [hfactor i] _ = w i ^ 2 * g i ^ 2 := by ring _ ≤ (W * w i) * g i ^ 2 := by exact mul_le_mul_of_nonneg_right hsq_le hg_nonneg _ = W * (w i * g i ^ 2) := by ring have hweighted : (∑ i, w i * g i ^ 2) = M⁻¹ 0 0 := by simpa only [g, M] using (equivKernel_weighted_sq_sum (N := N) (p := p) (x := x) (w := w) hM) calc (∑ i, equivKernelWeight p x w i ^ 2) ≤ ∑ i, W * (w i * g i ^ 2) := by exact Finset.sum_le_sum (fun i hi => hterm i) _ = W * (∑ i, w i * g i ^ 2) := by rw [Finset.mul_sum] _ = W * M⁻¹ 0 0 := by rw [hweighted] _ = W * (designMatrix p x w)⁻¹ 0 0 := by simp only [M] -
equivKernelWeight_abs_sum_sq_letheorem — Cauchy–Schwarz leverage bound for the equivalent kernel. The ℓ¹ leverage of the equivalent-kernel weights is controlled by the product of the (0,0) entries of the design moment matrix and its inverse: (∑ᵢ |Sᵢ|)² ≤ M₀₀ · (M⁻¹)₀₀, where M₀₀ = ∑ᵢ wᵢ is the total weight. (Cauchy–Schwarz on Sᵢ = wᵢ gᵢ split as √wᵢ · √wᵢ gᵢ, using ∑ᵢ wᵢ gᵢ² = (M⁻¹)₀₀.) Together with equivKernelWeight_sq_sum_le this reduces *both* the bias leverage ∑ᵢ|Sᵢ| and the variance leverage ∑ᵢ Sᵢ² to the design quantities M₀₀ and (M⁻¹)₀₀.hypothesesconclusion(∑ i, |equivKernelWeight p x w i|) ^ 2≤ (designMatrix p x w) 0 0 * (designMatrix p x w)⁻¹ 0 0Proof (Lean source)
theorem equivKernelWeight_abs_sum_sq_le {N p : ℕ} {x w : Fin N → ℝ} (hM : IsUnit (designMatrix p x w).det) (hw : ∀ i, 0 ≤ w i) : (∑ i, |equivKernelWeight p x w i|) ^ 2 ≤ (designMatrix p x w) 0 0 * (designMatrix p x w)⁻¹ 0 0 := by let M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := designMatrix p x w let g : Fin N → ℝ := fun i => ∑ k, M⁻¹ 0 k * x i ^ (k : ℕ) have hfactor : ∀ i, equivKernelWeight p x w i = w i * g i := by intro i calc equivKernelWeight p x w i = ∑ k, M⁻¹ 0 k * (w i * x i ^ (k : ℕ)) := by simp only [equivKernelWeight, M] _ = ∑ k, w i * (M⁻¹ 0 k * x i ^ (k : ℕ)) := by apply Finset.sum_congr rfl intro k hk ring _ = w i * g i := by simp only [g] rw [Finset.mul_sum] have habs : ∀ i, |equivKernelWeight p x w i| = w i * |g i| := by intro i rw [hfactor i, abs_mul, abs_of_nonneg (hw i)] have hM00 : M 0 0 = ∑ i, w i := by simp [M, designMatrix] have hweighted : (∑ i, w i * g i ^ 2) = M⁻¹ 0 0 := by simpa only [g, M] using (equivKernel_weighted_sq_sum (N := N) (p := p) (x := x) (w := w) hM) have hleft : (∑ i, sqrt (w i) * (sqrt (w i) * |g i|)) = ∑ i, |equivKernelWeight p x w i| := by apply Finset.sum_congr rfl intro i hi calc sqrt (w i) * (sqrt (w i) * |g i|) = (sqrt (w i) * sqrt (w i)) * |g i| := by ring _ = w i * |g i| := by rw [Real.mul_self_sqrt (hw i)] _ = |equivKernelWeight p x w i| := (habs i).symm have hfirst : (∑ i, sqrt (w i) ^ 2) = M 0 0 := by calc (∑ i, sqrt (w i) ^ 2) = ∑ i, w i := by apply Finset.sum_congr rfl intro i hi exact Real.sq_sqrt (hw i) _ = M 0 0 := hM00.symm have hsecond : (∑ i, (sqrt (w i) * |g i|) ^ 2) = M⁻¹ 0 0 := by calc (∑ i, (sqrt (w i) * |g i|) ^ 2) = ∑ i, w i * g i ^ 2 := by apply Finset.sum_congr rfl intro i hi calc (sqrt (w i) * |g i|) ^ 2 = sqrt (w i) ^ 2 * |g i| ^ 2 := by ring _ = w i * g i ^ 2 := by rw [Real.sq_sqrt (hw i), sq_abs] _ = M⁻¹ 0 0 := hweighted have hcs := Finset.sum_mul_sq_le_sq_mul_sq univ (fun i : Fin N => sqrt (w i)) (fun i : Fin N => sqrt (w i) * |g i|) rw [hleft, hfirst, hsecond] at hcs simpa only [M] using hcs
Bias 1 core · 1 supporting Bias bounds for interior local-polynomial regression, combining equivalent-kernel polynomial reproduction with the Hölder–Taylor remainder. ★ localPoly_intercept_bias
Interior local-polynomial bias O(h^β)
Bias bounds for interior local-polynomial regression, combining equivalent-kernel polynomial reproduction with the Hölder–Taylor remainder.
This file assembles the deterministic bias estimate for the interior local-polynomial regression estimator (Fan–Gijbels 1996 §3.1; Tsybakov 2009 Ch. 1) from its building blocks:
* wls_intercept_eq_equivKernelSmoother — the fitted intercept is the equivalent-kernel
linear smoother c₀ = ∑ᵢ Sᵢ f(aᵢ);
* equivKernelWeight_reproduces — those weights reproduce polynomials up to degree
p = holderDerivOrder β;
* linearSmoother_bias_window — a polynomial-reproducing smoother whose design lies within
bandwidth h has bias ≤ (M/p!)·(∑ᵢ|Sᵢ|)·h^β.
The result: the degree-p local-polynomial intercept fitted to a β-Hölder regression
function f (noise-free responses Yᵢ = f(aᵢ)), with an invertible weighted design moment
matrix and design points within bandwidth h of the target t, has bias
|c₀ − f t| ≤ (M/p!)·(∑ᵢ |Sᵢ|)·h^β,
i.e. O(h^β) once the leverage ∑ᵢ|Sᵢ| is controlled by the design density.
theorem localPoly_intercept_bias reviewed
⚑ flagged
Causalean.Stat.Nonparametric
Interior local-polynomial bias is O(h^β). Let p denote the largest natural number strictly below the smoothness index β. If β is positive, the Hölder constant M is nonnegative, the design weights w are nonnegative, the target point t lies in a window [lo,hi], every design point aᵢ lies in the same window, every design point is within bandwidth h of t, the regression function f is p times continuously differentiable, its p-th derivative is (β−p)-Hölder with constant M on the window, the weighted design moment matrix is invertible, and c globally minimizes the weighted degree-p least-squares objective at noise-free responses f(aᵢ), then the fitted intercept c 0 estimates f t with bias |c 0 − f t| ≤ (M/p!)·(∑ᵢ |Sᵢ|)·h^β, where Sᵢ are the local-polynomial equivalent-kernel weights.
Formal statement
hypotheses
N :
ℕ
β M lo hi t h :
ℝ
a w :
Fin N → ℝ
f :
ℝ → ℝ
c :
Fin ((holderDerivOrder β) + 1) → ℝ
hβ :
0 < β
hM :
0 ≤ M
hw :
∀ i, 0 ≤ w i
ht :
t ∈ Icc lo hi
ha :
∀ i, a i ∈ Icc lo hi
hwin :
∀ i, |a i - t| ≤ h
hf :
ContDiff ℝ (holderDerivOrder β) f
hb :
hMdet :
hmin :
∀ c' : Fin ((holderDerivOrder β) + 1) → ℝ,
(∑ i, w i * (f (a i) - ∑ j, c j * (a i - t) ^ (j : ℕ)) ^ 2)
≤ ∑ i, w i * (f (a i) - ∑ j, c' j * (a i - t) ^ (j : ℕ)) ^ 2
conclusion
|c 0 - f t|
≤ (M / ((holderDerivOrder β)).factorial) * (∑ i, |equivKernelWeight (holderDerivOrder β) (fun i => a i - t) w i|) * h ^ β
Proof (Lean source)
theorem localPoly_intercept_bias {N : ℕ} {β M lo hi t h : ℝ} {a w : Fin N → ℝ}
{f : ℝ → ℝ} {c : Fin ((holderDerivOrder β) + 1) → ℝ}
(hβ : 0 < β) (hM : 0 ≤ M)
(hw : ∀ i, 0 ≤ w i)
(ht : t ∈ Icc lo hi) (ha : ∀ i, a i ∈ Icc lo hi)
(hwin : ∀ i, |a i - t| ≤ h)
(hf : ContDiff ℝ (holderDerivOrder β) f)
(hb : ∀ x ∈ Icc lo hi, ∀ y ∈ Icc lo hi,
|iteratedDeriv (holderDerivOrder β) f x - iteratedDeriv (holderDerivOrder β) f y|
≤ M * |x - y| ^ (β - ((holderDerivOrder β) : ℝ)))
(hMdet : IsUnit (designMatrix (holderDerivOrder β) (fun i => a i - t) w).det)
(hmin : ∀ c' : Fin ((holderDerivOrder β) + 1) → ℝ,
(∑ i, w i * (f (a i) - ∑ j, c j * (a i - t) ^ (j : ℕ)) ^ 2)
≤ ∑ i, w i * (f (a i) - ∑ j, c' j * (a i - t) ^ (j : ℕ)) ^ 2) :
|c 0 - f t|
≤ (M / ((holderDerivOrder β)).factorial)
* (∑ i, |equivKernelWeight (holderDerivOrder β) (fun i => a i - t) w i|) * h ^ β := by
have hc0 : c 0 = ∑ i, equivKernelWeight (holderDerivOrder β) (fun i => a i - t) w i * f (a i) :=
wls_intercept_eq_equivKernelSmoother (x := fun i => a i - t) (w := w)
(Y := fun i => f (a i)) hw hMdet hmin
have hrep : ∀ k : ℕ, k ≤ (holderDerivOrder β) →
(∑ i, equivKernelWeight (holderDerivOrder β) (fun i => a i - t) w i * (a i - t) ^ k)
= if k = 0 then 1 else 0 :=
equivKernelWeight_reproduces hMdet
rw [hc0]
exact linearSmoother_bias_window hβ hM ht ha hwin hf hb hrep
1 supporting declaration (lemmas, instances)
-
localPoly_intercept_bias_withintheorem — Interior local-polynomial bias for a regression function smooth only on a window. Let p be the largest integer strictly below the smoothness index β. If β is positive, the Hölder constant M is nonnegative, the design weights w are nonnegative, the target point t lies in a window [lo, hi], every design point aᵢ lies in the same window and within bandwidth h of t, the regression function f is p times continuously differentiable on the window, its p-th derivative within the window is (β − p)-Hölder there with constant M, the weighted design moment matrix is invertible, and c minimizes the weighted degree-p least-squares objective at the noise-free responses f(aᵢ), then the fitted intercept satisfies |c₀ − f(t)| ≤ (M/p!) · (∑ᵢ |Sᵢ|) · h^β, where Sᵢ are the local-polynomial equivalent-kernel weights.hypothesesN :ℕβ M lo hi t h :ℝa w :Fin N → ℝf :ℝ → ℝc :Fin ((holderDerivOrder β) + 1) → ℝhβ :0 < βhM :0 ≤ Mhw :∀ i, 0 ≤ w iht :t ∈ Icc lo hiha :∀ i, a i ∈ Icc lo hihwin :∀ i, |a i - t| ≤ hhf :hb :hMdet :hmin :∀ c' : Fin ((holderDerivOrder β) + 1) → ℝ,(∑ i, w i * (f (a i) - ∑ j, c j * (a i - t) ^ (j : ℕ)) ^ 2)≤ ∑ i, w i * (f (a i) - ∑ j, c' j * (a i - t) ^ (j : ℕ)) ^ 2conclusion|c 0 - f t|≤ (M / ((holderDerivOrder β)).factorial) * (∑ i, |equivKernelWeight (holderDerivOrder β) (fun i => a i - t) w i|) * h ^ βProof (Lean source)
theorem localPoly_intercept_bias_within {N : ℕ} {β M lo hi t h : ℝ} {a w : Fin N → ℝ} {f : ℝ → ℝ} {c : Fin ((holderDerivOrder β) + 1) → ℝ} (hβ : 0 < β) (hM : 0 ≤ M) (hw : ∀ i, 0 ≤ w i) (ht : t ∈ Icc lo hi) (ha : ∀ i, a i ∈ Icc lo hi) (hwin : ∀ i, |a i - t| ≤ h) (hf : ContDiffOn ℝ (holderDerivOrder β) f (Icc lo hi)) (hb : ∀ x ∈ Icc lo hi, ∀ y ∈ Icc lo hi, |iteratedDerivWithin (holderDerivOrder β) f (Icc lo hi) x - iteratedDerivWithin (holderDerivOrder β) f (Icc lo hi) y| ≤ M * |x - y| ^ (β - ((holderDerivOrder β) : ℝ))) (hMdet : IsUnit (designMatrix (holderDerivOrder β) (fun i => a i - t) w).det) (hmin : ∀ c' : Fin ((holderDerivOrder β) + 1) → ℝ, (∑ i, w i * (f (a i) - ∑ j, c j * (a i - t) ^ (j : ℕ)) ^ 2) ≤ ∑ i, w i * (f (a i) - ∑ j, c' j * (a i - t) ^ (j : ℕ)) ^ 2) : |c 0 - f t| ≤ (M / ((holderDerivOrder β)).factorial) * (∑ i, |equivKernelWeight (holderDerivOrder β) (fun i => a i - t) w i|) * h ^ β := by rw [wls_intercept_eq_equivKernelSmoother (x := fun i => a i - t) (w := w) (Y := fun i => f (a i)) hw hMdet hmin] exact linearSmoother_bias_window_within hβ hM ht ha hwin hf hb (equivKernelWeight_reproduces hMdet)
CoordinateDerivative 4 core · 1 supporting This file represents bivariate multi-index partial derivatives by evaluating iterated Fréchet derivatives along repeated standard-coordinate directions, and bounds those evaluations by the multilinear operator norm. ★ coordinatePartial_abs_le_iteratedFDeriv_norm
Bivariate coordinate derivatives and operator-norm bounds
This file represents bivariate multi-index partial derivatives by evaluating iterated Fréchet derivatives along repeated standard-coordinate directions, and bounds those evaluations by the multilinear operator norm.
def coordinateMultiOrder reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a bivariate multi-index, the total order of that multi-index is the sum of its two coordinate orders.
Definition (Lean source)
def coordinateDirections reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a bivariate multi-index and a position in a list whose length is its total order, the associated ordered standard-coordinate direction is the first standard coordinate direction when the position is smaller than the first coordinate order, and the second standard coordinate direction otherwise.
Definition (Lean source)
def coordinatePartial reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a real-valued function on two-dimensional Euclidean space, a bivariate multi-index, and a point in that space, the scalar coordinate partial derivative is the iterated derivative of total order given by the multi-index, evaluated at the point along the associated ordered standard-coordinate directions.
Definition (Lean source)
parameters
def
coordinatePartial f alpha x :
ℝ
given by
lemma coordinatePartial_abs_le_iteratedFDeriv_norm reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
Evaluating the iterated Fréchet derivative of a function f along the standard coordinate directions given by a bivariate multi-index alpha at a point x, cannot increase its operator norm — the resulting scalar coordinate partial is bounded in absolute value by the operator norm of the full iterated derivative.
Formal statement
hypotheses
conclusion
|coordinatePartial f alpha x| ≤ ‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x‖
Proof (Lean source)
lemma coordinatePartial_abs_le_iteratedFDeriv_norm
(f : EuclideanSpace ℝ (Fin 2) → ℝ) (alpha : Fin 2 → ℕ) (x : EuclideanSpace ℝ (Fin 2)) :
|coordinatePartial f alpha x| ≤
‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x‖ := by
unfold coordinatePartial
have h := (iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x).le_opNorm
(coordinateDirections alpha)
have hprod : ∏ k : Fin (coordinateMultiOrder alpha),
‖coordinateDirections alpha k‖ ≤ 1 := by
simpa using Finset.prod_le_one (fun _ _ ↦ norm_nonneg _)
(fun k _ ↦ by
unfold coordinateDirections
split <;> simp [EuclideanSpace.norm_single])
simpa only [Real.norm_eq_abs, mul_one] using
h.trans (mul_le_mul_of_nonneg_left hprod (norm_nonneg _))
1 supporting declaration (lemmas, instances)
-
coordinatePartial_sub_abs_le_iteratedFDeriv_sub_normlemma — Differences of scalar coordinate partials are bounded by the operator norm of the corresponding Fréchet-derivative difference.hypothesesconclusion|coordinatePartial f alpha x - coordinatePartial f alpha z|≤ ‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x - iteratedFDeriv ℝ (coordinateMultiOrder alpha) f z‖Proof (Lean source)
lemma coordinatePartial_sub_abs_le_iteratedFDeriv_sub_norm (f : EuclideanSpace ℝ (Fin 2) → ℝ) (alpha : Fin 2 → ℕ) (x z : EuclideanSpace ℝ (Fin 2)) : |coordinatePartial f alpha x - coordinatePartial f alpha z| ≤ ‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x - iteratedFDeriv ℝ (coordinateMultiOrder alpha) f z‖ := by unfold coordinatePartial rw [← ContinuousMultilinearMap.sub_apply] have h := (iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x - iteratedFDeriv ℝ (coordinateMultiOrder alpha) f z).le_opNorm (coordinateDirections alpha) have hprod : ∏ k : Fin (coordinateMultiOrder alpha), ‖coordinateDirections alpha k‖ ≤ 1 := by simpa using Finset.prod_le_one (fun _ _ ↦ norm_nonneg _) (fun k _ ↦ by unfold coordinateDirections split <;> simp [EuclideanSpace.norm_single]) simpa only [Real.norm_eq_abs, mul_one] using h.trans (mul_le_mul_of_nonneg_left hprod (norm_nonneg _))
DesignMatrixPosDef 3 core · 3 supporting Positive-definiteness criteria for local-polynomial weighted design moment matrices, viewed as Gram matrices of centered monomial vectors. ★ designMatrix_posDef★ designMatrix_isUnit_det★ nondegenerate_of_distinct_points
Positive-definiteness and invertibility of the design moment matrix
Positive-definiteness criteria for local-polynomial weighted design moment matrices, viewed as Gram matrices of centered monomial vectors.
The weighted design moment matrix M_{jk} = ∑ᵢ wᵢ xᵢʲ xᵢᵏ of a degree-p local-polynomial
fit is a weighted Gram matrix of the monomial vectors (1, xᵢ, …, xᵢᵖ): its quadratic
form is vᵀ M v = ∑ᵢ wᵢ (∑ⱼ vⱼ xᵢʲ)². Hence with nonnegative weights it is positive
semidefinite, and it is positive definite — therefore invertible — exactly when the
design is non-degenerate (no nonzero degree-p polynomial vanishes at all positively
weighted design points; e.g. there are p+1 distinct points with positive weight, by
Vandermonde). This discharges the IsUnit (designMatrix p x w).det hypothesis used
throughout the local-polynomial analysis from a concrete condition on the design.
theorem designMatrix_posDef reviewed
⚑ flagged
Causalean.Stat.Nonparametric
The design moment matrix is positive definite under a non-degeneracy condition on the design. If the design weights w are nonnegative and no nonzero coefficient vector v yields a degree-p polynomial ∑ⱼ vⱼ xᵢʲ that vanishes at every positively weighted design point, then the design moment matrix is positive definite. (Implied by the existence of p+1 distinct design points with positive weight, via Vandermonde.)
Formal statement
hypotheses
N p :
ℕ
Fin N → ℝ
hw :
∀ i, 0 ≤ w i
hnd :
∀ v : Fin (p + 1) → ℝ
if
v ≠ 0
then
∃ i, 0 < w i ∧ (∑ j, v j * x i ^ (j : ℕ)) ≠ 0
conclusion
(designMatrix p x w).PosDef
Proof (Lean source)
theorem designMatrix_posDef {N p : ℕ} {x w : Fin N → ℝ} (hw : ∀ i, 0 ≤ w i)
(hnd : ∀ v : Fin (p + 1) → ℝ, v ≠ 0 →
∃ i, 0 < w i ∧ (∑ j, v j * x i ^ (j : ℕ)) ≠ 0) :
(designMatrix p x w).PosDef := by
refine Matrix.PosDef.of_dotProduct_mulVec_pos (designMatrix_isHermitian x w) ?_
intro v hv
have hstar : star v = v := by
funext i
exact star_trivial _
rw [hstar, designMatrix_quadForm]
obtain ⟨i₀, hwi₀, hpoly⟩ := hnd v hv
refine Finset.sum_pos' (fun i _ => mul_nonneg (hw i) (sq_nonneg _)) ?_
refine ⟨i₀, Finset.mem_univ _, ?_⟩
exact mul_pos hwi₀ (sq_pos_of_ne_zero hpoly)
theorem designMatrix_isUnit_det reviewed
⚑ flagged
Causalean.Stat.Nonparametric
Invertibility of the design moment matrix from design non-degeneracy. If the design weights w are nonnegative and the design is non-degenerate — no nonzero coefficient vector v yields a degree-p polynomial ∑ⱼ vⱼ xᵢʲ vanishing at every positively weighted design point, then the design moment matrix's determinant is a unit, i.e. the matrix is invertible: a positive definite matrix has a unit determinant, discharging the IsUnit (designMatrix p x w).det hypothesis used throughout the local-polynomial analysis.
Formal statement
hypotheses
N p :
ℕ
Fin N → ℝ
hw :
∀ i, 0 ≤ w i
hnd :
∀ v : Fin (p + 1) → ℝ
if
v ≠ 0
then
∃ i, 0 < w i ∧ (∑ j, v j * x i ^ (j : ℕ)) ≠ 0
conclusion
IsUnit (designMatrix p x w).det
Proof (Lean source)
theorem designMatrix_isUnit_det {N p : ℕ} {x w : Fin N → ℝ} (hw : ∀ i, 0 ≤ w i)
(hnd : ∀ v : Fin (p + 1) → ℝ, v ≠ 0 →
∃ i, 0 < w i ∧ (∑ j, v j * x i ^ (j : ℕ)) ≠ 0) :
IsUnit (designMatrix p x w).det :=
(Matrix.isUnit_iff_isUnit_det _).mp (designMatrix_posDef hw hnd).isUnit
theorem nondegenerate_of_distinct_points reviewed
⚑ flagged
Causalean.Stat.Nonparametric
Design non-degeneracy from distinct positively-weighted points (Vandermonde). For a set S of design indices, if every index in S carries a positive weight and the design points xᵢ take at least p+1 distinct values on S, then the design non-degeneracy condition holds: no nonzero coefficient vector v yields a degree-p polynomial ∑ⱼ vⱼ xᵢʲ that vanishes at every positively weighted design point.
Formal statement
Proof (Lean source)
theorem nondegenerate_of_distinct_points {N p : ℕ} {x w : Fin N → ℝ}
(S : Finset (Fin N)) (hpos : ∀ i ∈ S, 0 < w i)
(hdistinct : p + 1 ≤ (S.image x).card) :
∀ v : Fin (p + 1) → ℝ, v ≠ 0 →
∃ i, 0 < w i ∧ (∑ j, v j * x i ^ (j : ℕ)) ≠ 0 := by
classical
intro v hv
by_contra hcon
push_neg at hcon
let P : Polynomial ℝ :=
∑ j : Fin (p + 1), C (v j) * X ^ (j : ℕ)
have hP_eval : ∀ a : ℝ, P.eval a = ∑ j : Fin (p + 1), v j * a ^ (j : ℕ) := by
intro a
simp only [P, Polynomial.eval_finset_sum, Polynomial.eval_mul, Polynomial.eval_C,
Polynomial.eval_pow, Polynomial.eval_X]
have hP_coeff : ∀ j₀ : Fin (p + 1), P.coeff (j₀ : ℕ) = v j₀ := by
intro j₀
simp only [P, Polynomial.finset_sum_coeff, Polynomial.coeff_C_mul_X_pow]
rw [Finset.sum_eq_single j₀]
· simp
· intro j _ hj
by_cases hval : (j₀ : ℕ) = (j : ℕ)
· exact (hj (Fin.ext hval.symm)).elim
· simp [hval]
· intro hj₀
simp at hj₀
obtain ⟨j₀, hj₀⟩ := Function.ne_iff.mp hv
have hcoeff_ne : P.coeff (j₀ : ℕ) ≠ 0 := by
simpa [hP_coeff j₀] using hj₀
have hP_ne : P ≠ 0 := by
intro hzero
exact hcoeff_ne (by simp [hzero])
have hP_natDegree : P.natDegree ≤ p := by
simpa [P] using
(Polynomial.natDegree_sum_le_of_forall_le
(s := univ)
(f := fun j : Fin (p + 1) => C (v j) * X ^ (j : ℕ))
(n := p)
(by
intro j _
exact (Polynomial.natDegree_C_mul_X_pow_le (v j) (j : ℕ)).trans
(Nat.lt_succ_iff.mp j.isLt)))
let Z : Finset ℝ := S.image x
have hsubset : Z.val ⊆ P.roots := by
intro a ha
have haZ : a ∈ Z := by
simpa using ha
obtain ⟨i, hiS, hxi⟩ := Finset.mem_image.mp haZ
have hroot_eval : P.eval a = 0 := by
rw [hP_eval, ← hxi]
exact hcon i (hpos i hiS)
exact (Polynomial.mem_roots hP_ne).mpr (by
simpa [Polynomial.IsRoot] using hroot_eval)
have hZ_le_degree : Z.card ≤ P.natDegree :=
Polynomial.card_le_degree_of_subset_roots (p := P) (Z := Z) hsubset
have hZ_le_p : Z.card ≤ p := hZ_le_degree.trans hP_natDegree
have hZ_ge : p + 1 ≤ Z.card := by
simpa [Z] using hdistinct
omega
3 supporting declarations (lemmas, instances)
-
designMatrix_quadFormtheorem — Gram quadratic form of the design moment matrix. vᵀ M v = ∑ᵢ wᵢ (∑ⱼ vⱼ xᵢʲ)² — the design moment matrix is the weighted Gram matrix of the monomial feature vectors.hypothesesconclusionv ⬝ᵥ (designMatrix p x w *ᵥ v) = ∑ i, w i * (∑ j, v j * x i ^ (j : ℕ)) ^ 2Proof (Lean source)
theorem designMatrix_quadForm {N p : ℕ} (x w : Fin N → ℝ) (v : Fin (p + 1) → ℝ) : v ⬝ᵥ (designMatrix p x w *ᵥ v) = ∑ i, w i * (∑ j, v j * x i ^ (j : ℕ)) ^ 2 := by simp only [dotProduct, mulVec, designMatrix] calc (∑ j : Fin (p + 1), v j * ∑ k : Fin (p + 1), (∑ i : Fin N, w i * x i ^ (j : ℕ) * x i ^ (k : ℕ)) * v k) = ∑ j : Fin (p + 1), ∑ k : Fin (p + 1), ∑ i : Fin N, v j * (w i * x i ^ (j : ℕ) * x i ^ (k : ℕ)) * v k := by refine Finset.sum_congr rfl (fun j _ => ?_) rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun k _ => ?_) rw [Finset.sum_mul, Finset.mul_sum] exact Finset.sum_congr rfl (fun i _ => by ring) _ = ∑ j : Fin (p + 1), ∑ i : Fin N, ∑ k : Fin (p + 1), v j * (w i * x i ^ (j : ℕ) * x i ^ (k : ℕ)) * v k := by apply Finset.sum_congr rfl intro j _ rw [Finset.sum_comm] _ = ∑ i : Fin N, ∑ j : Fin (p + 1), ∑ k : Fin (p + 1), v j * (w i * x i ^ (j : ℕ) * x i ^ (k : ℕ)) * v k := by rw [Finset.sum_comm] _ = ∑ i, w i * (∑ j, v j * x i ^ (j : ℕ)) ^ 2 := by refine Finset.sum_congr rfl (fun i _ => ?_) rw [pow_two, Finset.sum_mul_sum, Finset.mul_sum] refine Finset.sum_congr rfl (fun j _ => ?_) rw [Finset.mul_sum] exact Finset.sum_congr rfl (fun k _ => by ring) -
designMatrix_isHermitiantheorem — The design moment matrix is symmetric.Proof (Lean source)
theorem designMatrix_isHermitian {N p : ℕ} (x w : Fin N → ℝ) : (designMatrix p x w).IsHermitian := by ext j k simp only [Matrix.conjTranspose_apply, designMatrix, star_trivial] exact Finset.sum_congr rfl (fun i _ => by ring) -
designMatrix_posSemideftheorem — The design moment matrix is positive semidefinite when the weights are nonnegative (a sum of weighted rank-one squares).Proof (Lean source)
theorem designMatrix_posSemidef {N p : ℕ} {x w : Fin N → ℝ} (hw : ∀ i, 0 ≤ w i) : (designMatrix p x w).PosSemidef := by refine Matrix.PosSemidef.of_dotProduct_mulVec_nonneg (designMatrix_isHermitian x w) ?_ intro v have hstar : star v = v := by funext i exact star_trivial _ rw [hstar, designMatrix_quadForm] exact Finset.sum_nonneg (fun i _ => mul_nonneg (hw i) (sq_nonneg _))
GramCoercivity 3 core · 7 supporting This file represents finite local-polynomial coefficient vectors as polynomials and proves a positive, dimension-dependent lower bound for their weighted squared moment on a nondegenerate radial interval. ★ radialPolynomialEnergy_coercive
Coercivity of local-polynomial moment matrices
This file represents finite local-polynomial coefficient vectors as polynomials and proves a positive, dimension-dependent lower bound for their weighted squared moment on a nondegenerate radial interval.
def localPolynomial reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a nonnegative polynomial degree and real coefficients indexed from zero through that degree, the local-polynomial coefficient polynomial is .
def radialPolynomialEnergy reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a nonnegative polynomial degree and real coefficients indexed from zero through that degree, the radial polynomial energy is the double sum of divided by , over all coefficient indices from zero through that degree.
lemma radialPolynomialEnergy_coercive reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a polynomial degree bound p, there is a positive constant such that the radial polynomial energy of any coefficient vector is bounded below by that constant times the sum of the squared coefficients: on the unit sphere of the sup norm on coefficient vectors, radial polynomial energy has a positive minimum, and homogeneity packages this as a coercive lower bound for all coefficient vectors.
Formal statement
hypotheses
p :
ℕ
conclusion
∃ c : ℝ,
0 < c
Proof (Lean source)
lemma radialPolynomialEnergy_coercive (p : ℕ) :
∃ c : ℝ, 0 < c ∧ ∀ v : Fin (p + 1) → ℝ,
c * ∑ i, (v i) ^ 2 ≤ radialPolynomialEnergy p v := by
let S : Set (Fin (p + 1) → ℝ) := sphere 0 1
have hScompact : IsCompact S := isCompact_sphere 0 1
have hSne : S.Nonempty := by
refine ⟨fun _i => 1, ?_⟩
rw [Metric.mem_sphere, dist_zero_right]
simpa using (pi_norm_const' (ι := Fin (p + 1)) (1 : ℝ))
obtain ⟨v0, hv0S, hv0min⟩ := hScompact.exists_isMinOn hSne
(radialPolynomialEnergy_continuous p).continuousOn
have hv0ne : v0 ≠ 0 := by
intro h
subst v0
simpa [S] using hv0S
let c := radialPolynomialEnergy p v0 / (p + 1 : ℝ)
have hqpos : (0 : ℝ) < p + 1 := by positivity
refine ⟨c, div_pos (radialPolynomialEnergy_pos p hv0ne) hqpos, ?_⟩
intro v
by_cases hv : v = 0
· subst v
simp [radialPolynomialEnergy]
· let r : ℝ := ‖v‖
have hrpos : 0 < r := norm_pos_iff.mpr hv
let u : Fin (p + 1) → ℝ := r⁻¹ • v
have huS : u ∈ S := by
rw [Metric.mem_sphere, dist_zero_right]
change ‖r⁻¹ • v‖ = 1
rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hrpos]
exact inv_mul_cancel₀ hrpos.ne'
have hmin := hv0min huS
have hscale := radialPolynomialEnergy_smul p r u
have hru : r • u = v := by
ext i
simp [u, r, hrpos.ne']
rw [hru] at hscale
have hsum : ∑ i, (v i) ^ 2 ≤ (p + 1 : ℝ) * r ^ 2 := by
calc
∑ i, (v i) ^ 2 ≤ ∑ _i : Fin (p + 1), r ^ 2 := by
apply Finset.sum_le_sum
intro i hi
simpa [sq_abs, r] using
(sq_le_sq₀ (abs_nonneg (v i)) (norm_nonneg v)).2
(norm_le_pi_norm v i)
_ = (p + 1 : ℝ) * r ^ 2 := by simp
dsimp [c]
calc
radialPolynomialEnergy p v0 / (p + 1 : ℝ) * ∑ i, (v i) ^ 2
= radialPolynomialEnergy p v0 *
((∑ i, (v i) ^ 2) / (p + 1 : ℝ)) := by ring
_ ≤ radialPolynomialEnergy p v0 * r ^ 2 := by
apply mul_le_mul_of_nonneg_left _ (radialPolynomialEnergy_pos p hv0ne).le
exact (div_le_iff₀ hqpos).2 (by simpa [mul_comm] using hsum)
_ ≤ radialPolynomialEnergy p u * r ^ 2 := by
exact mul_le_mul_of_nonneg_right hmin (sq_nonneg r)
_ = radialPolynomialEnergy p v := by
rw [mul_comm, ← hscale]
7 supporting declarations (lemmas, instances)
-
localPolynomial_evallemma — Evaluation of the coefficient polynomial is the dot product with the monomial basis.hypothesesconclusion(localPolynomial p v).eval u = ∑ i, v i * u ^ (i : ℕ)Proof (Lean source)
lemma localPolynomial_eval (p : ℕ) (v : Fin (p + 1) → ℝ) (u : ℝ) : (localPolynomial p v).eval u = ∑ i, v i * u ^ (i : ℕ) := by simp only [localPolynomial, Polynomial.eval_finset_sum, Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow, Polynomial.eval_X] -
localPolynomial_eq_zero_ifflemma — The coefficient polynomial vanishes only when every coefficient does.Proof (Lean source)
lemma localPolynomial_eq_zero_iff (p : ℕ) (v : Fin (p + 1) → ℝ) : localPolynomial p v = 0 ↔ v = 0 := by constructor · intro hp funext i have hc := congrArg (fun q : ℝ[X] => q.coeff (i : ℕ)) hp simp only [localPolynomial, Polynomial.finset_sum_coeff, Polynomial.coeff_C_mul_X_pow] at hc rw [Finset.sum_eq_single i] at hc · simpa using hc · intro j hj hji have hne : (i : ℕ) ≠ (j : ℕ) := by intro hij exact hji (Fin.ext hij.symm) simp [hne] · simp · rintro rfl simp [localPolynomial] -
radialPolynomialEnergy_eq_integrallemma — The explicit moment matrix is exactly the weighted squared-polynomial integral on the unit interval.hypothesesp :ℕv :Fin (p + 1) → ℝconclusionradialPolynomialEnergy p v = ∫ u in (0 : ℝ)..1, (∑ i, v i * u ^ (i : ℕ)) ^ 2 * uProof (Lean source)
lemma radialPolynomialEnergy_eq_integral (p : ℕ) (v : Fin (p + 1) → ℝ) : radialPolynomialEnergy p v = ∫ u in (0 : ℝ)..1, (∑ i, v i * u ^ (i : ℕ)) ^ 2 * u := by rw [radialPolynomialEnergy] simp_rw [pow_two, Fintype.sum_mul_sum] simp_rw [Finset.sum_mul] rw [intervalIntegral.integral_finset_sum] apply Finset.sum_congr rfl intro i hi rw [intervalIntegral.integral_finset_sum] apply Finset.sum_congr rfl intro j hj rw [show (fun u : ℝ => (v i * u ^ (i : ℕ)) * (v j * u ^ (j : ℕ)) * u) = fun u => (v i * v j) * u ^ ((i : ℕ) + (j : ℕ) + 1) by funext u; rw [pow_add]; ring] rw [intervalIntegral.integral_const_mul, integral_pow] · push_cast ring all_goals intros apply Continuous.intervalIntegrable fun_prop -
radialPolynomialEnergy_poslemma — A nonzero coefficient vector has strictly positive radial energy.Proof (Lean source)
lemma radialPolynomialEnergy_pos (p : ℕ) {v : Fin (p + 1) → ℝ} (hv : v ≠ 0) : 0 < radialPolynomialEnergy p v := by let f : ℝ → ℝ := fun u => (∑ i, v i * u ^ (i : ℕ)) ^ 2 * u have hfcont : Continuous f := by fun_prop have hfint : IntervalIntegrable f volume 0 1 := hfcont.intervalIntegrable 0 1 rw [radialPolynomialEnergy_eq_integral] have hpoly : localPolynomial p v ≠ 0 := by simpa [localPolynomial_eq_zero_iff] using hv have hroots : Finite {u : ℝ | Polynomial.IsRoot (localPolynomial p v) u} := (Polynomial.roots (localPolynomial p v)).toFinset.finite_toSet.subset (by intro u hu simpa [Polynomial.mem_roots hpoly] using hu) have hinter : Set.Infinite (Ioo (0 : ℝ) 1) := Set.Ioo_infinite (by norm_num) obtain ⟨u, huI, huroot⟩ := (hinter.diff hroots).nonempty have hune : (∑ i, v i * u ^ (i : ℕ)) ≠ 0 := by rw [← localPolynomial_eval] intro he exact huroot (by simpa [Polynomial.IsRoot] using he) have hfu : f u ≠ 0 := mul_ne_zero (pow_ne_zero 2 hune) (ne_of_gt huI.1) rw [intervalIntegral.integral_pos_iff_support_of_nonneg_ae' (by filter_upwards [ae_restrict_mem (measurableSet_uIoc : MeasurableSet (Set.uIoc (0 : ℝ) 1))] with x hx rw [Set.uIoc_of_le (by norm_num)] at hx have hx0 : 0 ≤ x := by exact hx.1.le change 0 ≤ (∑ i, v i * x ^ (i : ℕ)) ^ 2 * x exact mul_nonneg (sq_nonneg _) hx0) hfint] refine ⟨by norm_num, ?_⟩ let U := support f ∩ Ioo (0 : ℝ) 1 have hUopen : IsOpen U := hfcont.isOpen_support.inter isOpen_Ioo have hUne : U.Nonempty := ⟨u, hfu, huI⟩ exact lt_of_lt_of_le (hUopen.measure_pos volume hUne) (measure_mono (by intro x hx exact ⟨hx.1, hx.2.1, hx.2.2.le⟩)) -
radialPolynomialEnergy_continuouslemma — The radial energy is a continuous quadratic function of its coefficient vector.Proof (Lean source)
@[fun_prop] lemma radialPolynomialEnergy_continuous (p : ℕ) : Continuous (radialPolynomialEnergy p) := by unfold radialPolynomialEnergy fun_prop -
radialPolynomialEnergy_smullemma — Radial energy is homogeneous of degree two in the coefficient vector.hypothesesconclusionradialPolynomialEnergy p (a • v) = a ^ 2 * radialPolynomialEnergy p vProof (Lean source)
lemma radialPolynomialEnergy_smul (p : ℕ) (a : ℝ) (v : Fin (p + 1) → ℝ) : radialPolynomialEnergy p (a • v) = a ^ 2 * radialPolynomialEnergy p v := by unfold radialPolynomialEnergy rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i hi rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj simp only [Pi.smul_apply, smul_eq_mul] ring -
signedRadialPolynomialEnergy_coercivelemma — The same coercivity constant works in both signed-distance orientations. The negative orientation merely changes coefficient i by the sign (-1)^i, which preserves the sum of coefficient squares.hypothesesp :ℕProof (Lean source)
lemma signedRadialPolynomialEnergy_coercive (p : ℕ) : ∃ c : ℝ, 0 < c ∧ ∀ t : Bool, ∀ v : Fin (p + 1) → ℝ, c * ∑ i, (v i) ^ 2 ≤ ∫ u in (0 : ℝ)..1, (∑ i, v i * (if t then u else -u) ^ (i : ℕ)) ^ 2 * u := by obtain ⟨c, hc, hcoercive⟩ := radialPolynomialEnergy_coercive p refine ⟨c, hc, ?_⟩ intro t v cases t with | true => simpa [radialPolynomialEnergy_eq_integral] using hcoercive v | false => let w : Fin (p + 1) → ℝ := fun i => (-1 : ℝ) ^ (i : ℕ) * v i have hnorm : ∑ i, (w i) ^ 2 = ∑ i, (v i) ^ 2 := by apply Finset.sum_congr rfl intro i hi simp only [w, mul_pow] rw [show ((-1 : ℝ) ^ (i : ℕ)) ^ 2 = 1 by rw [← pow_mul]; simp] ring have hpoly (u : ℝ) : ∑ i, w i * u ^ (i : ℕ) = ∑ i, v i * (-u) ^ (i : ℕ) := by apply Finset.sum_congr rfl intro i hi simp only [w] rw [neg_pow] ring rw [← hnorm] refine (hcoercive w).trans_eq ?_ rw [radialPolynomialEnergy_eq_integral] apply intervalIntegral.integral_congr intro u hu dsimp only simp only [Bool.false_eq_true, ↓reduceIte] rw [hpoly]
SmootherVariance 1 core · 0 supporting Specializes the generic uncorrelated heteroskedastic linear-smoother variance bound (Causalean.Stat.Nonparametric.LinearSmoother.Variance) to the degree-p local-polynomial equivalent-kernel weights. ★ localPoly_intercept_variance_le
Variance of the interior local-polynomial estimator
Specializes the generic uncorrelated heteroskedastic linear-smoother variance bound
(Causalean.Stat.Nonparametric.LinearSmoother.Variance) to the degree-p
local-polynomial equivalent-kernel weights. The leverage ∑ᵢ Sᵢ² is controlled by the
intercept entry of the inverse design moment matrix (M⁻¹)₀₀
(equivKernelWeight_sq_sum_le), so the interior O((Nh)^{−1/2}) stochastic-error rate
reduces to the single design-concentration bound (M⁻¹)₀₀ = O(1/(Nh)).
theorem localPoly_intercept_variance_le reviewed
⚑ flagged
Causalean.Stat.Nonparametric
Variance of the interior local-polynomial estimator. The degree-p local-polynomial equivalent-kernel smoother ∑ᵢ Sᵢ Yᵢ, applied to a family Y of square-integrable responses whose distinct coordinates are uncorrelated and individual variances are bounded by σbar², with an invertible design moment matrix and nonnegative weights bounded above by a constant W, has variance Var[∑ᵢ Sᵢ Yᵢ] ≤ σ² · W · (M⁻¹)₀₀. This reduces the interior O((Nh)^{−1/2}) stochastic-error rate to the single design-concentration bound (M⁻¹)₀₀ = O(1/(Nh)).
Formal statement
hypotheses
Ω :
Type*
N p :
ℕ
μ :
x w :
Fin N → ℝ
Y :
Fin N → Ω → ℝ
σbar W :
ℝ
hY :
∀ i, MemLp (Y i) 2 μ
hnoise :
UncorrelatedVarianceFamily Y μ σbar
hM :
IsUnit (designMatrix p x w).det
hw :
∀ i, 0 ≤ w i
hwW :
∀ i, w i ≤ W
conclusion
Var[fun ω => ∑ i, equivKernelWeight p x w i * Y i ω; μ]
≤ σbar ^ 2 * (W * (designMatrix p x w)⁻¹ 0 0)
Proof (Lean source)
theorem localPoly_intercept_variance_le {Ω : Type*} {N p : ℕ} [MeasurableSpace Ω]
{μ : Measure Ω} [IsProbabilityMeasure μ] {x w : Fin N → ℝ} {Y : Fin N → Ω → ℝ}
{σbar W : ℝ}
(hY : ∀ i, MemLp (Y i) 2 μ)
(hnoise : UncorrelatedVarianceFamily Y μ σbar)
(hM : IsUnit (designMatrix p x w).det)
(hw : ∀ i, 0 ≤ w i) (hwW : ∀ i, w i ≤ W) :
Var[fun ω => ∑ i, equivKernelWeight p x w i * Y i ω; μ]
≤ σbar ^ 2 * (W * (designMatrix p x w)⁻¹ 0 0) :=
linearSmoother_variance_le hY hnoise (equivKernelWeight_sq_sum_le hM hw hwW)