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 fo 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.
Excercise 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ᵀ)|Φ⟩.
❓
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 }.