A Maximiser of the Quadratic Form of a Symmetric Matrix on Unit Vectors Orthogonal to Given Eigenvectors Is an Eigenvector

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 matrix-vector product, the dot product and the Euclidean norm $\lVert\cdot\rVert$ on $\mathbb{R}^{n}$, and eigenvectors of $A$. Let $k\in\mathbb{N}_{0}$ with $k<n$, and let $u:[k]\to\mathbb{R}^{n}$ be a map such that, 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$, and such that for every $i\in[k]$ there is $\mu\in\mathbb{R}$ for which $u_{i}$ is an eigenvector of $A$ with eigenvalue $\mu$. Let

$$K=\{x\in\mathbb{R}^{n}:\lVert x\rVert=1\text{ and }x\cdot u_{i}=0\text{ for every }i\in[k]\}.$$

¶ There is $v\in K$ with $x\cdot(Ax)\le v\cdot(Av)$ for every $x\in K$.

¶ If $v\in K$ and $x\cdot(Ax)\le v\cdot(Av)$ for every $x\in K$, then $v$ is an eigenvector of $A$ with eigenvalue $v\cdot(Av)$.