Lean, informalized

Nielsen & Chuang · Chapter 2, Introduction to quantum mechanics · p. 103

Exercise 2.71 - The trace of the square of a state is at most one, and equals one exactly on pure states

Purity at most one, with equality exactly for pure states.

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

Exercise 2.71 asks for a test of purity that reads nothing but the density operator: for a density operator ρ\rho, show that tr(ρ2)≤1\mathrm{tr}(\rho^2) \leq 1, with equality if and only if ρ\rho is a pure state.

A Quantum System

A quantum system SS is described by its state space, a finite dimensional complex Hilbert space.✦

A state ρ\rho of SS is a positive operator of unit trace on the state space of SS: ρ≥0,trρ=1.\rho \geq 0, \qquad \mathrm{tr}\,\rho = 1.(1)✦

Pure States and Purity

A pure state |ψ⟩\lvert\psi\rangle of SS is a vector of unit norm in the state space of SS, ⟨ψ|ψ⟩=1\langle\psi\vert\psi\rangle = 1.✦ Each pure state |ψ⟩\lvert\psi\rangle of SS determines the operator |ψ⟩⟨ψ|\lvert\psi\rangle\langle\psi\rvert on the state space of SS, the rank one projector onto |ψ⟩\lvert\psi\rangle.✦ A state ρ\rho of SS is pure when it is the rank one projector onto some pure state of SS: ρ=|ψ⟩⟨ψ|for some pure state |ψ⟩ of S.\rho = \lvert\psi\rangle\langle\psi\rvert \quad \text{for some pure state } \lvert\psi\rangle \text{ of } S.(2)✦

The purity of a state ρ\rho of SS is the real number tr(ρ2)\mathrm{tr}(\rho^2).✦

The Claim

Theorem 1. Let ρ\rho be a state of a quantum system SS. Its purity is at most one, tr(ρ2)≤1,\mathrm{tr}(\rho^2) \leq 1,(3)✦ and it equals one if and only if ρ\rho is pure in the sense of (2): tr(ρ2)=1⇔ρ is pure.\mathrm{tr}(\rho^2) = 1 \quad\Longleftrightarrow\quad \rho \text{ is pure}.(4)✦

What Is Checked

The claim is stated over the states (1) of a quantum system SS, their purity tr(ρ2)\mathrm{tr}(\rho^2), and the pure states of SS, which enter through their projectors |ψ⟩⟨ψ|\lvert\psi\rangle\langle\psi\rvert as in (2).

The library proves that the projector |ψ⟩⟨ψ|\lvert\psi\rangle\langle\psi\rvert onto a unit vector is positive with unit trace, and so is a state of SS.