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.
Ordered eigenvalues of Hermitian matrices are operator-norm Lipschitz
Statement
For Hermitian , write their eigenvalues in descending order with multiplicity as and . Then, for every ,
Facts & Assumptions
Given: Finite-dimensional Hermitian matrices and the operator -norm.
A complex normal endomorphism has an orthonormal eigenbasis (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).
For real self-adjoint matrices, Weyl's sum inequalities bound each ordered eigenvalue of a sum (Weyl inequalities bound the eigenvalues of a sum of self-adjoint endomorphisms).
A real self-adjoint matrix has a real orthonormal eigenbasis (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).
The operator -norm is the supremum of over unit vectors and, for a real self-adjoint matrix, equals the largest absolute eigenvalue (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||, Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).
Proof
Write with real. Hermitian symmetry gives and . Define and . Direct multiplication gives and ; the transpose identities show is real symmetric. Applying the same construction to yields by the supremum definition in [F4].
By [F1], for a unitary . Its realification is orthogonal, and the realification of the diagonal matrix has each twice on its diagonal. Therefore the descending eigenvalues of are ; the same holds for .
Put , , and . By [F3] and step 1.1, every eigenvalue of the real symmetric lies in using [F4]. Applying [F2] with the perturbation's largest eigenvalue for the upper bound and smallest eigenvalue for the lower bound gives for every . Taking and using step 2.1 proves the claimed complex-Hermitian eigenvalue bound.
Depends on
- Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely
- Weyl inequalities bound the eigenvalues of a sum of self-adjoint endomorphisms
- Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis
- The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||
- Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes
Used by
Dependency tree · two levels
16 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.