LemmaStatement: AI-adaptedProof: 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.

A Hermitian approximate-eigenpair residual locates a spectral value

Statement

Let $A = A^{*} \in C^{n \times n}$ , $n \geq 1$ , and equip $C^{n}$ with the standard Hermitian inner product $⟨ x, y ⟩ = \sum_{j = 1}^{n} x_{j} \overline{y_{j}}$ and its induced norm $∥ \cdot ∥_{2}$ . For $v \in C^{n} ∖ {0}$ and $θ \in R$ , if $ρ \geq ∥ A v - θ v ∥_{2}$ and $0 < ν \leq ∥ v ∥_{2}$ , then some eigenvalue $λ$ of $A$ satisfies $∣ λ - θ ∣ \leq ρ / ν$ .

Facts & Assumptions

Given: $A, v, θ, ρ, ν$ as in the statement.

[F1]

A Hermitian matrix has an orthonormal eigenbasis with real eigenvalues (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F2]

The displayed standard pairing is an inner product: linearity, conjugate symmetry and positive definiteness follow termwise. Its induced norm satisfies $∥ x ∥_{2}^{2} = \sum_{j} ∣ x_{j} ∣^{2}$ , and expansion in any orthonormal basis gives $∥ \sum_{j} c_{j} u_{j} ∥_{2}^{2} = \sum_{j} ∣ c_{j} ∣^{2}$ (Real and complex inner-product spaces and their induced length).

Proof

1.1givenF1F2choosealgebra

Choose an orthonormal eigenbasis $u_{1}, \dots, u_{n}$ with real eigenvalues $λ_{1}, \dots, λ_{n}$ , and write $v = \sum_{j} c_{j} u_{j}$ . Then $A v - θ v = \sum_{j} (λ_{j} - θ) c_{j} u_{j}$ , so [F2] gives $∥ A v - θ v ∥_{2}^{2} = \sum_{j} ∣ λ_{j} - θ ∣^{2} ∣ c_{j} ∣^{2} \geq d^{2} \sum_{j} ∣ c_{j} ∣^{2} = d^{2} ∥ v ∥_{2}^{2}$ , where $d = \min_{j} ∣ λ_{j} - θ ∣$ .

2.1givenstep 1.1algebra∎

Since $v \neq 0$ , $∥ v ∥_{2} > 0$ . Taking nonnegative square roots in step 1.1 and dividing by $∥ v ∥_{2}$ gives $d \leq ∥ A v - θ v ∥_{2} / ∥ v ∥_{2} \leq ρ / ν$ . The finite minimum defining $d$ is attained by some $j$ , and its eigenvalue obeys the required bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Nicholas J. Higham, Numerical Linear Algebra and Matrix Analysis, MIMS EPrint 2015.103, §§5.1–5.4 (standard reference, not scraped)