Stat.Nonparametric.LocalPoly
Degree-p local-polynomial regression substrate: equivalent-kernel weights, design positive definiteness, bias, variance, leverage rates, and pointwise risk bounds.
Weights 3 core · 4 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).
The weighted design moment matrix M_{jk} = ∑ᵢ wᵢ xᵢʲ xᵢᵏ of a degree-p local-polynomial fit with design points xᵢ (typically aᵢ − t) and weights wᵢ.
Definition (Lean source)
The local-polynomial equivalent-kernel weight Sᵢ = ∑ₖ (M⁻¹)₀ₖ wᵢ xᵢᵏ extracting the fitted intercept: the degree-p WLS intercept equals ∑ᵢ Sᵢ Yᵢ.
Definition (Lean source)
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
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
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 :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 : ℕ)) ^ 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 :conclusion(∑ 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 · 0 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.
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
Proof (Lean source)
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.
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
Proof (Lean source)
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
Proof (Lean source)
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)
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 sum_nonneg (fun i _ => mul_nonneg (hw i) (sq_nonneg _))
SmootherVariance 1 core · 0 supporting Specializes the generic spherical linear-smoother variance bound (Causalean.Stat.Nonparametric.LeastSquares.SmootherVariance) to the degree-p local-polynomial equivalent-kernel weights. ★ localPoly_intercept_variance_le
Variance of the interior local-polynomial estimator
Specializes the generic spherical linear-smoother variance bound
(Causalean.Stat.Nonparametric.LeastSquares.SmootherVariance) 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)).
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 that is spherical with common scale σ, 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)).