The Exercise

A principal system $Q$ in a state $\rho$ meets an environment $E$ in a state $\sigma$. The two start uncorrelated, evolve together under a unitary $U$, and then a general measurement with measurement operators $M_m$ is performed on the pair. Seen from $Q$ alone, each outcome $m$ acts on $\rho$ as a quantum operation $\mathcal{E}_m$. The exercise is to find an operator sum representation of each $\mathcal{E}_m$ and to show that outcome $m$ occurs with probability $\mathrm{tr}[\mathcal{E}_m(\rho)]$.

The library defines $\mathcal{E}_m$ and its operation elements for an environment in an arbitrary state, and states both parts of the exercise.

A Quantum System

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ The composite system $S \otimes T$ of two quantum systems $S$ and $T$ is the system whose state space is the tensor product of their state spaces; the principal system and the environment form the composite $Q \otimes E$.^✦

A state $\rho$ of $S$ is a positive operator of unit trace on the state space of $S$, pure or mixed.^✦ The product state $\rho \otimes \sigma$ of a state $\rho$ of $S$ and a state $\sigma$ of $T$ is the state of $S \otimes T$ whose density operator is the tensor product of those of $\rho$ and $\sigma$.^✦

A unitary $U$ of $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = I$.^✦ A state $\rho$ of $S$ evolves under a unitary $U$ of $S$ to the state $U \rho U^\dagger$.^✦

Measurements

A measurement $\{M_m\}$ on $S$ with a finite set of outcomes is a family of measurement operators $M_m$ on the state space of $S$, one for each outcome $m$, satisfying the completeness relation $$\sum_m M_m^\dagger M_m = I.$$(1)^✦ The positive operator valued measure (POVM) of a measurement $\{M_m\}$ is the family of effects $M_m^\dagger M_m$, one for each outcome.^✦ The probability of outcome $m$ when $\{M_m\}$ is performed on a state $\rho$ of $S$ is the value at $m$ of the distribution its POVM assigns to $\rho$, given by the Born rule $$p(m) = \mathrm{tr}\bigl(M_m^\dagger M_m \, \rho\bigr) = \mathrm{tr}\bigl(M_m \rho M_m^\dagger\bigr).$$(2)^✦ The state left by outcome $m$ on $\rho$, before it is normalized, is the operator $M_m \rho M_m^\dagger$ on the state space of $S$.^✦

The Operation on the Principal System

Given a state $\sigma$ of $E$, a unitary $U$ of $Q \otimes E$ and a measurement $\{M_m\}$ on $Q \otimes E$, the operation $\mathcal{E}_m$ of outcome $m$ sends a state $\rho$ of $Q$ to the operator on the state space of $Q$ obtained by tracing out the environment from the state that outcome $m$ leaves, before normalization, on the evolved product state $U(\rho \otimes \sigma)U^\dagger$: $$\mathcal{E}_m(\rho) = \mathrm{tr}_E\bigl[M_m U (\rho \otimes \sigma) U^\dagger M_m^\dagger\bigr].$$(3)^✦

Given a unitary $U$ and a measurement $\{M_m\}$ on $Q \otimes E$, a finite family of vectors $|w_j\rangle$ in the state space of $E$, not necessarily normalized, and a fixed orthonormal basis $|e_k\rangle$ of that space, the operation elements of outcome $m$ are the operators $E_{jk} = \langle e_k | M_m U | w_j \rangle$ on the state space of $Q$, one for each $j$ and each $k$, acting on a vector $|\psi\rangle$ of $Q$ as $$E_{jk} |\psi\rangle = \bigl(I \otimes \langle e_k|\bigr) \, M_m U \bigl(|\psi\rangle \otimes |w_j\rangle\bigr).$$(4)^✦

The Claim

What Is Checked

The claim is stated over the measurement of the evolved product state $U(\rho \otimes \sigma)U^\dagger$ of $Q \otimes E$, with its probabilities (2), and over the operation (3) with its elements (4).

About these constructions the library proves that the tensor product of two density operators is again positive of unit trace, and that conjugating a density operator by a unitary gives a density operator; together these make $U(\rho \otimes \sigma)U^\dagger$ a state of $Q \otimes E$. It proves also that each effect $M_m^\dagger M_m$ is positive and that the effects sum to the identity by (1), so the probabilities $p(m)$ form a distribution over the outcomes.