Session Perron_Frobenius

Theories

• HOL-Analysis.L2_Norm
• HOL-Analysis.Inner_Product
• HOL-Analysis.Product_Vector
• HOL-Analysis.Euclidean_Space
• HOL-Analysis.Linear_Algebra
• HOL-Analysis.Affine
• HOL-Analysis.Convex
• HOL-Analysis.Elementary_Topology
• HOL-Analysis.Abstract_Topology
• HOL-Analysis.Continuum_Not_Denumerable
• HOL-Analysis.Abstract_Topology_2
• HOL-Analysis.Metric_Arith
  • File ‹metric_arith.ML›
• HOL-Analysis.Elementary_Metric_Spaces
• HOL-Analysis.Finite_Cartesian_Product
• HOL-Analysis.Cartesian_Space
• HOL-Analysis.Connected
• HOL-Analysis.Elementary_Normed_Spaces
• HOL-Analysis.Norm_Arith
  • File ‹normarith.ML›
• HOL-Analysis.Topology_Euclidean_Space
• HOL-Analysis.Line_Segment
• HOL-Analysis.Convex_Euclidean_Space
• HOL-Analysis.Starlike
• HOL-Analysis.Abstract_Limits
• HOL-Analysis.Function_Topology
• HOL-Analysis.Product_Topology
• HOL-Analysis.T1_Spaces
• HOL-Analysis.Path_Connected
• HOL-Analysis.Uncountable_Sets
• HOL-Analysis.Homotopy
• HOL-Analysis.Homeomorphism
• HOL-Analysis.Operator_Norm
• HOL-Analysis.Extended_Real_Limits
• HOL-Analysis.Summation_Tests
• HOL-Analysis.Infinite_Sum
• HOL-Analysis.Uniform_Limit
• HOL-Analysis.Bounded_Linear_Function
• HOL-Analysis.Derivative
• HOL-Analysis.Brouwer_Fixpoint
• HOL-Analysis.Determinants
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• HOL-Types_To_Sets.Types_To_Sets
  • File ‹local_typedef.ML›
  • File ‹unoverloading.ML›
  • File ‹internalize_sort.ML›
  • File ‹unoverload_type.ML›
  • File ‹unoverload_def.ML›
• Matrix.Utility
• Polynomial_Factorization.Polynomial_Irreducibility
• Polynomial_Factorization.Square_Free_Factorization
• HOL-Analysis.Cartesian_Euclidean_Space
• Rank_Nullity_Theorem.Dual_Order
• Rank_Nullity_Theorem.Mod_Type
• Rank_Nullity_Theorem.Miscellaneous
• Pure-ex.Guess
• Sturm_Sequences.Misc_Polynomial
• Sturm_Sequences.Sturm_Library
• Sturm_Sequences.Sturm_Theorem
• Sturm_Sequences.Sturm_Method
  • File ‹sturm.ML›
• Cancel_Card_Constraint
  • File ‹cancel_card_constraint.ML›
• Bij_Nat
• HMA_Connect
• Perron_Frobenius_Aux
• Perron_Frobenius
• Roots_Unity
• Perron_Frobenius_Irreducible
• Perron_Frobenius_General
• Spectral_Radius_Theory
• HOL-Real_Asymp.Lazy_Eval
  • File ‹lazy_eval.ML›
• HOL-Real_Asymp.Inst_Existentials
  • File ‹inst_existentials.ML›
• HOL-Real_Asymp.Eventuallize
• HOL-Real_Asymp.Multiseries_Expansion
  • File ‹asymptotic_basis.ML›
  • File ‹exp_log_expression.ML›
  • File ‹expansion_interface.ML›
  • File ‹multiseries_expansion.ML›
  • File ‹real_asymp.ML›
• HOL-Real_Asymp.Multiseries_Expansion_Bounds
  • File ‹multiseries_expansion_bounds.ML›
• HOL-Real_Asymp.Real_Asymp
  • File ‹real_asymp_diag.ML›
• Spectral_Radius_Largest_Jordan_Block
• Hom_Gauss_Jordan
• Spectral_Radius_Theory_2
• Check_Matrix_Growth