Lean, informalized

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

Theorem 8.2 - Unitary freedom in the operator-sum representation of a quantum operation

Operator-sum forms of one operation differ by a unitary.

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 Theorem

A quantum operation on a system with state space HH is usually written in operator-sum form, through a family of operators on HH, its operation elements. The family is not fixed by the operation: two different families can act in the same way on every state. Theorem 8.2 says exactly when two families of operation elements give the same quantum operation.

The Operator-sum Map

Let HH and GG be complex Hilbert spaces, and let EiE_i, for ii in a finite set II, be operators from HH to GG. The operator-sum map ℰ\mathcal{E} of the family {Ei}\{E_i\} is the map taking each operator ρ\rho on HH to the operator on GG ℰ(ρ)=∑i∈IEiρEi†.\mathcal{E}(\rho) = \sum_{i \in I} E_i \, \rho \, E_i^\dagger .(1)✦

The Claim

Theorem 1. Let HH be a finite-dimensional complex Hilbert space and let EiE_i and FiF_i, for ii in one finite set II, be operators on HH, with operator-sum maps ℰ\mathcal{E} and ℱ\mathcal{F}. Then ℰ=ℱ\mathcal{E} = \mathcal{F} if and only if there is a unitary matrix uu, with rows and columns indexed by II, such that Ei=∑j∈IuijFjfor every i∈I.E_i = \sum_{j \in I} u_{ij} F_j \qquad \text{for every } i \in I .(2)✦

What Is Checked

The claim is stated over the operator-sum maps (1) of two families of operators on HH, and two such maps are equal when they agree on every operator on HH. About each such map the library proves that it is linear in ρ\rho: it takes sums to sums and commutes with multiplication by complex numbers.