TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Shift-invert maps eigenvalues exactly and transfers an inexact solve residual to the original eigenpair

Statement

Let $A \in C^{n \times n}$ , $σ \in C$ , and $M = A - σ I$ be invertible. Then a nonzero vector $u$ is an eigenvector of $A$ with eigenvalue $λ$ if and only if it is an eigenvector of $M^{- 1}$ with eigenvalue $θ = (λ - σ)^{- 1}$ . In particular, $λ = σ + 1 / θ$ and $θ \neq 0$ .

For any nonzero candidate $u$ , any $θ \neq 0$ , and any computed vector $y$ with solve residual $s_{0} = M y - u$ , define the transformed residual $r_{T} = y - θ u$ and $λ = σ + 1 / θ$ . Then $(A - λ I) u = θ^{- 1} (s_{0} - M r_{T}),$ and consequently $∥ (A - λ I) u ∥_{2} \leq \frac{∥ s_{0} ∥_{2} + ∥ M r_{T} ∥_{2}}{∣ θ ∣} .$

Facts & Assumptions

Given: $M = A - σ I$ invertible, a nonzero vector $u$ , a nonzero scalar $θ$ , and a computed solve vector $y$ with $s_{0} = M y - u$ .

[F1]

Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism: $A u = λ u$ with $u \neq 0$ is the definition of an eigenpair.

[F2]

Shift-invert and harmonic Ritz extraction with solve and pencil status: the inexact candidate solve records $s_{0} = M y - u$ and $r_{T} = y - θ u$ .

Proof

technique · direct

1.1givenF1algebra

If $A u = λ u$ , then $M u = (λ - σ) u$ . Invertibility of $M$ and $u \neq 0$ imply $λ \neq σ$ , so applying $M^{- 1}$ gives $M^{- 1} u = (λ - σ)^{- 1} u$ . Conversely, if $M^{- 1} u = θ u$ with $u \neq 0$ , multiplying by $M$ gives $M u = θ^{- 1} u$ ; hence $A u = (σ + θ^{- 1}) u$ . Thus the eigenvalue map is exact and the inverse Ritz value cannot be zero.

1.2givenF2algebra

From [F2], $M r_{T} = M y - θ M u = u + s_{0} - θ M u$ . Rearranging yields $M u - θ^{- 1} u = θ^{- 1} (s_{0} - M r_{T})$ . Since $M = A - σ I$ and $λ = σ + 1 / θ$ , the left side is $(A - λ I) u$ , proving the residual identity.

2.1step 1.2algebra∎

Taking Euclidean norms in step 1.2 and applying the triangle inequality gives the stated residual bound, which keeps the solve residual $s_{0}$ and the transformed residual after multiplication by $M$ as separate terms.

Depends on

Used by

Shift-invert isolates an interior vibration mode and records solve error Example

Dependency tree · two levels

12 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, Numerical Methods for Large Eigenvalue Problems, second edition, §8.1.1 (standard reference, not scraped)
Peter Arbenz, Lecture Notes on Solving Large Scale Eigenvalue Problems, §§11.4 and 12.6 (standard reference, not scraped)