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 definitions

• RKHS: the class of reproducing kernel Hilbert spaces
• RKHS.eval: the evaluation operator of a RKHS.
• RKHS.kerFun: the kernel functions of a RKHS.
• RKHS.kernel: the kernel of a RKHS as a matrix.
• RKHS.OfKernel: RKHS constructed from a positive semidefinite matrix.
• RKHS.outerKernel: the kernel generated from a function f : X → V with the rank-one operators ⟪f y, ·⟫ • f x as its entries.

Main results

• RKHS.kerFun_dense: the kernel functions are dense in the Hilbert space.
• RKHS.posSemidef_kernel: The kernel is positive semidefinite.
• RKHS.continuous_tfae: The joint continuity of the kernel, the continuity of the evaluation map and continuity of the kernel functions are all equivalent.
• RKHS.kernel_ofKernel: The kernel of the constructed RKHS OfKernel is equal to the matrix, this is essentially Moore's theorem.
• RKHS.RKHSSubmodule: a complete submodule of an RKHS is again an RKHS.
• RKHS.kerFun_submodule: the kernel functions of a submodule RKHS are an orthogonal projection of the kernel functions of the full RKHS.
• RKHS.kernel_submodule: the kernel of the submodule RKHS is formed by composing the adjoint of the kernel function of the full RKHS with a star projection acting on the kernel function of the full RKHS.

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, macro_inline]

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

def RKHS.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) : H →L[𝕜] V

Point evaluation fun f ↦ f x.

Equations

• RKHS.eval H x = ContinuousLinearMap.proj x ∘SL RKHS.coeCLM 𝕜

theorem RKHS.eval_def {𝕜 : 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) : eval H x = ContinuousLinearMap.proj x ∘SL coeCLM 𝕜

@[simp]

theorem RKHS.eval_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] (x : X) (f : H) : (eval H x) f = f x

theorem RKHS.continuous_eval_const {𝕜 : 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

@[deprecated RKHS.continuous_eval_const (since := "2026-08-19")]

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

Alias of RKHS.continuous_eval_const.

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 (RKHS.eval H x)

theorem RKHS.kerFun_eq_adjoint_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] [CompleteSpace H] [CompleteSpace V] (x : X) : kerFun H x = ContinuousLinearMap.adjoint (eval H x)

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

@[simp]

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_kerFun_sub_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 y : X) : ‖kerFun H x - kerFun H y‖ ^ 2 = ‖kernel H x x - kernel H y x - kernel H x y + kernel H y y‖

theorem RKHS.norm_kerFun_sub_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 y : X) : ‖kerFun H x - kerFun H y‖ = √‖kernel H x x - kernel H y x - kernel H x y + kernel H y y‖

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.continuous_kernel_tfae {𝕜 : 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] [TopologicalSpace X] : [Continuous fun (p : X × X) => kernel H p.1 p.2, Continuous (kerFun H), Continuous fun (x : X) => eval H x].TFAE

theorem RKHS.continuous_kernel_iff_continuous_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] [TopologicalSpace X] : (Continuous fun (p : X × X) => kernel H p.1 p.2) ↔ Continuous (kerFun H)

theorem RKHS.continuous_eval_iff_continuous_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] [TopologicalSpace X] : (Continuous fun (x : X) => eval H x) ↔ Continuous (kerFun H)

theorem RKHS.continuous_kernel_iff_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] [CompleteSpace H] [CompleteSpace V] [TopologicalSpace X] : (Continuous fun (p : X × X) => kernel H p.1 p.2) ↔ Continuous fun (x : X) => eval H x

theorem RKHS.continuous_of_continuous_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] [TopologicalSpace X] (h : Continuous fun (p : X × X) => kernel H p.1 p.2) (f : H) : Continuous ⇑f

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.

instance RKHS.instFactPosSemidefContinuousLinearMapIdKernel {𝕜 : 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] : Fact (kernel H).PosSemidef

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

theorem RKHS.posSemidef_iff_re_sum_kernel {𝕜 : 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)

theorem RKHS.posSemidef_iff_re_sum_kernel' {𝕜 : 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 ∧ ∀ (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')

theorem Matrix.PosSemidef.re_sum_kernel {𝕜 : 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)} (h : K.PosSemidef) (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)

theorem Matrix.PosSemidef.re_sum_kernel' {𝕜 : 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)} (h : K.PosSemidef) (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')

@[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 (max u_3 u_2) u_1)

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.

noncomputable def RKHS.equiv {𝕜 : 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] {H' : Type u_5} [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [CompleteSpace H'] [RKHS 𝕜 H' X V] (h : kernel H = kernel H') : H ≃ₗᵢ[𝕜] H'

If the two RKHS have the same kernel, then they are isometrically isomorphic.

Equations

• RKHS.equiv h = (RKHS.OfKernel.equivAux✝ ⋯).symm.trans (RKHS.OfKernel.equivAux✝ h)

theorem RKHS.equiv_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] {H' : Type u_5} [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [CompleteSpace H'] [RKHS 𝕜 H' X V] (h : kernel H = kernel H') (x : X) (v : V) : (equiv h) ((kerFun H x) v) = (kerFun H' x) v

@[simp]

theorem RKHS.coe_equiv {𝕜 : 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] {H' : Type u_5} [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [CompleteSpace H'] [RKHS 𝕜 H' X V] (h : kernel H = kernel H') (f : H) : ⇑((equiv h) f) = ⇑f

If the two RKHS have the same kernel, then the functions in the RKHSs agree as functions on X → V.

@[instance_reducible]

instance RKHS.instRKHSSubmodule {𝕜 : 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] (H₀ : Submodule 𝕜 H) : RKHS 𝕜 (↥H₀) X V

Equations

• RKHS.instRKHSSubmodule H₀ = { coeCLM := RKHS.coeCLM 𝕜 ∘SL H₀.subtypeL, coeCLM_injective := ⋯ }

@[simp]

theorem RKHS.coe_coe {𝕜 : 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] (H₀ : Submodule 𝕜 H) (f : ↥H₀) : ⇑↑f = ⇑f

theorem RKHS.kerFun_submodule {𝕜 : 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] (H₀ : Submodule 𝕜 H) [CompleteSpace ↥H₀] (x : X) : kerFun (↥H₀) x = H₀.orthogonalProjectionOnto ∘SL kerFun H x

theorem RKHS.kernel_submodule {𝕜 : 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] (H₀ : Submodule 𝕜 H) [CompleteSpace ↥H₀] (x y : X) : kernel (↥H₀) x y = ContinuousLinearMap.adjoint (kerFun H x) ∘SL H₀.starProjection ∘SL kerFun H y

theorem RKHS.kernel_orthogonal {𝕜 : 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] (H₀ : Submodule 𝕜 H) [CompleteSpace ↥H₀] : kernel ↥H₀ᗮ = kernel H - kernel ↥H₀

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

The kernel generated from a function f : X → V with the rank-one operators ⟪f y, ·⟫ • f x as its entries.

Equations

• RKHS.outerKernel 𝕜 f = Matrix.of fun (x y : X) => ((InnerProductSpace.rankOne 𝕜) (f x)) (f y)

@[simp]

theorem RKHS.outerKernel_apply (𝕜 : Type u_1) [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : X → V) (x y : X) : outerKernel 𝕜 f x y = ((InnerProductSpace.rankOne 𝕜) (f x)) (f y)

@[simp]

theorem RKHS.outerKernel_zero {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] : outerKernel 𝕜 0 = 0

theorem RKHS.outerKernel_inner (𝕜 : Type u_1) [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : X → V) (x y : X) (u v : V) : inner 𝕜 ((outerKernel 𝕜 f x y) u) v = (starRingEnd 𝕜) (inner 𝕜 (f y) u) * inner 𝕜 (f x) v

theorem RKHS.inner_outerKernel (𝕜 : Type u_1) [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : X → V) (x y : X) (u v : V) : inner 𝕜 u ((outerKernel 𝕜 f x y) v) = (starRingEnd 𝕜) (inner 𝕜 v (f y)) * inner 𝕜 u (f x)

theorem RKHS.posSemidef_outerKernel (𝕜 : Type u_1) [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (f : X → V) : (outerKernel 𝕜 f).PosSemidef

instance RKHS.instFactPosSemidefContinuousLinearMapIdOuterKernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (f : X → V) : Fact (outerKernel 𝕜 f).PosSemidef

theorem RKHS.kernel_span_singleton {𝕜 : 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) : kernel ↥(𝕜 ∙ f) = (↑‖f‖)⁻¹ ^ 2 • outerKernel 𝕜 ⇑f

theorem RKHS.posSemidef_norm_sq_smul_kernel_sub_outerKernel {𝕜 : 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] (f : OfKernel K) : (↑‖f‖ ^ 2 • K - outerKernel 𝕜 ⇑f).PosSemidef