ML.Kernel
Roll-up: the abstract RKHS interface, kernel Gram matrices with regularized positive definiteness, the kernel-ridge representer theorem, the Rademacher complexity rate for the L²-ball linear class, and the genuine square
RKHS 1 core · 0 supporting Mathlib has no RKHS hierarchy, so IsRKHS uses a minimal abstract interface: a real inner-product space H of functions on X with an evaluation map and a representer map satisfying the reproducing property f x = ⟪f, kₓ⟫. ★ IsRKHS
Reproducing-kernel Hilbert spaces (abstract interface)
Mathlib has no RKHS hierarchy, so IsRKHS uses a minimal abstract interface: a
real inner-product space H of functions on X with an evaluation map and a
representer map satisfying the reproducing property f x = ⟪f, kₓ⟫. This is
the interface consumed by the representer theorem and RKHS Rademacher bounds.
The candidate reproducing-kernel Hilbert space structure on a real inner-product space H of functions on X, given an evaluation map and a representer map, satisfies the reproducing property: evaluating any function of H at a point equals its inner product with the representer of that point.
Definition (Lean source)
EffectiveDimension 2 core · 7 supporting The effective dimension at regularization level λ > 0 of a positive operator with (summable, nonnegative) eigenvalue family μ : ι → ℝ is N(λ) = ∑ᵢ μᵢ / (μᵢ + λ) = tr(T (T + λ)⁻¹). ★ effectiveDimension★ effectiveDimension_le_trace_div
Effective dimension of a trace-class operator
The effective dimension at regularization level λ > 0 of a positive operator with
(summable, nonnegative) eigenvalue family μ : ι → ℝ is
N(λ) = ∑ᵢ μᵢ / (μᵢ + λ) = tr(T (T + λ)⁻¹).
It is the quantity that governs the variance term of kernel ridge regression: the
Caponnetto–De Vito optimal-rate analysis expresses the minimax L²(ρ) rate of kernel ridge
through N(λ) and the eigenvalue-decay/source-condition exponents. This file provides the
definition and its basic structural properties for the trace-class (summable-eigenvalue)
regime — the infinite-dimensional RKHS setting.
* effectiveDimension_nonneg — 0 ≤ N(λ);
* summable_effectiveDimension_term — the summand family is summable (so N(λ) is a genuine
real number, not the fallback value of a non-summable tsum);
* effectiveDimension_le_trace_div — N(λ) ≤ (tr T)/λ (the crude dimension-free bound);
* effectiveDimension_le_card — over finitely many eigenvalues, N(λ) ≤ #ι;
* effectiveDimension_antitone — N is antitone in λ (more regularization ⇒ smaller
effective dimension).
The downstream rate theorem (N(λ)/eigenvalue-decay ⇒ the n^{-2rb/(2rb+1)} kernel-ridge
L² rate) additionally requires Hilbert-space operator-concentration machinery (an operator
Bernstein inequality for (T+λ)^{-1/2}(T − T̂ₙ)(T+λ)^{-1/2}) that is a separate substrate; this
file is the definitional foundation it would build on.
The effective dimension N(λ) = ∑ᵢ μᵢ/(μᵢ+λ) of an operator with eigenvalue family μ at regularization level λ.
Definition (Lean source)
Dimension-free bound. For an eigenvalue family μ and regularization level lam, if every eigenvalue is nonnegative, the regularization level is strictly positive, and the eigenvalues are summable, i.e. the operator is trace-class, then the effective dimension N(lam) = ∑ᵢ μᵢ/(μᵢ+lam) is at most the trace ∑ᵢ μᵢ divided by lam. This is the bound that, with eigenvalue decay μᵢ ≍ i^{-b}, yields N(λ) = O(λ^{-1/b}).
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
effectiveDimension_term_nonneglemma — Each summand μᵢ/(μᵢ+λ) is nonnegative (for nonnegative eigenvalues and λ > 0).hypothesesμ :ι → ℝlam :ℝhμ :∀ i, 0 ≤ μ ihlam :0 < lami :ιconclusion0 ≤ μ i / (μ i + lam)Proof (Lean source)
lemma effectiveDimension_term_nonneg {μ : ι → ℝ} {lam : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam : 0 < lam) (i : ι) : 0 ≤ μ i / (μ i + lam) := div_nonneg (hμ i) (add_nonneg (hμ i) hlam.le) -
effectiveDimension_term_le_divlemma — Each summand is dominated by μᵢ/λ.hypothesesμ :ι → ℝlam :ℝhμ :∀ i, 0 ≤ μ ihlam :0 < lami :ιconclusionμ i / (μ i + lam) ≤ μ i / lamProof (Lean source)
lemma effectiveDimension_term_le_div {μ : ι → ℝ} {lam : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam : 0 < lam) (i : ι) : μ i / (μ i + lam) ≤ μ i / lam := by gcongr <;> linarith [hμ i] -
effectiveDimension_term_le_onelemma — Each summand is at most 1.hypothesesμ :ι → ℝlam :ℝhμ :∀ i, 0 ≤ μ ihlam :0 < lami :ιconclusionμ i / (μ i + lam) ≤ 1Proof (Lean source)
lemma effectiveDimension_term_le_one {μ : ι → ℝ} {lam : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam : 0 < lam) (i : ι) : μ i / (μ i + lam) ≤ 1 := by rw [div_le_one (add_pos_of_nonneg_of_pos (hμ i) hlam)] linarith [hμ i] -
summable_effectiveDimension_termlemma — For a trace-class operator (summable eigenvalues) the effective-dimension summands are summable, so effectiveDimension is a genuine real number.hypothesesconclusionSummable (fun i => μ i / (μ i + lam))Proof (Lean source)
lemma summable_effectiveDimension_term {μ : ι → ℝ} {lam : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam : 0 < lam) (hsum : Summable μ) : Summable (fun i => μ i / (μ i + lam)) := Summable.of_nonneg_of_le (fun i => effectiveDimension_term_nonneg hμ hlam i) (fun i => effectiveDimension_term_le_div hμ hlam i) (hsum.div_const lam) -
effectiveDimension_nonneglemma — The effective dimension is nonnegative.hypothesesμ :ι → ℝlam :ℝhμ :∀ i, 0 ≤ μ ihlam :0 < lamconclusion0 ≤ effectiveDimension μ lamProof (Lean source)
lemma effectiveDimension_nonneg {μ : ι → ℝ} {lam : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam : 0 < lam) : 0 ≤ effectiveDimension μ lam := tsum_nonneg (fun i => effectiveDimension_term_nonneg hμ hlam i) -
effectiveDimension_le_cardlemma — Over finitely many eigenvalues, N(λ) never exceeds the ambient dimension #ι.hypothesesconclusioneffectiveDimension μ lam ≤ (Fintype.card ι : ℝ)Proof (Lean source)
lemma effectiveDimension_le_card [Fintype ι] {μ : ι → ℝ} {lam : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam : 0 < lam) : effectiveDimension μ lam ≤ (Fintype.card ι : ℝ) := by unfold effectiveDimension rw [tsum_fintype] calc ∑ i, μ i / (μ i + lam) ≤ ∑ _i : ι, (1 : ℝ) := Finset.sum_le_sum fun i _ => effectiveDimension_term_le_one hμ hlam i _ = (Fintype.card ι : ℝ) := by simp [Finset.card_univ] -
effectiveDimension_antitonelemma — Monotonicity in the regularization level. More regularization shrinks the effective dimension: λ₁ ≤ λ₂ ⇒ N(λ₂) ≤ N(λ₁).hypothesesconclusioneffectiveDimension μ lam₂ ≤ effectiveDimension μ lam₁Proof (Lean source)
lemma effectiveDimension_antitone {μ : ι → ℝ} {lam₁ lam₂ : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam₁ : 0 < lam₁) (hle : lam₁ ≤ lam₂) (hsum : Summable μ) : effectiveDimension μ lam₂ ≤ effectiveDimension μ lam₁ := by have hlam₂ : 0 < lam₂ := lt_of_lt_of_le hlam₁ hle refine Summable.tsum_le_tsum (fun i => ?_) (summable_effectiveDimension_term hμ hlam₂ hsum) (summable_effectiveDimension_term hμ hlam₁ hsum) gcongr <;> linarith [hμ i, hlam₁, hle]
Gram 3 core · 0 supporting The file defines the Gram matrix gram k x, the positive-semidefinite-kernel predicate IsPSDkernel, and the regularized-Gram positive-definiteness theorem gram_add_lambda_posDef: if k is positive semidefinite and λ > 0, t ★ IsPSDkernel★ gram_add_lambda_posDef
Gram matrices of a kernel
The file defines the Gram matrix gram k x, the positive-semidefinite-kernel
predicate IsPSDkernel, and the regularized-Gram positive-definiteness theorem
gram_add_lambda_posDef: if k is positive semidefinite and λ > 0, then
K + λI ≻ 0. This is the finite-sample invertibility fact used by kernel ridge
regression.
The Gram matrix Kᵢⱼ = k(xᵢ, xⱼ) of a kernel k on a finite sample x.
A kernel is positive semidefinite when every Gram matrix is PSD.
Definition (Lean source)
For a finite sample x and kernel k, if k is positive semidefinite, i.e. every Gram matrix it produces is PSD and the regularization level lam is strictly positive, then the regularized Gram matrix gram k x + lam·I is positive definite, hence invertible.
Formal statement
Proof (Lean source)
Rate 2 core · 0 supporting The statistical rate for empirical risk minimization over an L²-norm-bounded class of linear predictors a ↦ ⟪w, a⟫ (the dual/feature-space view of kernel ridge: the representer theorem puts the estimator in an RKHS ball) ★ rademacherComplexity_l2_ball_le★ kernel_erm_excess_rate
Kernel / L²-ball linear predictors — Rademacher rate
The statistical rate for empirical risk minimization over an L²-norm-bounded class of
linear predictors a ↦ ⟪w, a⟫ (the dual/feature-space view of kernel ridge: the
representer theorem puts the estimator in an RKHS ball). The theorem
rademacherComplexity_l2_ball_le bounds the expected Rademacher complexity of the
W-ball class over Xb-bounded features by Xb·W/√n; kernel_erm_excess_rate
combines that bound with the generic ERM oracle inequality
(erm_oracle_inequality) to give the O(1/√n) excess-risk rate.
Built on FoML's linear_predictor_l2_bound' (empirical Rademacher bound for the L²-ball,
lifted here to the expected rademacherComplexity).
Rademacher complexity of the L²-ball linear class. If the feature bound Xb is nonnegative, the weight bound W is nonnegative, and every feature vector has Euclidean norm at most Xb, then the expected Rademacher complexity of the class of linear predictors with weight norm at most W, on a sample of size n, is at most Xb·W/√n.
Formal statement
Proof (Lean source)
Kernel ERM excess-risk rate over the L² ball. For features valued in the closed Xb-ball and linear predictors indexed by the closed W-ball, if the feature bound Xb is nonnegative, the weight bound W is nonnegative, the feature map X is measurable, the constant t satisfies the calibration t·(Xb·W)² ≤ 1/2, the tolerance ε is nonnegative, and the estimator ŵ attains empirical risk no larger than that of the comparator wstar, then the probability that the excess population risk of ŵ over wstar exceeds 4·Xb·W/√n + 2ε is at most exp(-ε²tn).
Formal statement
Proof (Lean source)
Ridge 2 core · 0 supporting Kernel ridge regression minimizes the regularized empirical risk over an RKHS. ★ representer_theorem
Kernel ridge regression — the representer theorem
Kernel ridge regression minimizes the regularized empirical risk over an RKHS.
This file defines krrRisk and proves representer_theorem: under λ > 0, any
global minimizer is a finite linear combination of the sample representers
k(·, xᵢ). The theorem is the dimension-reduction step from an RKHS-valued
optimization problem to a finite coefficient problem.
The kernel-ridge regularized empirical risk of an RKHS element f: (1/n) ∑ᵢ (f(xᵢ) − yᵢ)² + λ‖f‖².
Definition (Lean source)
For a complete reproducing-kernel Hilbert space H, if (feval, representer) realizes H as an RKHS on X, i.e. evaluation at each point equals the inner product with its representer, the regularization level lam is strictly positive, and fhat minimizes the regularized empirical risk krrRisk over all of H for the sample (x, y), then fhat lies in the span of the sample representers representer x₁, …, representer xₙ, i.e. it is a finite linear combination of them.
Formal statement
Proof (Lean source)
RKHSRademacher 1 core · 1 supporting This file proves the canonical RKHS-ball empirical Rademacher bound Rhat_n({‖f‖_H ≤ r}) ≤ κ * r / sqrt n, where κ² = sup_x K(x,x). ★ rkhs_ball_empiricalRademacher_le
RKHS-ball Rademacher complexity
This file proves the canonical RKHS-ball empirical Rademacher bound
Rhat_n({‖f‖_H ≤ r}) ≤ κ * r / sqrt n, where κ² = sup_x K(x,x). The main
Hilbert-space theorem is empiricalRademacherComplexity_innerBall_le; the RKHS
specialization is rkhs_ball_empiricalRademacher_le, which uses the reproducing
identity to turn function evaluation into an inner product. This is the
standard worst-case O(1 / sqrt n) kernel learning rate associated with
Bartlett--Mendelson style Rademacher complexity bounds.
In a reproducing-kernel Hilbert space H, if (feval, representer) realizes H as an RKHS on X, κ is a nonnegative bound, r is a nonnegative radius, and every sampled kernel representer representer (xs k) has norm at most κ, then the empirical Rademacher complexity, on the sample xs, of the closed ball of radius r in H is at most κ·r/√n.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
empiricalRademacherComplexity_innerBall_letheorem — For a sample of vectors bounded by κ and linear weights bounded by r, the empirical Rademacher complexity of the resulting linear class is at most κ times r divided by the square root of the sample size.hypothesesE :ι :Type*n :ℕκ r :ℝhκ :0 ≤ κhr :0 ≤ rY :Fin n → EhY :∀ k, ‖Y k‖ ≤ κw :ι → Ehw :∀ i, ‖w i‖ ≤ rProof (Lean source)
theorem empiricalRademacherComplexity_innerBall_le {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type*} {n : ℕ} (κ r : ℝ) (hκ : 0 ≤ κ) (hr : 0 ≤ r) (Y : Fin n → E) (hY : ∀ k, ‖Y k‖ ≤ κ) (w : ι → E) (hw : ∀ i, ‖w i‖ ≤ r) : empiricalRademacherComplexity n (fun i a => inner ℝ (w i) a) Y ≤ κ * r / sqrt n := by classical by_cases hι : Nonempty ι · letI : Nonempty ι := hι exact empiricalRademacherComplexity_innerBall_le_nonempty κ r hκ hr Y hY w hw · haveI : IsEmpty ι := not_nonempty_iff.mp hι unfold empiricalRademacherComplexity simp only [Signs.card, Nat.cast_pow, Nat.cast_ofNat, Int.reduceNeg, abs_mul, abs_inv, Nat.abs_cast, iSup_of_isEmpty, Finset.sum_const_zero, mul_zero, ge_iff_le] exact div_nonneg (mul_nonneg hκ hr) (Real.sqrt_nonneg _)
SquaredLoss 3 core · 0 supporting The genuine squared-loss statistical rate for empirical risk minimization over an L²-norm-bounded class of linear predictors a ↦ ⟪w, a⟫ (the dual/feature-space view of kernel ridge). ★ kernel_erm_squaredLoss_excess_rate
Kernel / L²-ball linear predictors — squared-loss excess-risk rate
The genuine squared-loss statistical rate for empirical risk minimization over an
L²-norm-bounded class of linear predictors a ↦ ⟪w, a⟫ (the dual/feature-space view of
kernel ridge). Unlike the bare-linear-functional version, the loss here is the regression
loss (⟪w, x⟩ − y)².
The Rademacher complexity of the squared-loss class is bounded by decomposing the centered
loss (⟪w,x⟩ − y)² − y² = ⟪w,x⟩² − 2y⟪w,x⟩:
* the quadratic part ⟪w,x⟩² is handled by the (infinite-index) Ledoux–Talagrand
contraction with the clamped square as the Lipschitz surrogate, reducing to the linear
L²-ball bound;
* the cross part 2y⟪w,x⟩ = ⟪w, 2y·x⟩ is itself a linear class over rescaled features,
handled directly by the linear L²-ball bound.
Combined with the generic ERM oracle inequality (erm_oracle_inequality_separable) this gives
the O(1/√n) squared-loss excess-risk rate kernel_erm_squaredLoss_excess_rate.
Feature × response data space: Xb-ball features paired with [-Yb, Yb] responses.
Definition (Lean source)
The W-ball of weight vectors.
Definition (Lean source)
Kernel ERM squared-loss excess-risk rate over the L² ball. For data pairing features in the closed Xb-ball with responses in [-Yb, Yb], and linear predictors indexed by the closed W-ball, if Xb is nonnegative, Yb is nonnegative, W is nonnegative, the data map X is measurable, the constant t satisfies the calibration t·((Xb·W)² + 2·Yb·Xb·W)² ≤ 1/2, the tolerance ε is nonnegative, and the estimator ŵ attains empirical squared loss no larger than that of the comparator wstar, then for the squared loss (⟪w,x⟩ − y)², the probability that the excess population risk of ŵ over wstar exceeds 4·(4(XbW)² + 2·Yb·Xb·W)/√n + 2ε is at most exp(-ε²tn).