TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Flexible GMRES minimizes over the actual preconditioned-vector span

Statement

Let $A \in M_{n} (C)$ and $b, x_{0} \in C^{n}$ , with the standard Hermitian inner product and induced Euclidean norm. Suppose the algorithm Flexible GMRES with variable right preconditioning completes $m \geq 1$ steps without breakdown, producing $Z_{m} = [z_{1}, \dots, z_{m}]$ and ${\overset{ˉ}{H}}_{m}$ . Define $β = ∥ b - A x_{0} ∥_{2}$ , let $e_{0} \in C^{m + 1}$ be the standard unit vector at coordinate $0$ , and define $V_{m + 1} \in M_{n \times (m + 1)} (C)$ by $(V_{m + 1})_{a, i - 1} = (v_{i})_{a}$ for $0 \leq a < n$ , $1 \leq i \leq m + 1$ . The one-based column label $i$ therefore occupies zero-based matrix column $i - 1$ . The matrices $Z_{m}$ and ${\overset{ˉ}{H}}_{m}$ use the algorithm's one-based-to-zero-based slot mapping. Then $A Z_{m} = V_{m + 1} {\overset{ˉ}{H}}_{m},$ and every $y \in C^{m}$ satisfies $b - A (x_{0} + Z_{m} y) = V_{m + 1} (β e_{0} - {\overset{ˉ}{H}}_{m} y), ∥ b - A (x_{0} + Z_{m} y) ∥_{2} = ∥ β e_{0} - {\overset{ˉ}{H}}_{m} y ∥_{2} .$ Consequently every least-squares minimizer $y_{m}$ in the algorithm produces a true-residual minimizer $x_{m} = x_{0} + Z_{m} y_{m}$ over $x_{0} + span {z_{1}, \dots, z_{m}} .$ Moreover, ${\overset{ˉ}{H}}_{m}$ has full column rank, so its least-squares minimizer is unique. The result makes no fixed-preconditioner spectral or convergence claim.

Facts & Assumptions

Given: A system $A x = b$ , an initial vector $x_{0}$ , and a completed $m$ -step run of the variable-right-preconditioned flexible GMRES algorithm with no breakdown.

[F1]

Flexible GMRES with variable right preconditioning: the initialization sets $r_{0} = b - A x_{0}$ , $β = ∥ r_{0} ∥_{2}$ , and, when $β \neq 0$ , $v_{1} = r_{0} / β$ .

[F2]

Flexible GMRES with variable right preconditioning: each column starts with $w = A z_{j}$ ; the ordered updates use $h_{i j} = ⟨ w, v_{i} ⟩$ and $w : = w - h_{i j} v_{i}$ ; after them $h_{j + 1, j} = ∥ w ∥_{2}$ , and a positive value normalizes $v_{j + 1} = w / h_{j + 1, j}$ .

[F3]

Flexible GMRES with variable right preconditioning: in zero-based matrix coordinates, column $k - 1$ of $Z_{j}$ is $z_{k}$ , and $({\overset{ˉ}{H}}_{j})_{i - 1, k - 1} = h_{i k}$ for $1 \leq k \leq j$ , $1 \leq i \leq k + 1$ ; $({\overset{ˉ}{H}}_{j})_{a, b} = 0$ when $a > b + 1$ , and the algorithm minimizes $∥ β e_{0} - {\overset{ˉ}{H}}_{j} y ∥_{2}$ .

[F4]

The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products: on each $C^{q}$ , $⟨ z, w ⟩ = \sum_{k < q} z_{k} \overline{w_{k}}$ is an inner product, linear in its first argument.

[F5]

The norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ induced by a real or complex inner product: the induced norm is $∥ v ∥_{2} = \sqrt{⟨ v, v ⟩}$ .

[F6]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: matrix multiplication is defined by the finite coordinate sums, so its columns act linearly on vectors.

[F7]

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$ : a linear map between finite-dimensional inner-product spaces has a least-squares minimizer, and any two minimizers differ by an element of the map's kernel.

[F8]

Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ : $span (S)$ is the smallest linear subspace containing $S$ .

[F9]

$span (S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $span (\emptyset) = {0_{V}}$ : a vector belongs to $span (S)$ exactly when it is a finite linear combination of elements of $S$ .

[F10]

$C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ : $C$ is a field, so the finite coordinate spaces and matrices in the statement are over a field.

[F11]

The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ : for every $q \in N$ , $C^{q}$ has the standard basis indexed by $i < q$ and is finite-dimensional; when $q \geq 1$ , its standard unit vector at coordinate $0$ has value $1$ there and $0$ elsewhere.

Proof

1.1givenF1F2F4F5algebrainduction

Since this run reaches the first step, [F1] gives $r_{0} \neq 0$ and $β = \sqrt{⟨ r_{0}, r_{0} ⟩} > 0$ . Since $β$ is real, $⟨ r_{0} / β, r_{0} / β ⟩ = β^{- 2} ⟨ r_{0}, r_{0} ⟩ = 1$ , so $v_{1}$ has norm $1$ . Inductively suppose $v_{1}, \dots, v_{j}$ are orthonormal. At the $i$ th Gram–Schmidt substep, the current vector $w$ is orthogonal to $v_{k}$ for $k < i$ . The update $w^{'} : = w - h_{i j} v_{i}$ , with $h_{i j} = ⟨ w, v_{i} ⟩$ , satisfies $⟨ w^{'}, v_{i} ⟩ = h_{i j} - h_{i j} ⟨ v_{i}, v_{i} ⟩ = 0$ and $⟨ w^{'}, v_{k} ⟩ = ⟨ w, v_{k} ⟩ - h_{i j} ⟨ v_{i}, v_{k} ⟩ = 0$ for each $k < i$ . These equalities use linearity in the first argument and orthonormality [F4]. After all $i = 1, \dots, j$ , the final $w$ is orthogonal to every current basis vector. Nonbreakdown gives $h_{j + 1, j} = ∥ w ∥_{2} > 0$ ; the same inner-product calculation gives $⟨ v_{j + 1}, v_{j + 1} ⟩ = h_{j + 1, j}^{- 2} ⟨ w, w ⟩ = 1$ , and its orthogonality follows from that of $w$ . Induction proves orthonormality through $v_{m + 1}$ .

1.2givenF2F3F6F7F10F11algebra

The finite matrix ${\overset{ˉ}{H}}_{m}$ defines a linear map $C^{m} \to C^{m + 1}$ between finite-dimensional inner-product spaces by [F6], [F10], and [F11]. By [F7], least-squares minimizers exist and any two differ by an element of $\ker {\overset{ˉ}{H}}_{m}$ . This kernel is zero: if ${\overset{ˉ}{H}}_{m} y = 0$ , its zero-based last row $a = m$ gives $h_{m + 1, m} y_{m - 1} = 0$ , hence $y_{m - 1} = 0$ . For each one-based row label $r = m, m - 1, \dots, 2$ in descending order, matrix row $r - 1$ has coefficient $h_{r, r - 1}$ in column $r - 2$ ; its other possibly nonzero terms use coordinates $y_{k - 1}$ with $k \geq r$ , already shown zero. Thus $h_{r, r - 1} y_{r - 2} = 0$ . Since $h_{r, r - 1} = h_{(r - 1) + 1, r - 1} > 0$ by no breakdown, we obtain $y_{r - 2} = 0$ . Thus every zero-based coordinate vanishes, ${\overset{ˉ}{H}}_{m}$ is injective, and its least-squares minimizer is unique.

1.3F2F3F6F10algebra

At the end of column $j$ , the successive subtractions give $A z_{j} = \sum_{i = 1}^{j} h_{i j} v_{i} + w$ . Since $w = h_{j + 1, j} v_{j + 1}$ , this is $A z_{j} = \sum_{i = 1}^{j + 1} h_{i j} v_{i}$ . Assembling these column identities for $j = 1, \dots, m$ yields $A Z_{m} = V_{m + 1} {\overset{ˉ}{H}}_{m}$ .

2.1givenF1F6F10F11step 1.3algebra

The initial residual is $r_{0} = b - A x_{0} = β v_{1}$ . The vector $e_{0}$ has value $1$ in coordinate $0$ and $0$ in every other coordinate by [F11], so $V_{m + 1} β e_{0} = β v_{1}$ . For any $y \in C^{m}$ , linearity and step 1.3 give $b - A (x_{0} + Z_{m} y) = r_{0} - A Z_{m} y = V_{m + 1} (β e_{0} - {\overset{ˉ}{H}}_{m} y)$ .

3.1F4F5step 1.1step 2.1algebra

For every $c \in C^{m + 1}$ , orthonormality from step 1.1 and the coordinate inner product [F4] give $∥ V_{m + 1} c ∥_{2}^{2} = ⟨ V_{m + 1} c, V_{m + 1} c ⟩ = \sum_{i = 1}^{m + 1} \sum_{k = 1}^{m + 1} c_{i - 1} \overline{c_{k - 1}} ⟨ v_{i}, v_{k} ⟩ = \sum_{i = 1}^{m + 1} ∣ c_{i - 1} ∣^{2} = ∥ c ∥_{2}^{2}$ . Taking the nonnegative square roots defined by [F5] proves norm preservation. Apply it to $c = β e_{0} - {\overset{ˉ}{H}}_{m} y$ in step 2.1 to obtain the asserted norm identity.

4.1step 1.2step 3.1F3F6F8F9F10F11∎

Put $S = {z_{1}, \dots, z_{m}}$ . By [F9], write any $u \in span (S)$ as $u = \sum_{a < q} c_{a} v_{a}$ with $v_{a} \in S$ . For each of the finitely many indices $a < q$ , choose $j_{a} \in {1, \dots, m}$ with $v_{a} = z_{j_{a}}$ ; successive finite induction supplies this list. Set $y^{(0)} = 0 \in C^{m}$ and, for $a < q$ , set $y^{(a + 1)} = y^{(a)} + c_{a} e_{j_{a} - 1}$ , where $e_{j_{a} - 1}$ is the standard coordinate vector. By [F3], [F6], and [F11], $Z_{m} e_{j_{a} - 1} = z_{j_{a}}$ ; the matrix-product coordinate formula and field distributivity then give by induction on $a$ that $Z_{m} y^{(a)} = \sum_{t < a} c_{t} z_{j_{t}}$ . Hence $u = Z_{m} y^{(q)}$ , so $span (S)$ is contained in the range of $Z_{m}$ . Conversely, [F3] and [F6] give $Z_{m} y = \sum_{k = 1}^{m} y_{k - 1} z_{k}$ for every $y \in C^{m}$ , so $Z_{m} y \in span (S)$ by [F8] and [F9]. Thus the range of $Z_{m}$ is exactly $span (S)$ . By step 3.1, each vector in this affine set has true-residual norm $∥ β e_{0} - {\overset{ˉ}{H}}_{m} y ∥_{2}$ . Therefore the unique least-squares minimizer from step 1.2 gives $x_{m} = x_{0} + Z_{m} y_{m}$ with minimum true residual over the whole affine span.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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

Yousef Saad, Iterative Methods for Sparse Linear Systems, 2nd ed., §9.4.1, printed pp. 287–289 (standard reference, not scraped)