Motivation

Finding the eigenvalues of a large matrix or linear operator by computing its characteristic polynomial is numerically unworkable: the roots of a degree-$n$ polynomial are exponentially sensitive to small coefficient perturbations, and no closed-form root formula exists once $n\ge5$. The power method avoids the polynomial entirely. Introduced in essentially its modern form by Müntz (1913) and von Mises and Pollaczek-Geiringer (1929), and analyzed rigorously alongside its shifted and inverse variants throughout the mid-20th century (Wilkinson, The Algebraic Eigenvalue Problem, 1965), it remains, in the guise of one power iteration per step, the engine inside PageRank, spectral clustering, and the Lanczos/Arnoldi methods used to find eigenpairs of matrices too large to diagonalize directly.

Setting

Let $E$ be a finite-dimensional inner product space over $\mathbb{k}\in\{\mathbb{R},\mathbb{C}\}$, with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $T:E\to E$ be a self-adjoint (symmetric) linear operator: $\langle Tx,y\rangle=\langle x,Ty\rangle$ for all $x,y\in E$. The spectral theorem for finite-dimensional self-adjoint operators gives an orthonormal basis $e_0,\dots,e_{n-1}$ of $E$ ($n=\dim E$) consisting of eigenvectors of $T$, with real eigenvalues $\lambda_0,\dots,\lambda_{n-1}$ satisfying $Te_i=\lambda_ie_i$.

Call $\lambda_{i_0}$ dominant if $|\lambda_j|<|\lambda_{i_0}|$ for every $j\neq i_0$ — it is then the unique eigenvalue of largest magnitude. Given a starting vector $x_0\in E$ with coordinates $x_0=\sum_ic_ie_i$ in the eigenbasis, the power iterates are $T^kx_0$ for $k=0,1,2,\dots$, and the Rayleigh quotient of $T$ at a nonzero vector $x$ is

$$R_T(x)=\frac{\operatorname{Re}\langle x,Tx\rangle}{\|x\|^2},$$

which recovers $\lambda_i$ exactly when $x$ is the eigenvector $e_i$.

Formalization targets

Iterate expansion

$$T^kx_0=\sum_i\bigl(c_i\lambda_i^{\,k}\bigr)\,e_i$$

Rewriting the $k$-th power iterate in the eigenbasis: applying $T$ $k$ times raises each coordinate's eigenvalue factor to the $k$-th power, since $T$ acts diagonally on the eigenbasis. This is the algebraic core the rest of the argument rescales and takes limits of.

Rescaled convergence

$$\lambda_{i_0}^{-k}\,T^kx_0\;\longrightarrow\;c_{i_0}\,e_{i_0}\quad(k\to\infty)$$

Given a dominant eigenvalue $\lambda_{i_0}\neq0$ and $c_{i_0}\neq0$, dividing the expansion above by $\lambda_{i_0}^k$ leaves the $i_0$-th term fixed at $c_{i_0}e_{i_0}$ while every other term is multiplied by $(\lambda_j/\lambda_{i_0})^k\to0$, since $|\lambda_j/\lambda_{i_0}|<1$ for $j\neq i_0$. This is the precise sense in which the power iterates "align" with the dominant eigenvector.

Goal — Rayleigh quotient convergence

$$R_T\bigl(T^kx_0\bigr)\;\longrightarrow\;\lambda_{i_0}\quad(k\to\infty)$$

The practical output of the power method: the Rayleigh quotient of the (unrescaled) iterates converges to the dominant eigenvalue itself, giving a numerically computable estimator that needs no knowledge of $\lambda_{i_0}$ in advance. This is the weakest statement that captures "the power method converges to the dominant eigenvalue" without hard-coding a convergence rate, so it is the mission's goal.

Significance

The power method is the template every practical large-scale eigenvalue algorithm departs from: shifted inverse iteration, Rayleigh quotient iteration (with locally cubic convergence), the QR algorithm, and Krylov subspace methods (Lanczos, Arnoldi) all begin from the same diagonal-power argument formalized here, then add a trick — a shift, a change of subspace, an orthogonalization step — to accelerate or extend it. The result itself is classical and completely settled mathematically; there is no open question in the convergence theory of the basic power method under the dominant-eigenvalue hypothesis used here. What this mission contributes is a machine-checked version of that classical argument built directly on Mathlib's existing finite-dimensional spectral theorem (LinearMap.IsSymmetric.eigenvalues/eigenvectorBasis) — as of this writing, Mathlib's InnerProductSpace/Spectrum.lean and Rayleigh.lean files contain the spectral decomposition itself, and a Rayleigh quotient for ContinuousLinearMap, but not this convergence statement.

Difficulty

The obvious first attempt is to bound $\|T^kx_0-\lambda_{i_0}^kc_{i_0}e_{i_0}\|$ by a naive sum of norms and take limits termwise; this works for the rescaled sequence (Milestone 2) but does not by itself give the Rayleigh-quotient limit, because $R_T$ is invariant only under nonzero scalar rescaling, not under limits taken carelessly — one has to first establish that the limit vector $c_{i_0}e_{i_0}$ is nonzero (using $c_{i_0}\neq0$), then invoke continuity of $R_T$ away from $0$ to transport the Tendsto from the rescaled sequence to $R_T(T^kx_0)=R_T(\lambda_{i_0}^{-k}T^kx_0)$. Getting the degenerate case $n=1$ right is the other trap: with only one eigenvalue, the dominance hypothesis is vacuous, and if that eigenvalue is allowed to be $0$ the rescaling $\lambda_{i_0}^{-k}$ divides by zero and the rescaled-convergence statement becomes false — the formalization must therefore assume $\lambda_{i_0}\neq0$ explicitly rather than deriving it from dominance alone.

Formalization scope

The mission works with a general RCLike 𝕜 field (real or complex $E$), a LinearMap.IsSymmetric operator on a FiniteDimensional inner product space, and Mathlib's own eigenvalues/ eigenvectorBasis (which already fixes the eigenbasis and a specific, decreasing-by-value ordering of eigenvalues — the formalization does not re-derive the spectral theorem). Dominance is stated by magnitude (|\lambda_j| < |\lambda_{i_0}|), not by position in Mathlib's ordering, since the dominant eigenvalue need not be the largest by value (it could be the most negative). The starting vector $x_0$ is arbitrary subject to $c_{i_0}\neq0$; no normalization ($\|x_0\|=1$) is imposed, since the Rayleigh quotient and the rescaled limit are both scale-invariant/ scale-equivariant. A trivializing formalization is ruled out explicitly: without both $\lambda_{i_0}\neq0$ and $c_{i_0}\neq0$, the $n=1$, $T=0$ counterexample above makes the rescaled-convergence statement false, so these are load-bearing hypotheses, not decoration. Contributions on the two milestones (the algebraic iterate expansion, and the rescaled-limit argument) are especially welcome, since they are reusable building blocks for any future mission on shifted/inverse power iteration or Rayleigh quotient iteration.

Selected references

• R. von Mises and H. Pollaczek-Geiringer, Praktische Verfahren der Gleichungsauflösung, ZAMM, 1929.
• J. H. Wilkinson, The Algebraic Eigenvalue Problem, Oxford University Press, 1965.
• L. N. Trefethen and D. Bau III, Numerical Linear Algebra, SIAM, 1997 (Lecture 27: the power method).