Stat.Nonparametric.Local­Poly.Estimator­Risk

Density constants for the local-polynomial kernel shape matrix

The bandwidth-free kernel shape matrix T_{jk} = ∫ K(u) u^{j+k} p(t+hu) du is the positive-density-weighted Gram matrix of the centered monomials, and the pure kernel-moment matrix G_{jk} = ∫ K(u) u^{j+k} du is its unit-density analogue. This file:

* defines weightMomentMatrix p W — the moment matrix ∫ W(u) u^{j+k} du of an arbitrary weight W : ℝ → ℝ, with its Gram quadratic form vᵀ (weightMomentMatrix p W) v = ∫ W(u) (∑ vⱼ uʲ)² du; * proves the Loewner sandwich c·G ⪯ T ⪯ C·G (on quadratic forms) from a pointwise weight domination c·W_G ≤ W_T ≤ C·W_G, which in turn follows from the design-density window bound cDesign ≤ p ≤ CDesign (the kernel weight K ≥ 0 carries the densities); * combines the sandwich with SquareCompletion.inv00_le_of_quadForm_sandwich to bound the shape matrix's intercept leverage and top weight by the density constants:

(T⁻¹)₀₀ ≤ (G⁻¹)₀₀ / cDesign, T₀₀ ≤ CDesign · G₀₀.

These discharge the (T⁻¹)₀₀ ≤ cInv and T₀₀ ≤ cTop hypotheses fed to population_scaling_of_conj, leaving no S-level invertibility/leverage assumption.

Change-of-variables factorization of the population design moment matrix

The population design moment matrix of the interior local-polynomial fit at bandwidth h and target t, against a design law with Lebesgue density p, has entries

S_{jk} = N · ∫ K((a−t)/h) · (a−t)^{j+k} · p(a) da.

The substitution u = (a−t)/h (a = t + h·u, da = h·du) factors it as a diagonal conjugation of the bandwidth-free shape matrix T_{jk} = ∫ K(u) u^{j+k} p(t+h·u) du:

S_{jk} = N · h^{j+k+1} · T_{jk} = (N·h) · (D · T · D)_{jk}, D = diagonal (fun j => h^j).

This is the literal factorization consumed by population_scaling_of_conj: it exposes the Θ(Nh) scale and the bandwidth-free shape matrix T (whose density-constant leverage bounds come from DensityConstants). The change of variables reuses the affine-rescaling pattern of Approximation/Kernel.lean.

Density-constant discharge of the local-polynomial leverage rate

Turns local-polynomial leverage hypotheses into explicit density and kernel-moment constants.

This module turns the abstract population-matrix leverage hypotheses for an interior local-polynomial fit into explicit density and kernel-moment constants. The earlier LocalPoly.Rate.population_scaling_of_conj reduced the leverage scaling to a bandwidth-free shape matrix T with assumed (T⁻¹)₀₀ ≤ cInv and T₀₀ ≤ cTop; here those constants become explicit density + kernel-moment quantities:

cInv = (G⁻¹)₀₀ / cDesign, cTop = CDesign · G₀₀,

with G = weightMomentMatrix p K the pure kernel-moment matrix and density-window bounds supplying the needed lower bound for the inverse rate and both lower/upper bounds for the leverage product. The chain is:

popDesignMatrix_factor (S = (Nh)·D T D, change of variables) → DensityConstants ((T⁻¹)₀₀ ≤ (G⁻¹)₀₀/cDesign, T₀₀ ≤ CDesign·G₀₀ via Loewner sandwich) → diagonal-conjugation scaling ((S⁻¹)₀₀ ≤ cInv/(Nh), S₀₀ ≤ cTop·(Nh)) → localPoly_inv00_rate / localPoly_leverage_bound.

The resulting localPoly_density_inv00_rate and localPoly_density_leverage_bound carry no hypothesis on the population matrix S other than the good design event (M entrywise within η of S) and explicit small-perturbation scale constants.

Interior local-polynomial estimator risk: bias and stochastic-L² bounds

Conditional local-polynomial estimator risk bounds, assembling interior bias and stochastic L² estimates for the windowed pointwise estimator.

This module assembles the conditional-on-design bias / variance bounds (localPoly_intercept_bias, localPoly_intercept_variance_le) and the bandwidth-free density-constant leverage facts produced by DensityLeverage:

* localPoly_estimatorBias_window — estimatorBias = |ĉ₀ − f(t)| ≤ Cbias · h^β with the explicit constant Cbias = (MH/p!) · L, where p = holderDerivOrder β and L = √(2·cInv·(cTop+1)) is the bandwidth-free leverage bound (MH the Hölder constant). The ℓ¹ leverage ∑ᵢ|Sᵢ| is squeezed by (∑ᵢ|Sᵢ|)² ≤ M₀₀·(M⁻¹)₀₀ ≤ L² (equivKernelWeight_abs_sum_sq_le). * localPoly_estimatorStochL2 — estimatorStochL2 = √Var(ĉ₀) ≤ Cvar · (Nh)^{-1/2} with the explicit constant Cvar = √(2σ²·W·cInv), from Var ≤ σ²·W·(M⁻¹)₀₀ and the leverage rate (M⁻¹)₀₀ ≤ 2·cInv/(Nh).

Both bounds hold conditionally on the design (equivalently, on the high-probability good design event of designMatrix_inv_concentration): once the leverage rate is supplied, the estimator risk reduces to a deterministic bias bound plus a conditional variance bound. The leverage constants cInv, cTop are the explicit density + kernel-moment quantities of localPoly_density_inv00_rate / localPoly_density_leverage_bound, so no S-level matrix hypothesis remains.

Square-completion bound on the (0,0) inverse entry under a Loewner sandwich

Linear-algebra bounds for the top-left inverse entry under positive-definite quadratic-form sandwiches.

The interior local-polynomial leverage (T⁻¹)₀₀ of the bandwidth-free kernel shape matrix T must be controlled by the density constants cDesign ≤ p ≤ CDesign together with the pure kernel-moment Gram matrix G. The clean route avoids Loewner inverse-monotonicity (absent from Mathlib): it uses only the elementary completing-the-square identity

(w − A⁻¹e)ᵀ A (w − A⁻¹e) ≥ 0 ⟺ 2 eᵀw − wᵀ A w ≤ eᵀ A⁻¹ e

valid for any positive definite A and vectors e, w. Evaluating it at the optimum w = A⁻¹e turns the inequality into the variational identity eᵀ A⁻¹ e = max_w (2 eᵀw − wᵀ A w), and a Loewner sandwich c·B ⪯ A (as quadratic forms) then transports the maximum:

(A⁻¹)₀₀ ≤ (B⁻¹)₀₀ / c.

This file proves that bound (and the trivial companion A₀₀ ≤ C·B₀₀ under A ⪯ C·B). It is the pure-linear-algebra heart of the density-constant discharge of the local-polynomial leverage rate.

Unconditional (full-sample-law) bias / variance of a truncated estimator

Unconditional risk bounds for truncated local-polynomial estimators, lifting conditional-on-design bias and variance estimates through good-design events.

The conditional-on-design capstones localPoly_estimatorBias_window and localPoly_estimatorStochL2 bound the bias / variance of the interior local-polynomial estimator given a non-degenerate design (equivalently, on the high-probability good-design event of designMatrix_inv_concentration). A full risk bound for the random-design estimator also needs bounds on the bias 𝔼[est] − f(t) and stochastic L² error √Var(est) under the full sample law, where the design itself is random.

This module performs that high-probability-to-L² lift as a pair of generic probabilistic facts, with no conditional-on-design caveat remaining:

* estimatorBias_unconditional — split 𝔼[est] = 𝔼[est·1_G] + 𝔼[est·1_{Gᶜ}] through the design σ-algebra m: on the good design event G the conditional bias |𝔼[est | m] − θ| ≤ B holds, while off G the truncation |est| ≤ M controls the contribution by 2M·μ(Gᶜ). Yields |𝔼[est] − θ| ≤ B + 2M·μ(Gᶜ). * estimatorVariance_unconditional — via the law of total variance Var(est) = 𝔼[Var(est | m)] + Var(𝔼[est | m]): the first term is the within-design variance (≤ Vrate on G, ≤ M² off it), the second is dominated by the squared conditional bias (≤ Bsq on G, ≤ 4M² off it). Yields Var(est) ≤ Vrate + Bsq + 5M²·μ(Gᶜ). * estimatorStochL2_unconditional — the √· form of the variance bound.

Each carries an explicit μ(Gᶜ) tail; designMatrix_inv_concentration makes that tail tiny (and a regime hypothesis absorbs it into the leading rate). The lift takes the conditional bias / variance bounds as hypotheses — exactly the output of the conditional capstones — and is otherwise self-contained: the conditional-expectation and law-of-total-variance machinery is MeasureTheory.condExp / ProbabilityTheory.condVar from Mathlib.