Lean, informalized

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

Exercise 9.22 - The error of a composite gate is at most the sum of its factors' errors, for a unitarily invariant distance obeying the triangle inequality

Two successive gates err by at most the sum of their errors.

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 gate UU acting on a quantum system should take a state ρ\rho to UρU†U\rho U^\dagger. An imperfect device takes it to ℰ(ρ)\mathcal{E}(\rho) instead, and the error of the device is the largest distance, over all input states, between the intended output UρU†U\rho U^\dagger and the actual output ℰ(ρ)\mathcal{E}(\rho). Run two such devices one after the other: first ℰ\mathcal{E} in place of UU, then ℱ\mathcal{F} in place of a second gate VV. The intended output is VUρU†V†VU\rho U^\dagger V^\dagger, the actual one ℱ(ℰ(ρ))\mathcal{F}(\mathcal{E}(\rho)). The exercise is to show that the error of the sequence is at most the sum of the two errors, for any distance that satisfies the triangle inequality and does not change when both of its arguments are conjugated by the same unitary.✦

A Quantum System

A quantum system SS is a physical object 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.✦

A unitary UU of SS is a closed system evolution of SS: an operator on the state space of SS with U†U=UU†=1U^\dagger U = U U^\dagger = 1.✦ The evolution of a state ρ\rho of SS under a unitary UU of SS is the state UρU†.U \rho U^\dagger .(1)✦ For two unitaries UU and VV of SS, the unitary VV after UU is the unitary VUVU of SS whose operator is the product of the operators of VV and UU, so that UU acts first.✦

The Gate Error

Let dd assign a real number d(ρ,σ)d(\rho, \sigma) to every pair of states ρ\rho, σ\sigma of SS. The gate error E(U,ℰ)E(U, \mathcal{E}) of a map ℰ\mathcal{E} from states of SS to states of SS, as an implementation of a unitary UU of SS, is the real number E(U,ℰ)=supρd(UρU†,ℰ(ρ)),E(U, \mathcal{E}) = \sup_{\rho} \, d\bigl(U \rho U^\dagger, \mathcal{E}(\rho)\bigr),(2)✦ the supremum taken over the states ρ\rho of SS.

The Claim

The triangle inequality for dd is d(ρ,τ)≤d(ρ,σ)+d(σ,τ)d(\rho, \tau) \le d(\rho, \sigma) + d(\sigma, \tau)(3) for all states ρ\rho, σ\sigma, τ\tau of SS. Invariance under unitaries is d(WρW†,WσW†)=d(ρ,σ)d(W \rho W^\dagger, W \sigma W^\dagger) = d(\rho, \sigma)(4) for every unitary WW of SS and all states ρ\rho, σ\sigma of SS.

Theorem 1. Let SS be a quantum system and let dd assign a real number to every pair of states of SS, satisfying the triangle inequality (3) and the invariance (4). Let UU and VV be unitaries of SS, and let ℰ\mathcal{E} and ℱ\mathcal{F} be maps from states of SS to states of SS such that the distances d(UρU†,ℰ(ρ))d(U \rho U^\dagger, \mathcal{E}(\rho)) and d(VσV†,ℱ(σ))d(V \sigma V^\dagger, \mathcal{F}(\sigma)) are bounded above as ρ\rho and σ\sigma range over the states of SS. Then the gate error of ℱ∘ℰ\mathcal{F} \circ \mathcal{E} as an implementation of VUVU is at most the sum of the two gate errors: E(VU,ℱ∘ℰ)≤E(U,ℰ)+E(V,ℱ).E(VU, \mathcal{F} \circ \mathcal{E}) \le E(U, \mathcal{E}) + E(V, \mathcal{F}).(5)✦

What Is Checked

The claim is stated over the states and the unitaries of a quantum system SS, the evolution (1) of a state under a unitary, the unitary VUVU that applies UU and then VV, and the gate error (2).

For these constructions the library proves that the evolution UρU†U \rho U^\dagger of a state is again a state, since conjugating a density operator by a unitary gives a density operator, and that VUVU is a unitary, as a product of unitaries.