Lean, informalized

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

Exercise 2.74 - The partial trace of a product of two pure states over one factor is pure

The reduced state of a product state is pure.

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

Two quantum systems AA and BB are in a product state: AA is in a pure state |ψ⟩|\psi\rangle, BB in a pure state |φ⟩|\varphi\rangle, and the composite system in |ψ⟩|φ⟩|\psi\rangle|\varphi\rangle. An observer with access to AA alone describes AA by its reduced density operator, the partial trace of the joint state over BB. The exercise is to show that this reduced state is pure.

Systems and States

A quantum system AA is a physical system whose state space is a finite dimensional complex Hilbert space.✦ The composite system A⊗BA \otimes B of two quantum systems AA and BB is the quantum system whose state space is the tensor product of the state spaces of AA and BB.✦

A pure state |ψ⟩|\psi\rangle of a quantum system AA is a vector in the state space of AA of unit norm, ‖ψ‖=1.\lVert \psi \rVert = 1 .(1)✦

For pure states |ψ⟩|\psi\rangle of AA and |φ⟩|\varphi\rangle of BB, the product |ψ⟩|φ⟩=|ψ⟩⊗|φ⟩|\psi\rangle|\varphi\rangle = |\psi\rangle \otimes |\varphi\rangle is the pure state of A⊗BA \otimes B whose vector is the tensor product of the two vectors.✦ We also write it |ψφ⟩|\psi\varphi\rangle.

A state ρ\rho of a quantum system AA is a density operator on the state space of AA: a positive operator of unit trace.✦

A pure state |ψ⟩|\psi\rangle of AA determines the state |ψ⟩⟨ψ||\psi\rangle\langle\psi| of AA, the projector of rank one onto |ψ⟩|\psi\rangle, which acts on a vector |ξ⟩|\xi\rangle of the state space as |ψ⟩⟨ψ||ξ⟩=⟨ψ|ξ⟩|ψ⟩.|\psi\rangle\langle\psi| \, |\xi\rangle = \langle \psi | \xi \rangle \, |\psi\rangle .(2)✦

A state ρ\rho of AA is pure when it is the projector onto some pure state of AA, ρ=|χ⟩⟨χ|for some pure state |χ⟩ of A.\rho = |\chi\rangle\langle\chi| \quad \text{for some pure state } |\chi\rangle \text{ of } A .(3)✦

The Partial Trace

The reduced state ρA\rho^A on AA of a state ρ\rho of the composite system A⊗BA \otimes B is the state of AA obtained by tracing out BB against an orthonormal basis {|j⟩}\{|j\rangle\} of the state space of BB, ρA=Tr⁡B(ρ)=∑j(IA⊗⟨j|)ρ(IA⊗|j⟩),\rho^A = \operatorname{Tr}_B(\rho) = \sum_j \bigl( I_A \otimes \langle j | \bigr) \, \rho \, \bigl( I_A \otimes | j \rangle \bigr) ,(4)✦ where IAI_A is the identity on the state space of AA.

The Claim

Theorem 1. Let AA and BB be quantum systems, |ψ⟩|\psi\rangle a pure state of AA and |φ⟩|\varphi\rangle a pure state of BB. Then the reduced state on AA of the state |ψφ⟩⟨ψφ||\psi\varphi\rangle\langle\psi\varphi| of A⊗BA \otimes B is pure: Tr⁡B(|ψφ⟩⟨ψφ|)=|χ⟩⟨χ|for some pure state |χ⟩ of A.\operatorname{Tr}_B\bigl( |\psi\varphi\rangle\langle\psi\varphi| \bigr) = |\chi\rangle\langle\chi| \quad \text{for some pure state } |\chi\rangle \text{ of } A .(5)✦

What Is Checked

The claim is stated over the product |ψφ⟩|\psi\varphi\rangle of a pure state of AA and a pure state of BB, the state |ψφ⟩⟨ψφ||\psi\varphi\rangle\langle\psi\varphi| it determines, its partial trace (4) over BB, and purity of a state of AA in the sense of (3).

The library proves that the product of two pure states has unit norm, the norm of a product vector being the product of the norms, so that |ψφ⟩|\psi\varphi\rangle is a pure state of A⊗BA \otimes B. It proves as well that the projector onto a unit vector is a density operator, and that the partial trace of a density operator is again a density operator; |ψφ⟩⟨ψφ||\psi\varphi\rangle\langle\psi\varphi| and its reduced state on AA are therefore states.