Motivation

Von Neumann's minimax theorem (Chapter VIII) settles two-player zero-sum games with scalar payoffs. In 1956, Blackwell asked the natural generalization: what can a player guarantee in a repeated game with vector-valued payoffs, where "winning" means driving the average payoff into a target set rather than above a target value? For decades the resulting theory — approachability — and the regret-minimization theory this book develops were believed to be different, with approachability seen as the stronger notion. Chapter 13 closes that gap: approachability and online convex optimization are shown to be algorithmically equivalent, each reducible to the other with no loss of efficiency, and along the way this equivalence yields a constructive, rate-quantified proof of Blackwell's own theorem.

Setting

A generalized vector game (Definition 13.2) is given by bounded convex closed decision sets $K_1,K_2$ and a vector payoff $u:K_1\times K_2\to\mathbb R^d$. A set $S$ is approachable (Definition 13.3) if some non-anticipating algorithm, playing in $K_1$ against any sequence $y_1,y_2,\dots\in K_2$, drives the average payoff's distance to $S$ to zero. Blackwell's theorem (13.4) characterizes exactly which $S$ are approachable via a purely geometric condition: every column-player strategy $y$ admits a row-player best response $x$ landing the payoff in $S$.

Section 13.2 constructs an explicit approachability algorithm from any OCO algorithm: given a best-response oracle realizing Blackwell's condition, Algorithm 37 runs the OCO algorithm on the proxy losses $f_t(w) = w^\top u_{t-1} - h_S(w)$ (the support function $h_S(w)=\max_{x\in S}\{w^\top x\}$ letting distance-to-$S$ be written, via Lemma 13.5's minimax duality, as a convex optimization problem over the unit ball), queries the oracle at the OCO algorithm's play $w_t$, and averages the resulting rewards.

Formalization targets

Theorem 13.7 (OCO-to-approachability rate, milestone)

$$\mathrm{Dist}(\bar u_T, S) \le \frac{\mathrm{Regret}_T(A)}{T}.$$

Theorem 13.4 — the mission's goal (sufficiency direction only)

$$\big(\forall y\in K_2,\ \exists x\in K_1,\ u(x,y)\in S\big) \implies S\ \text{is approachable}.$$

Significance

This chapter's headline claim — approachability and OCO are equivalent — is proved in two directions in the book (§13.2 and §13.3); this mission drafts the direction the book itself foregrounds as "the more interesting implication" and constructively proves: any sublinear-regret OCO algorithm converts directly into an explicit approachability algorithm with an explicit convergence rate, giving a self-contained, algorithmic proof of a 1956 game-theory theorem using 1990s–2000s online-learning machinery. Historically, this equivalence resolved a standing misconception (approachability believed strictly stronger) and reframes Blackwell's theorem as a special case of regret minimization rather than a separate theory requiring its own toolkit. No prior art was found on the platform for Blackwell approachability (planning search: q=Blackwell — the one hit, PRNGCompression.prng_no_free_lunch's cousin, an unrelated Rao-Blackwellization result, is not a substitute); this mission drafts both items fresh.

Difficulty

Theorem 13.4's statement is a clean geometric implication, but the book is explicit that its proof is entirely carried by Theorem 13.7 plus an unstated "explicit conclusion" left as an exercise (the passage from a finite-horizon rate bound to the asymptotic Dist → 0 claim, using any of the book's own sublinear-regret OCO algorithms as a witness). Theorem 13.7's own proof combines three nontrivial facts: Lemma 13.5's minimax-duality rewriting of $\mathrm{Dist}(\cdot, S)$ as a linear optimization over the unit ball (itself proved via Sion's minimax theorem, not excerpted here), the best-response oracle's defining inequality (13.2) applied pointwise at each round's $w_t$, and the OCO algorithm's own regret guarantee applied to the specific proxy-loss sequence $f_t$ built from the realized game trajectory — a genuine composition of three separate pieces of machinery from earlier in the book (Chapters III–VIII), not a routine substitution.

Formalization scope

IsApproachable is declared as its own definition (per BRIEF.md's explicit instruction, since Theorem 13.4 depends on it), with the non-anticipation clause made explicit (matching the series' IsOnlineAlgorithm convention from Chunk 03) even though the book's own Definition 13.3 states it only informally ("x_t ← A(y_1,\dots,y_{t-1})"). SupportFunction is h_S exactly as displayed, as a real supremum (a genuine maximum given the chapter's standing "closed, bounded" hypothesis on S). $\mathrm{Dist}(\cdot,S)$ throughout is Euclidean distance, rendered as Mathlib's Metric.infDist — confirmed the chapter uses no other distance notion (checked §13.1-13.3 directly, per the pitfall BRIEF.md flags). Theorem 13.7 transcribes Algorithm 37's $f_t(w)=w^\top u_{t-1}-h_S(w)$ construction faithfully, including its one-round offset (using the previous round's realized reward to build the current round's proxy loss, while the conclusion averages the current round's rewards) — exactly as the book's own pseudocode has it, not smoothed over.

Scope decision on Theorem 13.4's biconditional. The book states Theorem 13.4 as an ↔ but proves, and explicitly flags as proved, only the sufficiency direction (←): "The necessity of this condition is left as an exercise... Our reductions henceforth give an explicit proof of Blackwell's theorem [meaning: of the sufficiency direction]." Per CAPTAIN_BRIEF.md rule 6 and BRIEF.md's explicit instruction, this mission drafts only that direction, named as such in the goal item's own docstring; see STATUS.md.

Not formalized (out of scope for this mission, given the remaining budget and the explicit "exercise" status of several results on these pages): the necessity direction of Theorem 13.4; Lemma 13.5 (minimax duality for Dist, itself relying on Sion's theorem, not separately formalized here); Lemma 13.6 (the equivalent best-response-oracle condition); §13.3's entire approachability-to-OCO direction (Theorem 13.9, Lemma 13.8, the cone/polar-cone machinery of §13.3.1) and §13.3.3 (existence of a best-response oracle for the constructed set); the "explicit conclusion" of Blackwell's theorem from Theorem 13.7, left as an exercise by the book itself.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 13.
• D. Blackwell, "An analog of the minimax theorem for vector payoffs," Pacific Journal of Mathematics 6(1), 1956, 1-8.
• N. Abernethy, P. Bartlett, E. Hazan, "Blackwell approachability and no-regret learning are equivalent," COLT 2011.

Motivation

Online convex optimization (OCO) asks a learner to repeatedly pick a point in a convex set $K$, pay a cost that an adversary reveals only after the choice is made, and be judged against the best fixed point in hindsight. Chapter III of this series formalized the simplest general-purpose answer, online gradient descent (OGD): take a gradient step, project back onto $K$. OGD's analysis, however, is tied to the Euclidean geometry of the projection step — it treats every coordinate of $K$ alike, and its regret bound degrades badly when $K$'s natural geometry is not Euclidean (the probability simplex under the $\ell_1$ norm is the standard example, where a Euclidean-projection algorithm's regret scales with $\sqrt{n}$ in the dimension $n$, while an algorithm that exploits the simplex's own geometry attains regret scaling only with $\sqrt{\log n}$).

Regularized Follow the Leader (RFTL) is the meta-algorithm this chapter introduces to fix this: rather than fixing a specific geometry, RFTL is parameterized by an arbitrary regularization function $R$, and its regret bound depends on $R$ only through two scalar quantities the mission makes explicit — the range of $R$ over $K$, and a $R$-dependent "local norm" of the gradients. Choosing $R$ to match $K$'s geometry (entropy regularization on the simplex, for instance) recovers the sharp bounds that plain OGD cannot. RFTL and its close relative Online Mirror Descent (OMD), also introduced here, are the ancestors of essentially every regularization-based online learning algorithm in use today, including the multiplicative-weights/Hedge algorithm of Chapter I as a special case (entropy regularization on the simplex) and the exponentiated-gradient algorithm this book's own Chapter VIII reuses (Corollary 5.7, a further specialization of Theorem 5.2 this mission's Theorem 5.2 underlies). The naive "Follow the Leader" strategy this chapter opens by refuting — always play the empirically best point so far — is a natural first idea and provably fails: the book gives an explicit two-point cost sequence on which it incurs regret linear in the horizon. Regularization is the fix, and quantifying exactly how much it costs and buys is this chapter's content.

Setting

Fix a convex, nonempty decision set $K$ in a real inner product space $E$ and a sequence of convex cost functions $f_1, f_2, \dots : K \to \mathbb{R}$. As in Chapter III, regret after $T$ rounds is

$$\mathrm{Regret}_T = \sum_{t=1}^{T} f_t(x_t) - \min_{x^\star \in K} \sum_{t=1}^{T} f_t(x^\star).$$

A regularization function $R : K \to \mathbb{R}$ is a strongly convex, smooth, twice differentiable function with a positive-definite Hessian on the interior of $K$. Its Bregman divergence measures the gap between $R$ and its own first-order Taylor approximation:

$$B_R(x \| y) = R(x) - R(y) - \nabla R(y)^\top(x - y).$$

By the mean value theorem, $B_R(x\|y) = \tfrac12\|x-y\|_z^2$ for some point $z$ on the segment $[x,y]$, where $\|\cdot\|_z$ is the norm induced by the Hessian $\nabla^2 R(z)$; its dual norm, denoted $\|\cdot\|_z^*$, is the local norm at $z$. Writing $\|\cdot\|_t$ for the local norm between consecutive iterates $x_t, x_{t+1}$, the $R$-diameter of $K$ is $D_R^2 = \max_{x,y\in K}(R(x)-R(y))$.

The RFTL algorithm (Algorithm 13), with step size $\eta > 0$, plays $x_1 = \arg\min_{x\in K} R(x)$, then at every round updates

$$x_{t+1} = \arg\min_{x \in K}\Big\{\eta \sum_{s=1}^{t} \nabla_s^\top x + R(x)\Big\}, \qquad \nabla_t := \nabla f_t(x_t).$$

The agile Online Mirror Descent algorithm (Algorithm 14, agile version) instead maintains a dual point $y_t$ with $\nabla R(y_1) = 0$, updates it by $\nabla R(y_{t+1}) = \nabla R(x_t) - \eta \nabla_t$, and projects via the Bregman divergence, $x_{t+1} = \arg\min_{x\in K} B_R(x\|y_{t+1})$ (with $x_1$ defined the same way from $y_1$). RFTL and the lazy variant of OMD coincide for linear costs (Lemma 5.5, not formalized here — it is not used by either target); the agile variant's analysis is genuinely different and is the mission's second target.

Formalization targets

Target (Theorem 5.2 — RFTL's regret bound)

$$\mathrm{Regret}_T \;\le\; 2\eta \sum_{t=1}^{T} \|\nabla_t\|_t^{*2} \;+\; \frac{R(u) - R(x_1)}{\eta}, \qquad \text{for every } u \in K.$$

This is the mission's goal: RFTL, run with any admissible regularizer, attains a regret bound governed only by the cumulative squared local norm of the gradients and $R$'s range over $K$. The bound is proved via two milestones: Lemma 5.3 (regret controlled by the total "prediction drift" $\sum_t \nabla_t^\top(x_t - x_{t+1})$ plus $D_R^2/\eta$), which in turn rests on Lemma 5.4 (a "follow-the-leader beats be-the-leader" comparison inequality, proved by induction on the horizon).

Further target (Theorem 5.6 — agile OMD's regret bound)

$$\mathrm{Regret}_T \;\le\; \frac{\eta}{4} \sum_{t=1}^{T} \|\nabla_t\|_t^{*2} \;+\; \frac{R(u) - R(x_1)}{2\eta}, \qquad \text{for every } u \in K.$$

A structurally similar bound for the agile variant, included as its own goal-level item since — as the book states explicitly — its proof technique is unrelated to RFTL's, not a corollary of it.

Both targets are the book's own tightest, non-asymptotic statements: neither is weakened to an $O(\cdot)$ form, and the book's own further (unnumbered) corollary specializing Theorem 5.2 to a uniform local-norm bound $\|\nabla_t\|_t^* \le G_R$ is left out, matching this series' convention of formalizing only the numbered results.

Significance

The results themselves. Theorem 5.2 is the general regret theorem behind every regularization scheme in online learning: instantiating $R$ recovers the projected-gradient bound of Chapter III (Euclidean $R$), the multiplicative-weights bound of Chapter I (entropy $R$ on the simplex), and — through the exponentiated-gradient specialization (Corollary 5.7, not itself a target here) — the row-player regret bound this book's own Chapter VIII cites as "Eq. (8.1)" in its reduction of zero-sum games to regret minimization. Theorem 5.6 gives the same guarantee for an algorithm (agile OMD) that, unlike RFTL, maintains a feasible point at every round, which the book notes is preferable in the adaptive-regret setting of Chapter X.

Formalizing it. Both theorems have complete, elementary proofs in the source (no gaps, no "with high probability", no hidden regularity conditions); the mission's work is converting the analytic argument — the Bregman-divergence identity, the generalized Cauchy-Schwarz inequality bounding the drift term by the local norm, and the two induction arguments underlying Lemma 5.4 — into machine-checked statements. No formalization of RFTL, OMD, or the local-norm machinery exists on the platform (checked below); the closest Formalpedia entries state a related but distinctly narrower result.

Difficulty

The central obstacle is that the regularizer $R$ is a hypothesis, not a fixed function: the theorem must hold for every admissible $R$ simultaneously, so nothing about $R$ beyond its stated properties (strong convexity, smoothness, twice differentiability) may be used. A newcomer's first instinct — bound the local norm $\|\nabla_t\|_t^*$ by a fixed multiple of the Euclidean dual norm $\|\nabla_t\|_2$ — fails in general and is exactly the bound RFTL is designed to avoid needing; the whole point of the local-norm formulation is that it can be tight for regularizers (like entropy) whose Hessian is very far from a multiple of the identity. A second obstacle is Lemma 5.4's induction, which compares $x_{t+1}$ (a minimizer over $t+1$ terms) against $u$ using the minimality of $x_{t+1}$ at exactly the right instantiation — an argument that looks almost circular until the induction hypothesis is applied at $u = x_{t+2}$, not at the theorem's free variable.

Formalization scope

$K$ ranges over an arbitrary real, complete inner product space (a real Hilbert space), matching Chapters III and IV, not a fixed $\mathbb{R}^n$. The RFTL and agile-OMD update rules are represented relationally (IsArgMinOn), since Mathlib has no canonical argmin operator for a general convex set — mirroring IsMetricProjection's precedent from Chapter III. The Hessian at the mean-value-theorem's intermediate point is represented via the second Fréchet derivative of $R$'s gradient map (HasFDerivAt), since Mathlib has no dedicated Hessian type; the local dual norm is then any value satisfying the resulting existential characterization (IsLocalDualNormSq), stated once and shared by both targets. A boundedness hypothesis on $R$ over $K$ is added to Lemma 5.3's statement to keep the $R$-diameter $D_R^2$ from collapsing to Mathlib's junk value for an unbounded supremum — a condition every regularizer the book actually uses (strongly convex and smooth over a bounded $K$) already satisfies, so it narrows nothing.

Trivializing formalization ruled out. A regret bound stated for an "algorithm" defined loosely enough to include the after-the-fact optimal choice would be vacuous; IsRFTLRun and IsOMDAgileRun instead pin down the exact history-dependent update rule of Algorithms 13 and 14 (the current gradient sequence, the current regularizer, and nothing else) as a hypothesis, so a proof must genuinely use the specific update. Theorem 5.2 and Theorem 5.6 are kept as two separate items rather than one theorem parameterized by an algorithm choice, since — per the chapter's own remark that their analyses are unrelated — a merged statement would either need to branch internally on the algorithm or silently identify two genuinely different update rules.

Reuse and prior art. OnlineConvexOpt.FirstOrder.RegretT (Chapter III, published) is imported and reused verbatim, keeping the regret functional identical across the whole book. Definitions specific to Chapter IV (OnlineConvexOpt.SecondOrder, not yet published) are not imported per this series' convention that a draft cannot import another draft; quadForm is redeclared locally instead. On the platform, BanditAlgorithm.ftrl_regret_bound, BanditAlgorithm.mirror_descent_regret_bound, and BanditAlgorithm.ftrl_simplex_exp_weights_regret (the Bandit Algorithms series, Chapter XII) state regret bounds for FTRL and Mirror Descent in the linear-cost, bandit-idiom setting (a fixed linear loss $\langle a, y_t\rangle$ at each round, regret compared via a Bregman-divergence potential at fixed points). Hazan's Theorem 5.2 and 5.6 are for general convex $f_t$ and use the book's own local-norm object, which has no counterpart in those statements; they are read in full and are not faithful substitutes (different hypothesis class), so this mission drafts its own, independent items rather than reusing them.

Selected references

• Hazan, Introduction to Online Convex Optimization, 2nd ed., Chapter 5. arXiv:1909.05207v3
• Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning, 2012 (surveys RFTL/Mirror Descent under the name "Online Mirror Descent"). https://doi.org/10.1561/2200000018
• Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003 (the Euclidean special case this chapter generalizes). https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf

Motivation

Online decision-making problems — multi-armed bandits, contextual bandits, structured bandits, and episodic reinforcement learning — look superficially different but share a common shape: a learner repeatedly acts, observes feedback, and is scored by regret against the best action in hindsight. Foster, Kakade, Qian and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (Foster & Rakhlin, arXiv:2312.16730v1) develops a unifying account of this shape and asks a sharper question than "does this specific algorithm work?": for a given class of possible environments, what is the best regret any algorithm can achieve? The Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian and Rakhlin (2021, "The Statistical Complexity of Interactive Decision Making") and refined by Foster, Golowich, Qian, Rakhlin and Sekhari (2023), was proposed as the answer: a single real-valued complexity measure of a model class that simultaneously (i) drives a generic optimal-up-to-constants algorithm (Estimation-to-Decisions, E2D), and (ii) lower-bounds the regret of every algorithm. Item (ii) is what turns the DEC from "a complexity measure that happens to work for the algorithms we know" into a genuine characterization of statistical difficulty, in the same sense that minimax rates characterize the difficulty of estimation problems in classical statistics. This mission formalizes that lower bound.

Setting

Chapter 6 of the book (pp. 93–128) introduces Decision Making with Structured Observations (DMSO), a protocol general enough to subsume the contextual-bandit, structured-bandit and episodic tabular-RL protocols of earlier chapters. Over $T$ rounds, the learner selects a decision $\pi_t$ from a decision space $\Pi$; nature draws a reward-observation pair $(r_t, o_t)$ from a fixed, unknown model $M^\star(\cdot \mid \pi_t)$, where a model $M$ maps each decision to a distribution over a reward space $R$ and an observation space $O$. The learner has access to a model class $\mathcal{M}$ containing $M^\star$ (realizability). For $M \in \mathcal{M}$, write $f^M(\pi) := \mathbb{E}_{M,\pi}[r]$ for the mean reward function and $\pi_M := \arg\max_\pi f^M(\pi)$ for the optimal decision; regret is $\mathrm{Reg} := \sum_{t=1}^T f^{M^\star}(\pi_{M^\star}) - \mathbb{E}_{\pi_t \sim p_t}[f^{M^\star}(\pi_t)]$, exactly as in the bandit chapters, now for the general model class.

Because observations, not just mean rewards, now carry information, the DEC needs a way to measure distance between the full conditional distributions $M(\pi)$ and $\hat M(\pi)$, not just between scalars $f^M(\pi)$ and $f^{\hat M}(\pi)$. The chapter uses the squared Hellinger distance $D_H^2$, one of a family of Csiszár $f$-divergences that also includes total variation ($D_{TV}$) and Kullback-Leibler ($D_{KL}$) divergence. For a reference model $\hat M$ and scale $\gamma > 0$, the general Decision-Estimation Coefficient is the min-max game value

$$\mathrm{dec}_\gamma(\mathcal{M}, \hat M) := \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}} \mathbb{E}_{\pi \sim p}\bigl[f^M(\pi_M) - f^M(\pi) - \gamma \cdot D_H^2(M(\pi), \hat M(\pi))\bigr],$$

and $\mathrm{dec}_\gamma(\mathcal{M}) := \sup_{\hat M \in \mathrm{co}(\mathcal{M})} \mathrm{dec}_\gamma(\mathcal{M}, \hat M)$. This mission's Lean development (FoundationsRL.GeneralDM) formalizes discrete versions of $D_{TV}$, $D_H^2$, $D_{KL}$ for a finite outcome type, the DMSO regret, and this DEC.

Formalization targets

The goal is Proposition 28 (DEC Lower Bound), p. 105:

$$\exists\, c > 0 \text{ (sufficiently small)} : \forall\, T \text{ with } \mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\,\varepsilon_T,\; \varepsilon_T := c/\sqrt{T},\; \forall\, \text{algorithm}\; p,\; \exists\, M \in \mathcal{M} : \mathrm{regret}(M, p) \ge \tfrac{1}{20}\, \mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \cdot T.$$

Here $\mathrm{dec}^c_\varepsilon$ is the constrained DEC (§6.5.1), a variant of the offset DEC above that hard-constrains the information gain rather than subtracting it — a technical refinement needed to make the lower-bound direction go through — and the "localization condition" $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ is a genuine hypothesis of the proposition, not a footnote. Unlike almost every other target in this series of missions, the statement quantifies over every algorithm rather than naming one: it is a genuine impossibility result. Two supporting divergence facts are included as milestones because the DEC's information-theoretic argument rests on them: Lemma 19 ($D_{TV}^2 \le D_H^2 \le D_{KL}$) and Lemma 20 (a bounded-likelihood-ratio refinement bounding $D_{KL}$ in terms of $D_H^2$). The chapter's own matching upper bound, Proposition 26 (the E2D regret bound for the general DMSO protocol, the direct analogue of Chapter 4's Proposition 13), is included as a milestone to give the reader the matching pair the chapter presents together. Finally, Corollary 1 restates the lower bound in terms of the localized offset DEC (combining Proposition 28 with Proposition 27), included as a milestone showing the lower bound's reach beyond the constrained DEC alone.

Significance

Proposition 28 is what makes the DEC a genuine characterization of the statistical complexity of interactive decision making, rather than merely a sufficient condition for a particular algorithm family to succeed. Combined with the (uncited, technically deeper) matching upper bound for the constrained DEC — Proposition 29, stated but not proved in the book — it shows that for any finite model class, the constrained DEC is necessary and sufficient for low regret up to a $\sqrt{\log|\mathcal{M}|}$ factor in the localization radius: no complexity measure that is substantially different from the DEC can characterize the same problems. This is the general decision-making analogue of how minimax rates pin down statistical estimation, now for interactive protocols with adaptive feedback.

Formalizing the lower bound is new work: no result of this shape exists on the Prove2Me platform (searches for "decision-estimation", "general divergence", "constrained DEC" and "Hellinger" — the last of which surfaces two related-but-distinct affinity/Le Cam bounds from a different mission on bandit lower bounds — return no faithful prior art; see MODERATION_NOTES.md). The formal statement is the boxed proposition; the book gives a self-contained but simplified proof (two named simplifying assumptions, §6.5.3) and cites Foster, Golowich, Qian, Rakhlin & Sekhari (2023) for the unrestricted argument. This mission's Lean items are draft statements (:= by sorry), not proofs; formalizing the proof itself — a two-point adaptive testing argument using the chain rule for KL divergence and a change-of-measure step — is the open contribution this mission proposes.

Difficulty

The obvious first attempt is to try to prove the lower bound by exhibiting one fixed pair of hard models $M, \hat M$, as in classical two-point minimax lower bounds (Le Cam's method, Fano's inequality). This fails here because the decision-making protocol is interactive and adaptive: the algorithm's queries depend on what it has observed, so a model pair chosen obliviously (before seeing the algorithm) cannot in general be made indistinguishable to every algorithm — an adaptive algorithm can be constructed that distinguishes any two fixed models quickly by querying where they differ. The book's proof instead selects the "hard" alternative model $M$ as a function of the algorithm's own strategy (via the constrained DEC's arg max, Eq. (6.36)), so that the pair is hard specifically for the algorithm under consideration, then uses the chain rule for KL divergence plus the change-of-measure identity between the algorithm's induced distributions under $M$ and $\hat M$ to conclude that the algorithm's realized decisions must look similar under both models — hence it cannot get low regret on both simultaneously. Every step of this argument depends on the exact game structure of the constrained DEC, not just its numerical value; a formalization that leaves $\mathrm{dec}^c_\varepsilon$ as an unconstrained real parameter (rather than the actual $\inf$-$\sup$ game with its information-gain constraint) would make the lower bound's conclusion vacuous, since the hypothesis $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ would no longer track any actual property of $\mathcal{M}$.

Formalization scope

The decision space $\Pi$ and the outcome (reward, observation) alphabet $Y$ are both taken as finite types (Fintype); a model $m : \Pi \to Y \to \mathbb{R}$ is a conditional probability vector, and a reward-extraction map $\mathrm{rew} : Y \to \mathbb{R}$ recovers the mean reward $f^m(\pi) = \sum_y m(\pi)(y)\cdot\mathrm{rew}(y)$. hellingerSq, totalVariationDiscrete, klDivDiscrete specialize the book's general dominating-measure divergence formula (Eq. (6.5)) to the counting measure on this finite type; klDivDiscrete returns an ENNReal so its $+\infty$ case (when $P$ is not absolutely continuous w.r.t. $Q$) is represented honestly. The DEC, the constrained DEC and the localized subclass are literal sInf-of-sSup/sSup-of-sSup transcriptions of the book's min-max games — the same convention this series uses for the Chapter-4 DEC — not opaque free real numbers, which rules out the trivializing formalization named above.

Three deviations from this series' usual convention of pinning every constant to the value the book's own proof derives are deliberate and disclosed. First, the numerical constant $c$ in $\varepsilon_T := c/\sqrt{T}$ is explicitly called "not important" by the authors themselves (footnote a, p. 105); it is existentially quantified (∃ c > 0) rather than pinned to a numeral. Second — added at moderation, round 2, 2026-09-19, after the constant was found to be pinned incorrectly — the lower bound's own multiplicative constant is also existentially quantified (∃ c' > 0) rather than pinned to 1/20. The book's printed proof (§6.5.3, pp. 107–110) derives 1/20 (p. 110, not p. 109 as an earlier draft of this mission stated) only under two named simplifying assumptions the theorem's hypotheses do not carry (p. 107, "Simplifications": a class-wide bounded-curvature hypothesis, Eq. (6.34); and a bound on the unaugmented $\sup_{\hat M\in\mathcal M}\mathrm{decc}_\varepsilon(M,\hat M)$ rather than the officially-defined, augmented $\mathrm{decc}_\varepsilon(M) = \sup_{\hat M\in\mathrm{co}(\mathcal M)} \mathrm{decc}_\varepsilon(M\cup\{\hat M\},\hat M)$ this mission's decC implements). Since augmenting either supremum's domain can only raise its value, the printed proof's bound on the narrower, unaugmented quantity does not license a pinned 1/20 against the fully general decC this theorem states; the book itself attributes the proof of the general statement to an external reference (Foster, Golowich, Qian, Rakhlin & Sekhari 2023) not in this document. The existential c' matches the book's own unpinned $\gtrsim$ for Proposition 28 as printed on pp. 105–106. Third, "any algorithm" and $\mathbb{E}[\mathrm{Reg}(T)]$ are formalized, as throughout this series, without a full stochastic-process/history model: regret is a deterministic quantity evaluated at a fixed realized decision-distribution sequence $p : \mathrm{Fin}\,T \to \Pi \to \mathbb{R}$, rather than an expectation over an adaptive, history-dependent algorithm's own randomness. Formalizing the fully adaptive, measure-theoretic version of "any algorithm" — with an explicit filtration and expectation over the induced process law $P_M$ — is future work a solver could add; the current statement is faithful to the book's deterministic-per-realization content but not to its full generality over randomized, history-dependent strategies. The DMSO protocol (Def_FoundationsRL_GeneralDM_Protocol) and the DEC (Def_FoundationsRL_GeneralDM_DEC) are restated locally rather than imported from Chapter 4's mission (FoundationsRL.Structured), since draft items cannot import another chunk's drafts; contributions extending either mission to reuse the other's substrate once both are published are welcome.

Selected references

• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2023). Foundations of Reinforcement Learning and Interactive Decision Making. arXiv:2312.16730.
• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2021). The Statistical Complexity of Interactive Decision Making. arXiv:2112.13487.
• Foster, D. J., Golowich, N., Qian, J., Rakhlin, A., & Sekhari, A. (2023). A Unified Model and Dimension for Interactive Estimation. arXiv:2306.06184.
• Polyanskiy, Y., & Wu, Y. Information Theory: From Coding to Learning. Cambridge University Press (draft edition cited by the book as [68]).

Motivation

A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.

Setting

The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is

min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹,  Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.),  xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),

over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally, the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in which tree and which node data they use; this mission formalizes that shared shape once (Tree, Instance, Feasible, obj) and instantiates it twice.

Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of its own (different) chapter, restated here rather than imported (a draft cannot import another chunk's draft). An Instance H n m T bundles a tree's node-varying LP data (c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem (1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an aggregation map agg : TFine.Node → TCoarse.Node.

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
  each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
  coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
  ⟹ zCoarse ≤ zFine

This is the mission's only formalization target: BRIEF.md records that no separately numbered lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty; see STATUS.md for the explicit accounting of what else in this chapter was considered and left out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier result).

Significance

Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's multistage material builds on: it says precisely when replacing a multistage recourse problem's random data by within-period conditional expectations preserves a valid lower bound, and precisely identifies the condition (aggregated nodes sharing a current-period outcome must carry identical aggregated data) whose failure breaks the bound — a condition the book states is not decorative ("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418). Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition — the two missions' shared representation choice (documented in both STATUS.md files) means a future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's TFine) has a compatible object to work with, even though neither imports the other's draft.

Difficulty

The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual solution to the aggregated problem, the book constructs a dual-feasible solution to the exact problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data" hypothesis to make the constructed dual solution well-defined across the exact tree's finer structure. This is a real argument, not a citation, but it is left as sorry: formalizing the proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The value of this mission is the faithful statement of the bound and its exact hypotheses.

Formalization scope

• The book's own printed typo, resolved and documented. Theorem 1's hypothesis clause reads, as printed, "such that (ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" — S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR: the PDF's own typesetting has this repetition, not an artefact of text extraction. This formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome space to project onto (see Setting above — Tree records only history-node structure, not the underlying product space Ω = Ω₁ × ⋯ × Ω_H).
• W, c shared exactly, not aggregated, matching the book's explicit assumption that the recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2) ("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses (hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery that h/Tmat go through.
• zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real infimum's junk value 0 on an unbounded-below or empty feasible set (reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or nonempty by the hypotheses alone.
• The conditional-expectation defining equations are weighted, p·h/p·Tmat, not h/Tmat alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T) equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting measure on a finite partition. Instance's own hp_pos (every node's probability is strictly positive) rules out the degenerate case a bare unweighted equation would need to guard separately (a coarse node of probability 0, which cannot occur, is what the read-back of this theorem flags as the one case where the weighted equation would not pin down h_coarse/ Tmat_coarse themselves — moot here since hp_pos excludes it).
• Trivialization risk (this chapter's own). A formalization that let coarse.h/coarse.Tmat be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation defining equations) would still typecheck a "lower bound" conclusion but assert nothing about aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as arbitrary constants rather than as conditional expectations over a partition of the scenario space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing and present.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 10, §10.1 (pp. 417-420), Theorem 1 (p. 419).
• Birge, J.R. "Decomposition and partitioning methods for multistage stochastic linear programs." Operations Research 33 (1985), 989-1007 — the source Chapter 10's aggregation bounds draw on (cited in §10.2, the neighboring section this mission does not formalize).

Motivation

Two-stage stochastic programs with recourse — choose a first-stage decision $x$ now, observe a random outcome $\xi$, then choose a second-stage recourse decision $y(\xi)$ to repair whatever $x$ left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When $\xi$ ranges over a finite set of scenarios, the recourse function $Q$ that averages the second-stage cost over scenarios is piecewise linear and convex in $x$, so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over $x$ (and a scalar $\theta$ approximating the recourse cost) and, at each candidate $x$, a batch of second-stage linear programs that either certify $x$'s second-stage feasibility or supply a linear underestimate — a cut — of $Q$ around $x$. Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.

Setting

A two-stage recourse instance consists of a first-stage feasible region $K_1 = \{x \mid Ax = b,\ x \ge 0\}$ for $x \in \mathbb{R}^{n_1}$, and, for each of $K$ finite scenarios $k = 1, \dots, K$ (occurring with probability $p_k$), second-stage data $(q_k, h_k, T_k)$ defining the recourse subproblem

$$Q(x, \xi_k) = \min_{y \ge 0} \{ q_k^\top y \mid W y = h_k - T_k x \},$$

where the recourse matrix $W$ is fixed — the same across every scenario, the case this chapter treats. $K_2 = \{x \mid Q(x,\xi_k) < \infty \text{ for all } k\}$ is the set of $x$ for which every scenario's subproblem is feasible, and the two-stage problem is

$$\min_{x} \ c^\top x + Q(x) \quad \text{s.t.} \quad x \in K_1 \cap K_2, \qquad Q(x) = \sum_{k=1}^K p_k\, Q(x, \xi_k).$$

A basis of the recourse subproblem is an injective choice of $m_2$ of $W$'s columns (where $m_2$ is $W$'s row count); each basis $b$ determines a simplex multiplier $\pi = (W_b^\top)^{-1} q_b$, and when $b$ attains the true optimum of $Q(x,\xi_k)$, LP duality gives $Q(x,\xi_k) = \pi^\top(h_k - T_k x)$ — the mechanism that turns a batch of second-stage LP solves into linear cuts on $x$.

Formalization targets

The L-shaped algorithm proceeds in three steps, repeated until neither applies:

• Step 1 solves the current master program (the $K_1$-feasible $x$, plus $\theta$ once at least one optimality cut exists, minimizing $c^\top x + \theta$ subject to every cut recorded so far — or just $c^\top x$ over $K_1$ before the first optimality cut, matching the book's convention that $\theta$ "is set equal to $-\infty$ and is not considered" until then).
• Step 2 tests each scenario's second-stage feasibility at the Step-1 optimum via an auxiliary LP; if some scenario fails (the LP's optimal value is positive), its optimal basis yields a feasibility cut and the algorithm returns to Step 1.
• Step 3, once every scenario is feasible, checks whether $\theta$ already dominates the true recourse cost at $x$ (using each scenario's optimal basis via LP duality); if not, an optimality cut is added and the algorithm returns to Step 1; if so, $x$ is optimal and the algorithm stops.

Goal — Chapter 5, Theorem 2 (p. 198)

$$\text{When } \xi \text{ is a finite random variable, the L-shaped algorithm finitely converges to}$$ $$\text{an optimal solution when it exists, or proves } K_1 \cap K_2 = \varnothing.$$

Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying $K_1 \cap K_2 = \varnothing$) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.

Milestone — Chapter 5, Theorem 1 (p. 194)

$$\text{If } T \text{ is deterministic, } W \text{ is such that every } t \ge 0 \text{ lies in } \mathrm{pos}\,W,$$ $$\text{and } a = \min_k h_k \text{ (componentwise) is attained by some scenario } h_\ell,$$ $$\text{then } x \in K_2 \iff \exists\, y \ge 0,\ Wy = a - Tx.$$

A shortcut avoiding $K$ separate feasibility LPs at Step 2: under these structural assumptions on $W$, checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.

Significance

Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal $x$ exists.

Difficulty

The natural shortcut — state only "an optimal $x$ exists, or $K_1 \cap K_2 = \varnothing$" — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from $K_1 \cap K_2$ being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes $c^\top x + \theta$ jointly, but before the first one it optimizes $c^\top x$ alone; conflating the two (e.g. always requiring $\theta$ to be part of the optimum) does not match Step 1 as the book states it.

Formalization scope

First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of $m_2$ columns of $W$"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that pins the basis to one genuinely attaining the LP's true optimum. The recourse value $Q(x,\xi_k)$ is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far (Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already recorded, and the goal states a bounded-length Step-path from the empty state to a state admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact about $K_2$ as a separate lemma: the finiteness fact it is invoked for is already exposed directly and structurally by the finite Fintype bound on the number of bases, so no additional axiom stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized Decomposition, a different algorithm) are out of scope. The trivializing formalization this mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or- infeasible-$x$ statement with no reference to Steps 1-3 or to a finite bound on the number of iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.

Selected references

• R. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM Journal on Applied Mathematics, 17(4), 1969, pp. 638-663. https://doi.org/10.1137/0117061
• J. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 5. https://doi.org/10.1007/978-1-4614-0237-4
• G. Dantzig, Linear Programming under Uncertainty, Management Science, 1(3-4), 1955, pp. 197-206. https://doi.org/10.1287/mnsc.1.3-4.197

Motivation

Von Neumann introduced amenable groups in 1929 to explain the Hausdorff–Banach–Tarski paradox, and showed that the class $AG$ of amenable groups contains all finite and all abelian groups and is closed under four processes: (I) subgroups, (II) quotients, (III) extensions and (IV) directed unions. Day named the smallest class with these properties $EG$, the elementary amenable groups. For fifty years these were the only amenable groups anyone could exhibit, and von Neumann's question whether every non-amenable group contains a free subgroup on two generators — whether $AG$ equals the class $NF$ of groups without such a subgroup — was open. (It was answered in the negative by Ol'shanskii in 1980, the year of this paper, by different methods.)

Ching Chou's Elementary amenable groups (Illinois J. Math. 24 (1980) 396–407, doi:10.1215/ijm/1256047608) gives the structure theory of $EG$ that everything later relies on. Its central result is that the class can be built from finite and abelian groups by extensions and directed unions alone — subgroups and quotients add nothing (Proposition 2.2). From that description three things follow: periodic elementary amenable groups are locally finite, so the periodic non-locally-finite groups of Golod and Novikov–Adjan show $EG \subsetneq NF$ (Theorem 2.3); a finitely generated simple elementary amenable group is finite (Corollary 2.4); and Wolf's conjecture holds in $EG$: a finitely generated elementary amenable group is almost nilpotent or has exponential growth (Theorem 3.2, extending Milnor and Wolf's theorem for solvable groups). A final section introduces a packing property (P) of groups and proves it for every elementary amenable group (Proposition 4.2) and every residually elementary amenable group (Corollary 4.7).

On this platform the definition of $EG$ is already published (the bundle Chou_ElementaryAmenable, from the mission Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroup), together with the theorem that Thompson's group $F$ is not elementary amenable (Theorem 4.10) and, from Brin and Squier, that $F$ has no free subgroup on two generators (CannonFloydParry.no_free_subgroup_of_rank_two). This mission formalizes Chou's paper on top of that definition.

Setting

The class $EG$ and its constructible core. Chou.ElementaryAmenable G is an inductive predicate on groups: finite groups and abelian groups are in the class, and the class is closed under isomorphism, subgroups, quotients, extensions and directed unions of subgroups; each rule is a constructor of the published bundle Chou_ElementaryAmenable, where it is stated precisely. Chou builds the hierarchy $EG_0 \subseteq EG_1 \subseteq \cdots$ by transfinite recursion, applying only extensions and directed unions to the finite and abelian groups, and proves that $\bigcup_\alpha EG_\alpha$ is closed under subgroups and quotients, hence equals $EG$. The union $\bigcup_\alpha EG_\alpha$ is realised here without ordinals, as the inductive predicate Chou.Constructible, whose constructors are of_finite, of_commGroup, of_mulEquiv, extension and directedUnion; Chou's transfinite induction over $\alpha$ becomes structural induction over a derivation, with the same case analysis.

Periodic and locally finite groups. A group is periodic if every element has finite order (Mathlib's IsMulTorsion) and locally finite if every finitely generated subgroup is finite (Chou.IsLocallyFinite). Day's class $NF$ is Chou.NoFreeSubgroupOfRankTwo: no homomorphism from the free group on two generators into $G$ is injective.

Growth. For a finite generating set $S$ of $G$, Chou.wordBall S n is the set of products of at most $n$ factors, each in $S$ or with inverse in $S$. $G$ has exponential growth if for some finite generating set the ball of radius $n$ has at least $c^n$ elements for some $c > 1$ and all $n$; it is exponentially bounded if for some finite generating set and every $c > 1$ the balls are eventually smaller than $c^n$. Chou works with $|F^n|$ for products of exactly $n$ elements of a finite generating set $F$; for $F$ symmetric and containing the identity the two agree, and Wolf's observation that the growth type is independent of the generating set is one of the milestones. "Almost nilpotent" is Mathlib's Group.IsVirtuallyNilpotent: a nilpotent subgroup of finite index. A free subsemigroup on two generators means two elements $a, b$ such that distinct positive words in $a, b$ are distinct in $G$ (Chou.HasFreeSubsemigroupOfRankTwo).

Packings. A pair of subsets $(S, X)$ is a packing of $G$ if $(s, x) \mapsto sx$ is a bijection $S \times X \to G$ (Chou.IsPacking), and $G$ has property (P) if every finite subset lies in a finite $S$ for which some $(S, X)$ is a packing (Chou.HasPackingProperty). $G$ is residually elementary amenable if every $x \neq 1$ survives in some elementary amenable quotient (Chou.ResiduallyElementaryAmenable).

Target

The goal is Chou's description of the class, Proposition 2.2 (b) (p. 397): “$EG$ is the smallest class of groups which contains all finite groups and all abelian groups and is closed under processes (III) and (IV).” It is stated as the equivalence ElementaryAmenable G ↔ Constructible G. The milestones follow the paper's order.

Section 2. Proposition 2.1 in two halves — the constructible groups are closed under subgroups and under quotients — which is the whole proof of the goal. Theorem 2.3: periodic elementary amenable groups are locally finite; and its consequence that $NF \setminus EG$ is nonempty. Corollary 2.4: finitely generated simple elementary amenable groups are finite.

Section 3. Lemma 3.1 (an extension of almost nilpotent by almost nilpotent is almost nilpotent or of exponential growth), Theorem 3.2 and Rosenblatt's sharpening Theorem 3.2′, together with the facts Chou uses on the way: a finite-by-nilpotent group is almost nilpotent; a free subsemigroup forces exponential growth; Wolf's independence of the generating set; and Milnor's existence of the growth rate, in the form "exponentially bounded means not of exponential growth".

Section 4. Property (P) for finite groups, for $\mathbb Z$, for finitely generated abelian groups; Lemma 4.1 (directed unions and extensions preserve (P)); Proposition 4.2 (every elementary amenable group has (P)); Lemma 4.6 (a) and Corollary 4.7 (residually elementary amenable groups have (P)); and the free groups.

External theorems as milestones

Chou's Section 3 rests on results the paper cites rather than proves, none of which is in Mathlib. They are stated here as milestones in their own right, so that the dependence is visible and each is a well-defined target: the Milnor–Wolf theorem (a finitely generated solvable group that is exponentially bounded is almost nilpotent); M. Hall's theorem that a finitely generated group has finitely many subgroups of each finite index; that finitely generated nilpotent groups are finitely presented and that a group with a finitely presented subgroup of finite index is finitely presented; Milnor's Lemmas 1–2 in the form Chou states on p. 400 (in a finitely generated exponentially bounded group, a normal subgroup with finitely presented quotient is finitely generated); and Rosenblatt's variant of Lemma 3.1. Section 4 needs one more: free groups are residually finite. Lemma 3.1 and Theorems 3.2, 3.2′ can be closed only once these are; every other milestone is provable from Mathlib and the published library.

Two remarks on Theorem 2.3. Chou's witness for $NF \setminus EG$ is a periodic group that is not locally finite (Golod; Novikov–Adjan), whose existence is not formalized. The platform already holds a different witness: Thompson's group $F$ is not elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) and has no free subgroup on two generators (Brin–Squier); both are published and proved, and the milestone is proved from them. The inclusion $EG \subseteq NF$ itself is von Neumann's theorem that amenable groups contain no free subgroup of rank two, which passes through the definition of amenability and is not part of this mission.

What is left out

The ordinal-indexed hierarchy $EG_\alpha$ and the remark that it stabilises at some $\alpha_0 + 1$ (Proposition 2.2 (a)) are replaced by the inductive predicate. Chou's two examples of finitely generated groups in $EG$ that are not almost solvable (p. 402), the Golod–Shafarevich discussion, and Lemma 4.6 (b) (ordinal-indexed normal series) are omitted. Propositions 4.3–4.5 on almost convergent sets, and Milnor's remark that exponentially bounded groups are amenable, need invariant means on $\ell^\infty(G)$; amenability itself is the subject of Garrido I.

References

• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407.
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544.
• J. Milnor, Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968), 447–449; J. A. Wolf, Growth of finitely generated solvable groups and curvature of Riemannian manifolds, ibid. 421–446.
• J. M. Rosenblatt, Invariant measures and growth conditions, Trans. Amer. Math. Soc. 193 (1974), 33–53.
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. 42 (1996), 215–256 (Theorem 4.10); M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985), 485–498.

Motivation

Given independent random variables $X_1,X_2,\dots$, when does $\sum_n X_n$ converge? Not absolutely — that question is settled by $\sum_n\mathbb{E}|X_n|<\infty$ and is usually too strong. The interesting question is when the partial sums converge for almost every outcome, and here independence buys something that holds for no general sequence: convergence is not a delicate matter of cancellation but is decided, once and for all, by three numerical series.

Chapter 2 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) reaches this in section 2.5. Kolmogorov's three-series theorem fixes a truncation level $A>0$, replaces each $X_n$ by $Y_n=X_n\mathbb{1}(|X_n|\le A)$, and asserts that $\sum_n X_n$ converges almost surely if and only if

$$\sum_n\mathbb{P}(|X_n|>A)<\infty,\qquad \sum_n\mathbb{E}Y_n \text{ converges},\qquad \sum_n\operatorname{var}(Y_n)<\infty .$$

Three deterministic conditions on the distributions decide an almost-sure question about paths, and the answer does not depend on which $A$ is chosen. Through Kronecker's lemma this is also the route to the strong law of large numbers, which is how the chapter uses it.

Setting

Let $X_1,X_2,\dots$ be independent real random variables on a probability space, with partial sums $S_N=\sum_{n<N}X_n$. Say that $\sum_n X_n$ converges almost surely when for almost every $\omega$ the sequence $S_N(\omega)$ has a real limit; following Durrett, "$\sum a_n$ converges" means $\lim_N\sum_{n\le N}a_n$ exists, not that it converges absolutely.

Three tools from the same section support the theorem. Kolmogorov's maximal inequality strengthens Chebyshev from $\mathbb{P}(|S_n|\ge x)$ to the maximum of the whole path,

$$\mathbb{P}\Bigl(\max_{1\le k\le n}|S_k|\ge x\Bigr)\le x^{-2}\operatorname{var}(S_n),$$

for independent, centred, square-integrable summands. From it comes the convergence criterion: if $\mathbb{E}X_n=0$ and $\sum_n\operatorname{var}(X_n)<\infty$ then $\sum_n X_n$ converges almost surely. Kronecker's lemma is the deterministic bridge to averages: if $a_n\uparrow\infty$ and $\sum_n x_n/a_n$ converges then $a_n^{-1}\sum_{m\le n}x_m\to0$. And the Hewitt–Savage 0-1 law says that for an i.i.d. sequence every permutable event — one unchanged by rearranging finitely many coordinates — has probability $0$ or $1$.

Formalization targets

Goal — Theorem 2.5.8, Kolmogorov's three-series theorem

$$\sum_n X_n \text{ converges a.s.} \iff \begin{cases} \sum_n\mathbb{P}(|X_n|>A)<\infty,\\ \sum_n\mathbb{E}\bigl[X_n\mathbb{1}(|X_n|\le A)\bigr]\ \text{converges},\\ \sum_n\operatorname{var}\bigl(X_n\mathbb{1}(|X_n|\le A)\bigr)<\infty . \end{cases}$$

Both directions are asserted, as Durrett states the theorem. The truncation level $A>0$ is arbitrary and fixed in the statement; that the three conditions hold for one $A$ exactly when they hold for every $A$ is a consequence, not an assumption.

Supporting levels

Kolmogorov's maximal inequality (2.5.5); the convergence criterion under summable variances (2.5.6); Kronecker's lemma (2.5.9); and the Hewitt–Savage 0-1 law (2.5.4).

Significance

The result itself. The three-series theorem is the complete answer to a question that has no complete answer without independence, and the shape of the answer is the interesting part: a pathwise, almost-sure property is equivalent to three conditions each computable from the marginal distributions alone. Each of the three does a separate job — the first says $X_n$ and its truncation differ only finitely often, so Borel–Cantelli lets them be exchanged; the second controls the drift of the truncated sums; the third controls their fluctuation. The theorem is also the standard route to the strong law: applying it to $X_n/n$ and then Kronecker's lemma gives $S_n/n\to\mu$, which is why section 2.5 sits where it does.

Formalizing it. Mathlib has the strong law of large numbers (strong_law_ae), both Borel–Cantelli lemmas, and Kolmogorov's 0-1 law for the tail σ-field. It has none of the following: Kolmogorov's maximal inequality, the almost-sure convergence criterion for random series with summable variances, Kronecker's lemma, the Hewitt–Savage 0-1 law, or the three-series theorem. The mission therefore contributes the whole of section 2.5, and the pieces are reusable well beyond it — the maximal inequality and Kronecker's lemma in particular are standard tools with no probabilistic content in the second case at all.

Difficulty

The maximal inequality is the step where the argument stops being routine. Chebyshev bounds $\mathbb{P}(|S_n|\ge x)$ and no more; controlling the maximum over the whole path needs the first passage decomposition $A_k=\{|S_k|\ge x,\ |S_j|<x \text{ for } j<k\}$ and the observation that $S_k\mathbb{1}_{A_k}$ is measurable with respect to the first $k$ variables while $S_n-S_k$ is independent of them, so the cross terms vanish. That is a stopping-time argument in disguise, and it is what makes the whole section work.

The sufficiency half of the goal is then assembly: the third series and the convergence criterion give $\sum(Y_n-\mathbb{E}Y_n)$ convergent, the second adds the means back, and the first plus Borel–Cantelli replaces $Y_n$ by $X_n$. Necessity is the harder direction, and Durrett does not prove it in Chapter 2 at all — he defers it to Example 3.4.12, where it follows from the Lindeberg–Feller central limit theorem. A solver attacking the goal should expect the reverse implication to need machinery from outside this section.

The Hewitt–Savage law has a difficulty of its own kind: the natural statement is about a σ-field of events on a sequence space, and the proof approximates a permutable event by cylinder events and then applies the permutation that swaps the first $n$ coordinates with the next $n$.

Formalization scope

Random variables are measurable real-valued functions on a probability space and independence is Mathlib's iIndepFun. Variance is Mathlib's variance, and square-integrability is stated as membership in $L^2$ where the maximal inequality and the convergence criterion need it. The three-series theorem itself assumes no integrability: the truncated variables are bounded, so their means and variances exist automatically, which is exactly why the truncation is there.

"$\sum_n a_n$ converges" is formalized as convergence of the sequence of partial sums to a real limit, not as Summable, which in Mathlib means unconditional and hence absolute convergence for real series. This distinction is not pedantic here: condition (ii) of the theorem is convergence of $\sum\mathbb{E}Y_n$ in Durrett's sense and would be a strictly stronger condition if read as summability. Conditions (i) and (iii) are series of non-negative terms, where the two notions agree, and are stated as Summable.

Almost-sure convergence of $\sum_n X_n$ is "for almost every $\omega$ there exists a real $L$ with $S_N(\omega)\to L$" — the limit is not asserted to be measurable in $\omega$, and does not need to be for the statement to say what it should.

For the Hewitt–Savage law the sequence space is the countable product $\mathbb{N}\to S$ carrying the infinite product of copies of one law, which is Mathlib's Measure.infinitePi, and a permutable event is a measurable set invariant under every finitely supported permutation of the coordinates. That is Durrett's exchangeable σ-field stated directly rather than constructed as a σ-field object.

Contributions welcome beyond the listed items: the converse direction via Lindeberg–Feller (Example 3.4.12); the derivation of the strong law from the three-series theorem and Kronecker's lemma; the Marcinkiewicz–Zygmund law (2.5.12); and the rates of convergence of section 2.5.1.

Selected references

• Rick Durrett, Probability: Theory and Examples, Version 5 (January 11, 2019), section 2.5 (pp. 81–90); Theorems 2.5.4, 2.5.5, 2.5.6, 2.5.8, 2.5.9. Published as Cambridge Series in Statistical and Probabilistic Mathematics, 5th edition, 2019, DOI 10.1017/9781108591034
• A. N. Kolmogorov, Grundbegriffe der Wahrscheinlichkeitsrechnung, Springer, 1933.
• E. Hewitt and L. J. Savage, Symmetric measures on Cartesian products, Transactions of the American Mathematical Society 80 (1955), 470–501. DOI 10.1090/S0002-9947-1955-0076206-8
• P. Billingsley, Probability and Measure, 3rd ed., Wiley, 1995, section 22.

Motivation

A network of resistors solves an optimization problem. Nobody tells the electrons what to do; each one moves under a purely local rule, and the current distribution that emerges minimizes energy dissipation over all distributions satisfying Kirchhoff's node law. Add a wire and the network can only become easier to traverse. This is the encouraging case, and Chapter 4 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) opens with it.

Road traffic is the discouraging case. Drivers also follow a local rule — take the fastest route — and the pattern that emerges is again characterized by an optimization problem, but not the one anyone wants solved. Braess's paradox is the sharp form of the discrepancy: in a small road network carrying six cars per unit time, every route takes 83 time units at equilibrium; open an extra road, and at the new equilibrium every route takes 92. Building road capacity made everyone slower. The difference from the electrical case is that a driver's choice imposes a delay on everyone else sharing the road and the driver does not pay for it, and correcting that — pricing the externality — is how a decentralized rule can be made to produce good global behaviour. That idea recurs in Chapters 7 and 8 of the book as the basis of Internet congestion control.

Setting

The network is a set $\mathcal{J}$ of $J$ directed links. A route $r$ is a subset of links, and $\mathcal{R}$ is the set of $R$ routes under consideration — not necessarily all physically possible ones. The link-route incidence matrix $A$ has $A_{jr}=1$ when $j \in r$ and $A_{jr}=0$ otherwise. Writing $x_r$ for the flow on route $r$, the flow on link $j$ is

$$y_j=\sum_{r}A_{jr}x_r, \qquad\text{that is } y = Ax.$$

Each link has a delay function $D_j(y_j)$, continuous and increasing in the flow on that link, and the delay along a route is the sum of the delays of its links, $\sum_j D_j(y_j)A_{jr}$. Drivers care only about getting from origin to destination: $\mathcal{S}$ is the set of source–destination pairs, each route $r$ serves exactly one of them, written $s(r)$, and the flow requirement between pair $\sigma$ is $f_\sigma$.

A routing pattern is stable when no driver has an incentive to switch. Definition 4.2 makes this precise: a Wardrop equilibrium is a feasible vector of route flows $x$ such that

$$x_r>0 \;\Longrightarrow\; \sum_{j}D_j(y_j)A_{jr}=\min_{r'\in s(r)}\sum_{j}D_j(y_j)A_{jr'}, \qquad y = Ax .$$

Every route actually carrying traffic is a shortest route, in delay, for the traffic it carries.

Formalization targets

Goal — Theorem 4.3, a Wardrop equilibrium exists

$$\exists\, x \ge 0 \ \text{ with } Hx=f \ \text{ such that } x \text{ is a Wardrop equilibrium.}$$

The goal asserts existence only, for an arbitrary network, arbitrary route set and arbitrary continuous increasing delay functions. It fixes no uniqueness claim, because the equilibrium flows need not be unique even though the link loads are, and no efficiency claim, because Braess's paradox is precisely the statement that the equilibrium is not efficient.

Supporting levels

Kirchhoff's node law as the equations satisfied by the expected reward in the random-walk game of section 4.1; the two Braess networks of Figures 4.4a and 4.4b, with their equilibrium delays $83$ and $92$; convexity of $\int_0^{y}D(u)\,du$ for increasing $D$; the optimization characterization that makes the goal reachable — a minimizer of $\sum_j\int_0^{y_j}D_j(u)\,du$ over the feasible flows is a Wardrop equilibrium; and the exact externality decomposition of the queueing network of section 4.3.1.

Significance

The result itself. Theorem 4.3 is what makes the Wardrop equilibrium a usable object: a traffic model that could fail to have an equilibrium would be describing nothing. Its proof does more than establish existence — it identifies the equilibrium as the solution of a specific convex program, minimizing $\sum_j\int_0^{y_j}D_j(u)\,du$. That function is not the total delay $\sum_j y_jD_j(y_j)$, and the gap between the two is exactly Braess's paradox: selfish routing optimizes the wrong objective. Once the two objectives are written side by side, the fix is readable off them, and it is the fix used in practice — a toll on link $j$ equal to $y_jD_j'(y_j)$, the marginal delay a driver imposes on everyone else, makes the selfish objective coincide with the social one. Section 4.3 then carries the same accounting into queueing and loss networks, where the derivative of the mean cost splits into a term for the delay a customer suffers and a term for the knock-on cost it inflicts.

Formalizing it. Nothing here is open; Wardrop stated the principle in 1952 and Beckmann, McGuire and Winsten gave the optimization formulation in 1956. What the mission produces is a machine-checked model of selfish routing — incidence matrix, link flows, delay functions, the equilibrium condition — and a formal record of Braess's paradox as a concrete pair of networks rather than a story. Mathlib has no traffic or congestion-game theory.

Difficulty

Existence is not a fixed-point argument in the obvious variable: the best-response map of the routing game is not continuous, since a small change in flows can flip which route is shortest and move all the traffic. The book's route is to replace the equilibrium condition by the stationarity conditions of a convex program on a compact feasible set, where existence is routine and the content is the translation. The translation is where the care is needed, and it is stated here as a separate milestone: the first-order conditions say the Lagrange multiplier $\lambda_{s(r)}$ equals the route delay on routes carrying traffic and is a lower bound on the others, which is Definition 4.2 restated.

The subtlety worth naming in advance is that "increasing" is doing real work in two different places. It makes $\int_0^{y}D(u)\,du$ convex, which is what makes the program tractable; and it is what makes each $D_j(y_j)$ interpretable as a price. Neither convexity of $D_j$ itself nor strict monotonicity is needed, and assuming them would be assuming more than the book does.

Formalization scope

Links, routes and source–destination pairs are indexed by finite types. The incidence matrix is real-valued with entries constrained to be $0$ or $1$, matching the book's definition in this chapter (unlike Chapter 3, which allows general non-negative integers). The map from routes to source–destination pairs is given as a function $s$ rather than as the matrix $H$, which is exactly the book's statement that each column of $H$ sums to $1$.

Delay functions are total functions $\mathbb{R}\to\mathbb{R}$, continuous and monotone. This excludes the vertical asymptote that Figure 4.5 permits — a link with a finite capacity at which delay blows up — and that restriction is recorded here rather than left implicit. The equilibrium condition is stated as the inequality "$\text{delay on } r \le \text{delay on } r'$ for every $r'$ serving the same pair", which is Definition 4.2 with the minimum written out; the two are equivalent because $r$ itself serves $s(r)$, and the inequality form avoids having to produce a minimum over a possibly empty set.

The goal is not vacuous: the feasibility hypotheses ($f_\sigma\ge0$, and each source–destination pair served by at least one route) are exactly what makes the feasible set non-empty, and without them the existence claim would be false rather than trivial.

Contributions welcome beyond the listed items: uniqueness of the equilibrium link loads $y$; the marginal-cost toll that aligns the selfish and social optima; Rayleigh monotonicity (Exercise 4.3, that effective resistance does not decrease when a resistance is increased); the price of anarchy for affine delays; and Theorem 4.6 on the derivatives of the loss-network rate of return with respect to offered traffic and capacity.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4 (pp. 85–107); Definition 4.2, Theorem 4.3, sections 4.1–4.3. DOI 10.1017/cbo9781139565363
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1 (1952), 325–362. DOI 10.1680/ipeds.1952.11259
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
• D. Braess, Über ein Paradoxon aus der Verkehrsplanung, Unternehmensforschung 12 (1968), 258–268. DOI 10.1007/BF01918335
• Peter Doyle and J. Laurie Snell, Random Walks and Electric Networks, Mathematical Association of America, 1984. arXiv:math/0001057
• R. G. Gallager, A minimum delay routing algorithm using distributed computation, IEEE Transactions on Communications 25 (1977), 73–85. DOI 10.1109/TCOM.1977.1093711

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

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

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

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

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

Supporting levels

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors $x_i \in \{-1, 1\}$. Exhaustive search over $2^n$ sign patterns is intractable, so practitioners relax the problem: replace each sign $x_i$ by a unit vector $X_i$ in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.

Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.

Setting

Fix positive integers $m, n$. Consider a real $m \times n$ matrix $A = (a_{ij})$. Say $A$ is normalized if for every choice of numbers $x_1, \dots, x_m, y_1, \dots, y_n \in \{-1, 1\}$,

$$\Bigl| \sum_{i=1}^m \sum_{j=1}^n a_{ij}\, x_i y_j \Bigr| \;\le\; 1.$$

This says $A$, viewed as a bilinear form on $\{-1,1\}^m \times \{-1,1\}^n$, has sup-norm at most $1$. Now let $H$ be any real Hilbert space — a real vector space equipped with an inner product $\langle \cdot, \cdot \rangle$ complete in the induced norm — and consider vectors $u_1, \dots, u_m \in H$ and $v_1, \dots, v_n \in H$, each of unit norm $\|u_i\| = \|v_j\| = 1$. Replacing the scalar product $x_i y_j$ by the inner product $\langle u_i, v_j \rangle$ in the same bilinear form gives $\sum_{i,j} a_{ij} \langle u_i, v_j \rangle$, a real number depending on the choice of $H$ and of the unit vectors. The question is how large this can be, uniformly over every such choice.

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

$$A \text{ normalized} \;\Longrightarrow\; \Bigl| \sum_{i,j} a_{ij}\, \langle u_i, v_j\rangle \Bigr| \;\le\; K$$

for every real Hilbert space $H$ and unit vectors $u_i, v_j \in H$, where $K$ is a constant depending on neither $A$, its dimensions, nor $H$. This mission's goal formalizes the book's own first-pass bound $K \le 288$ (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for $K$, only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives $K \le 1.783$) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.

Significance

The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a $\{-1,1\}$-valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant $K$. Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP$(A)$ of the integer program INT$(A)$ satisfies INT$(A) \le$ SDP$(A) \le 2K \cdot$ INT$(A)$ — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).

Formalizing it. The inequality and its two chapter milestones are proved but not previously formalized on this platform (checked by concept search for "Grothendieck", "semidefinite", "positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller group). What remains after this mission is the sharper $K \le 1.783$ argument of Section 3.7 (the "kernel trick"), a separate, heavier development building on positive-definite kernels, and full proofs of every milestone below (currently open sorry goals).

Difficulty

The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound $\sum_{i,j} a_{ij}\langle u_i,v_j\rangle$ directly by exploiting the normalization hypothesis on $A$ — fails because the normalization hypothesis only controls $A$ against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto $\{-1,1\}$ without losing information. The book's proof instead represents each unit vector $u_i, v_j$ via a scalar Gaussian random variable $\langle g, u_i\rangle$ for a single Gaussian vector $g$, recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds $A$ against bounded $\pm 1$ inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small-$L^2$-norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space $L^2$ and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with $H = L^2$) as a self-referential bootstrap — this is why the proof fixes $K$ as the smallest valid constant before starting, rather than building it up from scratch.

Formalization scope

The goal and both milestones work with the real matrix and real inner product space directly; H is required to be a complete real inner product space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No dimension bound on $H$ is imposed — the inequality's content is exactly that $K$ does not grow with $\dim H$.

This mission does not formalize the sharper $K \le 1.783$ bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."

A trivializing formalization would state the goal with $K$ allowed to depend on $A$, $m$, $n$, or $H$ — every such bound is easy (e.g. $K = \sum_{ij} |a_{ij}|$) and carries none of the theorem's content; the Lean statement rules this out by quantifying $K$ before every other object. $\mathrm{INT}(A)$ and $\mathrm{SDP}(A)$ (Theorem 3.5.6) are defined from scratch in this chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value construction to reuse. The sub-gaussian (Orlicz $\psi_2$) norm used by Theorem 3.1.1 is reused, unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm) rather than redefined.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985), 93–116.
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803.
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995), 1115–1145.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 3, DOI 10.1017/9781108231596.

Motivation

Any dataset of $N$ points can be described exactly by embedding it in $\mathbb R^n$ for $n$ large enough — but a large $n$ is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with $N$. The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.

Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): $N$ points in any Euclidean space, of any dimension $n$, can be mapped by a single linear map into a space of dimension only $O(\varepsilon^{-2}\log N)$, distorting every pairwise distance by at most a factor of $1\pm\varepsilon$. The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathrm{Prob})$. A random orthogonal projection of rank $m$ in $\mathbb R^n$ is a map $P:\Omega\to(\mathbb R^n\to\mathbb R^n)$, continuous and linear for each $\omega$, such that almost surely $P_\omega$ is idempotent ($P_\omega\circ P_\omega = P_\omega$), self-adjoint, and has range of dimension $m$ — i.e. $P_\omega$ is the orthogonal projection onto some $m$-dimensional subspace $E_\omega\subset\mathbb R^n$. It is uniformly distributed in the Grassmannian $G_{n,m}$ (written $E\sim\mathrm{Unif}(G_{n,m})$) when its law is rotation invariant: for every orthogonal transformation $U$ of $\mathbb R^n$, the conjugated map $\omega\mapsto U\circ P_\omega\circ U^{-1}$ has the same law as $P$. Conjugating a projection by $U$ is exactly the projection onto the image of its range under $U$, so this says the law of the random subspace $E=\mathrm{range}(P)$ is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.

A companion notion drives the proof: a random vector $X$ is uniform on the Euclidean sphere of radius $r$, $X\sim\mathrm{Unif}(r\,S^{n-1})$, when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable $Y$ is sub-gaussian with sub-gaussian ($\psi_2$) norm $\|Y\|_{\psi_2} := \inf\{t>0:\mathbb E\exp(Y^2/t^2)\le 2\}$, the standard non-asymptotic measure of how light-tailed $Y$'s distribution is (a bounded or Gaussian random variable has finite $\psi_2$ norm; the tail probability $\mathbb P\{|Y|\ge s\}$ then decays at least as fast as $2\exp(-cs^2/\|Y\|_{\psi_2}^2)$).

Formalization targets

Goal (Theorem 5.3.1, Johnson-Lindenstrauss Lemma)

$$\exists\,C,c>0:\quad m\ge\frac{C}{\varepsilon^2}\log|X| \;\Longrightarrow\; \mathrm{Prob}\Bigl\{\forall x,y\in X:\ (1-\varepsilon)\|x-y\|_2\le \bigl\|\sqrt{\tfrac nm}\,P_\omega(x-y)\bigr\|_2\le(1+\varepsilon)\|x-y\|_2\Bigr\} \;\ge\;1-2\exp(-c\varepsilon^2 m)$$

for every finite $X\subset\mathbb R^n$, every $\varepsilon>0$, and every random orthogonal projection $P$ of rank $m$ uniformly distributed in $G_{n,m}$. The universal quantifier over pairs $x,y\in X$ sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on $n$, $m$, $N=|X|$, or $\varepsilon$; this is the weakest stable form of the claim (no numeral is hard-coded for $C$ or $c$), matching the book's own statement exactly.

Significance

The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension $m=O(\varepsilon^{-2}\log N)$ depends only on the number of points and the desired distortion, never on the ambient dimension $n$ or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with $n$ — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in $N$: Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of $\Omega(\varepsilon^{-2}\log N/\log(1/\varepsilon))$ on the target dimension, so the $\log N$ dependence cannot be removed.

The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.

Difficulty

The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the $\binom N2$ pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since $\|Pz\|_2$, viewed as a function of a rotated copy of $z$, is a $1$-Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.

Formalization scope

$X$ is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of $N$ points"; $N$ is read off as X.card. The random subspace $E\in G_{n,m}$ is represented throughout by the orthogonal projection $P$ onto it (IsUniformProjection), following the book's own statements, which are phrased in terms of $P$ rather than $E$; the scaled map $Q=\sqrt{n/m}\,P$ of the goal is written Real.sqrt (n/m) • P ω applied to x - y, using linearity of $P_\omega$ to realize $Qx-Qy = Q(x-y)$. Both "uniform on the sphere" and "uniform in the Grassmannian" are defined operationally by rotation invariance of the underlying law, since Mathlib has no ready-made normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance uniquely determines the corresponding measure among those supported on the relevant set, so the operational and constructive definitions coincide extensionally. Every "absolute constant" in the book ($C$ in Theorem 5.3.1's sample-complexity hypothesis, $c$ in every failure-probability bound, and the sub-gaussian constant $C$ of Theorem 5.1.4) is existentially quantified ahead of the dimension, sample size, and every other object, and pinned to no numeral — a formalization that hard-coded a specific numeral for any of these would be invalidated by the next sharper constant in the literature and would not match what the book actually proves.

A trivializing formalization is one that states the conclusion for a single fixed pair $x,y$ rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with $N$ points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).

Reusable infrastructure: subgaussianNorm (the Orlicz $\psi_2$ norm, restated per Vershynin Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric objects are of independent interest to any later chapter needing sub-gaussian random vectors or random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers' contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three supporting lemmas.

Selected references

• W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemporary Mathematics 26 (1984), 189–206.
• N. Alon, Problems and results in extremal combinatorics, I, Discrete Mathematics 273 (2003), 31–53. https://doi.org/10.1016/S0012-365X(03)00227-9
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 5. https://doi.org/10.1017/9781108231596