Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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 A∈Cn×n be Hurwitz, let α=−max⁡{Re⁡λ:λ∈σ(A)}>0, and write etA=∑k=0∞tkAk/k!. If A=UTU∗ is a unitary Schur triangularization and T=D+N with D diagonal and N strictly upper triangular, then for every t≥0,

∥etA∥2≤e−αt∑k=0n−1(t∥N∥2)kk!.

For real Hurwitz A, 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 A whose eigenvalues all have negative real part.

[F1]

Hurwitz matrices and the continuous Lyapunov equation: Hurwitz means every complex eigenvalue has strictly negative real part.

[F2]

If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular: Over C, a finite-dimensional endomorphism has an orthonormal basis in which it is upper triangular.

[F3]

The exponential series of a bounded operator: In a Banach space, the norm-convergent exponential series satisfies (etM)′=MetM=etMM.

[F4]

Every finite-dimensional normed space is Banach: Every finite-dimensional normed space is complete.

[F6]

The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: For compatible finite-dimensional maps, ∥ST∥2≤∥S∥2∥T∥2.

[F7]

The complex numbers are algebraically closed: Every nonconstant complex polynomial splits over C.

Proof

1.1F2F7algebra

For complex A, its characteristic polynomial splits by [F7], so [F2] gives A=UTU∗ with T upper triangular. For real A, regard its same real-entry matrix as acting on Cn; its characteristic polynomial also splits by [F7], so [F2] gives a unitary Schur triangularization there. If z=x+iy with real x,y, then ∥Az∥22=∥Ax∥22+∥Ay∥22, so the real and complex operator norms agree.

2.1F1F3F4F5step 1.1algebra

Write T=D+N, where D contains its diagonal and N is strictly upper triangular. By [F3] and [F4], the exponential series is differentiable in operator norm for each finite matrix. The identity (UTU∗)k=UTkU∗ in each series term gives etA=UetTU∗; [F5] gives ∥U∥2=∥U∗∥2=1. Each diagonal exponential satisfies ∥esD∥2≤e−αs for s≥0.

3.1F3step 2.1algebra

Differentiate e(t−s)DesT with respect to s and integrate from 0 to t. Since T−D=N, this gives etT=etD+∫0te(t−s)DNesT ds. Iterating this identity produces ordered-integral terms with k factors N and diagonal exponentials between them. The remainder after n iterations contains n 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 n times in an n×n matrix, so this remainder is zero.

4.1F5F6step 2.1step 3.1algebra∎

The ordered simplex for k integration variables has volume tk/k!. By [F6], each kth term has norm at most e−αt∥N∥2ktk/k!. Summing the terms 0≤k<n proves the bound for etT; [F5] and step 2.1 transfer it to etA.

Depends on

Used by

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