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.

- For instance, that if you embed a clasical probability distribution as a quantum mixed state, then the
- 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/Finite`

folder. There was a *tiny* bit of infinite-dimensional theory in the `QuantumInfo/InfiniteDim`

folder, but it's mostly been cleared out.

The docgen is available on my website, hopefully I remember to keep it well synced.

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 (in the form of a todo-list) are in TODO