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 trace eigenspace objective and a Lanczos start-angle bound
Example
Let and minimize on . The top eigenspace is , so the optimum is . Start Lanczos at and use the two-dimensional Krylov space. The normalized vector generated by , with , has Rayleigh quotient for , objective value , and objective gap . The Chebyshev start-angle theorem bounds the largest Ritz-value gap by . Direct arithmetic also gives for this explicit candidate; the candidate need not maximize the Rayleigh quotient on the Krylov space.
Facts & Assumptions
Given: The diagonal matrix , unit starting vector , and the Stiefel trace objective above.
The Stiefel gradient is the tangent projection of the ambient Euclidean gradient (Projected Euclidean gradients are the Stiefel and Grassmann gradients).
For a simple top eigenvalue, a nonzero top-eigenspace component of the start vector gives the stated Chebyshev Ritz-value error bound (Lanczos largest Ritz values obey a Chebyshev start-angle bound, including degenerate branches).
Proof
The ambient gradient of is . At , the Stiefel projection in [F1] is zero, so the eigendirection is stationary; at the global minimizer , . For the displayed start, is nonzero and belongs to .
The squared norm of this vector is , and its -quadratic form is . Dividing gives Rayleigh quotient , hence objective and gap .
Here , , , the top multiplicity is one, and . Since step 1.1 places the candidate in , its quotient shows . For Krylov dimension , the theorem [F2] gives Since , its Ritz gap obeys , so the candidate comparison and source bound agree. Also and are independent because the third coordinate of is zero while that of is nonzero, so the two-dimensional Krylov space is attained without breakdown.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
21 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, second edition (standard reference, not scraped)
- David Bindel, Matrix Computations (CS 6210), Cornell University, Lectures 38–39 (2012) (standard reference, not scraped)