The evolving-set identity $P^t(x,y)=\frac{\pi(y)}{\pi(x)}\mathbb P_{\{x\}}\{y\in S_t\}$

Proved

MarkovMixing.evolving_sets_identity

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

markov-chainsmixing-timesprobability

Let $P$ be a Markov chain on a finite state space $V$ with strictly positive stationary distribution $\pi$ , and write $Q(S,y)=\sum_{x\in S}\pi(x)P(x,y)$ for the stationary flow from a set $S$ into a state $y$ . The evolving-set process of Morris and Peres is the Markov chain on subsets of $V$ that, from the current set $S$ , draws $u$ uniform on $(0,1]$ and passes to the superlevel set $\{y:Q(S,y)/\pi(y)\ge u\}$ ; its transition probability from $S$ to $T$ is the length of the interval of thresholds $u$ realizing $T$ .

The theorem (Lemma 17.12 of Levin–Peres–Wilmer) asserts that the set process contains the original chain: for all states $x,y$ and every time $t$ ,

P^t(x,y)\;=\;\frac{\pi(y)}{\pi(x)}\;\mathbb P_{\{x\}}\bigl\{y\in S_t\bigr\},

where the right-hand probability is over the evolving-set process started from the singleton $\{x\}$ — the sum of its $t$ -step transition probabilities into the sets containing $y$ .

Every question about $t$ -step transition probabilities is thereby a question about how the random set grows and shrinks. Combined with the martingale property of $\pi(S_t)$ (the companion lemma), this identity is what converts martingale estimates on sets into the mixing and return-probability bounds of this mission.

Preamble

import Definitions.Def_mm_martingale

Formal statement

namespace MarkovMixing

/-- **Lemma 17.12** (LPW): the transition probabilities of the chain are
recovered from the evolving-set process by
`P^t(x,y) = (π(y)/π(x)) P_{{x}}{y ∈ S_t}`. -/
theorem evolving_sets_identity {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsStationary P π) (hpos : ∀ x : V, 0 < π x)
    (x y : V) (t : ℕ) :
    (P ^ t) x y = π y / π x *
      ∑ T ∈ Finset.univ.filter (fun T : Finset V => y ∈ T),
        ((evolvingSets P π) ^ t) {x} 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 17.4, Lemma 17.12, Eq. (17.14), p. 236

Read-back

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

Read-back: evolving_sets_identity

Let $V$ be a finite type with decidable equality, and let $P$ be a real matrix on $V\times V$ that is stochastic (all entries nonnegative, every row summing to $1$ ). Let $\pi : V \to \mathbb{R}$ be stationary for $P$ , meaning both that $\pi$ is a probability distribution ( $\pi_v \ge 0$ for all $v$ and $\sum_v \pi_v = 1$ ) and that the row vector $\pi$ is fixed by $P$ : $\sum_u \pi_u P(u, y) = \pi_y$ for every $y$ . Assume additionally that $\pi$ is strictly positive: $\pi_v > 0$ for every $v \in V$ . Fix vertices $x, y \in V$ and a natural number $t \ge 0$ (the case $t = 0$ is included).

Let $K$ denote the evolving-set matrix of $(P, \pi)$ : a real matrix whose index type is the collection of all subsets of $V$ , with entries

K(S, T) \;=\; \max\bigl(0,\ U(S,T) - L(S,T)\bigr),

where, writing the clamped threshold $\widehat{Q}(S, z) = \min\bigl(1, \max\bigl(0, \tfrac{\sum_{u\in S} \pi_u P(u,z)}{\pi_z}\bigr)\bigr)$ (total division; under the strict-positivity hypothesis the denominator is never $0$ ):

$U(S,T)$ is the minimum of $\widehat{Q}(S, z)$ over $z \in T$ when $T$ is nonempty, and equals $1$ when $T = \varnothing$ ;
$L(S,T)$ is the maximum of $\widehat{Q}(S, z)$ over $z \notin T$ when $T \ne V$ , and equals $0$ when $T = V$ .

The theorem asserts the exact identity

(P^t)_{x,y} \;=\; \frac{\pi_y}{\pi_x} \sum_{\substack{T \subseteq V \\ y \in T}} \bigl(K^t\bigr)_{\{x\},\,T},

where $(P^t)_{x,y}$ is the $(x,y)$ entry of the $t$ -th matrix power of $P$ ; $K^t$ is the $t$ -th matrix power of $K$ over the index type of all subsets of $V$ (with $K^0$ the identity matrix on subsets); the sum runs over all subsets $T$ of $V$ that contain $y$ (including $T = V$ and singletons); the row index of $K^t$ is the singleton $\{x\}$ ; and $\pi_y/\pi_x$ is real division (well-defined and nonzero here since $\pi$ is strictly positive). For $t = 0$ the identity reads: the indicator of $x = y$ equals $\pi_y/\pi_x$ times the indicator that $y \in \{x\}$ .

Human review

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

View graph

The evolving-set identity Pt(x,y)=π(y)π(x)P{x}{y∈St}P^t(x,y)=\frac{\pi(y)}{\pi(x)}\mathbb P_{\{x\}}\{y\in S_t\}Pt(x,y)=π(x)π(y)​P{x}​{y∈St​}

Read-back: evolving_sets_identity

The evolving-set identity $P^t(x,y)=\frac{\pi(y)}{\pi(x)}\mathbb P_{\{x\}}\{y\in S_t\}$