
PerronFrobenius
Theorem
for
Spectral
Radius
Analysis
Title: 
PerronFrobenius Theorem for Spectral Radius Analysis 
Authors:

Jose Divasón,
Ondřej Kunčar,
René Thiemann and
Akihisa Yamada

Submission date: 
20160520 
Abstract: 
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 nonnegative
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
nonnegative real matrix, and no real eigenvalue of A is strictly
larger than one, then A^{n} is polynomially bounded in n. 
Change history: 
[20171018]:
added PerronFrobenius theorem for irreducible matrices with generalization
(revision bda1f1ce8a1c)
[20180517]:
prove conjecture of CPP'18 paper: Jordan blocks of spectral radius have maximum size
(revision ffdb3794e5d5) 
BibTeX: 
@article{Perron_FrobeniusAFP,
author = {Jose Divasón and Ondřej Kunčar and René Thiemann and Akihisa Yamada},
title = {PerronFrobenius Theorem for Spectral Radius Analysis},
journal = {Archive of Formal Proofs},
month = may,
year = 2016,
note = {\url{http://isaafp.org/entries/Perron_Frobenius.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Jordan_Normal_Form, Polynomial_Factorization, Rank_Nullity_Theorem, Sturm_Sequences 
Used by: 
LLL_Factorization, Stochastic_Matrices 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

