Lemma 1.13 -- expected hitting times of an irreducible chain are finite

Open

MarkovMixing.summable_hitting_tails

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

markov-chainsmixing-timesprobability

For an irreducible chain and any states $x,z$ , the expected first hitting time $\mathbb{E}_x(\tau_z^+)$ is finite. Formally: the tail probabilities $\mathbb{P}_x\{\tau_z^+>t\}$ , expressed as finite sums of trajectory weights, form a summable family in $t$ -- their sum being the expectation by the tail-sum formula $\mathbb{E}Y=\sum_{t\ge0}\mathbb{P}\{Y>t\}$ .

Preamble

import Definitions.Def_mm_path

Formal statement

namespace MarkovMixing

/-- **Lemma 1.13** (LPW): for an irreducible chain, `E_x(τ⁺_z) < ∞` for all
states `x, z` — formalized as summability of the tail probabilities
`P_x{τ⁺_z > t}`, whose sum is the expectation. -/
theorem summable_hitting_tails {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P) (x z : V) :
    Summable (fun t : ℕ => avoidTailProb P x z t) := 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.5.2, Lemma 1.13, p. 11

Read-back

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

Let $V$ be an arbitrary finite type (with decidable equality), and let $P$ be a $V \times V$ matrix of real numbers that is assumed stochastic — meaning every entry satisfies $P(x,y) \ge 0$ and every row sums to one, $\sum_y P(x,y) = 1$ — and irreducible in the following sense: for every pair of states $x, y \in V$ there exists a natural number $t \ge 0$ (with $t = 0$ allowed, where $P^0$ is the identity matrix) such that the $(x,y)$ entry of the matrix power $P^t$ is strictly positive. Fix two states $x, z \in V$ (which forces $V$ to be nonempty; $x = z$ is allowed). For each $t \in \mathbb{N}$ define the real number

a_t \;=\; \sum_{\omega : \{0,1,\dots,t\} \to V} \mathbf{1}\big[\, \omega(0) = x \;\wedge\; \omega(i) \ne z \text{ for all } 1 \le i \le t \,\big] \cdot \prod_{i=0}^{t-1} P\big(\omega(i), \omega(i+1)\big),

i.e. $a_t$ is the finite sum, over all functions $\omega$ from $\{0,\dots,t\}$ to $V$ , of the path weight $\prod_{i=0}^{t-1} P(\omega(i),\omega(i+1))$ , restricted to those $\omega$ that start at $x$ and avoid $z$ at every index from $1$ to $t$ (the starting point $\omega(0)$ is not required to differ from $z$ ); probabilistically, $a_t$ is the probability that the chain started at $x$ has not visited $z$ at any of the times $1, \dots, t$ . Note the degenerate case $t = 0$ : the avoidance condition is vacuous and the path weight is an empty product, so $a_0 = 1$ . The theorem asserts (with proof currently omitted, i.e. the statement carries a sorry) that under these hypotheses the sequence $(a_t)_{t \in \mathbb{N}}$ is summable: the series $\sum_{t=0}^{\infty} a_t$ converges (in the standard sense of unconditional/absolute convergence of a family of reals). No claim is made about the value of the sum, its finiteness bound, or any relation to hitting times; only convergence of this series is asserted.

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