
Matrices,
Jordan
Normal
Forms,
and
Spectral
Radius
Theory
Title: 
Matrices, Jordan Normal Forms, and Spectral Radius Theory 
Authors:

RenĂ© Thiemann and
Akihisa Yamada (akihisa /dot/ yamada /at/ aist /dot/ go /dot/ jp)

Contributor:

Alexander Bentkamp (bentkamp /at/ gmail /dot/ com)

Submission date: 
20150821 
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 AFPentry on executable matrices, and its main advantage is its close connection to the HMArepresentation 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.

Change history: 
[20160107]: Added Schurdecomposition, GramSchmidt orthogonalization, uniqueness of Jordan normal forms
[20180417]: Integrated lemmas from deeplearning AFPentry of Alexander Bentkamp 
BibTeX: 
@article{Jordan_Normal_FormAFP,
author = {RenĂ© Thiemann and Akihisa Yamada},
title = {Matrices, Jordan Normal Forms, and Spectral Radius Theory},
journal = {Archive of Formal Proofs},
month = aug,
year = 2015,
note = {\url{https://isaafp.org/entries/Jordan_Normal_Form.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Polynomial_Factorization 
Used by: 
Complex_Bounded_Operators, Deep_Learning, Farkas, Groebner_Bases, Isabelle_Marries_Dirac, Linear_Programming, Modular_arithmetic_LLL_and_HNF_algorithms, Perron_Frobenius, QHLProver, Simplicial_complexes_and_boolean_functions, Stochastic_Matrices, Subresultants 
