The Spectral Theorem for Real Symmetric Matrices

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$ and $A\in\mathcal{S}(n)$, the set of symmetric matrices, with the set $\mathrm{O}(n)$ of orthogonal matrices, the transpose, the matrix product, the matrix-vector product, the diagonal matrix $\operatorname{diag}(\lambda)$ of $\lambda\in\mathbb{R}^{n}$, the standard basis vectors $e_{k}$, the dot product and the Euclidean norm $\lVert\cdot\rVert$ on $\mathbb{R}^{n}$, and eigenvectors and eigenvalues of $A$.

¶ There are $Q\in\mathrm{O}(n)$ and $\lambda\in\mathbb{R}^{n}$ such that $\lambda_{j}\ge\lambda_{k}$ for all $j,k\in[n]$ with $j\le k$, and $A=(Q\operatorname{diag}(\lambda))Q^{\top}$.

¶ If $Q\in\mathrm{O}(n)$ and $\lambda\in\mathbb{R}^{n}$ satisfy $A=(Q\operatorname{diag}(\lambda))Q^{\top}$, then for every $k\in[n]$ the vector $Qe_{k}$ is an eigenvector of $A$ with eigenvalue $\lambda_{k}$, and every eigenvalue of $A$ equals $\lambda_{k}$ for some $k\in[n]$.

¶ If $Q\in\mathrm{O}(n)$ and $\lambda\in\mathbb{R}^{n}$ satisfy $A=(Q\operatorname{diag}(\lambda))Q^{\top}$ and $\lambda_{j}\ge\lambda_{k}$ for all $j,k\in[n]$ with $j\le k$, then $\lambda_{n}\lVert x\rVert^{2}\le x\cdot(Ax)\le\lambda_{1}\lVert x\rVert^{2}$ for every $x\in\mathbb{R}^{n}$.