DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-01

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The MINRES iterate from the Lanczos tridiagonal least-squares problem

Definition

Let $A$ be Hermitian, let $x_{0}$ be an initial guess for $A x = b$ , let $r_{0} = b - A x_{0}$ , and put $β = ∥ r_{0} ∥_{2}$ . Assume Lanczos runs through step $m$ without breakdown and yields

$A Q_{m} = Q_{m + 1} {\overset{ˉ}{T}}_{m}, r_{0} = β q_{1} = β Q_{m + 1} e_{1},$

with ${\overset{ˉ}{T}}_{m}$ tridiagonal in the sense of With a Hermitian matrix, Arnoldi collapses to the Lanczos three-term recurrence and a real symmetric tridiagonal projection. A vector

$x_{m} : = x_{0} + Q_{m} y_{m}$

is an $m$ th MINRES iterate when $y_{m}$ minimizes

$∥ β e_{1} - {\overset{ˉ}{T}}_{m} y ∥_{2}$

over all $y \in C^{m}$ . Such a minimizer exists by For a linear map $T : V \to W$ between finite-dimensional inner-product spaces, $x$ minimises $∥ T x - b ∥$ if and only if $T^{*} (T x - b) = 0$ , equivalently $T^{*} T x = T^{*} b$ ; minimisers exist and any two differ by an element of $\ker T$ .

Depends on

Used by

For Hermitian A, including the indefinite case, MINRES minimizes the Euclidean residual over x₀+Kₘ(A,r₀) Theorem

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard Barrett et al., Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods (standard reference, not scraped)