Email Gateway (Aug 22 2022 at 13:25): Email Gateway (Aug 22 2022 at 13:25):From: Tobias Nipkow <nipkow@in.tum.de>
Perron-Frobenius Theorem for Spectral Radius Analysis
Jose Divasón, Ondřej Kunčar, René Thiemann, Akihisa Yamada
The spectral radius of a matrix A is the maximum norm of all eigenvalues of A.
In previous work we already formalized that for a complex matrix A, the values
in A^n grow polynomially in n if and only if the spectral radius is at most one.
One problem with the above characterization is the determination of all complex
eigenvalues. In case A contains only non-negative real values, a simplification
is possible with the help of the Perron-Frobenius theorem, which tells us that
it suffices to consider only the real eigenvalues of A, i.e., applying Sturm's
method can decide the polynomial growth of A^n.
We formalize the Perron-Frobenius theorem based on a proof via Brouwer's
fixpoint theorem, which is available in the HOL multivariate analysis (HMA)
library. Since the results on the spectral radius is based on matrices in the
Jordan normal form (JNF) library, we further develop a connection which allows
us to easily transfer theorems between HMA and JNF. With this connection we
derive the combined result: if A is a non-negative real matrix, and no real
eigenvalue of A is strictly larger than one, then A^n is polynomially bounded in n.
Much as I welcome new formalizations, especially such substantial and
fundamental ones, maybe we can call it a day for today ;-)
smime.p7s
Last updated: Apr 23 2024 at 12:29 UTC