Stat.Nonparametric.LinearSmoother
A linear smoother estimates f(t) by ∑ᵢ Sᵢ Yᵢ with weights that depend only on the design.
Bias 1 core · 3 supporting Bias bounds for polynomial-reproducing linear smoothers, converting Hölder–Taylor remainders into pointwise nonparametric smoothing error bounds. ★ linearSmoother_bias_window
Bias of a polynomial-reproducing linear smoother
Bias bounds for polynomial-reproducing linear smoothers, converting Hölder–Taylor remainders into pointwise nonparametric smoothing error bounds.
A linear smoother estimates the value of a regression function f at a point t
by a weighted sum ∑ᵢ Sᵢ f(aᵢ) of its values at finitely many design points aᵢ,
with weights Sᵢ that depend only on the design (e.g. the local-polynomial /
Nadaraya–Watson "equivalent kernel" weights). This file proves the deterministic
bias estimate that turns the pointwise Hölder–Taylor remainder
(holder_taylor_remainder) into a bias bound for the whole smoother:
if the weights reproduce polynomials up to degree p = holderDerivOrder β in the sense
∑ᵢ Sᵢ (aᵢ − t)ᵏ = [k = 0] for k ≤ p, then for a β-Hölder f
|∑ᵢ Sᵢ f(aᵢ) − f t| ≤ (M/p!) · ∑ᵢ |Sᵢ| · |aᵢ − t|^β.
The reproduction hypothesis is the property satisfied by local-polynomial equivalent-kernel
weights; the factors ∑ᵢ |Sᵢ| |aᵢ − t|^β are later bounded via the design density. This lemma is
thus the bias half of the interior local-polynomial estimator analysis
(Fan–Gijbels 1996; Tsybakov 2009 Ch. 1), kept design-agnostic.
linearSmoother_bias_window_within gives the same bound when f is smooth only on the window
containing the design points, with derivatives taken within the window.
Interior O(h^β) bias of a polynomial-reproducing linear smoother. Let p denote the largest natural number strictly below the smoothness index β. If β is positive, the Hölder constant M is 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, f is p times continuously differentiable, its p-th derivative is (β−p)-Hölder with constant M on the window, and the smoother weights S reproduce polynomials of degree up to p at t, then the smoother's bias collapses to the standard rate |∑ᵢ Sᵢ f(aᵢ) − f t| ≤ (M/p!) · (∑ᵢ |Sᵢ|) · h^β.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
linearSmoother_reproduces_taylorPolytheorem — A linear smoother whose weights reproduce polynomials up to degree p (∑ᵢ Sᵢ (aᵢ − t)ᵏ = [k = 0] for k ≤ p) reproduces the degree-p Taylor polynomial of f at t exactly: ∑ᵢ Sᵢ · T_p(aᵢ; t) = f t. Only the constant term of the Taylor polynomial survives the reproduction identities.hypothesesf :ℝ → ℝt :ℝN :ℕFin N → ℝp :ℕhrep :∀ k : ℕifk ≤ pthen(∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0conclusion(∑ i, S i * taylorPoly p f t (a i)) = f tProof (Lean source)
theorem linearSmoother_reproduces_taylorPoly {f : ℝ → ℝ} {t : ℝ} {N : ℕ} {a S : Fin N → ℝ} (p : ℕ) (hrep : ∀ k : ℕ, k ≤ p → (∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0) : (∑ i, S i * taylorPoly p f t (a i)) = f t := by have key : (∑ i, S i * taylorPoly p f t (a i)) = ∑ k ∈ range (p + 1), (iteratedDeriv k f t / (k.factorial : ℝ)) * (∑ i, S i * (a i - t) ^ k) := by simp_rw [taylorPoly, Finset.mul_sum] rw [Finset.sum_comm] refine Finset.sum_congr rfl (fun k _ => ?_) refine Finset.sum_congr rfl (fun i _ => ?_) ring rw [key] have step : (∑ k ∈ range (p + 1), (iteratedDeriv k f t / (k.factorial : ℝ)) * (∑ i, S i * (a i - t) ^ k)) = ∑ k ∈ range (p + 1), (iteratedDeriv k f t / (k.factorial : ℝ)) * (if k = 0 then (1 : ℝ) else 0) := Finset.sum_congr rfl (fun k hk => by rw [hrep k (Nat.lt_succ_iff.mp (Finset.mem_range.mp hk))]) rw [step, Finset.sum_eq_single 0] · simp [iteratedDeriv_zero] · intro k _ hk0; simp [hk0] · intro h; exact absurd (Finset.mem_range.mpr (Nat.succ_pos p)) h -
linearSmoother_bias_of_reproducestheorem — Bias of a polynomial-reproducing linear smoother. If the weights Sᵢ reproduce polynomials up to degree p = holderDerivOrder β at t (∑ᵢ Sᵢ (aᵢ − t)ᵏ = [k = 0] for k ≤ p), the design points aᵢ and t lie in a window [lo, hi], and f is β-Hölder there (p-times continuously differentiable with (β−p)-Hölder top derivative, constant M), then the smoother's bias is controlled by the weighted spread of the design: |∑ᵢ Sᵢ f(aᵢ) − f t| ≤ (M/p!) · ∑ᵢ |Sᵢ| · |aᵢ − t|^β. (Tsybakov 2009, Ch. 1.)hypothesesf :ℝ → ℝβ M lo hi t :ℝN :ℕFin N → ℝhβ :0 < βhM :0 ≤ Mht :t ∈ Icc lo hiha :∀ i, a i ∈ Icc lo hihf :ContDiff ℝ (holderDerivOrder β) fhb :hrep :∀ k : ℕifk ≤ (holderDerivOrder β)then(∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0conclusion|∑ i, S i * f (a i) - f t|≤ (M / ((holderDerivOrder β)).factorial) * ∑ i, |S i| * |a i - t| ^ βProof (Lean source)
theorem linearSmoother_bias_of_reproduces {f : ℝ → ℝ} {β M lo hi t : ℝ} {N : ℕ} {a S : Fin N → ℝ} (hβ : 0 < β) (hM : 0 ≤ M) (ht : t ∈ Icc lo hi) (ha : ∀ i, a i ∈ Icc lo hi) (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 β) : ℝ))) (hrep : ∀ k : ℕ, k ≤ (holderDerivOrder β) → (∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0) : |∑ i, S i * f (a i) - f t| ≤ (M / ((holderDerivOrder β)).factorial) * ∑ i, |S i| * |a i - t| ^ β := by have hrep_tay : (∑ i, S i * taylorPoly (holderDerivOrder β) f t (a i)) = f t := linearSmoother_reproduces_taylorPoly (holderDerivOrder β) hrep have hdiff : (∑ i, S i * f (a i)) - f t = ∑ i, S i * (f (a i) - taylorPoly (holderDerivOrder β) f t (a i)) := by rw [← hrep_tay, ← Finset.sum_sub_distrib] refine Finset.sum_congr rfl (fun i _ => ?_) rw [mul_sub] rw [hdiff] calc |∑ i, S i * (f (a i) - taylorPoly (holderDerivOrder β) f t (a i))| ≤ ∑ i, |S i * (f (a i) - taylorPoly (holderDerivOrder β) f t (a i))| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ i, |S i| * (M / ((holderDerivOrder β)).factorial * |a i - t| ^ β) := by refine Finset.sum_le_sum (fun i _ => ?_) rw [abs_mul] exact mul_le_mul_of_nonneg_left (holder_taylor_remainder hβ hM ht (ha i) hf hb) (abs_nonneg _) _ = (M / ((holderDerivOrder β)).factorial) * ∑ i, |S i| * |a i - t| ^ β := by rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun i _ => ?_) ring -
linearSmoother_bias_window_withintheorem — Bias of a polynomial-reproducing linear smoother for a 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 target point t lies in a window [lo, hi], every design point aᵢ lies in the same window and within bandwidth h of t, f is p times continuously differentiable on the window, its p-th derivative within the window is (β − p)-Hölder there with constant M, and the smoother weights S reproduce polynomials of degree up to p at t, then |∑ᵢ Sᵢ f(aᵢ) − f(t)| ≤ (M/p!) · (∑ᵢ |Sᵢ|) · h^β.hypothesesf :ℝ → ℝβ M lo hi t h :ℝN :ℕFin N → ℝhβ :0 < βhM :0 ≤ Mht :t ∈ Icc lo hiha :∀ i, a i ∈ Icc lo hihwin :∀ i, |a i - t| ≤ hhf :hb :hrep :∀ k : ℕifk ≤ (holderDerivOrder β)then(∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0conclusion|∑ i, S i * f (a i) - f t| ≤ (M / ((holderDerivOrder β)).factorial) * (∑ i, |S i|) * h ^ βProof (Lean source)
theorem linearSmoother_bias_window_within {f : ℝ → ℝ} {β M lo hi t h : ℝ} {N : ℕ} {a S : Fin N → ℝ} (hβ : 0 < β) (hM : 0 ≤ M) (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 β) : ℝ))) (hrep : ∀ k : ℕ, k ≤ (holderDerivOrder β) → (∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0) : |∑ i, S i * f (a i) - f t| ≤ (M / ((holderDerivOrder β)).factorial) * (∑ i, |S i|) * h ^ β := by set p := holderDerivOrder β with hp have hrep_tay : (∑ i, S i * taylorWithinEval f p (Icc lo hi) t (a i)) = f t := by have key : (∑ i, S i * taylorWithinEval f p (Icc lo hi) t (a i)) = ∑ k ∈ range (p + 1), ((k.factorial : ℝ)⁻¹ * iteratedDerivWithin k f (Icc lo hi) t) * (∑ i, S i * (a i - t) ^ k) := by simp_rw [taylor_within_apply, smul_eq_mul, Finset.mul_sum] rw [Finset.sum_comm] refine Finset.sum_congr rfl (fun k _ => ?_) refine Finset.sum_congr rfl (fun i _ => ?_) ring rw [key, Finset.sum_congr rfl (fun k hk => by rw [hrep k (Nat.lt_succ_iff.mp (Finset.mem_range.mp hk))]), Finset.sum_eq_single 0] · simp [iteratedDerivWithin_zero] · intro k _ hk0; simp [hk0] · intro hmem; exact absurd (Finset.mem_range.mpr (Nat.succ_pos p)) hmem have hdiff : (∑ i, S i * f (a i)) - f t = ∑ i, S i * (f (a i) - taylorWithinEval f p (Icc lo hi) t (a i)) := by rw [← hrep_tay, ← Finset.sum_sub_distrib] exact Finset.sum_congr rfl (fun i _ => by rw [mul_sub]) rw [hdiff] calc |∑ i, S i * (f (a i) - taylorWithinEval f p (Icc lo hi) t (a i))| ≤ ∑ i, |S i * (f (a i) - taylorWithinEval f p (Icc lo hi) t (a i))| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ i, |S i| * (M / (p.factorial : ℝ) * h ^ β) := by refine Finset.sum_le_sum (fun i _ => ?_) rw [abs_mul] exact mul_le_mul_of_nonneg_left ((holder_taylor_remainder_within hβ hM ht (ha i) hf hb).trans (mul_le_mul_of_nonneg_left (Real.rpow_le_rpow (abs_nonneg _) (hwin i) hβ.le) (div_nonneg hM (by positivity)))) (abs_nonneg _) _ = (M / (p.factorial : ℝ)) * (∑ i, |S i|) * h ^ β := by rw [← Finset.sum_mul] ring
Variance 2 core · 0 supporting Variance bounds for fixed-weight linear smoothers under uncorrelated heteroskedastic errors. ★ linearSmoother_variance_le
Variance of a fixed-weight linear smoother under heteroskedastic errors
Variance bounds for fixed-weight linear smoothers under uncorrelated heteroskedastic errors.
A linear smoother ∑ᵢ Sᵢ Yᵢ with deterministic weights Sᵢ (the local-polynomial /
series equivalent-kernel weights, conditional on the design) applied to an uncorrelated
random family Y whose cell variances are bounded by σ̄² has variance
Var[∑ᵢ Sᵢ Yᵢ] ≤ σ̄² · ∑ᵢ Sᵢ².
This is the generic (design-agnostic) variance half of the interior nonparametric estimator
analysis: it reduces the target stochastic-error bound O((Nh)^{−1/2}) to a leverage bound
∑ᵢ Sᵢ² = O(1/(Nh)). It is a direct corollary of the Gauss–Markov covariance–quadratic-form
identity (Causalean.Stat.GaussMarkov). Both the local-polynomial and the series/sieve estimators
consume it; the local-polynomial-specific corollary lives in
Causalean.Stat.Nonparametric.LocalPoly.SmootherVariance.
Stochastic-error bound for a fixed-weight linear smoother. If each response Yᵢ is square-integrable, distinct responses are uncorrelated and every response variance is bounded by σbar², and the sum of squared smoother weights, ∑ᵢ Sᵢ², is bounded by V, then the variance of the linear smoother ∑ᵢ Sᵢ Yᵢ is at most σbar² V.