Proposition 1.7 -- a positive power of an irreducible aperiodic chain

Open

MarkovMixing.exists_pow_pos

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

If the stochastic matrix $P$ is irreducible and aperiodic, then there is an integer $r>0$ such that every entry of $P^r$ is strictly positive: $P^r(x,y)>0$ for all states $x,y$ . This is the number-theoretic heart of the Convergence Theorem.

Preamble

import Definitions.Def_mm_basic

Formal statement

namespace MarkovMixing

/-- **Proposition 1.7** (LPW): if `P` is irreducible and aperiodic, then some
power of `P` has all entries strictly positive. -/
theorem exists_pow_pos {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (hap : Aperiodic P) :
    ∃ r : ℕ, 0 < r ∧ ∀ x y : V, 0 < (P ^ r) x y := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 1.3, Proposition 1.7, p. 8

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $V$ be an arbitrary finite type equipped with decidable equality (the statement does not require $V$ to be nonempty), and let $P$ be a $V \times V$ matrix with real entries. Assume three hypotheses. First, $P$ is stochastic in the sense of this bundle's custom definition: every entry satisfies $P_{x,y} \ge 0$ , and every row sums to one, $\sum_{y \in V} P_{x,y} = 1$ (if $V$ is empty, both conditions are vacuously true). Second, $P$ is irreducible in the bundle's sense: for every pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)_{x,y} > 0$ ; since $t = 0$ is allowed and $P^0$ is the identity matrix, this condition is automatically satisfied when $x = y$ , and only constrains pairs $x \ne y$ , for which some $t \ge 1$ must give a positive entry. Third, $P$ is aperiodic in the bundle's sense: for every state $x \in V$ , the quantity

\mathrm{period}(P, x) \;=\; \sup \{\, d \in \mathbb{N} \;\mid\; d \text{ divides every } t \in R(x) \,\}

equals $1$ , where $R(x) = \{\, t \in \mathbb{N} \mid t \ge 1 \text{ and } (P^t)_{x,x} > 0 \,\}$ is the set of return times of $x$ , and the supremum is the supremum in the natural numbers, which by convention takes the value $0$ when the set of common divisors is unbounded above (in particular, if $R(x)$ is empty then every natural number divides all of its elements vacuously, the divisor set is all of $\mathbb{N}$ , and the supremum is $0$ , so aperiodicity as defined here forces each $R(x)$ to be nonempty — every state must have some return time $t \ge 1$ with $(P^t)_{x,x} > 0$ — with greatest common divisor structure making $1$ the largest common divisor). Under these three hypotheses, the theorem asserts the existence of a natural number $r$ with $r > 0$ such that all entries of the $r$ -th matrix power of $P$ are strictly positive:

\exists\, r \in \mathbb{N},\quad r > 0 \;\wedge\; \forall x, y \in V,\; (P^r)_{x,y} > 0.

The claim is existential only — it asserts a single such exponent $r$ (which then makes $(P^r)_{x,y} > 0$ simultaneously for every ordered pair of states), and says nothing about positivity of $P^s$ for exponents $s$ other than $r$ , nor gives any bound on $r$ . If $V$ is empty, the inner universal statement is vacuous and the conclusion holds trivially (e.g. with $r = 1$ ).

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph