The evolving-set transition matrix is stochastic

Proved

MarkovMixing.evolving_sets_stochastic

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

markov-chainsmixing-timesprobability

For any real transition weights $P$ and state weights $\pi$ on a finite state space, the evolving-set threshold construction defines a stochastic matrix on the collection of subsets: every transition probability is nonnegative and, from every current subset $S$ , the probabilities of all possible next subsets sum to one.

Preamble

import Definitions.Def_mm_martingale

Formal statement

namespace MarkovMixing

/-- The threshold construction defining the evolving-set process is a stochastic matrix. -/
theorem evolving_sets_stochastic {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (π : V → ℝ) : IsStochastic (evolvingSets P π) := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, Section 17.4, Equation (17.13), pp. 249–250, https://pages.uoregon.edu/dlevin/MARKOV/markovmixing.pdf

View graph