Lean, informalized

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

Exercise 2.67 - A linear operator on a subspace that keeps inner products is the restriction of a unitary on the whole space

An operator preserving inner products extends to a unitary.

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

An operation on a quantum system is often given only on some of its states: on a few basis states, or on the states in which an auxiliary system starts out in |0⟩|0\rangle. Let VV be the state space of the system, a Hilbert space, and WW a subspace of VV. Let UU be a linear operator that takes each vector |w⟩|w\rangle of WW to a vector U|w⟩U|w\rangle of VV and preserves inner products: (U|w1⟩,U|w2⟩)=⟨w1|w2⟩for all |w1⟩,|w2⟩∈W.\bigl(U|w_1\rangle, U|w_2\rangle\bigr) = \langle w_1|w_2\rangle \qquad \text{for all } |w_1\rangle, |w_2\rangle \in W .(1) The exercise is to extend UU to a unitary operator on the whole of VV.

Unitary Operators

A unitary operator U′U' on VV is a linear map of VV onto itself that preserves all inner products: (U′|v1⟩,U′|v2⟩)=⟨v1|v2⟩for all |v1⟩,|v2⟩∈V.\bigl(U'|v_1\rangle, U'|v_2\rangle\bigr) = \langle v_1|v_2\rangle \qquad \text{for all } |v_1\rangle, |v_2\rangle \in V .(2)

The Claim

Theorem 1. Let WW be a subspace of a Hilbert space VV, and let UU be a linear operator from WW into VV that preserves inner products as in (1). Then there is a unitary operator U′U' on VV that agrees with UU on WW: U′|w⟩=U|w⟩for every |w⟩∈W.U'|w\rangle = U|w\rangle \qquad \text{for every } |w\rangle \in W .(3)✦

What Is Checked

The claim is stated over a linear operator UU from a subspace WW of VV into VV that preserves inner products, (1), and over the unitary operators on VV of (2). What the library proves about them is the existence of the extension (3).