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

### License

BSD License

### History

May 17, 2018
  prove conjecture of CPP'18 paper: Jordan blocks of spectral radius have maximum size (revision ffdb3794e5d5)
October 18, 2017
  added Perron-Frobenius theorem for irreducible matrices with generalization (revision bda1f1ce8a1c)

### Topics

- Mathematics/Algebra

### Session Perron_Frobenius

- Cancel_Card_Constraint
- Bij_Nat
- HMA_Connect
- Perron_Frobenius_Aux
- Perron_Frobenius
- Roots_Unity
- Perron_Frobenius_Irreducible
- Perron_Frobenius_General
- Spectral_Radius_Theory
- Spectral_Radius_Largest_Jordan_Block
- Hom_Gauss_Jordan
- Spectral_Radius_Theory_2
- Check_Matrix_Growth

### Depends on

- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Polynomial Factorization
- Rank-Nullity Theorem in Linear Algebra
- Sturm’s Theorem

### Used by

- Expander Graphs
- Verified Algorithms for Solving Markov Decision Processes
- A verified algorithm for computing the Smith normal form of a matrix
- A verified factorization algorithm for integer polynomials with polynomial complexity
- Stochastic Matrices and the Perron-Frobenius Theorem

### Auto-related entries

- Stochastic Matrices and the Perron-Frobenius Theorem
- The Cayley-Hamilton Theorem

## Cite

×

Perron_Frobenius-AFP

    @article{Perron_Frobenius-AFP,
      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{https://isa-afp.org/entries/Perron_Frobenius.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 18, 2017 : Isabelle2017
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- May 20, 2016 : Isabelle2016