Lean, informalized

Nielsen & Chuang · Chapter 10, Quantum error-correction · p. 443

Exercise 10.13 - How far amplitude damping can move a pure state of a qubit, measured by fidelity

Least fidelity of a pure state under amplitude damping.

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 qubit that loses energy to its environment undergoes amplitude damping, a channel ℰ\mathcal{E} fixed by a single parameter γ\gamma. A pure state |ψ⟩|\psi\rangle is sent through the channel, and the fidelity FF between what goes in and what comes out measures how much the channel has disturbed it. The exercise asks for the smallest value of this fidelity over all pure states of the qubit.

A Quantum System

A quantum system SS is a physical system whose state space is a finite dimensional complex Hilbert space.✦ The qubit is the two level system whose state space is ℂ2\mathbb{C}^2, with the ground state |0⟩|0\rangle and the excited state |1⟩|1\rangle as its standard basis.✦

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.✦ Each pure state |ψ⟩|\psi\rangle of SS determines the state |ψ⟩⟨ψ||\psi\rangle\langle\psi| of SS, the projector onto |ψ⟩|\psi\rangle.✦

The fidelity of two states ρ\rho and σ\sigma of a system SS is the nonnegative real number F(ρ,σ)=tr⁡ρσρ,F(\rho, \sigma) = \operatorname{tr} \sqrt{\sqrt{\rho}\, \sigma \sqrt{\rho}} ,(1)✦ where the square root of a positive operator is the positive operator obtained by taking the square root of each of its eigenvalues.

The Amplitude Damping Channel

For a parameter γ\gamma with 0≤γ≤10 \le \gamma \le 1, the operation elements of amplitude damping are the operators E0E_0 and E1E_1 on the state space of the qubit whose matrices in the basis |0⟩|0\rangle, |1⟩|1\rangle are E0=(1001−γ),E1=(0γ00).E_0 = \begin{pmatrix} 1 & 0 \\ 0 & \sqrt{1-\gamma} \end{pmatrix} , \qquad E_1 = \begin{pmatrix} 0 & \sqrt{\gamma} \\ 0 & 0 \end{pmatrix} .(2)✦

The amplitude damping channel ℰ\mathcal{E} with parameter γ\gamma is the map on states of the qubit given by ℰ(ρ)=E0ρE0†+E1ρE1†.\mathcal{E}(\rho) = E_0 \rho E_0^\dagger + E_1 \rho E_1^\dagger .(3)✦

It leaves the ground state alone, ℰ(|0⟩⟨0|)=|0⟩⟨0|\mathcal{E}(|0\rangle\langle 0|) = |0\rangle\langle 0|, and acts on the excited state as ℰ(|1⟩⟨1|)=(1−γ)|1⟩⟨1|+γ|0⟩⟨0|.\mathcal{E}(|1\rangle\langle 1|) = (1-\gamma)\, |1\rangle\langle 1| + \gamma\, |0\rangle\langle 0| .(4)

The Claim

Theorem 1. Let 0≤γ≤10 \le \gamma \le 1, and let ℰ\mathcal{E} be the amplitude damping channel with parameter γ\gamma. Then the least fidelity between a pure state |ψ⟩|\psi\rangle of the qubit and its image under ℰ\mathcal{E} is min|ψ⟩F(|ψ⟩⟨ψ|,ℰ(|ψ⟩⟨ψ|))=1−γ.\min_{|\psi\rangle} F\bigl(|\psi\rangle\langle\psi| ,\, \mathcal{E}(|\psi\rangle\langle\psi|)\bigr) = \sqrt{1-\gamma} .(5)✦

What Is Checked

The claim is stated over the qubit and its pure states, the state |ψ⟩⟨ψ||\psi\rangle\langle\psi| that each of them determines, the amplitude damping channel (3) built from the elements (2), and the fidelity (1) of two states.

The library proves that the projector onto a unit vector is a density operator, so that |ψ⟩⟨ψ||\psi\rangle\langle\psi| is a state. It proves that for 0≤γ≤10 \le \gamma \le 1 the elements satisfy the completeness relation E0†E0+E1†E1=IE_0^\dagger E_0 + E_1^\dagger E_1 = I, and that the channel therefore takes every state of the qubit to a state.