Session Stochastic_Matrices

Theories

• Polynomial_Interpolation.Ring_Hom
• Jordan_Normal_Form.Missing_Misc
• HOL-Algebra.Congruence
• HOL-Algebra.Order
• HOL-Algebra.Lattice
• HOL-Algebra.Complete_Lattice
• HOL-Algebra.Group
• HOL-Algebra.FiniteProduct
• HOL-Algebra.Ring
  • File ‹ringsimp.ML›
• Jordan_Normal_Form.Missing_Ring
• Jordan_Normal_Form.Conjugate
• HOL-Algebra.Module
• Jordan_Normal_Form.Matrix
• HOL-Library.More_List
• HOL-Computational_Algebra.Polynomial
• HOL-Computational_Algebra.Fraction_Field
• HOL-Computational_Algebra.Normalized_Fraction
• HOL-Computational_Algebra.Polynomial_Factorial
• Polynomial_Interpolation.Missing_Unsorted
• Polynomial_Interpolation.Missing_Polynomial
• Polynomial_Factorization.Order_Polynomial
• HOL-Computational_Algebra.Fundamental_Theorem_Algebra
• Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
• Polynomial_Interpolation.Ring_Hom_Poly
• Jordan_Normal_Form.Gauss_Jordan_Elimination
• Jordan_Normal_Form.Column_Operations
• Jordan_Normal_Form.Determinant
• Jordan_Normal_Form.Char_Poly
• Jordan_Normal_Form.Jordan_Normal_Form
• HOL-Algebra.Coset
• VectorSpace.RingModuleFacts
• VectorSpace.FunctionLemmas
• VectorSpace.MonoidSums
• VectorSpace.LinearCombinations
• VectorSpace.SumSpaces
• VectorSpace.VectorSpace
• Jordan_Normal_Form.Missing_VectorSpace
• Jordan_Normal_Form.VS_Connect
• Jordan_Normal_Form.Matrix_Kernel
• Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
• Jordan_Normal_Form.Gram_Schmidt
• Jordan_Normal_Form.Schur_Decomposition
• Jordan_Normal_Form.Jordan_Normal_Form_Existence
• Jordan_Normal_Form.Spectral_Radius
• Perron_Frobenius.Bij_Nat
• 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›
• Perron_Frobenius.Cancel_Card_Constraint
  • File ‹cancel_card_constraint.ML›
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• Perron_Frobenius.HMA_Connect
• Perron_Frobenius.Perron_Frobenius_Aux
• Perron_Frobenius.Perron_Frobenius
• Perron_Frobenius.Roots_Unity
• Rank_Nullity_Theorem.Dual_Order
• Rank_Nullity_Theorem.Mod_Type
• HOL-Library.Function_Algebras
• Rank_Nullity_Theorem.Miscellaneous
• Perron_Frobenius.Perron_Frobenius_Irreducible
• Stochastic_Matrix
• Stochastic_Vector_PMF
• Stochastic_Matrix_Markov_Models
• Eigenspace
• Stochastic_Matrix_Perron_Frobenius