Constructing a Hilbert space from a innerProductSpace

Stream: new members

[Tjeerd Jan Heeringa]

After following (parts of) the lean tutorial, I decided to transfer some of the known theorems in my area of research to Lean. One of these requires to construct a Hilbert space in a particular way. I am stuck in going from the innerProductSpace to the HilbertSpace. Can you help me out?

(I replaced the proofs by sorry to keep my message shorter)
Inside the theorem, I have a span

  let K_span := Submodule.span ℝ (Set.range K_family)

with K_family a set of functions from X to \R, defined an inner_product on it

  let inner_on_span : K_span → K_span → ℝ := by sorry

made that into an inner product space

let inner_core : InnerProductSpace.Core ℝ K_span := by
    refine'
    {
      inner := inner_on_span
      conj_inner_symm := by sorry
      add_left := by sorry
      smul_left := by sorry
      re_inner_nonneg := by sorry
      definite := by sorry
    }

and then took a completion

  letI : NormedAddCommGroup K_span := inner_core.toNormedAddCommGroup
  letI : InnerProductSpace ℝ K_span := InnerProductSpace.ofCore inner_core

  let H := UniformSpace.Completion K_span

However, I cannot do

  letI : CompleteSpace H := by infer_instance
  letI : NormedAddCommGroup H := by infer_instance
  letI : InnerProductSpace ℝ H := by infer_instance

to make it fully an HilbertSpace. The last two lines throw a failed to synthesize error. How do I make sure that the norm, inner product and function coercion (i.e. the thing that allows you to write f x for f\in H) from K_span to H?

[Kevin Buzzard]

Can you please post a #mwe so it's easier to diagnose the problem?

[Kenny Lau]

@H if you learn how to use loogle, it will help you a lot

[Tjeerd Jan Heeringa]

Not sure if I can post a file for an mwe, but here is the code of one:

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.Data.Real.Basic

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


set_option diagnostics true

open Real

variable {X : Type _}
variable {𝕜 : Type*} [RCLike 𝕜]
variable {H : Type _} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]

variable (x y : X)

@[ext]
class Kernel (α : Type*) where
  kernel : α → α → ℝ
  symmetric : ∀ x y : α, kernel x y = kernel y x
  posSemiDef : ∀ (n : ℕ) (xs : Fin n → α) (c : Fin n → ℝ),
      ∑ i ∈ Finset.univ, ∑ j ∈ Finset.univ, c i * c j * kernel (xs i) (xs j) ≥ 0

export Kernel (kernel)
-- class RKHS_eval(H : Type _) (X : Type _) extends HilbertSpace ℝ H where
class RKHS_kernel (H : Type _) (X : Type _) extends Kernel X, NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H where
  coeFun: H → X → ℝ
  coeFunInst : CoeFun H (λ _ => X → ℝ) := ⟨coeFun⟩
  Ksec: X → H
  Ksec_spec : ∀ x y : X, (Ksec x) y = Kernel.kernel x y
  reproducing : ∀ (x : X) (f : H), f x = inner (Ksec x) f

variable (f : H) (x : X)

/- Every kernel defines an RKHS_kernel instance -/
theorem Kernel.exists_RKHS_kernel (K : Kernel X) :
  ∃ (H : Type _) (inst : RKHS_kernel H X), inst.toKernel = K := by
  -- Define the family of kernel functions x ↦ k(x, •)
  let K_family : X → (X → ℝ) := fun x => K.kernel x

  -- Define the span of kernel sections
  let K_span := Submodule.span ℝ (Set.range K_family)

  -- For f = ∑_i c_i K_{x_i} and g = ∑_j d_j K_{y_j},
  -- define ⟨f, g⟩ = ∑_i ∑_j c_i d_j K(x_i, y_j)
  let inner_on_span : K_span → K_span → ℝ := by sorry

  -- Make K_span into an inner product space
  let inner_core : InnerProductSpace.Core ℝ K_span := by
    refine'
    {
      inner := inner_on_span
      conj_inner_symm := by sorry
      add_left := by sorry
      smul_left := by sorry
      re_inner_nonneg := by sorry
      definite := by sorry
    }

  letI : NormedAddCommGroup K_span := inner_core.toNormedAddCommGroup
  letI : InnerProductSpace ℝ K_span := InnerProductSpace.ofCore inner_core

  let H := UniformSpace.Completion K_span
  #check H

  letI : CompleteSpace H := by infer_instance
  letI : NormedAddCommGroup H := by infer_instance
  letI : InnerProductSpace ℝ H := by infer_instance

  -- Construct the RKHS_kernel instance
  refine ⟨H,
    { kernel := K.kernel
      symmetric := K.symmetric
      posSemiDef := K.posSemiDef
      coeFun := fun (f : H) x => inner (Ksec x) f
      coeFunInst := ⟨fun (f : H) x => inner (Ksec x) f⟩
      Ksec := Ksec
      Ksec_spec := by sorry
      reproducing := by sorry
    },
    rfl⟩

I tried using exact?, apply? and loogle (in the VSCode tab), but didn't really get anywhere on this problem. Did help with the previous problem of finding that I needed to use inner_core.toNormedAddCommGroup.

[Kenny Lau]

did you click my link

[Tjeerd Jan Heeringa]

Kenny Lau said:

did you click my link

Yeah I did. Got the same view in VSCode before, but struggled to find the right combination of writing it to get it to work. Its not writing H.innerProductSpace nor UniformSpace.Completion.innerProductSpace H. I am probably doing something silly. What should I do?

[Kenny Lau]

you should probably be doing something simpler if you don't know the difference between implicit and explicit arguments
(to be clear, this is not meant as an insult)

[Tjeerd Jan Heeringa]

Kenny Lau said:

you should probably be doing something simpler if you don't know the difference between implicit and explicit arguments
(to be clear, this is not meant as an insult)

The curly brackets and square brackets are implicit arguments that in the tutorial exercises I could just ignore because Lean figured them out. The round brackets are explicit arguments, but they are not here. That means I shouldn't have to pass anything. The stuff after the : is what I get back. In the documentation, I can see that it is an instance. In the tutorial, we have used by infer_instance to get instances. failed to synthesize error are errors with the type class inference, i.e. the square bracket stuff. In this case, to get an inner product space on H, we first need H to be a SeminormedAddCommGroup. K_span is a NormedAddCommGroup and H the completion of K_span, so I fail to understand why infer_instance cannot derive that H must be a NormedAddCommGroup. I can see that when enabling the options

set_option trace.Meta.synthInstance.answer true
set_option trace.Meta.synthInstance.newAnswer true

that H doesn't get more than just CompleteSpace from the completion. I am not understanding something and that's why I am asking for help. I would be happy with a pointer, even if it is back to the tutorials.

(I took your remark at first as gatekeeping, and am glad you clarified your intend)

[Kenny Lau]

@H

1. in your mwe, the letI : InnerProductSpace ℝ K_span line doesn't work, but I've fixed it
2. you're missing imports; it's recommended to put import Mathlib at the beginning, and then when you're done, minimise the imports by putting #min_imports at the end of the file
3. and then I tried just using the loogle results, and I get a type mismatch (in general it is very important to look at the error messages), so I tried letI : NormedAddCommGroup H := by convert UniformSpace.Completion.instNormedAddCommGroup K_span to see where the problem was
4. the problem is that X → ℝ already has a uniform space structure, which clashes with the new uniform space structure derived from inner_core, which I've fixed by turning off that instance Pi.uniformSpace

code:

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.Data.Real.Basic

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

set_option diagnostics true

open Real

variable {X : Type _}
variable {𝕜 : Type*} [RCLike 𝕜]
variable {H : Type _} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]

variable (x y : X)

@[ext]
class Kernel (α : Type*) where
  kernel : α → α → ℝ
  symmetric : ∀ x y : α, kernel x y = kernel y x
  posSemiDef : ∀ (n : ℕ) (xs : Fin n → α) (c : Fin n → ℝ),
      ∑ i ∈ Finset.univ, ∑ j ∈ Finset.univ, c i * c j * kernel (xs i) (xs j) ≥ 0

export Kernel (kernel)
-- class RKHS_eval(H : Type _) (X : Type _) extends HilbertSpace ℝ H where
class RKHS_kernel (H : Type _) (X : Type _) extends Kernel X, NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H where
  coeFun: H → X → ℝ
  coeFunInst : CoeFun H (λ _ => X → ℝ) := ⟨coeFun⟩
  Ksec: X → H
  Ksec_spec : ∀ x y : X, (Ksec x) y = Kernel.kernel x y
  reproducing : ∀ (x : X) (f : H), f x = inner (Ksec x) f

variable (f : H) (x : X)

#synth CompleteSpace (X → ℝ)

attribute [-instance] Pi.uniformSpace

/- Every kernel defines an RKHS_kernel instance -/
theorem Kernel.exists_RKHS_kernel (K : Kernel X) :
  ∃ (H : Type _) (inst : RKHS_kernel H X), inst.toKernel = K := by
  -- Define the family of kernel functions x ↦ k(x, •)
  let K_family : X → (X → ℝ) := fun x => K.kernel x

  -- Define the span of kernel sections
  let K_span := Submodule.span ℝ (Set.range K_family)

  -- For f = ∑_i c_i K_{x_i} and g = ∑_j d_j K_{y_j},
  -- define ⟨f, g⟩ = ∑_i ∑_j c_i d_j K(x_i, y_j)
  let inner_on_span : K_span → K_span → ℝ := by sorry

  -- Make K_span into an inner product space
  let inner_core : InnerProductSpace.Core ℝ K_span := by
    refine'
    {
      inner := inner_on_span
      conj_inner_symm := by sorry
      add_left := by sorry
      smul_left := by sorry
      re_inner_nonneg := by sorry
      definite := by sorry
    }
  let pre_core := instCoreOfCore ℝ K_span

  letI : NormedAddCommGroup K_span := inner_core.toNormedAddCommGroup
  letI : InnerProductSpace ℝ K_span := InnerProductSpace.ofCore pre_core

  let H := UniformSpace.Completion K_span
  #check H

  letI : CompleteSpace H := by infer_instance
  letI : NormedAddCommGroup H := UniformSpace.Completion.instNormedAddCommGroup K_span
  letI : InnerProductSpace ℝ H := UniformSpace.Completion.innerProductSpace

  -- Construct the RKHS_kernel instance
  refine ⟨H,
    { kernel := K.kernel
      symmetric := K.symmetric
      posSemiDef := K.posSemiDef
      coeFun := fun (f : H) x => inner (Ksec x) f
      coeFunInst := ⟨fun (f : H) x => inner (Ksec x) f⟩
      Ksec := Ksec
      Ksec_spec := by sorry
      reproducing := by sorry
    },
    rfl⟩

[Kenny Lau]

The line attribute [-instance] Pi.uniformSpace turns off the problematic instance

[Tjeerd Jan Heeringa]

Thank you very much for helping, Kenny Lau.

With your help and after updating Matlib so that PreInnerProductSpace.Core was working as intended, I managed to fully complete the proof.

[Jireh Loreaux]

If you're interested in defining RKHS, there was a mathlib 3 PR for that, which you could transport to Lean 4. mathlib3#16351

[metakuntyyy]

Also isn't for that reason of instance clashing where you define a wrapper so that you don't get instances you don't like on your Type?

[Tjeerd Jan Heeringa]

@Jireh Loreaux Thank you for pointing that out. I will see what I can do with it.

[Tjeerd Jan Heeringa]

@metakuntyyy I am not sure I understand what you mean. Could you clarify you message?

[metakuntyyy]

Tjeerd Jan Heeringa said:

metakuntyyy I am not sure I understand what you mean. Could you clarify you message?

So my understanding is if you want to put multiple instances on an object, that's a bad idea. So instead you create a wrapper around that object and equip your wrapper with the desired instances, in case there are conflicting instances. Here is an example of a wrapper for Lp spaces https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Lp/WithLp.html#WithLp

[Yoh Tanimoto]

another example is docs#WeakBilin. it is just a copy of E, but you give a different topology using the given bilinear form by declaring instances.

[Jireh Loreaux]

While true, I think WeakBilin is not the best example. We are lacking a bunch of the basic to/from API for it.