Generalized quantum Stein’s lemma paper

Stream: Quantum information

[Maris Ozols]

Congrats @Alex Meiburg, @Léo Lessa and @Rodolfo R. Soldati on your arXiv paper with a formal proof of generalized quantum Stein’s lemma! I didn't realize you were so close to formalizing it (I thought it would take a year or two)!

We are having a weekly Lean seminar in Amsterdam, so I was thinking that maybe one of you wants to give a talk on this via Zoom? We'll send you an e-mail about it...

[Alex Meiburg]

I thought it would take a year or two

Well, that's about right. I started the general repo in April 2024, and we started working on Stein's Lemma around January. :)

[Maris Ozols]

Cool! I was just not aware of how far you guys were when I saw the repo the first time.

[Alex Meiburg]

Yes, there's a lot of sorries in the repo that aren't needed for the main result. Which can obviously make it look a lot less complete than it is... for instance, we never need the idea of a "pi-type" kronecker product (the map from an indexed set of states, to a state on the indexed Hilbert space); a lot of things in there about channels / entropy / etc. that we don't need...

I'm in the process of trying to clean it up into a separate branch that shows sort of the more clean, minimal stuff needed for the work.