Lean, informalized

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

Exercise 2.17 - For a normal complex matrix, equality with its adjoint and a real spectrum are one condition

Normal matrices are Hermitian exactly when their spectrum is real.

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 quantum mechanics is a Hermitian operator, and the values a measurement of it can return are its eigenvalues, which are real. The exercise turns to the wider class of normal matrices and asks to show that a normal matrix is Hermitian if and only if all of its eigenvalues are real.✦

Matrices and Their Spectrum

To state the library’s claim for square matrices with complex entries, of any size, the following notions come first. The adjoint A†A^\dagger of such a matrix AA is its conjugate transpose, the matrix with entries (A†)ij=Aji¯(A^\dagger)_{ij} = \overline{A_{ji}}. A square complex matrix AA is Hermitian when it equals its adjoint, A†=A,A^\dagger = A,(1) and normal when it commutes with its adjoint, A†A=AA†.A^\dagger A = A A^\dagger.(2)

The spectrum spec⁡(A)\operatorname{spec}(A) of a square complex matrix AA is the set of complex numbers zz for which zI−AzI - A, with II the identity matrix, has no inverse, spec⁡(A)={z∈ℂ:zI−A is not invertible}.\operatorname{spec}(A) = \{\, z \in \mathbb{C} : zI - A \text{ is not invertible} \,\}.(3)

The Claim

Theorem 1. Let AA be a normal square matrix with complex entries. Then A†=Aif and only ifIm⁡z=0for every z∈spec⁡(A).A^\dagger = A \quad \text{if and only if} \quad \operatorname{Im} z = 0 \ \text{for every } z \in \operatorname{spec}(A).(4)✦

The spectrum of a matrix is the set of its eigenvalues, so this is the exercise.

What Is Checked

For every such matrix the library proves the equivalence (4).