Lean, informalized

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

Problem 11.1 - A trace inequality for convex functions of Hermitian operators, and the nonnegativity of relative entropy

A convex trace inequality and the sign of 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 Exercise

A real function ff, convex on an interval and differentiable at a point bb of it, lies above its tangent line at bb: f(a)−f(b)≥(a−b)f′(b)f(a) - f(b) \ge (a - b)\,f'(b) for every aa in the interval. The exercise asks for the same inequality with two Hermitian operators AA and BB in place of the numbers and a trace on each side, the generalized Klein inequality. It then turns to states, and asks to show that the relative entropy S(ρ∥σ)S(\rho\|\sigma), a measure of how distinguishable the state ρ\rho is from the state σ\sigma, is never negative, which is Klein’s inequality.

A Quantum System

The library states both inequalities for operators on the state space EE of a quantum system, a finite-dimensional complex Hilbert space.

A density operator ρ\rho on EE is a positive operator on EE of unit trace: ρ≥0,tr⁡ρ=1.\rho \ge 0, \qquad \operatorname{tr} \rho = 1.(1)✦

For a Hermitian operator A=∑aaPaA = \sum_a a\,P_a on EE, written by its eigenvalues aa and the projectors PaP_a onto their eigenspaces, and a real function ff defined at those eigenvalues, f(A)f(A) is the operator that applies ff to each eigenvalue and keeps the projectors: f(A)=∑af(a)Pa.f(A) = \sum_a f(a)\, P_a.(2)

The Claim

Theorem 1. Let AA and BB be Hermitian operators on EE, and let ff be a real function, convex on an interval that contains the eigenvalues of AA and of BB, and differentiable at each eigenvalue bb of BB with derivative f′(b)f'(b). Then tr⁡f(A)−tr⁡f(B)≥tr⁡((A−B)f′(B)).\operatorname{tr} f(A) - \operatorname{tr} f(B) \ge \operatorname{tr}\big((A - B)\, f'(B)\big).(3)✦

Theorem 2. Let ρ\rho and σ\sigma be density operators on EE, with every eigenvalue of σ\sigma strictly positive. Then the relative entropy of ρ\rho to σ\sigma is nonnegative: S(ρ∥σ)≥0.S(\rho\|\sigma) \ge 0.(4)✦

What Is Checked

The first claim is stated over two Hermitian operators on EE and a convex real function, the second over two density operators on EE in the sense of (1). The library also proves that every density operator is Hermitian, so the first claim, stated for Hermitian operators, applies to the density operators ρ\rho and σ\sigma of the second.