Lean, informalized

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

Theorem 2.2 - Simultaneous diagonalization of two Hermitian operators

Hermitian operators commute exactly when they share an eigenbasis.

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 Theorem

An observable of a quantum system is a Hermitian operator on its state space. Take two observables AA and BB of the same system. The theorem says that one orthonormal basis of the state space diagonalizes both at once if and only if AA and BB commute, AB=BAAB = BA.✦

The Claim

The library states the theorem on a finite-dimensional inner product space VV over the real or the complex numbers; let dd be its dimension. An operator AA on VV is Hermitian if, writing (⋅,⋅)(\cdot,\cdot) for the inner product on VV, (A|u⟩,|v⟩)=(|u⟩,A|v⟩)(A|u\rangle, |v\rangle) = (|u\rangle, A|v\rangle)(1) for all vectors |u⟩|u\rangle and |v⟩|v\rangle in VV.

Theorem 1. Let AA and BB be Hermitian operators on VV. Then AB=BAAB = BA if and only if there are an orthonormal basis |1⟩,…,|d⟩|1\rangle, \dots, |d\rangle of VV and scalars μ1,…,μd\mu_1, \dots, \mu_d and ν1,…,νd\nu_1, \dots, \nu_d such that A|i⟩=μi|i⟩andB|i⟩=νi|i⟩,i=1,…,d.A|i\rangle = \mu_i |i\rangle \quad\text{and}\quad B|i\rangle = \nu_i |i\rangle, \qquad i = 1, \dots, d.(2)✦

What Is Checked

The claim is stated over pairs of Hermitian operators, in the sense of (1), on a finite-dimensional real or complex inner product space, and over orthonormal bases of that space with as many vectors as its dimension. The library proves the equivalence (2) for every such space and every such pair, so it holds on the state space of any finite-dimensional quantum system.