{"id":5447,"date":"2016-05-22T07:00:29","date_gmt":"2016-05-22T05:00:29","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5447"},"modified":"2016-05-21T13:07:57","modified_gmt":"2016-05-21T11:07:57","slug":"resena-perron-frobenius-theorem-for-spectral-radius-analysis","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-perron-frobenius-theorem-for-spectral-radius-analysis\/","title":{"rendered":"Rese\u00f1a: Perron-Frobenius theorem for spectral radius analysis"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado <a href=\"http:\/\/www.isa-afp.org\/entries\/Perron_Frobenius.shtml\">Perron-Frobenius theorem for spectral radius analysis<\/a><\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\">Jose Divas\u00f3n<\/a> (del <a href=\"http:\/\/bit.ly\/1Rf5U7o\">grupo PSYCOTRIP (Programming and Symbolic Computation Team of the University of La Rioja<\/a>, Espa\u00f1a),<\/li>\n<li><a href=\"http:\/\/www21.in.tum.de\/~kuncar\">Ond\u0159ej Kun\u010dar<\/a> (de la <a href=\"http:\/\/www21.in.tum.de\/index\">Chair for Logic and Verification<\/a> en la <em>Technische Universit\u00e4t M\u00fcnchen<\/em>, Alemania),  <\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/thiemann\">Ren\u00e9 Thiemann<\/a> (del <a href=\"http:\/\/cl-informatik.uibk.ac.at\/\">Computational Logic Group<\/a> en la <em>University of Innsbruck<\/em>, Austria)   y <\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/ayamada\/\">Akihisa Yamada<\/a> (del <a href=\"http:\/\/cl-informatik.uibk.ac.at\/\">Computational Logic Group<\/a> en la <em>University of Innsbruck<\/em>, Austria).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  The <a href=\"http:\/\/bit.ly\/27KwAJb\">spectral radius<\/a> 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 <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=A%5En&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"A^n\" class=\"latex\" \/> 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 <em>complex<\/em> eigenvalues. In case A contains only non-negative real values, a simplification is possible with the help of the <a href=\"http:\/\/bit.ly\/27KwsZX\">Perron-Frobenius theorem<\/a>, which tells us that it suffices to consider only the real eigenvalues of A, i.e., applying Sturm&#8217;s method can decide the polynomial growth of A^n.<\/p>\n<p>  We formalize the Perron-Frobenius theorem based on a proof via <a href=\"http:\/\/bit.ly\/1Rfc47m\">Brouwer&#8217;s fixpoint theorem<\/a>, which is available in the <a href=\"http:\/\/bit.ly\/1Rfc0oh\">HOL multivariate analysis (HMA) library<\/a>. Since the results on the spectral radius is based on matrices in the <a href=\"http:\/\/bit.ly\/27Kxbuj\">Jordan normal form (JNF) library<\/a>, 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.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <a href=\"http:\/\/www.isa-afp.org\/entries\/Perron_Frobenius.shtml\">The Archive of Formal Proofs<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Perron_Frobenius\/index.html\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Perron-Frobenius theorem for spectral radius analysis Sus autores son Jose Divas\u00f3n (del grupo PSYCOTRIP (Programming and Symbolic Computation Team of the University of La Rioja, Espa\u00f1a), Ond\u0159ej Kun\u010dar (de la Chair for Logic and Verification en la Technische Universit\u00e4t M\u00fcnchen, Alemania), Ren\u00e9 Thiemann (del&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[144,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5447"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=5447"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5447\/revisions"}],"predecessor-version":[{"id":5448,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5447\/revisions\/5448"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5447"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5447"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5447"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}