Motivation

Howard's finite Markovian decision process (MDP) models a controller who, at each instant, observes the state of a system, chooses a decision, collects a reward and moves to a random next state with known transition probabilities. Howard's policy-iteration algorithm computes an optimal policy, and the model has been applied to inventory control, equipment replacement, quality control and marketing. Its weak point is the requirement that every transition probability be known exactly: in applications these numbers are estimated and are hard to measure.

Satia and Lave (Operations Research 21(3), 1973) relax this requirement. In their game-theoretic formulation, the controller knows only a set of admissible probability rows for every state–decision pair, and nature chooses the rows adversarially. This is the model now called a robust MDP with (s,a)-rectangular uncertainty, studied later by Iyengar (Math. Oper. Res. 2005) and Nilim and El Ghaoui (Oper. Res. 2005), who reprove and extend the dynamic-programming results for it. The paper gives a policy-iteration algorithm for the max-min criterion and proves that it terminates at an optimal policy. This mission formalizes that part of the paper (pp. 728–732).

Timeline:

• 1953: Shapley introduces stochastic games (PNAS 39).
• 1960: Howard, Dynamic Programming and Markov Processes, policy iteration for known transitions.
• 1973: Satia and Lave, max-min and max-max policy iteration for uncertain transitions (dynamic-programming equations and optimality of pure stationary policies cited from Satia's 1968 Stanford thesis).
• 2005: Iyengar; Nilim and El Ghaoui, robust dynamic programming under rectangular uncertainty.

Setting

There are finitely many states $i$ and, in state $i$, a finite nonempty set $D_i$ of decisions $k$. A transition $i\to j$ under decision $k$ earns reward $r^k_{ij}$; rewards are discounted by $\beta$ with $0\le\beta<1$. For every pair $(i,k)$ there is a nonempty, closed, convex set $S_i^k$ of probability rows $p=(p_1,\dots,p_N)$, $p_j\ge0$, $\sum_j p_j=1$. Nature's choice is a matrix $P\in S$: one row $p_i^k\in S_i^k$ for every pair.

A pure stationary policy $A=(A_1,\dots,A_N)$ selects $A_i\in D_i$. Under $P$ its present value $v^A(P)$ is the unique solution of equations (5),

$$v_i^A=\sum_j p^{A_i}_{ij}\big(r^{A_i}_{ij}+\beta v_j^A\big).$$

Nature's minimum is $\underline v_i(A)=\inf_{P\in S}v_i^A(P)$, and the max-min return of criterion (2) is $\bar v_i=\max_A\underline v_i(A)$. A policy is max-min optimal if $\underline v(A)=\bar v$ in every state.

The algorithm alternates two routines. Phase 1 (nature's policy evaluation) fixes $A$, computes $v^A$ from the current rows, replaces each row at $A_i$ by a minimizer of $\sum_j p_j(r^{A_i}_{ij}+\beta v^A_j)$ over $S_i^{A_i}$ (6), and stops when the minima reproduce $v^A$. Phase 2 (policy improvement) chooses in each state a decision $B_i$ maximizing the test quantity (7),

$$t_i^k(v)=\min_{p\in S_i^k}\sum_j p_j\big(r^k_{ij}+\beta v_j\big),$$

at $v=\underline v(A)$, keeping $A_i$ on ties; if $B=A$ the algorithm terminates.

Formalization targets

Goal: Proposition 5 with Proposition 3

Along every run $A^0,A^1,\dots$ of Phase 2 steps,

$$\underline v(A^n)\le\underline v(A^{n+1})\ \ \forall n,\qquad \exists\,n<\#\{\text{policies}\}:\ A^{n+1}=A^n,\ \ \underline v(A^n)=\bar v,$$

and the terminal policy attains the solution of the equations (4) and is $\varepsilon$-optimal for every $\varepsilon>0$.

Milestones

• Eq. (5): the present-value equations have a unique solution.
• $[I-\beta P]^{-1}$ is nonnegative with diagonal at least 1 for stochastic $P$ (proof of Proposition 5).
• Proposition 1: equations (4), with randomized decisions and mixed choices of nature, have a unique solution, and it is the max-min return.
• Proposition 2: a pure stationary policy attains it.
• A non-final Phase 1 iteration lowers nature's value weakly everywhere and strictly somewhere (proof of Proposition 4).
• Proposition 4: Phase 1 comes within $\varepsilon$ of nature's optimum after finitely many iterations.
• Proposition 3: at termination no pure stationary policy is better.
• Each policy change strictly improves the max-min return (proof of Proposition 5).

Significance

The goal certifies a complete algorithm for the max-min problem: it computes a policy that is optimal against the worst admissible transition probabilities, in all states at once, in finitely many improvement steps. Propositions 1 and 2 show that the dynamic-programming equations (4) characterize the max-min value and that neither side gains from randomization. The known-transition case (every $S_i^k$ a single row) recovers Howard's policy iteration.

On the platform, Howard-type policy iteration for known transitions has been formalized (the Bertsekas Dynamic Programming and Optimal Control missions); nothing with uncertain transitions exists. The results of this paper are proved in the literature (Satia's thesis, and in greater generality by Iyengar and by Nilim and El Ghaoui); none has a machine-checked proof. This mission produces the first formal robust-MDP model and robust policy-iteration theorem on the platform.

Difficulty

The obvious argument copies Howard's improvement lemma. It fails at two points. First, the value of a policy is itself the result of an inner optimization by nature, so comparing two policies requires comparing two different worst-case transition matrices; the matrix $P^{*B}$ minimizing against $B$ is not the one minimizing against $A$. Second, the proof of Proposition 4 as printed shows only that nature's values decrease and converge; that the limit is nature's optimum, over a continuum of admissible rows, needs a separate argument. Finally, Proposition 1 involves randomized strategies and probability measures on the uncertainty sets, and reducing them to pure strategies is the content of Propositions 1 and 2, not a definitional convenience.

Formalization scope

States are a finite type S (nonemptiness is not needed: every statement is unchanged in meaning at $N=1$ and trivially true at $N=0$), decisions a family D : S → Type* of finite nonempty types. The model fixes these conventions and readings:

• $0\le\beta<1$ (not printed; every return is an infinite discounted sum) and nonempty $S_i^k$ (not printed; Phase 1 presupposes a feasible row) are added standing hypotheses; closedness and convexity are the paper's.
• The present value is $[I-\beta P^A]^{-1}$ applied to the one-step rewards; the Eq. (5) milestone proves it is the unique solution of (5).
• "min over $p_i^k\in S_i^k$" in (2) is an infimum over the nonempty type of admissible choices $P\in S$, bounded below; "max over all policies" is a maximum over pure stationary policies, with randomization handled in (4).
• In (4), $\tau$ ranges over probability vectors on $D_j$ and $\alpha$ over probability measures on row vectors with $\alpha(S_j^k)=1$; the missing integral sign and unmatched brace of the printed display are corrected.
• "Optimal" = equal to the max-min return in every state; "$\varepsilon$-optimal" = within $\pm\varepsilon$ in every state (p. 731); "$\varepsilon$-optimal for nature" = within $\varepsilon$ of nature's minimum.
• "Terminates" = Phase 2 returns the same policy; "a finite number of iterations" is stated with the explicit bound "fewer than the number of policies".
• Phase 1 is taken exact in Phase 2 (the proofs of Propositions 3 and 5 use exact minimizers); the Phase 1 stopping test is printed without $\Sigma$ and the sum is formalized.
• Retention rule: Phase 2 keeps $A_i$ when it is already a maximizer. It is not printed, but it is Howard's rule and Proposition 5 is false without it.
• Proposition 5's "$\varepsilon$-optimal … in a finite number of iterations" is formalized as exact termination at an optimal policy, which implies the printed claim for every $\varepsilon$.

Equation (4) must not be collapsed to $\max_k\min_{p\in S_j^k}$ in its definition: that would make Proposition 2 true by definition. Similarly, the Phase 2 relation always has a successor and algorithm runs exist from every policy, so the goal is not vacuous.

Needed infrastructure: Neumann series for $I-\beta P$ with stochastic $P$, monotonicity of policy evaluation, existence of minimizers of linear functions on compact subsets of the simplex, and the contraction argument for the robust Bellman operator. These are reusable for any robust or known-transition MDP development. Proofs of any milestone, alternative arguments for Propositions 1 and 2, and extensions to the max-max criterion are welcome.

Selected references

• J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• L. S. Shapley, Stochastic Games, PNAS 39(10), 1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2), 257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5), 780–798, 2005. https://doi.org/10.1287/opre.1050.0216

Motivation

Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.

The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link $j$ is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.

Setting

The links are $\mathcal{J} = \{1,\dots,J\}$, link $j$ carrying $C_j$ circuits. A route $r$ belongs to a set $\mathcal{R}$ of $R$ routes, and the link-route incidence matrix $A$ records how much of each link a route needs: a call on route $r$ requires $A_{jr}$ circuits from link $j$ and is lost if any link has fewer than $A_{jr}$ free. (The classical case is $A$ a $0$–$1$ matrix and $A_{jr}=1$ exactly when $j\in r$; from section 3.3 the book allows any non-negative integers.)

Calls requesting route $r$ arrive as a Poisson process of rate $\nu_r$, independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing $n_r$ for the number of calls in progress on route $r$, the process $n=(n_r)$ is Markov on

$$S(C)=\{n\in\mathbb{Z}_+^{R} : An\le C\},$$

and is called a loss network with fixed routing.

Write $E(\nu,C)$ for Erlang's formula, $E(\nu,C)=\dfrac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}$, published in mission I of this series. The Erlang fixed point equations are

$$E_j \;=\; E\!\left((1-E_j)^{-1}\sum_r A_{jr}\,\nu_r\prod_i (1-E_i)^{A_{ir}},\; C_j\right), \qquad j=1,\dots,J. \tag{3.7}$$

The factor $(1-E_j)^{-1}$ removes link $j$'s own thinning from the product, so in the $0$–$1$ case the argument is $\sum_{r\ni j}\nu_r\prod_{i\in r\setminus\{j\}}(1-E_i)$, the reduced load offered to link $j$.

Formalization targets

Goal — Theorem 3.20, existence and uniqueness of the Erlang fixed point

$$\exists!\,(E_1,\dots,E_J)\in[0,1]^J \text{ satisfying } (3.7).$$

The goal fixes no formula for $E$ and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube $[0,1]^J$; uniqueness is the substance.

Supporting levels

The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution $\pi(n)=G(C)\prod_r \nu_r^{n_r}/n_r!$ on $S(C)$; and the acceptance probability $1-L_r=G(C)/G(C-Ae_r)$. Then the optimization side: that $E(\nu,C)$ and the utilization $\nu(1-E(\nu,C))$ are strictly increasing in $\nu$, which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on $B$, equation (3.6).

Significance

The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by $\int_0^{y_j}U(z,C_j)\,dz$. That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector $B$ coming from the maximum-probability problem.

Formalizing it. Nothing here is open. What the mission produces is the loss network model in Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked statement of the object the reduced-load approximation computes. It is also where this series' earlier missions pay off: the uncapacitated network is literally the open migration process of mission II with $\lambda\equiv 0$, $\mu\equiv 1$, $\varphi_j(n)=n$, and the exact distribution (3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I published.

Difficulty

Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization $\nu\bigl(1-E(\nu,C)\bigr)$ is strictly increasing in $\nu$, which is itself a milestone here.

A second, formal difficulty: the equations involve $(1-E_j)^{-1}$, so a solution with $E_j=1$ would be meaningless. It is worth checking before starting that no such solution exists for $C_j\ge 1$, rather than assuming it.

Formalization scope

Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only $0$–$1$), capacities are natural numbers, and arrival rates are positive reals. The feasible set $S(C)$ is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.

Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route $r$ is $n_r$ and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; $G(C)$ is the reciprocal of the sum in the book's notation. Capacities are assumed at least $1$ in the goal: a link with no circuits blocks everything, $E(\nu,0)=1$ identically, and the factor $(1-E_j)^{-1}$ would then be undefined rather than merely large.

The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.

Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the $0$–$1$ equations (3.1) of section 3.2; the utilization function $U(y,C)$ and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 3 (pp. 49–82); Lemma 3.4, equation (3.3), Theorems 3.10 and 3.20, equations (3.1), (3.5)–(3.9). DOI 10.1017/cbo9781139565363
• F. P. Kelly, Loss networks, Annals of Applied Probability 1 (1991), 319–378. DOI 10.1214/aoap/1177005872
• F. P. Kelly, Blocking probabilities in large circuit-switched networks, Advances in Applied Probability 18 (1986), 473–505. DOI 10.2307/1427303
• R. B. Cooper and S. Katz, Analysis of alternate routing networks with account taken of the nonrandomness of overflow traffic, Bell Telephone Laboratories memorandum, 1964.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1 on truncation.

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