Convergence theorem for finite Markov chains

DefinitionUnderlying matrix of a stochastic matrix#✓fully proved

Underlying matrix of probabilities of a StochasticMatrix.

def toMatrix (P : StochasticMatrix M) : Matrix (Fin (M + 1)) (Fin (M + 1)) ℝ :=
  P.prob
Uses 1 · Used by 11
Statement usesStochastic matrix
Used byPowers of an ergodic chain are eventually all positive · Pairwise positive powers of an ergodic chain · Ergodic finite Markov chain · Ergodicity is primitivity of the transition matrix · The uniform Markov chain is ergodic · Additivity of recursive matrix powers · Recursive matrix power agrees with the matrix power · Recursive powers of a stochastic matrix power · The identity Markov chain is not ergodic · Powers of an ergodic Markov chain are ergodic · Underlying matrix of a stochastic matrix power

DefinitionErgodic finite Markov chain#✓fully proved

A finite-state Markov chain (given by its stochastic transition matrix P) is ergodic if some positive power P^n has all strictly positive entries.

def IsErgodic (P : StochasticMatrix M) : Prop :=
  ∃ n : ℕ, 0 < n ∧ ∀ i j : Fin (M + 1), (P.toMatrix ^ n) i j > 0
Uses 2 · Used by 6
Statement usesStochastic matrix · Underlying matrix of a stochastic matrix
Used byPowers of an ergodic chain are eventually all positive · Pairwise positive powers of an ergodic chain · Ergodicity is primitivity of the transition matrix · The uniform Markov chain is ergodic · The identity Markov chain is not ergodic · Powers of an ergodic Markov chain are ergodic

TheoremRecursive matrix power agrees with the matrix power#✓fully proved

The recursively defined power matPow agrees with the ordinary matrix power.

theorem matPow_eq_pow (P : StochasticMatrix M) : ∀ (n : ℕ) (i j : Fin (M + 1)),
    P.matPow n i j = (P.toMatrix ^ n) i j
Uses 3 · Used by 8
Statement usesStochastic matrix · Matrix powers of a stochastic matrix · Underlying matrix of a stochastic matrix
Used byPowers of an ergodic chain are eventually all positive · Pairwise positive powers of an ergodic chain · The uniform Markov chain is ergodic · Additivity of recursive matrix powers · Recursive powers of a stochastic matrix power · The identity Markov chain is not ergodic · Powers of an ergodic Markov chain are ergodic · Underlying matrix of a stochastic matrix power

TheoremErgodicity is primitivity of the transition matrix#✓fully proved

Ergodicity is exactly primitivity of the transition matrix. This is the bridge to Mathlib: Matrix.IsPrimitive is the same condition for a bare matrix, while IsErgodic is the stochastic-matrix form, with nonnegativity supplied by the StochasticMatrix structure.

theorem isErgodic_iff_isPrimitive (P : StochasticMatrix M) :
    P.IsErgodic ↔ Matrix.IsPrimitive P.toMatrix
Uses 3
Statement usesStochastic matrix · Ergodic finite Markov chain · Underlying matrix of a stochastic matrix

TheoremPowers of a stochastic matrix are stochastic#✓fully proved

Every row of every power of a stochastic matrix sums to 1: powers of a stochastic matrix are stochastic.

theorem matPow_row_sum (P : StochasticMatrix M) : ∀ (n : ℕ) (i : Fin (M + 1)),
    ∑ j, P.matPow n i j = 1
Uses 2 · Used by 5
Statement usesStochastic matrix · Matrix powers of a stochastic matrix
Used byFixation probability of the chain · Loss probability of the chain · Limiting loss probability of the Wright–Fisher transition matrix · Later powers of a positive stochastic matrix power stay positive · Power of a stochastic matrix

TheoremFirst recursive power of a stochastic matrix#✓fully proved

One step of the power recursion: matPow 1 is the matrix itself.

theorem matPow_one (P : StochasticMatrix M) (i j : Fin (M + 1)) :
    P.matPow 1 i j = P.prob i j
Uses 2 · Used by 4
Statement usesStochastic matrix · Matrix powers of a stochastic matrix
Used byAlmost-sure absorption of the Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Limiting fixation probability of a Wright–Fisher chain · The uniform Markov chain is ergodic

TheoremAdditivity of recursive matrix powers#✓fully proved

Powers add: matPow (a + b) is the matrix product of matPow a and matPow b.

theorem matPow_add (P : StochasticMatrix M) (a b : ℕ) (i j : Fin (M + 1)) :
    P.matPow (a + b) i j = ∑ k, P.matPow a i k * P.matPow b k j
Uses 4 · Used by 4
Statement usesStochastic matrix · Matrix powers of a stochastic matrix
Proof usesRecursive matrix power agrees with the matrix power · Underlying matrix of a stochastic matrix
Used byAlmost-sure absorption of the Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Limiting fixation probability of a Wright–Fisher chain · Later powers of a positive stochastic matrix power stay positive

TheoremLater powers of a positive stochastic matrix power stay positive#✓fully proved

If some power w of a stochastic matrix is all-positive, then every later power m ≥ w is all-positive: write m = (m - w) + w, use matPow_add, and note that row i of matPow (m - w) sums to 1, so some entry of that row is positive, and that entry times the positive matPow w entry gives a positive summand.

theorem matPow_pos_of_le_of_pos_pow {P : StochasticMatrix M} {w m : ℕ}
    (hw : ∀ i j : Fin (M + 1), 0 < P.matPow w i j) (hwm : w ≤ m) (i j : Fin (M + 1)) :
    0 < P.matPow m i j
Uses 5 · Used by 2
Statement usesStochastic matrix · Matrix powers of a stochastic matrix
Proof usesAdditivity of recursive matrix powers · Powers of a stochastic matrix are nonnegative · Powers of a stochastic matrix are stochastic
Used byPowers of an ergodic chain are eventually all positive · Powers of an ergodic Markov chain are ergodic

TheoremPairwise positive powers of an ergodic chain#✓fully proved

An ergodic chain has, for every pair of states, some positive power with a positive (i, j)-entry. (This is the per-pair form; it is strictly weaker than ergodicity, which asks for one power working for all pairs at once.)

theorem IsErgodic.exists_matPow_pos {P : StochasticMatrix M} (h : P.IsErgodic)
    (i j : Fin (M + 1)) : ∃ n : ℕ, 0 < n ∧ 0 < P.matPow n i j
Uses 5
Statement usesStochastic matrix · Ergodic finite Markov chain · Matrix powers of a stochastic matrix
Proof usesRecursive matrix power agrees with the matrix power · Underlying matrix of a stochastic matrix

TheoremPowers of an ergodic chain are eventually all positive#✓fully proved

Once a power of an ergodic chain is all-positive, every later power is all-positive: there is a threshold w past which every power is all-positive.

theorem IsErgodic.eventually_all_matPow_pos {P : StochasticMatrix M} (h : P.IsErgodic) :
    ∃ w, 0 < w ∧ ∀ m, w ≤ m → ∀ i j : Fin (M + 1), 0 < P.matPow m i j
Uses 6
Statement usesStochastic matrix · Ergodic finite Markov chain · Matrix powers of a stochastic matrix
Proof usesRecursive matrix power agrees with the matrix power · Later powers of a positive stochastic matrix power stay positive · Underlying matrix of a stochastic matrix

DefinitionPower of a stochastic matrix#✓fully proved

The p-th power of a stochastic matrix, as a stochastic matrix.

def pow (P : StochasticMatrix M) (p : ℕ) : StochasticMatrix M where
  prob := P.matPow p
  nonneg := fun i j => matPow_nonneg P p i j
  row_sum := fun i => matPow_row_sum P p i
Uses 4 · Used by 3
Statement usesStochastic matrix · Matrix powers of a stochastic matrix · Powers of a stochastic matrix are nonnegative · Powers of a stochastic matrix are stochastic
Used byRecursive powers of a stochastic matrix power · Powers of an ergodic Markov chain are ergodic · Underlying matrix of a stochastic matrix power

TheoremUnderlying matrix of a stochastic matrix power#✓fully proved

The underlying matrix of P.pow p is the p-th matrix power of P.

theorem toMatrix_pow (P : StochasticMatrix M) (p : ℕ) :
    (P.pow p).toMatrix = P.toMatrix ^ p
Uses 4 · Used by 1
Statement usesStochastic matrix · Power of a stochastic matrix · Underlying matrix of a stochastic matrix
Proof usesRecursive matrix power agrees with the matrix power
Used byRecursive powers of a stochastic matrix power

TheoremRecursive powers of a stochastic matrix power#✓fully proved

Powers of a power: (P.pow p).matPow n = P.matPow (p * n).

theorem matPow_pow (P : StochasticMatrix M) (p n : ℕ) (i j : Fin (M + 1)) :
    (P.pow p).matPow n i j = P.matPow (p * n) i j
Uses 6 · Used by 1
Statement usesStochastic matrix · Matrix powers of a stochastic matrix · Power of a stochastic matrix
Proof usesRecursive matrix power agrees with the matrix power · Underlying matrix of a stochastic matrix · Underlying matrix of a stochastic matrix power
Used byPowers of an ergodic Markov chain are ergodic

TheoremPowers of an ergodic Markov chain are ergodic#✓fully proved

Every positive power of an ergodic chain is ergodic.

theorem IsErgodic.pow {P : StochasticMatrix M} (h : P.IsErgodic) {p : ℕ}
    (hp : 0 < p) : (P.pow p).IsErgodic
Uses 8
Statement usesStochastic matrix · Ergodic finite Markov chain · Power of a stochastic matrix
Proof usesMatrix powers of a stochastic matrix · Recursive matrix power agrees with the matrix power · Later powers of a positive stochastic matrix power stay positive · Recursive powers of a stochastic matrix power · Underlying matrix of a stochastic matrix

DefinitionUniform Markov chain on finitely many states#✓fully proved

The uniform chain: every transition has probability 1 / (M + 1).

noncomputable def uniform (M : ℕ) : StochasticMatrix M where
  prob := fun _ _ => ((M + 1 : ℕ) : ℝ)⁻¹
  nonneg := fun _ _ => by positivity
  row_sum := fun _ => by
    simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    exact mul_inv_cancel₀ (by positivity)
Uses 1 · Used by 2
Statement usesStochastic matrix
Used byThe uniform Markov chain is ergodic · Transition probabilities of the uniform chain

TheoremTransition probabilities of the uniform chain#✓fully proved

The uniform chain has constant transition probabilities 1 / (M + 1).

theorem prob_uniform (M : ℕ) (i j : Fin (M + 1)) :
    (uniform M).prob i j = ((M + 1 : ℕ) : ℝ)⁻¹
Uses 2 · Used by 1
Statement usesStochastic matrix · Uniform Markov chain on finitely many states
Used byThe uniform Markov chain is ergodic

TheoremThe uniform Markov chain is ergodic#✓fully proved

The uniform chain is ergodic, with witness n = 1.

theorem isErgodic_uniform (M : ℕ) : (uniform M).IsErgodic
Uses 8
Statement usesErgodic finite Markov chain · Uniform Markov chain on finitely many states
Proof usesStochastic matrix · Matrix powers of a stochastic matrix · Recursive matrix power agrees with the matrix power · First recursive power of a stochastic matrix · Transition probabilities of the uniform chain · Underlying matrix of a stochastic matrix

DefinitionIdentity Markov chain#✓fully proved

The identity chain: prob i j is 1 on the diagonal and 0 elsewhere.

def identity (M : ℕ) : StochasticMatrix M where
  prob := fun i j => if i = j then 1 else 0
  nonneg := fun i j => by split_ifs <;> norm_num
  row_sum := fun i => by simp
Uses 1 · Used by 3
Statement usesStochastic matrix
Used byPowers of the identity chain are the identity matrix · The identity Markov chain is not ergodic · Transition probabilities of the identity chain

TheoremTransition probabilities of the identity chain#✓fully proved

The identity chain has the displayed transition probabilities.

theorem prob_identity (M : ℕ) (i j : Fin (M + 1)) :
    (identity M).prob i j = if i = j then 1 else 0
Uses 2
Statement usesStochastic matrix · Identity Markov chain

TheoremPowers of the identity chain are the identity matrix#✓fully proved

Every power of the identity chain is the identity matrix.

theorem matPow_identity (M : ℕ) : ∀ (n : ℕ) (i j : Fin (M + 1)),
    (identity M).matPow n i j = if i = j then 1 else 0
Uses 2 · Used by 1
Statement usesIdentity Markov chain · Matrix powers of a stochastic matrix
Used byThe identity Markov chain is not ergodic

TheoremThe identity Markov chain is not ergodic#✓fully proved

The identity chain is not ergodic (for M ≥ 1): every power has a zero off-diagonal entry.

theorem not_isErgodic_identity {M : ℕ} (hM : 1 ≤ M) : ¬ (identity M).IsErgodic
Uses 6
Statement usesErgodic finite Markov chain · Identity Markov chain
Proof usesMatrix powers of a stochastic matrix · Recursive matrix power agrees with the matrix power · Powers of the identity chain are the identity matrix · Underlying matrix of a stochastic matrix

TheoremDoeblin's argument#✓fully proved

Doeblin's argument (Levin, Peres and Wilmer, proof of Theorem 4.9): if the r-step transition probabilities dominate δ π, then the total variation distance of Pⁿ(x, ·) from the stationary distribution π is at most (1 - δ) ^ ⌊n / r⌋. The bound is informative when r > 0 and 0 < δ; for r = 0 (n / 0 = 0) or δ ≤ 0 it reads d_TV ≤ 1 or weaker.

theorem tvDist_pow_le_of_minorization {P : Matrix S S ℝ} (hP : P ∈ rowStochastic ℝ S)
    {π : S → ℝ} (hπ0 : ∀ y, 0 ≤ π y) (hπ1 : ∑ y, π y = 1) (hstat : π ᵥ* P = π)
    {r : ℕ} {δ : ℝ} (hmin : ∀ x y, δ * π y ≤ (P ^ r) x y)
    (n : ℕ) (x : S) :
    tvDist (fun y => (P ^ n) x y) π ≤ (1 - δ) ^ (n / r)
Uses 1 · Used by 1
Statement usesTotal variation distance of functions on a finite set
Used byThe convergence theorem

TheoremThe convergence theorem#✓fully proved

The convergence theorem (Levin, Peres and Wilmer, Theorem 4.9): a primitive (irreducible and aperiodic) stochastic matrix with stationary distribution π converges to π geometrically fast in total variation, uniformly in the starting state.

theorem exists_tvDist_pow_le {P : Matrix S S ℝ} (hP : P ∈ rowStochastic ℝ S)
    (hprim : P.IsPrimitive) {π : S → ℝ} (hπ0 : ∀ y, 0 ≤ π y) (hπ1 : ∑ y, π y = 1)
    (hstat : π ᵥ* P = π) :
    ∃ C α : ℝ, 0 ≤ α ∧ α < 1 ∧
      ∀ (n : ℕ) (x : S), tvDist (fun y => (P ^ n) x y) π ≤ C * α ^ n
Uses 2 · Used by 3
Statement usesTotal variation distance of functions on a finite set
Proof usesDoeblin's argument
Used byThe systematic-scan Gibbs sampler converges to its target · The Metropolis–Hastings chain converges to its target · Convergence of matrix powers to the stationary distribution

TheoremConvergence of matrix powers to the stationary distribution#✓fully proved

For a primitive stochastic matrix with stationary distribution π, every row of Pⁿ converges to π: Pⁿ(x, y) → π(y).

theorem tendsto_pow_apply {P : Matrix S S ℝ} (hP : P ∈ rowStochastic ℝ S)
    (hprim : P.IsPrimitive) {π : S → ℝ} (hπ0 : ∀ y, 0 ≤ π y) (hπ1 : ∑ y, π y = 1)
    (hstat : π ᵥ* P = π) (x y : S) : Tendsto (fun n => (P ^ n) x y) atTop (𝓝 (π y))
Uses 2 · Used by 1
Proof usesThe convergence theorem · Total variation distance of functions on a finite set
Used byUniqueness of the stationary distribution of a primitive chain

TheoremUniqueness of the stationary distribution of a primitive chain#✓fully proved

A primitive stochastic matrix has at most one stationary distribution. In fact π' may be any stationary vector of total mass 1, not necessarily nonnegative.

theorem stationary_unique {P : Matrix S S ℝ} (hP : P ∈ rowStochastic ℝ S)
    (hprim : P.IsPrimitive) {π π' : S → ℝ} (hπ0 : ∀ y, 0 ≤ π y) (hπ1 : ∑ y, π y = 1)
    (hstat : π ᵥ* P = π)
    (hπ1' : ∑ y, π' y = 1) (hstat' : π' ᵥ* P = π') : π = π'
Uses 1
Proof usesConvergence of matrix powers to the stationary distribution

TheoremStationary distribution of a primitive chain has full support#✓fully proved

The stationary distribution of a primitive stochastic matrix has full support.

theorem stationary_pos {P : Matrix S S ℝ} (hprim : P.IsPrimitive) {π : S → ℝ}
    (hπ0 : ∀ y, 0 ≤ π y) (hπ1 : ∑ y, π y = 1) (hstat : π ᵥ* P = π) (y : S) : 0 < π y
26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.