Lean, informalized

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

Theorem 2.1 - When an operator on a finite-dimensional complex inner product space has an orthonormal eigenbasis

Normal operators are those diagonal in an orthonormal basis.

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

The state space of a quantum system is a complex inner product space VV of finite dimension dd, and an operator on it is written as a d×dd \times d matrix once a basis is chosen. Theorem 2.1, the spectral decomposition, says which linear operators MM on VV have a diagonal matrix in some orthonormal basis of VV.

Normal Operators

A linear operator MM on VV is normal if it commutes with its adjoint M†M^\dagger: MM†=M†M.M M^\dagger = M^\dagger M.(1)

The Claim

Theorem 1. Let MM be a linear operator on VV. Then MM is normal if and only if there are an orthonormal basis |e1⟩,…,|ed⟩|e_1\rangle, \dots, |e_d\rangle of VV and complex numbers λ1,…,λd\lambda_1, \dots, \lambda_d with M|ei⟩=λi|ei⟩,i=1,…,d.M|e_i\rangle = \lambda_i |e_i\rangle, \qquad i = 1, \dots, d.(2)✦

In such a basis MM has the matrix diag(λ1,…,λd)\mathrm{diag}(\lambda_1, \dots, \lambda_d), the form the exercise asks about.

What Is Checked

The claim is stated over a linear operator MM on a complex inner product space of finite dimension, with normality as in (1) and with an orthonormal basis and complex eigenvalues as in (2). The library proves the equivalence in both directions, for every such operator on every such space.