Reproducing Kernel Hilbert Spaces

This file defines vector-valued reproducing Kernel Hilbert spaces, which are Hilbert spaces of functions, as well as characterizing these spaces in terms of infinite-dimensional positive semidefinite matrices.

Main results

• RKHS: the class of reproducing kernel Hilbert spaces
• RKHS.kernel: the kernel of a RKHS as a matrix.
• RKHS.kerFun: the kernel functions of a RKHS.
• RKHS.kerFun_dense: the kernel functions are dense in the Hilbert space.
• RKHS.posSemidef_kernel: The kernel is positive semidefinite.
• RKHS.OfKernel: RKHS constructed from a positive semidefinite matrix.
• RKHS.kernel_ofKernel: The kernel of the constructed RKHS is equal to the matrix, this is essentially Moore's theorem.

TODO

• Privatize RKHS.H₀

References

• [Paulsen, Vern I. and Raghupathi, Mrinal, An introduction to the theory of reproducing kernel Hilbert spaces][MR3526117]

class RKHS (𝕜 : outParam (Type u_1)) (H : Type u_2) (X : outParam (Type u_3)) (V : outParam (Type u_4)) [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] : Type (max (max u_2 u_3) u_4)

A reproducing kernel Hilbert space is a Hilbert space with an injection to functions mapping into another Hilbert space, such that point evaluation is continuous.

• coeCLM : H →L[𝕜] X → V

  Continuous injection to functions from the reproducing kernel Hilbert space H to functions from the domain X to the Hilbert space V

• coeCLM_injective : Function.Injective ⇑(coeCLM 𝕜)

@[instance_reducible]

instance RKHS.instFunLike {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] : FunLike H X V

Each element of a reproducing kernel Hilbert space may be coerced into a function.

Equations

• RKHS.instFunLike = { coe := fun (f : H) => (RKHS.coeCLM 𝕜) f, coe_injective := ⋯ }

theorem RKHS.ext {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] {f g : H} (h : ∀ (x : X), f x = g x) : f = g

theorem RKHS.ext_iff {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] {f g : H} : f = g ↔ ∀ (x : X), f x = g x

@[simp]

theorem RKHS.coeCLM_apply {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] (f : H) : (coeCLM 𝕜) f = ⇑f

@[simp]

theorem RKHS.coe_zero {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] : ⇑0 = 0

@[simp]

theorem RKHS.coe_add {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] (f g : H) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem RKHS.coe_sub {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] (f g : H) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem RKHS.coe_neg {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] (f : H) : ⇑(-f) = -⇑f

@[simp]

theorem RKHS.coe_smul {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] (f : H) (c : 𝕜) : ⇑(c • f) = c • ⇑f

@[simp]

theorem RKHS.continuous_eval {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] (x : X) : Continuous fun (f : H) => f x

noncomputable def RKHS.kerFun {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x : X) : V →L[𝕜] H

The kernel functions of a reproducing kernel Hilbert space are the adjoint of the point evaluation.

Equations

• RKHS.kerFun H x = ContinuousLinearMap.adjoint (ContinuousLinearMap.proj x ∘SL RKHS.coeCLM 𝕜)

noncomputable def RKHS.kernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] : Matrix X X (V →L[𝕜] V)

The kernel of a reproducing kernel Hilbert space is a matrix of entries given by the kernel functions.

Equations

• RKHS.kernel H = Matrix.of fun (x y : X) => ContinuousLinearMap.adjoint (RKHS.kerFun H x) ∘SL RKHS.kerFun H y

theorem RKHS.kerFun_apply {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (y : X) (v : V) (x : X) : ((kerFun H y) v) x = (kernel H x y) v

theorem RKHS.kernel_apply {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x y : X) : kernel H x y = ContinuousLinearMap.adjoint (kerFun H x) ∘SL kerFun H y

@[simp]

theorem RKHS.adjoint_kerFun {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x : X) (f : H) : (ContinuousLinearMap.adjoint (kerFun H x)) f = f x

Point evaluation f ↦ f x is the adjoint of the kernel function kerFun H x.

@[simp]

theorem RKHS.kerFun_inner {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x : X) (v : V) (f : H) : inner 𝕜 ((kerFun H x) v) f = inner 𝕜 v (f x)

The "reproducing" property of the kernel functions, left version.

@[simp]

theorem RKHS.inner_kerFun {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x : X) (v : V) (f : H) : inner 𝕜 f ((kerFun H x) v) = inner 𝕜 (f x) v

The "reproducing" property of the kernel functions, right version.

theorem RKHS.kernel_inner {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x y : X) (v w : V) : inner 𝕜 ((kernel H x y) v) w = inner 𝕜 ((kerFun H y) v) ((kerFun H x) w)

The "reproducing" property of the kernel.

theorem RKHS.norm_kernel_eq_norm_kerFun_sq {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x : X) : ‖kernel H x x‖ = ‖kerFun H x‖ ^ 2

theorem RKHS.norm_kerFun_eq_sqrt_norm_kernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x : X) : ‖kerFun H x‖ = √‖kernel H x x‖

theorem RKHS.norm_kernel_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x y : X) : ‖kernel H x y‖ ≤ √‖kernel H x x‖ * √‖kernel H y y‖

theorem RKHS.norm_kernel_sq_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (x y : X) : ‖kernel H x y‖ ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖

theorem RKHS.norm_apply_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] (f : H) (x : X) : ‖f x‖ ≤ ‖f‖ * √‖kernel H x x‖

The evaluation of an element f of a reproducing kernel Hilbert space at a point x is bounded by ‖f‖ times the square root of the kernel diagonal ‖kernel H x x‖ at x.

theorem RKHS.tendstoUniformlyOn_of_norm_kerFun_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] {C : ℝ} {s : Set X} (hC : ∀ x ∈ s, ‖kerFun H x‖ ≤ C) {ι : Type u_5} {l : Filter ι} {F : ι → H} {f : H} (h : Filter.Tendsto F l (nhds f)) : TendstoUniformlyOn (fun (n : ι) => ⇑(F n)) (⇑f) l s

If the kernel functions are uniformly bounded on a set s (‖kerFun H x‖ ≤ C for x ∈ s), then convergence in H-norm implies uniform convergence of the underlying functions on s.

theorem RKHS.tendstoUniformly_of_norm_kerFun_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] {C : ℝ} (hC : ∀ (x : X), ‖kerFun H x‖ ≤ C) {ι : Type u_5} {l : Filter ι} {F : ι → H} {f : H} (h : Filter.Tendsto F l (nhds f)) : TendstoUniformly (fun (n : ι) => ⇑(F n)) (⇑f) l

If the kernel functions are uniformly bounded (‖kerFun H x‖ ≤ C for all x), then convergence in H-norm implies uniform convergence of the underlying functions.

theorem RKHS.kerFun_dense {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] : (Submodule.span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1) v = x}).topologicalClosure = ⊤

The span of the kernel functions is dense.

theorem RKHS.isHermitian_kernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] : (kernel H).IsHermitian

theorem RKHS.posSemidef_kernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [RKHS 𝕜 H X V] [CompleteSpace H] [CompleteSpace V] : (kernel H).PosSemidef

The kernel is a positive semidefinite matrix.

Construction of RKHS from kernel

theorem RKHS.posSemidef_tfae {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} : [K.PosSemidef, K.IsHermitian ∧ ∀ (f : X × V →₀ 𝕜), 0 ≤ RCLike.re (f.sum fun (xv : X × V) (z : 𝕜) => f.sum fun (xv' : X × V) (w : 𝕜) => (starRingEnd 𝕜) z * w * inner 𝕜 ((K xv'.1 xv.1) xv.2) xv'.2), K.IsHermitian ∧ ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun (x : X) (w : V) => vv.sum fun (x' : X) (w' : V) => inner 𝕜 ((K x' x) w) w')].TFAE

@[reducible, inline]

abbrev RKHS.H₀ {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (K : Matrix X X (V →L[𝕜] V)) : Type (max u_1 u_3 u_2)

Auxiliary construction for OfKernel. TODO: Privatize

Equations

• RKHS.H₀ K = (X × V →₀ 𝕜)

@[instance_reducible]

instance RKHS.instPreInnerProductSpaceCoreH₀ {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} [Fact K.PosSemidef] : PreInnerProductSpace.Core 𝕜 (H₀ K)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RKHS.instSeminormedAddCommGroupH₀ {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} [Fact K.PosSemidef] : SeminormedAddCommGroup (H₀ K)

Equations

• RKHS.instSeminormedAddCommGroupH₀ = InnerProductSpace.Core.toSeminormedAddCommGroup

@[instance_reducible]

noncomputable instance RKHS.instInnerProductSpaceH₀ {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} [Fact K.PosSemidef] : InnerProductSpace 𝕜 (H₀ K)

Equations

• RKHS.instInnerProductSpaceH₀ = InnerProductSpace.ofCore RKHS.instPreInnerProductSpaceCoreH₀

@[reducible, inline]

abbrev RKHS.OfKernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (K : Matrix X X (V →L[𝕜] V)) [Fact K.PosSemidef] : Type (max (max u_3 u_2) u_1)

The reproducing kernel Hilbert space generated by a positive semidefinite matrix. TODO: Make nonexposed def once deriving is fixed. See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/578850754

Equations

• RKHS.OfKernel K = UniformSpace.Completion (RKHS.H₀ K)

@[instance_reducible]

noncomputable instance RKHS.OfKernel.instRKHS {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} [Fact K.PosSemidef] : RKHS 𝕜 (OfKernel K) X V

Equations

• RKHS.OfKernel.instRKHS = { coeCLM := ContinuousLinearMap.pi fun (x : X) => ContinuousLinearMap.adjoint (RKHS.OfKernel.kerFun✝ K x), coeCLM_injective := ⋯ }

@[simp]

theorem RKHS.OfKernel.kernel_ofKernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} [Fact K.PosSemidef] : kernel (OfKernel K) = K

The kernel of the reproducing kernel Hilbert space generated by a positive semidefinite matrix is the original positive semidefinite matrix.