The Lemma

Take an operator $A$ on the state space $E$ of a quantum system, a finite-dimensional inner product space, and multiply it by a unitary operator $U$ on the same space. The trace $\operatorname{tr}(AU)$ is a number whose modulus changes with $U$. Lemma 9.5 bounds it: $\lvert \operatorname{tr}(AU) \rvert$ never exceeds the sum of the singular values of $A$, its trace norm, and a suitable choice of $U$ reaches that bound.

The Trace Norm

Let $E$ and $F$ be finite-dimensional inner product spaces, and let $d$ be the dimension of $E$. The singular values $s_1(T) \geq \cdots \geq s_d(T) \geq 0$ of a linear map $T$ from $E$ to $F$ are the square roots of the eigenvalues of $T^\dagger T$, and the trace norm $\|T\|_1$ of $T$ is their sum, $$\|T\|_1 = \sum_{i=1}^{d} s_i(T).$$(1)^✦ For an operator $A$ on $E$, a linear map of $E$ to itself, the trace norm $\|A\|_1$ is the sum (1) over the singular values of $A$.^✦

The Claim

What Is Checked

The claim is stated over the trace norm of an operator on $E$, the sum (1) of its singular values, and over the unitary operators on $E$ with the trace of $AU$. What the library proves about these constructions is (2).