The Theorem

A system is prepared in one of the pure states $\lvert\psi_1\rangle, \dots, \lvert\psi_n\rangle$, in the state $\lvert\psi_i\rangle$ with probability $p_i$. It is then described by the density operator of the ensemble $\{p_i, \lvert\psi_i\rangle\}$, $$\rho = \sum_{i=1}^{n} p_i \, \lvert\psi_i\rangle\langle\psi_i\rvert .$$(1)^✦ Theorem 2.5 says which operators arise in this way: an operator $\rho$ is the density operator of some ensemble if and only if it has trace one and is positive.^✦

A Quantum System

A quantum system $S$ is described by its state space $\mathcal{H}_S$, a finite dimensional complex Hilbert space.^✦ A pure state $\lvert\psi\rangle$ of $S$ is a unit vector of $\mathcal{H}_S$, $\langle\psi\vert\psi\rangle = 1$; it determines the operator $\lvert\psi\rangle\langle\psi\rvert$ on $\mathcal{H}_S$, the rank one projector onto $\lvert\psi\rangle$. A state $\rho$ of $S$, pure or mixed, is a positive operator of unit trace on $\mathcal{H}_S$: $$\rho \geq 0, \qquad \operatorname{tr} \rho = 1 .$$(2)^✦

An ensemble $\mathcal{E} = \{p_i, \lvert\psi_i\rangle\}_{i=1}^{n}$ of pure states of $S$ is a finite family of pure states $\lvert\psi_i\rangle$ of $S$ with probabilities $p_i$ that are nonnegative and sum to one.^✦ The density operator $\rho_{\mathcal{E}}$ of an ensemble $\mathcal{E} = \{p_i, \lvert\psi_i\rangle\}_{i=1}^{n}$ of pure states of $S$ is the operator $\sum_{i=1}^{n} p_i \, \lvert\psi_i\rangle\langle\psi_i\rvert$ on $\mathcal{H}_S$.^✦

The Claim

What Is Checked

The claim is stated over the states of a quantum system $S$ with a finite dimensional state space and over the ensembles of pure states of $S$, each with its density operator (1).

The library proves that both constructions give states of $S$: the projector $\lvert\psi\rangle\langle\psi\rvert$ onto a unit vector is positive with unit trace, and so is $\rho_{\mathcal{E}}$, a sum of such projectors with nonnegative weights that sum to one.