Quantum information theory

Stream: new members

[Erickson Tjoa]

Hi,

I am a postdoctoral researcher on quantum information and I am new to Lean. I am trying to learn the basics (starting from the Natural Numbers Game, for example). I find it really hard to keep myself going on this without a goal, so I was thinking of taking the book by Nielsen and Chuang and (very) slowly formalize each chapter as a goalpost.

I did a bit of search and I found that formalization of quantum information/quantum computing is somewhat limited. That said, this is probably me missing important works from very brief searches. That said, I know formalization is highly non-trivial task and I would like to better understand if (1) this is already an ongoing active project by a sub-community, and/or (2) whether this is an interesting sub-field to formalize. Given life's limitations I want to be more informed about whether it makes sense for me to be part of this effort before committing.

I would very much appreciate any input/concern/question/recommendations/contacts. Thanks!

[Patrick Massot]

@Frédéric Dupuis :up:

[Frédéric Dupuis]

Hi and welcome!

My main field of research is also quantum information, and I think it's definitely a field that would benefit from formalization -- that's why I'm here! (The ongoing saga of the generalized quantum Stein's lemma should be enough to convince anyone...) For the moment, there's nothing really specific to quantum information theory in mathlib, but you've arrived at a very interesting time. Right now, we have the basics of Hilbert spaces, and C*-algebra theory is advancing at a very rapid pace. Very recently, @Jireh Loreaux has PRed the continuous functional calculus, which allows us to apply functions to normal operators. (For the finite-dimensional case, this could have been done a bit faster via the spectral decomposition, but in mathlib we tend to aim directly for high levels of generality to avoid having to redo the work later.) This will open up a lot of very interesting avenues; I think very soon we'll be able to define CP maps, Schatten norms, fidelity, and so on.

Also, this might sound a bit counter-intuitive, but if one wants to start formalizing the results from a particular book, I think something like "Matrix Analysis" or "Positive Definite Matrices" by Rajendra Bhatia might be a better choice than Nielsen and Chuang, at least if the goal is to contribute to mathlib. Nielsen and Chuang is a great book to starting learning about quantum information, but it contains a lot of concrete examples, special cases, etc, that are not necessarily the best choice of material to formalize, whereas the Bhatia books are full of theorems we want to have and that would be relevant for formalizing quantum information papers down the road.

If you're interested in representation theory, this could be another area where there's a lot of work to be done. For instance, formalizing Young tableaux could be a nice first project to work on. In any case, I'd be happy to discuss this further!

[Yaël Dillies]

Young tableaux are already in mathlib

[Erickson Tjoa]

Hi Frédéric,

Thanks for your response, that's really helpful and insightful! Your suggestions about not going through Nielsen/Chuang makes a lot of sense, and maybe I should flesh out in more detail what I have in mind given what you said above. Most importantly I am glad that the progress is much more than I expected.

A disclaimer first is that I am in no capacity a mathematician and I don't prove theorems in my daily work or PhD, although I have benefitted from some (though limited) amount of rigorous background in quantum information (I guess at the level of Watrous and Wolf's lecture notes) along the way. That said, I was interested in this program partly because, indeed, of the quantum Stein's lemma (I met/know some of the authors involved in the saga). My PhD was closer to physics involving quantum field theory, and that's where I learnt more about C* and von Neumann algebras (the whole stuff about algebra of observables and classification of factors, for example). Right now I am working in quantum many-body and quantum information theory, where to my pleasant surprise some of these things do crop up. In any case, all the terminology you mentioned above (CP maps, Schatten p-norms, fidelity, C* algebras) are familiar to me to some extent, so I guess that's good news.

Actually your suggestion is very nice, since Bhatia has a lot of things one can really use (majorization, matrix inequalities) and I would love to see the strong subadditivity theorem being formalized properly. This would hopefully bring in convex stuffs into mathlib one day (if it is not already started). As for representation theory, that is of course also very nice since I came from QFT where representations of Lorentz group are crucial, and in my current group where a lot of work is done about many-body physics, this also matters when it comes to symmetry-protected phases.

Let me know if I should pm you instead of continuing this thread if this is more convenient. Right now, perhaps I could use some suggestions about what would be nice to start with (while I learn the basics of Lean). I can probably only spare my evenings to work on this but better than zero, probably. I guess the ones you mentioned above are:

1. Matrix analysis (Bhatia/Petz-Hiai kind)
2. C* algebra (which part of C* is this? Is the focus on von Neumann algebras or or something else?)
3. Continuous functional calculus (how much has it started?), towards CP maps etc.
4. Representation theory (finite? Lie group?)
5. Anything else?

Actually, since I am new, I was wondering if there is a rough estimate/intuition about what would constitute good "first project"? It looks like the community is ready to even formalize Fermat's Last Theorem (FLT), but I am guessing the "hardness of the subject" is less of a problem than the "hardness of formalizing in Lean" (whatever that means).

[Frédéric Dupuis]

Yaël Dillies said:

Young tableaux are already in mathlib

Nice, I had missed that! Before I suggest anything else in that direction, Schur-Weyl duality is not yet in mathlib, is it? :-)

[Yaël Dillies]

Don't think so!

[Frédéric Dupuis]

For C*-algebras, so far the focus has been on getting the continuous function calculus to work, since this was a major bottleneck; we have the definition of von Neumann algebras (see docs#VonNeumannAlgebra), but very little else. For representation theory, you can have a look at what we have so far by poking around docs#Representation in the docs.

For a first project, as you can imagine there's a big difference between a good first project for one person and a big multiyear project for a team with funding :-) My guess is that some simple representation theory would be a good place to start. To bounce back on my earlier suggestion about Young tableaux, it looks like Young diagrams (docs#YoungDiagram) and semistandard Young tableaux (docs#Ssyt) are there, but not standard Young tableaux -- that could be a good start by itself. This can later be continued by working towards the connection to irreps of the symmetric group, Schur-Weyl duality, etc. Working out irreps of you favorite group is likely to be a decent project also. Once we get a good API for the continuous functional calculus with operator square roots and so on (which I expect will be very soon), there should be good first projects opening up in more "standard" quantum information material.

Also, I'm happy to keep the discussion going here, there are not so many people interested specifically in quantum information here yet, but there is fairly broad interest in pretty much all of the relevant areas of math.

[Kevin Buzzard]

Regarding representation theory: I am slightly concerned by the following issue. The representation theory of finite groups, even up to orthonormality of characters, is being developed via objects in the category FdRep. This seems like quite a lot of pain away from, for example, a homomorphism G ->* \C.

[Frédéric Dupuis]

Indeed it would be nice to have a more down-to-earth development of this material.

[Frédéric Dupuis]

Another good first project might be to define creation, annihilitation, position and momentum operators. We have the underlying Hilbert space, but I don't think we have those yet.

[Jireh Loreaux]

Surely docs#Ssyt should be renamed to SSYT.

[Jireh Loreaux]

(or even something more informative)

[Erickson Tjoa]

So do I understand correctly that for matrix analysis it is actually better to wait for continuous functional calculus to happen?

[Frédéric Dupuis]

Jireh Loreaux said:

Surely docs#Ssyt should be renamed to SSYT.

Yes, like SemistandardYoungTableau!

[Frédéric Dupuis]

Erickson Tjoa said:

So do I understand correctly that for matrix analysis it is actually better to wait for continuous functional calculus to happen?

Well, we're pretty much there already! The unital CFC is there, but at this point I guess we might as well define the square root using the non-unital CFC which is almost there now.

[Yoh Tanimoto]

hello, I would like very much to see quantum physics in mathlib, too!
Is there any ongoing project on the spectral decomposition (infinite-dimensional)?
I see that docs#rieszContentAux is under development (one would have to show that this gives a measure). Is anyone working on that?

[Jireh Loreaux]

@Frédéric Dupuis #11328

[Jireh Loreaux]

The continuous functional calculus for unital C⋆-algebras is now available (with all the bells and whistles as of about an hour ago, so you need a really fresh Mathlib for it). You can do things like existence and uniqueness of positive semidefinite square roots:

import Mathlib

variable {A : Type*} [PartialOrder A] [NormedRing A] [StarOrderedRing A]
  [NormedAlgebra ℂ A] [CstarRing A] [CompleteSpace A] [StarModule ℂ A]

noncomputable section

open NNReal

def cfc_sqrt (a : A) : A := cfc a sqrt

attribute [fun_prop] continuous_sqrt

lemma sq_cfc_sqrt (a : A) (ha : 0 ≤ a) : (cfc_sqrt a) ^ 2 = a := by
  simp_rw [cfc_sqrt, ← cfc_pow a sqrt 2 ha, sq_sqrt, cfc_id' ℝ≥0 a]

lemma cfc_sqrt_unique {a b : A} (hb : 0 ≤ b) (hab : b ^ 2 = a) :
    b = cfc_sqrt a := by
  simpa only [← cfc_comp_pow b 2 sqrt, sqrt_sq, cfc_id' ℝ≥0 b] using congr_arg (cfc · sqrt) hab

I hope that within the next few weeks we'll have the non-unital version up and running.

[Jireh Loreaux]

You can activate this for matrices today by adding

attribute [local instance] Matrix.instL2OpNormedRing Matrix.instL2OpNormedAlgebra Matrix.instCstarRing