Lean, informalized

Lean, informalized

With the help of AI, theorems in mathematics, physics and engineering are now found and proved in Lean, at a pace and scale that no group of people could match. The promise is a body of knowledge that is both vast and certain, but it is written in a language that few scientists can read. For most of the scientific community, it remains out of reach.

A formal result has two parts, and they are trusted in different ways. The first is the proof. Lean’s kernel checks it step by step, by a deterministic procedure with neither AI nor any statistical process in it. A proof the kernel accepts is certified correct, independently of any human judgment. The second is the statement: what exactly has been proved. No machine can settle whether a statement means what a scientist takes it to mean, so this part needs human verification, and a scientist can verify only what they can read.

AxInform is built to support this second part, by bridging the semantic gap between what a statement means in Lean and what a scientist takes it to mean. It states each result of a Lean library as a scientist of the field would, and links every sentence to the Lean declaration behind it, so that a reader can confirm, claim by claim, that what was proved is what they think it is.

In Lean

theorem bellPhiPlus_ne_tmul (a b : PureState qubit) : bellPhiPlus ≠ a ⊗ b

In words

The Bell state |Φ+⟩=(|00⟩+|11⟩)/2|\Phi^+\rangle = (|00\rangle + |11\rangle)/\sqrt{2} is not a product state: for every pair of pure states aa and bb of a single qubit, it differs from the product aa ⊗\otimes bb.

A claim of Exercise 2.68. Hovering over a phrase finds the Lean it stands for. Read the page

A working example: AxQM

AxQM is a Lean library that formalizes 479 items of Nielsen & Chuang’s Quantum Computation and Quantum Information: 381 exercises, 55 theorems, 33 problems, and ten propositions, corollaries and lemmas, from ten chapters of the book. Each has a page written by AxInform, listed below by chapter.

Chapter 2 Introduction to quantum mechanics 77 items
  1. Exercise 2.1 Three dependent vectors in two complex dimensions. p. 63
  2. Exercise 2.2 The matrix of an operator depends on the basis. p. 64
  3. Exercise 2.6 An inner product is conjugate linear in its first argument. p. 66
  4. Exercise 2.7 Two orthogonal vectors and their normalized forms. p. 66
  5. Exercise 2.8 Gram-Schmidt vectors of a basis span the space. p. 66
  6. Exercise 2.9 The four Pauli matrices as combinations of outer products. p. 68
  7. Exercise 2.10 The outer product of two basis vectors is a matrix unit. p. 68
  8. Exercise 2.11 Eigenvectors and diagonal forms of the Pauli matrices. p. 69
  9. Exercise 2.12 The shear of a qubit has no diagonal form. p. 69
  10. Exercise 2.14 The adjoint conjugates the coefficients of a sum. p. 70
  11. Exercise 2.17 Normal matrices are Hermitian exactly when their spectrum is real. p. 70
  12. Exercise 2.18 Eigenvalues of a unitary have modulus one. p. 71
  13. Exercise 2.20 An operator’s matrix under a change of orthonormal basis. p. 71
  14. Exercise 2.21 Hermitian means real and diagonal in an orthonormal basis. p. 71
  15. Exercise 2.22 Eigenvectors of a Hermitian operator with different eigenvalues are orthogonal. p. 71
  16. Exercise 2.23 Every eigenvalue of a projector is zero or one. p. 71
  17. Exercise 2.24 A positive operator is Hermitian. p. 71
  18. Theorem 2.1 Normal operators are those diagonal in an orthonormal basis. p. 72
  19. Exercise 2.26 Two and three copies of the plus state. p. 74
  20. Exercise 2.27 Tensor products of Pauli matrices depend on the order. p. 74
  21. Exercise 2.28 Complex conjugation distributes over the tensor product. p. 74
  22. Exercise 2.30 The tensor product of two Hermitian operators is Hermitian. p. 74
  23. Exercise 2.31 Tensor products of positive operators are positive. p. 74
  24. Exercise 2.32 A tensor product of projectors is a projector. p. 74
  25. Exercise 2.33 The Hadamard transform as a matrix of signs. p. 74
  26. Exercise 2.34 The square root and the logarithm of a matrix. p. 75
  27. Exercise 2.36 The Pauli matrices XX and YY have trace zero. p. 76
  28. Exercise 2.39 The Gell-Mann matrices form an orthonormal Hermitian basis. p. 76
  29. Theorem 2.2 Hermitian operators commute exactly when they share an eigenbasis. p. 77
  30. Exercise 2.40 The commutator of two Pauli matrices gives the third. p. 77
  31. Theorem 2.3 Every operator is a unitary times a positive one. p. 78
  32. Exercise 2.41 Any two different Pauli matrices other than II anticommute. p. 78
  33. Exercise 2.42 A product is half the sum of commutator and anticommutator. p. 78
  34. Exercise 2.43 The multiplication table of the Pauli matrices. p. 78
  35. Exercise 2.44 Commuting and anticommuting with an invertible operator forces zero. p. 78
  36. Exercise 2.45 The adjoint of a commutator is a commutator of adjoints. p. 78
  37. Exercise 2.47 An imaginary multiple of a commutator of Hermitian operators is Hermitian. p. 78
  38. Corollary 2.4 Every square matrix is diagonal between two unitaries. p. 79
  39. Exercise 2.48 Polar decompositions of positive, unitary and Hermitian matrices. p. 79
  40. Exercise 2.49 A normal operator factors into its moduli and phases. p. 79
  41. Exercise 2.50 Left and right polar decompositions of one matrix. p. 79
  42. Exercise 2.52 Two Hadamard gates in a row cancel. p. 82
  43. Exercise 2.53 The Hadamard gate has eigenvalues plus and minus one. p. 82
  44. Exercise 2.55 Evolution under a Hamiltonian is unitary. p. 84
  45. Exercise 2.56 Unitaries as exponentials of Hermitian matrices. p. 84
  46. Exercise 2.57 Two measurements in succession make one measurement. p. 86
  47. Exercise 2.58 An observable has a sharp value in its eigenstates. p. 88
  48. Exercise 2.59 The average and spread of XX in the state |0⟩|0\rangle. p. 90
  49. Exercise 2.60 Eigenvalues and eigenprojectors of a Pauli observable. p. 90
  50. Exercise 2.61 Measuring a qubit along an arbitrary axis. p. 90
  51. Exercise 2.62 A measurement equal to its own POVM is projective. p. 92
  52. Exercise 2.63 Measurement operators as a unitary times a square root. p. 92
  53. Exercise 2.64 Telling linearly independent states apart with certainty. p. 93
  54. Exercise 2.65 No relative phase between plus and minus in their basis. p. 93
  55. Exercise 2.66 X⊗ZX \otimes Z on a Bell pair averages to zero. p. 94
  56. Exercise 2.67 An operator preserving inner products extends to a unitary. p. 95
  57. Exercise 2.68 The Bell state is not a product of qubit states. p. 96
  58. Exercise 2.69 The Bell states form an orthonormal basis of two qubits. p. 98
  59. Exercise 2.70 The Bell states agree on every observable of one qubit. p. 98
  60. Theorem 2.5 Every density operator comes from an ensemble. p. 101
  61. Theorem 2.6 Ensembles of the same state differ by a unitary. p. 103
  62. Exercise 2.71 Purity at most one, with equality exactly for pure states. p. 103
  63. Exercise 2.72 Qubit states as points of the Bloch ball. p. 105
  64. Exercise 2.73 Minimal ensembles for ρ\rho can contain any pure state in its support. p. 105
  65. Exercise 2.74 The reduced state of a product state is pure. p. 106
  66. Exercise 2.75 Each half of a Bell state is maximally mixed. p. 106
  67. Theorem 2.7 A pure state of two systems as a single sum. p. 109
  68. Exercise 2.76 The Schmidt number is at most the smaller dimension. p. 110
  69. Exercise 2.77 A state of three qubits with no triorthogonal form. p. 110
  70. Exercise 2.78 When a pure state of two systems is a product. p. 110
  71. Exercise 2.79 Three states of two qubits in Schmidt form. p. 111
  72. Exercise 2.80 Pure states with equal Schmidt coefficients differ by local unitaries. p. 111
  73. Exercise 2.81 Two purifications differ by a unitary on the reference. p. 111
  74. Exercise 2.82 Measuring the reference system recovers the ensemble. p. 111
  75. Problem 2.1 Functions of a Pauli observable depend on two values. p. 117
  76. Problem 2.2 The Schmidt number as a rank, with two bounds. p. 117
  77. Problem 2.3 An operator identity and Tsirelson’s bound for two qubits. p. 118
Chapter 4 Quantum circuits 56 items
  1. Exercise 4.1 Where the Pauli eigenstates sit on the Bloch sphere. p. 174
  2. Theorem 4.1 Every qubit gate from rotations about two axes. p. 175
  3. Exercise 4.2 The matrix of a rotation about the xx axis. p. 175
  4. Exercise 4.3 The T gate acts as a rotation about the zz axis. p. 175
  5. Exercise 4.4 The Hadamard gate as three rotations and a phase. p. 175
  6. Exercise 4.6 Rotation gates turn the Bloch vector about their axis. p. 175
  7. Exercise 4.7 Conjugating YY by XX reverses its sign. p. 175
  8. Exercise 4.8 Every qubit gate is a phase times a rotation. p. 175
  9. Corollary 4.2 A qubit gate from two bit flips and three gates. p. 176
  10. Exercise 4.9 Every qubit unitary as a phase and three rotations. p. 176
  11. Exercise 4.10 Every qubit gate from rotations about xx and yy. p. 176
  12. Exercise 4.11 Three rotations about two axes. p. 176
  13. Exercise 4.12 The Hadamard gate from rotations about two axes. p. 176
  14. Exercise 4.13 Between two Hadamard gates, XX and ZZ trade places. p. 177
  15. Exercise 4.14 Conjugating TT by HH gives an xx rotation. p. 177
  16. Exercise 4.15 The product of two rotations of a qubit. p. 177
  17. Exercise 4.16 Matrices of a Hadamard on one of two qubits. p. 178
  18. Exercise 4.17 A CNOT from a controlled Z and two Hadamards. p. 179
  19. Exercise 4.18 The controlled Z gate is symmetric in its two qubits. p. 179
  20. Exercise 4.19 The controlled NOT gate rearranges a density matrix. p. 179
  21. Exercise 4.20 Hadamard gates turn the controlled NOT around. p. 179
  22. Exercise 4.21 Five controlled gates build a doubly controlled unitary. p. 181
  23. Exercise 4.22 A doubly controlled gate from six controlled NOTs. p. 181
  24. Exercise 4.23 Controlled rotations from two controlled NOT gates. p. 181
  25. Exercise 4.24 Figure 4.9, gate by gate. p. 182
  26. Exercise 4.25 The Fredkin gate from Toffoli gates and two qubit gates. p. 182
  27. Exercise 4.26 Rotations and controlled NOTs give the Toffoli gate up to phases. p. 183
  28. Exercise 4.27 Eight CNOT and Toffoli gates cycle seven basis states. p. 183
  29. Exercise 4.28 Five controls on a squared unitary without work qubits. p. 184
  30. Exercise 4.29 The multiply controlled NOT in quadratically many gates. p. 184
  31. Exercise 4.30 Multiply controlled gates from quadratically many elementary gates. p. 184
  32. Exercise 4.31 Pushing Pauli operators through a CNOT gate. p. 185
  33. Exercise 4.32 An unread measurement leaves the partner system unchanged. p. 187
  34. Exercise 4.33 A circuit that measures in the Bell basis. p. 187
  35. Exercise 4.34 Measuring a Hermitian unitary with a control qubit. p. 188
  36. Exercise 4.35 Measuring the control qubit commutes with the controlled gate. p. 188
  37. Exercise 4.36 Three gates add two numbers modulo four. p. 189
  38. Exercise 4.37 The two-qubit Fourier transform as five two-level unitaries. p. 191
  39. Exercise 4.38 A unitary with no short two-level decomposition. p. 191
  40. Exercise 4.39 Building a two level unitary on three qubits. p. 193
  41. Exercise 4.40 When powers of a rotation approximate other rotations about its axis. p. 196
  42. Exercise 4.41 A rotation by arccos⁡(3/5)\arccos(3/5) with probability 5/85/8. p. 197
  43. Exercise 4.42 Cosine three fifths gives an irrational fraction of a turn. p. 198
  44. Exercise 4.43 Hadamard, phase, CNOT and Toffoli with measurement are universal. p. 198
  45. Exercise 4.44 A single three qubit gate is universal. p. 198
  46. Exercise 4.45 Gate products keep their scaled integer form. p. 198
  47. Exercise 4.46 Real parameters of a traceless Hermitian matrix on nn qubits. p. 205
  48. Theorem 4.3 Alternating short steps give the exponential of a sum. p. 207
  49. Exercise 4.47 Commuting terms split the time evolution. p. 207
  50. Exercise 4.48 Local Hamiltonians have polynomially many terms. p. 207
  51. Exercise 4.49 Three product formulas for the exponential of a sum. p. 208
  52. Exercise 4.50 The symmetric Trotter step has cubic error. p. 208
  53. Exercise 4.51 Simulating a Pauli string Hamiltonian by a change of basis. p. 210
  54. Problem 4.1 Turning a reversible computation into a phase. p. 212
  55. Problem 4.3 Any unitary as a limit of Trotter products of Pauli exponentials. p. 212
  56. Problem 4.6 Single qubit gates and a teleported controlled NOT are universal. p. 213
Chapter 5 The quantum Fourier transform and its applications 31 items
  1. Exercise 5.1 The quantum Fourier transform is a unitary matrix. p. 217
  2. Exercise 5.2 The Fourier transform sends zero to the uniform superposition. p. 217
  3. Exercise 5.3 Operation counts of the direct and the fast Fourier transform. p. 221
  4. Exercise 5.4 A controlled phase gate from two CNOT gates. p. 221
  5. Exercise 5.5 Undoing the quantum Fourier transform on a qudit. p. 221
  6. Exercise 5.6 Phase errors add up over the Fourier circuit’s gates. p. 221
  7. Exercise 5.7 Controlled powers raise a unitary to the controls’ value. p. 222
  8. Exercise 5.8 Each eigenstate’s estimate survives in proportion to its weight. p. 225
  9. Exercise 5.9 Measuring a Hermitian unitary with a controlled gate. p. 225
  10. Exercise 5.10 The order of 5 modulo 21 is 6. p. 226
  11. Exercise 5.12 Multiplication modulo NN by a number coprime to it is unitary. p. 227
  12. Exercise 5.13 Undoing the Fourier sum of the order finding eigenstates. p. 227
  13. Exercise 5.14 Modular addition prepares the state of order finding. p. 227
  14. Theorem 5.1 A close fraction that is not a convergent. p. 229
  15. Exercise 5.16 Inverse prime squares sum to at most three quarters. p. 231
  16. Theorem 5.2 A nontrivial square root of one gives a factor. p. 233
  17. Theorem 5.3 The bound on good units, corrected by one power of two. p. 233
  18. Exercise 5.18 Factoring 91 with the order of 4. p. 234
  19. Exercise 5.19 Fifteen is the smallest number that needs order finding. p. 234
  20. Exercise 5.20 A periodic function transforms into evenly spaced peaks. p. 238
  21. Exercise 5.21 Fourier states are eigenstates of every cyclic shift. p. 238
  22. Exercise 5.22 The double Fourier sum reduces to one eigenstate. p. 239
  23. Exercise 5.23 Inverting the Fourier transform of the discrete logarithm. p. 239
  24. Exercise 5.24 Recovering a discrete logarithm from two phase estimates. p. 239
  25. Exercise 5.26 A character sum splits along the cyclic factors. p. 242
  26. Problem 5.1 Phase estimation of the cyclic shift on a prime qudit. p. 243
  27. Problem 5.2 Measuring the Fourier transform one qubit at a time. p. 243
  28. Problem 5.3 A controlled unitary turns an eigenphase into a probability. p. 243
  29. Problem 5.4 Fast multiplication brings quantum factoring below cubic cost. p. 244
  30. Problem 5.5 Logarithmically many samples separate two hidden subgroups. p. 244
  31. Problem 5.6 Adding a constant as a phase in the Fourier basis. p. 244
Chapter 6 Quantum search algorithms 20 items
  1. Exercise 6.1 The Grover phase shift in terms of a projector. p. 251
  2. Exercise 6.2 Each amplitude is reflected through the mean. p. 251
  3. Exercise 6.3 The sine of the Grover rotation angle. p. 252
  4. Exercise 6.4 Searching for several solutions succeeds at least half the time. p. 254
  5. Exercise 6.5 Marking solutions only when the extra qubit is zero. p. 255
  6. Exercise 6.6 The dotted box circuit is a conditional phase shift. p. 255
  7. Exercise 6.7 Two oracle circuits that evolve a state under a projector. p. 258
  8. Exercise 6.9 A simulation step of quantum search in closed form. p. 259
  9. Exercise 6.10 Two alternating evolutions find the marked item exactly. p. 260
  10. Exercise 6.11 A Hamiltonian that finds one of several solutions. p. 261
  11. Exercise 6.12 A Hamiltonian that finds the marked state in fixed time. p. 261
  12. Exercise 6.13 Classical sampling needs order NN draws to count solutions. p. 261
  13. Exercise 6.14 Classical counting needs a linear number of queries. p. 262
  14. Exercise 6.15 A lower bound on squared distances to an orthonormal set. p. 270
  15. Exercise 6.16 Search with average success needs order N\sqrt{N} queries. p. 270
  16. Exercise 6.17 A query lower bound for search with several solutions. p. 271
  17. Exercise 6.18 Multilinear polynomials agreeing on the Boolean cube are equal. p. 273
  18. Exercise 6.19 A polynomial that equals OR on every string of bits. p. 273
  19. Problem 6.2 Three reflection oracles told apart by one Bell measurement. p. 274
  20. Exercise 6.20 Computing OR without error takes a query per bit. p. 274
Chapter 7 Quantum computers: physical realization 36 items
  1. Exercise 7.7 A phase shifter on one mode of a dual rail qubit. p. 291
  2. Exercise 7.9 A Hadamard gate from a phase shifter and a beamsplitter. p. 292
  3. Exercise 7.10 An interferometer turns a phase shift into a qubit rotation. p. 292
  4. Exercise 7.13 Deutsch’s algorithm from beamsplitters and a Kerr gate. p. 294
  5. Exercise 7.16 Dipole selection rules for the orbital and magnetic quantum numbers. p. 300
  6. Exercise 7.18 The time evolution of an atom coupled to a cavity mode. p. 303
  7. Exercise 7.21 The phase acquired by two photons coupled to an atom. p. 305
  8. Exercise 7.22 Absorption of one photon, alone or from a pair. p. 306
  9. Exercise 7.23 A controlled NOT from a Kerr phase and single qubit gates. p. 308
  10. Exercise 7.25 Total spin of two qubits obeys the angular momentum relations. p. 314
  11. Exercise 7.26 Two spins combine into a triplet and a singlet. p. 314
  12. Exercise 7.27 Three spins one half form a quartet and two doublets. p. 314
  13. Exercise 7.28 Adding a nuclear spin 3/2 to an electron spin. p. 315
  14. Exercise 7.29 An atom’s decay probability grows linearly in time. p. 316
  15. Exercise 7.31 The Hadamard gate as two rotations and a phase. p. 319
  16. Exercise 7.32 CNOT, up to a phase flip, from controlled Z and two rotations. p. 324
  17. Exercise 7.35 The dipolar coupling averages to zero over all directions. p. 328
  18. Exercise 7.36 Thermal states of one and two nuclear spins. p. 329
  19. Exercise 7.37 Four lines from three spins, a doublet from two. p. 329
  20. Exercise 7.38 Conjugating by XX runs free precession backward. p. 332
  21. Exercise 7.39 Pauli conjugations average a qubit term to zero. p. 332
  22. Exercise 7.40 Refocusing pulses reduce the dipolar coupling to one term. p. 332
  23. Exercise 7.41 Controlled Z from a spin coupling and two rotations. p. 332
  24. Exercise 7.42 Two CNOT gates permute three populations cyclically. p. 334
  25. Exercise 7.43 Three gates that relabel the populations of three spins. p. 335
  26. Exercise 7.44 How large an effective pure manifold can be. p. 335
  27. Exercise 7.45 Nine experiments fix the state of two spins. p. 336
  28. Exercise 7.46 Spin tomography needs every choice of measurement axes. p. 337
  29. Exercise 7.47 Two coupled spins make a controlled NOT up to phases. p. 338
  30. Exercise 7.48 A pulse sequence that prepares a Bell state. p. 338
  31. Exercise 7.49 A SWAP gate from rotations and a spin coupling. p. 338
  32. Exercise 7.50 Pulse sequences for three Grover oracles. p. 339
  33. Exercise 7.51 Shortening the Grover iteration on two nuclear spins. p. 339
  34. Exercise 7.52 Exchange between two spins gives a swap and a CNOT. p. 345
  35. Problem 7.1 Cycling the nonzero bit strings with quadratically many gates. p. 346
  36. Problem 7.2 Beamsplitters and phase shifters build any unitary, at exponential cost. p. 346
Chapter 8 Quantum noise and quantum operations 37 items
  1. Exercise 8.1 A pure state evolves as its density operator does. p. 357
  2. Exercise 8.2 Outcome probability and collapse from a single operator. p. 357
  3. Exercise 8.3 An operator sum when input and output systems differ. p. 361
  4. Exercise 8.4 A controlled flip on the environment dephases the qubit. p. 361
  5. Exercise 8.5 A spin flip through an environment has two operation elements. p. 361
  6. Exercise 8.7 A joint measurement seen from the principal system. p. 364
  7. Exercise 8.8 Completing operation elements to a unitary model. p. 365
  8. Exercise 8.9 Operations realized by a unitary and an environment measurement. p. 366
  9. Theorem 8.1 Quantum operations are the maps with an operator sum. p. 368
  10. Theorem 8.2 Operator-sum forms of one operation differ by a unitary. p. 372
  11. Theorem 8.3 No more operation elements than the dimension squared. p. 373
  12. Exercise 8.10 Mixing operation elements into orthogonal ones. p. 373
  13. Exercise 8.11 A bound on the number of operation elements. p. 373
  14. Exercise 8.12 Trading an orthogonal factor for a rotation. p. 375
  15. Exercise 8.13 Every qubit unitary is a rotation of the Bloch ball. p. 375
  16. Exercise 8.14 A rotation times a symmetric factor of negative determinant. p. 375
  17. Exercise 8.16 Projecting onto zero is not an affine Bloch map. p. 378
  18. Exercise 8.17 Averaging over the Pauli matrices gives the maximally mixed state. p. 379
  19. Exercise 8.18 The depolarizing channel never increases a trace power. p. 379
  20. Exercise 8.19 Operation elements of the depolarizing channel on a qudit. p. 379
  21. Exercise 8.20 Amplitude damping from a circuit on two qubits. p. 380
  22. Exercise 8.21 Amplitude damping from a beam splitter coupling. p. 381
  23. Exercise 8.22 Amplitude damping of a qubit, entry by entry. p. 381
  24. Exercise 8.23 A damped dual-rail qubit stays intact or leaves the code. p. 381
  25. Exercise 8.24 Spontaneous emission into one mode is amplitude damping. p. 381
  26. Exercise 8.25 A qubit’s populations fix its temperature. p. 382
  27. Exercise 8.26 Phase damping from a single controlled rotation. p. 385
  28. Exercise 8.27 A unitary that turns phase damping into a phase flip. p. 385
  29. Exercise 8.28 Phase damping from a controlled flip on the environment. p. 386
  30. Exercise 8.29 Depolarizing and phase damping are unital, amplitude damping is not. p. 386
  31. Exercise 8.31 Random phase kicks damp each coherence by a Gaussian factor. p. 386
  32. Exercise 8.33 Fixing an affine Bloch map takes at least four points. p. 394
  33. Exercise 8.34 Recovering a two-qubit process from sixteen outputs. p. 394
  34. Exercise 8.35 The process matrix of amplitude damping from tomography. p. 394
  35. Problem 8.1 Amplitude damping as the solution of a master equation. p. 395
  36. Problem 8.2 Teleportation results that Bob can undo determine the input. p. 395
  37. Problem 8.3 Unital qubit channels are mixtures of unitaries. p. 396
Chapter 9 Distance measures for quantum information 33 items
  1. Exercise 9.1 The trace distance between two pairs of distributions. p. 400
  2. Exercise 9.2 Trace distance of two distributions on two outcomes. p. 400
  3. Exercise 9.3 Classical fidelity of two pairs of distributions. p. 400
  4. Exercise 9.4 Trace distance as the largest difference on one event. p. 401
  5. Exercise 9.5 The trace distance as a maximum over events. p. 401
  6. Exercise 9.6 Trace distances between qubit mixtures in two bases. p. 403
  7. Theorem 9.1 Trace distance as the largest distance between measurement statistics. p. 405
  8. Exercise 9.7 Two states differ by orthogonal positive operators. p. 405
  9. Theorem 9.2 A quantum channel never increases the trace distance. p. 406
  10. Theorem 9.3 How far apart two mixtures of states can be. p. 407
  11. Exercise 9.8 The trace distance is convex in each argument. p. 408
  12. Exercise 9.9 Every quantum channel fixes some state. p. 408
  13. Exercise 9.10 A strictly contractive channel has exactly one fixed state. p. 408
  14. Exercise 9.11 A partly resetting channel has one fixed point. p. 408
  15. Exercise 9.12 Depolarizing noise brings qubit states closer together. p. 409
  16. Exercise 9.13 Fixed points and contraction of the bit flip channel. p. 409
  17. Theorem 9.4 Fidelity as the largest overlap of purifications. p. 410
  18. Lemma 9.5 The trace norm as a maximum over unitaries. p. 410
  19. Exercise 9.14 Fidelity is unchanged by a common unitary evolution. p. 410
  20. Exercise 9.15 Fidelity as the largest overlap with a fixed purification. p. 411
  21. Exercise 9.16 The maximally entangled vector gives the transpose, not the adjoint. p. 411
  22. Exercise 9.17 Bounds on the angle between two states. p. 413
  23. Theorem 9.6 Fidelity never decreases under a quantum channel. p. 414
  24. Theorem 9.7 Fidelity of two mixtures dominates a weighted sum of fidelities. p. 414
  25. Exercise 9.18 A channel never widens the angle between two states. p. 414
  26. Exercise 9.19 Fidelity of mixtures is at least the average fidelity. p. 415
  27. Exercise 9.20 The fidelity is concave in its first entry. p. 415
  28. Exercise 9.21 Trace distance dominates one minus squared fidelity. p. 416
  29. Exercise 9.22 Two successive gates err by at most the sum of their errors. p. 418
  30. Exercise 9.23 Average fidelity is one exactly when the source’s states are left unchanged. p. 419
  31. Problem 9.1 The squared fidelity is an infimum over positive operators. p. 423
  32. Problem 9.2 All of the entanglement fidelity in one operation element. p. 423
  33. Problem 9.3 Fidelity on the support bounds the entanglement fidelity. p. 423
Chapter 10 Quantum error-correction 85 items
  1. Exercise 10.1 Encoding a qubit in the three qubit bit flip code. p. 428
  2. Exercise 10.2 The bit flip channel as an occasional measurement of XX. p. 429
  3. Exercise 10.3 Two parity checks give the bit flip syndrome. p. 430
  4. Exercise 10.4 Eight projectors diagnose a bit flip but spoil superpositions. p. 432
  5. Exercise 10.5 The phase flip syndrome of Shor’s code compares block signs. p. 433
  6. Exercise 10.6 Undoing a phase flip on any of three qubits. p. 433
  7. Theorem 10.1 A recovery exists exactly when the error correction conditions hold. p. 436
  8. Theorem 10.2 Correcting a set of errors corrects their linear combinations. p. 438
  9. Exercise 10.7 The bit flip code satisfies the error correction conditions. p. 438
  10. Exercise 10.8 The phase flip code satisfies the error correction conditions. p. 441
  11. Exercise 10.9 The phase flip code protects against projector errors. p. 441
  12. Exercise 10.10 The Shor code satisfies the error correction conditions. p. 441
  13. Exercise 10.11 Averaging over the four Paulis leaves the maximally mixed state. p. 441
  14. Exercise 10.12 The least fidelity of the depolarizing channel. p. 441
  15. Exercise 10.13 Least fidelity of a pure state under amplitude damping. p. 443
  16. Exercise 10.14 Encoding by repetition as a linear code. p. 446
  17. Exercise 10.15 Column addition leaves a linear code unchanged. p. 446
  18. Exercise 10.16 Row operations on a parity check matrix keep its code. p. 447
  19. Exercise 10.17 A parity check matrix for the repetition code. p. 447
  20. Exercise 10.18 A parity check matrix annihilates its generator matrix. p. 447
  21. Exercise 10.19 The generator matrix for a parity check matrix in standard form. p. 447
  22. Exercise 10.20 Distance of a linear code read off its parity check columns. p. 448
  23. Exercise 10.21 Redundancy bounds the minimum distance of a linear code. p. 449
  24. Exercise 10.22 Hamming codes have distance three and correct one error. p. 449
  25. Exercise 10.23 Error-correcting binary linear codes exist up to an entropy bound. p. 449
  26. Exercise 10.24 Weak self-duality read off the generator matrix. p. 450
  27. Exercise 10.25 Summing signs over a code detects its dual. p. 450
  28. Exercise 10.26 A circuit of controlled NOT gates computes the syndrome. p. 451
  29. Exercise 10.27 Signed and shifted CSS codes correct the same errors. p. 452
  30. Exercise 10.28 A transposed check matrix generates the Hamming code. p. 452
  31. Exercise 10.29 The stabilized space as a subspace and an intersection. p. 454
  32. Exercise 10.30 A Pauli subgroup without −I-I has neither iIiI nor −iI-iI. p. 455
  33. Exercise 10.32 The six Steane generators fix both codewords. p. 456
  34. Proposition 10.3 Generators are independent exactly when their check rows are. p. 457
  35. Exercise 10.33 Two Pauli strings commute exactly when their twisted product vanishes. p. 457
  36. Exercise 10.34 Which generators keep minus the identity out of a stabilizer. p. 457
  37. Exercise 10.35 Elements of a Pauli subgroup without −I-I square to II. p. 457
  38. Proposition 10.4 Flipping one sign among independent Pauli strings. p. 458
  39. Proposition 10.5 The dimension of the space a stabilizer fixes. p. 458
  40. Exercise 10.36 How CNOT conjugates the Pauli operators of two qubits. p. 460
  41. Exercise 10.37 YY on the control picks up XX on the target. p. 460
  42. Theorem 10.6 Unitaries normalizing the Pauli group as short Clifford circuits. p. 461
  43. Exercise 10.38 Four conjugations fix a unitary only up to a phase. p. 461
  44. Exercise 10.39 The phase gate carries XX to YY and leaves ZZ fixed. p. 461
  45. Exercise 10.40 Each normalizer gate is a short Clifford circuit up to phase. p. 462
  46. Exercise 10.41 Pauli operators under the Toffoli and π/8\pi/8 gates. p. 462
  47. Theorem 10.7 Stabilizer circuits simulated efficiently on a classical computer. p. 464
  48. Exercise 10.42 Stabilizers check teleportation of XX and ZZ eigenstates. p. 464
  49. Exercise 10.43 A subgroup of the Pauli group lies in its normalizer. p. 465
  50. Theorem 10.8 Which Pauli errors a stabilizer code corrects. p. 466
  51. Exercise 10.44 The normalizer of a Pauli subgroup without −I-I is its centralizer. p. 466
  52. Exercise 10.45 Errors on known qubits are correctable below the distance. p. 467
  53. Exercise 10.46 Two parity checks stabilize the phase flip code. p. 467
  54. Exercise 10.47 Eight generators that fix both Shor codewords. p. 468
  55. Exercise 10.48 The logical XX and ZZ of Shor’s nine qubit code. p. 468
  56. Exercise 10.49 The five qubit code corrects single qubit Pauli errors. p. 469
  57. Exercise 10.50 The five qubit code saturates the quantum Hamming bound. p. 469
  58. Exercise 10.51 The CSS code is a stabilizer code correcting tt errors. p. 470
  59. Exercise 10.52 Flipping all seven qubits exchanges the two Steane logical states. p. 470
  60. Exercise 10.53 The encoded ZZ operators are independent. p. 471
  61. Exercise 10.54 Encoded XX operators from a check matrix in standard form. p. 471
  62. Exercise 10.55 The Steane code’s logical XX from its standard form. p. 471
  63. Exercise 10.56 A commuting unitary carries a fixed state to a fixed state. p. 471
  64. Exercise 10.57 Standard forms of the five qubit and Shor codes. p. 472
  65. Exercise 10.58 Measuring an observable through a control qubit. p. 474
  66. Exercise 10.59 Two parity measurements built from CNOT and Hadamard gates. p. 474
  67. Exercise 10.60 One ancilla qubit records the eigenvalue of a generator. p. 474
  68. Exercise 10.61 Correcting a single qubit error on the Steane code. p. 474
  69. Exercise 10.62 Two concatenated stabilizer codes still encode one qubit. p. 482
  70. Exercise 10.63 Exchanging X‾\bar X and Z‾\bar Z while preserving the code is the encoded Hadamard. p. 482
  71. Exercise 10.65 Swapping a qubit with one controlled NOT and a measurement. p. 487
  72. Exercise 10.66 Applying the T gate through an ancilla and a measurement. p. 487
  73. Exercise 10.67 Two circuit identities for the Toffoli gate. p. 487
  74. Exercise 10.68 Applying a Toffoli gate without applying it to the data. p. 488
  75. Exercise 10.69 A single fault leaves at most one bit flip. p. 491
  76. Exercise 10.70 A phase flip on the ancilla changes only the readout. p. 491
  77. Exercise 10.71 Measuring e−iπ/4SXe^{-i\pi/4}SX to prepare the π/8\pi/8 ancilla. p. 491
  78. Exercise 10.72 Three stabilizers single out the Toffoli ancilla. p. 491
  79. Exercise 10.73 Seven operators pin down the Steane logical zero. p. 493
  80. Exercise 10.74 Preparing the encoded zero of the five qubit code. p. 493
  81. Problem 10.1 Codes and recoveries carried across equivalent channels. p. 495
  82. Problem 10.2 Nested classical codes that give good quantum codes. p. 495
  83. Problem 10.3 An encoding circuit for stabilizer codes in standard form. p. 495
  84. Problem 10.4 Encoding a qubit by teleporting it into a code. p. 496
  85. Problem 10.5 Teleporting a CNOT onto two encoded qubits. p. 496
Chapter 11 Entropy and information 47 items
  1. Exercise 11.1 A fair coin or die has the most entropy. p. 501
  2. Exercise 11.2 An additive measure of information is a logarithm. p. 501
  3. Exercise 11.3 The binary entropy is largest at one half. p. 504
  4. Exercise 11.4 The binary entropy is strictly concave. p. 504
  5. Theorem 11.1 Relative entropy vanishes exactly when the distributions agree. p. 505
  6. Theorem 11.2 Only the uniform distribution has entropy log⁡d\log d. p. 505
  7. Exercise 11.5 Joint entropy never exceeds the sum of the marginal entropies. p. 505
  8. Theorem 11.3 Entropy inequalities for two and three random variables. p. 506
  9. Exercise 11.6 Strong subadditivity is tight exactly for Markov chains. p. 507
  10. Exercise 11.7 Conditional entropy as a relative entropy, and its sign. p. 507
  11. Theorem 11.4 Conditional entropy splits one variable at a time. p. 508
  12. Theorem 11.5 Processing cannot increase information about the source. p. 509
  13. Exercise 11.8 Mutual information is not subadditive for a parity bit. p. 509
  14. Exercise 11.9 A bit and its copies defeat superadditivity of mutual information. p. 509
  15. Exercise 11.10 A Markov chain read backwards is a Markov chain. p. 510
  16. Theorem 11.7 The relative entropy of two states is never negative. p. 511
  17. Exercise 11.11 The entropy of two pure qubit states and a mixed one. p. 511
  18. Exercise 11.12 The entropy of a mixture of two nonorthogonal states. p. 511
  19. Theorem 11.6 States close in trace distance have close entropies. p. 512
  20. Theorem 11.8 Bounds on the von Neumann entropy and the entropy of mixtures. p. 513
  21. Exercise 11.13 Entropy adds over independent systems. p. 514
  22. Exercise 11.14 Negative conditional entropy marks entangled pure states. p. 514
  23. Theorem 11.9 A projective measurement never lowers the entropy. p. 515
  24. Exercise 11.15 Resetting a qubit by measurement can lower its entropy. p. 515
  25. Exercise 11.16 Equal reduced states on one side, orthogonal on the other. p. 516
  26. Exercise 11.17 A mixed state attaining the bound of Araki and Lieb. p. 516
  27. Exercise 11.18 Entropy of a mixture equals the average only for equal states. p. 517
  28. Exercise 11.19 Unitary averaging and the unique state of maximal entropy. p. 517
  29. Theorem 11.10 How much entropy mixing states can add. p. 518
  30. Exercise 11.20 Pinching by a projector as a mixture of two unitaries. p. 518
  31. Exercise 11.21 The entropy of a mixture is at least the average entropy. p. 518
  32. Exercise 11.22 The entropy of a mixture is at least the average entropy. p. 518
  33. Exercise 11.23 Joint concavity is stronger than concavity in each variable. p. 519
  34. Theorem 11.11 A trace of two operator powers is jointly concave. p. 520
  35. Theorem 11.12 Mixing pairs of states cannot raise their relative entropy. p. 520
  36. Corollary 11.13 The conditional entropy is concave in the joint state. p. 520
  37. Theorem 11.14 Entropy is strongly subadditive and weakly monotone. p. 521
  38. Exercise 11.24 Two entropies bounded by those of two overlapping pairs. p. 521
  39. Exercise 11.25 The conditional entropy is concave in the joint state. p. 521
  40. Theorem 11.15 Conditioning lowers entropy and local operations never raise mutual information. p. 522
  41. Exercise 11.26 Two mutual informations bounded by twice one entropy. p. 522
  42. Theorem 11.16 Conditional entropy is subadditive in both arguments. p. 523
  43. Theorem 11.17 Discarding a subsystem cannot raise relative entropy. p. 524
  44. Problem 11.1 A convex trace inequality and the sign of relative entropy. p. 525
  45. Problem 11.2 Relative entropy under sums and mixtures of positive operators. p. 525
  46. Problem 11.3 Adding a system can lower quantum conditional entropy. p. 525
  47. Problem 11.4 Strong subadditivity conditioned on a fourth system. p. 526
Chapter 12 Quantum information theory 57 items
  1. Exercise 12.1 Two orthogonal states of a qubit can be cloned. p. 530
  2. Theorem 12.1 The information a measurement yields is bounded by entropies. p. 531
  3. Exercise 12.2 A measurement recorded in a qudit is a channel. p. 533
  4. Exercise 12.3 Each qubit carries at most one bit. p. 535
  5. Exercise 12.4 Four symmetric qubit states carry less than one bit. p. 535
  6. Theorem 12.2 Few typical sequences carry almost all the probability. p. 539
  7. Theorem 12.4 A source compresses reliably above its entropy, not below. p. 540
  8. Theorem 12.3 The average of many trials approaches the mean. p. 541
  9. Exercise 12.5 Compression without error at any rate above the entropy. p. 542
  10. Theorem 12.5 Many copies of a state fill only a typical subspace. p. 543
  11. Theorem 12.6 A quantum source compresses down to its entropy. p. 544
  12. Exercise 12.6 Block fidelity depends only on the Hamming weight. p. 546
  13. Exercise 12.7 Compressing a qubit source above its Shannon entropy. p. 546
  14. Exercise 12.8 Compressing a source of pure states above its entropy. p. 546
  15. Theorem 12.7 The capacity of a noisy channel as maximal mutual information. p. 553
  16. Exercise 12.9 The erasure channel against the binary symmetric channel. p. 553
  17. Exercise 12.10 Two channels in series have no more capacity than either. p. 553
  18. Theorem 12.8 A channel’s product state capacity is its Holevo quantity. p. 555
  19. Exercise 12.11 Pure input states suffice for a channel’s Holevo quantity. p. 555
  20. Theorem 12.9 Entropy exchange bounded by the entanglement fidelity. p. 563
  21. Exercise 12.13 Entropy exchange is concave in the quantum operation. p. 563
  22. Theorem 12.10 Coherent information is capped by entropy and never raised by processing. p. 564
  23. Exercise 12.14 Errors on a decoupled part of a code are correctable. p. 567
  24. Exercise 12.15 Entropy bounds for two quantum operations in turn. p. 568
  25. Exercise 12.16 Perfect recovery exchanges the entropy the noise added. p. 571
  26. Proposition 12.11 Majorized vectors are mixtures of permuted copies. p. 574
  27. Exercise 12.17 Tail sums of two vectors decide majorization. p. 574
  28. Exercise 12.18 Vectors majorized by one vector form a convex set. p. 574
  29. Exercise 12.19 Matching the first entry keeps the rest majorized. p. 574
  30. Theorem 12.13 Majorization as a mixture of unitary conjugates. p. 575
  31. Proposition 12.14 From a pure state, one round of communication suffices. p. 575
  32. Theorem 12.15 Majorization decides when one state converts into another. p. 576
  33. Exercise 12.20 Majorization gives conversion. p. 577
  34. Exercise 12.21 A borrowed qubit that makes a conversion possible. p. 577
  35. Exercise 12.22 Converting one entangled state into another without classical communication. p. 577
  36. Exercise 12.23 Distillable entanglement bounded by the reduced state’s entropy. p. 580
  37. Exercise 12.24 Local operations never raise the Schmidt number. p. 580
  38. Theorem 12.16 A lower bound on entropy after universal hashing. p. 584
  39. Exercise 12.25 Counting the keys a network of users needs. p. 584
  40. Theorem 12.17 Conditioning seldom costs much collision entropy. p. 585
  41. Proposition 12.18 Telling nonorthogonal states apart disturbs them. p. 586
  42. Exercise 12.26 Bob’s bit when the bases match and when they differ. p. 588
  43. Exercise 12.27 Checking a random half rarely misses many errors. p. 589
  44. Exercise 12.28 Bob’s outcome one can occur exactly when the bits differ. p. 591
  45. Exercise 12.29 Six states of a qubit read in matched and mismatched bases. p. 591
  46. Exercise 12.30 A sharply peaked distribution has little entropy. p. 594
  47. Exercise 12.31 The eavesdropper learns at most the entropy of the state. p. 594
  48. Exercise 12.32 Local parities give the two Bell labels. p. 595
  49. Exercise 12.33 Commuting observables have a classical joint distribution. p. 597
  50. Exercise 12.34 Distilling Bell pairs by projecting onto a stabilizer code. p. 597
  51. Exercise 12.35 Phase coset states of a code resolve the identity. p. 598
  52. Exercise 12.36 Bell pairs are a sum of matched coset states. p. 598
  53. Exercise 12.37 Measuring one qubit of a Bell pair fixes both. p. 598
  54. Problem 12.1 The Holevo bound from a quantity that never grows. p. 602
  55. Problem 12.2 Distinct overlapping pure states cannot be cloned. p. 602
  56. Exercise 12.38 Identifying each signal state lets an eavesdropper go unseen. p. 602
  57. Problem 12.4 A machine that copies two states cannot copy their mixtures. p. 603

No item matches.