Stochastic Systems

Motivation

A Brownian path is continuous, and that is essentially all it is. It has no derivative anywhere, it crosses zero infinitely often in every interval $(0,\epsilon)$, and it becomes positive and negative immediately after time zero. None of this is visible from the finite-dimensional distributions; it is a statement about the germ of the path at a point, and the tool that unlocks it is a zero-one law.

Chapter 7 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) develops that tool. The natural filtration $\mathcal F^{0}_{s}=\sigma(B_r:r\le s)$ is enlarged to $\mathcal F^{+}_{s}=\bigcap_{t>s}\mathcal F^{0}_{t}$, which allows "an infinitesimal peek at the future" — a quantity like $\limsup_{t\downarrow s}(B_t-B_s)/f(t-s)$ is $\mathcal F^{+}_{s}$-measurable but not $\mathcal F^{0}_{s}$-measurable. Blumenthal's 0-1 law (Theorem 7.2.3) says that at $s=0$ this enlargement buys nothing probabilistically: the germ $\sigma$-field $\mathcal F^{+}_{0}$ is trivial.

Everything local follows. If the path had any chance of staying non-positive on some interval $(0,\epsilon)$, that would be a germ event of probability at least $1/2$ by symmetry, so it has probability one — and the path enters $(0,\infty)$ immediately. Continuity then forces it to return to zero immediately as well. Combined with the time inversion $X_t=tB(1/t)$, which turns the germ at $0$ into the tail at $\infty$, the same law gives $\limsup_{t\to\infty}B_t/\sqrt t=\infty$ and the recurrence of one-dimensional Brownian motion.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $B:\mathbb R_{\ge0}\to\Omega\to\mathbb R$ a Brownian motion: its finite-dimensional laws are centred Gaussian with covariance $\operatorname{cov}(B_s,B_t)=s\wedge t$, and almost every path is continuous. In particular $B_0=0$ almost surely, so this is Durrett's $\mathbb P_0$.

Three $\sigma$-fields organize the chapter:

$$\mathcal F^{0}_{t}=\sigma(B_s:s\le t),\qquad \mathcal F^{+}_{0}=\bigcap_{t>0}\mathcal F^{0}_{t},\qquad \mathcal T=\bigcap_{t\ge0}\sigma(B_s:s\ge t).$$

The first is the past, the second the germ at time zero, the third the tail at infinity.

A path $f$ is Lipschitz at the point $s$ with constant $C$ when $|f(t)-f(s)|\le C|t-s|$ for all $t$ within some positive distance of $s$. A path differentiable at $s$ is Lipschitz at $s$, so failing this at every point and for every constant is a strong form of nowhere differentiability.

Formalization targets

Goal — Theorem 7.2.3, Blumenthal's 0-1 law

$$A\in\mathcal F^{+}_{0}\quad\Longrightarrow\quad \mathbb P(A)\in\{0,1\}.$$

In words: the germ $\sigma$-field is trivial. Nothing about the path in an arbitrarily short initial interval is genuinely random.

Supporting levels

Theorem 7.1.5, that Brownian paths are Hölder continuous of every exponent $\gamma<1/2$ on every bounded interval; Theorem 7.1.6, that with probability one they are not Lipschitz at any point, hence nowhere differentiable — the Paley–Wiener–Zygmund theorem in the proof of Dvoretsky, Erdős and Kakutani; Theorem 7.2.4, that the path enters $(0,\infty)$ immediately; Theorem 7.2.5, that its zero set accumulates at $0$; and Theorem 7.2.8, that $\limsup_{t\to\infty}B_t/\sqrt t=+\infty$ and $\liminf_{t\to\infty}B_t/\sqrt t=-\infty$.

Significance

The results themselves. Blumenthal's law is the gateway to every local path property of Brownian motion, and Durrett uses it immediately for exactly that. Theorems 7.2.4 and 7.2.5 together say the path oscillates across zero infinitely often in every initial interval — the reason the zero set is an uncountable closed set of Lebesgue measure zero, and the reason the "first return to zero" is not a useful notion at time $0$. Theorem 7.2.8 is the same law pushed to $t\to\infty$ by time inversion, and it is what makes one-dimensional Brownian motion recurrent (Theorem 7.2.9).

The Hölder pair is the sharp description of path regularity. Exponent $\gamma<1/2$ always works, $\gamma>1/2$ never does, and the borderline $1/2$ is subtle: $\mathbb P(t\in H_{1/2})=0$ for each fixed $t$, but Davis (1983) showed $\mathbb P(H_{1/2}\ne\emptyset)=1$. Nowhere differentiability is the historical headline — Paley, Wiener and Zygmund (1933) — and the proof given here is a short covering argument rather than a series construction.

Formalizing them. Mathlib has the object but almost none of the theory. It defines IsPreBrownianReal and IsBrownianReal, proves that a centred Gaussian process with covariance $s\wedge t$ is pre-Brownian, and supplies the invariances — negation, scaling $t\mapsto c^{-1/2}B(ct)$, the shift $t\mapsto B(t_0+t)-B(t_0)$, and the time inversion $t\mapsto tB(1/t)$ — together with the weak Markov property IsPreBrownianReal.indepFun_shift. It does not have the germ or tail $\sigma$-fields, Blumenthal's law, the strong Markov property, any path-regularity result, or the Kolmogorov–Chentsov continuity theorem: Probability/Process/Kolmogorov.lean defines IsKolmogorovProcess, the hypothesis, and stops there. So this mission supplies the $\sigma$-fields and then everything Durrett proves with them.

Difficulty

The goal reduces to Durrett's Theorem 7.2.2, that $\mathbb E(Z\mid\mathcal F^{+}_{s})=\mathbb E(Z\mid\mathcal F^{0}_{s})$ for bounded path-measurable $Z$; at $s=0$, $\mathcal F^{0}_{0}=\sigma(B_0)$ is trivial because $B_0=0$ almost surely, so $\mathbf 1_A=\mathbb E(\mathbf 1_A\mid\mathcal F^{+}_{0})=\mathbb P(A)$ almost surely, and an indicator almost surely equal to a constant forces that constant to be $0$ or $1$. Theorem 7.2.2 itself is a monotone class argument on top of the Markov property, and the Markov property in this setting is Mathlib's indepFun_shift plus the observation that the conditional expectation of a product $\prod_m f_m(B_{t_m})$ over $\mathcal F^{+}_{s}$ lands in $\mathcal F^{0}_{s}$. Assembling that is the work.

Theorem 7.2.4 is then three lines — $\mathbb P_0(\tau\le t)\ge\mathbb P_0(B_t>0)=1/2$ by symmetry of the Gaussian, let $t\downarrow0$, apply the goal — provided the event has been shown to lie in the germ field, which is where continuity of paths enters. Theorem 7.2.5 follows from 7.2.4 applied to $B$ and $-B$ together with the intermediate value theorem.

Theorem 7.1.5 needs the Kolmogorov–Chentsov continuity theorem, which has to be built: from $\mathbb E|B_t-B_s|^{2m}=C_m|t-s|^m$ one gets Hölder-$\gamma$ control for $\gamma<(m-1)/2m$, and $m\to\infty$ gives every $\gamma<1/2$. The dyadic chaining and Borel–Cantelli step is the substance, and it is worth building as a general theorem about IsKolmogorovProcess rather than only for Brownian motion.

Theorem 7.1.6 is self-contained and short: fix $C$, let $A_n$ be the event that some $s\in[0,1]$ has $|B_t-B_s|\le C|t-s|$ whenever $|t-s|\le3/n$, and bound $\mathbb P(A_n)\le n\,\mathbb P(|B_1|\le5Cn^{-1/2})^3\le n\{10Cn^{-1/2}(2\pi)^{-1/2}\}^3\to0$; since $A_n$ increases, every $\mathbb P(A_n)=0$.

Theorem 7.2.8 needs the tail 0-1 law, Theorem 7.2.7, which is the goal transported through the time inversion $X_t=tB(1/t)$ — Mathlib's IsPreBrownianReal.inv — because the tail field of $B$ is the germ field of $X$. With that, $\mathbb P_0(B_n/\sqrt n\ge K\ \text{i.o.})\ge\mathbb P_0(B_1\ge K)>0$ by scaling, so the probability is one, and $K$ is arbitrary.

Formalization scope

The process is Mathlib's IsBrownianReal, indexed by ℝ≥0, on an abstract probability space — not the canonical path space $C[0,\infty)$ that Durrett uses. This is why the shift operators $\theta_s$ and the family $\{\mathbb P_x\}$ do not appear: there is one measure, the process starts at $0$ almost surely, and each statement is about that process. Theorem 7.2.7 as Durrett states it quantifies over all starting points and has no direct analogue here; the tail 0-1 law for the process started at $0$ does, and is listed under contributions as the route to Theorem 7.2.8.

The three $\sigma$-fields are built as suprema and infima in the lattice of $\sigma$-algebras on $\Omega$: pastSigma B t is the supremum of the pullbacks of the Borel field along $B_s$ for $s\le t$, and germSigma B, tailSigma B are the corresponding infima. The goal carries the hypothesis that each $B_t$ is measurable, not merely almost-everywhere measurable, which is what IsPreBrownianReal gives and what puts these $\sigma$-fields below the ambient one; the canonical construction satisfies it, and without it "$\mathbb P(A)$" for a germ event would be an outer measure.

Hölder continuity is stated locally — for almost every path, every $T$ admits a constant — since global Hölder continuity on $[0,\infty)$ is false. The order of quantifiers puts the null set first, so a single path works for every $T$ at once.

The hitting statements avoid an infimum over a possibly empty set. "$\tau=0$ almost surely" is written as: almost surely, for every $\epsilon>0$ there is $t\in(0,\epsilon)$ with $B_t>0$; and "$T_0=0$ almost surely" as the same with $B_t=0$. These are equivalent to Durrett's statements and say what the infimum is there to say. Similarly Theorem 7.2.8 is written with ∃ᶠ … in atTop rather than as an extended-real $\limsup$, which is what "$\limsup=+\infty$" means and avoids a coercion.

LipschitzAtPoint f s C is "there is a scale $\delta>0$ on which $|f(t)-f(s)|\le C|t-s|$". Its negation for every $s$ and every $C$ is Theorem 7.1.6, and it has content in both directions: the identity path is Lipschitz at every point with $C=1$, while $t\mapsto\sqrt t$ is not Lipschitz at $0$ with $C=1$ — both checked in Lean before publishing.

Existence is not part of this mission. Mathlib proves nothing of the form "a Brownian motion exists", and nothing here needs it: every item takes a Brownian motion as a hypothesis. That the hypothesis is satisfiable is a theorem — Durrett's 7.1.1, via Kolmogorov extension and the continuity theorem — and it is listed under contributions, where it belongs, since building it is a project of its own.

Contributions welcome beyond the listed items: Kolmogorov–Chentsov as a general statement about IsKolmogorovProcess; Theorem 7.1.1, the existence of Brownian motion; Theorem 7.2.2 in full, for every $s$; the tail 0-1 law and Theorem 7.2.9, recurrence; the strong Markov property and the reflection principle of section 7.3; and Exercise 7.1.5, that no path is Hölder of any exponent $\gamma>1/2$.

Selected references

• Rick Durrett, Probability: Theory and Examples, Version 5 (11 January 2019), chapter 7, sections 7.1 and 7.2 (pp. 353–365); Theorems 7.1.5, 7.1.6, 7.2.3, 7.2.4, 7.2.5, 7.2.8. Published as the 5th edition, Cambridge University Press, 2019, DOI 10.1017/9781108591034
• R. M. Blumenthal, An extended Markov property, Transactions of the American Mathematical Society 85 (1957), 52–72. DOI 10.1090/S0002-9947-1957-0088102-2
• R. E. A. C. Paley, N. Wiener and A. Zygmund, Notes on random functions, Mathematische Zeitschrift 37 (1933), 647–668. DOI 10.1007/BF01474606
• A. Dvoretzky, P. Erdős and S. Kakutani, Nonincrease everywhere of the Brownian motion process, Proceedings of the Fourth Berkeley Symposium II (1961), 103–116.
• N. Wiener, Differential space, Journal of Mathematics and Physics 2 (1923), 131–174. DOI 10.1002/sapm192321131
• I. Karatzas and S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer, 1991, chapter 2. DOI 10.1007/978-1-4612-0949-2

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

Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) studies a network with a fixed set of users, and shows that a decentralized rate control converges to a fair allocation. Chapter 8 asks the question one time scale up. Files finish and their flows leave; new files arrive and new flows appear. The number of flows on each route is therefore itself a random process, and the rate allocation — assumed to settle instantly, since rate control runs much faster than files arrive and depart — depends on it.

The question is whether this system is stable: does the number of flows in progress stay bounded, or does it grow without limit? The answer is the best one could hope for. A weighted $\alpha$-fair allocation, the family that contains proportional fairness, TCP fairness, max-min fairness and throughput maximization as special cases, is stable exactly when the offered load at each resource is below that resource's capacity. No more is required — no condition coupling different resources, no dependence on $\alpha$, no dependence on the topology beyond the loads themselves.

Setting

A network has $J$ resources and $R$ routes with incidence matrix $A$. Let $n_r$ be the number of flows active on route $r$ and $x_r$ the rate given to each of them, so route $r$ consumes $n_rx_r$ at each resource it uses. Flows arrive on route $r$ as a Poisson process of rate $\nu_r$ and carry files that are exponentially distributed with parameter $\mu_r$, so

$$n_r\to n_r+1 \text{ at rate } \nu_r, \qquad n_r\to n_r-1 \text{ at rate } \mu_rn_rx_r(n),$$

and $\rho_r=\nu_r/\mu_r$ is the load on route $r$.

Given weights $w_r>0$ and $\alpha\in(0,\infty)$, the weighted $\alpha$-fair allocation is the solution of

$$\text{maximize } \sum_r w_rn_r\frac{x_r^{1-\alpha}}{1-\alpha} \quad\text{subject to } \sum_{r:j\in r}n_rx_r\le C_j,\ x\ge0, \tag{8.1}$$

with $\sum_r w_rn_r\log x_r$ in place of the objective when $\alpha=1$. Written in the aggregate rates $X_r=n_rx_r$ this becomes

$$\text{maximize } G(X)=\sum_r w_rn_r^{\alpha}\frac{X_r^{1-\alpha}}{1-\alpha} \quad\text{subject to } \sum_{r:j\in r}X_r\le C_j,\ X\ge0. \tag{8.4}$$

The family interpolates between the fairness notions of Chapter 7: $\alpha\to0$ with $w\equiv1$ maximizes throughput, $\alpha=1$ is weighted proportional fairness, $\alpha=2$ with $w_r=1/T_r^2$ is TCP fairness, and $\alpha\to\infty$ with $w\equiv1$ approaches max-min fairness.

Formalization targets

Goal — the drift inequality behind Theorem 8.2

Suppose the load respects every capacity, $\sum_{r:j\in r}\rho_r<C_j$ for all $j$. Then there is an $\epsilon>0$, depending only on the loads and capacities, such that for every flow count $n$ and the $\alpha$-fair aggregate rates $X=X(n)$,

$$\sum_r w_r\rho_r^{-\alpha}n_r^{\alpha}\bigl(\rho_r-X_r\bigr) \;\le\;-\epsilon\sum_r w_rn_r^{\alpha}\rho_r^{1-\alpha}.$$

The left-hand side is the drift of the Lyapunov function $L(n)=\sum_r(w_r/\mu_r)\rho_r^{-\alpha}n_r^{\alpha+1}/(\alpha+1)$, by the identity (8.3); the right-hand side is the book's displayed bound. The single $\epsilon$ is uniform in $n$, which is what a Foster–Lyapunov argument needs, and it is the whole deterministic content of Theorem 8.2's sufficiency half.

Supporting levels

The derivative $w_rn_r^{\alpha}X_r^{-\alpha}$ of the objective, in the same form for every $\alpha\in(0,\infty)$ including $\alpha=1$ (Exercise 8.3); strict concavity of the objective; the characterization of the optimum by $x_r=(w_r/\sum_{j\in r}p_j)^{1/\alpha}$ with primal and dual feasibility and complementary slackness (Exercise 8.4); the tangent-plane inequality (8.5) that concavity gives at the optimum; the drift identity (8.3); and that $\alpha=1$ recovers weighted proportional fairness, connecting this chapter to Proposition 7.4 of mission VII.

Significance

The result itself. Theorem 8.2 says the stability region of an $\alpha$-fair network is the largest it could possibly be — the same region a single isolated resource would have — and that it does not shrink as $\alpha$ varies. That is a strong statement about a large design space, and it is not automatic: section 8.4 of the book exhibits rate allocation schemes for which it fails, so the natural condition (8.2) is a property of $\alpha$-fairness and not of rate allocation in general. Since the family covers the fairness notions actually implemented in transport protocols, the theorem is what licenses treating "is the load below capacity?" as the only capacity-planning question at flow level.

Formalizing it. Nothing here is open; the theorem is due to Bonald and Massoulié (2001), with the fluid-limit machinery from Gromoll and Williams and from Massoulié. What the mission produces is a machine-checked $\alpha$-fair allocation — objective, derivative, concavity, KKT conditions — and the exact drift inequality, on top of the congestion-control layer published in mission VII of this series, whose networkFeasible and linkFlow it reuses. Mathlib has no network utility maximization and no fairness criteria.

Difficulty

The proof is short but the step that makes it work is easy to miss. The drift is $\sum_r w_rn_r^{\alpha}\rho_r^{-\alpha}(\rho_r-X_r)$, and there is no reason for this to be negative term by term — some routes are over-served and some under-served. What makes the sum negative is that $\rho$ is itself a feasible point of the same optimization problem (8.4) that $X$ solves, and $G$ is concave, so the tangent plane at $\rho$ lies above $G$:

$$G'(U)\cdot(U-X)\le G(U)-G(X)\le0 \quad\text{for every feasible } U .$$

Since $G'(U)_r=w_rn_r^{\alpha}U_r^{-\alpha}$, taking $U=\rho$ gives the drift $\le0$ immediately. Strict negativity comes from taking $U=(1+\epsilon)\rho$ instead, which is still feasible because (8.2) is a strict inequality, and then dividing through by $(1+\epsilon)^{\alpha}$. The whole argument is one application of concavity at a cleverly chosen point, and the choice of that point is the content.

The scaling that makes it uniform in $n$ is the other thing to notice: $\epsilon$ depends only on how much slack (8.2) leaves, not on $n$, because $n$ enters $G'$ only through the common factor $n_r^{\alpha}$ that appears on both sides.

Formalization scope

Resources and routes are indexed by finite types, the incidence matrix is real-valued with entries $0$ or $1$, and the feasible set is mission VII's networkFeasible, so Chapters 7 and 8 agree on what a feasible flow vector is. The objective is stated in the aggregate variables $X_r=n_rx_r$ of problem (8.4) rather than the per-flow rates of (8.1): they are equivalent, but (8.4) is the form the drift argument uses and the form in which the feasible set does not depend on $n$.

The objective is defined with an explicit case split at $\alpha=1$, exactly as the book defines it, and the derivative milestone asserts that the resulting derivative has the same form $w_rn_r^{\alpha}X_r^{-\alpha}$ in both cases — which is the point of Exercise 8.3. Powers are real exponents, so positivity of the flow counts, weights, loads and rates is hypothesised wherever a power appears.

What is formalized and what is quoted. Theorem 8.2 is a statement about positive recurrence of a Markov process, proved by a Foster–Lyapunov criterion whose remaining hypotheses the book leaves to Exercises 8.6 and D.2. There is no theory of continuous-time Markov chains on a countable state space in Mathlib to state positive recurrence against, so this mission formalizes the deterministic drift inequality that carries the argument and quotes the probabilistic wrapper. The inequality is exactly the one the book displays, including the $\epsilon$, and the necessity half — that the process is unstable when (8.2) fails — is a coupling argument and is quoted too.

The goal is not vacuous: the hypotheses are satisfiable, and for a single resource of capacity $C$ the $\alpha$-fair optimum is $X_r=Cw_r^{1/\alpha}n_r/\sum_sw_s^{1/\alpha}n_s$, for which the inequality holds with $\epsilon=C/\sum_r\rho_r-1$ and strictly positive slack.

Contributions welcome beyond the listed items: the single-resource equilibrium distribution of Exercise 8.1 and the geometric law of the total number of flows; the bounded-drift estimate of Exercise 8.6; the necessity half of Theorem 8.2; the limiting cases $\alpha\to0$ and $\alpha\to\infty$; and the instability examples of section 8.4.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 8 (pp. 186–199); problem (8.1), Theorem 8.2, equations (8.2)–(8.5). DOI 10.1017/cbo9781139565363
• T. Bonald and L. Massoulié, Impact of fairness on Internet performance, ACM SIGMETRICS Performance Evaluation Review 29 (2001), 82–91. DOI 10.1145/384268.378433
• J. Mo and J. Walrand, Fair end-to-end window-based congestion control, IEEE/ACM Transactions on Networking 8 (2000), 556–567. DOI 10.1109/90.879343
• L. Massoulié, Structural properties of proportional fairness: stability and insensitivity, Annals of Applied Probability 17 (2007), 809–839. DOI 10.1214/105051607000000014
• H. C. Gromoll and R. J. Williams, Fluid limits for networks with bandwidth sharing and general document size distributions, Annals of Applied Probability 19 (2009), 243–280. DOI 10.1214/08-AAP541

Motivation

When many stations share one broadcast channel, something has to decide who transmits. A token passed around the stations works when there are few of them and none is silent for long, but it scales badly and breaks if the token is lost. The alternative is to let stations transmit whenever they like and use randomness to recover from the resulting collisions. That is the design of ALOHA, built in the 1970s to connect terminals across the Hawaiian islands, and of Ethernet, and of essentially every contention-based access protocol since.

Chapter 5 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such protocols can achieve, and the answers are largely negative. ALOHA with a fixed retransmission probability jams: with probability one there is a finite random time after which every slot contains a collision and no packet ever succeeds again, for every positive arrival rate. Ethernet's binary exponential backoff does better, but only just: it has a positive critical arrival rate, above which only finitely many packets are ever transmitted, and it is still not positive recurrent at rates where it does transmit infinitely many. The chapter's general statement is the one this mission targets: any backoff slower than exponential jams at every positive arrival rate.

Setting

Time is slotted, and a transmission attempt occupies exactly one slot. New packets arrive in a Poisson stream of rate $\nu$, so the number arriving in a slot is Poisson with mean $\nu$. A slot in which exactly one station transmits carries its packet successfully; a slot in which two or more transmit is a collision and carries nothing.

In an acknowledgement-based scheme a station learns nothing about the channel except whether its own transmissions succeeded. A packet arriving in slot $t$ attempts transmission in slots $t+x_0, t+x_1, \dots$ with $1 = x_0 < x_1 < \cdots$, the sequence chosen independently for each packet, and

$$h(x) = \mathbb{P}(x \in X), \qquad h(1) = 1$$

is the retransmission function. For ALOHA, $h(x) = f$ for every $x > 1$; for Ethernet's binary exponential backoff, $\sum_{r \le t} h(r) \sim \log_2 t$.

Now imagine the channel externally jammed from time $0$, so that every retransmission actually occurs. The attempts in slot $t$ are then Poisson with mean $\nu\sum_{r=1}^{t}h(r)$, and the probability that fewer than two attempts are made in slot $t$ is

$$P_t=\Bigl(1+\nu\sum_{r=1}^{t}h(r)\Bigr)\exp\Bigl(-\nu\sum_{r=1}^{t}h(r)\Bigr).$$

The expected number of such slots is $H(\nu)=\sum_{t\ge1}P_t$, which is decreasing in $\nu$, and the critical rate is

$$\nu_c=\inf\{\nu : H(\nu)<\infty\}.$$

Theorem 5.11 of the book says $\nu_c$ deserves its name: below it infinitely many packets are transmitted with probability one, above it only finitely many.

Formalization targets

Goal — condition (5.7): slower-than-exponential backoff has $\nu_c=0$

$$\frac{1}{\log t}\sum_{x=1}^{t}h(x)\longrightarrow\infty \quad\Longrightarrow\quad H(\nu)=\sum_{t\ge1}P_t<\infty \ \text{ for every } \nu>0 .$$

Since $H(\nu)<\infty$ for every positive $\nu$, the critical rate is $\nu_c=0$, and by Theorem 5.11 the expected number of successful transmissions is finite at every positive arrival rate. The goal fixes no constant and no rate: it says only that the dividing line between "jams always" and "has a positive capacity" sits at logarithmic growth of $\sum_{x\le t}h(x)$, which is exponential growth of the backoff.

Supporting levels

The ALOHA drift calculation of section 5.1 and its consequence that the drift is positive once the backlog is large enough; the summability $\sum_n p(n)<\infty$ that combines with Borel–Cantelli to give Proposition 5.3; the monotonicity of $P_t$ in $\nu$; the opposite extreme, that a scheme with $\sum_x h(x)<\infty$ — one that gives up on a packet after finitely many attempts — has $\nu_c=\infty$; that ALOHA's own retransmission function satisfies condition (5.7); and the bound of Remark 5.14, that a positive recurrent acknowledgement-based scheme needs $\nu\le e^{-\nu}$ and hence $\nu<0.5672$, which is strictly below Ethernet's $\nu_c=\log 2$.

Significance

The result itself. Condition (5.7) is the chapter's structural statement about random access, and it is a sharp one. Any retransmission rule under which a packet keeps trying at a rate that does not decay fast enough — a fixed probability, a polynomially growing backoff, anything short of exponential — has critical rate zero: the channel jams at every positive load. Exponential backoff is not a tuning choice, it is the minimum that makes the protocol work at all, and the $\log b$ formula for a backoff by factor $b$ (Exercise 5.7) then says how much capacity each choice of $b$ buys. The gap recorded in Remark 5.14 is the other half of the picture: even above the threshold, "infinitely many packets get through" is much weaker than "the backlog is stable", and between $0.567$ and $\log 2 \approx 0.693$ Ethernet does the first and provably not the second.

Formalizing it. None of this is open; the analysis is due to Kelly and MacPhee (1987) and Aldous (1987). What the mission contributes is a machine-checked account of the analytic core: the definitions of $P_t$, $H(\nu)$ and $\nu_c$, the two extremes of the classification, and the ALOHA calculations. Mathlib has no protocol analysis and nothing about random access channels.

Difficulty

The obstacle is a modelling one and it is worth stating plainly rather than discovering halfway through. The chapter's headline results — Proposition 5.3 that ALOHA jams almost surely, Theorem 5.11 that $\nu_c$ is the critical rate, Theorem 5.15 that geometric Ethernet is transient — are statements about sample paths of a Markov chain built on a Poisson arrival stream, and their proofs are coupling arguments comparing a system started empty with one started with a backlog. Nothing in Mathlib supports that construction, and building it is a research-scale project rather than a chapter. This mission therefore formalizes the analytic half and quotes the probabilistic half, which is the same division the book itself makes when it computes $\nu_c$ for a scheme: Theorem 5.11 is proved once, and every subsequent statement about a protocol is a convergence question about $\sum_t P_t$.

Within that analytic half the difficulty is real but ordinary. The summand $P_t$ is a product of a factor growing with $\sum_{r\le t}h(r)$ and one decaying exponentially in it, so the growth hypothesis has to be turned into a summable bound without assuming any regularity of $h$ beyond non-negativity — in particular $\sum_{r\le t}h(r)$ need not be eventually monotone in any useful quantitative sense, only divergent faster than $\log t$.

Formalization scope

The retransmission function is any non-negative real sequence; the normalization $h(1)=1$ is not imposed, since none of the statements need it and imposing it would exclude the comparison schemes. $P_t$ and the partial sums are real-valued, and "$H(\nu)<\infty$" is stated as summability of the sequence rather than as a bound on an extended-real sum, so convergence is asserted rather than assumed. The goal is stated for each fixed $\nu>0$ separately, which is what makes $\nu_c=0$; it is not stated as a claim about the infimum, because the infimum of the set $\{\nu : H(\nu)<\infty\}$ adds nothing once the set is known to be all of $(0,\infty)$.

The growth hypothesis is the book's condition (5.7) verbatim: $\bigl(\log t\bigr)^{-1}\sum_{x\le t}h(x)\to\infty$. Note that at $t=0$ and $t=1$ the quotient involves $\log t \le 0$ and is not meaningful; divergence to infinity is an eventual statement, so this costs nothing, but it is why the hypothesis is a limit rather than a pointwise bound.

The mission is not vacuous in either direction: the ALOHA milestone exhibits a retransmission function satisfying the hypothesis, and the $\sum_x h(x)<\infty$ milestone exhibits one that fails it as strongly as possible, with $H(\nu)=\infty$ for every $\nu$.

Contributions welcome beyond the listed items: Ethernet's $\sum_{r\le t}h(r)\sim\log_2 t$ and the resulting $\nu_c=\log 2$; the generalization $\nu_c=\log b$ of Exercise 5.7; the scheme $h(x)=1/(x\log x)$ with $\nu_c=\infty$; the continuous-time halving $\nu_c=\frac12\log b$ of Kelly and MacPhee; and, for anyone willing to build the probabilistic layer, Proposition 5.3 and Theorem 5.11 themselves.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 5 (pp. 108–132); Definition 5.1, Proposition 5.3, Theorems 5.11 and 5.15, condition (5.7), Examples 5.8, 5.12 and 5.13, Remark 5.14. DOI 10.1017/cbo9781139565363
• N. Abramson, The ALOHA system — another alternative for computer communications, AFIPS Conference Proceedings 37 (1970), 281–285. DOI 10.1145/1478462.1478502
• F. P. Kelly and I. M. MacPhee, The number of packets transmitted by collision detect random access schemes, Annals of Probability 15 (1987), 1557–1568. DOI 10.1214/aop/1176991992
• D. J. Aldous, Ultimate instability of exponential back-off protocol for acknowledgement-based transmission control of random access communication channels, IEEE Transactions on Information Theory 33 (1987), 219–223. DOI 10.1109/TIT.1987.1057295
• R. M. Metcalfe and D. R. Boggs, Ethernet: distributed packet switching for local computer networks, Communications of the ACM 19 (1976), 395–404. DOI 10.1145/360248.360253

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

The final sections of Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) derive the discrete-time Kalman filter (§4.7 Theorem 1, attributed to Kalman 1960) purely from Hilbert space geometry: the optimal estimate of a linearly evolving random state is an orthogonal projection onto the span of past measurements, and the projection updates recursively as measurements arrive. This derivation — no Gaussian assumptions, no density calculations — is a canonical application of the projection theorem formalized in Mission I and the estimation theory of Mission II.

Setting

Following §4.2 and §4.7 of the source, all random variables have zero mean and finite second moments, and are treated as elements of a Hilbert space of random variables: an abstract real inner product space $H$ in which the inner product of two random variables is their correlation, $\langle a, b\rangle = E[ab]$. Random $n$-vectors are families $\mathrm{Fin}\ n \to H$; two random variables are uncorrelated iff they are orthogonal in $H$; the covariance matrix of a zero-mean random vector $x$ is the Gram matrix $\langle x_i, x_j\rangle$. A white process $u$ satisfies $E[u(k)u(l)^\top] = Q(k)\,\delta_{kl}$.

The dynamic model (§4.7) consists of a state process and measurements

$$x(k+1) = \Phi(k)\,x(k) + u(k), \qquad v(k) = M(k)\,x(k) + w(k), \qquad k = 0, 1, 2, \dots$$

with known matrices $\Phi(k) \in \mathbb{R}^{n\times n}$, $M(k) \in \mathbb{R}^{m\times n}$, white noises $u, w$ with covariances $Q(k)$, $R(k)$ ($R(k)$ positive definite), mutually uncorrelated and uncorrelated with the initial state $x(0)$. The estimate $\hat x(k+1 \mid k)$ is the projection of each component of $x(k+1)$ onto the subspace spanned by the components of $v(0), \dots, v(k)$.

Formalization targets

The goal is §4.7 Theorem 1: the estimates generated by the recursion

$$\hat x(k+1 \mid k) = \Phi(k) P(k) M^\top(k)\big[M(k)P(k)M^\top(k) + R(k)\big]^{-1}\big(v(k) - M(k)\hat x(k \mid k-1)\big) + \Phi(k)\, \hat x(k \mid k-1)$$ $$P(k+1) = \Phi(k) P(k)\big\{I - M^\top(k)[M(k)P(k)M^\top(k) + R(k)]^{-1} M(k) P(k)\big\}\Phi^\top(k) + Q(k),$$

started from $\hat x(0 \mid -1) = 0$ and $P(0) = \operatorname{cov} x(0)$, are the linear minimum-variance estimates: each $\hat x(k \mid k-1)$ lies in the span of past measurement components, its error is orthogonal to all past measurements, and its error covariance is $P(k)$.

Milestones: orthogonality of the innovation $v(k) - M(k)\hat x(k\mid k-1)$ to the past-data subspace, and the single-step updating formula (§4.6 Example 1) — given a prior projection with error covariance $R$ and new data $y = W\beta + \varepsilon$, the updated projection is $\hat\beta + RW^\top(WRW^\top + Q)^{-1}(y - W\hat\beta)$ with error covariance $R - RW^\top(WRW^\top+Q)^{-1}WR$.

Significance

The Kalman filter is among the most used algorithms in engineering — navigation, tracking, control, time-series analysis — and this mission gives it a machine-checked correctness statement at the natural level of generality: linear minimum-variance optimality over arbitrary zero-mean second-order processes, with no Gaussian hypothesis. Mathlib currently has no Kalman filter and no linear filtering theory. The abstract Hilbert-space formulation also makes the development directly reusable: the update milestone is a general two-stage projection lemma independent of the dynamic model.

Difficulty

The recursion couples two invariants that must be established simultaneously by induction: the geometric one (the error is orthogonal to the growing measurement subspace, and the estimate lies in it) and the algebraic one (the error Gram matrix equals $P(k)$). Whiteness enters precisely through the index inequalities — $u(k)$ and $w(k)$ are orthogonal to everything generated by $x(0), u(0..k{-}1), w(0..k{-}1)$ — and an off-by-one in these ranges silently breaks the induction. Invertibility of $M(k)P(k)M^\top(k) + R(k)$ must be derived, not assumed: $P(k)$ is positive semidefinite as a Gram matrix and $R(k)$ is positive definite. The naive approach of expanding all projections over a concrete probability space adds measure-theoretic overhead the abstract formulation avoids entirely.

Formalization scope

The Hilbert space of random variables is an abstract H : Type with [NormedAddCommGroup H] [InnerProductSpace ℝ H]; zero means are implicit in this representation (§4.7 assumes all variables zero-mean), so expectations never appear — only inner products. Matrix-vector actions on random vectors are written componentwise as ∑ j, A i j • x j. Processes are indexed by ℕ, with x̂(0 | -1) rendered as xh 0 = 0 and covariances as explicit Gram identities. Whiteness and uncorrelatedness are hypotheses on inner products with if k = l then _ else 0. The span of past data at time $k$ is Submodule.span ℝ {a | ∃ l < k, ∃ j, a = v l j}. The recursion defining xh and P is supplied as hypotheses, so the goal asserts exactly the optimality and covariance claims of the source theorem. Statements deliberately avoid Mathlib's orthogonalProjection; the projection property is asserted by membership plus orthogonality, which characterizes it uniquely.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. §4.6–4.7, pp. 90–97. ISBN 0-471-55359-X.
• R. E. Kalman, A new approach to linear filtering and prediction problems, J. Basic Eng. 82 (1960), 35–45. https://doi.org/10.1115/1.3662552

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