Lean, informalized

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

Exercise 2.60 - The eigenvalues ±1\pm 1 of vˆ⋅σ→\hat v \cdot \vec{\sigma} on a qubit and the projectors onto its two eigenspaces

Eigenvalues and eigenprojectors of a Pauli observable.

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, say the spin of an electron, is measured along a direction in space given by a unit vector vˆ=(v1,v2,v3)\hat v = (v_1, v_2, v_3). The observable is vˆ⋅σ→\hat v \cdot \vec{\sigma}, the component along vˆ\hat v of the Pauli vector σ→=(X,Y,Z)\vec{\sigma} = (X, Y, Z) whose entries are the Pauli matrices of (3) below. Along zˆ\hat z it is ZZ, with eigenvalue +1+1 on |0⟩|0\rangle and −1-1 on |1⟩|1\rangle. The exercise asks for the eigenvalues of vˆ⋅σ→\hat v \cdot \vec{\sigma} in an arbitrary direction, which are again +1+1 and −1-1, and for the projectors onto the two eigenspaces, which are P±=12(I±vˆ⋅σ→)P_\pm = \tfrac12 (I \pm \hat v \cdot \vec{\sigma}), where II is the identity operator.

The library states the eigenvalues for the Pauli observable along vˆ\hat v, and the projectors for any observable AA with A2=IA^2 = I on any quantum system, both introduced below.

A Quantum System

A quantum system SS is a physical system whose state space is a finite dimensional complex Hilbert space.✦ A pure state ψ\psi of SS is a unit vector |ψ⟩|\psi\rangle in the state space of SS.✦

An observable AA on SS is a self adjoint operator on the state space of SS, A†=AA^\dagger = A.✦ A pure state ψ\psi of SS is an eigenstate of an observable AA on SS with eigenvalue μ\mu, a real number, when A|ψ⟩=μ|ψ⟩.A |\psi\rangle = \mu |\psi\rangle .(1)✦

The projectors P+P_+ and P−P_- of an observable AA on SS are the operators P+=12(I+A),P−=12(I−A)P_+ = \tfrac12 (I + A), \qquad P_- = \tfrac12 (I - A)(2) on the state space of SS.

The Pauli Observable

The qubit is the quantum system whose state space is ℂ2\mathbb{C}^2.✦ The Pauli matrices are the complex 2×22 \times 2 matrices X=(0110),Y=(0−ii0),Z=(100−1).X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}.(3) For a real vector n→=(n1,n2,n3)\vec{n} = (n_1, n_2, n_3) in three dimensions, the matrix n→⋅σ→\vec{n} \cdot \vec{\sigma} is the complex 2×22 \times 2 matrix n→⋅σ→=n1X+n2Y+n3Z.\vec{n} \cdot \vec{\sigma} = n_1 X + n_2 Y + n_3 Z .(4)✦ The Pauli observable n→⋅σ→\vec{n} \cdot \vec{\sigma} is the observable on the qubit whose operator is the matrix (4) acting on ℂ2\mathbb{C}^2.✦

The Claim

Theorem 1. Let vˆ\hat v be a unit vector in three dimensions, v12+v22+v32=1v_1^2 + v_2^2 + v_3^2 = 1. If a pure state ψ\psi of the qubit is an eigenstate of the Pauli observable vˆ⋅σ→\hat v \cdot \vec{\sigma} with eigenvalue μ\mu, then μ=1orμ=−1.\mu = 1 \quad \text{or} \quad \mu = -1 .(5)✦ There are pure states ψ+\psi_+ and ψ−\psi_- of the qubit with (vˆ⋅σ→)|ψ+⟩=|ψ+⟩,(\hat v \cdot \vec{\sigma}) \, |\psi_+\rangle = |\psi_+\rangle ,(6)✦ (vˆ⋅σ→)|ψ−⟩=−|ψ−⟩.(\hat v \cdot \vec{\sigma}) \, |\psi_-\rangle = -|\psi_-\rangle .(7)✦

Theorem 2. Let AA be an observable on a quantum system SS, with projectors P±P_\pm as in (2). If A2=IA^2 = I, then AP+=P+,A P_+ = P_+ ,(8)✦ AP−=−P−.A P_- = -P_- .(9)✦ For every vector uu in the state space of SS with Au=uA u = u, P+u=u,P_+ u = u ,(10)✦ and for every such uu with Au=−uA u = -u, P−u=u.P_- u = u .(11)✦

What Is Checked

The first theorem is stated over the Pauli observable vˆ⋅σ→\hat v \cdot \vec{\sigma} on the qubit, built from the Pauli matrices (3) as in (4), and over its eigenstates in the sense of (1); the second over an observable AA on an arbitrary quantum system and its operators P±P_\pm of (2).

The library proves that the matrix n→⋅σ→\vec{n} \cdot \vec{\sigma} is Hermitian for every real vector n→\vec{n}, so the Pauli observable is self adjoint, an observable on the qubit.