Task list

Stream: Quantum information

[Alex Meiburg]

:wave: Some people were wondering about some good ~beginner tasks to get started with on the quantumInfo repo. I thought I would try to list some here, as they come to me.

• Show that the replacement channel is completely positive.
• Showing that capacity of the identity channel is (at least) log(D)
• Defining "partial trace" as a CPTP map. There's already Matrix.traceLeft, but there needs to be the fact that it's linear, and probably also a HermitianMat.traceLeft would be good.
• There are several sorries about POVM's; they are not fleshed out very well.
• It would also be great to have the notion of "the two-element POVM defined by one operator T, with 0 <= T <= 1", and lemmas/theorems about it. I'm thinking something like def POVM₂ (T : HermitianMat d) : POVM Bool d := ... .
• Right now most of the repo is very focused on arbitrary finite dimensions, but of course there's a lot of qubit-specific stuff to be said. Building out Qubit/Basic.lean with some facts like "what is the Pauli group" / "what is the Clifford group", or some basic equations ("H * Z * H = X") would be great. Even better if done for arbitrary qudits where possible. :)

There's also the (somewhat out of date?) stuff in TODO.md. That tries to align material to Mark Wilde's textbook, which is available as a pdf here.

[Alex Meiburg]

I just updated the documentation on the website, it was running pretty out of date: https://ohaithe.re/Lean-QuantumInfo/

[Alex Meiburg]

alrighty, and bumped to latest Lean / Mathlib.