Theorem 5.6.6 — the convergence theorem
ProvedDurrettProbability.markov_convergenceLet be a transition probability on a countable state space that is
- irreducible — for every pair of states,
- aperiodic — every state has period one, the greatest common divisor of being , and
- equipped with a stationary distribution .
Then for all states and ,
The chain forgets its starting point: the distribution after steps converges to whatever it was at time zero. This is what makes a stationary distribution a long-run frequency rather than merely a fixed point of a linear map, and it is the theorem underlying Markov chain Monte Carlo, card shuffling, and the equilibrium analysis of queueing and inventory models.
Both hypotheses are needed and neither can be dropped. Without irreducibility the limit depends on which part of the state space the chain starts in. Without aperiodicity, oscillates: a chain alternating between two halves of its state space never forgets the parity of the clock, and Durrett's Theorem 5.7.2 gives the corrected statement for that case. Periodicity, as the book puts it, is the only thing that can prevent convergence.
The standard proof is a coupling on : run two independent copies, one from and one from , under . Aperiodicity and irreducibility make the product chain irreducible, is stationary for it, so the two copies meet with probability one, and after they meet they may be exchanged.
Formalization Note The conclusion is pointwise convergence of the transition probabilities, not convergence in total variation and not with a rate; those are strengthenings and are listed under contributions. The transition probability is a function on a countable type with non-negative entries, summable rows and rows summing to one, and every quantity involved is defined by a recursion on the matrix rather than through a measure on path space.
import Mathlib import Definitions.Def_DurrettProbability_MarkovChain open Filter
namespace DurrettProbability
theorem markov_convergence {S : Type*} [Countable S] [DecidableEq S]
(p : S → S → ℝ) (hp : IsTransition p) (hirr : Irreducible p)
(haper : ∀ x, Aperiodic p x) (π : S → ℝ) (hπ : StationaryDist p π) (x y : S) :
Tendsto (fun n : ℕ => stepProb p n x y) atTop (nhds (π y)) := by sorry
end DurrettProbabilityConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.