Stat.Nonparametric.Approximation
Approximation-theoretic estimates behind the bias analysis of nonparametric estimators; nothing here is random.
HolderTaylorMonomial 2 core · 0 supporting This module converts the diagonal Fréchet Taylor polynomial supplied by a multivariate Hölder condition into an explicitly indexed monomial polynomial. ★ holder_taylor_monomial_approx_uniform_center★ holder_taylor_monomial_approx
Monomial approximation of multivariate Hölder functions
This module converts the diagonal Fréchet Taylor polynomial supplied by a multivariate Hölder condition into an explicitly indexed monomial polynomial. The resulting remainder constant is uniform over the Hölder ball.
For a dimension and a finite monomial family, positive smoothness and Hölder parameters, a neighbourhood radius, and an exponent enumeration containing every multi-index through the Taylor order, there is one nonnegative constant such that, for every centre, every domain containing the closed coordinatewise box of half-width r around the centre, every function f in the standard Hölder ball of smoothness β and radius L on that domain, and every bandwidth h strictly between zero and r, some coefficient vector makes the monomial polynomial with the enumerated exponents approximate f(x0 + h u) within the constant times L h^β, uniformly over rescaled points u with all coordinates in [-1,1].
Formal statement
Proof (Lean source)
Local monomial approximation in a Hölder ball. Fix a centre x0 in d-dimensional Euclidean space and a finite family expo of exponent multi-indices. If the smoothness index β is positive, the Hölder constant L is positive, the neighbourhood radius r is positive, the closed sup-norm cube of radius r around x0 is contained in the domain S, and expo lists every exponent multi-index of total degree up to the Taylor order, then there is a constant C_b ≥ 0, depending only on β and d, such that every function f in the standard Hölder ball of exponent β, constant L, and domain S is approximated near x0, at any bandwidth h ∈ (0, r), by a monomial combination in the expo basis with error at most C_b · L · h^β, uniformly over the unit cube of rescaled directions.
Formal statement
Proof (Lean source)
Kernel 3 core · 2 supporting Convolution approximation bounds for Hölder functions using finite-order kernels with vanishing moments. ★ kernelSmoothingBias_bound
Kernel convolution approximation for Hölder functions
Convolution approximation bounds for Hölder functions using finite-order kernels with vanishing moments.
The definition kernelSmoothingBias records an unnormalised Lebesgue convolution difference. The
main theorem bounds this difference by O(h^β) when a kernel of order
p = holderDerivOrder β is applied to a β-Hölder function. No design density or normalising
denominator is present, so the object is not by itself the population bias of a general
random-design regression smoother.
The mechanism: substitute u = t + h v; the kernel's vanishing moments
∫ vʲ K = 0 (1 ≤ j ≤ p) annihilate the degree-p Taylor polynomial of f at t,
leaving only the Hölder–Taylor remainder
|f(t+hv) − T_p(t+hv)| ≤ (M/p!)·(h|v|)^β (holder_taylor_remainder), which
integrates against |K| (supported in [-1,1]) to O(h^β).
A kernel of order at least p: supported in [-1,1], integrable, with unit mass ∫ K = 1 and vanishing moments ∫ uʲ K(u) du = 0 for 1 ≤ j ≤ p. These are the kernel assumptions used by the convolution approximation bound below.
Definition (Lean source)
K is supported in [-1,1].
K has unit mass.
The moments 1,…,p of K vanish.
Given a real-valued function, a kernel function, a target point, and a bandwidth, the unnormalised Lebesgue convolution difference averages f(u) - f(t) using the rescaled kernel h⁻¹ K((u-t)/h). It contains neither a design density nor a normalising denominator.
Definition (Lean source)
The kernel convolution approximation error is O(h^β). Let p be the largest natural number strictly below the smoothness index β. If β is positive, the Hölder constant M is nonnegative, the bandwidth h is positive, the kernel K has order p, the function f is p times continuously differentiable, and its p-th derivative is (β−p)-Hölder with constant M on the window [t−h, t+h], then the absolute unnormalised convolution difference at t is bounded by (M/p! · ∫|K|)·h^β. For positive integer β = m, p = m - 1 and the Hölder exponent is 1.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
integrable_of_abs_le_const_mul_kerneltheorem — If a function F is dominated in absolute value by a constant multiple C·|K| of an integrable kernel K, then F is itself integrable. This is the integrability workhorse for kernel-smoothing arguments: every factor multiplying K (a monomial, a Taylor remainder) is bounded by |K| on the kernel's support and vanishes off it.hypothesesconclusionProof (Lean source)
theorem integrable_of_abs_le_const_mul_kernel {K F : ℝ → ℝ} {C : ℝ} (hKi : Integrable K) (hF : AEStronglyMeasurable F) (hbd : ∀ v, |F v| ≤ C * |K v|) : Integrable F := by refine Integrable.mono' (hKi.abs.const_mul C) hF ?_ filter_upwards with v simpa only [Real.norm_eq_abs] using hbd v -
kernelSmoothingBias_changeOfVartheorem — Change of variables for the kernel smoothing bias. Substituting u = t + h v (h > 0) turns the bias integral into ∫ K(v) (f(t+hv) − f t) dv: the h⁻¹ prefactor cancels the Jacobian h, and (u−t)/h = v.hypothesesf K :ℝ → ℝt h :ℝhh :0 < hconclusionkernelSmoothingBias f K t h = ∫ v, K v * (f (t + h * v) - f t)Proof (Lean source)
theorem kernelSmoothingBias_changeOfVar (f K : ℝ → ℝ) (t h : ℝ) (hh : 0 < h) : kernelSmoothingBias f K t h = ∫ v, K v * (f (t + h * v) - f t) := by unfold kernelSmoothingBias set ψ : ℝ → ℝ := fun u => K ((u - t) / h) * (f u - f t) with hψ have hL : (∫ u, h⁻¹ * K ((u - t) / h) * (f u - f t)) = h⁻¹ * ∫ u, ψ u := by rw [← integral_const_mul] refine integral_congr_ae (Filter.Eventually.of_forall (fun u => ?_)) simp only [hψ]; ring have hR : (∫ v, K v * (f (t + h * v) - f t)) = ∫ v, ψ (t + h * v) := by refine integral_congr_ae (Filter.Eventually.of_forall (fun v => ?_)) have harg : (t + h * v - t) / h = v := by rw [add_sub_cancel_left]; field_simp simp only [hψ, harg] rw [hL, hR]; symm calc (∫ v, ψ (t + h * v)) = ∫ v, (fun w => ψ (t + w)) (h * v) := rfl _ = |h⁻¹| • ∫ w, (fun w => ψ (t + w)) w := by simpa using Measure.integral_comp_mul_left (fun w : ℝ => ψ (t + w)) h _ = |h⁻¹| • ∫ w, ψ (t + w) := rfl _ = |h⁻¹| • ∫ u, ψ u := by rw [integral_add_left_eq_self ψ t] _ = h⁻¹ * ∫ u, ψ u := by rw [smul_eq_mul, abs_of_pos (inv_pos.mpr hh)]