Motivation

A Gaussian process is a family $(X_t)_{t\in T}$ of jointly Gaussian real random variables indexed by an arbitrary set $T$ — not necessarily time. The canonical example is $X_t = \langle g, t\rangle$ for $t$ ranging over a subset $T\subseteq\mathbb R^n$ and $g$ a standard Gaussian vector in $\mathbb R^n$; this single family already encodes questions as varied as the operator norm of a random matrix, the size of a random projection, and the metric complexity of a convex body. In every one of these applications the object of interest reduces to the same quantity: $E\sup_{t\in T} X_t$, the expected supremum of the process.

Bounding $E\sup_{t\in T} X_t$ directly is hard — computing it exactly is possible only in special cases, such as the reflection principle for Brownian motion. Slepian's inequality (David Slepian, 1962) sidesteps this by comparison: if a second Gaussian process $(Y_t)_{t\in T}$ has matching variances and at-least-as-large pairwise increments as $(X_t)_{t\in T}$, then $Y$'s supremum stochastically dominates $X$'s. This turns a hard direct estimate into a search for a simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely geometric lower bound on $E\sup_{t\in T}X_t$ from the covering numbers of $(T,d)$ (Theorem 7.4.1, Sudakov's minoration inequality). Together these results are the entry point to the theory of Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer, 2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random process indexed by a set $T$ is a family $(X_t)_{t\in T}$ of real random variables on $\Omega$. It is a Gaussian process if every finite linear combination $\sum_{t\in T_0} a_t X_t$ ($T_0\subseteq T$ finite, $a_t\in \mathbb R$) is a (possibly degenerate) normal random variable — equivalently, every finite marginal $(X_t)_{t\in T_0}$ is a multivariate Gaussian vector. A process is mean zero if $EX_t = 0$ for every $t$.

For a mean zero process, the increments $d(t,s) := \lVert X_t - X_s\rVert_{L^2} = (E(X_t - X_s)^2)^{1/2}$ always define a (pseudo)metric on $T$ — the canonical metric — turning the otherwise unstructured index set into a metric space. For a metric space $(T,d)$ and $\varepsilon

0$, the **covering number**$N(T,d,\varepsilon)$is the smallest cardinality of a finite subset$N\subseteq T$such that every point of$T$is within$\varepsilon$of some point of$N$(an$\varepsilon$-net);$N(T,d,\varepsilon) := \infty$ if no finite net exists.

Because $T$ need not be countable, $\sup_{t\in T} X_t(\omega)$ need not be a measurable function of $\omega$. Following the book's own convention, every quantity built from this supremum — $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ — is instead defined through the process's finite-dimensional marginals: as the supremum, over finite nonempty $T_0\subseteq T$, of $E\max_{t\in T_0}X_t$ (respectively $P\{\max_{t\in T_0}X_t\ge\tau\}$). This sidesteps the measurability question entirely, at the cost of the quantity possibly being $+\infty$.

Formalization targets

Slepian's inequality (Theorem 7.2.1, goal)

Let $(X_t)_{t\in T}$ and $(Y_t)_{t\in T}$ be mean zero Gaussian processes with $EX_t^2 = EY_t^2$ and $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ for all $t,s\in T$. Then for every $\tau\in\mathbb R$,

$$P\{\sup_{t\in T} X_t \ge \tau\} \le P\{\sup_{t\in T} Y_t \ge \tau\},$$

and consequently $E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t$.

Sudakov-Fernique's inequality (Theorem 7.2.11, milestone)

Under only the increment hypothesis $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ (no equal-variance hypothesis),

$$E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t.$$

This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.

Sudakov's minoration inequality (Theorem 7.4.1, milestone)

Let $(X_t)_{t\in T}$ be a mean zero Gaussian process with canonical metric $d$. For every $\varepsilon\ge 0$ at which $N(T,d,\varepsilon)=:N$ is finite,

$$E\sup_{t\in T} X_t \ge c\,\varepsilon\,\sqrt{\log N}$$

for an absolute constant $c>0$. This is the weakest, most stable form of the bound: it names no numerical value for $c$, so it survives any later sharpening of the constant.

Slepian's inequality, finite-dimensional case (Theorem 7.2.9, milestone)

The vector-indexed special case of Theorem 7.2.1 ($T$ finite), proved first by Gaussian interpolation and then extended to the general index set.

Significance

The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used routinely to bound suprema of Gaussian processes without needing to track variances explicitly. Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and together giving matching bounds — up to a logarithmic factor, and exactly in many cases of interest — on $E\sup_{t\in T}X_t$ purely from the covering numbers of $(T,d)$. Downstream, this machinery gives the sharp bound $E\lVert A\rVert \le \sqrt m + \sqrt n$ on Gaussian random matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other convex sets (Corollary 7.4.4).

Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing the statements faithfully and precisely — including the finite-marginal convention needed to make $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ meaningful for an uncountable index set without begging the underlying measurability question. The Gaussian interpolation technique itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the proof method for the milestones and belongs to solvers closing them.

Difficulty

The obvious first idea — bound $E\sup_t X_t$ by controlling each $X_t$ separately, e.g. via a union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the joint Gaussianity across $t$, not marginal tail behavior at each fixed $t$. A union bound needs a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities need neither — they compare two processes directly through their covariance structure, which is what makes the technique (Gaussian interpolation: continuously deform the covariance of one process into the other's, and track how a smooth, nearly-indicator functional behaves along the path) work with no assumption on $T$ beyond the two hypotheses stated. The genuine difficulty is the smooth-interpolation argument itself — showing that $E f(Z(u))$ is monotone in $u$ for the right choice of test function $f$ — which is exactly the part left as a milestone for solvers to formalize, not sketched here per the mission format's own rule against proof ideas.

Formalization scope

$E\sup_{t\in T}X_t$ (ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a real-valued definition would silently default to the junk value $0$ when the set of finite-marginal expectations is unbounded above — exactly the case the book itself records as $E\sup_{t\in T}X_t=\infty$ (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\} (ProcessTailProb) stays real-valued, since it is always bounded in $[0,1]$ and so carries no such risk. Both are defined through finite nonempty subsets of $T$, per the book's own footnote to Section 7.2; no separability, continuity, or countability assumption is placed on $T$ itself.

Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it. Integrability of every quantity appearing under an expectation is not stated as a separate hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a Gaussian process has finite moments of every order, exactly as the book takes for granted.

Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof actually covers — $N(T,d,\varepsilon)$ finite, taken as a hypothesis = (N : ℕ) rather than as a case split inside the conclusion — since the book itself defers the infinite-covering-number case to a separate, unproved exercise (7.4.2). This keeps $T$ fully general (still possibly uncountable) at every fixed $\varepsilon$ where the net is finite, which rules out a trivializing reading of the theorem: nothing here forces $T$ itself to be finite or countable, only the covering number at the scale $\varepsilon$ in play, which is the book's own hypothesis.

Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric, and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9 ("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian width and generic chaining; per this series' plan those missions restate them locally (drafts cannot import another draft's definitions), using this chunk's forms as the faithful reference. Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable definitions layer, beyond what any one milestone needs, are welcome.

Selected references

• Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018. https://www.math.uci.edu/~rvershyn/papers/HDP-book/HDP-book.pdf
• D. Slepian, "The one-sided barrier problem for Gaussian noise", Bell System Technical Journal 41 (1962), 463–501.
• V. N. Sudakov, "Gaussian random processes and measures of solid angles in Hilbert space", Soviet Mathematics Doklady 12 (1971), 412–415.
• X. Fernique, "Regularité des trajectoires des fonctions aléatoires gaussiennes", in École d'Été de Probabilités de Saint-Flour IV-1974, Springer Lecture Notes in Mathematics 480 (1975), 1–96.
• M. Talagrand, Upper and Lower Bounds for Stochastic Processes: Modern Methods and Classical Problems, Springer, 2014.

Motivation

Most stochastic programs cannot be solved exactly: the expectation defining the objective is an integral over a continuous or high-dimensional random parameter, and evaluating it exactly is as hard as the optimization itself. The standard remedy is Monte Carlo: draw a sample of size ν from the random parameter, replace the true expectation by the sample average, and solve the resulting finite-dimensional "sample average approximation" (SAA) instead. This only helps if the SAA's optimal value and optimal solution actually converge to the true problem's as ν → ∞, and if that convergence is fast enough to be useful with a sample size one can actually draw and solve. Birge & Louveaux's Chapter 9, §9.5, states the two central asymptotic results that justify this approach for a general (not necessarily linear, not necessarily two-stage) stochastic program: a central limit theorem describing the SAA optimal value's fluctuations around the truth (Theorem 6, after Shapiro [1991]), and an exponential-rate large-deviation bound on how quickly both the SAA value and the SAA solution concentrate near their true counterparts as the sample grows (Theorem 7, after Dai, Chen & Birge [2000]). This mission formalizes both statements.

Setting

Fix a feasible set X ⊆ ℝⁿ of first-stage decisions and an outcome space Ξ carrying a σ-algebra. The book considers the general stochastic program

z* = inf_{x ∈ X} ∫_Ξ g(x,ξ) P(dξ),                                                        (5.1)

with g : ℝⁿ × Ξ → ℝ an abstract integrand — no longer specialized to the two-stage recourse cost Q(x,ξ) of Chapters 3–7, matching the book's own level of generality at this point in §9.5 — and ξ a random element of (Ξ, 𝓑, P). Given an i.i.d. sample ξ₁, ξ₂, … from P, the sample average approximation of size ν is

zν = inf_{x ∈ X} (1/ν) Σᵢ₌₁^ν g(x,ξᵢ) .                                                    (5.2)

Both z* and zν are attained (an optimal solution x* of (5.1); a random optimal solution xν(ω) of (5.2) at each sample outcome ω). The two chapter results describe, in different regimes, how (zν, xν) relates to (z*, x*) as ν → ∞.

Formalized in this mission: X sits in EuclideanSpace ℝ (Fin n); the sample is a sequence ξ : ℕ → Ω → Ξ on an ambient probability space (Ω, P), independent and identically distributed (Mathlib's iIndepFun/IdentDistrib); z*, x*, zν, xν are given as hypotheses that pin them down as the optimal value and an optimal point of (5.1)/(5.2) (a lower bound over X plus attainment at the named point), rather than computed via sInf/sSup of an image set — Real's extended-real infimum returns the junk value 0 on an unbounded-below or empty set, which would silently misstate the theorems if X, g are only assumed as loosely as the book states them.

Formalization targets

Goal — Chapter 9, Theorem 7 (p. 412)

∀ ε>0, ∃ α>0, ∃ β>0,
  (∀ ν>0, P[|zν − z*| ≥ ε] ≤ α·e^{−βν})
  ∧ (x* the unique optimal solution of (5.1) → ∀ ν≥1, P[‖xν − x*‖ ≥ ε] ≤ α·e^{−βν})

under the moment hypothesis: there exist a>0, θ₀>0, η : Ξ → ℝ with |g(x,ξ)| ≤ a·η(ξ) for all x ∈ X, and E[e^{θ·η(ξ)}] < ∞ for every θ ∈ [0,θ₀]. This is the mission's goal because it is a clean, self-contained existential-constants statement — no algorithm to define, unlike most of the chapter's other convergence results — and because, like Chunk 03's Theorem 6(a), the book's own proof cites an external paper (Dai, Chen & Birge [2000], Theorems 3.1–3.2) and gives no in-text derivation: the statement itself, not a derivation from a preceding numbered result of this book, is the mission's content.

Milestone — Chapter 9, Theorem 6 (p. 411)

X compact, g(x,·) measurable ∀x∈X, g Lipschitz in x with an L²(μ) envelope a,
x0 the unique minimizer of x ↦ E g(x) over X
  ⟹ √ν·[zν − E g(x0)] converges in distribution to N(0, Var g(x0))

Included as a milestone (not used in Theorem 7's proof, which the book does not give — see above) because it is the chapter's other general SAA convergence result, standing on the same setup (5.1)–(5.2), and because Mathlib's MeasureTheory.Function.ConvergenceInDistribution (the TendstoInDistribution predicate) plus Probability.Distributions.Gaussian.Real (gaussianReal) and Mathlib's own i.i.d. central limit theorem (ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub) supply exactly the vocabulary needed to state — not prove — a faithful weak-convergence-to-Gaussian conclusion. Chunk 09's BRIEF.md flagged this as a milestone to attempt "only if your workspace has enough of a weak-convergence/CLT toolkit in Mathlib to state it faithfully"; the toolkit is present (verified directly, not assumed from substrate.md, which predates this rev's addition of ConvergenceInDistribution.lean), so it is included.

Significance

Every practical Monte Carlo solution method for stochastic programming — every discretization, every scenario-reduction heuristic, every "solve on a sample and hope" approach used throughout the rest of the book and the wider literature — rests on exactly these two results: that the SAA converges at all (Theorem 6's CLT gives the asymptotic distribution of the error) and that it converges fast enough to bound the error at a finite, computable sample size (Theorem 7's exponential rate). Formalizing them gives Prove2Me a first foothold in convergence-rate theory for stochastic optimization under sampling, a genre distinct from the concentration-of-measure results already reachable via Mathlib's sub-Gaussian machinery (Probability/Moments/SubGaussian.lean): sub-Gaussian concentration bounds a fixed-size sample's deviation from its own mean, not the rate-in-ν convergence of a nested sequence of optimization problems' values and solutions to a limiting problem's — the object Theorem 7 is actually about.

Difficulty

Theorem 6 needs a functional/uniform argument over the whole feasible set X (not the plain i.i.d. CLT at the single point x0) to control the interaction between sampling noise and the optimization over x; the book states it without proof, citing Shapiro [1991]. Theorem 7's constants α, β are produced by a large-deviation argument specific to the exponential-moment condition, again cited rather than derived in the book. Both are left as sorry; the value of this mission is the faithful statement, matching the difficulty pattern already established for Chunk 03's Theorem 6(a) (a result the book itself only cites).

Formalization scope

• Existential constants left abstract, never sharpened or weakened. Theorem 7's α, β are ∃-bound exactly as the book leaves them (trap 8 of reference/FAITHFULNESS_TRAPS.md: the existentials sit outside every quantifier they must be uniform over — in particular outside the ∀ ν). No closed form for α, β in terms of a, θ0, ε is invented.
• The book's own typo is corrected, and the correction is flagged. The printed (5.8) reads P[E[zν − z*)] ≥ ε] ≤ αe^{−βν} — an unmatched parenthesis and a stray E[·] around a quantity that is already deterministic. milestones.yaml/MODERATION_NOTES.md quote the typo verbatim; the Lean and natural_language_statement use the unambiguous P[|zν − z*| ≥ ε] the surrounding prose (and every other occurrence of this quantity in the section) plainly intends.
• g is left fully abstract, not specialized to the two-stage recourse cost Q(x,ξ) of Chunks 03–07, matching §9.5's own generality and keeping this mission independent of every other chunk's namespace (no cross-chunk import, per missions/README.md's "Prior art" column for this chunk: "none expected").
• z*, x*, zν, xν are hypothesis-characterized, not sInf/sSup-defined, to avoid the real extended-value junk-value trap (trap 5) discussed under Setting above.
• Measurability of zν, xν is an added hypothesis (hzSAA_meas/hxSAA_meas/hzSAA_meas in Theorem 6), not derivable from the other hypotheses since g is abstract; the book is silent on this technical point, standard for an applied convergence theorem, but Lean's P {ω | …} needs it for the displayed probability to be the actual measure of the event rather than an outer-measure value on a possibly non-measurable set.
• Convergence in distribution (Theorem 6) is formalized via Mathlib's TendstoInDistribution, with the limiting Gaussian supplied as an explicit random variable Y on a separate probability space with HasLaw Y (gaussianReal 0 σ²) P' — the same pattern Mathlib's own CLT (tendstoInDistribution_inv_sqrt_mul_sum_sub) uses for its own conclusion.
• Trivialization risk (this chapter's own, beyond paper.md's book-wide list item 5). A formalization that quantifies α, β universally, or with an invented closed form, would assert something the book's proof (cited, not given) does not establish; a formalization of Theorem 7 that used a computable sInf-defined zν on a set that is not shown bounded below would let the conclusion hold vacuously via the junk value 0, independent of the genuine large-deviation content — both are excluded by the choices above.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 9, §9.5 (pp. 409–412).
• Shapiro, A. "Asymptotic properties of statistical estimators in stochastic programming." Annals of Statistics 19 (1991), 1463–1466 — proof of Theorem 6 (their Theorem 3.3).
• Dai, L., Chen, C.-H., Birge, J.R. "Convergence properties of two-stage stochastic programming." Journal of Optimization Theory and Applications 106 (2000), 489–509 — proof of Theorem 7 (their Theorems 3.1–3.2).
• King, A.J., Rockafellar, R.T. "Asymptotic theory for solutions in statistical estimation and stochastic programming." Mathematics of Operations Research 18 (1993), 148–162 — the general theory of §9.5's opening (Theorem 5), the chapter's third general result, not formalized here (see STATUS.md for why it is out of scope).

Motivation

Sequential planning problems — inventory replenishment, hydro-thermal power scheduling, asset-liability management — routinely span more than two decision epochs, with information about the future revealed gradually as each period unfolds. A two-stage recourse model (decide now, observe once, recourse once) is too coarse for these: it either collapses the whole horizon into a single "wait and see" observation or forces an ad-hoc rolling-horizon heuristic with no optimality guarantee. The multistage stochastic program is the natural model that keeps the full sequence of decisions and observations, and Benders (L-shaped) decomposition is the workhorse algorithm the field has used to solve it since Van Slyke and Wets [1969] introduced it for the two-stage case. Ho and Manne [1974] and Glassey [1973] first proposed nested decomposition for deterministic multistage models; Louveaux [1980] extended it to multistage quadratic stochastic programs, and Birge [1985] gave the linear multistage generalization this mission formalizes, later implemented at scale by Pereira and Pinto [1985] and Gassmann [1990] and still the basis of production stochastic-programming solvers today.

Setting

A multistage stochastic linear program unfolds over $H$ stages $t = 1,\dots,H$. At each stage, uncertainty resolves into one of finitely many realizations, so the whole process of realizations forms a scenario tree: a single scenario at $t=1$ (the root), branching into finitely many scenarios at $t=2$, each of those again branching at $t=3$, and so on. Write $k$ for a scenario (a tree node) and $a(k)$ for its ancestor, the scenario at stage $t-1$ that $k$ descends from; $D^{t+1}(j)$ is the set of scenario $j$'s descendants at the next stage. Each scenario $k$ at stage $t$ carries its own decision vector $x^t_k \ge 0$, bounded above ($x^t_k \le u^t_k$, coordinatewise), subject to the linear constraint

$$W^t x^t_k = h^t_k - T^{t-1}_k x^{t-1}_{a(k)},$$

where the recourse matrix $W^t$ depends only on the stage (fixed recourse) while the transition matrix $T^{t-1}_k$ and right-hand side $h^t_k$ may vary scenario by scenario. Stacking every scenario's constraint over the whole tree gives the deterministic equivalent linear program, minimizing the probability-weighted total cost $\sum_k p_k (c^t_k)^\top x^t_k$ over this feasible region — problem (3.4.1) in the source.

The nested L-shaped method solves (3.4.1) by decomposition rather than forming this (typically enormous) single LP directly. Each scenario $k$ owns a small subproblem, $\mathrm{NLDS}(t,k)$, that looks exactly like a two-stage L-shaped subproblem: it has $k$'s own constraint and bound, plus a running set of feasibility cuts and optimality cuts accumulated so far, plus, if $k$ has descendants, an approximation variable $\theta^t_k$ standing in for the (unknown, convex, piecewise-linear) future cost $Q^{t+1}_k$ of everything downstream of $k$. Solving $\mathrm{NLDS}(t,k)$ either finds it infeasible — in which case a feasibility cut is derived from the infeasibility certificate and sent up to $k$'s parent — or finds an optimal dual solution, whose aggregate over all of $j$'s children (weighted by conditional probability) becomes a candidate optimality cut for $j = a(k)$. The method sweeps forward and backward across the tree, feasibility and optimality cuts accumulating at every internal node, until no node's subproblem produces a fresh cut.

Formalization targets

Goal (Chapter 6, Theorem 1)

$$\text{if every }\Xi_t\text{ is finite and every }x_t\text{ has a finite upper bound, then the nested L-shaped method}$$ $$\text{converges finitely to an optimal solution of the deterministic equivalent (3.4.1), or correctly certifies its infeasibility.}$$

This is the chapter's only numbered result and the weakest faithful statement of "the method works": it makes no claim about the number of iterations beyond finiteness, and none about which sequencing protocol (forward-forward-back, or any other) is used to choose which subproblem to solve next.

Significance

Finite convergence is what separates an algorithm from a heuristic: without it, nothing rules out an infinite sequence of ever-finer cuts that never certifies optimality or infeasibility. Birge's 1985 result is the reason nested Benders decomposition can be used as an exact method rather than an approximation, and every later refinement (bunching, sifting, multicuts, parallel implementations, all mentioned in the source text) modifies how cuts are generated or which subproblem is solved next without touching this finiteness guarantee — they are all still instances of the same cut-generation mechanism this mission formalizes. The two-stage case (Chapter 5, Theorem 2) is the $H=2$ special case of this theorem; the mission's tree-indexed state and transition relation are written to specialize to the two-stage development directly when the tree has one branching level, though the two developments are not connected by an import (see Formalization scope). No machine-checked proof of either the two-stage or multistage case appears to exist prior to this series; formalizing it here produces the first Lean statement of the mechanism nested Benders decomposition rests on.

Difficulty

The obvious first idea — prove finiteness by bounding the total number of cuts a node can ever receive, the way a flat scenario set bounds the two-stage method's cut count by its number of LP bases — fails because a node's own subproblem is not a fixed-size LP: every cut recorded at node $k$ becomes a new row of $k$'s own constraint set, so the "number of possible bases" at $k$ keeps changing as the algorithm runs, and the bound at $k$ depends recursively on how many cuts $k$'s own children could ever produce. The book's actual argument (p. 290) is a genuine induction on the stage index, from the last stage backward: assume the bound holds for every node at stage $t+1$, then combinatorially bound the finite number of extended bases at stage $t$ that this permits, then take the finite union over every possible extension size. This mission's Lean development commits to a scope that keeps a node's basis a fixed-size object (see below) rather than re-deriving that combinatorial bound.

Formalization scope

Every stage shares one decision dimension $n$ and one constraint dimension $m$ (Fin n, Fin m); the book allows these to vary by stage but nothing in Theorem 1's statement needs that generality. Scenario probabilities p are the unconditional probability of reaching a node, required strictly positive and summing to $1$ within each stage (Instance.hp_pos, Instance.hp_sum); the aggregation formulas use only the ratio $p_k/p_j$ for $k$ a child of $j$, which reads the same whether p is unconditional or conditional, so this is a normalization choice, not a substantive restriction. The upper bound ub is ℝ-valued rather than extended-real-valued, which is Theorem 1's own hypothesis ("finite upper bounds"), not an added convention.

The one deliberate scope-narrowing choice, flagged here and in MODERATION_NOTES.md, and strengthened in this revision after moderator review (2026-09-19, CHANGES_REQUESTED.md #2): a node $k$'s dual witness (Basis, FeasBasis) is read off $k$'s original constraint (1.2) alone — the fixed-size recourse matrix $W^{\mathrm{stage}(k)}$ — never off the extended constraint set (1.2)-(1.4). The gap this leaves is broader than "accumulated cuts are ignored": $k$'s own continuation variable $\theta_k$ — present in (1.1)'s objective, and fixed to $0$ from Step 0 onward, not merely absent until cuts accumulate — has no representation at all in Basis, multiplier, basisValue, or the optimality-cut coefficients optCutCoeffs computes for a parent $j$ of $k$. Consequently, whenever a child $k$ used in an optimality cut is itself an interior node ($k$ has children of its own, i.e. $\mathrm{stage}(k) < H-1$, which happens for every $H \geq 3$ tree), the mechanized cut coefficients are not the book's $(E^{t-1}_j, e^{t-1}_j)$ of Eq. (1.1) and are not the printed algorithm's mechanism at that node — they are the dual of $k$'s plain sub-LP alone, omitting $k$'s own contribution to the recourse value entirely, not only the portion contributed by $k$'s accumulated cuts. This gap is inert exactly when every child aggregated in a cut is a last-stage node ($H \le 2$, where the mechanism coincides with the already-published two-stage sibling 05-two-stage-methods) and active for every deeper cut, which is most of what a general Tree H actually exercises. Concretely: as mechanized, the optimality-cut half of Step (Bases.optCutCoeffs, Step.opt) is faithful to the printed nested L-shaped method's cut-generation step only when every child it aggregates over is a last-stage node; for an interior child it computes a value that omits that child's own $\theta$ term rather than the book's recursive one. The feasibility-cut half (Bases.feasCutCoeffs, Step.feas) has no such gap — feasibility does not involve $\theta$ at any stage — and the tree/instance layer (Tree, Instance) and the goal theorem's own outer shape are unaffected: thm1_finite_convergence's statement (existence of a finite, Step-reachable state that is infeasible-certified or globally optimal) is not weakened, but the reader should treat the mechanized Step relation itself, for H ≥ 3, as a documented variant of Steps 1-2 rather than a literal transcription of them at every node — see STATUS.md's Revision section for the moderator exchange this responds to. Reworking cut generation to consume each child's own current $(x_k, \theta_k)$ witness directly, so that an interior child's continuation value is no longer dropped, is left to a future revision; it is a materially larger change (the child's local optimum is then piecewise-linear rather than linear in its own parent's decision, so the duality argument needs a genuinely different — not merely extended — basis notion) than this session's time budget allows. This keeps every basis type a fixed-size Fin m → Fin n object, exactly as in the two-stage method, and keeps the algorithm's finite-step bound an explicit, provable cardinality (|Node × FeasBasis| + |Node → Basis|) rather than the book's own implicit, recursively-defined one. The trivializing formalization this scope choice must not fall into — declaring victory by proving the plain two-stage case is what convergence "reduces to" without ever quantifying over the tree — is avoided because every definition and the goal statement itself are stated for a general Tree H with unrestricted branching, not merely $H = 2$; what is disclosed above is a gap in how faithfully Step models the book's own cut-generation mechanism at depth, not a restriction of the statement to $H = 2$.

Reusable beyond this mission: Def_StochasticProg_Multistage_Tree (the finite scenario tree) is a natural building block for 07-integer-programs (an integer restriction of the same two-stage subproblem) and 10-multistage-approximations (multistage Jensen bounds, which need the same tree). Contributions welcome: a faithful account of the extended-basis induction sketched above, and a formalization of Chapter 6, Theorem 3 (finite termination of the quadratic nested decomposition of Section 6.2), which this mission omits for time (see STATUS.md).

Selected references

• J.R. Birge, "Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs", Operations Research 33(5), 1985.
• R.M. Van Slyke, R. Wets, "L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming", SIAM Journal on Applied Mathematics 17(4), 1969. https://doi.org/10.1137/0117061
• H.I. Gassmann, "MSLiP: A Computer Code for the Multistage Stochastic Linear Programming Problem", Mathematical Programming 47, 1990. https://doi.org/10.1007/BF01580858
• M.V.F. Pereira, L.M.V.G. Pinto, "Stochastic Optimization of a Multireservoir Hydroelectric System: A Decomposition Approach", Water Resources Research 21(6), 1985. https://doi.org/10.1029/WR021i006p00779
• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

A micron-sized bead suspended in water and held by an optical tweezer is one of the standard measuring instruments of soft-matter physics: the bead's fluctuating position reports on the viscosity of the medium, on the stiffness of the trap, and on the forces exerted by whatever is attached to the bead. The quantity that experiments record is the mean-squared displacement (MSD) $\langle r^2 \rangle (t)$ of the bead. Interpreting such data rests on a single classical calculation, due to Paul Langevin (1908): write Newton's second law for the bead including the drag of the fluid, the trap force and the fluctuating force of the molecular environment, multiply the equation by the position, and average over realizations. What comes out is a closed, deterministic, second-order ordinary differential equation for $\langle r^2 \rangle$ — no stochastic calculus required. This mission formalizes exactly that derivation, and the solution of the resulting equation, for a particle in a harmonic trap.

Setting

A particle of mass $m > 0$ moves in $d$ Cartesian dimensions. Its position at time $t \in \mathbb{R}$ is the vector $r(t)$ with components $x_i(t)$, $i = 1,\dots,d$; its velocity components are $v_i(t) = \dot{x}_i(t)$ and its acceleration components $a_i(t) = \dot{v}_i(t)$. The particle feels three forces: a hydrodynamic drag $-\zeta \dot{r}$ with drag coefficient $\zeta$; a harmonic trap force $-k r$ with spring constant $k$; and a random force $f(t)$ exerted by the surrounding medium, which is held at temperature $T$. Newton's second law then reads

$$m \ddot{r}(t) = -\zeta \dot{r}(t) - k\, r(t) + f(t).$$

A single solution of this equation, for one realization of the random force, is called a path. An ensemble is a probability space $(\Omega,\mu)$ of such paths, and the ensemble average of a quantity $A$ is $\langle A \rangle = \int_\Omega A \, d\mu$. Two physical inputs single out a thermal environment: the random force is uncorrelated with the instantaneous position, $\langle r \cdot f \rangle = 0$, and the velocity obeys equipartition, $m \langle \dot{r}^2 \rangle = d\, k_B T$ with $k_B$ Boltzmann's constant. The mean-squared displacement is $M(t) = \langle r(t)^2 \rangle$.

Formalization targets

Goal — the MSD equation

$$m \ddot{M}(t) + \zeta \dot{M}(t) + 2 k\, M(t) = 2 d\, k_B T , \qquad M(t) = \langle r(t)^2 \rangle .$$

This is the weakest stable form of the result: it fixes no initial condition, no sign convention on the roots, and no regime (inertial or overdamped), and every later statement about the MSD of a trapped Brownian particle is a consequence of it.

Milestone level — the pathwise identity

For each realization, with $S = r^2$,

$$\tfrac{m}{2} \ddot{S} + \tfrac{\zeta}{2} \dot{S} + k\, S = m\, \dot{r}^2 + r \cdot f ,$$

which is Newton's equation contracted with $r$ and rewritten using $r \cdot \dot r = \tfrac12 \dot S$ and $r \cdot \ddot r = \tfrac12 \ddot S - \dot r^2$.

Milestone level — the explicit solution

With $\lambda_\pm$ the two distinct roots of $m\lambda^2 + \zeta\lambda + 2k = 0$,

$$M(t) = \frac{d\,k_B T}{k} \left[ 1 + \frac{\lambda_- e^{\lambda_+ t} - \lambda_+ e^{\lambda_- t}} {\lambda_+ - \lambda_-} \right]$$

solves the goal equation with $M(0) = \dot M(0) = 0$, and in the inertialess (overdamped) case the solution reduces to $M(t) = \frac{d k_B T}{k}\left(1 - e^{-2kt/\zeta}\right)$, which grows as $2 d (k_B T/\zeta) t$ at short times and saturates at the equipartition plateau $d k_B T / k$.

Significance

The MSD equation is what converts a measured displacement trace into physical numbers: its plateau $d k_B T/k$ calibrates trap stiffness, its short-time slope gives the diffusion coefficient $D = k_B T/\zeta$, and the crossover between the two identifies the relaxation time $\zeta/(2k)$. The derivation is also the historical template for treating noisy dynamics without a theory of stochastic integrals: Langevin's move of averaging the equation multiplied by $r$ is what makes the noise term drop out.

Formalizing it produces a machine-checked statement of the classical calculation together with the assumptions it actually needs, each of which is carried explicitly as a hypothesis rather than left implicit in the prose: interchange of ensemble averaging with time differentiation, integrability of the averaged quantities, decorrelation of the random force from the position, and equipartition. The pathwise identity and the solution-verification statements are elementary calculus; the substance of the mission is that the physical derivation is faithful once those hypotheses are written down.

Difficulty

The obvious route — solve the stochastic equation for $r(t)$ and then square and average — requires a theory of stochastic integration against the random force, whose statistics the problem never specifies beyond the two averaged facts above. Langevin's derivation avoids this entirely, but the step "average the equation" hides two real assumptions: that $\langle \cdot \rangle$ commutes with $d/dt$ (so that $\langle \ddot{S}\rangle$ is the second derivative of $M$), and that $\langle r \cdot f \rangle$ vanishes at every time. Neither follows from the equation of motion; both must be hypotheses, and stating them precisely without weakening the theorem into vacuity is the formalization problem.

Formalization scope

Paths are represented in components: position, velocity, acceleration and force are families $x, v, a, f : \mathrm{Fin}\ d \to \mathbb{R} \to \mathbb{R}$, and the model predicate records that $v$ is the derivative of $x$, that $a$ is the derivative of $v$, and that Newton's law holds at every time, so no differentiability is smuggled in. Euclidean contractions are the single helper $\mathrm{dotSum}\ d\ u\ w\ t = \sum_i u_i(t) w_i(t)$, so that $r^2$, $r\cdot\dot r$, $\dot r^2$ and $r \cdot f$ are all instances of one definition. Ensembles are an arbitrary probability space with the integral as average, and paths are indexed by the sample point; the averaging assumptions appear as hypotheses relating $M$ and its derivatives to integrals of the pathwise quantities. Dimension $d$ is arbitrary, the source's $d = 3$ being a special case.

No hypothesis of the goal is vacuous: a deterministic ensemble (one path, a Dirac measure) with $f \equiv 0$ and a particle at rest satisfies all of them when $k_B T = 0$, and nondegenerate instances exist for every choice of parameters, so the statement is not satisfied only in an empty context. All statements target real-valued time and real coefficients; no positivity of $m$, $\zeta$, $k$ is assumed except where a milestone needs it for an asymptotic claim.

Selected references

• P. Langevin, Sur la théorie du mouvement brownien, C. R. Acad. Sci. Paris 146 (1908), 530–533. English translation: D. S. Lemons and A. Gythiel, Paul Langevin's 1908 paper "On the Theory of Brownian Motion", American Journal of Physics 65 (1997), 1079–1081. https://doi.org/10.1119/1.18725
• Nonequilibrium Statistical Physics, Honour School of Mathematical and Theoretical Physics Part C, Trinity Term 2018 examination paper A15282W1, Question 1.

Motivation

Reflection positivity turns a factorized weight across a reflection plane into a positive-semidefinite kernel of observables. The first mission in this series certified that finite split-weight mechanism and its two-observable chessboard inequality. A physical finite-volume Gibbs model needs one more layer before it can consume those results: its unnormalized weight must have a strictly positive partition function, normalization must preserve the split representation, and the hypotheses used for probability normalization must not be confused with those used for reflection positivity.

This mission isolates that finite algebraic layer. It does not present the results as new mathematics; its purpose is to make the interfaces and their failure modes explicit enough for later clock and XY consumers.

Setting

Let $X$ be a finite half-configuration space and let a full configuration be $(x,y)\in X\times X$. A split weight is

$$W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y),$$

where $A$ is finite, $c_a\in\mathbb R$, and $\phi_a:X\to\mathbb R$. Its partition function and normalized weight are

$$Z=\sum_{x,y\in X}W(x,y),\qquad \widehat W(x,y)=\frac{W(x,y)}{Z}.$$

For observables $F_i:X\to\mathbb R$, define the reflected kernel

$$K_{ij}=\sum_{x,y\in X}\widehat W(x,y)F_i(x)F_j(y).$$

Positive semidefiniteness means symmetry together with nonnegativity of every real quadratic form.

Formalization targets

The mission keeps two logically independent requirements visible. Nonnegative split coefficients $c_a\ge0$ give reflection positivity through a weighted Gram factorization. Pointwise nonnegativity $W(x,y)\ge0$, together with one strictly positive value, gives $Z>0$ and probability normalization. Neither requirement is silently substituted for the other.

The positive targets prove:

1. finite normalization of a nonnegative, nonzero weight;
2. closure of split data under common half-factors;
3. closure of split data under pointwise products;
4. preservation of reflection positivity under division by $Z>0$; and
5. the combined probability, PSD-kernel, and chessboard conclusions

$$K_{ij}^{2}\le K_{ii}K_{jj}.$$

Two controls freeze the boundary. The symmetric two-point matrix with diagonal $1$ and off-diagonal $2$ is pointwise positive and normalizes to a probability weight, but its raw and normalized delta-observable kernels are not PSD. Conversely, zero split data have nonnegative coefficients and PSD raw kernels, but $Z=0$ and their formally normalized weight is not a probability weight.

Significance

The result is a reusable adapter between an unnormalized finite Gibbs factorization and the previously certified reflection-positive kernel API. It prevents a later model proof from treating pointwise positivity as if it were a Gram representation, or treating reflection positivity as if it guaranteed a nonzero normalizer. The next physical consumer can therefore focus on proving an explicit nonnegative factorization of its cross-plane Boltzmann weight.

Scope

All types and sums used for normalization and kernels are finite, and all weights, coefficients, features, observables, and matrices are real. The mission proves no clock- or XY-specific Gibbs factorization, no spectral or Gaussian-domination theorem, no thermodynamic limit, and no Kosterlitz--Thouless conclusion. Those require separate missions. Physical $R1$ and $G1$ are not conclusions here.

References

• J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, Phase transitions and reflection positivity. I. General theory and long range lattice models, Communications in Mathematical Physics 62 (1978), 1--34. https://doi.org/10.1007/BF01940327
• Prove2Me mission Finite Reflection Positivity Methods I: Split Weights and Infrared Modes, mission db962332-7a71-4d34-a01c-e85cdee243ce.
• LeanProofs, ReflectionPositivityInfraredBound.lean, repository snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef: https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean

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

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