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 Hurwitz matrix exponential has a polynomial-exponential decay bound
Statement
Let be Hurwitz, let , and write . If is a unitary Schur triangularization and with diagonal and strictly upper triangular, then for every ,
For real Hurwitz , the same bound holds for its real matrix exponential, with the complex operator norm of its realification equal to the real one.
Facts & Assumptions
Given: A finite-dimensional real or complex matrix whose eigenvalues all have negative real part.
Hurwitz matrices and the continuous Lyapunov equation: Hurwitz means every complex eigenvalue has strictly negative real part.
If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular: Over , a finite-dimensional endomorphism has an orthonormal basis in which it is upper triangular.
The exponential series of a bounded operator: In a Banach space, the norm-convergent exponential series satisfies .
Every finite-dimensional normed space is Banach: Every finite-dimensional normed space is complete.
Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: A unitary operator preserves the norm of every vector.
The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: For compatible finite-dimensional maps, .
The complex numbers are algebraically closed: Every nonconstant complex polynomial splits over .
Proof
For complex , its characteristic polynomial splits by [F7], so [F2] gives with upper triangular. For real , regard its same real-entry matrix as acting on ; its characteristic polynomial also splits by [F7], so [F2] gives a unitary Schur triangularization there. If with real , then , so the real and complex operator norms agree.
Write , where contains its diagonal and is strictly upper triangular. By [F3] and [F4], the exponential series is differentiable in operator norm for each finite matrix. The identity in each series term gives ; [F5] gives . Each diagonal exponential satisfies for .
Differentiate with respect to and integrate from to . Since , this gives . Iterating this identity produces ordered-integral terms with factors and diagonal exponentials between them. The remainder after iterations contains strictly upper-triangular factors, with diagonal factors between them and an upper-triangular exponential at the end; every nonzero matrix-entry path would have to increase its index at least times in an matrix, so this remainder is zero.
The ordered simplex for integration variables has volume . By [F6], each th term has norm at most . Summing the terms proves the bound for ; [F5] and step 2.1 transfer it to .
Depends on
- Hurwitz matrices and the continuous Lyapunov equation
- Every finite-dimensional normed space is Banach
- The exponential series of a bounded operator
- If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular
- The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||
- Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces
- The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2
- The complex numbers are algebraically closed
Used by
- Exact Newton-Kleinman iteration preserves stability, decreases cost matrices, and converges quadratically locally Theorem
- Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution Theorem
- The Hurwitz Lyapunov integral is the unique solution and has the stated positivity Theorem
Dependency tree · two levels
49 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
- Valeria Simoncini, Computational Methods for Linear Matrix Equations, SIAM Review 58(3), 2016 (standard reference, not scraped)
- Elias Jarlebring, Numerical Methods for Lyapunov Equations, lecture notes in numerical linear algebra, 2017 (standard reference, not scraped)