The Exercise

A quantum system with state space $H$ is in the state $\rho$ and undergoes an operation $\mathcal{E}$ given by operation elements $E_0, \dots, E_{n-1}$ . The same operation can be written with other operation elements. The exercise asks for a set of them, $F_0, \dots, F_{n-1}$ , in which the whole entanglement fidelity of $\rho$ under $\mathcal{E}$ comes from the first element, every other element having $\operatorname{tr}(\rho F_i) = 0$ .

Operation Elements and Entanglement Fidelity

Let $H$ be a finite-dimensional complex Hilbert space. The operation $\mathcal{E}$ with operation elements $E_0, \dots, E_{n-1}$ , operators on $H$ , is the linear map on operators $X$ on $H$ given by $\mathcal{E}(X) = \sum_i E_i X E_i^\dagger .$ (1) Two families of operators are operation elements of one operation when they give the same map (1).

The entanglement fidelity $F(\rho, E)$ of an operator $\rho$ on $H$ with respect to a finite family $E = (E_i)$ of operators on $H$ is the real number $F(\rho, E) = \sum_i \bigl|\operatorname{tr}(\rho E_i)\bigr|^2 .$ (2)^✦

The Claim

Theorem 1. Let $\rho$ be an operator on $H$ , and let $E_0, \dots, E_{n-1}$ , with $n \ge 1$ , be the operation elements of an operation $\mathcal{E}$ . Then there are operation elements $F_0, \dots, F_{n-1}$ of the same operation, $\sum_i F_i X F_i^\dagger = \mathcal{E}(X)$ for every operator $X$ on $H$ , such that $\operatorname{tr}(\rho F_i) = 0 \quad (i \neq 0), \qquad F(\rho, E) = \bigl|\operatorname{tr}(\rho F_0)\bigr|^2 .$ (3)^✦

What Is Checked

The claim is stated over the entanglement fidelity (2) of an operator $\rho$ on $H$ and a family of operators on $H$ , and over the operation (1) through which its two families are compared. What the library proves about them is the claim (3) itself.