Lean, informalized

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

Exercise 2.23 - The projector built from finitely many orthonormal vectors, and the two values its eigenvalues can take

Every eigenvalue of a projector is zero or one.

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 projector acts on the state space of a quantum system by sending each vector to its orthogonal projection onto a fixed subspace. The exercise asks to show that every eigenvalue of a projector is either 00 or 11.

The Projector

Let VV be an inner product space over the real or the complex numbers, of finite or infinite dimension. For a family of vectors |vi⟩|v_i\rangle of VV, one for each index ii of a set II, and a finite set s⊆Is \subseteq I of indices, the projector PP of the family over ss is the operator on VV given by the sum of the outer products of the vectors with index in ss, P=∑i∈s|vi⟩⟨vi|.P = \sum_{i \in s} |v_i\rangle\langle v_i| .(1)✦ The family is orthonormal when ⟨vi|vj⟩=δij\langle v_i | v_j \rangle = \delta_{ij} for all indices ii and jj.

The Claim

Theorem 1. Let |vi⟩|v_i\rangle, i∈Ii \in I, be an orthonormal family of vectors of VV, let s⊆Is \subseteq I be finite, and let PP be the projector (1) of the family over ss. If a nonzero vector |ψ⟩|\psi\rangle of VV and a scalar μ\mu satisfy P|ψ⟩=μ|ψ⟩P|\psi\rangle = \mu|\psi\rangle, then μ=0orμ=1.\mu = 0 \quad \text{or} \quad \mu = 1 .(2)✦

With the |vi⟩|v_i\rangle, i∈si \in s, an orthonormal basis of a subspace WW of VV, PP is the projector onto WW and this is the exercise.

What Is Checked

The claim is stated over the projector (1). What the library proves about this projector is the claim (2).