Physics?

Stream: general

[Wojciech Nawrocki]

Hey, I'm curious - are there any physicists here looking at formalising some of the vector algebra for quantum theory? I couldn't find anything related to e.g. Hilbert spaces.

[Kevin Buzzard]

A first year undergraduate student of mine formalised the definition of Hilbert spaces as part of their summer project, but I don't think there's anything in the official maths library.

[Sean Leather]

I don't recall any physicists coming forward openly. But if you are one, you'd better beware.

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Banach%20spaces.lean and and there are inner product spaces too, but actually I don't see Hilbert space yet.

[Andreas Swerdlow]

I’m pretty sure I fixed the issue with Hilbert space so hope to PR soon

[Andreas Swerdlow]

Although I only have one trivial lemma about Hilbert Spaces specifically

[Wojciech Nawrocki]

Ok, thanks! I was looking at (maybe) formalising some results that require notions of a Hilbert space.
@Andreas Swerdlow do you mean it might be included in mathlib at some point?

[Andreas Swerdlow]

Hopefully, but it probably needs some cleaning up

[Ben]

Hello all,

I'm a Physicist but am just starting to learn Lean (as in a few days ago). I have almost no experience with proofs. I'm interested in figuring out how Lean can be applied to mathematical derivations in Physics.

[Dean Young]

Kevin Buzzard said:

A first year undergraduate student of mine formalised the definition of Hilbert spaces as part of their summer project, but I don't think there's anything in the official maths library.

I would be interested to see that. Did this project construct the tensor product and hom as well? What about the Riesz representation theorem?

[Kevin Buzzard]

This was all in lean 3 many years ago, and I should think Andreas didn't do anything which couldn't be knocked off in an afternoon nowadays, given what we have. We might well even have Hilbert spaces now, I thought we even had L^p spaces now. I doubt we had them in 2018 when I made that comment.

[Dean Young]

Thanks for this, professor Buzzard. Maybe you could also mention to Archie that Jiazhen and I are keen to meet concerning CW-complexes.

[Jireh Loreaux]

@Dean Young we have the Riesz representation theorem: docs#InnerProductSpace.toDualMap

[Jireh Loreaux]

We don't yet have the tensor product of Hilbert spaces though.

[Dean Young]

@Jireh What about hom?

[Jireh Loreaux]

sorry, what hom?

[Dean Young]

The inner product space of bounded maps between two inner product spaces, essentially using the inner product structure of the second.

[Jireh Loreaux]

I suppose you mean to restrict to Hilbert-Schmidt operators? Or do you mean for finite dimensional spaces?

[Dean Young]

Sorry, you're right. It's not the projective tensor product - bounded maps, but instead the tensor product of Hilbert spaces and Hilbert-Schmidt operators that I want. Do we have those?

[Jireh Loreaux]

No, I don't believe we have completions of any kind of tensor products in Mathlib at the moment. This is on my long-term TODO list, but I probably won't get to it for a while.

[Dean Young]

Ok-- I think I want to create the full-on-monoidal-closed category. Would it be ok if I reach out to you when I finish?

[Jireh Loreaux]

@Anatole Dedecker did you do some work on the tensor product of HIlbert spaces (as lp of lp)? I thought I remember this at some point, but I can't find it.

[Anatole Dedecker]

No I didn't, I had some plans from Hilbert-Schmidt operators (using trace-class) but nothing got into Mathlib. Maybe you're thinking about mathlib#16407, which allows us to complete inner product spaces into Hilbert spaces (how interesting!) ?

[Jireh Loreaux]

mathlib#16407

[Anatole Dedecker]

:face_palm:
Thanks!

[Jireh Loreaux]

The linkifer is broken.

[Jireh Loreaux]

ah, okay.

[Frédéric Dupuis]

(deleted)

[Anatole Dedecker]

So really the only missing piece to get tensor products of hilbert spaces is to write the inner product instance on (a type alias of) the algebraic tensor product. We may want to have a more general API for this, but honestly tensor product of Hilbert spaces are so much more common that maybe we can just do it ?

[Dean Young]

@Anotole Could I just lobby that it be grouped with the mentioned hom and potentially the map of H₂ ⊗ [H₂, H₃] ⭢ H₃ and H₃ ⭢ [H₂,H₂ ⊗ H₃] .

[Dean Young]

@Anatole Dedecker or were you saying that the tensor is more common than the hom? Also we may want that H* ⊗ H' ≅ [H,H'] ?

[Anatole Dedecker]

Your bracket is Hilbert-Schmidt operators ? I have no concrete plans right now (and shouldn't engage in yet another project), I was just laying down what exists and what is easy. The other types of tensor products I meant is all the zoo of norms you can put on a tensor product, and probably at some point we will want the tensor products of Hilbert Spaces to be implemented as a particular case of that.

[Eric Wieser]

Note we have a tracking issue, #6020

[Jireh Loreaux]

Anatole, it shouldn't be that much work to define cross norms, so I think we should do that whenever we implement any tensor product completion.

[Jireh Loreaux]

I should mention that @Frédéric Marbach may have something small to PR about Hilbert-Schmidt operators, but I'm not sure about that.

[Anatole Dedecker]

Jireh Loreaux said:

Anatole, it shouldn't be that much work to define cross norms, so I think we should do that whenever we implement any tensor product completion.

I believe you, I never took the time to properly think about it.

[Frédéric Marbach]

Jireh Loreaux said:

I should mention that Frédéric Marbach may have something small to PR about Hilbert-Schmidt operators, but I'm not sure about that.

I had indeed started working on Hilbert-Schmidt and trace-class operators in #LFTCM 2024, but I have no particular expertise in this topic, and I am very far from having prepared anything significant yet. So I am glad to let you work on it without any constraint.