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.

Density-based local-polynomial leverage bounds under shape positive definiteness

Derives explicit leverage constants from density and kernel moments, conditional on a positive definite density-weighted shape matrix.

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. In addition to density-window bounds and positive definiteness of G, both headline theorems assume positive definiteness of the density-weighted shape matrix T; this module does not derive that condition. 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 formulate the good design event in the rescaled polynomial basis. Writing D = diag(1,h,...,h^p) and M = D B D, the empirical matrix B = D⁻¹ M D⁻¹ is compared directly with (Nh) • T. This is the nonvacuous local-polynomial normalization: the intercept leverage is unchanged because D₀₀ = 1.

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 for any fixed design satisfying their explicit leverage hypotheses. This file does not define a random-design good event or derive those hypotheses from a concentration theorem. 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.

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 scalar factor 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.

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.

Generic full-sample-law bias / variance lifts for a truncated estimator

Generic unconditional risk bounds for a truncated estimator, lifting assumed conditional bias and variance estimates through a measurable good event.

The results take a sub-σ-algebra, a measurable good event, and the relevant conditional bias and variance bounds as hypotheses. They do not construct a random local-polynomial estimator or show that a design-concentration event supplies those hypotheses.

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. The caller must bound that probability and establish the conditional hypotheses for the same estimator and event. The lift is otherwise self-contained: the conditional-expectation and law-of-total-variance machinery is MeasureTheory.condExp / ProbabilityTheory.condVar from Mathlib.