Perron-Frobenius Theorem for Spectral Radius Analysis

Resumen

The spectral radius of a matrixAis the maximum norm of alleigenvalues ofA. In previous work we already formalized that for acomplex matrixA, the values inAngrow polynomially innif andonly if the spectral radius is at most one. One problem with the abovecharacterization is the determination of allcomplexeigenvalues. In caseAcontains only non-negative real values, a simplification is possiblewith the help of the Perron-Frobenius theorem, which tells us that itsuffices to consider only therealeigenvalues ofA, i.e., applying Sturm’smethod can decide the polynomial growth ofAn.We formalize the Perron-Frobenius theorem based on a proof viaBrouwer’s fixpoint theorem, which is available in the HOL multivari-ate analysis (HMA) library. Since the results on the spectral radius isbased on matrices in the Jordan normal form (JNF) library, we fur-ther develop a connection which allows us to easily transfer theoremsbetween HMA and JNF. With this connection we derive the combinedresult: ifAis a non-negative real matrix, and no real eigenvalue ofAis strictly larger than one, thenAnis polynomially bounded inn