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

Motivation

The central limit theorem tells us that a normalized sum of independent random variables converges in distribution to a Gaussian. For applications — bounding the failure probability of a randomized algorithm, controlling the error of a Monte Carlo estimator, proving a generalization bound in learning theory — a limiting distribution is not enough: what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed sample size $N$, not merely as $N \to \infty$. Hoeffding's inequality (Wassily Hoeffding, 1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit Gaussian-type tail bound for a weighted sum of independent random variables, valid for every $N$, with all constants made explicit. They are the workhorses behind concentration of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix norms, or the restricted isometry property has to pass through this chapter first, because every one of those results is itself an application of a weighted-sum concentration inequality to a specific choice of random variables.

The central limit theorem's own error term is the obstruction that direct concentration inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav Esseen, 1942) bounds the normal approximation's error at order $1/\sqrt N$, which is too slow to recover a genuinely exponential tail bound for finite $N$. Hoeffding's and Bernstein's inequalities are proved instead by a direct argument — bounding the moment generating function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes the central limit theorem or its error term at all.

The sub-gaussian and sub-exponential norms

Fix a probability space $(\Omega, \mathcal F, P)$. For a real random variable $X$ on $(\Omega, \mathcal F, P)$, define its sub-gaussian norm

$$\|X\|_{\psi_2} := \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \text{ is finite and } \le 2\}$$

and its sub-exponential norm

$$\|X\|_{\psi_1} := \inf\{t > 0 : \mathbb E \exp(|X|/t) \text{ is finite and } \le 2\}.$$

In both definitions, the requirement that the exponential moment be finite (i.e. that the moment-generating integrand be integrable), and not merely satisfy "$\le 2$" as a bare inequality, is essential: without it a moment that is genuinely infinite for a given $t$ would vacuously count as "$\le 2$" under the Bochner integral's convention that a non-integrable function integrates to $0$, and every random variable — however heavy-tailed — would trivially have norm $0$. $X$ is called sub-gaussian (respectively sub-exponential) when this infimum is over a nonempty set, i.e. when some finite $t$ makes the moment finite and at most $2$. These are genuine norms (up to the identification of almost-surely-equal random variables) on the vector space of random variables for which they are finite, and they are the natural non-asymptotic yardsticks for tail heaviness: $\|X\|_{\psi_2} < \infty$ characterizes a Gaussian-type tail $P\{|X| \ge t\} \le 2\exp(-ct^2/\|X\|_{\psi_2}^2)$, while $\|X\|_{\psi_1} < \infty$ characterizes an exponential-type tail $P\{|X| \ge t\} \le 2\exp(-ct/\|X\|_{\psi_1})$. Every bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli) random variable — is sub-gaussian, and the square of a sub-gaussian random variable is sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared coordinate $g_i^2$ of a standard Gaussian vector, or the exponential distribution itself.

Formalization targets

Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let $X_1, \dots, X_N$ be independent, mean-zero, sub-exponential random variables on $(\Omega, \mathcal F, P)$, and let $a = (a_1, \dots, a_N) \in \mathbb R^N$. Then, for every $t \ge 0$,

$$P\Bigl\{\Bigl|\sum_{i=1}^N a_i X_i\Bigr| \ge t\Bigr\} \;\le\; 2\exp\left[-c\min\left(\frac{t^2}{K^2\|a\|_2^2}, \frac{t}{K\|a\|_\infty}\right)\right],$$

where $K = \max_i \|X_i\|_{\psi_1}$ and $c > 0$ is an absolute constant that does not depend on $N$, the $X_i$, $a$, or $t$.

The goal is deliberately the weighted and sub-exponential form, the weakest of the chapter's results that is still stable under the improvements a solver might find: it neither fixes $a_i \equiv 1$ (the unweighted Theorem 2.8.1, a special case) nor restricts to the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are included as milestones because Bernstein's own proof is built directly from them.

Significance

The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a sub-gaussian tail $\exp(-ct^2/(K\|a\|_2)^2)$ near the mean, transitioning to a heavier sub-exponential tail $\exp(-ct/(K\|a\|_\infty))$ far from it, exactly the behavior one should expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls $\sum \varepsilon_i \varepsilon_j$-type terms, which are themselves products of sub-gaussians and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding empirical-process suprema whose summands are not bounded but merely light-tailed.

Formalizing it. No formalization of Bernstein's inequality — in either the weighted or unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked 2026-09-17). What this mission produces is not just the statement but the machinery underneath it: a working Orlicz-norm treatment of $\psi_1$ and $\psi_2$ that a later mission (the Hanson–Wright inequality, or any future chapter that needs sub-exponential concentration) can build on directly.

Difficulty

The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove the weak law of large numbers — gives only a polynomial tail bound decaying like $1/N$, far too weak to be useful (this is exactly the point made by the chapter's opening discussion of the coin-tossing example, comparing the linear decay from Chebyshev against the target exponential decay). The central limit theorem promises the right shape of tail asymptotically but, per Berry–Esseen, with an error of order $1/\sqrt N$ that swamps any exponential gain for large deviations — the CLT approximation is simply not valid in the tail regime the inequality needs. The actual argument instead controls the moment generating function of the full sum directly and optimizes an exponential (Chernoff) tilt; this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and 2.7.1 show all these characterizations are equivalent up to constants. The min of two terms in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to a single term in either direction would either be false (dropping the exponential term) or needlessly weak (dropping the Gaussian term, which is what a naive union bound over the worst single term would give).

Formalization scope

Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P) (Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which corresponds directly to the book's $P\{\cdot\}$.

Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and 2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is 0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied by every t for which the moment is actually infinite, collapsing the sub-gaussian norm of a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed variable) to 0 — a trivializing formalization the mission was moderated to rule out. The same Integrable conjunct appears in every moment hypothesis (general_hoeffding, bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so that the hypothesis is not satisfied vacuously by non-integrable exponential moments either. HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy parameter $\sigma^2$ (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally from the Orlicz $\psi_2$ norm — equivalent up to a constant factor by the book's own Proposition 2.5.2, but not interchangeable without restating that equivalence — and Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz norms) is used for both $\psi_1$ and $\psi_2$ throughout the mission, rather than mixing Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.

Every occurrence of the book's "$c$ is an absolute constant" is formalized as a genuine existential quantifier fixed before the random variables, the vector a, and t are introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is substituted for c anywhere; a solver's proof may use any positive constant it can establish, exactly mirroring the book's own non-constructive existence claims. The trivializing formalization this rules out is fixing c to a specific small numeral (which would be a strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the statement by allowing c to depend on N, the $X_i$, a, or t (which would make the theorem vacuous, since any such bound trivially holds for a small enough $c$ depending on the instance).

Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters $p_i$ are given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent $t$ in $(e\mu/t)^t$. Hoeffding's inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained, needing only the two-point probability hypothesis defining the Rademacher distribution.

Selected references

• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.2307/2282952
• S. Bernstein, The Theory of Probabilities, Gastehizdat Publishing House, Moscow, 1946 (Russian; the inequality is due to Bernstein's earlier 1920s–1930s work, this textbook states the modern sub-exponential form following later expositions).
• A. C. Berry, The Accuracy of the Gaussian Approximation to the Sum of Independent Variates, Transactions of the American Mathematical Society 49(1), 1941. https://doi.org/10.2307/1990053
• C.-G. Esseen, On the Liapunoff Limit of Error in the Theory of Probability, Arkiv för Matematik, Astronomi och Fysik A28, 1942.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 2. https://doi.org/10.1017/9781108231596

Motivation

Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set $T \subseteq \mathbb{R}^n$ is a convex combination of at most $n+1$ points of $T$. That bound is tight and grows with the dimension $n$, which makes it useless whenever $n$ is large — exactly the regime of interest in high-dimensional probability.

B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate $x$ to accuracy $\varepsilon$, the number of points needed depends only on $\varepsilon$, never on $n$. Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.

Setting

A convex combination of finitely many points $z_1, \dots, z_m \in \mathbb{R}^n$ is a sum $\sum_{i=1}^m \lambda_i z_i$ with $\lambda_i \ge 0$ and $\sum_i \lambda_i = 1$. The convex hull $\operatorname{conv}(T)$ of a set $T \subseteq \mathbb{R}^n$ is the set of all convex combinations of all finite collections of points of $T$. The diameter of $T$ is $\operatorname{diam}(T) = \sup\{\|s-t\|_2 : s, t \in T\}$, the Euclidean norm throughout.

The classical Carathéodory theorem states that every $x \in \operatorname{conv}(T)$ is a convex combination of at most $n+1$ points of $T$ — with $n+1$ generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate $x$ rather than represent it exactly, and willing to use only combinations with equal coefficients $1/k$ (an average of $k$ points, with repetition allowed), how large must $k$ be as a function of the desired accuracy?

Formalization targets

Goal — Theorem 0.0.2, Approximate Carathéodory's theorem

$$\text{diam}(T) \le 1,\ x \in \operatorname{conv}(T),\ k \in \mathbb{Z}_{>0} \ \Longrightarrow\ \exists\, x_1,\dots,x_k \in T:\quad \left\| x - \frac{1}{k}\sum_{j=1}^{k} x_j \right\|_2 \le \frac{1}{\sqrt{k}}.$$

The quantifiers are exactly this order: for every bounded $T$, every point of its convex hull, and every target $k$, such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points $k$ does not depend on the dimension $n$, and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.

Milestone — Corollary 0.0.4, Covering polytopes by balls

$$P = \operatorname{conv}(T),\ |T| = N,\ \operatorname{diam}(P) \le 1,\ \varepsilon > 0 \ \Longrightarrow\ \exists\, C,\ |C| \le N^{\lceil 1/\varepsilon^2 \rceil}:\quad P \subseteq \bigcup_{c \in C} \overline{B}(c, \varepsilon).$$

This is a direct application of the goal to computational geometry's covering problem: how many balls of radius $\varepsilon$ are needed to cover a polytope, and where should they be centered.

Significance

The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond $\mathbb{R}^n$: it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an $\varepsilon$-net of a hypothesis class.

Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average $k$ i.i.d. samples, and bound the variance) is left open for solvers.

Difficulty

The identity that makes the proof work — averaging $k$ independent copies of a random vector concentrates around its mean at rate $1/\sqrt{k}$ in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct $x_1,\dots,x_k$ by some explicit combinatorial recipe, does not see a path to a bound independent of $n$. The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.

Formalization scope

Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so ‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for $\operatorname{diam}(T) = \sup\{\|s-t\|_2\}$. The convex hull is Mathlib's convexHull ℝ T; by Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex combination of finitely many points of $T$, so no bespoke convex-combination definition is introduced — this mission needs no supporting definitions of its own. In the corollary, "a polytope $P$ with $N$ vertices" is formalized, following the book's own proof, as $P = \operatorname{conv}(T)$ for a finite vertex set $T$ with $\#T = N$, rather than via a separate Polytope structure (which Mathlib does not provide and the book's argument does not need). The covering bound $N^{\lceil 1/\varepsilon^2\rceil}$ is an exponent, not a product with $N$ — matching the book's own proof, which counts the $N^k$ ordered $k$-tuples of vertices with repetition, $k := \lceil 1/\varepsilon^2\rceil$; the typeset "$N\lceil 1/\varepsilon^2\rceil$" in the corollary statement is the same juxtaposition-as-exponent notation the proof uses for "$N^k$" one line earlier.

A trivializing formalization is ruled out explicitly: the goal must hold for every integer $k > 0$ and every $x \in \operatorname{conv}(T)$, not merely some convenient choice — e.g. $k = 1$ together with $x \in T$ trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent $k$ works uniformly over all points of the hull. The formal statement quantifies $T$, then $x$, then $k$, and only then asserts existence of the $x_1,\dots,x_k$, exactly in that order.

Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by either formalized result's proof) is not drafted here: Mathlib already proves the corresponding statement via affine independence (Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean), from which the book's "$n+1$ points" bound follows via AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone because no corresponding theorem is yet published on the Prove2Me platform to point at (checked 2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results), and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than reuse it.

Selected references

• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, DOI 10.1017/9781108231596, Appetizer (pp. 1–5).
• G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle (Maurey–Schwartz), 1980–1981, exposé no. 5. numdam.org/item/SAF_1980-1981____A5_0
• B. Carl, "Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces," Annales de l'Institut Fourier, 35(3), 1985, 79–118. numdam.org/item/AIF_1985__35_3_79_0

Motivation

Two-stage stochastic programs with recourse require evaluating $Q(x) = \mathbb E_\xi[Q(x,\xi)]$, the expected value of a recourse function, at every candidate first-stage decision $x$. When $\xi$ is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: $Q(x,\cdot)$ is convex whenever the recourse problem is a linear program in $\xi$, and convexity alone is enough to sandwich $\mathbb E_\xi[Q(x,\xi)]$ between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ and an integrand $g : D \times \Xi \to \mathbb R$, where $\Xi \subseteq E$ is the (convex, closed) support of a random vector $\xi : \Omega \to \Xi$ and $E$ is a real vector space (in the recourse application, $g(x,\cdot) = Q(x,\cdot)$ and $D$ is the first-stage feasible region). Write $\mathbb E(g(x)) = \mathbb E_\xi[g(x,\xi)] = \int_\Xi g(x,\xi)\, P(d\xi)$.

A partition of $\Xi$ into $\nu$ measurable blocks $S^\nu = \{S_1,\dots,S_\nu\}$ determines, for each block, its probability $p_l = P[\xi \in S_l]$ and its conditional mean $\xi^l = \mathbb E[\xi \mid S_l]$. Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets $S_l = \xi^{-1}(\text{region}_l) \subseteq \Omega$, with $p_l = P(S_l)$ and $\xi^l = p_l^{-1}\int_{S_l}\xi\,dP$ the Bochner integral average of $\xi$ over the block; the two descriptions coincide.

Formalization targets

Goal — Chapter 8, Theorem 1 (Jensen lower bound), p. 346

$$g(x,\cdot) \text{ convex on } \Xi \ \Longrightarrow\ \mathbb E(g(x)) \ \ge\ \sum_{l=1}^{\nu} p_l\, g(x,\xi^l).$$

This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of $g(x,\cdot)$ and integrability.

Chapter 8, Theorem 2 (Edmundson-Madansky upper bound), pp. 347-348

For $\Xi$ compact, let $\mathrm{ext}\,\Xi$ be the extreme points of $\mathrm{co}\,\Xi$, carrying the Borel field of all its subsets. If, for every $\xi \in \Xi$, $\varphi(\xi,\cdot)$ is a probability measure on $\mathrm{ext}\,\Xi$ with barycenter $\xi$ (i.e. $\int_{\mathrm{ext}\,\Xi} e\,\varphi(\xi,de) = \xi$) and $\omega \mapsto \varphi(\xi(\omega), A)$ is measurable for every $A$, then

$$\mathbb E(g(x)) \ \le\ \int_{\mathrm{ext}\,\Xi} g(x,e)\, \lambda(de), \qquad \lambda(A) = \int_\Omega \varphi(\xi(\omega), A)\, P(d\omega).$$

Together the two targets give the chapter's headline sandwich: for convex $g(x,\cdot)$, the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.

Significance

The Jensen bound is the workhorse of discrete-distribution approximation in stochastic programming: it is what makes $Q^\nu(x) = \sum_l p_l Q(x,\xi^l)$ a valid, refinable lower-approximation of the true recourse function, and it underlies the partition-refinement schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the $L$-shaped method and separable-programming solvers described later in the chapter (§8.3). The Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no certificate of how far a lower approximation can be from the truth, and the mean-consistent LP refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over $\lambda$. Both bounds are, to date, unformalized: the platform holds no theorem matching either a finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition convex" — no relevant hits), so this mission is a first formalization of both, not a reformulation of existing platform content. Mathlib supplies the raw convexity substrate this mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the set-average integral Jensen inequality (ConvexOn.map_set_average_le in Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1 performs — but no existing lemma assembles these into the partitioned, conditional-mean statement the book actually states.

Difficulty

The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about $\Sigma_l p_l g(x,\xi^l)$, a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing $\mathbb E(g(x))$ as $\sum_l P(S_l)\,\mathbb E[g(x,\xi)\mid S_l]$ (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace $\mathbb E[g(x,\xi)\mid S_l]$ by $g(x,\xi^l)$ from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of $\Xi$, continuity of $g(x,\cdot)$ on $\Xi$, integrability on the block) and then summing the $\nu$ per-block inequalities against weights $p_l$ that themselves depend on the partition — an easy step to get wrong by, e.g., letting $\xi^l$ be an arbitrary point of $S_l$ rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration $\lambda$ correctly: $\lambda$ is a probability measure defined as an integral of the kernel-like family $\varphi$ against $P\circ\xi^{-1}$, and both the barycenter condition on $\varphi$ and the measurability of $\omega \mapsto \varphi(\xi(\omega),A)$ are load-bearing — dropping either makes $\lambda$ ill-defined or the bound's proof inapplicable.

Formalization scope

$\Xi \subseteq E$ for $E$ a complete real normed vector space (NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's proof needs it. The parameter $x$ ranges over an arbitrary type $\alpha$ with $D \subseteq \alpha$, and $g$ is left as a bare function α → E → ℝ, matching the book's level of abstraction (the recourse LP's own data $A,b,c,q,W,T,h$ is never used in either proof).

The partition is formalized directly on the sample space $\Omega$ (a Partition structure: pairwise-disjoint measurable blocks covering $\Omega$, each of positive measure) rather than on $\Xi$, per the equivalence noted under Setting; $\xi^l$ is defined as the Bochner-integral average $p_l^{-1}\int_{S_l}\xi\,dP$, so it is forced to be the conditional mean and cannot be weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main faithfulness trap for this chapter.

Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content: ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the interior of their domain, which is what the book implicitly relies on; stated explicitly since $E$ is not assumed finite-dimensional) and integrability of $\xi$ and of $g(x,\xi(\cdot))$ (needed for $\mathbb E(g(x))$ and each $\xi^l$ to be well-defined). For Theorem 2, the disintegrating family $\varphi$ is E → Measure Ext for an abstract type Ext (standing for $\mathrm{ext}\,\Xi$) with the discrete MeasurableSpace (every subset measurable, matching the book's "Borel field ... the collection of all subsets"), mapped into $E$ by an embedding toE whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure $\lambda$ (named μExt in the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation (2.6) rather than constructed, since constructing a measure from a set function is a separate, book-external piece of measure theory the chapter's own proof does not perform either — it simply asserts $\lambda$ is the probability measure with that value on every set.

A trivializing formalization is ruled out explicitly: a version that lets $\xi^l$ range over an arbitrary point of $S_l$, or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.

Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's ConvexOn.map_set_average_le applied per block with the exact decomposition of $\int_\Omega$ into $\sum_l \int_{S_l}$ over the partition's disjoint, covering blocks. Reusable beyond this mission: the Partition structure and its weight/condMean accessors generalize to any chapter needing a finite measurable partition with conditional means (this book's later approximation schemes, §8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or formalizing the partition-refinement monotonicity $\mathbb E(g(x)) \ge \mathbb E^{\nu+1}(g(x)) \ge \mathbb E^\nu(g(x))$ (eq. 2.3, not part of this mission's milestone list since it is not itself a numbered theorem) as a follow-up, are welcome.

Selected references

• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• J.L.W.V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes, Acta Mathematica 30 (1906), 175-193. https://doi.org/10.1007/BF02418571
• H.P. Edmundson, Bounds on the expectation of a convex function of a random variable, The RAND Corporation, Paper 982, 1956.
• A. Madansky, Bounds on the expectation of a convex function of a multivariate random variable, Annals of Mathematical Statistics 30 (1959), 743-746. https://doi.org/10.1214/aoms/1177706207
• A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960), 197-204. https://doi.org/10.1287/mnsc.6.2.197
• H.I. Gassmann, W.T. Ziemba, A tight upper bound for the expectation of a convex function of a multivariate random variable, Mathematical Programming Study 27 (1986), 39-53. https://doi.org/10.1007/BFb0121114
• J.R. Birge, R.J-B. Wets, Designing approximation schemes for stochastic optimization problems, in particular for stochastic programs with recourse, Mathematical Programming Study 27 (1986), 54-102. https://doi.org/10.1007/BFb0121122

Motivation

Every stochastic program is, in practice, compared against a shortcut. A decision maker facing genuine uncertainty is tempted either to replace the random data by its mean and solve one deterministic problem, or to imagine that perfect information about the future were available and solve a separate deterministic problem per scenario. Both temptations have precise answers: the expected value of perfect information (EVPI) measures how much a decision maker should be willing to pay for a perfect forecast, and the value of the stochastic solution (VSS) measures the cost of ignoring uncertainty altogether by solving the mean-value problem. Both concepts originate in decision analysis — EVPI traces to Raiffa and Schlaifer (1961) — and were brought into stochastic programming by Madansky (1960), who proved the first chain of inequalities relating the wait-and-see value, the recourse value and the expected-value-solution's cost. Birge and Louveaux, Introduction to Stochastic Programming, 2nd ed. (Springer, 2011), Chapter 4, gives the standard modern treatment, including a refined family of bounds — built from pairs subproblems against a chosen reference scenario — that sharpen VSS beyond the original mean-scenario comparison. This mission formalizes that chapter's capstone: the five-quantity, four-inequality chain that pins VSS between two computable optimal values.

Setting

Fix a two-stage stochastic program with fixed recourse: a finite family of K scenarios $\xi_1,\dots,\xi_K$ in $\mathbb R^d$, each occurring with probability $p_k \ge 0$, $\sum_k p_k = 1$; a first-stage feasible set $K_1 \subseteq \mathbb R^{n_1}$; and, for every first-stage decision $x \in \mathbb R^{n_1}$ and every scenario $\xi \in \mathbb R^d$, a scenario cost $z(x,\xi)$ — the optimal value of $c^Tx + \min\{q^Ty \mid Wy = h(\xi) - Tx,\ y \ge 0\}$. By convention $z(x,\xi) = +\infty$ when $x$ has no feasible second-stage recourse under $\xi$, and $z(x,\xi) = -\infty$ when the second-stage program is unbounded below.

From $z$, five basic quantities are defined (Birge & Louveaux §4.1–§4.2):

• The recourse problem's value, $RP = \min_{x \in K_1} \mathbb E_\xi\, z(x,\xi)$ — the best a decision maker can do without foreknowledge of $\xi$ (the "here-and-now" solution).
• The wait-and-see value, $WS = \mathbb E_\xi\big[\min_{x \in K_1} z(x,\xi)\big]$ — the average cost if $\xi$ were revealed before choosing $x$.
• The expected value of perfect information, $EVPI = RP - WS$.
• The expected value problem's solution $\bar x(\bar\xi)$, optimal for the deterministic problem at the mean scenario $\bar\xi = \mathbb E(\xi)$; its recourse cost, the expected result of using the EV solution, is $EEV = \mathbb E_\xi\, z(\bar x(\bar\xi), \xi)$.
• The value of the stochastic solution, $VSS = EEV - RP$ — the extra cost of implementing the mean-scenario decision instead of solving the recourse problem.

Section 4.6 refines VSS by replacing the mean scenario with an arbitrary reference scenario $\xi^r$ (not necessarily one of the $K$ possible scenarios, e.g. a worst case), with assumed probability $p_r = P(\xi=\xi^r)$:

• $\bar x^r$, optimal for $\min_{x\in K_1} z(x,\xi^r)$, gives the expected value of the reference-scenario solution, $EVRS = \mathbb E_\xi\, z(\bar x^r,\xi)$, and the generalized $VSS = EVRS - RP$.
• For each scenario $\xi^k$, the pairs subproblem of $\xi^r$ and $\xi^k$ treats them as a two-point distribution with weights $p_r$ and $1-p_r$: its optimal value is $\min_{x\in K_1}\big[p_r\,z(x,\xi^r) + (1-p_r)\,z(x,\xi^k)\big]$, attained at some $\bar x^k$. Averaging these optimal values over $k$ (rescaled by $1/(1-p_r)$) gives the sum of pairs expected values, $SPEV$. Taking, instead, the smallest full expected cost $\mathbb E_\xi\,z(\bar x^k,\xi)$ among the $K{+}1$ candidate solutions $\{\bar x^1,\dots,\bar x^K,\bar x^r\}$ gives the expectation of pairs expected value, $EPEV$.

Formalization targets

Goal — Chapter 4, Theorem 9 (p. 174)

$$0 \;\le\; EVRS - EPEV \;\le\; VSS \;\le\; EVRS - SPEV \;\le\; EVRS - WS .$$

Four links, each with independent content: nonnegativity of the leftmost gap, then two genuine inequalities (from the pairs-subproblem comparisons of Propositions 7 and 8), then the identity $VSS = EVRS - RP$ folded against $RP \ge WS$'s reverse-direction cousin. This is the weakest statement that keeps all five quantities distinct — stating only the outer bound $0 \le VSS \le EVRS-WS$ would erase exactly the refinement (via pairs subproblems) that makes the chapter's method useful.

Supporting propositions (milestones, in attack order)

• Proposition 1 (p. 166): $WS \le RP \le EEV$.
• Proposition 5(a) (pp. 167–168): $0 \le EVPI$ and $0 \le VSS$ (mean-scenario form), for any stochastic program.
• Proposition 7 (p. 173): $WS \le SPEV \le RP$.
• Proposition 8 (p. 174): $RP \le EPEV \le EVRS$.

Significance

The chain gives a decision maker two computable, non-obvious bounds on VSS — a quantity that is otherwise expensive to pin down exactly, since $RP$ itself already requires solving the full recourse problem. $EVRS - EPEV$ and $EVRS - SPEV$ are both computable from $K+1$ (or $K$) two-scenario LPs, far cheaper than the full $K$-scenario recourse problem, so Theorem 9 turns an expensive exact quantity into a pair of cheap certified bounds. Formalizing it fixes, once and for all, the exact hypotheses and quantifier structure of Madansky's original inequality (Proposition 1) together with the later pairs-subproblem refinement (Propositions 6–8, Birge 1982), often cited informally as "the VSS bounds" without distinguishing $EEV$, $EVRS$, $EPEV$ and $SPEV$. No part of this chain is on Mathlib or Formalpedia today (checked by concept query, not title); this is a first, from-scratch treatment of two-stage recourse value-of-information theory as formal objects.

Difficulty

The obvious first idea — collapse $RP$, $WS$, $EV$, $EEV$, $EVRS$, $EPEV$, $SPEV$ to one "the optimal value of the LP" and prove a single inequality — throws away the entire content of the chapter. Each quantity restricts the minimization to a different feasible object: $RP$ minimizes jointly over $x$; $WS$ swaps the order of $\min$ and $\mathbb E$; $EEV$/$EVRS$ evaluate one fixed $x$ under every scenario; $SPEV$ and $EPEV$ each minimize over a family of pairs subproblems rather than the full $K$-scenario problem. The chain's proof (Propositions 7–8) depends on this precisely: Proposition 7's lower bound uses that each pairs-subproblem-optimal $(\bar x^k,\bar y^k)$ is feasible (not necessarily optimal) for the single-scenario problem at $\xi^r$, and its upper bound uses that the recourse-optimal $(x^*, y^*(\xi^r), y^*(\xi^k))$ is feasible (not necessarily optimal) for the pairs subproblem — a feasible-but-not-optimal argument in each direction, not a direct comparison of objective values. Losing track of which solution is fixed and which is optimized destroys the argument entirely.

Formalization scope

An Instance bundles the finite scenario set (Fin K, probabilities p : Fin K → ℝ with p ≥ 0, ∑ p = 1, scenarios xi : Fin K → (Fin d → ℝ)), the first-stage feasible set K1 : Set (Fin n1 → ℝ), and the scenario cost z : (Fin n1 → ℝ) → (Fin d → ℝ) → EReal, using the extended reals to carry the book's own +∞/−∞ conventions for infeasibility and unboundedness rather than silently restricting to a finite-valued special case (a genuine risk of trivialization here, since Example 2 of the chapter exhibits $EEV = +\infty$). All optimal values (RP, WS, EV, EVPI, EEV, VSS, EVRS, generalized VSS, SPEV, EPEV) are defined directly from z, matching the book's own level of abstraction in this chapter (which never unfolds z into the underlying LP's $A,b,c,q,W,T,h$ data — those appear only in Chapter 3). Because EEV, the mean-scenario VSS, EVRS, the generalized VSS, and EPEV are each defined relative to an optimal solution of some sub-problem — the book itself only ever says "let $\bar x(\bar\xi)$ denote some optimal solution" — every theorem using them states that solution and its optimality as explicit hypotheses (x ∈ K1 and z x … = ⨅ …), never baking it into a Classical.choiced value; this keeps the quantifier structure faithful to the book's own "let ... be an optimal solution" phrasing. Proposition 5's part (b) — the upper bound $EVPI \le EEV-EV$, $VSS \le EEV-EV$ "for stochastic programs with fixed recourse matrix and fixed objective coefficients" — needs a different scope: that hypothesis is a structural property of the underlying LP data ($W$, $c$, $q$ fixed across scenarios) invisible once $z$ is abstracted away as above, and pinning it down would require modeling the LP's $A,b,c,q,W,T,h(\xi)$ data explicitly (as Chapter 3's mission does for its convexity theorem). That part is out of scope here and is not needed for Theorem 9's own chain, which rests only on Proposition 5(a).

Collapsing any two of $RP$, $WS$, $EV$, $EEV$, $EVRS$, $EPEV$, $SPEV$ to a single "value of the LP" — the trivialization this book-wide series flags for Chapter 4 — is ruled out by construction: each is its own definition over its own feasible object, and Theorem 9's statement names all five quantities in the chain rather than only its outer bound. The two occurrences of "VSS" in the chapter (the original mean-scenario $EEV-RP$ of §4.2, and the reference-scenario $EVRS-RP$ generalization of §4.6, used only in Theorem 9) are likewise kept as two distinct definitions rather than conflated under one name.

Every addition and subtraction between EReal values in this mission — inside expect, WS, EVPI, VSS, EVRS's appearance in VSSRef, the pair sum inside pairsValue, the sum inside SPEV, and all four differences in Theorem 9's own chain — uses three explicit operations, badd/bsub/bsum, that implement the book's own convention (p. 164) that +∞ (infeasibility) dominates, i.e. (+∞)+(−∞)=+∞, rather than Mathlib's native EReal addition, whose ⊤+⊥=⊥ would make VSS ≥ 0 (Proposition 5(a)) and the goal's own leftmost inequality false whenever a witness solution is infeasible in a positive-probability scenario — exactly the situation of the book's own Example 2 (pp. 174-175). The reference scenario's probability $p_r=\Pr(\xi=\xi^r)$ (p. 172) is likewise not a free parameter but a definition, refProb, computed from the instance itself as $\sum_{k:\,\xi^k=\xi^r}p_k$; SPEV's sum is correspondingly restricted to the scenarios other than the reference scenario ($\xi^k\ne\xi^r$), matching the book's own proof of Proposition 7, which uses $\sum_{k\ne r}p_k=1-p_r$. The single hypothesis refProb I xir < 1 on Propositions 7, 8 and the goal says that some other scenario remains possible, which the book's own $(1-p_r)^{-1}$ factor presupposes.

Reusable beyond this mission: the Instance definition and the RP/WS/EV quantities are the natural base for any later chapter of this series that needs the two-stage recourse value (e.g. Chapter 3's convexity mission, Chapter 5's L-shaped method); contributions extending this Instance to the full LP data of the underlying two-stage program, or adding Proposition 5(b) and Proposition 2's Jensen-inequality argument on top of it, are welcome.

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011, Chapter 4. DOI: 10.1007/978-1-4614-0237-4
• A. Madansky, "Inequalities for Stochastic Linear Programming Problems", Management Science 6(2), 1960, 197–204.
• H. Raiffa and R. Schlaifer, Applied Statistical Decision Theory, Harvard Business School, 1961.
• J.R. Birge, "The Value of the Stochastic Solution in Stochastic Linear Programs with Fixed Recourse", Mathematical Programming 24(1), 1982, 314–325.