Kolmogorov decomposition of a positive-definite kernel

This file constructs the canonical Hilbert-space realization of a scalar-valued positive-definite kernel. A kernel K : α → α → 𝕜 is first regarded as the operator-valued kernel whose (a, b) entry is multiplication by K a b on the one-dimensional Hilbert space 𝕜. Mathlib's RKHS.OfKernel construction then gives a Hilbert space and kernel vectors Φ a satisfying

⟪Φ a, Φ b⟫_𝕜 = K a b.

The span of the kernel vectors is dense, so this is the minimal Kolmogorov decomposition rather than an arbitrary realization. Its universal property gives a unique linear isometry into any other realization, and a linear isometric equivalence when that realization is also minimal.

The completion and reproducing-kernel construction are Mathlib's RKHS.OfKernel; this file supplies the scalar-kernel bridge and its characteristic API.

Main declarations

• TauCeti.positiveDefiniteKernelOperator: regard a scalar kernel as an operator-valued kernel.
• TauCeti.posSemidef_positiveDefiniteKernelOperator: positivity of that operator kernel.
• Matrix.PosSemidef.KolmogorovSpace: the canonical Hilbert space.
• Matrix.PosSemidef.kolmogorovFeature: its canonical feature map.
• Matrix.PosSemidef.inner_kolmogorovFeature: the Kolmogorov identity.
• Matrix.PosSemidef.kolmogorovFeature_dense: minimality of the decomposition.
• Matrix.PosSemidef.kolmogorovIsometry: the universal comparison isometry.
• Matrix.PosSemidef.kolmogorovEquiv: equivalence with any other minimal realization.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups, Springer GTM 100 (1984), Chapter 3.

noncomputable def TauCeti.positiveDefiniteKernelOperator {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (K : α → α → 𝕜) : Matrix α α (𝕜 →L[𝕜] 𝕜)

A scalar kernel regarded as an operator-valued kernel on the one-dimensional Hilbert space 𝕜: the entry at (a, b) is left multiplication by K a b.

Equations

• TauCeti.positiveDefiniteKernelOperator K = Matrix.of fun (a b : α) => (ContinuousLinearMap.mul 𝕜 𝕜) (K a b)

@[simp]

theorem TauCeti.positiveDefiniteKernelOperator_apply {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (K : α → α → 𝕜) (a b : α) (z : 𝕜) : (positiveDefiniteKernelOperator K a b) z = K a b * z

theorem TauCeti.posSemidef_positiveDefiniteKernelOperator {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : Matrix.PosSemidef K) : (positiveDefiniteKernelOperator K).PosSemidef

The operator-valued kernel obtained from a scalar positive-definite kernel is positive semidefinite. This is the bridge needed by Mathlib's RKHS.OfKernel construction.

@[reducible, inline]

noncomputable abbrev Matrix.PosSemidef.KolmogorovSpace {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : PosSemidef K) : Type (max u v)

The canonical Hilbert space in the Kolmogorov decomposition of K.

This is an abbreviation because Mathlib's RKHS.OfKernel currently has to be an abbreviation in order for its normed-group and inner-product instances to reduce.

Equations

• hK.KolmogorovSpace = RKHS.OfKernel (TauCeti.positiveDefiniteKernelOperator K)

noncomputable def Matrix.PosSemidef.kolmogorovFeature {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : PosSemidef K) (a : α) : hK.KolmogorovSpace

The canonical feature map into the Kolmogorov space. It sends a to the reproducing-kernel vector at a, evaluated on the scalar 1.

Equations

• hK.kolmogorovFeature a = (RKHS.kerFun hK.KolmogorovSpace a) 1

@[simp]

theorem Matrix.PosSemidef.inner_kolmogorovFeature {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : PosSemidef K) (a b : α) : inner 𝕜 (hK.kolmogorovFeature a) (hK.kolmogorovFeature b) = K a b

Kolmogorov identity. Inner products of the canonical feature vectors recover the original kernel.

@[simp]

theorem Matrix.PosSemidef.norm_kolmogorovFeature_sq {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : PosSemidef K) (a : α) : ‖hK.kolmogorovFeature a‖ ^ 2 = RCLike.re (K a a)

The squared norm of a canonical feature vector is the real part of the corresponding diagonal kernel value.

@[simp]

theorem Matrix.PosSemidef.norm_kolmogorovFeature_sub_sq {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : PosSemidef K) (a b : α) : ‖hK.kolmogorovFeature a - hK.kolmogorovFeature b‖ ^ 2 = RCLike.re (K a a) - 2 * RCLike.re (K a b) + RCLike.re (K b b)

The squared distance between two canonical feature vectors, expressed entirely in terms of the original kernel.

theorem Matrix.PosSemidef.kolmogorovFeature_dense {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : PosSemidef K) : (Submodule.span 𝕜 (Set.range hK.kolmogorovFeature)).topologicalClosure = ⊤

The canonical feature vectors have dense linear span in the Kolmogorov space. Thus the construction is minimal: it contains no orthogonal summand invisible to the kernel.

noncomputable def Matrix.PosSemidef.kolmogorovIsometry {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} {E : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (hK : PosSemidef K) (φ : α → E) (hφ : ∀ (a b : α), inner 𝕜 (φ a) (φ b) = K a b) : hK.KolmogorovSpace →ₗᵢ[𝕜] E

The unique linear isometry from the canonical Kolmogorov space into any Hilbert-space realization of K. It sends each canonical feature vector to the corresponding vector in the given realization.

Equations

• hK.kolmogorovIsometry φ hφ = { toLinearMap := ↑((Finsupp.linearCombination 𝕜 φ).extendOfNorm (Finsupp.linearCombination 𝕜 hK.kolmogorovFeature)), norm_map' := ⋯ }

@[simp]

theorem Matrix.PosSemidef.kolmogorovIsometry_apply {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} {E : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (hK : PosSemidef K) (φ : α → E) (hφ : ∀ (a b : α), inner 𝕜 (φ a) (φ b) = K a b) (a : α) : (hK.kolmogorovIsometry φ hφ) (hK.kolmogorovFeature a) = φ a

The universal comparison isometry sends canonical feature vectors to the vectors of the given realization.

theorem Matrix.PosSemidef.kolmogorovIsometry_unique {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} {E : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (hK : PosSemidef K) (φ : α → E) (hφ : ∀ (a b : α), inner 𝕜 (φ a) (φ b) = K a b) (T : hK.KolmogorovSpace →ₗᵢ[𝕜] E) (hT : ∀ (a : α), T (hK.kolmogorovFeature a) = φ a) : T = hK.kolmogorovIsometry φ hφ

A linear isometry out of the canonical Kolmogorov space is uniquely determined by its values on the canonical feature vectors.

theorem Matrix.PosSemidef.kolmogorovIsometry_surjective {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} {E : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (hK : PosSemidef K) (φ : α → E) (hφ : ∀ (a b : α), inner 𝕜 (φ a) (φ b) = K a b) (hφdense : (Submodule.span 𝕜 (Set.range φ)).topologicalClosure = ⊤) : Function.Surjective ⇑(hK.kolmogorovIsometry φ hφ)

If the vectors in a realization of K have dense linear span, the universal comparison isometry is surjective.

noncomputable def Matrix.PosSemidef.kolmogorovEquiv {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} {E : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (hK : PosSemidef K) (φ : α → E) (hφ : ∀ (a b : α), inner 𝕜 (φ a) (φ b) = K a b) (hφdense : (Submodule.span 𝕜 (Set.range φ)).topologicalClosure = ⊤) : hK.KolmogorovSpace ≃ₗᵢ[𝕜] E

The canonical Kolmogorov space is linearly isometric to every other minimal realization of the same kernel.

Equations

• hK.kolmogorovEquiv φ hφ hφdense = LinearIsometryEquiv.ofSurjective (hK.kolmogorovIsometry φ hφ) ⋯

@[simp]

theorem Matrix.PosSemidef.kolmogorovEquiv_apply {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} {E : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (hK : PosSemidef K) (φ : α → E) (hφ : ∀ (a b : α), inner 𝕜 (φ a) (φ b) = K a b) (hφdense : (Submodule.span 𝕜 (Set.range φ)).topologicalClosure = ⊤) (a : α) : (hK.kolmogorovEquiv φ hφ hφdense) (hK.kolmogorovFeature a) = φ a

The equivalence with another minimal realization sends canonical feature vectors to the vectors of that realization.