Quantum and SVD in LEAN

Stream: Is there code for X?

[Jam Kabeer Ali Khan]

Support for singular value decomposition in LEAN. I am trying to utilize LEAN to formalize the infrastructure needed to do proofs for Quantum. Is there support for singular value decomposition in Lean, and has anyone worked with the formalization of quantum in LEAN?

[Joseph Tooby-Smith]

Hi @Jam Kabeer Ali Khan ! Can you be a bit more descriptive about what you mean by 'Quantum'? We have things related to quantum mechanics in PhysLean, but I'm not sure if this is what you mean.

[Joseph Tooby-Smith]

Regarding SVD there was at one point this: #6042,
and related discussion at: #PR reviews > PR #6042 Singular Value Decomposition

[Jam Kabeer Ali Khan]

Hi @Joseph Tooby-Smith, yes sure. So, I need to formalize some notion of predicates, in a logic, which are density operators in Hilbert spaces, but using extended positive reals for eigenvalues in the spectral decomposition. What I am trying to understand is whether there is enough support in Lean to formalize this. So, I am looking for the infrastructure for this formalization. Here is a reference in Coq for things I need: quantum.v, and svd.v (both files have some docs on top to give u a basic idea). In summary, I need the notion of projections, density operators, Hilbert spaces, etc. Thanks for the help! Apologize if I am not clear enough, and lemme know if u need more context.

[Joseph Tooby-Smith]

Ok, thanks for your explanation. This makes sense to me (although I can't open the second file you linked to).
Mathlib has Hilbert spaces, and it would not surprise me if someone had defined density operators somewhere in Lean, but I am not sure of any places of the top of my head.

This is something which would be nice to have in PhysLean at some point, so if you'd be interested in contributing there, that would be great :).

[Jam Kabeer Ali Khan]

Oh, I fixed the link. Yes, we found Hilbert spaces in Mathlib, and so far, couldn't find much related to the density operators. Yes, we plan to add this to MathLib or PhysLean if we decide to go for Lean instead of Coq, but so far it seems we need the notion of singular value decomposition for spectral decomposition and this Coq has for now.

[Jireh Loreaux]

Do you need this in finite or infinite dimensional spaces?

[Jam Kabeer Ali Khan]

This is finite dimensional

[Jireh Loreaux]

In that case, I recommend resurrecting #6042

[Alex Meiburg]

https://github.com/Timeroot/Lean-QuantumInfo
has density operators, spectra of states, unitary decomposition, some things about CPTP maps

[Alex Meiburg]

I don't know how you can have "extended positive reals for eigenvalues" in a density operator in a finite-dimensional space, given that they (presumably) need to add to 1 - or in some versions that I've seen, a trace in the interval [0,1].

[Alex Meiburg]

Actually, you say SVD, but for quantum mechanics you should (typically?) only need the eigenvalue decomposition, which is already there in Mathlib.