Lean, informalized

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

Exercise 9.15 - The fidelity of two states is the largest overlap of one fixed purification of the first with the purifications of the second

Fidelity as the largest overlap with a fixed purification.

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

Let ρ\rho and σ\sigma be two states of a quantum system, and fix one purification |ψ⟩|\psi\rangle of ρ\rho. The exercise is to show that the largest overlap |⟨ψ|φ⟩||\langle\psi|\varphi\rangle|, as |φ⟩|\varphi\rangle runs over the purifications of σ\sigma, is the fidelity F(ρ,σ)F(\rho,\sigma).✦ This is Uhlmann’s theorem with the purification of ρ\rho held fixed.

A Quantum System

A quantum system SS is a physical system whose state space 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 of the state spaces of SS and TT.✦

A state ρ\rho of SS is a positive operator of unit trace on the state space of SS.✦ A pure state |ψ⟩|\psi\rangle of SS is a unit vector in the state space of SS, with ⟨ψ|ψ⟩=1\langle\psi|\psi\rangle = 1.✦ Each pure state |ψ⟩|\psi\rangle determines the state |ψ⟩⟨ψ||\psi\rangle\langle\psi| of SS, the rank one projector onto |ψ⟩|\psi\rangle.✦ 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 their unit vectors, conjugate linear in |ψ⟩|\psi\rangle.✦

Purifications and Fidelity

The reduced state of a state ρ\rho of a composite system S⊗TS \otimes T is the state tr⁡2(ρ)\operatorname{tr}_2(\rho) of SS, the partial trace of ρ\rho over the second factor, taken against an orthonormal basis of the state space of TT.✦

A purification of a state ρ\rho of SS is a pure state |ψ⟩|\psi\rangle of S⊗SS \otimes S, the system together with a copy of itself, whose reduced state on the first factor is ρ\rho: tr⁡2|ψ⟩⟨ψ|=ρ.\operatorname{tr}_2 |\psi\rangle\langle\psi| = \rho .(1)

The fidelity of two states ρ\rho and σ\sigma of SS is the nonnegative real number F(ρ,σ)=tr⁡ρσρ,F(\rho,\sigma) = \operatorname{tr}\sqrt{\sqrt{\rho}\,\sigma\sqrt{\rho}} ,(2)✦ with the square root of a positive operator taken on its eigenvalues.

The Claim

Theorem 1. Let ρ\rho and σ\sigma be states of a quantum system SS, and let |ψ⟩|\psi\rangle be a pure state of S⊗SS \otimes S that purifies ρ\rho, as in (1). Then F(ρ,σ)=max|φ⟩|⟨ψ|φ⟩|,F(\rho,\sigma) = \max_{|\varphi\rangle} \, |\langle\psi|\varphi\rangle| ,(3)✦ where the maximum runs over the pure states |φ⟩|\varphi\rangle of S⊗SS \otimes S with tr⁡2|φ⟩⟨φ|=σ\operatorname{tr}_2 |\varphi\rangle\langle\varphi| = \sigma.

What Is Checked

The claim is stated over states of a quantum system SS, pure states of the composite system S⊗SS \otimes S with their overlap and their projectors |ψ⟩⟨ψ||\psi\rangle\langle\psi|, the partial trace tr⁡2\operatorname{tr}_2 that makes |ψ⟩|\psi\rangle and |φ⟩|\varphi\rangle purifications, and the fidelity (2).

The library proves that the projector onto a unit vector is a density operator, so that |ψ⟩⟨ψ||\psi\rangle\langle\psi| is a state, and that the partial trace of a density operator is a density operator, so that the reduced state of a state of S⊗TS \otimes T is a state of SS.