Proposition 11.4 -- the Matthews lower bound on cover times

Proved

MarkovMixing.matthews_lower

by Shuze Chen · Aug 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let $P$ be an irreducible Markov chain on a finite state space $V$ . Write $\mathbb E_x(\tau_y)$ for the expected number of steps to reach $y$ from $x$ , and

t_{\mathrm{cov}}=\max_{x\in V}\ \mathbb E_x(\tau_{\mathrm{cov}})

for the worst-case expected cover time, $\tau_{\mathrm{cov}}$ being the first time the chain has visited every state.

The theorem (the Matthews lower bound, Proposition 11.4 of Levin–Peres–Wilmer) asserts: for every set $A\subseteq V$ with at least two states and every $m\ge0$ below all hitting times within $A$ — that is, $m\le\mathbb E_a(\tau_b)$ for all distinct $a,b\in A$ —

t_{\mathrm{cov}}\;\ge\;m\,\Bigl(1+\frac12+\cdots+\frac1{|A|-1}\Bigr).

The randomized survey argument of the Matthews upper bound reverses: covering must in particular collect the hard-to-reach set $A$ , and revealing $A$ 's states in random order forces a harmonic sum of waiting times, each at least $m$ . Choosing $A$ well (spread-out states with mutual hitting times close to $t_{\mathrm{hit}}$ ) makes upper and lower bounds match up to constants.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **Proposition 11.4, the Matthews lower bound** (LPW): for any set `A` of
states and any `m` below all hitting times between distinct states of `A`,
`t_cov ≥ m (1 + 1/2 + ⋯ + 1/(|A|−1))`. -/
theorem matthews_lower {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (A : Finset V) (hA : 2 ≤ A.card) (m : ℝ) (hm : 0 ≤ m)
    (hmin : ∀ a ∈ A, ∀ b ∈ A, a ≠ b → m ≤ expSetHitTime P a {b}) :
    m * ∑ k ∈ Finset.Icc 1 (A.card - 1), (1 : ℝ) / k ≤ coverTimeMax P := 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 11.3, Proposition 11.4, p. 145

View graph