Perron-Frobenius Theorem for Spectral Radius Analysis


Title: Perron-Frobenius Theorem for Spectral Radius Analysis
Authors: Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada
Submission date: 2016-05-20

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 An 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 An.

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 An is polynomially bounded in n.

Change history: [2017-10-18]: added Perron-Frobenius theorem for irreducible matrices with generalization (revision bda1f1ce8a1c)
[2018-05-17]: prove conjecture of CPP'18 paper: Jordan blocks of spectral radius have maximum size (revision ffdb3794e5d5)
  author  = {Jose Divasón and Ondřej Kunčar and René Thiemann and Akihisa Yamada},
  title   = {Perron-Frobenius Theorem for Spectral Radius Analysis},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2016,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Jordan_Normal_Form, Polynomial_Factorization, Rank_Nullity_Theorem, Sturm_Sequences
Used by: LLL_Factorization, Smith_Normal_Form, Stochastic_Matrices