The mathematics of systems that evolve under randomness, modeled as families of random variables indexed by time — from Markov chains and martingales to Brownian motion and stochastic differential equations. The field spans stochastic analysis, filtering and optimal control under uncertainty, ergodic behavior of random dynamics, and concentration of measure, with models reaching across physics, engineering, finance, and biology.
Missions
Captain: Shuze Chen
The Markov Chain Central Limit TheoremResearch Paper
Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem $$\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).$$ On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.
90 thms5 active usersReviewed
🏆Completed
Captain: tianyipeng
Markov Entanglement: Value Decomposition Error in Multi-agent MDPsResearch Paper
Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not *entangled* — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.
25 thms3 active usersReviewed
🏆Completed
Captain: tianyipeng
Markov Entanglement: Decomposition Error via Agent-wise TV DistanceResearch Paper
Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a *Markov entanglement* measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.
4 thms3 active usersReviewed
🏆Completed
Captain: wenxinzhang
Single-Server Queueing Convergence via Forward CouplingTextbook
Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.
5 thms2 active usersReviewed
Captain: Shuze Chen
Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook
# Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution
## Motivation
Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one **stationary distribution** — a probability vector $\pi$ with $\pi = \pi P$ — and that this $\pi$ is strictly positive and encodes the long-run behaviour of the chain through the return-time identity $\pi(x) = 1/\mathbb{E}_x(\tau_x^+)$. Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this $\pi$, so nothing in the subject can be formalized before this mission is.
This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, *Markov Chains and Mixing Times* (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on $\mathbb{Z}$). Later missions in the series build on the definitions published here.
## Setting
A chain on a finite state space $\Omega$ is presented by its **transition matrix**, a matrix $P \in \mathbb{R}^{\Omega\times\Omega}$ with nonnegative entries whose rows sum to $1$. A **distribution** is a row vector $\mu$ with nonnegative entries summing to $1$; one step of the chain carries $\mu$ to $\mu P$, and the $t$-step transition probabilities are the entries of the matrix power $P^t$.
The chain is **irreducible** if for all states $x, y$ there is a $t$ with $P^t(x,y) > 0$. The **period** of a state $x$ is $\gcd\,\mathcal{T}(x)$ where $\mathcal{T}(x) = \{t \ge 1 : P^t(x,x) > 0\}$, and the chain is **aperiodic** if every state has period $1$. A distribution $\pi$ is **stationary** if $\pi P = \pi$, and $\pi$ and $P$ are in **detailed balance** (the chain is *reversible*) if $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$.
Trajectory events over a finite horizon are finite sums of path weights: a length-$t$ trajectory is a function $\omega : \{0,\dots,t\} \to \Omega$, with weight $\prod_{i<t} P(\omega_i, \omega_{i+1})$ conditional on its starting state. The tail probability $\mathbb{P}_x\{\tau_z^+ > t\}$ of the first hitting time $\tau_z^+ = \min\{t \ge 1 : X_t = z\}$ is the sum of the weights of the trajectories from $x$ that avoid $z$ at times $1,\dots,t$, and expectations of hitting times are recovered by the tail-sum formula $\mathbb{E}(Y) = \sum_{t\ge0} \mathbb{P}\{Y > t\}$, formalized as a `tsum` over $t$.
## Formalization targets
### Goal
$$\text{$P$ stochastic and irreducible on a finite nonempty $\Omega$} \;\Longrightarrow\; \exists!\, \pi,\ \pi = \pi P .$$
This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of $\pi$ to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.
### Milestones toward and around the goal
The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with
$$\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$$
(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure $\pi(x) = \deg(x)/2|E|$ of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal $\hat P$ and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas $\mathbb{P}_k\{X_\tau = n\} = k/n$ and $\mathbb{E}_k(\tau) = k(n-k)$ (Proposition 2.1), the coupon collector expectation $n\sum_{k\le n} 1/k$ and tail bound $e^{-c}$ (Propositions 2.3 and 2.4), and the reflection principle and the bound $\mathbb{P}_k\{\tau_0 > r\} \le 12k/\sqrt{r}$ for simple random walk on $\mathbb{Z}$ (Lemma 2.18 and Theorem 2.17).
## Significance
*The result itself.* Existence and uniqueness of $\pi$ is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity $\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$ ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the $n \log n + cn$ analysis of the top-to-random shuffle in a later mission of this series.
*Formalizing it.* Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (`mm_basic`, `mm_path`, `mm_classical`) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.
## Difficulty
The delicate point is the existence proof. The natural first idea — extract $\pi$ from an eigenvector of $P^{\mathsf T}$ for eigenvalue $1$, or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds $\tilde\pi(y) = \mathbb{E}_z(\text{visits to } y \text{ before } \tau_z^+)$ and verifies $\tilde\pi P = \tilde\pi$ by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging `tsum` with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on $\pm 1$ paths — the bijection is easy to describe and fiddly to implement.
## Formalization scope
States form a `Fintype` with decidable equality; chains are `Matrix V V ℝ` with the row-stochasticity predicate `IsStochastic`; distributions are functions `V → ℝ` with the predicate `IsDist`. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as $\sup\{d : d \mid t \text{ for all } t \in \mathcal{T}(x)\}$, which equals $\gcd \mathcal{T}(x)$ when $\mathcal{T}(x) \neq \varnothing$ and takes the junk value $0$ otherwise. Expectations of hitting times are `tsum`s of tail probabilities, with the usual junk value $0$ for non-summable families — the statements are arranged (e.g. multiplicatively, $\pi(x)\cdot\mathbb{E}_x(\tau_x^+) = 1$) so that junk values cannot make them vacuously true. Existence statements carry a `Nonempty V` hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on $\mathbb{Z}$ are presented directly by their driving randomness (uniform draws `Fin t → Fin n`, uniform sign strings `Fin r → Bool`), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all $2^r$ strings are equally likely.
Contributions welcome beyond the milestone list: `simp` lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting `pathWeight` sums to matrix powers — these will be reused by every later mission in the series.
## Selected references
- D. A. Levin, Y. Peres, E. L. Wilmer, *Markov Chains and Mixing Times*, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
- J. R. Norris, *Markov Chains*, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511810633
- D. Aldous, J. A. Fill, *Reversible Markov Chains and Random Walks on Graphs*, 2002 (unfinished monograph). https://www.stat.berkeley.edu/~aldous/RWG/book.html