The Exercise

Three quantum systems $A$, $B$ and $C$ are in a joint state $\rho$. Tracing out part of $\rho$ gives a reduced state, and with it an entropy, for each single system and for each pair. The exercise is weak monotonicity of the von Neumann entropy: the entropies of $A$ and of $C$ add up to no more than those of the pairs $AB$ and $BC$, which overlap in $B$.^✦

The library states this for a state of $A \otimes (B \otimes C)$, the system composed of $A$ and of the system $B \otimes C$, as defined below. The pair $BC$ is then a factor of the composite and $AB$ is not, so the reduced state of $AB$ is taken after the three systems are regrouped as $(A \otimes B) \otimes C$.

Systems and Their Composites

A quantum system $Q$ is a physical object whose state space is a finite dimensional complex Hilbert space.^✦ The composite system $Q \otimes R$ of two systems $Q$ and $R$ is the quantum system whose state space is the tensor product of the state spaces of $Q$ and $R$.^✦

An identification of systems $e$ between $Q$ and $R$ is a linear isometric bijection from the state space of $Q$ onto that of $R$.^✦ The regrouping $\alpha = \alpha_{A,B,C}$ of three systems is the identification of $A \otimes (B \otimes C)$ with $(A \otimes B) \otimes C$ that rebrackets the tensor product of vectors $u$, $v$ and $w$ in the state spaces of $A$, $B$ and $C$, $$\alpha \colon u \otimes (v \otimes w) \mapsto (u \otimes v) \otimes w .$$(1)^✦

States, Reduced States and Entropy

A state $\rho$ of $Q$ is a positive operator of unit trace on the state space of $Q$.^✦ The relabelling of a state $\rho$ of $Q$ along an identification $e$ of $Q$ with $R$ is the state $e \rho e^{-1}$ of $R$, the operator of $\rho$ conjugated by $e$.^✦

The reduced state $\rho_Q$ of a state $\rho$ of $Q \otimes R$ is the state of $Q$ obtained by tracing out $R$^✦, and the reduced state $\rho_R$ is the state of $R$ obtained by tracing out $Q$.^✦ In orthonormal bases $\{|i\rangle\}$ of the state space of $Q$ and $\{|j\rangle\}$ of that of $R$, $$\rho_Q = \operatorname{Tr}_R \rho = \sum_j (I \otimes \langle j|)\, \rho \,(I \otimes |j\rangle), \qquad \rho_R = \operatorname{Tr}_Q \rho = \sum_i (\langle i| \otimes I)\, \rho \,(|i\rangle \otimes I).$$(2)

The von Neumann entropy of a state $\rho$ of a system is the Shannon entropy, in nats, of the eigenvalues of $\rho$, $$S(\rho) = -\operatorname{tr}(\rho \log \rho).$$(3)^✦

The Claim

For a state $\rho$ of $A \otimes (B \otimes C)$, the reduced states that enter the inequality are $$\rho_A = \operatorname{Tr}_{BC}\, \rho, \qquad \rho_{BC} = \operatorname{Tr}_A\, \rho, \qquad \rho_C = \operatorname{Tr}_B\, \rho_{BC}, \qquad \rho_{AB} = \operatorname{Tr}_C \bigl(\alpha \rho \alpha^{-1}\bigr),$$(4) Their entropies are written $S(A) = S(\rho_A)$, $S(B,C) = S(\rho_{BC})$, $S(C) = S(\rho_C)$ and $S(A,B) = S(\rho_{AB})$.

What Is Checked

The claim is stated over a state of the composite of three systems, the partial traces of a state of a composite over either factor, the relabelling of a state along the regrouping (1), and the von Neumann entropy (3).

The library proves that each of these constructions yields a state: the partial trace of a density operator over either factor is a density operator, and conjugation by an isometry preserves positivity and trace, so a relabelled state is again a state.