Unbounded operators (Quantum Mechanics)

Stream: Is there code for X?

[Izan Beltran]

Hi! Is there code to handle unbounded operators? I know there is some basic definitions and theorems (LinearPMap), but particularly, the kind of unbounded operators used in Quantum Mechanics, (essentially) self-adjoint operators in dense domains. I would like to work with these, and be able to mix with other bounded operators in a relatively confortable way. These kind of operators have nice results like real eigenvalues, etc...
Thanks!

[Joseph Tooby-Smith]

We have examples of unbounded operations in PhysLean for quantum mechanics here: https://github.com/HEPLean/PhysLean/tree/master/PhysLean/QuantumMechanics/OneDimension/Operators

[Moritz Doll]

LinearPMap is the right thing. It still misses a lot, because I stopped working on it, but I was more or less going through a book on spectral theory of unbounded operators and translating it to Lean. I think the adjoint was implemented for LinearPMap, but I could be wrong or it never made it into mathlib.

[Moritz Doll]

On the other hand, for a lot of things it might be easier working with operators defined on a smaller space that is dense in L^2, probably the best thing we have at the moment is the Schwartz space.

[Moritz Doll]

The problem with the unbounded operators is that you have to check the domains if you want to do arithmetic. I forgot what kind of statement I wanted to prove, but it was some identity involving addition and composition, and it was insanely tedious to get formalized.

[Moritz Doll]

Ok, I am not imagining things and self-adjointness did make it in: LinearPMap.isSelfAdjoint_def