Is there code for Hilbert Spaces?

Stream: Is there code for X?

[Kent Van Vels]

Is there code for Hilbert spaces? Hilbert spaces are Cauchy-complete inner product space.

I have just been doing this

import Mathlib.tactic

variable {RC E : Type*} [RCLike RC]

variable [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace RC E]

Is this the correct way to declare that E is Hilbert space over the field RC?

[Rémy Degenne]

Yes, this is the correct way.

[Kent Van Vels]

Ok, thanks. I feel better now.

[Notification Bot]

Kent Van Vels has marked this topic as resolved.

[Iván Renison]

Hello, I wanted to ask, way are we using that for Hilbert spaces instead of having a proper definition?

[Notification Bot]

Iván Renison has marked this topic as unresolved.

[Kevin Buzzard]

docs#NormedAddCommGroup docs#CompleteSpace docs#InnerProductSpace

[Kevin Buzzard]

The first and last things are data, and the middle one is a Prop (and should be called IsCompleteSpace to reduce confusion IMO). Ivan it's not clear what you're proposing instead. Where do you want the data to go?

[Kevin Buzzard]

Would alias IsHilbertSpace := CompleteSpace work for you?

[Iván Renison]

I was thinking more in something like an alias but including the tree, NormedAddCommGroup, CompleteSpace and InnerProductSpace, to be able to use [IsHilbertSpace RC E instead of [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace RC E].
I don't know, is something like that possible?

[Yaël Dillies]

Yes, this is possible with class abbrev (search for that on Zulip)

[Kevin Buzzard]

docs#NumberField

[Kevin Buzzard]

Number fields were an example where we could say "let K be a number field" by just throwing typeclass assumptions on K, and it seems that this was ultimately implemented by making a new Prop-valued class which just has fields equal to the old Prop-valued classes but extending the data-carrying classes

[Kevin Buzzard]

(is it usual that we can't see which structures are classes in the docs or is this related to the current docs notation breakage?)

[Yaël Dillies]

I assume it is related, yes. cf #mathlib4 > No notation in #docs

[Iván Renison]

Great! This looks good:

class HilbertSpace (𝕜 : Type*) (E : Type*) [RCLike 𝕜] [SeminormedAddCommGroup E] where
  [normedAddCommGroup : NormedAddCommGroup E]
  [innerProductSpace : InnerProductSpace 𝕜 E]
  [isCompleteSpace : CompleteSpace E]

[Iván Renison]

Would this be a good addition to Mathlib?

[Yaël Dillies]

Sure! Although we will want it to be a class abbrev (not sure what's up with NumberField either)

[Rémy Degenne]

You don't want to have both SeminormedAddCommGroup E and NormedAddCommGroup E though. That defines two unrelated norms on E.

[Iván Renison]

You are right Rémy, thanks

[Iván Renison]

Okay, then I will work on adding this with a class abbrev

[Iván Renison]

Thank you

[Yury G. Kudryashov]

If you're going to add this definition, then you probably want to create a [HilbertSpace k E] : NormedAddCommGroup E instance. This instance will lead to a search for HilbertSpace ?k E with unknown ?k every time Lean looks for NormedAddCommGroup E.

[Yury G. Kudryashov]

Should we use variable_alias and variable? for that instead?

[Yury G. Kudryashov]

Also, [HilbertSpace Real E] [HilbertSpace Complex E] leads to two potentially incompatible [NormedAddCommGroup E] structures.

[Sébastien Gouëzel]

I think sticking with

variable [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace RC E]

is really better: it doesn't clutter typeclass search with additional classes which could impact performance, and as Yuri points out you don't want to have a class which extends NormedAddCommGroup E but with an additional field parameter RC that Lean couldn't guess.

[Yury G. Kudryashov]

If I read the docs correctly, then variable_alias lets you write

variable? [HilbertSpace RC E]

and get it unfolded to

variable [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace RC E]

It also claims that it drops assumptions that can be deduced from the already available variables, so

variable? [NormedAddCommGroup E] [HilbertSpace RC E]

should become

variable? [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace RC E]

too, without a duplicate [NormedAddCommGroup E] assumption.

[Yaël Dillies]

Yury G. Kudryashov said:

Should we use variable_alias and variable? for that instead?

This is what I was suggesting with class abbrev

[Yury G. Kudryashov]

AFAICT, class abbrev is different from variable_alias.

[Yury G. Kudryashov]

Because it creates an actual typeclass that will show up in the assumptions.

[Jireh Loreaux]

Yeah, I think we've determined that Mathlib should never use class abbrev.

[Yaël Dillies]

That doesn't it can't provide some class abbrev for downstream use

[Eric Wieser]

That most likely just leaves people rope to tangle themselves in. variable_alias for downstream use sounds more user-friendly

[Iván Renison]

Using variable? [HilbertSpace 𝕜 F] (with variable_alias in the definition) triggers a suggestion:

Try this: variable? [HilbertSpace 𝕜 F] => [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F]

[Iván Renison]

So I don't now if it is a good idea to use only variable? [HilbertSpace 𝕜 F] in Mathlib

[Eric Wieser]

Indeed mathlib should not use variable?, but it should provide tools so that users can use variable?