The power method converges

The rayleighQuotient definition takes a field $\mathbb{k}$ (either $\mathbb{R}$ or $\mathbb{C}$, via the RCLike typeclass), a finite- or infinite-dimensional inner product space $E$ over $\mathbb{k}$, a $\mathbb{k}$-linear map $T : E \to E$, and a vector $x \in E$, and it defines the real number $R_T(x) := \dfrac{\operatorname{Re}\langle x, Tx\rangle}{\|x\|^2}$, where $\langle \cdot,\cdot\rangle$ is the inner product and $\|x\|$ is the norm induced by that inner product; this expression is defined for every $x$, including $x = 0$, at which point $\|x\|^2 = 0$ and the quotient is a division by zero (which in Lean evaluates to $0$ under the junk-value convention). The theorem rayleighQuotient_iterate_tendsto fixes a field $\mathbb{k}$ and a finite-dimensional inner product space $E$ over $\mathbb{k}$ (dimension $n := \dim_{\mathbb{k}} E$), and a self-adjoint linear map $T : E \to E$; it names the associated $n$ real eigenvalues $\lambda_0,\dots,\lambda_{n-1}$ and an orthonormal eigenbasis $(e_i)_{i<n}$ with $T e_i = \lambda_i e_i$. It further takes an arbitrary vector $x_0 \in E$ and a distinguished index $i_0$ (forcing $n \ge 1$), subject to three hypotheses: (i) strict dominance $|\lambda_j| < |\lambda_{i_0}|$ for every $j \ne i_0$; (ii) $\lambda_{i_0} \ne 0$; and (iii) writing $x_0 = \sum_i c_i e_i$, that $c_{i_0} \ne 0$. Under these hypotheses, the conclusion, with rayleighQuotient unfolded, asserts that the sequence $k \mapsto \dfrac{\operatorname{Re}\langle T^k x_0,\, T(T^k x_0)\rangle}{\|T^k x_0\|^2}$ converges, as $k \to \infty$, to $\lambda_{i_0}$, with no claim about the rate of convergence and no explicit hypothesis ruling out $T^k x_0 = 0$ for some $k$ (in which case that term of the sequence is $0$ by the junk-value convention). The proof term is sorry, so this theorem is not proved as given.