Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper)
Jose Divasón, Sebastiaan J. C. Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada · 2018
Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of An for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations.