Proposition 1.22 -- the time reversal of a chain

Open

MarkovMixing.time_reversal

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

markov-chainsmixing-timesprobability

For an irreducible chain with stationary distribution $\pi$ , the time reversal $\hat P(x,y)=\pi(y)P(y,x)/\pi(x)$ is a stochastic matrix, $\pi$ is stationary for $\hat P$ , and started from $\pi$ the reversed chain traverses every trajectory with the same probability as the original chain traverses the reversed trajectory:

\pi(x_0)P(x_0,x_1)\cdots P(x_{t-1},x_t)=\pi(x_t)\hat P(x_t,x_{t-1})\cdots\hat P(x_1,x_0).

Preamble

import Definitions.Def_mm_path

Formal statement

namespace MarkovMixing

/-- **Proposition 1.22** (LPW): for an irreducible chain with stationary
distribution `π`, the time reversal `P̂` is a stochastic matrix, `π` is
stationary for `P̂`, and started from `π` the chain run through `P̂` traverses
every trajectory with the same probability as the original chain traverses the
reversed trajectory. -/
theorem time_reversal {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π) :
    IsStochastic (timeReversal P π) ∧ IsStationary (timeReversal P π) π ∧
    ∀ (t : ℕ) (ω : Fin (t + 1) → V),
      π (ω 0) * pathWeight P ω =
        π (ω (Fin.last t)) * pathWeight (timeReversal P π) (fun i => ω i.rev) := 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.6, Proposition 1.22, p. 15

Read-back

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

Let $V$ be an arbitrary finite type (possibly empty) with decidable equality, let $P$ be a $V \times V$ matrix of real numbers, and assume: (i) $P$ is stochastic in the sense that every entry satisfies $P(x,y) \ge 0$ and every row sums to one, $\sum_y P(x,y) = 1$ ; (ii) $P$ is irreducible in the sense that for every pair $x, y \in V$ there exists a natural number $t \ge 0$ (the value $t = 0$ is allowed, in which case $P^0$ is the identity matrix, so this condition is automatic when $x = y$ ) with $(P^t)(x,y) > 0$ ; and (iii) $\pi : V \to \mathbb{R}$ is a stationary distribution for $P$ , meaning $\pi(x) \ge 0$ for all $x$ , $\sum_x \pi(x) = 1$ , and the row-vector identity $\pi P = \pi$ holds, i.e. $\sum_x \pi(x)\,P(x,y) = \pi(y)$ for every $y$ . Define the time-reversal matrix $\hat P$ entrywise by

\hat P(x,y) = \frac{\pi(y)\,P(y,x)}{\pi(x)},

where the division is the total real division that returns $0$ when the denominator $\pi(x)$ is zero (positivity of $\pi$ is not a hypothesis, so entries with $\pi(x) = 0$ are literally $0$ ). The theorem then asserts the conjunction of three claims: (1) $\hat P$ is stochastic (all entries nonnegative and every row of $\hat P$ sums to one); (2) $\pi$ is a stationary distribution for $\hat P$ (again in the sense: $\pi$ is nonnegative, sums to one, and $\pi \hat P = \pi$ ); and (3) for every natural number $t \ge 0$ and every function $\omega$ from $\{0, 1, \dots, t\}$ to $V$ (an arbitrary sequence of $t+1$ states, with no requirement that consecutive states be reachable),

\pi(\omega_0) \cdot \prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1}) \;=\; \pi(\omega_t) \cdot \prod_{i=0}^{t-1} \hat P(\omega_{t-i}, \omega_{t-i-1}),

that is, the probability weight of the path $\omega_0, \dots, \omega_t$ under $P$ started from $\pi$ equals the weight of the reversed path $\omega_t, \omega_{t-1}, \dots, \omega_0$ under $\hat P$ started from $\pi$ — here the path weight of a sequence under a matrix is the product of the matrix entries along its consecutive steps, which is the empty product $1$ when $t = 0$ , making the $t = 0$ case the trivial identity $\pi(\omega_0) = \pi(\omega_0)$ . If $V$ is empty, all three claims hold vacuously (though hypothesis (i) and (iii) are then also vacuous or degenerate: the row-sum and total-mass conditions quantify over no elements or sum over an empty set, and $\sum_x \pi(x) = 1$ with empty $V$ would read $0 = 1$ , making the hypotheses unsatisfiable in that case).

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