Lean, informalized

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

Theorem 9.4 - The fidelity of two states is the largest overlap of their purifications

Fidelity as the largest overlap of purifications.

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.

Uhlmann’s Theorem

Two states ρ\rho and σ\sigma of a quantum system, mixed in general, can be compared through pure states of a larger system. Join the system to a reference system and consider the pure states of the pair whose reduced state on the original system, the state left after discarding the reference system, is ρ\rho, and those whose reduced state is σ\sigma: these are the purifications of the two states. Uhlmann’s theorem is Theorem 9.4 of Nielsen and Chuang.

The library states it for two states of one quantum system SS, with a second copy of SS as the reference system.

A Quantum System

A quantum system SS is a physical system whose state space ℋS\mathcal{H}_S is a finite dimensional complex Hilbert space.✦ The composite system S⊗TS \otimes T of two quantum systems SS and TT is the quantum system whose state space is the tensor product ℋS⊗ℋT\mathcal{H}_S \otimes \mathcal{H}_T of theirs.✦

A state ρ\rho of SS is a positive operator of unit trace on ℋS\mathcal{H}_S, ρ≥0,tr⁡ρ=1.\rho \geq 0, \qquad \operatorname{tr}\rho = 1 .(1)✦ A pure state |ψ⟩|\psi\rangle of SS is a unit vector in ℋS\mathcal{H}_S, ⟨ψ|ψ⟩=1\langle\psi|\psi\rangle = 1.✦ Each pure state |ψ⟩|\psi\rangle of SS determines the state |ψ⟩⟨ψ||\psi\rangle\langle\psi| of SS, the projector onto |ψ⟩|\psi\rangle.✦

The partial trace tr⁡2ρ\operatorname{tr}_2\rho of a state ρ\rho of a composite system S⊗TS \otimes T is the reduced state of ρ\rho on SS, obtained by tracing out TT against an orthonormal basis {|j⟩}\{|j\rangle\} of ℋT\mathcal{H}_T, tr⁡2ρ=∑j(I⊗⟨j|)ρ(I⊗|j⟩),\operatorname{tr}_2\rho = \sum_j \bigl(I \otimes \langle j|\bigr)\,\rho\, \bigl(I \otimes |j\rangle\bigr) ,(2)✦ with II the identity on ℋS\mathcal{H}_S.

Overlap and Fidelity

The overlap of two pure states |ψ⟩|\psi\rangle and |φ⟩|\varphi\rangle of SS is the complex number ⟨ψ|φ⟩\langle\psi|\varphi\rangle, the inner product of the two unit vectors.✦

The fidelity of two states ρ\rho and σ\sigma of SS is the real number F(ρ,σ)=tr⁡ρ1/2σρ1/2,F(\rho,\sigma) = \operatorname{tr}\sqrt{\rho^{1/2}\,\sigma\,\rho^{1/2}} ,(3)✦ where ρ1/2\rho^{1/2} is the positive square root of ρ\rho and the outer root is the positive square root of the positive operator ρ1/2σρ1/2\rho^{1/2}\sigma\rho^{1/2}.

The Claim

Theorem 1. Let ρ\rho and σ\sigma be states of a quantum system SS. Then F(ρ,σ)=max|ψ⟩,|φ⟩|⟨ψ|φ⟩|,F(\rho,\sigma) = \max_{|\psi\rangle,\,|\varphi\rangle} \bigl\lvert \langle\psi|\varphi\rangle \bigr\rvert ,(4)✦ where the maximum runs over all pure states |ψ⟩|\psi\rangle and |φ⟩|\varphi\rangle of the composite system S⊗SS \otimes S with tr⁡2|ψ⟩⟨ψ|=ρ\operatorname{tr}_2|\psi\rangle\langle\psi| = \rho and tr⁡2|φ⟩⟨φ|=σ\operatorname{tr}_2|\varphi\rangle\langle\varphi| = \sigma.

What Is Checked

The claim (4) is stated over states of a quantum system SS, pure states of the composite system S⊗SS \otimes S with the states |ψ⟩⟨ψ||\psi\rangle\langle\psi| they determine, the partial trace (2) over the second factor, the overlap of two pure states and the fidelity (3).

Of these constructions the library proves that the projector |ψ⟩⟨ψ||\psi\rangle\langle\psi| onto a unit vector is a state, and that the partial trace of a state is again a state, so that tr⁡2|ψ⟩⟨ψ|\operatorname{tr}_2|\psi\rangle\langle\psi| is a state of SS.