Lean, informalized

Nielsen & Chuang · Chapter 11, Entropy and information · p. 520

Theorem 11.12 - Joint convexity of the quantum relative entropy, for two pairs of states and for finite families

Mixing pairs of states cannot raise their relative entropy.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Theorem

Take two pairs of states of one quantum system, ρ1\rho_1 with σ1\sigma_1 and ρ2\rho_2 with σ2\sigma_2, and a coin that falls heads with probability p1p_1 and tails with probability p2=1−p1p_2 = 1 - p_1. Prepare ρ1\rho_1 on heads and ρ2\rho_2 on tails, then forget the outcome: the system is in the mixture ρ\rho of ρ1\rho_1 and ρ2\rho_2 with these weights. The same coin, with σ1\sigma_1 on heads and σ2\sigma_2 on tails, prepares the mixture σ\sigma.

Theorem 11.12 of Nielsen and Chuang states that the relative entropy of ρ\rho with respect to σ\sigma is at most the average, with the coin’s probabilities, of the relative entropies of the two pairs.✦

A Quantum System

A quantum system QQ is a physical system whose state space is a finite dimensional complex Hilbert space.✦ A state ρ\rho of QQ, pure or mixed, is a positive operator of unit trace on the state space of QQ.✦

Relative Entropy

The support of a state ρ\rho of QQ is the subspace of the state space of QQ spanned by the eigenvectors of ρ\rho with nonzero eigenvalue. The relative entropy S(ρ∥σ)S(\rho\|\sigma) of a state ρ\rho of QQ with respect to a state σ\sigma of QQ whose support contains that of ρ\rho is the real number S(ρ∥σ)=tr⁡(ρlog⁡ρ)−tr⁡(ρlog⁡σ).S(\rho\|\sigma) = \operatorname{tr}(\rho\log\rho) - \operatorname{tr}(\rho\log\sigma).(1)✦

The Claim

Theorem 1. Let ρ1,ρ2,σ1,σ2\rho_1, \rho_2, \sigma_1, \sigma_2 be states of a quantum system QQ such that the support of ρ1\rho_1 lies in the support of σ1\sigma_1 and the support of ρ2\rho_2 in the support of σ2\sigma_2, and let p1,p2≥0p_1, p_2 \ge 0 with p1+p2=1p_1 + p_2 = 1. Then the states ρ=p1ρ1+p2ρ2\rho = p_1\rho_1 + p_2\rho_2 and σ=p1σ1+p2σ2\sigma = p_1\sigma_1 + p_2\sigma_2 satisfy S(ρ∥σ)≤p1S(ρ1∥σ1)+p2S(ρ2∥σ2).S(\rho\|\sigma) \le p_1 S(\rho_1\|\sigma_1) + p_2 S(\rho_2\|\sigma_2).(2)✦ More generally, let ρk\rho_k and σk\sigma_k, for k=1,…,nk = 1, \dots, n, be states of QQ such that the support of each ρk\rho_k lies in the support of σk\sigma_k, and let p1,…,pn≥0p_1, \dots, p_n \ge 0 with ∑kpk=1\sum_k p_k = 1. Then the states ρ=∑kpkρk\rho = \sum_k p_k\rho_k and σ=∑kpkσk\sigma = \sum_k p_k\sigma_k satisfy S(ρ∥σ)≤∑k=1npkS(ρk∥σk).S(\rho\|\sigma) \le \sum_{k=1}^{n} p_k\, S(\rho_k\|\sigma_k).(3)✦

What Is Checked

The claim is stated over the states of a quantum system QQ and over the relative entropy (1) of one state of QQ with respect to another.