Lean, informalized

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

Theorem 11.9 - The entropy of a state before and after a projective measurement whose outcome is not read

A projective measurement never lowers the 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 system is prepared in a state ρ\rho and measured with a projective measurement, with projectors PiP_i for its outcomes ii. The outcome is not read. Whoever describes the system afterwards knows only the probability of each outcome, so the state they assign is the mixture of the collapsed states, each weighted by that probability: ρ′=∑iPiρPi\rho' = \sum_i P_i \rho P_i. Theorem 11.9 compares the von Neumann entropy of ρ′\rho' with that of ρ\rho and says when the two are equal.

A Quantum System

A quantum system QQ is a physical system whose state space ℋ\mathcal{H} is a finite dimensional complex Hilbert space.✦ A state ρ\rho of QQ is a density operator on ℋ\mathcal{H}, a positive operator of unit trace.✦

The von Neumann entropy of a state ρ\rho of QQ is the real number S(ρ)=−tr⁡(ρlog⁡ρ),S(\rho) = -\operatorname{tr}(\rho \log \rho),(1)✦ the Shannon entropy of the eigenvalues of ρ\rho, measured in nats.

Measurements

A measurement on QQ with a finite set of outcomes is a family of measurement operators MiM_i on ℋ\mathcal{H}, one for each outcome ii, that satisfies the completeness relation, II being the identity on ℋ\mathcal{H}: ∑iMi†Mi=I.\sum_i M_i^\dagger M_i = I.(2)✦ A measurement {Mi}\{M_i\} on QQ is projective when each of its operators is an orthogonal projector, Mi†=Mi=Mi2M_i^\dagger = M_i = M_i^2.✦ Its operators are then written PiP_i.

For a measurement {Mi}\{M_i\} on QQ and a state ρ\rho of QQ, the unread postmeasurement state is the state ρ′\rho' of QQ with density operator ρ′=∑iMiρMi†.\rho' = \sum_i M_i \rho M_i^\dagger.(3)✦ For a projective measurement this is the state ρ′\rho' of the exercise.

The Claim

Theorem 1. Let {Pi}\{P_i\} be a projective measurement on a quantum system QQ, let ρ\rho be a state of QQ, and let ρ′\rho' be its unread postmeasurement state (3). Then S(ρ)≤S(ρ′),S(\rho) \le S(\rho'),(4)✦ and S(ρ′)=S(ρ)if and only ifρ′=ρ.S(\rho') = S(\rho) \quad \text{if and only if} \quad \rho' = \rho.(5)✦

What Is Checked

The claim is stated for every projective measurement on a quantum system QQ with a finite set of outcomes and every state ρ\rho of QQ, in terms of the unread postmeasurement state (3) and the von Neumann entropy (1).

About these constructions the library proves that ρ′\rho' is again a state of QQ: the operator ∑iMiρMi†\sum_i M_i \rho M_i^\dagger is positive, and its trace is one by the completeness relation (2).