Lean, informalized

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

Exercise 2.22 - Two eigenvectors of an observable with different eigenvalues have zero inner product

Eigenvectors of a Hermitian operator with different eigenvalues are orthogonal.

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 observable of a quantum system is a Hermitian operator AA on its state space. Take two eigenvectors of AA, |v⟩|v\rangle with eigenvalue λ\lambda and |w⟩|w\rangle with eigenvalue μ\mu, and let λ≠μ\lambda \neq \mu: two states in which the observable has definite and different values. The exercise is to show that the two vectors are orthogonal.

Hermitian Operators and Eigenvectors

The library states the claim for operators on an inner product space VV, where the inner product of |v⟩|v\rangle and |w⟩|w\rangle is written (|v⟩,|w⟩)(|v\rangle, |w\rangle).

A linear operator AA on VV is Hermitian when, for all vectors |v⟩|v\rangle and |w⟩|w\rangle in VV, (A|v⟩,|w⟩)=(|v⟩,A|w⟩).(A|v\rangle, |w\rangle) = (|v\rangle, A|w\rangle).(1)

An eigenvector of a linear operator AA on VV with eigenvalue λ\lambda is a nonzero vector |v⟩|v\rangle in VV such that A|v⟩=λ|v⟩.A|v\rangle = \lambda |v\rangle.(2)

The Claim

Theorem 1. Let AA be a Hermitian operator on an inner product space VV, and let |v⟩|v\rangle and |w⟩|w\rangle be eigenvectors of AA with eigenvalues λ\lambda and μ\mu, where λ≠μ\lambda \neq \mu. Then |v⟩|v\rangle and |w⟩|w\rangle are orthogonal: (|v⟩,|w⟩)=0.(|v\rangle, |w\rangle) = 0.(3)✦

What Is Checked

The claim is stated over a Hermitian operator on an inner product space, as defined by (1), and over two of its eigenvectors, as defined by (2), whose eigenvalues differ. What the library proves about them is the orthogonality (3).