### Abstract

Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.

To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and prove the result that every complex matrix has a Jordan normal form using a constructive prove via Schur decomposition.

The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices, and its main advantage is its close connection to the HMA-representation which allowed us to easily adapt existing proofs on determinants.

All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.

### License

BSD License

### History

April 17, 2018
  Integrated lemmas from deep-learning AFP-entry of Alexander Bentkamp
January 7, 2016
  Added Schur-decomposition, Gram-Schmidt orthogonalization, uniqueness of Jordan normal forms

### Topics

- Mathematics/Algebra

### Session Jordan_Normal_Form

- Missing_Misc
- Missing_Ring
- Conjugate
- Matrix
- Matrix_IArray_Impl
- Gauss_Jordan_Elimination
- Gauss_Jordan_IArray_Impl
- Column_Operations
- Determinant
- Determinant_Impl
- Show_Matrix
- Char_Poly
- Jordan_Normal_Form
- Missing_VectorSpace
- VS_Connect
- Gram_Schmidt
- Schur_Decomposition
- Jordan_Normal_Form_Existence
- Matrix_Impl
- Strassen_Algorithm
- Strassen_Algorithm_Code
- Matrix_Comparison
- Ring_Hom_Matrix
- Derivation_Bound
- Complexity_Carrier
- Show_Arctic
- Matrix_Complexity
- Matrix_Kernel
- Jordan_Normal_Form_Uniqueness
- Spectral_Radius
- DL_Missing_List
- DL_Rank
- DL_Missing_Sublist
- DL_Submatrix
- DL_Rank_Submatrix

### Depends on

- Polynomial Factorization

### Used by

- The Schwartz-Zippel Lemma
- Hardness of Lattice Problems
- Verified Algorithms for Solving Markov Decision Processes
- Simplicial Complexes and Boolean functions
- Complex Bounded Operators
- Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
- Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
- Linear Programming
- Quantum Hoare Logic
- Farkas' Lemma and Motzkin’s Transposition Theorem
- Stochastic Matrices and the Perron-Frobenius Theorem
- Subresultants
- Expressiveness of Deep Learning
- Perron-Frobenius Theorem for Spectral Radius Analysis
- Gröbner Bases Theory

### Auto-related entries

- Perron-Frobenius Theorem for Spectral Radius Analysis

## Cite

×

Jordan_Normal_Form-AFP

    @article{Jordan_Normal_Form-AFP,
      author  = {René Thiemann and Akihisa Yamada},
      title   = {Matrices, Jordan Normal Forms, and Spectral Radius Theory},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Jordan_Normal_Form.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 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Aug 23, 2015 : Isabelle2015