Stochastic Matrices and the Perron-Frobenius Theorem


Title: Stochastic Matrices and the Perron-Frobenius Theorem
Author: René Thiemann
Submission date: 2017-11-22
Abstract: Stochastic matrices are a convenient way to model discrete-time and finite state Markov chains. The Perron–Frobenius theorem tells us something about the existence and uniqueness of non-negative eigenvectors of a stochastic matrix. In this entry, we formalize stochastic matrices, link the formalization to the existing AFP-entry on Markov chains, and apply the Perron–Frobenius theorem to prove that stationary distributions always exist, and they are unique if the stochastic matrix is irreducible.
  author  = {René Thiemann},
  title   = {Stochastic Matrices and the Perron-Frobenius Theorem},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2017,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Jordan_Normal_Form, Markov_Models, Perron_Frobenius