Motivation

The coupling method of Mission III asks for a coupling of two copies of a chain from every pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) replaces that global demand by a local one. The path coupling technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across edges; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the transportation metric (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in $O(n\log n)$ steps once $q>2\Delta$), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for counting colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.

Setting

All chains live on a finite state space $V$ with a transition matrix $P$; $P^t(x,\cdot)$ is the time-$t$ distribution from $x$, $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ the total variation distance, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ the worst-case distance to the stationary distribution $\pi$, and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ the mixing time. A coupling of distributions $\mu,\nu$ is a distribution $q$ on $V\times V$ with marginals $\mu$ and $\nu$.

Given a metric-like cost $\rho$ on pairs of states, the transportation metric between two distributions is the cheapest expected cost of moving one onto the other:

$$\rho_K(\mu,\nu)=\min\Bigl\{\sum_{x,y}\rho(x,y)\,q(x,y)\;:\;q\ \text{a coupling of}\ \mu,\nu\Bigr\}.$$

Given a connected graph structure $G$ on the state space with edge lengths $\ell\ge1$, the path metric $\rho(x,y)$ is the least total length of a $G$-path from $x$ to $y$.

For the colorings application: a $q$-coloring of the vertices of a graph is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, $n$ is the number of vertices and $\Delta$ the maximum degree of the graph being colored.

Formalization targets

Goal

Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper $q$-colorings, if $q>2\Delta$ then

$$t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{q-\Delta}{q-2\Delta}\;n\,\bigl(\log n-\log\varepsilon\bigr)\Bigr\rceil.$$

Milestones

• Lemma 14.3 and Remark 14.2 — the transportation distance is attained by an optimal coupling, and satisfies the triangle inequality (so it is a genuine metric on distributions).
• Theorem 14.6, path coupling (Bubley–Dyer) — if for every edge $\{x,y\}$ of a connected graph structure there is a coupling of the one-step distributions $P(x,\cdot),P(y,\cdot)$ contracting the path metric by $e^{-\alpha}$ in expectation, then one step of the chain contracts the transportation metric of arbitrary distribution pairs by $e^{-\alpha}$.
• Corollary 14.7 — under the same hypotheses, $d(t)\le e^{-\alpha t}\,\mathrm{diam}(V)$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil(\log\mathrm{diam}(V)-\log\varepsilon)/\alpha\rceil$, where $\mathrm{diam}(V)$ is the largest path-metric distance between two states.
• Theorem 14.12, approximate counting — for $q>2\Delta$ there is a randomized estimator, computed from an explicit polynomial number of independent uniform random seeds, which with probability at least $1-\eta$ estimates the number of proper $q$-colorings within a $(1\pm\varepsilon)$ factor: rapid sampling yields rapid approximate counting.

Significance

The results. Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the $q>2\Delta$ colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to $\#\mathrm P$-hard counting problems.

Formalizing them. Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.

Difficulty

The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires gluing two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant $(q-2\Delta)/(q-\Delta)$ emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing $|\Omega|^{-1}$ as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.

Formalization scope

The transportation metric is an sInf over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an sInf over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever $q>2\Delta$ (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability $\ge1-\eta$" is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.

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
• R. Bubley, M. Dyer, Path coupling: a technique for proving rapid mixing in Markov chains, FOCS 1997. https://doi.org/10.1109/SFCS.1997.646111
• M. Jerrum, A very simple algorithm for estimating the number of k-colorings of a low-degree graph, Random Structures Algorithms 7 (1995). https://doi.org/10.1002/rsa.3240070205
• M. Jerrum, L. Valiant, V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986). https://doi.org/10.1016/0304-3975(86)90174-X

Motivation

A reversible Markov chain is an electrical network: states are nodes, and the conductance $c(x,y)=\pi(x)P(x,y)$ turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the dictionary and its two crown results: the commute time identity of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, $\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)=c_G\,R(a\leftrightarrow b)$, and the Matthews method bounding cover times by hitting times with harmonic-number precision.

Setting

A network is a symmetric nonnegative conductance function $c$ on pairs of vertices; the associated walk moves with probabilities

$$P(x,y)=c(x,y)/c(x)$$

where $c(x)=\sum_y c(x,y)$, and $c_G=\sum_x c(x)$. A function $h$ is harmonic at $x$ if $h(x)=\sum_y P(x,y)h(y)$. The voltage with boundary values $1$ at $a$ and $0$ at $z$ is $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$, the harmonic extension of its boundary data; the current flowing out of $a$ has strength $\|I\|=\sum_y c(a,y)\,[W(a)-W(y)]$, and the effective resistance is $R(a\leftrightarrow z)=\|I\|^{-1}$. A flow from $a$ to $z$ is an antisymmetric edge function obeying the node law off $\{a,z\}$; its energy is $\mathcal E(\theta)=\sum_e\theta(e)^2/c(e)$. Hitting times $\tau_S=\min\{t\ge0:X_t\in S\}$, their expectations, the Green's function $G_{\tau_z}(a,x)$, the maximal hitting time $t_{\mathrm{hit}}$, and the cover time $t_{\mathrm{cov}}$ (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.

Formalization targets

Goal

$$\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)\;=\;c_G\,R(a\leftrightarrow b).$$

This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.

Milestones

Reversibility and stationarity of the network walk with $\pi(x)=c(x)/c_G$ (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, $h(x)=\mathbb E_x f(X_{\tau_B})$); Lemma 9.6 (the Green's function identity $G_{\tau_z}(a,a)=c(a)R(a\leftrightarrow z)$); Theorem 9.10 (Thomson's principle: $R(a\leftrightarrow z)$ is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: $\sum_y\mathbb E_a(\tau_y)\pi(y)$ does not depend on $a$); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: $t_{\mathrm{cov}}\le t_{\mathrm{hit}}\,(1+\tfrac12+\dots+\tfrac1n)$); Proposition 11.4 (the matching Matthews lower bound over subsets).

Significance

The results. The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a $\log n$ factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where $R(a\leftrightarrow\infty)$ decides transience.

Formalizing them. Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.

Difficulty

The identity chain behind the goal runs: Green's function of the stopped walk $\to$ escape probability $\mathbb P_a\{\tau_z<\tau_a^+\}=\bigl(c(a)R(a\leftrightarrow z)\bigr)^{-1}$ (via harmonic uniqueness) $\to$ the Aldous–Fill occupation identity $G_\tau(a,x)=\mathbb E_a(\tau)\pi(x)$ for stopping times with $X_\tau=a$ — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.

Formalization scope

Networks are functions $c:V\times V\to\mathbb R$ with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is defined probabilistically as $\mathbb P_x\{\tau_a<\tau_z\}$ (the book's harmonic characterization is Proposition 9.1); $R(a\leftrightarrow z)$ is the reciprocal of the explicit current strength, with total division junk when $a,z$ are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and $0^2/0=0$ handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound $m$ for the pairwise hitting times of the subset $A$ — equivalent to the book's min over pairs and easier to instantiate.

Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.

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
• P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057
• A. K. Chandra, P. Raghavan, W. L. Ruzzo, R. Smolensky, P. Tiwari, The electrical resistance of a graph captures its commute and cover times, STOC 1989. https://doi.org/10.1145/73007.73062
• P. Matthews, Covering problems for Markov chains, Ann. Probab. 16 (1988). https://doi.org/10.1214/aop/1176991894

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 tsums 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

Motivation

Reinforcement learning in a changing environment has a difficulty that is absent from a fixed Markov decision process: transition data gathered earlier may describe a different system from the one the decision maker currently faces. A learning algorithm therefore estimates transitions from a recent window of observations. The estimate comes with a confidence region, a set of transition laws consistent with the data at a chosen statistical radius. In the general nonstationary setting studied by Cheung, Simchi-Levi and Zhu, their algorithm widens this region to ensure that it can contain a model whose states remain readily reachable. Such a model is needed for the paper's dynamic regret analysis. Section 7 isolates a structural condition under which widening is unnecessary: every destination is reachable from every state with a uniformly positive one-step probability under a suitable action. Cheung, Simchi-Levi and Zhu, §7.

This mission formalizes Proposition 4 of that paper, the precise claim that the original, unwidened transition region contains a model with a controlled diameter. It is one of three separate missions for the paper. The result supports the paper's no-widening variant of its learning algorithm; it is not a claim that every model in the confidence region has small diameter. Cheung, Simchi-Levi and Zhu, Proposition 4.

Setting

There are finitely many states $\mathcal S$ and, for each state $s$, a nonempty finite set $\mathcal A_s$ of permitted actions. At each time $t\in[T]$, the system has a reward $r_t(s,a)\in[0,1]$ and a probability distribution $p_t(\cdot\mid s,a)$ for the next state. The distribution may change with $t$. A trajectory records the observed state $s_q$, chosen action $a_q$, and successor state $s_{q+1}$ at each time $q$. These are the model primitives in §2.2. Cheung, Simchi-Levi and Zhu, pp. 6–7.

An episode begins at $\tau(m)$ and uses a window of length $W$. At time $t$ in that episode, $N_t(s,a)$ counts how often the pair $(s,a)$ appears between $(\tau(m)-W)\vee1$ and $t-1$; $N_t^+(s,a)=\max\{1,N_t(s,a)\}$. The empirical row $\hat p_t(\cdot\mid s,a)$ counts observed successors and divides by $N_t^+(s,a)$. The corresponding average true row $\bar p_t$ averages the time-varying transition probabilities over the same visits. Both are zero vectors when there are no visits. Cheung, Simchi-Levi and Zhu, equations (3) and (5).

Write $SA=\sum_s|\mathcal A_s|$, so this is the number of allowed state-action pairs. At confidence level $\delta$, the transition radius is $\operatorname{rad}_{p,t}(s,a)=2\sqrt{2S\log(SAT/\delta)/N_t^+(s,a)}$. The region $H_{p,t}(s,a;\eta)$ consists of probability vectors within $\ell_1$ distance $\operatorname{rad}_{p,t}(s,a)+\eta$ of $\hat p_t$. Here $\eta=0$ means no widening. The estimation event $E_p$ bounds the $\ell_1$ distance between $\bar p_t$ and $\hat p_t$ by that radius for each allowed pair. Cheung, Simchi-Levi and Zhu, pp. 12, 14.

For a stationary transition model and policy $\pi$, the hitting time $\Lambda(s'\mid\pi,s)$ counts transitions until the first arrival at $s'$ after starting at $s$. This includes the first return time when $s=s'$. Its diameter is $D=\max_{s,s'}\min_\pi\mathbb E[\Lambda(s'\mid\pi,s)]$. Infinite expectations are possible in the definition. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization targets

Goal: Proposition 4

Assumption 2 supplies $\zeta>0$ and an allowed action $a_{(s,s')}$ for every ordered pair of states, fixed across time, such that $p_t(s'\mid s,a_{(s,s')})\ge\zeta$ for all $t\in[T]$. Conditional on $E_p$, Proposition 4 says that for every time in the horizon there exists a transition model $p$ whose every allowed row belongs to $H_{p,t}(s,a;0)$ and whose diameter obeys

$$D(\mathcal S,\mathcal A,p)\le\bar D:=\frac1\zeta.$$

The target is existential: the region need only contain one such model at each time. The milestone list follows the two cases in the proof of Lemma 13, the lemma's model existence claim, and the expected hitting-time bound in the proof of Proposition 4. Cheung, Simchi-Levi and Zhu, pp. 21, 49–50.

Significance

Proposition 4 identifies a condition under which the algorithm can use $\eta=0$ while retaining a uniform diameter guarantee for at least one plausible transition model. The paper uses this to analyze a no-widening version of its dynamic regret bound, and later applies that viewpoint to inventory control. Without a bounded-diameter model in the region, the diameter-dependent regret argument does not apply in the same form. Cheung, Simchi-Levi and Zhu, §7.

The proposition and its appendix proof are known results of the paper. This mission asks for a machine-checked account of the exact confidence region, its pathwise estimation event, Lemma 13, and the diameter claim. A general finite MDP with probability-valued transition rows is already available as the published FiniteMDPLearning definition; the paper-specific window estimators and its return-time diameter still need formal proofs. The paper's headline Theorems 1–4 are not posed here because their displayed bounds hide constants in $\widetilde O(\cdot)$ notation. Cheung, Simchi-Levi and Zhu, p. 6 and Theorems 1–4.

Difficulty

The obvious idea that the true transition law belongs to the confidence region can fail under drift: the region is centered on recent observations, while the law at the current time may differ from the laws that generated those observations. Even the average true row has a special case. At an unvisited pair, equation (5) sets it to the zero vector, which is not a probability distribution and therefore is not a member of the simplex-valued confidence region. The existence claim must cover visited and unvisited pairs while preserving one-step reachability for all targets under a single transition law. Cheung, Simchi-Levi and Zhu, pp. 12, 49–50.

The diameter also uses the paper's first-arrival-after-start convention. A library travel time that is zero when source equals target misses the return-time cases and would weaken the stated conclusion. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization scope

States and actions are Fin S and Fin A; permitted actions are state-dependent finite sets. Extra MDP rows for disallowed actions are never consulted. The finite MDP type supplies valid probability rows and bounded rewards. Hitting times and the diameter use extended nonnegative reals, so infinite values are represented without a default real value. The diameter ranges over allowed deterministic stationary policies and over all ordered state pairs, including equal pairs. Time is zero-based in Lean: paper time $t\in[T]$ is index $t-1<T$, and the paper's window becomes the half-open interval [τm-W,t). The paper's $N^+$ is at least one, so its estimators never divide by zero. A result at arbitrary $t$ with $\tau_m\le t<T$ covers every episode time without assuming any additional episode schedule property.

The Lean statement makes two domain conditions explicit: $S>1$ and $0<\delta<1$. These ensure the paper's claim that the radius at an unvisited pair is at least one; it can fail when $S=1$ and the confidence level is close to one. Assumption 2 is required for every time in the horizon, with $\zeta>0$. The event $E_p$ is the $\ell_1$ estimation inequality at the selected time. The paper writes it as membership of $\bar p_t$ in a simplex-valued region for every pair, but that literal wording is false at an unvisited pair because $\bar p_t=0$ there. At visited pairs, the inequality and membership agree. This convention is disclosed in the definition item and keeps the theorem meaningful on ordinary early trajectories.

The region is centered at the exact empirical $\hat p_t$, uses $\eta=0$, and constrains every allowed row of the constructed model. The diameter uses its full extended-real value, and $\zeta$ is strictly positive; dropping any of these clauses would change the claim. Reusable contributions include finite-state hitting-time estimates and windowed transition estimation identities. Proofs of the four milestones and the goal, as well as small lemmas connecting the published MDP measure to successive transition rows, are welcome.

Selected references

• W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. arXiv
• T. Jaksch, R. Ortner and P. Auer, Near-optimal Regret Bounds for Reinforcement Learning, Journal of Machine Learning Research 11, 2010. JMLR

Motivation

The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues $1=\beta_0>\beta_1\ge\dots\ge\beta_{m-1}\ge-1$, the distance to stationarity after $n$ steps is governed by $\beta_*^{\,n}$, where $\beta_*=\max(\beta_1,|\beta_{m-1}|)$ (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue $\beta_1$ are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue $\beta_{\min}=\beta_{m-1}$: a chain whose smallest eigenvalue is close to $-1$ oscillates almost periodically and mixes slowly whatever $\beta_1$ is. A chain is aperiodic exactly when $\beta_{\min}>-1$, but that qualitative fact gives no rate.

Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on $\beta_{\min}$ uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.

Timeline:

• 1988–1989, Jerrum and Sinclair: conductance (Cheeger-type) bounds on $\beta_1$ for chains on combinatorial structures.
• 1991, Diaconis and Stroock: path bounds for $\beta_1$ (Proposition 1, the Poincaré inequality $\beta_1\le1-1/\kappa$) and for $\beta_{\min}$ (Proposition 2, this mission), with the specializations to random walks on graphs (Corollaries 1 and 2).

Setting

Let $X$ be a finite set and $P(x,y)$ the transition matrix of an irreducible Markov chain on $X$, reversible with respect to a probability distribution $\pi$:

$$Q(x,y)=\pi(x)P(x,y)=\pi(y)P(y,x)\qquad(x,y\in X).$$

The operator $(P\varphi)(x)=\sum_yP(x,y)\varphi(y)$ is self-adjoint on $L^2(\pi)$, with inner product $\langle\varphi,\psi\rangle_{L^2(\pi)}=\sum_x\varphi(x)\psi(x)\pi(x)$, so its eigenvalues are real. Write $E(\varphi^2)=\sum_x\varphi(x)^2\pi(x)$ and let $\beta_{\min}$ be the smallest eigenvalue of $P$.

The graph of the chain has vertex set $X$, an edge from $x$ to $y$ when $Q(x,y)>0$, and a self-loop at $x$ when $Q(x,x)>0$. An odd closed path $\sigma_x$ at $x$ is a sequence of edges from $x$ back to $x$, with an odd number of edges, in which no directed edge is traversed twice. Its length is

$$|\sigma_x|_Q=\sum_{e\in\sigma_x}Q(e)^{-1}.$$

A system of odd paths $\Sigma=(\sigma_x)_{x\in X}$ chooses one such path for every point, and its load is

$$\iota=\iota(\Sigma)=\max_e\sum_{\sigma_x\ni e}|\sigma_x|_Q\,\pi(x),$$

the maximum over directed edges $e$ of the weighted length of the paths through $e$ (display (1.7) of the paper).

For the random walk on a graph $G=(X,E)$, $P(x,y)=1/d(x)$ when $\{x,y\}\in E$, with $d(x)$ the degree, and $\pi(x)=d(x)/2|E|$. There $d_*$ is the maximum degree, $\sigma_*$ the largest number of edges of a path in $\Sigma$, and $b_*=\max_e\sharp\{\sigma\in\Sigma:e\in\sigma\}$.

Formalization targets

Goal: Proposition 2

For an irreducible, aperiodic, reversible chain and every system $\Sigma$ of odd closed paths,

$$\beta_{\min}\ge-1+\frac{2}{\iota(\Sigma)}.$$

Milestones (the steps of the paper's proof)

1. The identity (1.8): $\tfrac12\sum_{x,y}(\varphi(x)+\varphi(y))^2Q(x,y)=E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}$.
2. Along an odd closed path $x,y,w,\dots,z,x$: $\varphi(x)=\tfrac12\{(\varphi(x)+\varphi(y))-(\varphi(y)+\varphi(w))+\dots+(\varphi(z)+\varphi(x))\}$.
3. For every $\varphi$: $E(\varphi^2)\le\frac{\iota}{2}\big(E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}\big)$.
4. Every eigenvalue $\beta$ of $P$ satisfies $\beta\ge-1+2/\iota$.

Companions

• Corollary 2. For the random walk on a connected, non-bipartite graph and any system $\Sigma$ of odd paths, $\beta_{\min}\ge-1+\dfrac{2}{d_*\sigma_*b_*}$.
• Remark 1.3. With odd paths $\sigma_{xy}$ for every ordered pair and $\tilde\iota=\max_e\sum_{\sigma_{xy}\ni e}|\sigma_{xy}|_Q\pi(x)\pi(y)$: $\beta_{\min}\ge-1+1/\tilde\iota$.

Significance

Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds $\beta_1\le1-1/\kappa$ through paths between pairs of points, it bounds the absolute spectral gap $1-\beta_*$ entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.

Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the $L^2(\pi)$ inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that $-1$ is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.

Difficulty

Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while $\iota$ counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs $(x,y)$, including $x=y$, in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels $\varphi(x)$ instead of doubling it.

The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small $\iota$, and the choice of $\Sigma$ is part of every application.

Formalization scope

The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that $\pi$ is a probability vector) and DetailedBalance. $Q$ is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). $\beta_{\min}$ is the infimum of the real eigenvalues of $P$, a minimum for a stochastic matrix on a nonempty set.

Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with $Q>0$. The paper defines $|\sigma_x|_Q$ "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. $\iota$ is a real supremum over the finite set of directed edges with $Q>0$, and it is $0$ only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to $\beta_{\min}\ge-1$ by $2/0=0$. The system $\Sigma$ is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption $|X|\ge2$ is made.

Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, $b_*$ counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.

Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.

Selected references

• P. Diaconis and D. Stroock, Geometric bounds for eigenvalues of Markov chains, Ann. Appl. Probab. 1(1):36–61, 1991. https://doi.org/10.1214/aoap/1177005980
• A. Sinclair and M. Jerrum, Approximate counting, uniform generation and rapidly mixing Markov chains, Inform. and Comput. 82(1):93–133, 1989. https://doi.org/10.1016/0890-5401(89)90067-9
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (2nd ed. 2017). https://doi.org/10.1090/mbk/107

Motivation

How fast a finite Markov chain forgets its starting point is the central quantitative question in the analysis of Monte Carlo algorithms, card shuffling and random walks on groups. The classical tool is the spectral gap $\lambda$, which controls convergence in $\ell^2(\pi)$ but loses a factor $1/\pi(x)$ when converted into a bound for a chain started at a point. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) brought the logarithmic Sobolev constant $\alpha$, introduced by Gross for Gaussian measures (Amer. J. Math. 97 (1975)), into the study of finite chains, and showed that it gives sharper mixing bounds in many examples.

The entropy route to ergodicity is the cleanest consequence of a log-Sobolev inequality: the relative entropy of the chain's law with respect to stationarity decays exponentially at rate $2\alpha$, and at rate $4\alpha$ for reversible chains. The paper notes that the reversible case is contained in Bakry's Saint-Flour lectures (Lecture Notes in Math. 1581, 1994) and Stroock's notes on Gibbs states (Lecture Notes in Math. 1563, 1993), and that Miclo (preprint, 1995) treated the nonreversible case.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$. Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$, with $\pi(x)>0$ for every $x$. Functions act on the right, $Kf(x)=\sum_yK(x,y)f(y)$, and $\langle f,g\rangle=\sum_xf(x)g(x)\pi(x)$ is the inner product of $\ell^2(\pi)$, with norms $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$. The chain is reversible if $\pi(x)K(x,y)=\pi(y)K(y,x)$ for all $x,y$.

The continuous-time heat semigroup is

$$H_t=e^{-t(I-K)}=e^{-t}\sum_{n\ge0}\frac{t^n}{n!}K^n,$$

acting on functions by $H_tf(x)=\sum_yH_t(x,y)f(y)$ and on probability measures by $\mu H_t(y)=\sum_xH_t(x,y)\mu(x)$. The row $H_t^x=H_t(x,\cdot)$ is the law at time $t$ of the chain started at $x$.

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$; it is bilinear but not symmetric unless the chain is reversible. With

$$\mathcal L(f)=\sum_x|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),$$

the log-Sobolev constant is

$$\alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.$$

The relative entropy of a probability $\mu$ is $\mathrm{Ent}_\pi(\mu)=\sum_x\mu(x)\log\frac{\mu(x)}{\pi(x)}$, and the total variation distance is $\|\mu-\pi\|_{TV}=\sup_{A\subset\mathcal X}|\mu(A)-\pi(A)|$.

Formalization targets

Goal: Theorem 3.6 (p. 722)

For every probability measure $\mu$ on $\mathcal X$,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-2\alpha t},\qquad t>0,$$

and, if $(K,\pi)$ is reversible,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-4\alpha t},\qquad t>0.$$

Milestones

1. §2.1, Remarks (ii), p. 702: if $\mu=f\pi$ then $\mu H_t$ has density $H_t^*f$, where $H_t^*$ is the semigroup of the adjoint kernel $K^*(x,y)=K(y,x)\pi(y)/\pi(x)$.
2. Lemma 2.5, second part, p. 707: $\partial_t\,\mathrm{Ent}_\pi(H_tf)|_{t=0}=-\mathcal E(f,\log f)$.
3. Lemma 2.7, p. 708: $\mathcal E(\log f,f)\ge2\,\mathcal E(\sqrt f,\sqrt f)$, and $\ge4\,\mathcal E(\sqrt f,\sqrt f)$ for reversible chains.
4. §3.3, p. 722: for $f\ge0$ with $\|f\|_2=1$ and $\mu=f^2\pi$, $\mathcal L(f)=\mathrm{Ent}_\pi(\mu)$.
5. (2.8), p. 710: $2\|\mu-\pi\|_{TV}^2\le\mathrm{Ent}_\pi(\mu)\le\|\mu-\pi\|_{TV}+\tfrac12\|\mu/\pi-1\|_{\pi,2}^2$.

Companion: (3.3) (p. 723)

For an irreducible chain, every $x$ and $t>0$,

$$2\|H_t^x-\pi\|_{TV}^2\le\Big(\log\frac1{\pi(x)}\Big)e^{-2\alpha t},$$

with $2\alpha$ replaced by $4\alpha$ for reversible chains.

Significance

Theorem 3.6 turns a single functional inequality into a convergence statement valid for every initial law, with no spectral assumption and no reversibility in the first half. Through Pinsker's inequality it gives (3.3), whose prefactor $\log(1/\pi(x))$ replaces the factor $1/\pi(x)$ of the spectral bound $4\|H_t^x-\pi\|_{TV}^2\le\pi(x)^{-1}e^{-2\lambda t}$. When $\pi(x)$ is exponentially small in the size of the problem, as for random walks on large groups or product spaces, $\log(1/\pi(x))$ is polynomial where $1/\pi(x)$ is exponential, and the time needed to make the bound small drops accordingly. This is the mechanism behind the sharp mixing bounds the paper derives from $\alpha$.

The results are proved in the paper and are classical; they are not, to our knowledge, formalized. The platform has measure-theoretic statements of Pinsker's inequality and the published finite Markov chain vocabulary of Levin–Peres–Wilmer (stochastic matrices, stationarity, total variation, the heat kernel), but nothing about log-Sobolev constants of finite chains, the entropy derivative along a Markov semigroup, or entropy decay. A formal development provides the entropy layer of the finite-chain theory: the adjoint semigroup, the dissipation identity, the comparison of $\mathcal E(\log f,f)$ with $\mathcal E(\sqrt f,\sqrt f)$, and Pinsker's inequality in the encoding used by the mixing-time library.

Difficulty

The statement is about measures, while the natural quantities to differentiate are densities with respect to $\pi$, and for a nonreversible chain the density of $\mu H_t$ evolves under the adjoint semigroup, not under $H_t$. The Dirichlet form is not symmetric, so the order of its arguments matters at every step, and the improvement from $2\alpha$ to $4\alpha$ holds only under reversibility.

The obvious first idea, differentiating $\mathrm{Ent}_\pi(\mu H_t)$ term by term, meets $\log 0$ wherever the density vanishes. The initial law may be a point mass, and for a reducible chain the density can stay zero at positive times. The argument must therefore handle the boundary $t=0$ and the degenerate laws separately from the smooth interior. The constant $\alpha$ is defined as an infimum over all functions, with no claim that it is attained or positive.

Formalization scope

The state space is a Fintype with decidable equality, $K$ is a real matrix with the published predicate MarkovMixing.IsStochastic, $\pi$ satisfies MarkovMixing.IsStationary K π and $\pi(x)>0$ for all $x$, and reversibility is MarkovMixing.DetailedBalance K π. $H_t$ is the published MarkovMixing.heatKernel K t (the Poisson series), the adjoint kernel is MarkovMixing.timeReversal K π, and total variation is MarkovMixing.tvDist. Time is real, and the decay statements are for $t>0$.

The local definitions are $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$, the norms $\|f\|_p$, $\mathcal L$, $\alpha$ as a real infimum over the ratios with $\mathcal L(f)\ne0$, $\mathrm{Ent}_\pi(\mu)$, and $\mu H_t$ as the row vector $\mu\,H_t$. Lean's Real.log 0 = 0 implements $0\log0=0$. The goal does not assume irreducibility: it is true for every stochastic $K$ with a positive invariant probability, and a reducible chain has $\alpha=0$. The companion (3.3) keeps irreducibility, the standing assumption of Section 3. In Lemmas 2.5 and 2.7 the paper's $f\ge0$ is strengthened to $f>0$, because $\log f$ is $-\infty$ at a zero of $f$ on the page and $0$ in Lean.

Several encodings would make the goal trivially true and are ruled out. $\alpha$ is not assumed positive. $\mu$ is a probability, since for $\mu=2\pi$ the entropy is a positive constant in $t$. $\pi$ is invariant and positive, so $\mu/\pi$ is meaningful. The eigenvalue-based MarkovMixing.spectralGap is not used. Applying $H_t$ to $\mu$ as a function, $H_t\mu$, is not the same as $\mu H_t$ for a nonreversible chain.

A complete development needs: termwise differentiation of the heat-kernel series and the semigroup property $\partial_tH_t=(K-I)H_t$; the adjoint identity for $H_t$; elementary convexity inequalities for $\log$ and $\sqrt{\cdot}$; the symmetric form of $\mathcal E$ for reversible chains; Pinsker's inequality on a finite set; and a scalar Grönwall lemma. The heat-kernel calculus and Pinsker's inequality in the MarkovMixing.tvDist encoding are reusable by the other missions of this series and by any mixing-time development. Proofs of individual milestones are welcome independently of the goal.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6 (1996), 695–750. https://doi.org/10.1214/aoap/1034968224
• L. Gross, Logarithmic Sobolev inequalities, Amer. J. Math. 97 (1975), 1061–1083. https://doi.org/10.2307/2373688
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017. https://doi.org/10.1090/mbk/107

Motivation

Inspection and revision cost money, but continued production can allow a deteriorating process to remain in a costly state. A controller therefore needs a rule that converts incomplete information about the process into an action. Ross's two-state model makes that decision precise: the process can be good or bad, the bad state persists until revision, and inspection reveals the current state. The observable state for decision making is a probability rather than the underlying process state. This setup is useful when quality is inferred from occasional inspection and actions must be chosen before the state is known. Ross proved structural results for discounted control in this model, including sufficient conditions for a policy with one inspection interval and for a policy with no inspection at all. Ross (1971)

The conditions in Theorem 3.7 use the model's optimal value itself. They are therefore structural tests for the shape of an optimal rule, rather than parameter-only design formulas. The preceding concavity, monotonicity and Lipschitz estimates explain which features of that value function support the tests. The mission records those estimates alongside the main result, so the target is a coherent part of the paper rather than an isolated inequality. Ross (1971), pp. 589–593

Setting

The belief $P\in[0,1]$ is the probability that the production process is in the bad state at the beginning of a period. A good process becomes bad during a period with probability $\pi\in[0,1]$ if it is not revised. A bad process remains bad. Thus producing without inspection changes the next belief to $T(P)=P+\pi-\pi P$. The discount factor is $\beta\in(0,1)$. Producing without inspection has cost $0$ in the good state and cost $C$ in the bad state, so its expected current cost is $CP$. Inspection costs $I$ in either state, and revision costs $R$ in either state. The standing order is $0<C<I<R$. The explicit $C>0$ records that $C$ is a cost and makes the quotient in Theorem 3.7 meaningful.

Write $V_\beta(P)$ for the discounted value starting from belief $P$. Inspection reveals the current state: the next belief is $\pi$ after observing a good process and $1$ after observing a bad one. Revision resets the next belief to $\pi$. The three current-plus-continuation costs are

$$\begin{aligned} q_{\mathrm P}(P)&=CP+\beta V_\beta(T(P)),\\ q_{\mathrm I}(P)&=I+\beta P V_\beta(1)+\beta(1-P)V_\beta(\pi),\\ q_{\mathrm R}(P)&=R+\beta V_\beta(\pi). \end{aligned}$$

The Bellman equation is $V_\beta(P)=\min\{q_{\mathrm P}(P),q_{\mathrm I}(P),q_{\mathrm R}(P)\}$. A stationary rule is $\beta$-optimal here when it chooses an action attaining this minimum at every admissible belief. This is the paper's decision rule criterion associated with equation (3). Ross (1971), p. 590, equation (3)

Formalization targets

The first target is the sufficient condition for an optimal three-region rule. Set $\Delta=V_\beta(1)-V_\beta(\pi)$. If

$$\frac{(1-\beta)(R+\beta V_\beta(\pi))}{C}\le\frac{R-I}{\beta\Delta},$$

there are thresholds $\pi\le P_1\le P_2$ such that an optimal rule produces for $P<P_1$, inspects for $P_1\le P<P_2$, and revises for $P\ge P_2$. The revise interval may be empty: if no admissible belief has revision as an optimal action, $P_2$ may exceed $1$. If revision is optimal somewhere, the conclusion includes $P_2\le1$. This is a repair to the printed bound in Theorem 3.7(a); the proof on p. 593 explicitly lets a missing threshold be infinite. Ross (1971), pp. 592–593, Theorem 3.7(a)

The second target gives an optimal no-inspection rule. If

$$I+\beta\Delta\ge\frac{C}{1-\beta(1-\pi)} \quad\text{or}\quad \frac{R-I}{\beta\Delta}\le\frac{R}{C}\bigl(1-\beta(1-\pi)\bigr),$$

then some $P_1\ge\pi$ gives an optimal rule that produces below $P_1$ and revises from $P_1$ onward. A threshold above $1$ is allowed and means that the rule produces throughout the admissible belief interval. Both alternatives in the source's condition are retained. Ross (1971), p. 592, Theorem 3.7(b)

Significance

The theorem identifies two kinds of simple stationary rule that can be optimal despite the value function depending on an unobserved process state. It says more than the existence of an optimal action at each belief: the selected actions can be arranged in belief intervals, and in the second regime inspection can be omitted entirely. These statements provide a compact description of decisions over the full continuum $P\in[0,1]$. Ross (1971), Theorem 3.7

The result was proved in the 1971 paper. This mission asks for machine-checked Lean proofs of its two repaired clauses, the value equation, and the stated shape estimates. The definitions and finite-horizon bound can also support later formalizations of related belief-state control models. No proof of this mission's draft theorem is claimed merely by compiling its statement.

Difficulty

The action costs have different shapes as functions of belief: inspection and revision give affine and constant expressions, while the production alternative includes the value at an updated belief. The apparent order of their pairwise crossings does not by itself establish that one selected rule attains the minimum at every belief. Equalities at a threshold also matter, since the rule must be optimal at the boundary points. The printed upper bound on the last threshold fails when revision never minimizes the Bellman equation; imposing it without qualification would make the formal target false.

Formalization scope

Lean represents a belief as a real number and restricts all claims to $[0,1]$. It defines $V^0=0$ and obtains $V^{n+1}$ by taking the minimum of the three action costs with continuation $V^n$, exactly as in equation (4). The value $V_\beta$ is the limit of these iterates; convergence and boundedness are part of the equation (3) milestone. This prevents an arbitrary function satisfying a convenient fixed-point hypothesis from replacing the value the paper studies. The rule types are total real-to-action functions, while optimality is checked for every admissible belief, including $P=1$ and both thresholds.

The paper's general Lemma 2.1 is represented by its scalar two-state instance. The finite-horizon Lipschitz bound and its limiting corollary use $P_1,P_2\in[0,1]$. The last quotient in Corollary 3.6 divides by $\pi$, so that second inequality is stated under $\pi>0$; the first inequality, and the main theorem, cover $\pi=0$. If $\pi=1$, then $\Delta=0$. Lean's real division gives a zero quotient in that case; the two implications in Theorem 3.7 remain valid under this convention. The development needs reusable results about convergence of discounted value iteration, concavity and monotonicity on an interval, and elementary estimates for affine belief updates. Contributions establishing those results or proving either sufficient-condition clause are within scope.

Selected references

• Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587

Motivation

A production process can deteriorate without an operator seeing its current condition. Producing a unit, inspecting the process, and revising the process have different immediate costs and different effects on what can be known or controlled next period. The operator therefore needs a rule based on a belief about deterioration, rather than on the hidden physical state. Ross's two-state model asks when the simplest rule, producing every period without inspection, is actually optimal over an unlimited discounted horizon Ross 1971.

The question matters whenever an action has a cost now but may reduce future losses. Paying for inspection only supplies information; paying for revision restores a deteriorated process. The answer depends on the bad-state production cost, the deterioration probability, the revision charge, and the weight assigned to future periods. A comparison of immediate costs alone cannot settle whether revision is worthwhile. Ross's Theorem 3.4 gives an exact boundary between a regime where producing forever is optimal from every initial belief and a regime where revision is forced when deterioration is nearly certain Ross 1971, Theorem 3.4.

Setting

There are two underlying states: good and bad. The current state is hidden, and $P\in[0,1]$ is the probability that it is bad at the beginning of a period. Producing without inspection costs zero in the good state and $C$ in the bad state, so its expected immediate cost is $CP$. A good process becomes bad with probability $\pi$ in one period; a bad process remains bad until revision. Thus a period of production without inspection changes the belief to $T(P)=P+\pi-\pi P$. These are the conventions of the paper's Section 3 Ross 1971, p. 590.

The other actions are inspection, at cost $I$, and revision, at cost $R$. Inspection reveals the current state: the next belief is $1$ when the state was bad and $\pi$ when it was good. Revision returns the process to the good state before its next transition, so the next belief is $\pi$. The standing parameter conditions are $0<\beta<1$, $0\le\pi\le1$, and $0<C<I<R$; $\beta$ is the discount factor. The paper explicitly assumes $C<I<R$ and a discount factor in $(0,1)$. Positive $C$ states the intended positive bad-state cost and makes the threshold comparison meaningful Ross 1971, pp. 588, 590.

For a future-cost function $W$, the three Bellman alternatives at belief $P$ are $CP+\beta W(TP)$, $I+\beta P W(1)+\beta(1-P)W(\pi)$, and $R+\beta W(\pi)$. Their minimum defines one step of finite-horizon value iteration, beginning with $V^0=0$. The limit $V_\beta(P)$ is the optimal discounted cost. Write $R^0$ for the rule that always produces without inspection, and define its cost from the actual discounted series $\psi(P)=\sum_{n=0}^{\infty}\beta^n C T^nP$ Ross 1971, equations (3)–(5).

Formalization targets

The first target establishes that value iteration converges on $[0,1]$, gives a bounded solution to the two-state Bellman equation, and identifies that solution uniquely among bounded functions. The iterated update and Ross's equation (5) then evaluate the cost of $R^0$:

$$T^nP=1-(1-P)(1-\pi)^n,\qquad \psi(P)=\frac{C}{1-\beta}-\frac{C(1-P)}{1-\beta(1-\pi)}.$$

The sensitivity milestones retain the exact finite-horizon factor in Lemma 3.5 and the infinite-horizon bound in Corollary 3.6. In particular, for $P_1,P_2\in[0,1]$,

$$|V_\beta(P_1)-V_\beta(P_2)|\le \frac{C|P_1-P_2|}{1-\beta(1-\pi)}.$$

The mission goal is both clauses of Theorem 3.4. The always-produce rule is optimal from every initial belief exactly at and above the threshold

$$R\ge\frac{C}{1-\beta(1-\pi)}.$$

Below that threshold, revision is the unique minimizing action for beliefs sufficiently near $1$ from the left Ross 1971, pp. 591–592.

Significance

The theorem gives a parameter test for omitting both inspection and revision from an optimal policy in this model. Its second clause adds a local statement when that test fails: near certain deterioration, merely allowing revision as one optimal choice is insufficient; any optimal choice must revise. The sensitivity bounds quantify the effect of imperfect knowledge of the state and supply continuity of the value function used in the paper's treatment of that neighborhood Ross 1971, Theorem 3.4 and Corollary 3.6.

Ross proved these results in 1971. This mission asks for machine-checked proofs of the paper's exact statements in a concrete two-state discounted model. The reusable formal objects are the belief update, the three-action Bellman operator, finite-horizon values, and the always-produce cost series. The goal and milestones here are open formalization targets; their mathematical status as published theorems is distinct from their proof status in Lean.

Difficulty

The cost of always producing can be computed explicitly, but equality with the optimal value is a global assertion about all beliefs and all three available actions. A comparison at one belief does not certify optimality everywhere. The reverse implication also has to recover a parameter inequality from optimality of a policy, rather than from its immediate cost alone. The strict conclusion near $P=1$ requires control of the value as the belief varies; pointwise action comparison at $P=1$ does not itself establish an interval Ross 1971, pp. 591–592.

Formalization scope

The Lean model uses real parameters and a real belief restricted to $[0,1]$. It has three explicit actions and the exact right-hand sides of equation (3). Its value is the limit of iteration from $V^0=0$, so $V^1=\min\{CP,I,R\}$ matches the paper. Convergence, boundedness, and Bellman uniqueness are stated as a milestone. The always-produce cost is the infinite series of actual stage costs, with its closed form reserved for a separate milestone. Consequently, defining the cost by equation (5) cannot make that milestone true by definition.

The discounted-optimality claim for $R^0$ means $\psi(P)=V_\beta(P)$ for every $P\in[0,1]$. The phrase “every optimal policy revises” is represented by revision being strictly cheaper in the Bellman equation than both other actions; this expresses a unique minimizing action for a stationary decision at that belief. “Near $1$” means a one-sided neighborhood within $[0,1]$. The second inequality in Corollary 3.6 is stated only when $\pi>0$, because division by $\pi=0$ has a default value in Lean. The first inequality and Theorem 3.4 retain the $\pi=0$ case.

The development needs real series, limits, finite-horizon recursion, elementary inequalities, and bounded fixed-point reasoning. Proofs of the model-specific Bellman equation, cost identity, exact sensitivity bounds, and Theorem 3.4 are welcome. General tools for discounted Bellman operators or real-series identities would also be useful beyond this mission. No policy class is smuggled in as an arbitrary hypothesis: the value and the cost of $R^0$ are computed from the model data.

Selected references

• Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587.

Motivation

The contact process is the basic model of an infection spreading on a graph: infected sites recover at a constant rate, and healthy sites are infected at a rate that depends on how many of their neighbours are infected. T. E. Harris introduced it in Contact Interactions on a Lattice (Ann. Probab. 2, 1974, doi:10.1214/aop/1176996493), and it became one of the central examples of the theory of interacting particle systems (Liggett, Interacting Particle Systems, 1985, Ch. VI; Liggett, Stochastic Interacting Systems, 1999, Part I). Its questions are those of epidemiology and population dynamics on a spatial grid: does a finite infection die out, and how large does it get on the way?

Harris's paper gives the first rigorous subcritical bounds. Section 7 treats two quantities for a process started from a finite set: the probability $p_\infty(\xi)$ of surviving forever, and the expected size $m_t(\xi)$ at time $t$. This mission formalizes the second, Theorem 7.6: under an explicit condition on the rates, the expected size is integrable in time. The companion mission (Contact Interactions on a Lattice I) formalizes Theorem 7.1, extinction under the same condition.

A short timeline. Harris (1974) defined the process, proved monotonicity, subadditivity and submodularity by coupling, and gave the bounds of §7 and a survival result for large rates (§9). Holley and Liggett (Ann. Probab. 3, 1975) developed duality for such systems. Holley and Liggett's paper also proves, for a discrete-time branching process with interference, the analogue $P_F(A_n\ne\varnothing)\le E_F|A_n|\le\lambda^n|F|$ of the size bounds studied here; it is a different process, related but not reused.

Setting

Fix $d \ge 1$ and the lattice $Z_d$ of integer points $x = (x^1, \dots, x^d)$. Sites $x, y$ are neighbours, $x \sim y$, if $\sum_i |x^i - y^i| = 1$; $N_x$ is the set of the $2d$ neighbours of $x$. A configuration is a finite set $\xi \subset Z_d$ (the set $\Xi_0$); $|\xi|$ is its number of points, $\xi(N_x)$ is the number of neighbours of $x$ in $\xi$, and $x \sim \xi$ means $x \notin \xi$ and $x$ has a neighbour in $\xi$.

The parameters are a death rate $\mu \ge 0$ and birth rates $\lambda_0 = 0, \lambda_1, \dots, \lambda_{2d} \ge 0$. The contact process is the continuous-time Markov chain on finite configurations that, from $\xi$, removes a point $x \in \xi$ at rate $\mu$ and adds a site $x \sim \xi$ at rate $\lambda_{\xi(N_x)}$. Its total jump rate is

$$q_\xi = \mu|\xi| + \sum_{x \sim \xi} \lambda_{\xi(N_x)} .$$

The empty configuration is absorbing. $P_t(\xi, \eta)$ is its transition function, $r(\xi,\eta) = q_{\xi\eta}/q_\xi$ the transition matrix of its jump chain, and

$$m_t(\xi) = \mathscr E_\xi\, |\xi_t| = \sum_{\eta} P_t(\xi, \eta)\, |\eta|$$

the expected size at time $t$. In the Lean development these are trans μ lam t ξ η, jump μ lam ξ η and meanSize μ lam t ξ, where lam k is $\lambda_k$.

Formalization targets

Goal: Theorem 7.6 (p. 982)

If $\mu > 0$ and

$$\frac{\lambda_k}{\mu} < \frac{k}{2d-1}, \qquad k = 1, \dots, 2d,$$

then for every finite $\xi$,

$$\int_0^\infty m_t(\xi)\, dt < \infty .$$

Milestones

In the paper's proof order:

1. Lemma 4.7: $m_t(\xi) \le |\xi|\, e^{(2d\Lambda - \mu)t}$ with $\Lambda = \max_i \lambda_i$.
2. Lemma 5.8, its $m_t$ half: $\lambda_k \le \min_{j \ge k} \lambda'_j$ implies $m_t \le m'_t$.
3. The change of time scale: multiplying all rates by $c$ replaces $m_t$ by $m_{ct}$.
4. Remark 5.5, three times. $m_t$ is increasing in $\xi$ when $\lambda_k \uparrow$; it is subadditive when also $\lambda_k / k \downarrow$; and it is submodular when $\lambda$ is concave and non-decreasing.
5. The first-jump equation (7.7) for a pair of neighbours, with $K = 2 + (4d-2)\lambda$.
6. The bound after (7.11): $M_2(T) - M_1(T) \le 1/(1 - (2d-1)\lambda)$.
7. Lemma 7.5: if $\int_0^\infty m_t(\{x\})\,dt = \infty$, then $\int_0^\infty (m_t(\xi) - m_t(\{x\}))\,dt = \infty$ for $|\xi| \ge 2$.

After the goal come two consequences: Lemma 4.11, $m_{t+h}(\xi) \ge e^{-\mu h} m_t(\xi)$, and Remark 7.12, $m_t(\xi) \to 0$.

Significance

The theorem says that the total expected infection time, summed over all sites, is finite. That is stronger than extinction (Theorem 7.1), and it quantifies how fast the process dies out on average. With Lemma 4.11 it gives $m_t(\xi) \to 0$. Bounds on the expected size are the standard route to subcritical estimates for spatial epidemics and branching systems with interference. The milestones are also the paper's general tools. Monotonicity, subadditivity and submodularity of $m_t$, comparison of rate sequences, and time scaling hold for every contact process and are reusable beyond this mission.

The theorem has been known since 1974, and the formalization of the contact process is new work: the platform has no machine-checked development of an interacting particle system on $Z_d$, nor of a continuous-time chain with unbounded rates. The mission produces a formal model of the contact process from a finite set, a Lean proof of the subcritical bound, and the coupling inequalities (stated here for $m_t$) that any further work on the process will need.

Difficulty

The obvious argument fails. One would bound the growth rate of $|\xi_t|$ by its worst case: a site is born at rate at most $\lambda_k$ for each of at most $2d|\xi|$ boundary sites. This gives only Lemma 4.7, an exponential bound whose exponent $2d\Lambda - \mu$ is positive in most of the regime of the theorem. The factor $2d - 1$ instead of $2d$ comes from correlations: a newly born site always has an occupied neighbour, so it adds at most $2d - 1$ new boundary sites. Capturing this needs the comparison between a single site and a pair of neighbours in (7.7)–(7.11), together with submodularity, which is a coupling statement about the whole process. Lemma 7.5 then has to turn a bound on the difference $M_2 - M_1$ into a bound on $M_1$, and the paper omits its proof.

In the formal setting the chain has unbounded rates (since $q_\xi$ grows with $|\xi|$), so its transition function is not a matrix exponential. Uniformization does not apply either, and every statement goes through the minimal solution of the backward equations.

Formalization scope

• The chain model. The process is the countable-state chain on finite configurations that the paper itself uses from §4 on. Theorems 4.1 and 4.3 show that the infinite-volume process started in $\Xi_0$ is this chain. No process on infinite configurations and no probability space is constructed, and $P_\xi$, $\mathscr E_\xi$ enter only through $P_t$.
• The transition function. $P_t$ is the minimal transition function of the rates (4.4)–(4.5), $P_t = \sup_n P^{(n)}_t$, where $P^{(n)}_t$ is defined by Feller's backward recursion over at most $n$ jumps.
• Finite initial sets. Statements the paper makes for all $\xi \in \Xi$ (Lemmas 4.11 and 5.8, Remark 5.5) are drafted for finite $\xi$.
• Values. $P_t$, $p_t$ and $m_t$ take values in $[0, \infty]$. Integrals of $m_t$ are Lebesgue integrals of $[0,\infty]$-valued functions.
• Lattice. Sites are Fin d → ℤ with the $\ell^1$ adjacency of the paper.
• Standing hypotheses. Every statement carries $d \ge 1$, $\mu \ge 0$, $\lambda_0 = 0$ and $\lambda_k \ge 0$ for $k \le 2d$. Conditions on $\lambda$ range over $k \le 2d$ only, since $\lambda_k$ for $k > 2d$ never enters the model. The goal adds $\mu > 0$, which the paper's ratio $\lambda_k/\mu$ presupposes.

Several trivializing formalizations are excluded:

• $m_t$ is not a real tsum, which would be $0$ when the series diverges;
• the integral is not a real Bochner integral, which would be $0$ for a non-integrable function;
• the rate condition does not range over all $k \in \mathbb N$;
• $\mu > 0$ is not left implicit: in Lean $\lambda_k / 0 = 0$, and at $\mu = 0$ the conclusion is false;
• the goal is not stated for singletons only.

A complete development needs the backward equation and non-explosion for $P_t$ (Theorem 4.3, formalized in the companion mission), Fubini–Tonelli for $\sum$ and $\int$ in $[0,\infty]$, and couplings of contact processes. The couplings are the paper's auxiliary multi-type processes (§§5–6), or an equivalent argument on the generator. Contributions are welcome at every level. The coupling lemmas and the backward and forward equations for minimal chains are the parts most reusable beyond this mission.

Selected references

• T. E. Harris, Contact interactions on a lattice, Ann. Probab. 2(6), 969–988, 1974. https://doi.org/10.1214/aop/1176996493
• R. Holley, T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, Ann. Probab. 3(4), 643–663, 1975. https://doi.org/10.1214/aop/1176996306
• T. M. Liggett, Interacting Particle Systems, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
• W. Feller, On the integro-differential equations of purely discontinuous Markoff processes, Trans. Amer. Math. Soc. 48, 488–515, 1940. https://doi.org/10.1090/S0002-9947-1940-0002697-3
• J. R. Norris, Markov Chains, Cambridge University Press, 1997, §2.8. https://doi.org/10.1017/CBO9780511810633