The Theorem

A physical process takes the state $\rho$ of a system to a state of a system that may differ from the first, and it may occur only with some probability, as when one outcome of a measurement is kept. Nielsen and Chuang describe such a process by a map $\Phi$ from operators on the input state space $H$ to operators on the output state space $G$ , and lay down three axioms that make $\Phi$ a quantum operation. Theorem 8.1 identifies the maps that satisfy them: they are the operator sum representations, built from finitely many operators $E_k$ from $H$ to $G$ , the operation elements, each acting on the input state as $\rho \mapsto E_k \rho E_k^\dagger$ .

The library states this characterization twice: once for linear maps between the operators of any two finite dimensional complex Hilbert spaces, and again, once quantum systems are in hand, for maps between their state spaces.

Quantum Systems and Quantum Operations

A quantum system $S$ is a physical system whose state space $H_S$ is a finite dimensional complex Hilbert space.^✦

Let $H$ and $G$ be finite dimensional complex Hilbert spaces. A linear map $\Phi$ from operators on $H$ to operators on $G$ satisfies the axioms of a quantum operation, labeled A1, A2 and A3, when it has the following three properties.

For every density operator $\rho$ on $H$ , the trace $\mathrm{tr}\,\Phi(\rho)$ , the probability that the process occurs, lies between $0$ and $1$ .
$\Phi$ is convex linear on density operators: $\Phi\bigl(\sum_i p_i \rho_i\bigr) = \sum_i p_i \Phi(\rho_i)$ for probabilities $p_i$ .
$\Phi$ is completely positive: for every further system $R$ with state space $H_R$ , the map $\mathcal{I}_R \otimes \Phi$ , with $\mathcal{I}_R$ the identity map on operators of $H_R$ , takes positive operators on $H_R \otimes H$ to positive operators on $H_R \otimes G$ .

A quantum operation $\Phi$ from a quantum system $S$ to a quantum system $T$ is a linear map from operators on $H_S$ to operators on $H_T$ that satisfies the axioms A1 to A3.^✦

The Claim

Theorem 1. Let $H$ and $G$ be finite dimensional complex Hilbert spaces and $\Phi$ a linear map from operators on $H$ to operators on $G$ . Then $\Phi$ satisfies the axioms A1 to A3 if and only if it has an operator sum representation: there are finitely many operators $E_1, \dots, E_m$ from $H$ to $G$ with $\Phi(A) = \sum_{k=1}^{m} E_k A E_k^\dagger \quad \text{for every operator $A$ on $H$}, \qquad \sum_{k=1}^{m} E_k^\dagger E_k \le I_H .$ (1)^✦ Likewise, for quantum systems $S$ and $T$ , a linear map $\Phi$ from operators on $H_S$ to operators on $H_T$ is a quantum operation from $S$ to $T$ if and only if there are finitely many operation elements with $\Phi = \sum_{k=1}^{m} E_k \,(\cdot)\, E_k^\dagger, \qquad E_k \colon H_S \to H_T, \qquad \sum_{k=1}^{m} E_k^\dagger E_k \le I_{H_S} .$ (2)^✦

What Is Checked

The library proves both equivalences in both directions, (1) for any two such Hilbert spaces and (2) for any two quantum systems.