Lean, informalized

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

Theorem 11.7 - The sign of the relative entropy of two states, and when it is zero

The relative entropy of two states is never negative.

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

Take two states ρ\rho and σ\sigma of the same quantum system. Their relative entropy is a real number that measures how far ρ\rho lies from σ\sigma. Theorem 11.7 of the book, Klein’s inequality, gives it the first property one asks of a distance between states.

A Quantum System

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

The Relative Entropy

The relative entropy S(ρ∥σ)S(\rho\|\sigma) of a state ρ\rho to a state σ\sigma, both states of SS, is the real number S(ρ∥σ)=tr⁡(ρlog⁡ρ)−tr⁡(ρlog⁡σ).S(\rho\|\sigma) = \operatorname{tr}(\rho\log\rho) - \operatorname{tr}(\rho\log\sigma).(1)✦ The support of a state is the subspace spanned by its eigenvectors with nonzero eigenvalue.

The Claim

Theorem 1. Let ρ\rho and σ\sigma be states of a quantum system SS, and let the support of ρ\rho lie in the support of σ\sigma. Then the relative entropy of ρ\rho to σ\sigma is never negative, S(ρ∥σ)≥0,S(\rho\|\sigma) \ge 0,(2)✦ and it is zero exactly when the two states are equal, S(ρ∥σ)=0⇔ρ=σ.S(\rho\|\sigma) = 0 \iff \rho = \sigma.(3)✦

What Is Checked

The claim is stated over a quantum system SS with a finite dimensional state space, two states ρ\rho and σ\sigma of SS, and the relative entropy (1) of the first to the second.