Stat.Nonparametric.Least­Squares

Design-agnostic weighted least-squares primitives for nonparametric estimators: normal equations, projection optimality, smoother bias, and spherical-error variance.

Normal­Equations 3 core · 3 supporting Normal equations and projection-optimality identities for weighted linear least-squares fits with nonnegative observation weights. ★ lstsq_normal_equations

Normal equations for weighted linear least squares

Normal equations and projection-optimality identities for weighted linear least-squares fits with nonnegative observation weights.

A weighted linear least-squares fit chooses coefficients c minimizing ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ)² against a design matrix Φ (basis functions evaluated at the data) with nonnegative weights wᵢ. This file proves the first-order optimality conditions — the normal equations

∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ) Φᵢₖ = 0 for every basis index k,

directly from global minimality (no differentiability API: the objective is quadratic along each coordinate direction, so a one-variable perturbation forces the linear coefficient to vanish). The abstract design matrix Φ specialises to: * local polynomial regression — Φᵢⱼ = (aᵢ − t)ʲ (wls_normal_equations), the source of the equivalent-kernel polynomial-reproduction property (Fan–Gijbels 1996); * series / sieve regression — Φᵢⱼ = φⱼ(Xᵢ) for a basis φ (Newey 1997; Chen 2007). These are the algebraic identities underlying both interior local-polynomial and series-estimator analyses.

def lstsqResidual reviewed
Causalean.Stat.Nonparametric

The weighted residual at coefficient vector c against design matrix Φ: rᵢ(c) = Yᵢ − ∑ⱼ cⱼ Φᵢⱼ.

Definition (Lean source)
noncomputable def lstsqResidual {N : ℕ} {ι : Type*} [Fintype ι] (Φ : Fin N → ι → ℝ) (Y : Fin N → ℝ) (c : ι → ℝ) (i : Fin N) : ℝ := Y i - ∑ j, c j * Φ i j
Causalean.Stat.Nonparametric.lstsqResidual · Causalean/Stat/Nonparametric/LeastSquares/NormalEquations.lean:38
def lstsqObjective reviewed
Causalean.Stat.Nonparametric

The weighted sum of squares ∑ᵢ wᵢ rᵢ(c)².

Definition (Lean source)
noncomputable def lstsqObjective {N : ℕ} {ι : Type*} [Fintype ι] (Φ : Fin N → ι → ℝ) (w Y : Fin N → ℝ) (c : ι → ℝ) : ℝ := ∑ i, w i * lstsqResidual Φ Y c i ^ 2
Causalean.Stat.Nonparametric.lstsqObjective · Causalean/Stat/Nonparametric/LeastSquares/NormalEquations.lean:44
theorem lstsq_normal_equations reviewed
Causalean.Stat.Nonparametric

Normal equations for weighted linear least squares. If the weights w are nonnegative and the coefficient vector c globally minimizes the weighted sum of squares ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ)² over all coefficient vectors, then the weighted residual is orthogonal to every design column: ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ) Φᵢₖ = 0 for each basis index k.

Formal statement
hypotheses
N :
ℕ
ι :
Type*
Fintype ι
Fin N → ι → ℝ
w Y :
Fin N → ℝ
c :
ι → ℝ
hw :
∀ i, 0 ≤ w i
hmin :
∀ c' : ι → ℝ, lstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c'
conclusion
∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0
Proof (Lean source)
theorem lstsq_normal_equations {N : ℕ} {ι : Type*} [Fintype ι] {Φ : Fin N → ι → ℝ} {w Y : Fin N → ℝ} {c : ι → ℝ} (hw : ∀ i, 0 ≤ w i) (hmin : ∀ c' : ι → ℝ, lstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c') : ∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0 := by intro k classical let r : Fin N → ℝ := fun i => lstsqResidual Φ Y c i let A : ℝ := ∑ i, w i * r i * Φ i k let B : ℝ := ∑ i, w i * (Φ i k) ^ 2 have hres_update (s : ℝ) (i : Fin N) : lstsqResidual Φ Y (update c k (c k + s)) i = r i - s * Φ i k := by unfold lstsqResidual dsimp [r] have hfun : (fun j : ι => update c k (c k + s) j * Φ i j) = update (fun j : ι => c j * Φ i j) k ((c k + s) * Φ i k) := by funext j by_cases hj : j = k · subst hj simp · simp [update, hj] have hsum : (∑ j : ι, update c k (c k + s) j * Φ i j) = (∑ j : ι, c j * Φ i j) + s * Φ i k := by rw [hfun, sum_update_univ_eq_sub_add] ring rw [hsum] change Y i - ((∑ j : ι, c j * Φ i j) + s * Φ i k) = (Y i - ∑ j : ι, c j * Φ i j) - s * Φ i k ring have hobj (s : ℝ) : lstsqObjective Φ w Y (update c k (c k + s)) = lstsqObjective Φ w Y c - 2 * s * A + s ^ 2 * B := by unfold lstsqObjective calc (∑ i, w i * lstsqResidual Φ Y (update c k (c k + s)) i ^ 2) = ∑ i, (w i * r i ^ 2 - 2 * s * (w i * r i * Φ i k) + s ^ 2 * (w i * (Φ i k) ^ 2)) := by apply Finset.sum_congr rfl intro i hi rw [hres_update s i] ring _ = (∑ i, w i * lstsqResidual Φ Y c i ^ 2) - 2 * s * A + s ^ 2 * B := by simp [Finset.sum_sub_distrib, Finset.sum_add_distrib, Finset.mul_sum, A, B, r] have hquad : ∀ s : ℝ, 0 ≤ -2 * s * A + s ^ 2 * B := by intro s have h := hmin (update c k (c k + s)) rw [hobj s] at h linarith have hB : 0 ≤ B := by dsimp [B] apply sum_nonneg intro i hi exact mul_nonneg (hw i) (sq_nonneg _) exact linear_coeff_eq_zero_of_quadratic_nonneg hB hquad
Causalean.Stat.Nonparametric.lstsq_normal_equations · Causalean/Stat/Nonparametric/LeastSquares/NormalEquations.lean:77 · uses lstsqObjective , lstsqResidual
3 supporting declarations (lemmas, instances)
  • wls_normal_equations theorem — Normal equations for weighted polynomial least squares (local-polynomial 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.
    hypotheses
    N p :
    ℕ
    Fin N → ℝ
    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
    conclusion
    ∀ k : Fin (p + 1), ∑ i, w i * (Y i - ∑ j, c j * x i ^ (j : ℕ)) * x i ^ (k : ℕ) = 0
    Proof (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
    Causalean.Stat.Nonparametric.wls_normal_equations · Causalean/Stat/Nonparametric/LeastSquares/NormalEquations.lean:140
  • lstsq_pythagoras theorem — Pythagorean decomposition for weighted least squares. If the residual at c is orthogonal to every design column (∑ᵢ wᵢ rᵢ(c) Φᵢₖ = 0 for all k — e.g. c is the least-squares minimizer, by lstsq_normal_equations), then for any coefficient vector c' the weighted sum of squares splits exactly as SSE(c') = SSE(c) + ∑ᵢ wᵢ (∑ⱼ (cⱼ − c'ⱼ) Φᵢⱼ)²: the orthogonality kills the cross term, so the excess error is the weighted norm of the fitted-value difference.
    hypotheses
    N :
    ℕ
    ι :
    Type*
    Fintype ι
    Fin N → ι → ℝ
    w Y :
    Fin N → ℝ
    c :
    ι → ℝ
    hortho :
    ∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0
    c' :
    ι → ℝ
    conclusion
    lstsqObjective Φ w Y c'
    = lstsqObjective Φ w Y c + ∑ i, w i * (∑ j, (c j - c' j) * Φ i j) ^ 2
    Proof (Lean source)
    theorem lstsq_pythagoras {N : ℕ} {ι : Type*} [Fintype ι] {Φ : Fin N → ι → ℝ} {w Y : Fin N → ℝ} {c : ι → ℝ} (hortho : ∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0) (c' : ι → ℝ) : lstsqObjective Φ w Y c' = lstsqObjective Φ w Y c + ∑ i, w i * (∑ j, (c j - c' j) * Φ i j) ^ 2 := by classical let d : Fin N → ℝ := fun i => ∑ j, (c j - c' j) * Φ i j have hkey : ∀ i, lstsqResidual Φ Y c' i = lstsqResidual Φ Y c i + d i := by intro i unfold lstsqResidual dsimp [d] calc Y i - ∑ j, c' j * Φ i j = (Y i - ∑ j, c j * Φ i j) + ((∑ j, c j * Φ i j) - ∑ j, c' j * Φ i j) := by ring _ = (Y i - ∑ j, c j * Φ i j) + ∑ j, (c j - c' j) * Φ i j := by congr 1 rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro j hj ring have hcross : (∑ i, w i * lstsqResidual Φ Y c i * d i) = 0 := by dsimp [d] calc (∑ i, w i * lstsqResidual Φ Y c i * (∑ j, (c j - c' j) * Φ i j)) = ∑ i, ∑ j, (c j - c' j) * (w i * lstsqResidual Φ Y c i * Φ i j) := by apply Finset.sum_congr rfl intro i hi rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring _ = ∑ j, ∑ i, (c j - c' j) * (w i * lstsqResidual Φ Y c i * Φ i j) := by rw [Finset.sum_comm] _ = ∑ j, (c j - c' j) * (∑ i, w i * lstsqResidual Φ Y c i * Φ i j) := by apply Finset.sum_congr rfl intro j hj rw [Finset.mul_sum] _ = 0 := by simp [hortho] unfold lstsqObjective have hsum : (∑ i, w i * lstsqResidual Φ Y c' i ^ 2) = (∑ i, w i * lstsqResidual Φ Y c i ^ 2) + 2 * (∑ i, w i * lstsqResidual Φ Y c i * d i) + ∑ i, w i * d i ^ 2 := by calc (∑ i, w i * lstsqResidual Φ Y c' i ^ 2) = ∑ i, (w i * lstsqResidual Φ Y c i ^ 2 + 2 * (w i * lstsqResidual Φ Y c i * d i) + w i * d i ^ 2) := by apply Finset.sum_congr rfl intro i hi rw [hkey i] ring _ = (∑ i, w i * lstsqResidual Φ Y c i ^ 2) + 2 * (∑ i, w i * lstsqResidual Φ Y c i * d i) + ∑ i, w i * d i ^ 2 := by rw [Finset.sum_add_distrib, Finset.sum_add_distrib, Finset.mul_sum] rw [hsum, hcross] dsimp [d] ring
    Causalean.Stat.Nonparametric.lstsq_pythagoras · Causalean/Stat/Nonparametric/LeastSquares/NormalEquations.lean:160
  • lstsq_objective_le_of_orthogonal theorem — Optimality of the orthogonal least-squares fit. With nonnegative weights, a residual orthogonal to every design column attains the minimal weighted sum of squares: SSE(c) ≤ SSE(c') for every c'. (Immediate from lstsq_pythagoras, the excess term being a nonnegative weighted sum of squares.)
    hypotheses
    N :
    ℕ
    ι :
    Type*
    Fintype ι
    Fin N → ι → ℝ
    w Y :
    Fin N → ℝ
    c :
    ι → ℝ
    hw :
    ∀ i, 0 ≤ w i
    hortho :
    ∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0
    c' :
    ι → ℝ
    conclusion
    lstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c'
    Proof (Lean source)
    theorem lstsq_objective_le_of_orthogonal {N : ℕ} {ι : Type*} [Fintype ι] {Φ : Fin N → ι → ℝ} {w Y : Fin N → ℝ} {c : ι → ℝ} (hw : ∀ i, 0 ≤ w i) (hortho : ∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0) (c' : ι → ℝ) : lstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c' := by rw [lstsq_pythagoras hortho c'] have hnn : 0 ≤ ∑ i, w i * (∑ j, (c j - c' j) * Φ i j) ^ 2 := sum_nonneg (fun i _ => mul_nonneg (hw i) (sq_nonneg _)) linarith
    Causalean.Stat.Nonparametric.lstsq_objective_le_of_orthogonal · Causalean/Stat/Nonparametric/LeastSquares/NormalEquations.lean:230
Smoother­Bias 1 core · 2 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 exactly the property satisfied by the local-polynomial weighted-least-squares weights (it is the first block of the normal equations); 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.

theorem linearSmoother_bias_window reviewed
Causalean.Stat.Nonparametric

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
hypotheses
f :
ℝ → ℝ
β M lo hi t h :
ℝ
N :
ℕ
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 :
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 : ℕ
if
k ≤ (holderDerivOrder β)
then
(∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0
conclusion
|∑ i, S i * f (a i) - f t| ≤ (M / ((holderDerivOrder β)).factorial) * (∑ i, |S i|) * h ^ β
Proof (Lean source)
theorem linearSmoother_bias_window {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 : 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|) * h ^ β := by refine le_trans (linearSmoother_bias_of_reproduces hβ hM ht ha hf hb hrep) ?_ rw [mul_assoc] refine mul_le_mul_of_nonneg_left ?_ (div_nonneg hM (by positivity)) rw [Finset.sum_mul] refine Finset.sum_le_sum (fun i _ => ?_) exact mul_le_mul_of_nonneg_left (Real.rpow_le_rpow (abs_nonneg _) (hwin i) hβ.le) (abs_nonneg _)
Causalean.Stat.Nonparametric.linearSmoother_bias_window · Causalean/Stat/Nonparametric/LeastSquares/SmootherBias.lean:105 · uses holderDerivOrder
2 supporting declarations (lemmas, instances)
  • linearSmoother_reproduces_taylorPoly theorem — 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.
    hypotheses
    f :
    ℝ → ℝ
    t :
    ℝ
    N :
    ℕ
    Fin N → ℝ
    p :
    ℕ
    hrep :
    ∀ k : ℕ
    if
    k ≤ p
    then
    (∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0
    conclusion
    (∑ i, S i * taylorPoly p f t (a i)) = f t
    Proof (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
    Causalean.Stat.Nonparametric.linearSmoother_reproduces_taylorPoly · Causalean/Stat/Nonparametric/LeastSquares/SmootherBias.lean:37
  • linearSmoother_bias_of_reproduces theorem — 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.)
    hypotheses
    f :
    ℝ → ℝ
    β M lo hi t :
    ℝ
    N :
    ℕ
    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 : ℕ
    if
    k ≤ (holderDerivOrder β)
    then
    (∑ i, S i * (a i - t) ^ k) = if k = 0 then 1 else 0
    conclusion
    |∑ 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
    Causalean.Stat.Nonparametric.linearSmoother_bias_of_reproduces · Causalean/Stat/Nonparametric/LeastSquares/SmootherBias.lean:65
Smoother­Variance 1 core · 1 supporting Variance identities and leverage bounds for fixed-weight linear smoothers under spherical errors. ★ linearSmoother_variance_le

Variance of a fixed-weight linear smoother under spherical errors

Variance identities and leverage bounds for fixed-weight linear smoothers under spherical errors.

A linear smoother ∑ᵢ Sᵢ Yᵢ with deterministic weights Sᵢ (the local-polynomial / series equivalent-kernel weights, conditional on the design) applied to a spherical random family Y — distinct cells uncorrelated, each of variance σ² — 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.GaussMarkov). Both the local-polynomial and the series/sieve estimators consume it; the local-polynomial-specific corollary lives in Causalean.Stat.Nonparametric.LocalPoly.SmootherVariance.

theorem linearSmoother_variance_le reviewed
Causalean.Stat.Nonparametric

Stochastic-error bound for a fixed-weight linear smoother. If each response Yᵢ is square-integrable, the responses form a spherical family with common scale σ — each has variance σ², and distinct responses are uncorrelated, and the sum of squared smoother weights, ∑ᵢ Sᵢ², is bounded by V, then the variance of the linear smoother ∑ᵢ Sᵢ Yᵢ is at most σ² V.

Formal statement
hypotheses
Ω :
Type*
N :
ℕ
MeasurableSpace Ω
μ :
Measure Ω
IsProbabilityMeasure μ
Y :
Fin N → Ω → ℝ
S :
Fin N → ℝ
σ V :
ℝ
hY :
∀ i, MemLp (Y i) 2 μ
hsph :
SphericalFamily Y μ σ
hlev :
(∑ i, S i ^ 2) ≤ V
conclusion
Var[fun ω => ∑ i, S i * Y i ω; μ] ≤ σ ^ 2 * V
Proof (Lean source)
theorem linearSmoother_variance_le {Ω : Type*} {N : ℕ} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Y : Fin N → Ω → ℝ} {S : Fin N → ℝ} {σ V : ℝ} (hY : ∀ i, MemLp (Y i) 2 μ) (hsph : SphericalFamily Y μ σ) (hlev : (∑ i, S i ^ 2) ≤ V) : Var[fun ω => ∑ i, S i * Y i ω; μ] ≤ σ ^ 2 * V := by rw [linearSmoother_variance_spherical hY hsph] exact mul_le_mul_of_nonneg_left hlev (sq_nonneg σ)
Causalean.Stat.Nonparametric.linearSmoother_variance_le · Causalean/Stat/Nonparametric/LeastSquares/SmootherVariance.lean:49 · uses SphericalFamily
1 supporting declaration (lemmas, instances)