Section 7.1.1 -- the counting bound

Proved

MarkovMixing.counting_lower_bound

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible, aperiodic Markov chain on a finite state space $V$ whose stationary distribution is uniform. Let

\Delta=\max_{x\in V}\#\{y: P(x,y)>0\}

be the maximal number of states reachable from a single state in one step. For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ with $\max_x\|P^t(x,\cdot)-\pi\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance.

The theorem (the counting bound, §7.1.1, display (7.2) of Levin–Peres–Wilmer) asserts: for every $0<\varepsilon<1$ ,

t_{\mathrm{mix}}(\varepsilon)\;\ge\;\frac{\log\bigl(|V|\,(1-\varepsilon)\bigr)}{\log\Delta}.

The reason: in $t$ steps the chain can reach at most $\Delta^t$ states, and until $\Delta^t$ is comparable to $|V|$ the time- $t$ distribution misses most of a uniform target. In particular chains with bounded branching need at least $\log|V|/\log\Delta$ steps to mix.

Preamble

import Definitions.Def_mm_lower
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace MarkovMixing

/-- **§7.1.1, Eq. (7.2)** (LPW), the counting bound: for a chain with uniform
stationary distribution, `t_mix(ε) ≥ log(|Ω|(1−ε)) / log Δ`, where `Δ` is
the maximal number of states accessible in one step. -/
theorem counting_lower_bound {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (hap : Aperiodic P) (hπ : IsStationary P (uniformDist V))
    (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    Real.log ((Fintype.card V : ℝ) * (1 - ε)) / Real.log (maxOutDegree P) ≤
      (mixingTime P (uniformDist V) ε : ℝ) := 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 7.1.1, Eq. (7.2), p. 87

Read-back

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

Read-back: `counting_lower_bound`

Let $V$ be a finite, nonempty type with decidable equality, and let $P$ be a $V \times V$ real matrix subject to the following hypotheses.

Stochastic: every entry satisfies $P_{x,y} \ge 0$ and every row sums to $1$ : $\sum_y P_{x,y} = 1$ for all $x$ .
Irreducible (as defined in this bundle): for every ordered pair of states $x, y$ there exists a natural number $t \ge 0$ with $(P^t)_{x,y} > 0$ . (Since $t = 0$ is allowed and $P^0 = I$ , the condition is automatic when $x = y$ ; it is a genuine reachability requirement only for $x \neq y$ .)
Aperiodic (as defined in this bundle): for every state $x$ , the period of $x$ equals $1$ , where the period is defined as the supremum (in $\mathbb{N}$ , with the convention that the supremum of an unbounded or empty-bounded set is $0$ ) of the set of natural numbers $d$ that divide every $t \ge 1$ with $(P^t)_{x,x} > 0$ .
Uniform stationarity: the uniform function $u(x) = |V|^{-1}$ (where $|V|$ is the cardinality of $V$ ) is a probability distribution ( $u(x) \ge 0$ for all $x$ and $\sum_x u(x) = 1$ ) and is invariant under $P$ acting on row vectors: $u P = u$ .
$\varepsilon$ is a real number with $0 < \varepsilon < 1$ (both inequalities strict).

Define $\Delta := \max_{x \in V} \#\{ y : P_{x,y} > 0 \}$ , the maximum over states $x$ of the number of states $y$ with a strictly positive transition entry $P_{x,y}$ (a natural number). Define the mixing time

t_{\mathrm{mix}}(\varepsilon) := \min\Big\{ t \in \mathbb{N} \;:\; \max_{x \in V} \; d_{TV}\big((P^t)_{x,\cdot},\, u\big) \le \varepsilon \Big\},

where $d_{TV}(\mu, \nu) := \sup_{A \subseteq V} \big| \sum_{x \in A} \mu(x) - \sum_{x \in A} \nu(x) \big|$ is the supremum over all subsets $A$ of the discrepancy of masses (the standard total-variation distance, without an extra factor of $\tfrac12$ ), $(P^t)_{x,\cdot}$ is the $x$ -th row of the $t$ -th matrix power, and the minimum is taken with the convention that it equals $0$ if no such $t$ exists.

The theorem then asserts the inequality of real numbers

\frac{\log\big(|V| \cdot (1 - \varepsilon)\big)}{\log \Delta} \;\le\; t_{\mathrm{mix}}(\varepsilon),

where $\log$ is the real natural logarithm and the natural numbers $|V|$ , $\Delta$ , and $t_{\mathrm{mix}}(\varepsilon)$ are cast to reals. Conventions that silently shape the claim: real division by zero yields $0$ , so if $\Delta \le 1$ (giving $\log \Delta = 0$ ; note that stochasticity with $V$ nonempty forces $\Delta \ge 1$ ) the left-hand side is $0$ and the statement reduces to $0 \le t_{\mathrm{mix}}(\varepsilon)$ , which is automatic; likewise $\log$ of a nonpositive argument is $0$ by Mathlib convention, and the left-hand side may be negative (e.g. when $|V|(1-\varepsilon) < 1 < \Delta$ ), again making the inequality weak in those regimes. The bound is non-strict ( $\le$ ), and it bounds the mixing time at accuracy $\varepsilon$ from below by $\log(|V|(1-\varepsilon)) / \log \Delta$ .

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

Section 7.1.1 -- the counting bound

Read-back: counting_lower_bound

Read-back: `counting_lower_bound`