Lean, informalized

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

Theorem 8.3 - Any operator sum on a space of dimension dd rewritten with d2d^2 operation elements

No more operation elements than the dimension squared.

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 on a system acts on its states through a family of operation elements, and the family that describes it is not unique: families of different lengths can give the same operation. Theorem 8.3 bounds the number of operation elements a description needs, in terms of the dimension dd of the system’s state space alone.

Operator Sums

Let HH be the state space of the system, a complex Hilbert space of finite dimension dd. The operator sum ℰ\mathcal{E} of a finite family of operators E1,…,EmE_1, \dots, E_m on HH is the linear map on operators on HH that sends an operator ρ\rho to ℰ(ρ)=∑k=1mEkρEk†.\mathcal{E}(\rho) = \sum_{k=1}^{m} E_k \, \rho \, E_k^\dagger .(1) The EkE_k are its operation elements, or Kraus operators. A quantum operation in operator-sum form is a map ℰ\mathcal{E} that sends an operator ρ\rho to ∑k=1mEkρEk†\sum_{k=1}^m E_k \, \rho \, E_k^\dagger for some finite family of operators E1,…,EmE_1, \dots, E_m on HH.

The Claim

Theorem 1. Let HH be a complex Hilbert space of finite dimension dd, and let E1,…,EmE_1, \dots, E_m be operators on HH. Then there are d2d^2 operators F1,…,Fd2F_1, \dots, F_{d^2} on HH with the same operator sum: ∑j=1d2FjρFj†=∑k=1mEkρEk†for every operator ρ on H.\sum_{j=1}^{d^2} F_j \, \rho \, F_j^\dagger = \sum_{k=1}^{m} E_k \, \rho \, E_k^\dagger \qquad \text{for every operator } \rho \text{ on } H .(2)✦

Applied to the operation elements of a quantum operation, this is the theorem: the operation has an operator-sum representation with d2d^2 operation elements.✦

What Is Checked

The claim is stated over the operator sum (1) of a finite family of operators on a finite-dimensional complex Hilbert space, with no condition on the family: it need not come from a trace-preserving operation, and its length mm is arbitrary.

What the library proves about these maps is the equality (2) of two operator sums as linear maps, on all operators on HH, density operators among them.