channel events

Stream: Quantum information

[Notification Bot]

Public channel created by Frédéric Dupuis. Description:

Discussions about formalising quantum information, quantum computation, and related areas.

[Maris Ozols]

Just dropping by to say 'Hi!'. I'm learning Lean at the moment and I'm also interested to apply it in the context of quantum computing (specifically, quantum algorithms). I feel like I'm still too much of a beginner to contribute here. Right now as a toy example for learning purposes, I'm trying to formalize the single-qutrit Pauli and Clifford groups. Maybe later once I know a bit more I can also try to contribute something here.

[Alex Meiburg]

Wonderful, hi! :)

[Frédéric Dupuis]

Hi, nice to see you here!

[Alvan Arulandu]

Hello! I'm Alvan, I've done a touch of Lean but am trying to learn more and am poking around the repo to help where I can. It's good to meet everyone :)

If anyone has recommendations on what to look at / work on beyond the task list, I'd love to hear them!

[Alex Meiburg]

Well, one thing that would be very nice to have - the API around Matrix.IsHermitian.eigenvalues is currently pretty limited. Some theorems that would be good to have:

• The eigenvalues of c • A are c • the eigenvalues of A
• The eigenvalues of -A are the negatives of the eigenvalues of A (immediate consequence of the above)
• The eigenvalues of A + I are 1 plus the eigenvalues of A. (Here "I" would actually be 1 in Lean.)
• The eigenvalues of A ⊗ₖ B are the products of the eigenvalues of A and B. (That's the scoped notation for kroneckerMap.)

[Alex Meiburg]

In general the API around even talking about these equalities is kind of awkward, because "eigenvectors" are this inherently somewhat non-canonical choice of basis, and "eigenvalues" are this sorted list turned into a function (as opposed to a Multiset).

I have the correspondence between Matrix.IsHermitian.eigenvalues and Matrix.charpoly.roots in my quantumInfo repo, but... I think things could be better

[Alex Meiburg]

So maybe really a better starting point would be proving one or more kinds of "eigenvalue extensionality theorem". A few examples of what I mean:

• If A is diagonalized by two different unitaries, then those diagonalized matrices are equal up to permuting the diagonal.
• A and B have equal Matrix.IsHermitian.eigenvalues iff there is a unitary turning one into the other.
• The above is also true if you replace "equal eigenvalues" with "equal eigenvalues up to permutation", since Matrix.IsHermitian.eigenvalues is always sorted.
• If every eigenvector of A is an eigenvector of B, and they have equal eigenvalues, then they're equal matrices.