Mark Wilde's book "Quantum Information Theory" provides a solid guide to QIT in general; early on
in the development of QuantumInfo, it was conceived that we could try to match the repository to
that book where reasonably possible as a way to ensure good coverage. This document generally
gives that correspondence, although it may be rather out of date (probably last current as of
early 2025). Of course there's also a lot of content in QuantumInfo that goes well beyond the scope
of that book, too.
Each of the items below is an item in Mark Wilde's book, "Quantum Information Theory". The following emoji indicate possible status:
- ✅ - Completed, and proved with no
sorrys. - 📝 - All required definitions are present and the question is stated / the theorem is in a form that could be used, but it is unproved / depends on
sorry. - ❓ - This has not yet been stated or fully defined.
- 🤷 - This is unlikely / undesirable to be formalized.
- 😂 - This didn't need to be proved, because it was just the definition (or something similar).
- 🤔 - This is not a fact in the book but something related that would be nice to have (and we don't have yet).
There's very little from Chapters 2 or 3 to include right now. Chapter 2 is an intuitive (and less rigorous) overview of classical coding theory. Chapter 3 is a lot of practice of qubit computations, and we haven't worked the special case of qubits yet much.
Exercise 2.1.1: The entropy of a uniform variable is log |X|, where |X| is the size of the variable's alphabet.
✅ Hₛ_uniform in ClassicalInfo.Entropy.
Property 2.1.1, 2.1.2, 2.1.3: Basic properties of typical sets. 🤷 Typical sets aren't defined until Chapter 14, we will prove things then.
Exercise 2.2.1: If the average (across codewords) probability of a codeword C getting incorrectly decoded is ε, then by Markov's inequality least half of the codewords have at most 2ε of incorrect decoding.
🤷 ENNReal.finset_card_const_le_le_of_tsum_le states the interesting bit (Markov's inequality for finite set cardinalities), the application to codewords will come when we need it.
Bras, Kets
✅ Bra and Ket in QuantumInfo.Finite.Braket.
Exercise 3.2.1: Determine the Bloch sphere angles for the states ∣-〉and ∣+〉. ❓ Eventually we'll define qubits, basic states like these, and the Bloch sphere, and can add lemmas for these.
Exercise 3.3.1: A linear operator unitary iff it is norm-preserving.
❓ This is stated for linear operators as unitary.linearIsometryEquiv, and the "only if" is more explicitly as unitary.norm_map. Would be good to have for Matrix.unitaryGroup.
There's a whole bunch about Pauli matrices. We haven't specialized to qubits yet, so these are all ❓.
Exercise 3.3.2: Find a matrix representation of [X,Z] in the basis ∣0〉, ∣1〉.
Exercise 3.3.3: Show that the Pauli matrices are all Hermitian, unitary, and square to the identity, and their eigenvalues are ±1.
Exercise 3.3.4: Represent the eigenstates of the Y operator in the standard computational basis.
Exercise 3.3.5: Show that the Paulis either commute or anticommute.
Exercise 3.3.6: With σi, i=0..3, show that Tr{σi σj} = δij.
Exercise 3.3.7: Matrix representation of Hadamard gate.
Exercise 3.3.8: Hadamard is its own inverse.
Exercise 3.3.9: A particular exercise in changing bases; this is 🤷.
Exercise 3.3.10: HXH = Z and HZH=X. Sure, if we make simp lemmas for Clifford products this can be in there.
Definition 3.3.1: Function of a Hermitian operator (by a function on its spectrum). ❓ This we definitely would like, currently they're all ad-hoc.
Exercise 3.3.11: Explicit forms for rotation operators. ❓ Requires Bloch sphere and rotation gates. Will probably be the definitions of them.
Postulate: Born rule.
✅ We have MState.measure which has this baked in. But we could also have it for bras and kets.
Definition: von Neumann measurement. A POVM that is not just projective, but given by an orthonormal basis. ❓ Could be a nice Prop on POVMs.
Exercise 3.4.1: POVM associated to the X operator measurement. ❓ Definitely want this.
Exercise 3.4.2, 3.4.3: Asking (something like) 〈ψ∣H∣ψ〉= Ex[H.measure (pure ψ)].
❓ Definitely want to prove. Doesn't need qubits, either.
Uncertainty principle ❓ Could do the state-dependent version given in the book. The averaged-case expectation value one comes as a result. But this would require defining + working with the Haar measure over kets.
Exercise 3.4.4, 3.4.5: Longish story about uncertainty princple. 🤷 Won't prove the thing asked, it's a very specific thing.
Exercise 3.5.1: This is askings for products of operators on qubits as tensor products. 😂 This is precisely how we define it to start with.
Exercise 3.5.2: Asking that〈ξ1⊗ξ2‖ψ1⊗ψ2〉=〈ξ1‖ψ1〉〈ξ2‖ψ2〉.
❓ Basic fact about braket products types.
Exercise 3.5.3: Matrix representation of CNOT gate as [1,0,0,0;0,1...] etc.
✅ In Qubits.Basic, defined using Qubit.controllize and proven equivalent to the above matrix
Exercise 3.5.4: Prove (H⊗H)(CNOT)(H⊗H) = |+⟩⟨+|⊗I + |-⟩⟨-|⊗Z.
🤷 Very specific equality.
Exercise 3.5.5: CNOT(1→2) commutes with CNOT(1→3).
Exercise 3.5.6: CNOT(2→1) commutes with CNOT(3→1).
❓ Depending on how we define the qubits to a gate, might be fine (in which case let's do the generic one for any controlled gate), or a pain.
No-Cloning theorem (for unitaries): There is no unitary that clones perfectly from |ψ0⟩ to |ψ0⟩. ❓ Should be easy to state and prove. 🤔 No-Cloning theorem (for channels): There is no channel that clones perfectly from ρ to ρ⊗ρ. 🤔 Proving the bounds on the optimal universal quantum clone (5/6 fidelity etc.)
Exercise 3.5.7: Orthogonal states can be perfectly cloned. ❓ Stated for two orthogonal qubit states, we'll prove for orthogonal sets of qudits.
Exercise 3.5.8: No-Deletion theorem. No unitary from |ψψA⟩ to |ψ0B⟩ for fixed ancilla states A and B. ❓
Definition 3.6.1: Entangled pure states.
✅ Ket.IsEntangled in QuantumInfo.Finite.Braket
Exercise 3.6.1, 3.6.2: The Bell state = ( |++⟩ + |--⟩ )/√2. This means shared randomness in Z or X basis.
🤷 Too specific. Could say something like "the Bell state is identical in many bases", which is Exercise 3.7.12.
Exercise 3.6.3: Cloning implies signalling. 🤷 If we can prove that cloning doesn't exist, this gives an immediate exfalso proof, so this isn't interesting.
CHSH Game ❓ Defining it, giving optimal classical and quantum strategies.
Exercise 3.6.5, 3.66, 3.6.7: Numerical exercises with Bell states. 🤷 Maybe just defining Bell states as a basis for 2-qubit states.
Exercise 3.7.1 - 3.7.11: Lemmas about qudit X and Z operators. ❓ Sure, if we define them.
Exercise 3.7.12: "Transpose trick" for Bell state |Φ⟩, that (U⊗I)|Φ⟩=(I⊗Uᵀ)|Φ⟩.
✅ transposeTrick in Braket.lean.
Theorem 3.8.1, Exercise 3.8.1: Schmidt Decomposition. ❓
Exercise 3.8.2: Schmidt decomposition determines if a state is entangled or product. ❓
Definition 4.1.1: Matrix trace.
✅ Matrix.trace in Mathlib.
Exercise 4.1.1: The trace is cyclic.
✅ Matrix.trace_mul_cycle in Mathlib.
Definition 4.1.2: Defining the density operator of an ensemble. ❓ We define density operators, but could write an "of_ensemble" function.
Exercise 4.1.2: The density matrix of pure (indicator 0).
🤷 Feels specific and not like a useful lemma.
Exercise 4.1.3: Matrix trace as the expectation value of maximally entangled state. ❓
Exercise 4.1.4: Trace of operator functions, Tr[f(GG*)] = Tr[f(G*G)].
❓ Requires Definition 3.3.1 first.
Exercise 4.1.5: Computing density operators of some particular ensembles. 🤷
Exercise 4.1.6: The spectrum of a density operator forms a distribution.
✅ MState.spectrum is a Distribution, in QuantumInfo.Finite.MState.
Definition 4.1.3: The density operator is a PSD operator with trace 1.
✅ MState in QuantumInfo.Finite.MState.
Definition 4.1.4: The maximally mixed state.
✅ MState.uniform in QuantumInfo.Finite.MState.
Exercise 4.1.7: A uniform ensemble of {|0⟩, |1⟩, |+⟩, |-⟩} is the maximally mixed state. 🤷
Exercise 4.1.8: The set of density operators is a convex set.
✅ MState.instMixable in QuantumInfo.Finite.MState.
Definition 4.1.5: Purity of a mixed state.
✅ MState.purity in QuantumInfo.Finite.MState.
Exercise 4.1.9: Purity is equal to 1 iff the state is pure.
✅ MState.pure_iff_purity_one in QuantumInfo.Finite.MState.
Exercise 4.1.10-4.1.13: Specific to qubits and the Bloch sphere. ❓
Unitary Evolution of a Mixed State
✅ MState.U_conj in QuantumInfo.Finite.Unitary
Evolution of an ensemble of mixed states ❓ Could define ensemble as distribution over a finite set of MStates.
Exercise 4.1.14, 4.1.15: Some facts about embedding classical probabilities into quantum states. 🤷 Probably not useful for anything else.
Definition 4.2.1: POVMs as PSD matrices that sum to the identity.
✅ POVM in QuantumInfo.Finite.POVM.
Exercise 4.2.1: The five "Chrysler" states on a qubit, scaled down by (2/5), form a POVM. 🤷 Very specific.
Exercise 4.2.2(a): Suppose an ensemble ρ_X has a bound τ, so that ∀(x ∈ X), τ ≽ p_x ρ(x). Then the maximum expected probability of a POVM identifying x from the distribution is at most Tr[τ]. Exercise 4.2.2(b): In a d dimensional ensemble, no more than d possible symbols can be lossessly stored. ❓ Seems unlikely to be used later but fine to state and prove.
Definition 4.3.1: Product State (density operator).
✅ MState.prod in QuantumInfo.Finite.MState constructs product states. No predicate form.
Exercise 4.3.1(a): ρ.purity = (U_swap * ρ ⊗ ρ).trace.
Exercise 4.3.1(b): For an operator function f, Tr[f(ρ)] = ( f(ρ) ⊗ I(d) ).swap.trace.
❓ Should be an easy index chase.
Exercise 4.3.2: Just a step of a scenario, not really a theorem. 🤷
Exercise 4.3.3: Every separable state Σ x, ρx ⊗ σx is also of the form ∑ x, pure (φ x) ⊗ pure (ψ x).
Definition 4.3.2: Separable state.
✅ MState.IsSeparable in QuantumInfo.Finite.MState.
Definition 4.3.3: Entangled (mixed) state.
✅ MState.IsEntangled in QuantumInfo.Finite.MState.
Exercise 4.3.4: Convexity of separable states.
❓ Will have to write this as Mixable { ρ : MState (d₁ × d₂) // ρ.IsSeparable }.