Representer theorem

DefinitionRegularized risk in a reproducing kernel Hilbert space#✓fully proved

The regularized risk L (f x₁, …, f xₙ) + Ω ‖f‖ of f in the RKHS H.

noncomputable def regularizedRisk (x : Fin n → X) (L : (Fin n → V) → ℝ) (Ω : ℝ → ℝ) (f : H) :
    ℝ :=
  L (fun i => f (x i)) + Ω ‖f‖

Used by 5

Used byThe representer theorem · Existence of a minimizer · Uniqueness of the minimizer · Kernel ridge objective as a regularized risk · The representer theorem

DefinitionKernel expansion map centered at the sample points#✓fully proved

The kernel expansion map c ↦ ∑ i, kerFun H (x i) (c i). Its range is the span of the kernel functions at the sample points x i.

noncomputable def kernelExpansion (x : Fin n → X) : (Fin n → V) →L[𝕜] H :=
  ∑ i, kerFun H (x i) ∘L ContinuousLinearMap.proj i

Used by 8

Used byKernel ridge fit is the unique minimizer · The representer theorem · Existence of a minimizer · Values of a kernel expansion at the sample points · Kernel ridge regression fit · Fitted values of kernel ridge regression · Kernel ridge regression · The representer theorem

TheoremThe representer theorem#✓fully proved

The representer theorem (closed-span form): if Ω is strictly increasing on [0, ∞), every global minimizer of the regularized risk lies in the closure of the span of the kernel functions at the sample points.

theorem mem_topologicalClosure_range_of_isMinimizer {x : Fin n → X} {L : (Fin n → V) → ℝ}
    {Ω : ℝ → ℝ} (hΩ : StrictMonoOn Ω (Set.Ici 0)) {f : H}
    (hf : ∀ g : H, regularizedRisk H x L Ω f ≤ regularizedRisk H x L Ω g) :
    f ∈ (LinearMap.range (kernelExpansion H x).toLinearMap).topologicalClosure

Uses 2 · Used by 1

Statement usesKernel expansion map centered at the sample points · Regularized risk in a reproducing kernel Hilbert space

Used byThe representer theorem

TheoremThe representer theorem#✓fully proved

The representer theorem (Schölkopf, Herbrich and Smola, Theorem 1): for a finite-dimensional output space V (for instance a scalar kernel, V = 𝕜) and Ω strictly increasing on [0, ∞), every global minimizer of L (f x₁, …, f xₙ) + Ω ‖f‖ is a kernel expansion ∑ i, kerFun H (x i) (c i).

theorem exists_eq_kernelExpansion_of_isMinimizer [FiniteDimensional 𝕜 V] {x : Fin n → X}
    {L : (Fin n → V) → ℝ} {Ω : ℝ → ℝ} (hΩ : StrictMonoOn Ω (Set.Ici 0)) {f : H}
    (hf : ∀ g : H, regularizedRisk H x L Ω f ≤ regularizedRisk H x L Ω g) :
    ∃ c : Fin n → V, f = kernelExpansion H x c

Uses 3

Statement usesKernel expansion map centered at the sample points · Regularized risk in a reproducing kernel Hilbert space

Proof usesThe representer theorem

TheoremExistence of a minimizer#✓fully proved

For finite-dimensional V, a continuous loss bounded below, and a continuous regularizer that is monotone on [0, ∞) and tends to ∞, the regularized risk has a global minimizer, and it can be taken to be a kernel expansion.

theorem exists_kernelExpansion_isMinimizer [FiniteDimensional 𝕜 V] (x : Fin n → X)
    {L : (Fin n → V) → ℝ} (hL : Continuous L) (hLb : BddBelow (Set.range L)) {Ω : ℝ → ℝ}
    (hΩc : Continuous Ω) (hΩm : MonotoneOn Ω (Set.Ici 0)) (hΩt : Tendsto Ω atTop atTop) :
    ∃ c : Fin n → V, ∀ g : H,
      regularizedRisk H x L Ω (kernelExpansion H x c) ≤ regularizedRisk H x L Ω g

Uses 2

Statement usesKernel expansion map centered at the sample points · Regularized risk in a reproducing kernel Hilbert space

TheoremUniqueness of the minimizer#✓fully proved

Uniqueness of the minimizer (real scalars): for a convex loss L and a regularizer Ω that is strictly convex and monotone on [0, ∞) (for instance Ω t = λ t² with λ > 0), the regularized risk has at most one global minimizer.

theorem isMinimizer_unique {x : Fin n → X} {L : (Fin n → V) → ℝ} (hL : ConvexOn ℝ Set.univ L)
    {Ω : ℝ → ℝ} (hΩc : StrictConvexOn ℝ (Set.Ici 0) Ω) (hΩm : MonotoneOn Ω (Set.Ici 0))
    {f₁ f₂ : H} (h₁ : ∀ g : H, regularizedRisk H x L Ω f₁ ≤ regularizedRisk H x L Ω g)
    (h₂ : ∀ g : H, regularizedRisk H x L Ω f₂ ≤ regularizedRisk H x L Ω g) : f₁ = f₂

Uses 1

Statement usesRegularized risk in a reproducing kernel Hilbert space

DefinitionKernel Gram matrix#✓fully proved

The Gram matrix K i j = k(x i, x j) of a real scalar kernel at the sample points, where k(x, y) = kernel H x y 1.

noncomputable def kernelGram (x : Fin n → X) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j => kernel H (x i) (x j) 1

Used by 7

Used byKernel ridge fit is the unique minimizer · Values of a kernel expansion at the sample points · Kernel ridge regression fit · Fitted values of kernel ridge regression · Kernel ridge regression · Kernel Gram matrix is positive semidefinite · Kernel ridge regression = GBLUP = RR-BLUP

DefinitionKernel ridge regression objective#✓fully proved

The kernel ridge objective ∑ i, (y i - f (x i))² + λ ‖f‖².

noncomputable def kernelRidgeRisk (x : Fin n → X) (y : Fin n → ℝ) (lam : ℝ) (f : H) : ℝ :=
  ∑ i, (y i - f (x i)) ^ 2 + lam * ‖f‖ ^ 2

Used by 3

Used byKernel ridge fit is the unique minimizer · Kernel ridge objective as a regularized risk · Kernel ridge regression

DefinitionKernel ridge regression fit#✓fully proved

The kernel ridge fit: the kernel expansion with coefficients (K + λ I)⁻¹ y.

noncomputable def kernelRidgeFit (x : Fin n → X) (y : Fin n → ℝ) (lam : ℝ) : H :=
  kernelExpansion H x ((kernelGram H x + lam • (1 : Matrix (Fin n) (Fin n) ℝ))⁻¹ *ᵥ y)

Uses 2 · Used by 4

Statement usesKernel expansion map centered at the sample points · Kernel Gram matrix

Used byKernel ridge fit is the unique minimizer · Fitted values of kernel ridge regression · Kernel ridge regression · Kernel ridge regression = GBLUP = RR-BLUP

TheoremKernel ridge objective as a regularized risk#✓fully proved

The kernel ridge objective is the regularized risk with the squared loss and Ω t = λ t².

theorem kernelRidgeRisk_eq_regularizedRisk (x : Fin n → X) (y : Fin n → ℝ) (lam : ℝ) (f : H) :
    kernelRidgeRisk H x y lam f =
      regularizedRisk H x (fun v => ∑ i, (y i - v i) ^ 2) (fun t => lam * t ^ 2) f

Uses 2

Statement usesKernel ridge regression objective · Regularized risk in a reproducing kernel Hilbert space

TheoremValues of a kernel expansion at the sample points#✓fully proved

The values of a kernel expansion at the sample points are K c.

theorem kernelExpansion_apply_sample (x : Fin n → X) (c : Fin n → ℝ) (j : Fin n) :
    kernelExpansion H x c (x j) = (kernelGram H x *ᵥ c) j

Uses 2 · Used by 3

Statement usesKernel expansion map centered at the sample points · Kernel Gram matrix

Used byKernel ridge fit is the unique minimizer · Fitted values of kernel ridge regression · Kernel ridge regression

TheoremKernel Gram matrix is positive semidefinite#✓fully proved

The kernel Gram matrix is positive semidefinite.

theorem posSemidef_kernelGram (x : Fin n → X) : (kernelGram H x).PosSemidef

Uses 1 · Used by 2

Statement usesKernel Gram matrix

Used byKernel ridge fit is the unique minimizer · Kernel ridge regression

TheoremFitted values of kernel ridge regression#✓fully proved

The fitted values of kernel ridge regression are K (K + λ I)⁻¹ y.

theorem kernelRidgeFit_apply (x : Fin n → X) (y : Fin n → ℝ) (lam : ℝ) (j : Fin n) :
    kernelRidgeFit H x y lam (x j) =
      ((kernelGram H x * (kernelGram H x + lam • (1 : Matrix (Fin n) (Fin n) ℝ))⁻¹) *ᵥ y) j

Uses 4 · Used by 1

Statement usesKernel Gram matrix · Kernel ridge regression fit

Proof usesKernel expansion map centered at the sample points · Values of a kernel expansion at the sample points

Used byKernel ridge regression = GBLUP = RR-BLUP

TheoremKernel ridge regression#✓fully proved

Kernel ridge regression (Kimeldorf and Wahba): for λ > 0 the kernel ridge fit minimizes ∑ i, (y i - f (x i))² + λ ‖f‖² over the whole RKHS.

theorem kernelRidgeRisk_kernelRidgeFit_le (x : Fin n → X) (y : Fin n → ℝ) {lam : ℝ}
    (hlam : 0 < lam) (g : H) :
    kernelRidgeRisk H x y lam (kernelRidgeFit H x y lam) ≤ kernelRidgeRisk H x y lam g

Uses 6

Statement usesKernel ridge regression fit · Kernel ridge regression objective

Proof usesKernel expansion map centered at the sample points · Values of a kernel expansion at the sample points · Kernel Gram matrix · Kernel Gram matrix is positive semidefinite

TheoremKernel ridge fit is the unique minimizer#✓fully proved

The kernel ridge fit is the unique minimizer for λ > 0.

theorem eq_kernelRidgeFit_of_le (x : Fin n → X) (y : Fin n → ℝ) {lam : ℝ} (hlam : 0 < lam)
    {g : H}
    (hg : kernelRidgeRisk H x y lam g ≤ kernelRidgeRisk H x y lam (kernelRidgeFit H x y lam)) :
    g = kernelRidgeFit H x y lam

Uses 6

Statement usesKernel ridge regression fit · Kernel ridge regression objective

Proof usesKernel expansion map centered at the sample points · Values of a kernel expansion at the sample points · Kernel Gram matrix · Kernel Gram matrix is positive semidefinite

TheoremProjection onto Riesz representers with Pythagorean residual#✓fully proved

Orthogonal projection onto the span of the Riesz representers preserves the values of the functionals, and the Pythagorean identity holds for the residual.

theorem exists_mem_span_norm_sq_add {ι : Type*} [Fintype ι]
    (L : ι → (H →L[ℝ] ℝ)) (g : H) :
    ∃ s ∈ Submodule.span ℝ (Set.range fun i => (InnerProductSpace.toDual ℝ H).symm (L i)),
      (∀ i, L i s = L i g) ∧ ‖g‖ ^ 2 = ‖s‖ ^ 2 + ‖g - s‖ ^ 2

Used by 2

Used byProjection onto Riesz representers does not increase the norm · Representer theorem

TheoremProjection onto Riesz representers does not increase the norm#✓fully proved

Orthogonal projection onto the span of the Riesz representers does not increase the norm.

theorem exists_mem_span_values_eq_norm_le {ι : Type*} [Fintype ι]
    (L : ι → (H →L[ℝ] ℝ)) (g : H) :
    ∃ s ∈ Submodule.span ℝ (Set.range fun i => (InnerProductSpace.toDual ℝ H).symm (L i)),
      (∀ i, L i s = L i g) ∧ ‖s‖ ≤ ‖g‖

Uses 1

Proof usesProjection onto Riesz representers with Pythagorean residual

TheoremRepresenter theorem#✓fully proved

Any minimizer of a ridge-regularized problem F (fun i => L i g) + Λ * ‖g‖ ^ 2 with Λ > 0 lies in the span of the Riesz representers of the functionals L i.

theorem mem_span_of_isMinOn {ι : Type*} [Fintype ι]
    (L : ι → (H →L[ℝ] ℝ)) (F : (ι → ℝ) → ℝ) {Λ : ℝ} (hΛ : 0 < Λ) {f : H}
    (hf : IsMinOn (fun g : H => F (fun i => L i g) + Λ * ‖g‖ ^ 2) Set.univ f) :
    f ∈ Submodule.span ℝ (Set.range fun i => (InnerProductSpace.toDual ℝ H).symm (L i))

Uses 1

Proof usesProjection onto Riesz representers with Pythagorean residual

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.