Lean, informalized

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

Theorem 11.10 - The entropy of a mixture of states, bounded by the mean entropy and the entropy of the weights

How much entropy mixing states can add.

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 Exercise

A source prepares a quantum system in one of finitely many states ρi\rho_i, choosing the iith with probability pip_i. Whoever does not know the choice assigns the system the mixture ρ=∑ipiρi\rho = \sum_i p_i \rho_i. Its entropy is at most the average entropy of the states plus the Shannon entropy of the choice✦, and the bound is reached exactly when the states that occur have mutually orthogonal supports.✦

A Quantum System

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

The mixture ρ\rho of states ρi\rho_i of QQ, indexed by ii in a finite set, with weights pi≥0p_i \ge 0 that sum to one, is the state of QQ whose density operator is the convex combination ρ=∑ipiρi.\rho = \sum_i p_i \rho_i .(1)✦

Entropy

The Shannon entropy of a probability distribution q1,…,qnq_1, \dots, q_n is −∑kqklog⁡qk-\sum_k q_k \log q_k, with the natural logarithm, so that it is measured in nats.✦ The von Neumann entropy S(ρ)S(\rho) of a state ρ\rho of QQ is the Shannon entropy of the eigenvalues of ρ\rho: S(ρ)=−tr⁡(ρlog⁡ρ).S(\rho) = -\operatorname{tr}(\rho \log \rho).(2)✦

The Claim

The Shannon entropy H(p)H(p) of the weights p=(pi)p = (p_i) of a mixture is H(p)=−∑ipilog⁡piH(p) = -\sum_i p_i \log p_i, with the same natural logarithm.✦

Theorem 1. Let ρ\rho be the mixture (1) of finitely many states ρi\rho_i of a quantum system QQ with weights pi≥0p_i \ge 0 summing to one. Then S(ρ)≤∑ipiS(ρi)+H(p),S(\rho) \le \sum_i p_i S(\rho_i) + H(p),(3)✦ and S(ρ)=H(p)+∑ipiS(ρi)if and only ifρiρj=0 for all i≠j with pi≠0,pj≠0.S(\rho) = H(p) + \sum_i p_i S(\rho_i) \quad\text{if and only if}\quad \rho_i \rho_j = 0 \text{ for all } i \neq j \text{ with } p_i \neq 0,\ p_j \neq 0 .(4)✦

What Is Checked

The theorem is stated over the states of a quantum system QQ and their mixtures (1), and compares the von Neumann entropy (2) of a mixture with those of its components and with the Shannon entropy of the weights. About these constructions the library proves that the mixture is a state of QQ: a convex combination of density operators with nonnegative weights summing to one is again positive with unit trace.