Lean, informalized

Nielsen & Chuang · Chapter 8, Quantum noise and quantum operations · p. 373

Exercise 8.11 - Every operator sum between spaces of dimensions dd and d′d' can be written with dd′dd' operation elements

A bound on the number of operation elements.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

A quantum operation takes states of a system with state space HH, of dimension dd, to states of a system with state space GG, of dimension d′d'. In operator-sum form it acts through operation elements EiE_i, linear operators from HH to GG, and a given representation may use any finite number of them. The exercise is to show that every quantum operation from HH to GG has an operator-sum representation with dd′dd' operation elements.

The Operator Sum

Let HH and GG be finite-dimensional complex Hilbert spaces. The operator sum of a family {Ei}i∈I\{E_i\}_{i \in I} of linear operators from HH to GG, over a finite index set II, is the linear map from operators on HH to operators on GG that sends ρ\rho to ∑i∈IEiρEi†,\sum_{i \in I} E_i \rho E_i^\dagger ,(1) and the EiE_i are its operation elements.

The Claim

Theorem 1. Let HH and GG be finite-dimensional complex Hilbert spaces of dimensions dd and d′d', and let {Ei}i∈I\{E_i\}_{i \in I} be a finite family of linear operators from HH to GG. Then there are dd′dd' linear operators F1,…,Fdd′F_1, \dots, F_{dd'} from HH to GG with the same operator sum: ∑k=1dd′FkρFk†=∑i∈IEiρEi†for every operator ρ on H.\sum_{k=1}^{dd'} F_k \rho F_k^\dagger = \sum_{i \in I} E_i \rho E_i^\dagger \qquad \text{for every operator $\rho$ on $H$.}(2)✦

The operation elements of any quantum operation from HH to GG form such a family, so this is the exercise.

What Is Checked

The claim is stated over the operator sum (1) of a finite family of operators from HH to GG, and over the dimensions dd and d′d' of the two spaces. What the library proves about the operator sum is the equality (2) of maps on all operators on HH, states among them.