Markov Chain

Motivation

Networks of queues model computer systems, communication networks and manufacturing lines: customers (jobs, packets, parts) move between service centers, wait, receive service and move on. Their equilibrium behaviour determines throughputs, utilizations and response times, and for most networks it can only be computed by solving the full balance equations of a continuous-time Markov chain whose state space grows combinatorially with the number of centers and customers. A product-form network is one whose equilibrium distribution factorizes over the centers; for such networks performance measures can be computed exactly by efficient algorithms (convolution, mean value analysis), and this is the basis of much of classical computer-performance modelling.

Timeline of the main product-form results:

• 1957–1963, Jackson (Oper. Res. 5, 1957; Manag. Sci. 10, 1963): open networks of exponential FCFS queues, one customer class, Poisson arrivals.
• 1967, Gordon and Newell (Oper. Res. 15): the closed single-class exponential case.
• 1975, Baskett, Chandy, Muntz and Palacios (J. ACM 22): several customer classes with class switching, four service disciplines (FCFS, processor sharing, infinite server, preemptive-resume LCFS), service times with rational Laplace transforms at the last three, and open, closed or mixed networks with state-dependent Poisson arrivals. This is the BCMP theorem, the subject of this mission.
• 1975–1979, Kelly (J. Appl. Prob. 12, 1975; Reversibility and Stochastic Networks, Wiley 1979): symmetric queues and quasi-reversibility, a general framework containing the BCMP disciplines.

Setting

A network has $N$ service centers and $R$ customer classes. A class-$r$ customer finishing service at center $i$ next requires center $j$ in class $s$ with probability $p_{i,r;j,s}$ and leaves the network with probability $1-\sum_{j,s}p_{i,r;j,s}$. The pairs $(i,r)$ are partitioned into subchains $E_1,\dots,E_m$ that routing never leaves. Each center has one of four types:

1. FCFS, with an exponential service time of rate $\mu_i$ common to all classes;
2. a single processor-sharing server (each of $n$ customers is served at rate $1/n$);
3. an infinite-server center;
4. a single preemptive-resume LCFS server.

At types 2–4 the class-$r$ service time is Coxian: $u_{ir}\ge1$ exponential stages of rates $\mu_{irl}$, and after stage $l$ the customer continues with probability $a_{irl}$ or finishes with probability $b_{irl}=1-a_{irl}$. The state $S=(x_1,\dots,x_N)$ records the FCFS order of classes at type 1, the number $m_{irl}$ of class-$r$ customers in stage $l$ at types 2 and 3, and the LCFS order of (class, stage) pairs at type 4. External arrivals are Poisson, either with rate $\lambda(M(S))$ depending on the total population $M(S)$ (process A) or with one stream per subchain of rate $\lambda_k(M(S/E_k))$ (process B); an arrival joins center $j$ in class $s$ with probability $q_{js}$. A subchain with $q\equiv0$ is closed and keeps a fixed population $K_k$.

With relative arrival rates $e_{ir}\ge0$ solving the traffic equations $\sum_{(i,r)}e_{ir}p_{i,r;j,s}+q_{js}=e_{js}$ and $A_{irl}=\prod_{j<l}a_{irj}$ (the probability of reaching stage $l$, stages numbered from 0), the paper defines $f_i(x_i)$ per center type and a factor $d(S)$ from the arrival rates.

Formalization targets

Goal: the BCMP theorem (§3.2, pp. 253–254)

$$\pi(S)=d(S)\,f_1(x_1)\,f_2(x_2)\cdots f_N(x_N)$$

satisfies the global balance equations of the network, and, under the paper's assumption that the equilibrium distribution is unique, every equilibrium distribution equals $\pi/Z$ whenever $Z=\sum_S\pi(S)$ is finite and positive. The goal covers all four center types, open, closed and mixed networks, and both arrival processes.

Milestones

• §3.1 (p. 252): independent balance implies global balance.
• §3.2 (p. 254): the product form satisfies the independent balance equations.
• §4.1 (p. 254): the aggregate-state probabilities are $C\,d(S)\,g_1(y_1)\cdots g_N(y_N)$.

A further supporting item, also from §4.1 (p. 254), states that summing $f_i$ over local states with fixed class counts gives $g_i$. So $g_i$ depends on the service times only through their means $1/\mu_{ir}=\sum_lA_{irl}/\mu_{irl}$.

Significance

The theorem places the four disciplines, class switching and mixed open/closed populations under one formula. Its corollary in §4.1, that aggregate probabilities depend on service time distributions only through their means (insensitivity), is what makes the model usable with measured mean service times, and it underlies the convolution and mean value analysis algorithms for normalizing constants.

The result is classical and proved on paper. As far as the platform's catalogue shows, it is not formalized: the platform has Kelly's single-class migration process with exponential service, a special case. A machine-checked BCMP theorem would provide a verified multiclass queueing-network model (states, event-driven transition rates, balance equations) on which later results can build: mean value analysis, the state-dependent rates of §5, and the open-network marginals of §4.2.

The printed statement contains an error. The paper defines $A_{irl}=\prod_{j=1}^{l}a_{irj}$ (p. 253). With the branching of its Figs. 1 and 3, this product includes the branch out of stage $l$. For exponential service ($u_{ir}=1$) it gives $A_{ir1}=a_{ir1}=0$, so every $f_i$ of a type 2–4 center with a customer present vanishes, and a closed network of such centers would have no normalizable solution. The mission states the corrected theorem with $A_{irl}=\prod_{j<l}a_{irj}$, which the mean-service-time identity of §4.1 also requires. The type-2 factor $1/m_{ikl}!$ is read as $1/m_{irl}!$.

Difficulty

The algebra of the paper's proof is local: each independent balance equation reduces to the traffic equations. The difficulty is in making that statement precise for a real state space. The independent balance equations need a consistent labelling of each moving customer by the "stage" it leaves and enters. That labelling has to cover FCFS centers, where per-class labels are inconsistent (p. 253), the outside world of each open subchain, and LCFS preemption. Every in-flow into a state is a sum over predecessor states, and those states differ by list operations (appending at an FCFS tail, pushing on an LCFS head) or by stage-count updates. The factorials in the processor-sharing and infinite-server factors, and the telescoping identity $\sum_lA_{irl}b_{irl}=1$ for departures, must line up exactly with the rates. The obvious shortcut is to check global balance directly for a single class with exponential service. That covers neither class switching, nor Coxian stages, nor mixed networks.

Formalization scope

Centers are Fin N, classes Fin R and subchains Fin m. The class-$r$ stages at center $i$ are Fin (u i r) with u i r : ℕ+, numbered from 0. A local state is an inductive type with three shapes (FCFS list, stage-count array, LCFS list of (class, stage) pairs). The state space is the subtype of configurations whose shapes match the center types and whose closed subchains hold their fixed populations. Transition rates are the sums of the rates of explicit events (arrivals, FCFS completions, stage moves and completions, LCFS moves and completions). Global balance uses tsum; every state has finitely many successors and predecessors with nonzero rate, so these sums are finite. The standing assumptions (substochastic routing closed on subchains, closed subchains with no arrivals and no departures, positive rates, continuation probabilities in $[0,1]$ vanishing at the last stage) are collected in Network.IsValid. Irreducibility of subchains is not assumed, and any nonnegative solution of the traffic equations is allowed. Under process B the product in $d(S)$ runs over open subchains only. Uniqueness of the equilibrium is a hypothesis, as in the paper. The type-1 rate is constant, and the state-dependent rates of Condition 1 and §5 are not covered.

The following formalizations would trivialize the mission and are ruled out: stating only global balance of $\pi$ (satisfied by $\pi\equiv0$), quantifying over arbitrary rate functions instead of the rates built from the network data, and restricting the goal to exponential service or to a single class.

Needed infrastructure: finite-support tsum manipulations, multinomial identities for the §4.1 sums over orderings and stage assignments, and bookkeeping for list and array updates. The model and the balance-equation layer can be reused for later queueing missions. Contributions are welcome on each milestone, on the per-center-type pieces of the independent balance check, and on helper lemmas about the event system.

Selected references

• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2):248–260, 1975. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4):518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• J. R. Jackson, Jobshop-like Queueing Systems, Management Science 10(1):131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2):254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. http://www.statslab.cam.ac.uk/~frank/rsn.html
• D. R. Cox, A Use of Complex Probabilities in the Theory of Stochastic Processes, Proc. Cambridge Phil. Soc. 51:313–319, 1955. https://doi.org/10.1017/S0305004100030231

When the supplier is the risk

Every model in the earlier chapters of this series treats demand as the uncertain quantity and supply as given. Chapter 9 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reverses the roles: demand is deterministic and the supplier fails. A disruption is a binary event, modeled as a two-state Markov process between up and down periods, during which nothing can be ordered. The chapter's thesis, from Snyder and Shen (2006), is that supply uncertainty is a mirror image of demand uncertainty: the optimal base-stock level has the same critical-fractile form as the newsvendor solution but with the fractile taken over the disruption-length distribution (Tomlin 2006), and consolidation, which pools demand risk, now does nothing to expected cost and multiplies its variance, the risk-diversification effect of Schmitt, Sun, Snyder and Shen (2015). The chapter closes with the reliable fixed-charge location problem of Snyder and Daskin (2005). This mission formalizes the chapter's theorems on disruptions, with the risk-diversification theorem as its goal.

Setting

A supplier that is up is disrupted next period with probability $\alpha$; one that is down recovers with probability $\beta$. The disruption chain records $0$ when the supplier is up and $n \ge 1$ in the $n$-th consecutive period of a disruption; its stationary distribution is $\pi_0 = \beta/(\alpha+\beta)$ and $\pi_n = \frac{\alpha\beta}{\alpha+\beta}(1-\beta)^{n-1}$ (disruptionPmf), with distribution function $F(n) = \sum_{i \le n}\pi_i$ (disruptionCdf).

A single location faces demand $d$ per period, pays $h$ per unit held and $p$ per unit backordered per period, and follows a base-stock policy: it orders up to $S$ in every up period and nothing in down periods. In the $n$-th period of a disruption it has $S - (n+1)d$ units on hand or backordered, so its cost is $\hat g(S, n) = h[S-(n+1)d]^+ + p[(n+1)d - S]^+$ (periodCost), and the expected cost per period is $g(S) = \sum_n \pi_n \hat g(S, n)$ (meanCost), with variance $V(S)$ over the disruption state (varCost). The critical fractile $\gamma = p/(p+h)$ and $F^{-1}(\gamma)$, the smallest $n$ with $F(n) \ge \gamma$, determine the optimal level.

In the reliable fixed-charge location problem (RFLP), sites fail independently with probability $q$ and each customer is assigned to a chain of facilities: its level-$r$ facility serves it when the $r$ closer facilities are disrupted, until it is assigned to an emergency facility $u$ that never fails and charges the penalty $\theta_i$. The objective (9.61) is fixed cost plus expected transportation cost, with coefficients $\psi_{ijr} = h_i c_{ij} q^r (1-q)$ (rflpPsi, rflpCost) under the constraints (9.62)-(9.67) (RFLPFeasible).

Formalization targets

Goal: Theorem 9.9

For $N$ identical locations and the centralized location formed by merging them (demand $Nd$):

$$S^*_C = NS^*, \qquad g^*_C = g^*_D = Ng^*, \qquad V^*_C = N V^*_D = N^2 V^*,$$

that is, an optimal single-location level $S$ scales to the optimal centralized level $NS$, the centralized expected cost at $NS$ is $N$ times the single-location cost, and its variance is $N^2$ times the single-location variance. This is risk_diversification.

Supporting targets

Lemma 9.2, the stationary distribution and distribution function of the disruption chain; Lemma 9.4, that the optimal base-stock level is a multiple of $d$; Theorem 9.5, $S^* = d + dF^{-1}(p/(p+h))$, as the least minimizer of $g$; and Theorem 9.10, that in every optimal RFLP solution consecutive backup assignments are ordered by cost. Theorem 9.3, the optimality of base-stock policies, is cited by the book to Song and Zipkin without a model of the policy space and is not a target; Proposition 9.1 and the multisupplier results of Sect. 9.4 are left for a later mission, as discussed below.

Significance

Theorem 9.5 is the supply-side newsvendor formula: it says exactly how much inventory buys protection against disruptions of a given length, and it underlies the disruption models used in practice for raw-material buffers. Theorem 9.9 is the chapter's central insight and the reason supply and demand uncertainty call for opposite strategies: pooling reduces expected cost under demand uncertainty but only redistributes risk under supply uncertainty, concentrating it. Its three identities are what a risk-averse planner needs to compare the two designs by a mean-variance criterion. Theorem 9.10 is what lets the RFLP be formulated without ordering constraints and solved by Lagrangian relaxation like the UFLP.

None of these results has a machine-checked proof. The book proves Theorem 9.5 and the identities behind Theorem 9.9, sketches Lemma 9.4, and leaves Lemma 9.2 and Theorem 9.10 as exercises. The formal treatment of the piecewise-linear cost $g$ and its finite differences is reusable for the yield-uncertainty and multi-supplier models of the same chapter.

Difficulty

The cost $g$ is an infinite series whose terms grow linearly in $n$ against a geometric weight, so every statement about it begins with summability, and the finite-difference identity $\Delta g(S) = d[(h+p)F(S/d - 1) - p]$ requires exchanging a difference with a sum. Theorem 9.5 then needs the convexity and piecewise linearity of $g$ to pass from a sign condition on slopes at multiples of $d$ to a global minimum over all real $S$, and the identification of the least minimizer needs the slopes to be strictly negative below $S^*$. The obvious idea, treating the problem as a discrete newsvendor over multiples of $d$, is only half of the argument: it does not by itself exclude non-multiple minimizers, which is what Lemma 9.4 asserts.

Lemma 9.2 is elementary but the stationary equations involve a series over all down states, and the proof must establish summability before manipulating it. Theorem 9.9's scaling identities are termwise, but the optimality transfer in part 1 requires the scaling to preserve minimizers, which follows from the cost identity holding for every $S$.

Theorem 9.10 is an exchange argument on a binary program with layered constraints. The delicate case is the emergency facility: swapping it into a lower level is infeasible, and the correct move is to promote it and drop the later assignment, which changes the constraints for every higher level; the argument must show feasibility of the modified solution level by level.

Formalization scope

The disruption distribution is given by Lemma 9.2's formula rather than defined as the stationary distribution, and Lemma 9.2 shows it satisfies the stationary equations; the theorems assume $0 < \alpha \le 1$ and $0 < \beta \le 1$, under which every series is a geometric series times a polynomial and is summable. The quantity $F^{-1}(\gamma)$ enters Theorem 9.5 as a natural number $k$ characterized by $F(k) \ge \gamma$ and $F(n) < \gamma$ for $n < k$, which exists since $F(n) \to 1 > \gamma$; the conclusion asserts both optimality and leastness of $d + dk$ among all real levels.

Theorem 9.9 is stated as the scaling of the single-location functions; the decentralized totals $Ng^*$ and $NV^*$ are the mean and variance of a sum of $N$ independent copies, which the book asserts rather than derives, and are not modeled separately. In the RFLP, levels are indexed by Fin m, the emergency facility is a designated index $u$ whose data satisfy the book's conventions through the hypotheses, and demands are positive with $0 < q < 1$, both needed: with $q = 0$ or $h_i = 0$ backup assignments are free and any order is optimal.

The EOQ with disruptions (Proposition 9.1) is a renewal-reward derivation without a formal model of the renewal process in the book, and the multisupplier newsvendor of Sect. 9.4 (Lemma 9.6, Theorems 9.7 and 9.8) rests on differentiability conditions the book defers to Dada et al. and on a lemma it leaves as an exercise; both are natural extensions on the same definitions rather than targets here.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 9. https://doi.org/10.1002/9781119584445
• B. Tomlin, On the value of mitigation and contingency strategies for managing supply chain disruption risks, Management Science 52(5), 2006. https://doi.org/10.1287/mnsc.1060.0515
• A. J. Schmitt, S. A. Sun, L. V. Snyder and Z.-J. M. Shen, Centralization versus decentralization: risk pooling, risk diversification, and supply chain disruptions, Omega 52, 2015. https://doi.org/10.1016/j.omega.2014.10.010
• L. V. Snyder and M. S. Daskin, Reliability models for facility location: the expected failure cost case, Transportation Science 39(3), 2005. https://doi.org/10.1287/trsc.1040.0107
• L. V. Snyder and Z.-J. M. Shen, Supply and demand uncertainty in multi-echelon supply chains, working paper, 2006. https://doi.org/10.1287/msom.1080.0224

Motivation

A Markov process is reversible when, in equilibrium, transitions from $x$ to $y$ occur at the same average rate as transitions from $y$ to $x$. Algebraically this is the detailed balance condition $\pi(x)q(x,y)=\pi(y)q(y,x)$, and it is the single most useful structural property a network process can have: it replaces a global linear system by one equation per pair of states, and it hands you the equilibrium measure as a product of rate ratios rather than as the solution of anything.

The catch is that detailed balance mentions $\pi$, which is exactly what one is trying to find. Chapter 2 of Richard Serfozo's Introduction to Stochastic Networks (Springer, 1999) removes the circularity. Kolmogorov's criterion characterizes reversibility by a condition on the rates alone: around every closed path, the product of the forward rates equals the product of the backward rates. And the proof is constructive — once the criterion holds, the invariant measure is

$$\pi(x)=\prod_{i=1}^{n}\frac{q(x_{i-1},x_i)}{q(x_i,x_{i-1})}$$

along any path from a fixed origin $x^0$ to $x$, the criterion being precisely what makes the answer independent of the path chosen.

Setting

$q(x,y)$ is a non-negative rate function on a state space $\mathbb E$, with the two-way communication property that $q(x,y)$ and $q(y,x)$ are positive together — a process failing this is visibly not reversible, since some transition would be possible but its reverse would not. A path $x_0,\dots,x_n$ is a sequence with $q(x_{i-1},x_i)>0$ throughout, and $q$ is assumed irreducible: every state is reachable from every other along a path. Write $\rho(x,y)=q(x,y)/q(y,x)$ for the rate ratio.

$q$ is reversible when some positive $\pi$ satisfies the detailed balance equations. Such a $\pi$ is automatically an invariant measure, the total balance equations being the sum of the detailed ones.

Formalization targets

Goal — Theorem 2.8, Kolmogorov's criterion and the canonical measure

Three statements are equivalent:

1. $q$ is reversible;
2. (Kolmogorov's criterion) for every closed sequence $x_0,\dots,x_n=x_0$,

$$\prod_{i=1}^{n}q(x_{i-1},x_i)=\prod_{i=1}^{n}q(x_i,x_{i-1});$$

3. for every path, $\prod_{i=1}^n\rho(x_{i-1},x_i)$ depends on the path only through its endpoints.

And when they hold, fixing any origin $x^0$ there is a positive $\pi$ with $\pi(x^0)=1$ satisfying detailed balance and given at every state by the product of ratios along any path from $x^0$.

Supporting levels

The canonical form (2.2), that $q$ is reversible with respect to $\pi$ exactly when $q(x,y)=\gamma(x,y)/\pi(x)$ for a symmetric non-negative $\gamma$; Example 2.1, the birth–death process with $\pi(x)=\prod_{n=1}^{x}\lambda(n-1)/\mu(n)$; Theorem 2.2, that a process whose communication graph is a tree is reversible; and Theorem 2.5, the time-reversal criterion, which identifies a stationary distribution from a candidate reversed rate function without mentioning reversibility at all.

Significance

The results themselves. Kolmogorov's criterion is the working test. It is how one checks that a birth–death process, a random walk on a tree, a reversible Jackson network or a Whittle network with reversible routing is reversible, and it is a finite check on cycles rather than a search for an unknown measure. The ratio form (iii) is what gets used in practice: it says the product of ratios along a path is a well-defined function of the endpoints, which is exactly what licenses defining $\pi$ by that product.

Theorem 2.2 is the structural special case with no computation at all — a tree has no cycles, so the criterion is vacuous and reversibility is automatic. Theorem 2.5 points in a different direction: it identifies a stationary distribution from a guess at the time-reversed rates, and it is the tool Serfozo uses later to prove the Whittle equilibrium theorem a second way and to establish that departure processes from networks are Poisson.

Formalizing them. Mathlib has no reversibility theory for Markov processes: no detailed balance, no Kolmogorov criterion, no time reversal of a rate function. It has SimpleGraph.IsTree, which the tree item uses, and nothing else that bears on this chapter. The whole apparatus is contributed here.

Difficulty

The goal is a genuine equivalence with a constructive core, and the three implications are of quite different character.

(i) $\Rightarrow$ (ii) is the easy one: multiply the detailed balance equations around the closed path and cancel the $\pi$'s, which is legitimate because the $\pi$ values are positive. Note the criterion is asserted for arbitrary closed sequences, not only for paths; the two-way property is what makes both sides vanish together when some rate is zero.

(ii) $\Leftrightarrow$ (iii) is a cycle-splicing argument: two paths with the same endpoints concatenate, one reversed, into a closed path, and the criterion says its forward and backward products agree, which is the equality of ratio products.

(ii) $\Rightarrow$ (i) is where the construction lives. Fix an origin $x^0$; irreducibility gives a path to every state; define $\pi$ by the ratio product; (iii) makes it well defined; and then detailed balance at an edge follows by extending a path by that edge. Serfozo's Remark 2.9 gives the same construction as a recursion over the sets $\mathbb E_n$ of states reachable in $n$ steps, which may be the easier route to organize.

The birth–death item is a telescoping recursion, $\pi(x+1)\mu(x+1)=\pi(x)\lambda(x)$, and the observation that the two families of detailed balance equations — for $y=x+1$ and for $y=x-1$ — are the same family. Theorem 2.2 is a cut argument: removing an edge of a tree splits the state space into two pieces joined by that edge alone, so the flow balance across the cut is the detailed balance equation for that edge. Theorem 2.5 is two lines of rearrangement once the sums are known to converge.

Formalization scope

The state space is an arbitrary type and $q$ is an arbitrary non-negative real rate function; nothing here needs a process, a measure space or even countability, because reversibility as Serfozo defines it "applies to any nonnegative rates or probabilities as an algebraic property, not necessarily associated with a stochastic process". The same statements therefore cover discrete-time chains with $q$ read as transition probabilities, which is what the book points out.

Paths are functions $\{0,\dots,n\}\to\mathbb E$ with positive consecutive rates. A path of length zero is a single state and its ratio product is the empty product $1$, which is consistent with $\pi(x^0)=1$.

Kolmogorov's criterion is stated for arbitrary closed sequences, exactly as the book states it, not only for closed paths. Under two-way communication the two readings agree — if one rate in the sequence vanishes then so does its reverse and both products are zero — but the book's form is the one that is directly checkable.

The canonical measure is not defined by a choice function. Instead the conclusion asserts the existence of a positive $\pi$ with $\pi(x^0)=1$ satisfying detailed balance and agreeing with the ratio product along every path from the origin. That is the content of (2.9) without needing to pick a path for each state.

Theorem 2.2 is stated for a finite state space. Serfozo assumes the process is ergodic, and the cut-flow argument then sums the balance equations over one side of the cut; on an infinite state space that summation needs an integrability condition that the book leaves implicit in "ergodic". Finiteness makes the rearrangement unconditional and the statement clearly true; the general case is listed under contributions.

Theorem 2.5 is stated as the conclusion that $\pi$ satisfies the balance equations, with explicit summability hypotheses for the three families of sums involved. That $\pi$ is the stationary distribution additionally requires it to be normalized and the process to be ergodic, neither of which is part of the algebraic content.

Contributions welcome beyond the listed items: Theorem 2.4, the characterization of reversibility by invariance of the finite-dimensional distributions under time reversal; Remark 2.9's recursive construction of the canonical measure; Theorem 2.22 on reversible network processes with batch movements; Theorem 2.31 and the partition-reversible processes of Sections 2.8 and 2.9; and the reversibility criteria for Jackson and Whittle networks in Examples 2.24 and 2.25.

Selected references

• Richard Serfozo, Introduction to Stochastic Networks, Applications of Mathematics 44, Springer, 1999, chapter 2, pp. 44–51; (2.1), (2.2), Example 2.1, Theorems 2.2, 2.5 and 2.8, Remark 2.9. DOI 10.1007/978-1-4612-1482-3
• A. N. Kolmogoroff, Zur Theorie der Markoffschen Ketten, Mathematische Annalen 112 (1936), 155–160. DOI 10.1007/BF01565412
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979; reissued Cambridge University Press, 2011, chapter 1. DOI 10.1017/CBO9781139226424
• P. Whittle, Systems in Stochastic Equilibrium, Wiley, 1986, chapters 1 and 10.

Motivation

A Markov chain forgets. Run it long enough and the distribution of its position stops depending on where it started — that is the intuition behind shuffling a deck, behind Markov chain Monte Carlo, behind PageRank, and behind the stationary analyses of every queueing model. Chapter 5 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) makes it a theorem, and identifies exactly what can go wrong.

Two things can. The chain may fail to reach parts of the state space, and the answer is irreducibility. Or it may reach them only on a lattice of times — a chain alternating between two halves of its state space never forgets whether the clock is even or odd — and the answer is aperiodicity. Theorem 5.6.6 says that is the complete list: an irreducible, aperiodic chain with a stationary distribution has $p^n(x,y)\to\pi(y)$, for every pair of states, whatever the starting point.

Setting

Let $S$ be a countable state space and $p(x,y)$ a transition probability: non-negative, with each row summing to one. The $n$-step transition probabilities are the matrix powers, $p^0(x,y)=\delta_{xy}$ and $p^{n+1}(x,y)=\sum_z p(x,z)p^n(z,y)$.

Hitting is described by the first-passage probabilities $f^n(x,y)=\mathbb{P}_x(T_y=n)$, given by $f^1(x,y)=p(x,y)$ and $f^{n+1}(x,y)=\sum_{z\ne y}p(x,z)f^n(z,y)$ — the chain moves once and then reaches $y$ for the first time, having avoided it meanwhile. Summing them gives

$$\rho_{xy}=\mathbb{P}_x(T_y<\infty)=\sum_{n\ge1}f^n(x,y),\qquad \mathbb{E}_yT_y=\sum_{n\ge1}n\,f^n(y,y).$$

A state is recurrent when $\rho_{yy}=1$, the chain is irreducible when $\rho_{xy}>0$ for all $x,y$, and a state $x$ is aperiodic when the greatest common divisor of $I_x=\{n\ge1:p^n(x,x)>0\}$ is $1$. A stationary distribution is a probability vector $\pi$ with $\sum_x\pi(x)p(x,y)=\pi(y)$.

Formalization targets

Goal — Theorem 5.6.6, the convergence theorem

$$p \text{ irreducible},\ \text{aperiodic},\ \text{with stationary distribution } \pi \quad\Longrightarrow\quad p^n(x,y)\longrightarrow\pi(y)\ \text{ for all } x,y .$$

The goal asserts pointwise convergence of the transition probabilities, not convergence in total variation and not a rate; those are strengthenings, and stating the weakest useful form is what keeps the theorem stable.

Supporting levels

Theorem 5.3.1, that a state is recurrent exactly when $\sum_n p^n(y,y)$ diverges — the bridge between the hitting picture and the matrix picture; Theorem 5.3.2, that recurrence is contagious; Theorem 5.5.10, that every state in the support of a stationary distribution is recurrent; and Theorem 5.5.11, that for an irreducible chain with a stationary distribution $\pi(x)=1/\mathbb{E}_xT_x$.

Significance

The result itself. Theorem 5.6.6 is what licenses reading a stationary distribution as a long-run frequency. Without it, $\pi$ is merely a fixed point of a linear map; with it, $\pi(y)$ is the limiting probability of being at $y$, from any start. Theorem 5.5.11 then gives the quantity a second, purely local meaning — $\pi(x)$ is the reciprocal of the mean return time to $x$ — which is the identity behind every renewal-reward computation in applied probability and behind the "expected time between visits" estimates that Monte Carlo methods rely on. The two necessary hypotheses are sharp: a periodic chain has $p^n(x,y)$ oscillating rather than converging, and Durrett's Theorem 5.7.2 gives the corrected statement in that case.

Formalizing it. Mathlib has no countable-state Markov chain theory. It has ProbabilityTheory.Kernel and an Irreducible notion for kernels, but nothing about recurrence, transience, first-passage decompositions, stationary measures or the convergence theorem, and nothing that specializes to a transition matrix on a countable set. The mission therefore contributes the whole apparatus of sections 5.3, 5.5 and 5.6 — the $n$-step and first-passage probabilities, $\rho_{xy}$, the mean return time, recurrence, irreducibility, aperiodicity and stationarity — together with the results that make it usable.

Difficulty

The usual proof of the goal is a coupling argument, and it is short but not obvious: run two independent copies of the chain, one from $x$ and one from $\pi$, on the product space $S\times S$ with transition probability $\bar p((x_1,x_2),(y_1,y_2))=p(x_1,y_1)p(x_2,y_2)$; aperiodicity plus irreducibility make the product chain irreducible, $\pi\times\pi$ is stationary for it, so it is recurrent and the two copies meet almost surely; after they meet they can be exchanged. Each step of that is a separate obligation, and the one that consumes aperiodicity is the irreducibility of the product chain — for a periodic chain it fails, which is exactly why the theorem does.

The number-theoretic ingredient is worth flagging: irreducibility of the product needs that $I_x=\{n:p^n(x,x)>0\}$, being closed under addition with $\gcd 1$, contains every sufficiently large integer. That is the numerical semigroup fact, and it is where aperiodicity is actually used.

Formalization scope

The state space is any countable type with decidable equality, and the transition probability is a plain function $S\times S\to\mathbb{R}$ constrained by IsTransition: non-negative entries, summable rows, rows summing to one. Sums over the state space are unconditional sums, so no finiteness is assumed anywhere.

The chain's law is not constructed. Every quantity here — $p^n$, $f^n$, $\rho_{xy}$, $\mathbb{E}_yT_y$ — is defined by an explicit recursion on the transition matrix, not as an expectation against a measure on path space. This is a deliberate choice: building the path measure is a substantial project of its own, and none of the statements in these sections need it. The recursions are the standard ones and they are the definitions the book's own computations use. The cost is that probabilistic statements about paths, such as Theorem 5.6.1 on the almost-sure limit of the visit counts $N_n(y)/n$, cannot be phrased in this language and are not part of the mission.

Conventions: $p^0$ is the identity matrix; $f^n$ vanishes at $n=0$; $\rho_{xy}$ and $\mathbb{E}_yT_y$ are unconditional sums over $n\ge1$, so an infinite mean return time appears as a non-summable series rather than as an extended real. Theorem 5.5.11 is therefore stated as summability together with $\pi(x)\cdot\mathbb{E}_xT_x=1$, which asserts finiteness of the mean return time rather than silently relying on a division convention.

Aperiodicity is "the only natural number dividing every element of $I_x$ is $1$", which is $\gcd I_x=1$ written without needing a gcd of a set; it is false when $I_x$ is empty, which is correct, since the period of such a state is undefined.

The goal is not vacuous: the hypotheses are satisfiable by any strictly positive transition matrix on a finite set.

Contributions welcome beyond the listed items: Theorem 5.3.3 on finite closed sets; the decomposition theorem 5.3.5; existence of a stationary measure from a recurrent state (5.5.7) and its uniqueness (5.5.9); the equivalence of positive recurrence and the existence of a stationary distribution (5.5.12); Theorem 5.7.2 for the periodic case; and the path-level results of section 5.6, which need the chain's law on path space.

Selected references

• Rick Durrett, Probability: Theory and Examples, Version 5 (11 January 2019), chapter 5, sections 5.3, 5.5 and 5.6 (pp. 281–320); Theorems 5.3.1, 5.3.2, 5.5.10, 5.5.11, 5.6.6. Published as the 5th edition, Cambridge University Press, 2019, DOI 10.1017/9781108591034
• J. R. Norris, Markov Chains, Cambridge University Press, 1998, chapter 1. DOI 10.1017/CBO9780511810633
• D. A. Levin and Y. Peres, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017. DOI 10.1090/mbk/107
• W. Doeblin, Exposé de la théorie des chaînes simples constantes de Markoff à un nombre fini d'états, Revue Mathématique de l'Union Interbalkanique 2 (1938), 77–105.

Motivation

A queueing network is a collection of service stations through which customers — jobs, packets, telephone calls, patients — move one at a time. The state of such a network is a vector of occupancy counts, one per station, and the number of states grows exponentially in the number of stations, so solving the equilibrium equations directly is hopeless for any network worth modelling. The product form is what rescues the subject: for a large and identifiable class of networks the equilibrium distribution factorizes into one term per station, as if the stations were independent, and a network of $J$ stations costs $J$ one-dimensional calculations instead of one exponentially large one.

Chapter 2 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) establishes this for migration processes, the Markov model in which individuals move between colonies one at a time at a rate that factorizes as $\lambda_{jk}\varphi_j(n_j)$: a part depending only on the two colonies and a part depending only on the occupancy of the source. The class covers single-server and $s$-server queues, infinite-server queues, and networks of them, open or closed.

Setting

There are $J$ colonies, and a state is a vector $n = (n_1,\dots,n_J)$ of non-negative integers, $n_j$ being the number of individuals in colony $j$. Three operators move one individual:

$$T^{jk}n \ \text{ moves one from } j \text{ to } k, \qquad T^{j\to}n \ \text{ removes one from } j, \qquad T^{\to k}n \ \text{ adds one to } k .$$

An open migration process is the Markov process on $\mathbb{Z}_+^J$ with transition rates

$$q(n, T^{jk}n)=\lambda_{jk}\varphi_j(n_j), \qquad q(n, T^{j\to}n)=\mu_j\varphi_j(n_j), \qquad q(n, T^{\to k}n)=\nu_k ,$$

where $\varphi_j(0)=0$: nothing leaves an empty colony. Immigration into colony $k$ is Poisson of rate $\nu_k$. Taking $\mu\equiv 0$ and $\nu\equiv 0$ and restricting to states of a fixed total $\sum_j n_j = N$ gives a closed migration process. Setting $\varphi_j(n)=\min(n,s)$ models an $s$-server queue at colony $j$; $\varphi_j(n)=n$ models individuals moving independently.

The traffic equations define $(\alpha_j)$ from the rates. In the open case they are

$$\alpha_j\Bigl(\mu_j+\sum_k \lambda_{jk}\Bigr) \;=\; \nu_j+\sum_k \alpha_k\lambda_{kj}, \qquad j = 1,\dots,J,$$

and in the closed case $\alpha_j\sum_k \lambda_{jk}=\sum_k \alpha_k\lambda_{kj}$ with $\alpha_j>0$ and $\sum_j\alpha_j=1$. Finally set

$$g_j=\sum_{n=0}^{\infty}\frac{\alpha_j^{\,n}}{\prod_{r=1}^{n}\varphi_j(r)} .$$

Formalization targets

Goal — Theorem 2.8, the product form of an open migration process

If $g_1,\dots,g_J<\infty$ then

$$\pi(n)=\prod_{j=1}^{J}\pi_j(n_j), \qquad \pi_j(m)=g_j^{-1}\,\frac{\alpha_j^{\,m}}{\prod_{r=1}^{m}\varphi_j(r)}$$

is an equilibrium distribution: it satisfies the equilibrium equations for the open migration rates, and it sums to one over $\mathbb{Z}_+^J$. Both halves are asserted, because the first alone is satisfied by every positive multiple of $\pi$ and the second is what makes the convergence hypothesis $g_j<\infty$ do work.

Supporting levels

The closed-network product form of Theorem 2.4; the two families of partial balance equations (2.3) and (2.4) that the proof reduces to; Theorem 2.9, that the time reversal of a stationary open migration process is again an open migration process with rates $\lambda'_{jk}=\alpha_k\lambda_{kj}/\alpha_j$, $\mu'_j=\nu_j/\alpha_j$ and $\nu'_k=\alpha_k\mu_k$; the single M/M/1 queue that the chapter starts from; the cycle identity (2.6) behind Little's law; and the traffic equations of Kendall's family-size process, an open migration process with infinitely many colonies.

Significance

The result itself. Theorem 2.8 says that at a fixed time the occupancies $n_1,\dots,n_J$ of an open migration network are independent, each distributed as if its colony were fed by a Poisson stream of rate $\alpha_j\lambda_j$ — even though the actual arrival stream into a colony is in general not Poisson, and the occupancies are emphatically not independent as processes. That gap between the one-time-marginal and the process is the reason the theorem is useful and the reason it is easy to misapply. Everything downstream in the book rests on it: the loss networks of Chapter 3 are the truncation of a product-form process to a capacity set, and the flow-level models of Chapter 8 ask when a product form survives a bandwidth-sharing policy. Theorem 2.9 supplies the reversibility argument from which Burke's theorem and the Poisson character of the exit streams follow.

Formalizing it. The mathematics is classical — Jackson (1957), Whittle (1968), Kelly (1979) — and none of it is open. What the mission produces is a machine-checked model of a queueing network: the migration operators, the rate matrix, the traffic equations and the product form, in a form later missions in this series import rather than restate. Mathlib has no queueing theory and no theory of continuous-time Markov chains on a countable state space, so this is the first such development. It builds on the DetailedBalance / FullBalance layer published in mission I.

Difficulty

An open migration process is not reversible — the detailed balance equations fail, as Figure 2.5 of the book shows with an arrival stream of geometrically sized bursts — so the method of Chapter 1 does not apply and the equilibrium equations must be met head on. The content of the proof is that they split: a separate balance holds for each colony $j$ (rate of individuals leaving colony $j$ equals rate arriving into it) and one more across the boundary with the outside world, and each of those is equivalent to a traffic equation. Finding that split is the step, and it is why the partial balance equations are milestones in their own right.

The formal obstacle is different and worth naming. The equilibrium equation at a state $n$ sums over the states that can jump into $n$, and the naive transcription $\sum_{j,k}\pi(T^{jk}n)q(T^{jk}n,n)$ silently assumes $T^{jk}n$ is a state, which fails when $n_j=0$. Over $\mathbb{Z}_+^J$ such a term must be dropped, and a formalization that keeps it — with $n_j-1$ read as truncated subtraction — states something false.

Formalization scope

The state space is Fin J → ℕ, a function from a finite index type of colonies to occupancy counts, with J finite; no irreducibility is assumed, since none of the statements below need it. Rates are real-valued and the whole rate matrix is a single function of two states, assembled as a sum of indicator terms over the possible transitions, so the equilibrium equations can be stated as the FullBalance predicate of mission I, with unconditional sums over the countable state space. This is what avoids the trap above: a sum over actual states never includes a would-be-negative one, and any spurious coincidence of operators at a boundary carries a $\varphi_j(0)=0$ factor and contributes nothing.

Conventions the development commits to: $\lambda_{jj}=0$, so a transfer is always between distinct colonies; $\varphi_j(0)=0$ and $\varphi_j(r)>0$ for $r\ge 1$; $\alpha_j>0$; and $g_j$ is asserted via HasSum, which states convergence and the value at once, rather than as an extended real that might be infinite. Occupancy vectors use truncated natural subtraction, so the partial balance and reversed-rate statements carry an explicit $n_j\ge 1$ where the book's state space carries it implicitly; the goal itself does not need such a guard.

A trivializing formalization is ruled out by the second conjunct of the goal: the equilibrium equations alone are a homogeneous linear condition satisfied by $\pi\equiv 0$, whereas the requirement that $\pi$ sum to $1$ forces the constants $g_j$ to be exactly the ones stated.

Contributions welcome beyond the listed items: Burke's theorem (2.1) and the Poisson character of the exit streams, Corollary 2.10, the closed-form of the telephone banking example (Exercise 2.6), the Chinese restaurant process of Exercise 2.13, and Bartlett's theorem (2.17) on linear migration processes over a general space.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 2 (pp. 22–48); Theorems 2.4, 2.8, 2.9, 2.13, equations (2.1)–(2.6). DOI 10.1017/cbo9781139565363
• James R. Jackson, Networks of waiting lines, Operations Research 5 (1957), 518–521. DOI 10.1287/opre.5.4.518
• P. Whittle, Equilibrium distributions for an open migration process, Journal of Applied Probability 5 (1968), 567–571. DOI 10.2307/3211921
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapters 2 and 3.
• David G. Kendall, Some problems in mathematical genealogy, in Perspectives in Probability and Statistics (J. Gani, ed.), Academic Press, 1975, 325–345.
• John D. C. Little, A proof for the queuing formula: $L = \lambda W$, Operations Research 9 (1961), 383–387. DOI 10.1287/opre.9.3.383

Motivation

In the early twentieth century Agner Krarup Erlang worked for the Copenhagen Telephone Company and faced a sizing question that every shared-resource operator still faces: how many parallel circuits must a telephone link carry so that an arriving call is almost never turned away? The answer he published — the Erlang loss formula — is still the standard dimensioning tool for circuit-switched links, call centres, hospital beds, rental fleets, and any system in which a customer who finds every server occupied leaves rather than waits.

The formula is the first capstone of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), where it closes Chapter 1 and supplies the building block for the loss networks of Chapter 3. It is also the cleanest possible demonstration of the book's method: write down the transition rates of a Markov process, guess that the process is reversible, solve the detailed balance equations, and read the answer off the normalizing constant. This mission formalizes that chapter: the reversibility apparatus, the birth-and-death chain of the loss link, and Erlang's formula itself.

Setting

A link carries $C$ parallel circuits. Calls arrive as a Poisson process of rate $\lambda$ and each call, while it lasts, occupies one circuit for an exponentially distributed holding time of parameter $\mu$; holding times are independent of one another and of the arrival times. A call that arrives to find all $C$ circuits busy is lost — it does not queue.

Let $X(t)\in\{0,1,\dots,C\}$ be the number of busy circuits. Then $X$ is a Markov process with transition rates

$$q(j,j+1)=\lambda \quad (j=0,\dots,C-1), \qquad q(j,j-1)=j\mu \quad (j=1,\dots,C),$$

and $q(j,k)=0$ otherwise. A collection of numbers $\pi=(\pi(j))$ is in detailed balance with rates $q$ when

$$\pi(j)\,q(j,k)=\pi(k)\,q(k,j)\qquad\text{for all }j,k,$$

and satisfies the equilibrium (full balance) equations when

$$\pi(j)\sum_k q(j,k)=\sum_k \pi(k)\,q(k,j)\qquad\text{for all }j .$$

Detailed balance is the statement that, in equilibrium, transitions from $j$ to $k$ occur as frequently as transitions from $k$ to $j$. Writing $\nu=\lambda/\mu$ for the traffic intensity, Erlang's formula is

$$E(\nu,C)=\frac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}.$$

Formalization targets

Goal — Erlang's formula

$$\pi \text{ in detailed balance with } q, \ \sum_{j=0}^{C}\pi(j)=1 \quad\Longrightarrow\quad \pi(C)=E\!\left(\tfrac{\lambda}{\mu},C\right).$$

The goal fixes no numerical constant: it says that whatever probability vector solves the detailed balance equations of the loss link assigns exactly $E(\nu,C)$ to the blocking state. The hypothesis is detailed balance rather than full balance, which is what the book's derivation actually uses and is the stronger assumption to discharge.

Supporting levels

$$\pi(j)=\frac{\nu^{j}}{j!}\,\pi(0), \qquad \sum_{j=0}^{C} j\,\pi(j)=\nu\bigl(1-E(\nu,C)\bigr), \qquad \frac{d}{d\nu}E(\nu,C)=-\bigl(1-E(\nu,C)\bigr)\bigl(E(\nu,C)-E(\nu,C-1)\bigr),$$

together with the reversibility results that justify the method: detailed balance implies full balance, the reversed process of Proposition 1.1 has rates $q'(j,k)=\pi(k)q(k,j)/\pi(j)$ and retains $\pi$ as an equilibrium distribution, and $q'=q$ holds exactly when $\pi$ and $q$ are in detailed balance.

Significance

The result itself. $E(\nu,C)$ is the blocking probability of the link, so it converts a traffic measurement $\nu$ and a target grade of service into a circuit count. It is insensitive: the same formula holds for any holding-time distribution with mean $1/\mu$, which is why it survives as an engineering tool far outside the exponential model that produces it here. Chapter 3 of the book builds loss networks on top of it, and the Erlang fixed point that approximates a whole network is a system of coupled copies of this one formula. The derivative identity is the ingredient that makes $E(\nu,C)$ tractable in optimization: it shows $E$ is increasing in $\nu$, and the recursion it encodes is how the formula is evaluated numerically without overflow.

Formalizing it. Nothing here is open mathematics; the value of the mission is a machine-checked statement of the loss model and a reusable reversibility layer. Mathlib has no theory of detailed balance or of reversible Markov processes over a countable state space, so this mission contributes the first: the predicates DetailedBalance and FullBalance, the reversed rate matrix, and the three structural facts relating them. Those are shared by every later mission in this series — the migration processes of Chapter 2 and the loss networks of Chapter 3 are all proved reversible or quasi-reversible by exactly these means.

Difficulty

The obvious route to $\pi(C)$ is to solve the equilibrium equations directly, and for a birth-and-death chain that is a three-term recursion whose general solution needs two boundary conditions. Detailed balance replaces it with a two-term recursion and one boundary condition, and the whole content of the reversibility section is that the substitution is legitimate. The remaining work is bookkeeping that Lean makes less forgiving than the page does: the detailed balance equations must be indexed so that the $j=0$ and $j=C$ boundaries are not silently assumed away, the normalizing sum must be shown positive before it can be inverted, and the induction that produces $\nu^{j}/j!$ has to carry the Fin (C+1) index through Nat.factorial. For the derivative identity, the naive differentiation of a quotient gives $\left(\sum_{j\le C-1}\nu^{j}/j!\right)$ in the numerator, and recognizing it as $\bigl(1-E(\nu,C)\bigr)$ times the denominator is the step that produces the stated form.

Formalization scope

The state space is Fin (C + 1), so the link with $C$ circuits has $C+1$ states and finiteness is built in; $\pi$ is a plain function Fin (C + 1) → ℝ constrained by hypotheses rather than a PMF, so that the normalization $\sum_j \pi(j) = 1$ appears explicitly wherever it is used. FullBalance is written with unconditional sums (tsum) over an arbitrary state space, so the same predicate serves the countable chains of later chapters; over a Fintype it is the finite sum. Rates are real-valued and q j j = 0 by construction, matching the book's convention that a Markov process must change state when it jumps.

The rates carry $\lambda,\mu>0$ as hypotheses. This rules out the degenerate reading in which $\mu = 0$ makes every downward rate vanish: with $\mu=0$ the detailed balance equations force $\pi(j)\lambda = 0$ for $j<C$, so the only normalized solution is the point mass at $C$, and $\pi(C)=1$ while Lean evaluates $E(\lambda/0,C)=E(0,C)=0$ for $C\ge1$; the goal would be false. Erlang's formula is stated for the last state Fin.last C, not for an unconstrained index, so it cannot be satisfied by a degenerate reindexing.

Contributions welcome beyond the listed items: the insensitivity of $E(\nu,C)$ to the holding time distribution, the recursion $E(\nu,C)=\nu E(\nu,C-1)/(C+\nu E(\nu,C-1))$, the finite-source variant $\pi_M(j)\propto\binom{M}{j}(\eta/\mu)^{j}$ and the PASTA statement that an arriving call in that model sees $\pi_{M-1}$, and the parking-space identity $\sum_{C\ge 0}E(\nu,C)$ of Exercise 1.9.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 1 (pp. 13–21), equations (1.2), (1.4), (1.5), Proposition 1.1, Exercises 1.7 and 1.8. DOI 10.1017/cbo9781139565363
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektrotkeknikeren 13 (1917), 5–13.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1.
• J. R. Norris, Markov Chains, Cambridge University Press, 1998. DOI 10.1017/CBO9780511810633

Restless multi-armed bandits are the standard model for allocating a scarce resource across many independently-evolving agents: N arms, each a small Markov chain, and a budget that lets you activate only a fixed fraction of them at each step. The joint problem is PSPACE-hard, so practice runs on index policies — score each arm by a priority index computed from its own local state, then activate the top ones until the budget runs out — and evaluates them by value decomposition: approximate the joint Q-function by a sum of per-arm local Q-functions, each computed from a single arm's chain. The decomposition is used everywhere from Whittle-index heuristics to modern multi-agent RL, and it is used without an error bound.

Chen and Peng (arXiv:2506.02385) supply one. Their companion mission established the general principle: the value decomposition error of a multi-agent chain is controlled by its measure of Markov entanglement, the distance from the chain's transition matrix to the nearest separable one. This mission carries that principle to the restless-bandit setting and proves that index policies are asymptotically separable — their entanglement decays like 1/sqrt(N), so the decomposition error is sublinear in N while the joint Q-function itself is of order N. The relative error vanishes as the system grows, which is exactly why the practice works.

The argument runs through the mean-field limit. Because the arms are homogeneous, the only thing that matters about a joint state is its configuration: the fraction of arms in each local state. Under an index policy the configuration evolves by a map that does not depend on N at all, and under two standard technical conditions — a uniform global attractor property and non-degeneracy — that map has a unique attracting fixed point m*. The chain of reasoning is: policy entanglement is bounded by how far the realised policy sits from the mean-field limiting policy (Proposition 1); that distance is bounded by the configuration's deviation from m* (Lemma 2/8); and the deviation concentrates at rate 1/sqrt(N) by a concentration-plus-local-stability argument adapted from Gast, Gaujal and Yan. The concentration and stability inputs (Lemmas 9, 10, 11) are results of Gast et al. and are formalized here as well, so the mission stands on its own.

The mission also formalizes the mean-field map on the whole simplex and checks it against the N-agent characterisation, which is what makes the piecewise-affine and stability analysis expressible at all.

Motivation

Every sampling guarantee in this series so far is approximate: run the chain for $t_{\mathrm{mix}}(\varepsilon)$ steps and the output is within $\varepsilon$ of stationarity. In 1996 Propp and Wilson showed that, astonishingly, one can often sample exactly from the stationary distribution of a chain — with no error at all and no knowledge of the mixing time — by running the chain not forward from the present but from the past. Their algorithm, coupling from the past (CFTP), drives all states simultaneously with the same sequence of random update maps drawn from times $-1,-2,-3,\dots$; as soon as the composed map from some time $-t$ collapses the entire state space to a single value, that value is an exact sample from $\pi$. Chapter 22 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009; the chapter is by Propp and Wilson themselves) presents the algorithm, the monotone shortcut that makes it practical for huge state spaces, and the proof of exactness. This mission — the final one of the series — formalizes that correctness proof.

Setting

Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$. A random mapping representation of $P$ is a probability distribution $\nu$ on update functions $f:V\to V$ that reproduces the transition probabilities in one step:

$$\nu\{f: f(x)=y\}\;=\;P(x,y)\qquad\text{for all }x,y.$$

Sampling $f\sim\nu$ and applying it to the current state is exactly one $P$-step — simultaneously from every possible current state.

CFTP draws i.i.d. maps $f_{-1},f_{-2},\dots\sim\nu$ indexed by past times and composes them forward from the past up to time zero:

$$F^0_{-t}\;=\;f_{-1}\circ f_{-2}\circ\cdots\circ f_{-t}.$$

Note the order: extending the horizon deeper into the past prepends new randomness inside the composition, while the maps near time $0$ stay fixed — this is the crucial asymmetry between running from the past and running into the future. The composition has coalesced when $F^0_{-t}$ is a constant map — all starting states have been funneled to one common value — and the algorithm outputs that value. In the monotone variant, $V$ carries a partial order with a bottom state $\hat0$ and a top state $\hat1$ and every update map is monotone; then it suffices to track the two extreme trajectories.

Formalization targets

Goal

Correctness of coupling from the past (Propp–Wilson; §22.2–22.3), the capstone of the series: if $\nu$ is a random mapping representation of $P$, $\pi$ is stationary for $P$, and coalescence is almost sure, then for every state $y$ the probability that the CFTP composition has coalesced to the value $y$ within $t$ steps from the past tends, as $t\to\infty$, to exactly $\pi(y)$ — the output of the algorithm is an exact sample from the stationary distribution, with no mixing-time error term.

Milestones

• Proposition 1.5 / §22.3 — every finite Markov chain has a random mapping representation: a suitable $\nu$ always exists.
• Coalescence (§22.3) — if some finite composition of update maps collapses the state space with positive probability, then coalescence is almost sure: the probability that $F^0_{-t}$ is not yet constant tends to $0$ as $t\to\infty$.
• Monotone CFTP (§22.2) — if the state space has a bottom $\hat0$ and a top $\hat1$ and every update map is monotone, then the composition is constant as soon as it merely identifies $\hat0$ and $\hat1$: checking two trajectories certifies coalescence of all of them.

Significance

The results. CFTP is one of the most striking algorithmic ideas probability has produced: a Las Vegas algorithm whose output distribution is exactly $\pi$, side-stepping every mixing-time estimate of the previous twelve missions. The monotone shortcut is what made it explode in practice — for the Ising model of Mission IX the $2^n$ trajectories collapse to two, and Propp–Wilson famously drew exact Ising samples on large grids at the critical temperature. CFTP remains the foundation of exact-simulation methods across statistical physics, spatial statistics, and randomized algorithms.

Formalizing it. The correctness argument is short but famously slippery — the standard pitfall (running the coupling into the future yields a biased sample) is precisely a statement about the order of composition, which a formal proof pins down mercilessly. Nothing about exact sampling exists in any proof-assistant library. Formalized CFTP correctness is a fitting keystone: it consumes the random-map representation (Chapter 1), stationarity (Mission I), and the almost-sure-coalescence analysis, and certifies the algorithm practitioners actually run.

Difficulty

The whole content lies in managing the composition order and the limiting argument without measure theory. The probability space at horizon $t$ is the finite product of $t$ copies of $\nu$ (tuples of update maps, weighted by products); the key observation — for fixed $t$, the law of $F^0_{-t}$ applied to any fixed start equals the law of $t$ forward steps — is a finite re-indexing argument. Exactness then follows from a sandwich: on the event of coalescence by time $t$, the output equals $F^0_{-t}(x)$ for every $x$; choosing the start according to $\pi$ shows the output law differs from $\pi$ by at most the non-coalescence probability, and the hypothesis drives that to zero. Formalizing this needs care at exactly the point where informal proofs wave: the event "coalesced by $-t$" is increasing in $t$ because the maps near zero are shared between horizons — the tuple encoding must make this monotonicity provable. The coalescence milestone is a geometric-trials argument (independent blocks each collapse with probability bounded below), and the monotone milestone is an induction showing monotonicity of compositions plus the squeeze between the extreme trajectories. All randomness is finite products of a finite distribution; limits are limits of explicit real sequences.

Formalization scope

Update-map distributions are functions $(V\to V)\to\mathbb R$ with the distribution predicate of Mission I; the random-map representation condition is a finite-sum identity. The composition $F^0_{-t}$ is encoded by a tuple $F:\mathrm{Fin}\,t\to(V\to V)$ with $F(i)$ the map used at time $-(i{+}1)$, folded so that the last entry applies first — the from-the-past order. Coalescence probabilities and output probabilities are finite sums over tuples of products of $\nu$-weights; "coalescence is almost sure" is the statement that the non-coalescence probability tends to $0$, and the goal's conclusion is a limit of real sequences (Filter.Tendsto), not a measure-theoretic almost-sure statement. The monotone milestone is stated abstractly for any finite partial order with OrderBot and OrderTop and any tuple of monotone maps — reusable beyond CFTP. No measure theory, filtrations, or i.i.d. infrastructure is required anywhere.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (Chapter 22, by J. G. Propp and D. B. Wilson). https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• J. G. Propp, D. B. Wilson, Exact sampling with coupled Markov chains and applications to statistical mechanics, Random Structures Algorithms 9 (1996). https://doi.org/10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO;2-O
• D. B. Wilson, How to couple from the past using a read-once source of randomness, Random Structures Algorithms 16 (2000). https://doi.org/10.1002/(SICI)1098-2418(200003)16:2<85::AID-RSA1>3.0.CO;2-H

Motivation

The first mission of this series established that an irreducible finite Markov chain has a unique stationary distribution $\pi$. The present mission, covering Chapters 3–4 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009), answers the two questions that make that fact useful. First, the inverse problem of sampling: given a target distribution $\pi$ — uniform over proper colorings, a Gibbs measure, a posterior — how does one build a chain whose stationary distribution is $\pi$? The Metropolis and Glauber constructions of Chapter 3 are the universal answers, and they are the engine of Markov chain Monte Carlo across statistical physics, Bayesian statistics, and approximate counting. Second, the convergence question: in what sense, and how fast, does an irreducible aperiodic chain approach $\pi$? Chapter 4 introduces the total variation distance, proves the Convergence Theorem — geometric convergence to stationarity — and defines the mixing time, the parameter the entire remainder of the book estimates.

Setting

All chains live on a finite state space $V$ and are presented by row-stochastic matrices, with the definitions of Mission I. The total variation distance between distributions $\mu$ and $\nu$ is

$$\|\mu-\nu\|_{\mathrm{TV}} = \max_{A\subseteq V}\,|\mu(A)-\nu(A)|,$$

the maximal discrepancy over events. A coupling of $\mu$ and $\nu$ is a distribution on $V\times V$ whose marginals are $\mu$ and $\nu$. For a chain $P$ with stationary $\pi$ one sets

$$d(t)=\max_x \|P^t(x,\cdot)-\pi\|_{\mathrm{TV}},\qquad \bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{\mathrm{TV}},$$

and the mixing time is $t_{\mathrm{mix}}(\varepsilon)=\min\{t : d(t)\le\varepsilon\}$, with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$.

The Metropolis chain for a target $\pi$ and a symmetric proposal chain $\Psi$ accepts a proposed move $x\to y$ with probability $1\wedge \pi(y)/\pi(x)$; a general (not necessarily symmetric) base chain is handled by the ratio $\bigl(\pi(y)\Psi(y,x)\bigr)/\bigl(\pi(x)\Psi(x,y)\bigr)\wedge 1$. The Glauber dynamics for a distribution $\pi$ on configurations $V^{\text{sites}}$ picks a uniform site and re-samples its value from $\pi$ conditioned on the rest.

Formalization targets

Goal

$\text{$P$ irreducible and aperiodic}\;\Longrightarrow\;\exists\,\alpha\in(0,1),\ C>0:\quad d(t)\le C\alpha^{t}.$

This is Theorem 4.9, the Convergence Theorem. It asserts only the geometric shape of convergence, leaving all quantitative rates to later missions, which is why it is the goal.

Milestones

The milestones are the chapter's working parts: stationarity and reversibility of the Metropolis chain for symmetric and general base chains (§3.2, Exercise 3.1), stationarity and reversibility of the Glauber dynamics (§3.3, Exercise 3.2); the three characterizations of total variation distance — the half-$\ell^1$ formula (Proposition 4.2 with Remark 4.3), the supremum over $[-1,1]$-bounded test functions (Proposition 4.5), and the coupling characterization with an optimal coupling attaining it (Proposition 4.7 with Remark 4.8); the comparison $d\le\bar d\le 2d$ (Lemma 4.11) and submultiplicativity $\bar d(s+t)\le\bar d(s)\bar d(t)$ (Lemma 4.12); the standard mixing-time consequences $d(\ell\, t_{\mathrm{mix}}(\varepsilon))\le(2\varepsilon)^\ell$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil\log_2\varepsilon^{-1}\rceil\, t_{\mathrm{mix}}$ (§4.5); and the equality of distance to stationarity for a group walk and its inverse walk (Lemma 4.13 and Corollary 4.14).

Significance

The results. The Convergence Theorem is the qualitative foundation on which quantitative mixing theory stands: it guarantees that $t_{\mathrm{mix}}(\varepsilon)$ is finite, so every bound in Missions III–XIII is a bound on a well-defined quantity. The TV characterizations are used constantly — the coupling characterization is the engine of Mission III, the half-$\ell^1$ formula of every explicit computation. The Metropolis and Glauber stationarity results justify the chains analyzed in Missions III (colorings, hardcore), VIII (path coupling) and IX (Ising). Submultiplicativity of $\bar d$ is what makes $t_{\mathrm{mix}}$ a meaningful single number.

Formalizing them. None of this exists in Mathlib: there is no total variation distance for finitely supported distributions, no coupling theory, no mixing time, no MCMC correctness statement. The definition layer published here (TV distance, $d$, $\bar d$, $t_{\mathrm{mix}}$, couplings, Metropolis, Glauber) is imported by every subsequent mission of the series.

Difficulty

The tempting proof of Theorem 4.9 via spectral decomposition fails twice: it needs reversibility, which the theorem does not assume, and spectral machinery that arrives only in Mission VII. The book's proof is the Doeblin decomposition: by Proposition 1.7 some power satisfies $P^r(x,y)\ge\delta\pi(y)$, so $P^r=(1-\theta)\Pi+\theta Q$ with $\Pi$ the rank-one matrix of rows $\pi$, and induction gives $P^{rk}=(1-\theta^k)\Pi+\theta^kQ^k$. The formal work is matrix algebra with careful bookkeeping of the remainder chain $Q$, plus the monotonicity of $d$ needed to interpolate between multiples of $r$. For Proposition 4.7 the delicate half is constructing the optimal coupling: mass $\mu\wedge\nu$ on the diagonal and the normalized product of the positive parts off it, with the degenerate case $\mu=\nu$ handled separately. The Glauber stationarity statement must be phrased with care because configurations outside the support of $\pi$ have junk rows; the formalization asserts stochasticity only at supported configurations, and detailed balance globally.

Formalization scope

Total variation distance is defined as the supremum over events, $\bigsqcup_{A}\,|\mu(A)-\nu(A)|$ over Finset V, exactly as in (4.1); the half-$\ell^1$ formula is a milestone, not the definition. The mixing time is sInf of the set $\{t : d(t)\le\varepsilon\}$ in $\mathbb N$ (junk value $0$ if empty — impossible under the goal theorem). Couplings are distributions on the product with prescribed marginals; no probability-space machinery is used. The mixing-time inequalities are stated with the integer-rounding slack made explicit (e.g. $\lceil\log_2\varepsilon^{-1}\rceil$ via Nat.ceil of a real logarithm) so that no statement is true only "up to rounding". The Metropolis definitions use total real division, so the hypotheses require $\pi>0$ pointwise; this matches the book, which divides by $\pi(x)$ throughout.

Welcome contributions beyond the milestones: simp lemmas for tvDist, monotonicity of $d$ and $\bar d$ in $t$, and triangle-inequality infrastructure — all reused by Missions III–XIII.

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
• N. Metropolis, A. Rosenbluth, M. Rosenbluth, A. Teller, E. Teller, Equation of state calculations by fast computing machines, J. Chem. Phys. 21 (1953). https://doi.org/10.1063/1.1699114
• W. Doeblin, Exposé de la théorie des chaînes simples constantes de Markov à un nombre fini d'états, Rev. Math. Union Interbalkan. 2 (1938).

Why short-horizon outcome windows

Randomized experiments (A/B tests) on ride-sharing marketplaces, recommendation systems and digital-health services assign each arriving user to treatment or control. The assignment changes the system state seen by later users, so observations are not independent: this is temporal interference, or carryover. The difference-in-means estimator ignores it, and in Markovian models its bias can be as large as the treatment effect itself (Farias, Li, Peng, Zheng 2022; Hu, Wager 2022). Corrections based on off-policy evaluation or on differences of $Q$-values assume a stationary environment, while real systems have time-varying dynamics and the experimenter observes a single trajectory.

Johari, Peng and Xing propose the truncated policy gradient (TPG) estimator: each instantaneous outcome in the difference-in-means estimator is replaced by the sum of the next $k+1$ outcomes. The paper shows that this estimates, without bias, the derivative of a truncated policy value, and derives bias and variance bounds, a central limit theorem and a consistent variance estimator in nonstationary Markovian environments. This mission formalizes those statements.

Setting

Time is $t=0,1,\dots,T-1$ (the paper's time $t+1$). The state space $S$ is finite and the action $Z_t\in\{0,1\}$ is control or treatment. For each time $t$ and action $z$ there is a transition matrix $P_z^t$ with $\mathbb P(X_{t+1}=x'\mid X_t=x,Z_t=z)=P_z^t(x,x')$; the matrices may change arbitrarily with $t$, which is the nonstationarity. The initial state $X_0$ has distribution $\rho$. The reward $Y_t$ is drawn from a distribution $R(\cdot\mid X_t,Z_t)$ on $\mathbb R$, independently of everything else given $(X_t,Z_t)$, and $R([-M,M]\mid x,z)=1$ for all $x,z$. Write $r(x,z)=\int y\,R(dy\mid x,z)$.

The policy $\pi_\theta$ assigns treatment with probability $\theta$ at every time, independently of everything else. $\pi_1$ is all-treatment, $\pi_0$ is all-control, and the experiment runs $\pi_{1/2}$. Write $P_\theta^t=\theta P_1^t+(1-\theta)P_0^t$ and $\mathbb E_\theta$ for expectation under $\pi_\theta$. The value function and the global average treatment effect (GATE) are

$$J(\theta)=\frac1T\sum_{t=0}^{T-1}\mathbb E_\theta[Y_t],\qquad \tau=J(1)-J(0).$$

The TPG estimator with truncation size $k$ is

$$\widehat\tau_k=\frac1T\sum_{u=0}^{T-1}\Bigl(\frac{\mathbf 1\{Z_u=1\}}{1/2}-\frac{\mathbf 1\{Z_u=0\}}{1/2}\Bigr)\sum_{t=u}^{\min(u+k,\,T-1)}Y_t ,$$

so $\widehat\tau_0$ is the difference-in-means estimator.

Two quantities control the bounds. The mixing assumption (Assumption 1) asks for $\gamma\in(0,1)$ with $\|f'P_z^t-fP_z^t\|_{\mathrm{TV}}\le\gamma\,\|f'-f\|_{\mathrm{TV}}$ for all $t<T$, all $z$ and all probability vectors $f,f'$ on $S$, where $\|f-f'\|_{\mathrm{TV}}=\tfrac12\|f-f'\|_1$. The kernel deviation is $\delta=\max_{t<T}\max_{x}\|P_1^t(x,\cdot)-P_0^t(x,\cdot)\|_{\mathrm{TV}}$.

Formalization targets

Goal: Theorem 1, bias and variance of the TPG estimator

There are absolute constants $C_1,C_2>0$ such that for every environment, every $T\ge1$, every $0\le k\le T$ and every $\gamma\in(0,1)$ and $M$ as above,

$$\bigl|\mathbb E_{1/2}[\widehat\tau_k]-\tau\bigr|\le C_1\Bigl(\frac{1-\gamma^k}{(1-\gamma)^2}\,\delta^2M+\frac{\gamma^k}{1-\gamma}\,\delta M\Bigr),\qquad \operatorname{Var}_{1/2}(\widehat\tau_k)\le C_2\Bigl(\frac{(k+1)^2M^2}{T}+\frac{\gamma\,(k+1)M^2}{T(1-\gamma)}\Bigr).$$

The constants are left unspecified, as in the paper's $O(\cdot)$ statement, so an improvement of the constants does not invalidate the goal.

Explicit constants: Propositions 5 and 6

For data collected under $\pi_\theta$ with $\theta\in(0,1)$, the paper gives both bounds with explicit constants, for the TPG estimator and for a reward-corrected variant. At $\theta=1/2$, Proposition 5 reads

$$\bigl|\mathbb E[\widehat\tau_k]-\tau\bigr|\le\frac{2\delta M\gamma^k}{1-\gamma}+2\delta^2M\,\Psi_k(\gamma),\qquad \operatorname{Var}(\widehat\tau_k)\le\frac{4M^2(k+1)}{T}\Bigl(2k+3+\frac{4\gamma}{1-\gamma}\Bigr),$$

with $\Psi_k(\gamma)=\sum_{j=0}^{k-2}(j+1)\gamma^j$.

Policy-gradient identities: Propositions 1–4

$J$ and its truncated analogue $J_k$ are differentiable at $1/2$, with derivative equal to the horizon average of differences of ($k$-truncated) $Q$-values, and $\mathbb E_\theta[\widehat\tau^{\mathrm{TPG}}_{\theta,k}]$ equals the corresponding derivative for every $\theta\in(0,1)$. Without the mixing assumption, the untruncated estimator satisfies $|\mathbb E[\widehat\tau_T]-\tau|\le C\,T^2\delta^2M$ and $\operatorname{Var}(\widehat\tau_T)\le2M^2(T+1)$.

Asymptotics: Theorem 2, Lemmas 1–5 and Corollary 1

For fixed $k$, under mixing at all times, a positive limit $\sigma_k^2$ of the normalized variance (Assumption 2) and a Cesàro mean-stability condition (Assumption 3),

$$\sqrt T\,\bigl(\widehat\tau_k-\mathbb E[\widehat\tau_k]\bigr)\Rightarrow\mathcal N(0,\sigma_k^2),\qquad \widehat\Omega_T\xrightarrow{p}\sigma_k^2,$$

where $\widehat\Omega_T$ is a Newey–West estimator with bandwidth $L_T\to\infty$, $L_T=O(T^{1/3})$. The supporting statements are a covariance inequality under strong mixing, the bound $\alpha(h)\le\gamma^{h-1}$ on the mixing coefficients of the experimental process and its consequence for the summands of the estimator, the central limit theorem alone, and consistency of the ideal and of the feasible variance estimators.

What the results give

Theorem 1 separates two error sources: a term of second order in $\delta$ that does not grow with $T$, and a term that decays geometrically in $k$. Together with Proposition 2 it shows what truncation buys: a variance bound of order $(k+1)^2/T$ instead of order $T$, at the price of a bias term of order $\gamma^k$. Theorem 2 supplies standard errors for the estimator from a single nonstationary trajectory.

All results of the paper are proved on paper; none has a machine-checked proof. The work of this mission is the formal proofs of the stated results. The definition layer (a finite-state nonstationary Markov decision process with real rewards, its trajectory law under time-varying randomization, total-variation contraction, strong-mixing windows, a Newey–West estimator) can be reused for other results on experiments with Markovian interference.

Where the difficulty lies

The first idea is to bound $|J'(1/2)-(J(1)-J(0))|$ by the second derivative of $J$ on $[0,1]$. Every pair of times contributes to that second derivative, so this route gives the $T^2\delta^2M$ of Proposition 2 and nothing uniform in the horizon. Theorem 1 is uniform in $T$, and its bound has no term of first order in $\delta$ beyond the truncation term; Proposition 5 shows that such a term is present at every allocation $\theta\ne1/2$. Formal proofs have to handle ordered products of time-varying stochastic matrices and signed measures of total mass zero, with a contraction that is assumed one step at a time.

The variance bound and Theorem 2 concern a dependent, non-identically distributed sequence observed once. Mathlib has no central limit theorem for nonhomogeneous Markov chains and no covariance inequality for strongly mixing sequences; the paper relies on Arlotto and Steele (2016) for the former and on an inequality from Doukhan (1994) for the latter.

Formalization scope

TPG.Env S packages $(P,\rho,R)$ for a finite type S. Kernels are real matrices with nonnegative entries and rows summing to one, indexed by all $t\in\mathbb N$; a statement with horizon $T$ uses only the times below $T$. A trajectory is a function Fin T → S × Bool × ℝ, and Env.trajLaw is its law for an arbitrary sequence of treatment probabilities, built as a finite mixture over state and action paths of product reward laws. $J$, $\tau$, $J_k$ and the $Q$-values are defined from this law, and expectations given $\{Z_u=z\}$ are taken under the conditional measure. Rewards are bounded through the hypothesis E.RewardBound M; the standing assumptions of the paper enter each theorem as hypotheses, and S carries the discrete measurable structure.

Statements require $T\ge1$ and $0\le k\le T$, as in the paper. Asymptotic statements compute the law of each statistic under the horizon-$T$ measure: convergence in distribution is tested against bounded continuous functions, and convergence in probability is stated for each $\varepsilon>0$. The limit $\sigma_k^2$ is a parameter constrained by Assumption 2. For $\theta\notin[0,1]$ the law of $\pi_\theta$ is not a probability law and no statement depends on it. The hypotheses are satisfiable for every $T$, $k$ and $\gamma$: an environment with one state and a nonzero constant reward satisfies all of them, including Assumptions 2 and 3, so no statement is vacuous.

Not included: Definition 1 and Lemma 6 of the paper (Dobrushin coefficients and the Arlotto–Steele theorem on general Borel state spaces), the stationary difference-in-$Q$ discussion of Appendix C, the constant-reward example showing that the variance order is attained, and the numerical studies. Formal statements of those, and auxiliary lemmas about Env.trajLaw, ordered matrix products and total-variation contraction, are welcome contributions.

Selected references

• R. Johari, T. Peng, W. Xing, Estimation of Treatment Effects Under Nonstationarity via the Truncated Policy Gradient Estimator, arXiv preprint, 2025–2026. https://arxiv.org/abs/2506.05308
• V. F. Farias, A. A. Li, T. Peng, A. Zheng, Markovian Interference in Experiments, Advances in Neural Information Processing Systems 35, 2022. https://arxiv.org/abs/2206.02371
• Y. Hu, S. Wager, Switchback Experiments under Geometric Mixing, arXiv preprint, 2022. https://arxiv.org/abs/2209.00197
• A. Arlotto, J. M. Steele, A Central Limit Theorem for Temporally Nonhomogeneous Markov Chains with Applications to Dynamic Programming, Mathematics of Operations Research 41(4), 2016. https://doi.org/10.1287/moor.2016.0784
• P. Doukhan, Mixing: Properties and Examples, Lecture Notes in Statistics 85, Springer, 1994. https://doi.org/10.1007/978-1-4612-2642-0