Formalize RKHS: Type error in constructing function space

Stream: new members

[Tjeerd Jan Heeringa]

I am trying to formalize into lean the reproducing kernel Hilbert spaces. I am doubting whether I set it up right, because my types doesn't match.

The problem here is that of going from the pre-RKHS H_{pre} to the RKHS H by taking the norm-closure of

$$H_{pre}= \{ x\mapsto k(x,y) | y\in X\}$$

where $K:X\times X\to \mathbb{R}$ is a positive semi-definite, symmetric function and the norm is induced by the semi-inner product on $H_{pre}$ given by

$$\langle\sum_{n}c_n K(x_n,\cdot), \sum_m d_m K(y_m,\cdot\rangle = \sum_n\sum_m c_m * d_m * K(x_n,y_m)$$

There is a unique pre-RKHS and RKHS for every kernel. I have the maps that take me from kernel to pre-RKHS, but the map from pre-RKHS to RKHS doesn't work out: in the line

def ofPreRKHS (K : Kernel X) (pre : PreRKHS X K) : RKHS H X

the H is not expected same type. Can you give me pointers to how to fix this?

Minimum working example:

import Mathlib

import Mathlib.Topology.Basic
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Topology.Continuous
import Mathlib.Data.Real.Basic

import Mathlib.Analysis.Normed.Group.Uniform
import Mathlib.Topology.Algebra.GroupCompletion
import Mathlib.Topology.MetricSpace.Completion

set_option autoImplicit true

open Real

variable {X H : Type*}
variable (x y : X)
variable (f : H)

structure Kernel X where
  kernel : X → X → ℝ
  symmetric : ∀ x y : X, kernel x y = kernel y x
  posSemiDef : ∀ (c : X →₀ ℝ), ∑ x ∈ c.support, ∑ y ∈ c.support, c x * c y * kernel x y ≥ 0

class PreRKHS X (K: Kernel X) where
  carrier : Submodule ℝ (X → ℝ) := Submodule.span ℝ (Set.range K.kernel)
  carrier_spec : carrier = Submodule.span ℝ (Set.range K.kernel)
  preInnerCore : PreInnerProductSpace.Core ℝ carrier
  seminormedAddCommGroup : SeminormedAddCommGroup carrier
  funLike : FunLike carrier X ℝ
  Ksec : X → carrier
  Ksec_spec : ∀ x y : X, (Ksec x) y = K.kernel x y

class RKHS H X
  extends Kernel X, NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H, FunLike H X ℝ
  where
    Ksec: X → H
    Ksec_spec : ∀ x y : X, (Ksec x) y = kernel y x
    reproducing : ∀ (x : X) (f : H), f x = inner f (Ksec x)

namespace RKHS

noncomputable def ofPreRKHS (K : Kernel X) (pre : PreRKHS X K) : RKHS H X := by
  let K_span := pre.carrier
  letI : SeminormedAddCommGroup K_span := InnerProductSpace.Core.toSeminormedAddCommGroup (c := pre.preInnerCore)
  letI : InnerProductSpace ℝ K_span := InnerProductSpace.ofCore pre.preInnerCore
  letI : UniformSpace K_span := PseudoMetricSpace.toUniformSpace

  let H := UniformSpace.Completion pre.carrier

  letI : CompleteSpace H := by infer_instance
  letI : NormedAddCommGroup H := UniformSpace.Completion.instNormedAddCommGroup K_span
  letI : InnerProductSpace ℝ H := UniformSpace.Completion.innerProductSpace
  letI : FunLike H X ℝ := sorry
  let rkhs : RKHS H X := sorry
  exact rkhs

end RKHS

(I have written out the proofs of the sorry bits but omitted them for brevity.)

[Yongxi Lin (Aaron)]

You have already declared H before your definition ofPreRKHS, and you let H := UniformSpace.Completion pre.carrier. This actually create two H s in your proof, which is the reason why you have type errors.

You probably want sth like

noncomputable def ofPreRKHS (K : Kernel X) (pre : PreRKHS X K) : RKHS (UniformSpace.Completion pre.carrier) X := by
  sorry

instead.

I also want to mention that this is also probably not the correct approach to define RKHS. The bounded pointwise evaluation functional definition (https://en.wikipedia.org/wiki/Reproducing_kernel_Hilbert_space) is easier to be implemented in Lean. And once you have this definition, you can show that the space you constructed from a kernel is an example of RKHS according to this definition.

[Tjeerd Jan Heeringa]

In my local code I actually have evaluation-based definition and the kernel-based definition. The evaluation-based definition of the RKHS is in lean 4 I use is

class RKHS H X
  extends NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H, FunLike H X ℝ
  where
    eval : X → H → ℝ := fun x => fun f => f x
    eval_bounded_linear : ∀ x, IsBoundedLinearMap ℝ (eval x)
    eval_spec : ∀ (x : X) (f : H), eval x f = f x

I can easily go back and forth between this evaluation-based definition and the kernel-based definition. However, for the current problem, I don't think it really matters which one I use. The only thing that would change is what is written instead of the sorry in let rkhs : RKHS H X := sorry.

[Tjeerd Jan Heeringa]

I used your tip on how to rewrite the theorem to write is as

noncomputable def ofPreRKHS (K : Kernel X) (pre : PreRKHS X K) : RKHS (UniformSpace.Completion pre.carrier) X := by
  letI : SeminormedAddCommGroup (pre.carrier) := InnerProductSpace.Core.toSeminormedAddCommGroup (c := pre.preInnerCore)
  letI : InnerProductSpace ℝ (pre.carrier) := InnerProductSpace.ofCore pre.preInnerCore
  letI : UniformSpace (pre.carrier) := PseudoMetricSpace.toUniformSpace

  letI : CompleteSpace (UniformSpace.Completion pre.carrier) := by infer_instance
  letI : NormedAddCommGroup (UniformSpace.Completion pre.carrier) := UniformSpace.Completion.instNormedAddCommGroup (pre.carrier)
  letI : InnerProductSpace ℝ (UniformSpace.Completion pre.carrier) := UniformSpace.Completion.innerProductSpace
  letI : FunLike (UniformSpace.Completion pre.carrier) X ℝ := sorry
  let rkhs : RKHS (UniformSpace.Completion pre.carrier) X := sorry
  exact rkhs

This is already a lot close because the error is now

Type mismatch
  rkhs
has type
  RKHS (@UniformSpace.Completion (↥(PreRKHS.carrier K)) this✝³) X
but is expected to have type
  RKHS (@UniformSpace.Completion (↥(PreRKHS.carrier K)) instUniformSpaceSubtype) X

The this✝³ refers to the line letI : UniformSpace (pre.carrier) := PseudoMetricSpace.toUniformSpace. It suggests to me that I have the wrong underlying UniformSpace. Commenting out that line gives at the line letI : NormedAddCommGroup (UniformSpace.Completion pre.carrier) := UniformSpace.Completion.instNormedAddCommGroup (pre.carrier) the error

Type mismatch
  UniformSpace.Completion.instNormedAddCommGroup ↥(PreRKHS.carrier K)
has type
  NormedAddCommGroup (@UniformSpace.Completion (↥(PreRKHS.carrier K)) PseudoMetricSpace.toUniformSpace)
but is expected to have type
  NormedAddCommGroup (@UniformSpace.Completion (↥(PreRKHS.carrier K)) instUniformSpaceSubtype)

I could also let Lean try to infer it itself by writing letI : NormedAddCommGroup (UniformSpace.Completion pre.carrier) := by infer_instance but that gives a failed to synthesize error. So, not sure how to tell lean to use the right uniform space. How do I proceed?

[Tjeerd Jan Heeringa]

I resolved the type issues. They were due to me not taking into account the quotienting properly. I needed to write

def PreRKHS.quotientSpace {K : Kernel X} (pre : PreRKHS X K) := pre.carrier ⧸ PreRKHS.null_space (K:= K)

noncomputable def ofPreRKHS (K : Kernel X) (pre : PreRKHS X K) : RKHS (UniformSpace.Completion (PreRKHS.quotientSpace pre)) X := by
  letI : NormedAddCommGroup (UniformSpace.Completion (PreRKHS.quotientSpace pre)) := UniformSpace.Completion.instNormedAddCommGroup (PreRKHS.quotientSpace pre)
  letI : InnerProductSpace ℝ (UniformSpace.Completion (PreRKHS.quotientSpace pre)) := UniformSpace.Completion.innerProductSpace
  letI : FunLike (UniformSpace.Completion (PreRKHS.quotientSpace pre)) X ℝ := sorry
  let rkhs : RKHS (UniformSpace.Completion (PreRKHS.quotientSpace pre)) X := sorry
  exact rkhs

and define some instances for the quotient space. Removing the line

letI : UniformSpace (pre.carrier) := PseudoMetricSpace.toUniformSpace

and creating the instances made sure that the quotient had the right UniformSpace type and the errors went away.

Thanks again for pointing me in the right direction, @Yongxi Lin (Aaron).

[Bill Cochran]

(deleted)