Proof of The Spectral Theorem for Real Symmetric Matrices

Each result cited is universally quantified over the data in its own statement. We work in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices. For $x\in\mathbb{R}^{n}$ write $q(x)=x\cdot(Ax)$, a real number by The Dot Product on $\mathbb{R}^n$ §dot-product. No choice principle is used: the induction below instantiates one existential statement at each step, inside the proof of that step.

Matrix equality by columns. (C) If $M,N\in\mathcal{M}_{n}(\mathbb{R})$ and $Me_{j}=Ne_{j}$ for every $j\in[n]$, then $M=N$: for $i,j\in[n]$, $M_{ij}=(Me_{j})_{i}=(Ne_{j})_{i}=N_{ij}$ by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §column, and $M=N$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §equality.

Clause diagonalization.

The induction statement. For $k\in\mathbb{N}_{0}$, a map $u:[k]\to\mathbb{R}^{n}$ and $j\in[k]$, let

$$K_{j}(u)=\{x\in\mathbb{R}^{n}:\lVert x\rVert=1\text{ and }x\cdot u_{i}=0\text{ for every }i\in[j-1]\}.$$

For $k\in\mathbb{N}_{0}$ let $P(k)$ be the statement: there is a map $u:[k]\to\mathbb{R}^{n}$ such that (P1) for all $i,j\in[k]$, $u_{i}\cdot u_{j}=1$ if $i=j$ and $u_{i}\cdot u_{j}=0$ if $i\neq j$; (P2) for every $j\in[k]$, $u_{j}\in K_{j}(u)$ and $q(x)\le q(u_{j})$ for every $x\in K_{j}(u)$; (P3) for every $j\in[k]$, $u_{j}$ is an eigenvector of $A$ with eigenvalue $q(u_{j})$. Let $R(k)$ be the statement: if $k\le n$ then $P(k)$; and let $\{k\in\mathbb{N}_{0}:R(k)\}$ be the class of those $k$ for which it holds.

Base. $[0]$ is empty, and the empty map $u:[0]\to\mathbb{R}^{n}$ satisfies (P1), (P2) and (P3) vacuously; so $R(0)$ holds.

Step. Let $k\in\mathbb{N}_{0}$ with $R(k)$, and suppose $k+1\le n$. Then $k<n$, so $P(k)$ holds; let $u:[k]\to\mathbb{R}^{n}$ satisfy (P1), (P2) and (P3). By (P1), and by (P3) with $\mu=q(u_{i})$, the data $n$, $A$, $k$ and $u$ satisfy the hypotheses of A Maximiser of the Quadratic Form of a Symmetric Matrix on Unit Vectors Orthogonal to Given Eigenvectors Is an Eigenvector; let $K=\{x\in\mathbb{R}^{n}:\lVert x\rVert=1\text{ and }x\cdot u_{i}=0\text{ for every }i\in[k]\}$ be its set. By A Maximiser of the Quadratic Form of a Symmetric Matrix on Unit Vectors Orthogonal to Given Eigenvectors Is an Eigenvector §maximiser there is $v\in K$ with $q(x)\le q(v)$ for every $x\in K$, and by A Maximiser of the Quadratic Form of a Symmetric Matrix on Unit Vectors Orthogonal to Given Eigenvectors Is an Eigenvector §eigenvector $v$ is an eigenvector of $A$ with eigenvalue $q(v)$. Let $u':[k+1]\to\mathbb{R}^{n}$ be the map with $u'_{i}=u_{i}$ for $i\in[k]$ and $u'_{k+1}=v$, as in Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion §extension. For $j\in[k]$, $[j-1]\subseteq[k]$, so $K_{j}(u')=K_{j}(u)$; and $K_{k+1}(u')=K$. We check (P1)-(P3) for $u'$. (P1): for $i,j\in[k]$ this is (P1) for $u$. Also $v\cdot v=\lVert v\rVert^{2}=1$ by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §square, and for $i\in[k]$, $v\cdot u_{i}=0$ as $v\in K$, and $u_{i}\cdot v=0$ by The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §symmetric. (P2): for $j\in[k]$ this is (P2) for $u$, as $K_{j}(u')=K_{j}(u)$; for $j=k+1$ it is $v\in K$ and the maximising property of $v$. (P3): for $j\in[k]$ this is (P3) for $u$; for $j=k+1$ it is the eigenvector property of $v$. So $P(k+1)$ holds, and $R(k+1)$ holds.

By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, the successor of $k$ being $k+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one, $R(k)$ holds for every $k\in\mathbb{N}_{0}$; in particular $P(n)$ holds. Let $u:[n]\to\mathbb{R}^{n}$ satisfy (P1), (P2) and (P3) with $k=n$, and let $\lambda\in\mathbb{R}^{n}$ be the map $j\mapsto q(u_{j})$.

Ordering. Let $j,k\in[n]$ with $j\le k$. Then $[j-1]\subseteq[k-1]$, so $K_{k}(u)\subseteq K_{j}(u)$. By (P2) for $k$, $u_{k}\in K_{k}(u)\subseteq K_{j}(u)$, and by (P2) for $j$, $\lambda_{k}=q(u_{k})\le q(u_{j})=\lambda_{j}$. So $\lambda_{j}\ge\lambda_{k}$ for all $j,k\in[n]$ with $j\le k$.

The orthogonal matrix. By (P1), $u_{i}\cdot u_{j}=\delta_{ij}$ for all $i,j\in[n]$, with $\delta_{ij}$ the entries of $I_{n}$ as in Identity Matrix and Standard Basis Vectors §identity; so by Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion §from-columns there is $Q\in\mathrm{O}(n)$ with $Qe_{j}=u_{j}$ for every $j\in[n]$. For $j\in[n]$, by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §matrix-vector, (P3) and Real Eigenvalues and Eigenvectors of a Real Square Matrix §eigenvector,

$$(AQ)e_{j}=A(Qe_{j})=Au_{j}=\lambda_{j}u_{j},$$

and, as $\operatorname{diag}(\lambda)e_{j}=\lambda_{j}e_{j}$ by Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices §diagonal-eigenvalues and Real Eigenvalues and Eigenvectors of a Real Square Matrix §eigenvector,

$$(Q\operatorname{diag}(\lambda))e_{j}=Q(\operatorname{diag}(\lambda)e_{j})=Q(\lambda_{j}e_{j})=\lambda_{j}(Qe_{j})=\lambda_{j}u_{j}.$$

By (C), $AQ=Q\operatorname{diag}(\lambda)$. By Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion §inverse, $QQ^{\top}=I_{n}$, so by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §identity and Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §associative,

$$A=AI_{n}=A(QQ^{\top})=(AQ)Q^{\top}=(Q\operatorname{diag}(\lambda))Q^{\top}.$$

Clause eigenvectors. Let $Q\in\mathrm{O}(n)$ and $\lambda\in\mathbb{R}^{n}$ with $A=(Q\operatorname{diag}(\lambda))Q^{\top}$, and write $D=\operatorname{diag}(\lambda)$.

Let $k\in[n]$. By Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices §diagonal-eigenvalues, $e_{k}$ is an eigenvector of $\operatorname{diag}(\lambda)$ with eigenvalue $\lambda_{k}$. By Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices §similarity, applied to $Q$ and to $\operatorname{diag}(\lambda)$ in place of $A$, $Qe_{k}$ is an eigenvector of $(QD)Q^{\top}=A$ (written $QDQ^{\top}$ in that clause) with eigenvalue $\lambda_{k}$.

Let $\mu$ be an eigenvalue of $A$, and by Real Eigenvalues and Eigenvectors of a Real Square Matrix §eigenvalue let $x$ be an eigenvector of $A$ with eigenvalue $\mu$. By Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion §inverse, $Q^{\top}\in\mathrm{O}(n)$, and $(Q^{\top})^{\top}=Q$ by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §transpose. By Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices §similarity, applied to $Q^{\top}$ in place of $Q$, $Q^{\top}x$ is an eigenvector of $(Q^{\top}A)Q$ (written $Q^{\top}A(Q^{\top})^{\top}$ in that clause) with eigenvalue $\mu$. As $Q^{\top}Q=I_{n}$ by Orthogonal Real Matrices §membership, Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §associative and Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §identity give

$$(Q^{\top}A)Q=\bigl((Q^{\top}(QD))Q^{\top}\bigr)Q=\bigl(((Q^{\top}Q)D)Q^{\top}\bigr)Q=(DQ^{\top})Q=D(Q^{\top}Q)=DI_{n}=D=\operatorname{diag}(\lambda).$$

So $\mu$ is an eigenvalue of $\operatorname{diag}(\lambda)$, by Real Eigenvalues and Eigenvectors of a Real Square Matrix §eigenvalue, and $\mu=\lambda_{k}$ for some $k\in[n]$ by Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices §diagonal-eigenvalues.

Clause rayleigh. Let $Q$ and $\lambda$ be as in that clause, let $x\in\mathbb{R}^{n}$ and $y=Q^{\top}x$. For $z\in\mathbb{R}^{n}$, by The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §symmetric and Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §adjoint (with $Q$ in place of $A$),

$$x\cdot(Qz)=(Qz)\cdot x=z\cdot(Q^{\top}x)=(Q^{\top}x)\cdot z .$$

Hence, by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §matrix-vector and Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices §diagonal-algebra,

$$x\cdot(Ax)=x\cdot\bigl((Q\operatorname{diag}(\lambda))y\bigr)=x\cdot\bigl(Q(\operatorname{diag}(\lambda)y)\bigr)=y\cdot(\operatorname{diag}(\lambda)y)=\sum_{k=1}^{n}\lambda_{k}y_{k}^{2}.$$

By Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion §isometry for $Q^{\top}\in\mathrm{O}(n)$ (Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion §inverse) and by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §square, $\lVert x\rVert^{2}=\lVert y\rVert^{2}=\sum_{k=1}^{n}y_{k}^{2}$. Let $k\in[n]$. Since $1\le k\le n$, the hypothesis on $\lambda$, applied to the pairs $(1,k)$ and $(k,n)$, gives $\lambda_{n}\le\lambda_{k}\le\lambda_{1}$; and $y_{k}^{2}=y_{k}y_{k}$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product with $2=1+1$, while $0\le y_{k}y_{k}$ by Rules of Arithmetic and Order in an Ordered Field §squares, so $y_{k}^{2}\ge0$ and $\lambda_{n}y_{k}^{2}\le\lambda_{k}y_{k}^{2}\le\lambda_{1}y_{k}^{2}$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §nonnegative-scaling. By Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §comparison and Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §distributive,

$$\lambda_{n}\lVert x\rVert^{2}=\sum_{k=1}^{n}\lambda_{n}y_{k}^{2}\le\sum_{k=1}^{n}\lambda_{k}y_{k}^{2}=x\cdot(Ax)\le\sum_{k=1}^{n}\lambda_{1}y_{k}^{2}=\lambda_{1}\lVert x\rVert^{2}.$$