Lean, informalized

Nielsen & Chuang · Chapter 9, Distance measures for quantum information · p. 405

Exercise 9.7 - The difference of two density operators split into positive parts with orthogonal supports

Two states differ by orthogonal positive operators.

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 system. The exercise asks for ρ−σ\rho - \sigma to be written as Q−RQ - R, with QQ and RR positive operators supported on orthogonal subspaces of the state space.✦

The spectral decomposition of ρ−σ\rho - \sigma gives such a pair: QQ keeps the positive eigenvalues with their eigenvectors, and RR keeps the negative ones with their sign reversed.

A Quantum System

A quantum system SS is a physical system 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: ρ≥0,tr⁡ρ=1.\rho \geq 0, \qquad \operatorname{tr} \rho = 1 .(1)✦

The Claim

Theorem 1. Let ρ\rho and σ\sigma be states of a quantum system SS. Then there are positive operators QQ and RR on the state space of SS, with orthogonal ranges, such that ρ−σ=Q−R,QR=0.\rho - \sigma = Q - R, \qquad QR = 0 .(2)✦

The support of a positive operator is its range, the orthogonal complement of its kernel, so the orthogonal ranges of QQ and RR are the orthogonal supports of the exercise.

What Is Checked