timeroot/lean-quantuminfo

Quantum information theory in Lean 4

This repository aims to contain definitions and proofs of basic ideas in quantum information theory. Some major goals, in rough order of difficulty, would be:

• Defining most notions of "distance", "entropy", "information", "capacity" that occur in the literature.
• Showing that these reflect the classical notions where applicable
  • For instance, that if you embed a clasical probability distribution as a quantum mixed state, then the classical conditional entropy and the quantum conditional entropy are the same number.
• Strong sub-additivity of von Neumann entropy
• Holevo's theorem
• The LSD theorem on quantum capacity
• Non-additivity of quantum capacity

All of this will be done only in the theory finite-dimensional Hilbert spaces. Reasons:

• Most quantum information theory is done in this setting anyway. Not to say that the infinite-dimensional work isn't important, just that this is what more researchers spend their time thinking about.
• Infinite-dimensional quantum theory can be weirdly behaved.
• Dealing with infinite-dimensional quantum theory is just hard. You need e.g. trace-class operators, CTC functions, and people often can't even agree on the definitions. (For instance, does a mixed state necessarily have a finite spectrum? I've seen it both ways.)

Most stuff is in the QuantumInfo/FiniteDim folder. There was a tiny bit of infinite-dimensional theory in the QuantumInfo/InfiniteDim folder, but it's mostly been cleared out.

Docmentation of the main definitions can be found at DOC.md. A majority of the work will be outlining the major definitions and theorems from Mark Wilde's Quantum Information Theory. A correspondence to the definitions and theorems (mostly as todo-list!) are in TODO.md

lean-quantuminfo's Issues

Mathlib has `-x * log x` and some things on entropy

Maybe you're already aware or don't want to constantly update how Mathlib is used, but some of the things in your repo are already in Mathlib. For example some of the things here:

Lean-QuantumInfo/ClassicalInfo/Entropy.lean

Line 15 in aed3615

def H₁ : Prob → ℝ :=

are at Mathlib.Analysis.SpecialFunctions.Log.NegMulLog.

I defined binary entropy (which maybe you don't need explicitly) which will be merged soon here

and there is measure-theoretic entropy which maybe will get merged eventually here