The Theorem

Theorem 11.11 is Lieb’s theorem, a statement about positive operators and their powers. Take positive operators $A$ and $B$ , an operator $K$ that carries the space on which $B$ acts into the space on which $A$ acts, with adjoint $K^\dagger$ carrying the space of $A$ back to that of $B$ , and an exponent $t$ between $0$ and $1$ , and form the trace of $K^\dagger A^t K B^{1-t}$ , where $A^t$ and $B^{1-t}$ are the powers of $A$ and $B$ to the exponents $t$ and $1-t$ . Mix two such pairs as one mixes two density operators into an ensemble: with probabilities $a$ and $b$ , the pairs $(A_1, B_1)$ and $(A_2, B_2)$ give the pair $(aA_1 + bA_2,\ aB_1 + bB_2)$ . The theorem compares the trace for the mixed pair with the average, under the same probabilities, of the traces for the two pairs.

The library takes $A$ acting on a complex Hilbert space $E$ and $B$ on $\mathbb{C}^n$ .

Positive Operators and Their Powers

An operator $A$ on $E$ is positive, written $A \ge 0$ , if $\langle\psi|A|\psi\rangle$ is real and nonnegative for every vector $|\psi\rangle$ in $E$ . The positive operators on $E$ form the set $\mathcal{P}(E)$ , and those on $\mathbb{C}^n$ the set $\mathcal{P}(\mathbb{C}^n)$ .

The power $A^s$ of a positive operator $A$ , for a real exponent $s \ge 0$ , is the operator with the same eigenvectors as $A$ and each eigenvalue $\lambda$ replaced by $\lambda^s$ : where $A = \sum_i \lambda_i |i\rangle\langle i|$ , $A^s = \sum_i \lambda_i^s\, |i\rangle\langle i| .$ (1)

The function $f_t$ the theorem is about takes a pair $(A, B)$ in $\mathcal{P}(E) \times \mathcal{P}(\mathbb{C}^n)$ to the real part of the trace of the operator $K^\dagger A^t K B^{1-t}$ on $\mathbb{C}^n$ : $f_t(A, B) = \operatorname{Re} \operatorname{tr}\bigl(K^\dagger A^t K B^{1-t}\bigr).$ (2)

The Claim

Theorem 1. Let $K$ be an operator from $\mathbb{C}^n$ to a complex Hilbert space $E$ , and let $0 \le t \le 1$ . Then $f_t$ is jointly concave on the convex set of pairs of positive operators, so that for $A_1, A_2$ in $\mathcal{P}(E)$ , $B_1, B_2$ in $\mathcal{P}(\mathbb{C}^n)$ and weights $a, b \ge 0$ with $a + b = 1$ , $a\, f_t(A_1, B_1) + b\, f_t(A_2, B_2) \le f_t(aA_1 + bA_2,\ aB_1 + bB_2).$ (3)^✦ $f_t\bigl(a(A_1, B_1) + b(A_2, B_2)\bigr) \ge a\, f_t(A_1, B_1) + b\, f_t(A_2, B_2).$ (4)^✦

What Is Checked

The claim is stated over the positive operators on $E$ and on $\mathbb{C}^n$ , their powers (1), and the trace on $\mathbb{C}^n$ through which $f_t$ is defined in (2).

Besides the inequalities (3) and (4), the library proves that the pairs of positive operators form a convex set, the domain on which $f_t$ is concave.