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 B-dual residual bounds distance to the spectrum of a Hermitian-definite pencil
Statement
Let , let , and let be Hermitian with positive definite. For and , put . Then where is the finite generalized spectrum and . Equivalently, the interval with centre and radius contains at least one generalized eigenvalue.
Facts & Assumptions
Given: A Hermitian-definite pencil , a nonzero vector , and a real scalar .
The B-inner product, B-norm, and dual residual norm: for , and .
A Hermitian-definite pencil has a real spectrum and a B-orthonormal eigenbasis: has an orthonormal eigenbasis and its eigenvalues are the generalized eigenvalues of .
Regular matrix pencils and homogeneous generalized eigenvalues: is the set of finite ratios from homogeneous roots with .
Proof
Let and . Since , the transformed residual is By [F1], and .
Let be the orthonormal eigenbasis of from [F2], with real eigenvalues . By [F3], these are exactly the finite generalized eigenvalues in . Write . Then Taking square roots and applying step 1.1 proves the bound.
Depends on
Used by
Dependency tree · two levels
13 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
- Peter Arbenz, Lecture Notes on Solving Large Scale Eigenvalue Problems, §11.4 (standard reference, not scraped)
- LAPACK Users' Guide, Generalized Symmetric Definite Eigenproblems (standard reference, not scraped)