The evolving-set identity
ProvedMarkovMixing.evolving_sets_identityLet be a Markov chain on a finite state space with strictly positive stationary distribution , and write for the stationary flow from a set into a state . The evolving-set process of Morris and Peres is the Markov chain on subsets of that, from the current set , draws uniform on and passes to the superlevel set ; its transition probability from to is the length of the interval of thresholds realizing .
The theorem (Lemma 17.12 of Levin–Peres–Wilmer) asserts that the set process contains the original chain: for all states and every time ,
where the right-hand probability is over the evolving-set process started from the singleton — the sum of its -step transition probabilities into the sets containing .
Every question about -step transition probabilities is thereby a question about how the random set grows and shrinks. Combined with the martingale property of (the companion lemma), this identity is what converts martingale estimates on sets into the mixing and return-probability bounds of this mission.
import Definitions.Def_mm_martingale
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