Lean, informalized

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

Theorem 2.6 - Two ensembles of equal size give one density operator exactly when a unitary matrix relates them

Ensembles of the same state differ by a unitary.

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 Theorem

A system prepared in the pure state |ψi⟩|\psi_i\rangle with probability pip_i, an ensemble {pi,|ψi⟩}\{p_i, |\psi_i\rangle\} of pure states, is described by a single density operator, and different ensembles can give the same one.

Theorem 2.6 says exactly when two ensembles of pure states give the same density operator. The library states it for two ensembles with the same number of states.

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, pure and mixed states alike.✦

A pure state |ψ⟩|\psi\rangle of SS is a vector of unit norm in the state space of SS, fixed physically up to a global phase.✦ It gives the state |ψ⟩⟨ψ||\psi\rangle\langle\psi| of SS, the rank one projector onto |ψ⟩|\psi\rangle.✦

Ensembles

An ensemble of pure states {pi,|ψi⟩}\{p_i, |\psi_i\rangle\} of SS consists of nn pure states |ψi⟩|\psi_i\rangle of SS and weights pip_i, labelled by i=1,…,ni = 1, \dots, n, that form a probability distribution: every pip_i is nonnegative and ∑ipi=1\sum_i p_i = 1.✦

The density operator of an ensemble {pi,|ψi⟩}\{p_i, |\psi_i\rangle\} of SS is the state ρ=∑ipi|ψi⟩⟨ψi|\rho = \sum_i p_i\,|\psi_i\rangle\langle\psi_i|(1)✦ of SS. The subnormalized vectors of an ensemble {pi,|ψi⟩}\{p_i, |\psi_i\rangle\} of SS are the vectors |ψ̃i⟩=pi|ψi⟩|\tilde\psi_i\rangle = \sqrt{p_i}\,|\psi_i\rangle(2)✦ in the state space of SS, one for each label ii.

Two ensembles {pi,|ψi⟩}\{p_i, |\psi_i\rangle\} and {qj,|φj⟩}\{q_j, |\varphi_j\rangle\} of SS are unitarily related when they have the same number nn of states and there is a unitary n×nn \times n matrix uu of complex numbers that carries the subnormalized vectors |φ̃j⟩=qj|φj⟩|\tilde\varphi_j\rangle = \sqrt{q_j}\,|\varphi_j\rangle of the second into those of the first: |ψ̃i⟩=∑juij|φ̃j⟩for every i.|\tilde\psi_i\rangle = \sum_j u_{ij}\,|\tilde\varphi_j\rangle \quad\text{for every } i.(3)✦

The Claim

Theorem 1. Let {pi,|ψi⟩}\{p_i, |\psi_i\rangle\} and {qj,|φj⟩}\{q_j, |\varphi_j\rangle\} be ensembles of pure states of a quantum system SS with the same number of states. They have the same density operator, ∑ipi|ψi⟩⟨ψi|=∑jqj|φj⟩⟨φj|,\sum_i p_i\,|\psi_i\rangle\langle\psi_i| = \sum_j q_j\,|\varphi_j\rangle\langle\varphi_j|,(4)✦ if and only if they are unitarily related.

What Is Checked

The claim is stated over two ensembles of pure states of a quantum system: it compares their density operators (1) and asks for a unitary relation (3) between their subnormalized vectors (2).

The library proves that the density operator of an ensemble is a state of SS: it is positive, and its trace is one, since each projector |ψi⟩⟨ψi||\psi_i\rangle\langle\psi_i| has unit trace and the probabilities sum to one. It proves as well that the projector |ψ⟩⟨ψ||\psi\rangle\langle\psi| onto a unit vector is a density operator.