Function coercion for Reproducing Kernel Hilbert Spaces

Stream: new members

[Hampus Nyberg]

Hello!
I just made an introduction here. Basically I'm trying to formalize Reproducing Kernel Hilbert Spaces.
Reproducing kernel Hilbert spaces are simply Hilbert spaces of functions together with some compatibility property.
As I understand someone was trying to do this before but were running into some troubles (!3#16351) and I think I'm running into the same ones. Anyway, this is what I have so far:

import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.LinearAlgebra.Matrix.PosDef

open InnerProductSpace
open scoped ComplexOrder

noncomputable section



class RKHS (α : Type*)(𝕜 : Type*) [RCLike 𝕜] (E : Type*) [NormedAddCommGroup E] extends
  InnerProductSpace 𝕜 E, CompleteSpace E where
  defult : α
  eval : α → NormedSpace.Dual 𝕜 E
  eval_ext : ∀f:E, ∀x:α, eval x f = 0 → f = 0
section


variable {α : Type*}{𝕜 : Type*} [RCLike 𝕜] {E : Type*} [NormedAddCommGroup E]
namespace RKHS


instance toFun (H : RKHS α 𝕜 E): FunLike E α 𝕜 where -- instance does not provide concrete values for (semi-)out-params
  coe := fun f ↦ fun x ↦ H.eval x f
  coe_injective' := by
    simp[Function.Injective]
    intro f g hfg
    apply congrFun at hfg
    replace hfg :  ∀ (x : α), (H.eval x f) - (H.eval x g) = (0 : 𝕜) := fun x ↦ sub_eq_zero_of_eq (hfg x)
    replace hfg :  ∀ (x : α), H.eval x (f-g) = (0 : 𝕜) := by
      intro x
      specialize hfg x
      rw [← hfg]
      exact ContinuousLinearMap.map_sub (H.eval x) f g
    rw[← sub_eq_zero]
    apply H.eval_ext (f-g)
    refine hfg ?_
    use H.defult


def Kernelfun (H : RKHS α 𝕜 E) : α → E :=
  fun a ↦ (toDual 𝕜 E).symm (H.eval a)


def Kernel (H : RKHS α 𝕜 E) : α → α → 𝕜 :=
  fun a b ↦ ⟪(H.Kernelfun) a, (H.Kernelfun) b⟫_𝕜

end RKHS


def infPosDef (K : α → α → 𝕜) : Prop :=
  ∀ (s : Finset α), Matrix.PosDef (fun (a:s) (b:s) ↦ K a b)

def infPosSemidef (K : α → α → 𝕜) : Prop :=
  ∀ (s : Finset α), Matrix.PosSemidef (fun (a:s) (b:s) ↦ K a b)

namespace RKHS

theorem KernelPosSemidef (H : RKHS α 𝕜 E) : infPosSemidef (H.Kernel) := by
  intro s
  constructor
  · apply Matrix.IsHermitian.ext_iff.mpr
    simp [Kernel]
  · intro x
    simp only [Matrix.mulVec, dotProduct, Kernel,Pi.star_apply, RCLike.star_def]
    conv =>
      arg 2; arg 2
      intro j
      conv =>
        rw[Finset.mul_sum]
        arg 2
        intro i
        rw[←mul_assoc,← smul_left, mul_comm,←inner_smul_right]
      rw[← inner_sum]
    rw[← sum_inner]
    apply RCLike.le_iff_re_im.mpr
    constructor
    · rw[← norm_sq_eq_inner]
      simp
    · simp

Ok so in the above the E should be thought of as a set of functions from α to 𝕜, 𝕜 as either the real or the complex numbers, and α as any (non-empty) set that the functions are defined on.

Now it would be nice to be able to coerce from an element of E to a function from α to 𝕜 once we have a RKHS instance but I get errors when trying to say that we should have an instance of FunLike E α 𝕜. Ill mention that it works if I replace "instance" with "def" in the above but then it can't synthesise this instance automatically which would be ideal.

Is there any way to get this to work? I have tried defining the RKHS class a bunch of different ways but I keep running into similar problems. Thanks in advance for any help!

[Jireh Loreaux]

I still think that my comment on that PR is the way to go here:

As a second option which I'm fairly certain will work: instead of having an actual submodule or extending fun_like, just use an injective linear map, like this

class RKHS (H : Type*) [InnerProductSpace 𝕜 H] where
  toFuns : H →ₗ[𝕜] (X → V)
  toFuns_injective : Function.Injective (toFuns : H → X → V)
  continuous_eval' : ∀ (x : X), Continuous (fun (f : H) ↦ toFuns f x)

You can then set up a FunLike instance in the natural way. I think if the first one doesn't work, then the second is definitely the way to go unless I'm missing something.

Note: with this approach, RKHS.add_apply' and RKHS.smul_apply' become simp lemmas about your FunLike instance (i.e., ⇑(f + g) = ⇑f + ⇑g and ⇑(c • f) = c • ⇑f), and you can write down a "new" continuous_eval that is phrased as ∀ x : X, continuous (fun f : H ↦ ⇑f x)

(updated for Lean 4 code)

[Hampus Nyberg]

I got this to work! Sorry for overlooking this approach before. Thank you! :)