Lean, informalized

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

Exercise 9.9 - Every channel on a finite dimensional system leaves some state unchanged

Every quantum channel fixes some state.

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 quantum channel takes each state of a system to a state of the same system. Exercise 9.9 asks to show that every channel has a fixed state, a state it leaves unchanged.

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.✦

Quantum Channels

A quantum channel ℰ\mathcal{E} on SS is a map from the states of SS to the states of SS that is the restriction to states of a linear map Φ\Phi on the operators on the state space of SS, with Φ\Phi completely positive and trace preserving: ℰ(ρ)=Φ(ρ)for every state ρ,tr⁡Φ(A)=tr⁡Afor every operator A.\mathcal{E}(\rho) = \Phi(\rho) \quad \text{for every state } \rho, \qquad \operatorname{tr} \Phi(A) = \operatorname{tr} A \quad \text{for every operator } A.(1)✦

The Claim

Theorem 1. Let SS be a quantum system that has at least one state, and let ℰ\mathcal{E} be a quantum channel on SS. Then ℰ\mathcal{E} has a fixed point: there is a state ρ\rho of SS with ℰ(ρ)=ρ.\mathcal{E}(\rho) = \rho.(2)✦

What Is Checked

The claim is stated over a quantum channel ℰ\mathcal{E} on a system SS, in the sense of (1), acting on the density operators of SS. What the library proves about these channels is the theorem of the previous section, for a state space of any finite dimension.