Operations Research

Motivation

Minimum mean square error (MMSE) estimation — predicting a signal $x$ from a noisy observation $y$ by minimizing expected squared prediction error — underlies linear systems theory, linear regression, Kalman filtering, and multiple-input multiple-output signal processing. Its classical solution assumes the joint distribution of $(x,y)$ is known exactly; in practice it is estimated from data, and the estimator inherits sampling error and model risk. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter shows that hedging the MMSE objective against every distribution in a Wasserstein ball around the empirical distribution — an infinite-dimensional worst case over an intractable set of measures, a priori — collapses to a tractable, finite-dimensional convex semidefinite program (Theorem 25, p. 29), building on the Gelbrich-hull machinery of Section 2.3. This mission formalizes that reduction.

Setting

Fix $m_x, m_y \in \mathbb{N}$ and let $\xi = (x,y) \in \mathbb{R}^{m_x} \times \mathbb{R}^{m_y}$ be a random vector: $x$ the signal to be estimated, $y$ the observation. An estimator is a measurable function $\psi : \mathbb{R}^{m_y} \to \mathbb{R}^{m_x}$; write $\Psi$ for the family of all estimators. The distribution of $\xi$ is only known to lie in a type-2 Wasserstein ball $B_{\varepsilon,2}(\hat P_N)$ centered at an elliptical nominal distribution $\hat P_N = E_g(\hat\mu,\hat\Sigma)$ with nominal mean $\hat\mu \in \mathbb{R}^m$ ($m=m_x+m_y$), nominal covariance $\hat\Sigma \in S^m_+$, and density generator $g$. The distributionally robust MMSE estimation problem is

$$\inf_{\psi \in \Psi} \sup_{Q \in B_{\varepsilon,2}(\hat P_N)} E_Q\big[\|x-\psi(y)\|_2^2\big]. \tag{35}$$

Writing $\hat\Sigma = \begin{pmatrix}\hat\Sigma_{xx}&\hat\Sigma_{xy}\\\hat\Sigma_{yx}& \hat\Sigma_{yy}\end{pmatrix}$ blockwise, the nonlinear convex SDP

$$\max_S f(S) = \mathrm{Tr}[S_{xx} - S_{xy}S_{yy}^{-1}S_{yx}] \quad \text{s.t.} \quad S = \begin{pmatrix}S_{xx}&S_{xy}\\S_{yx}&S_{yy}\end{pmatrix} \succeq 0,\; S_{xx} \succeq 0,\; S_{yy} \succeq 0,\; \mathrm{Tr}[S+\hat\Sigma-2(\hat\Sigma^{1/2}S\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2,\; S \succeq \lambda_{\min}(\hat\Sigma) I \tag{36}$$

is the finite-dimensional relaxation the chapter builds toward.

Formalization targets

Goal (Theorem 25, distributionally robust MMSE estimator). If $\hat\Sigma \succ 0$, then the optimal value of problem (35) equals the optimal value of SDP (36). Moreover, if $S^\star$ is optimal in (36) with $S^\star_{yy}$ invertible, then the affine function

$$\psi^\star(y) = S^\star_{xy}(S^\star_{yy})^{-1}(y-\hat\mu_y) + \hat\mu_x$$

attains the outer infimum of (35) — it is a distributionally robust MMSE estimator, exhibited in closed form from an SDP optimizer.

Significance

Theorem 25 reduces an a priori infinite-dimensional, worst-case functional optimization problem (an infimum over all measurable estimators of a supremum over all distributions within a Wasserstein ball) to a finite convex program with one linear matrix inequality, one Loewner-order lower bound, and one trace/matrix-square-root constraint — solvable in polynomial time, with the optimal estimator recovered in closed form from the SDP's optimal block matrix. It shows that robustifying MMSE estimation against distributional ambiguity does not sacrifice tractability: the resulting estimator remains affine, the same functional form as the classical (non-robust) best linear unbiased estimator, only with its coefficients drawn from a regularized covariance estimate rather than the raw sample covariance. Formalizing it fixes, machine-checkably, the exact shape of that regularization — which SDP constraints are load-bearing (the Loewner lower bound in particular rules out a numerically unstable near-singular $S_{yy}$) and which conditions ($\hat\Sigma \succ 0$, $S^\star_{yy}$ invertible) the closed-form estimator formula actually needs.

Difficulty

The paper's own remark (p. 29) names the two nontrivial steps: first, "establishing a minimax theorem for (35) and exploiting the properties of elliptical distributions" to show the outer infimum is attained by an affine estimator — a priori (35) ranges over all measurable $\psi$, and there is no obvious reason the worst case forces linearity. Second, "combining this structural insight with Theorem 16" (the SDP-representability result for indefinite quadratic losses under an elliptical nominal distribution, itself a nontrivial closed-form reduction of an infinite-dimensional worst-case risk) to convert the now-restricted problem over affine estimators into the finite SDP (36). Neither step is a routine consequence of the ambiguity-set definitions alone; each requires structural facts about elliptical distributions and quadratic losses proved earlier in the chapter.

Formalization scope

The signal-observation space is EuclideanSpace ℝ (Fin mx ⊕ Fin my), with $x$ and $y$ recovered as the two summand projections; the block matrix $S$ is Matrix (Fin mx ⊕ Fin my) (Fin mx ⊕ Fin my) ℝ, and Matrix.toBlocks₁₁/toBlocks₁₂/toBlocks₂₁/toBlocks₂₂ give its four blocks. The constraint "$S_{xy}=S_{yx}^\top$" is not stated as a separate hypothesis: it follows automatically once $S$ is symmetric (implied by S.PosSemidef), so encoding the feasible set from a single symmetric S rather than four independently-quantified blocks makes it structurally impossible to drop — see pitfall 4 of BRIEF.md. The outer infimum of problem (35) ranges only over measurable $\psi$ (Measurable ψ on the binder), matching the paper's own definition of $\Psi$ as "the family of all possible measurable estimators" (p. 29) exactly. λ_min(Σ̂) is taken as a hypothesis parameter characterized by the two properties that make it the minimum ("≤ every eigenvalue of Σ̂, and attained by some eigenvalue"), rather than invoking a specific Mathlib min-eigenvalue API by name. S_{yy}⁻¹ uses the ordinary matrix inverse (junk zero matrix when singular), matching the paper's literal notation; S^\star_{yy} invertible is stated as an added hypothesis, not present verbatim on the page, because the paper leaves the formula's well-definedness implicit — disclosed per pitfall 5 rather than silently assumed away. The paper's own "which is always solvable" clause is not asserted: Theorem 25 states, as part of itself, that SDP (36) attains its maximum (an unconditional existence claim for an optimal $S^\star$); this formalization states only the conditional consequences of such an $S^\star$ existing, not that one does — proving or asserting solvability is out of this mission's scope, so the Lean statement is strictly weaker than Theorem 25's own conclusion on this point, disclosed rather than silently dropped. All risk-style suprema are EReal-valued and Integrable-guarded, matching the series' convention. No milestone theorem is included: the paper's own proof sketch derives (33)'s and by extension (36)'s SDP "via Theorem 16", but Theorem 16 (indefinite quadratic loss and $p=2$, eq. 23) was itself judged too heavy to state faithfully in 02-gelbrich's time budget and is not redefined here either — see STATUS.md. Theorem 24 (the Wasserstein shrinkage estimator, this chapter's originally recommended goal) is out of scope: its closed-form eigenvalue transformation (eq. 34a/34b) requires transcribing nested square roots from a rendered PDF page that this session's time budget did not allow verifying to the standard the brief demands (pitfall 1); the brief's own documented fallback to Theorem 25 was taken instead.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Nguyen, V. A., Shafieezadeh-Abadeh, S., Yue, M.-C., Kuhn, D., & Wiesemann, W. (2021). Optimistic distributionally robust optimization for nonparametric likelihood approximation. Advances in Neural Information Processing Systems, 32.
• Shafieezadeh-Abadeh, S., Nguyen, V. A., Kuhn, D., & Mohajerin Esfahani, P. (2018). Wasserstein distributionally robust Kalman filtering. Advances in Neural Information Processing Systems, 31.

Motivation

Distributionally robust optimization (DRO) hedges a decision against every distribution within some ambiguity set around an estimated (nominal) distribution, rather than trusting the estimate exactly. When the ambiguity set is a ball of radius $\varepsilon$ around the empirical distribution $\hat P_N$ in the type-$p$ Wasserstein metric, the resulting worst-case risk problem inherits attractive statistical guarantees (Mohajerin Esfahani & Kuhn 2018) but is, in general, an optimization problem over an infinite-dimensional space of measures. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter surveys when this problem becomes computationally tractable. One route — the subject of this mission — discards everything about the nominal distribution except its mean vector and covariance matrix and replaces the Wasserstein ball with a set built only from these two moments, the Gelbrich hull. The construction is due to Gelbrich (1990), who first bounded the Wasserstein distance between two distributions using only their means and covariances.

Setting

Fix $\Xi \subseteq \mathbb{R}^m$, a nominal distribution $\hat P_N \in \mathcal{P}(\Xi)$, a radius $\varepsilon > 0$ and an exponent $p \ge 1$. The type-$p$ Wasserstein distance between two probability measures $Q, Q'$ on $\mathbb{R}^m$ is

$$W_p(Q,Q') = \Big(\inf_{\pi \in \Pi(Q,Q')} \int \|\xi-\xi'\|^p \, d\pi(\xi,\xi')\Big)^{1/p},$$

the infimum over couplings $\pi$ (probability measures on $\mathbb{R}^m \times \mathbb{R}^m$ with marginals $Q$ and $Q'$) of the $p$-th root of the expected $p$-th power of Euclidean distance. The Wasserstein ambiguity set is $B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\}$, and the worst-case risk of a loss function $\ell$ is $R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)]$.

Suppose $\hat P_N$ has mean vector $\hat\mu$ and covariance matrix $\hat\Sigma \in S^m_+$ (the positive semidefinite $m\times m$ matrices). The mean-covariance uncertainty set is

$$U_\varepsilon(\hat\mu,\hat\Sigma) = \Big\{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}\big[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2}\Sigma\hat\Sigma^{1/2})^{1/2}\big] \le \varepsilon^2\Big\},$$

where $\Sigma^{1/2}$ is the positive-semidefinite square root. The Gelbrich hull is $G_\varepsilon(\hat\mu,\hat\Sigma) = \{Q \in \mathcal{P}(\Xi) : (E_Q[\xi],\mathrm{Cov}_Q[\xi]) \in U_\varepsilon(\hat\mu,\hat\Sigma)\}$: the distributions on $\Xi$ whose own mean and covariance lie in $U_\varepsilon(\hat\mu,\hat\Sigma)$. An elliptical distribution $E_g(\mu,\Sigma)$ has density $f(\xi) = C \cdot \det(\Sigma)^{-1} g\big((\xi-\mu)^\top\Sigma^{-1}(\xi-\mu)\big)$ for a density generator $g$ and normalizing constant $C$; two elliptical distributions "have the same density generator" when their $g$ coincide (e.g. both Gaussian, both Student-$t_\nu$ for the same $\nu$).

Formalization targets

Goal (Theorem 13, Gelbrich hull). For every $p \ge 2$,

$$B_{\varepsilon,p}(\hat P_N) \subseteq G_\varepsilon(\hat\mu,\hat\Sigma).$$

This is an outer approximation: every distribution within $\varepsilon$ of $\hat P_N$ in Wasserstein distance has a mean and covariance inside $U_\varepsilon(\hat\mu,\hat\Sigma)$, so optimizing over the Gelbrich hull instead of the Wasserstein ball can only enlarge the feasible set, never shrink it below the truth.

Supporting results. Theorem 4 (Gelbrich bound) gives the moment-only lower bound on $W_2$ that Theorem 13 is built from, with equality for elliptical distributions sharing a generator. Proposition 1 sharpens the goal's containment to an equality on the mean-covariance projection itself, under the same two conditions ($\Xi = \mathbb{R}^m$, $\hat P_N$ elliptical). Corollary 1 propagates the goal's set containment to the risk level: $R_{\varepsilon,p}(\hat P_N,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell)$ for every $\ell$, where $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ is the Gelbrich risk.

Significance

Theorem 13 is the hinge between an intractable infinite-dimensional worst-case-risk problem and a tractable one: the paper goes on (Theorem 16, outside this mission's scope) to show that for quadratic loss functions and elliptical nominal distributions the Gelbrich risk itself equals the optimal value of a semidefinite program with two linear matrix inequality constraints — and that, under those same conditions, the Wasserstein worst-case risk, the Gelbrich risk and the SDP value all coincide. Corollary 1 is what makes the Gelbrich risk usable as a conservative surrogate even outside that special case: it upper-bounds the true worst-case risk for any loss function and any $p \ge 2$, at the cost of discarding all but first- and second-order information about the nominal distribution. Formalizing the goal and Corollary 1 gives the exact scope in which this moment-relaxation is licensed — the $p \ge 2$ restriction and the outer-approximation direction are both easy to get backwards, and this mission's Lean encoding fixes both irreversibly.

Difficulty

The obvious first argument is to prove containment pointwise: fix $Q \in B_{\varepsilon,p}(\hat P_N)$ and show its mean and covariance land in $U_\varepsilon(\hat\mu,\hat\Sigma)$. That reduces Theorem 13 to Proposition 1's containment half, which in turn reduces to the Gelbrich bound (Theorem 4) applied to the pair $(Q,\hat P_N)$ — the inequality direction of Theorem 4 suffices for containment; only the sharper equality direction (needed for Proposition 1's own equality clause) requires the elliptical hypothesis. The non-obvious step is Theorem 4 itself: bounding $W_2(Q,Q')$ below by a closed-form expression in the two distributions' first two moments only, for arbitrary $Q,Q'$ with those moments, requires an argument that survives every coupling $\pi$ — the paper's proof goes through a lower bound on the coupling's cross-covariance term via the eigenvalues of $\Sigma^{1/2}\Sigma'\Sigma^{1/2}$, not a direct manipulation of $W_2$'s definition.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m); a "distribution" is a MeasureTheory.Measure on it constrained by Q Set.univ = 1 (probability) and Q Ξᶜ = 0 (support in Ξ). The Wasserstein distance is ENNReal-valued (Definition 1's infimum over couplings, matching 01-duality's convention); the worst-case and Gelbrich risks are EReal-valued suprema restricted to loss functions integrable under the candidate distribution, avoiding Mathlib's junk value for a non-integrable Bochner integral. $\Sigma^{1/2}$ is the positive-semidefinite matrix square root, picked by choice from its defining existential and applied in this mission only to matrices hypothesized (or, per Section 2.3's standing assumption, given) positive semidefinite. Elliptical distributions (IsElliptical) are represented by the paper's own density formula (a measure equal to volume.withDensity of C·det(Σ)⁻¹·g((ξ-μ)ᵀΣ⁻¹(ξ-μ)) for some C>0), together with the mean/covariance facts every theorem in this chunk reads off directly; an earlier draft kept only the latter, under which "same density generator" held vacuously for any moment-matched pair — corrected after moderation flagged it (see STATUS.md). Because 01-duality (Wasserstein distance, ambiguity set, worst-case risk) is not yet a published mission, this chunk redefines those objects locally in its own namespace rather than importing an unpublished draft, per the series' definition-reuse policy; a future upload can retire the duplication once 01-duality is live. A formalization that dropped Theorem 4's "same density generator" condition from its equality clause, or that stated the goal's containment for all $p\ge 1$ rather than $p \ge 2$, would be trivializing or simply false — both are explicit hypotheses in the Lean statements. Matrix.PosSemidef and its Loewner order carry the $S^m_+$ constraints; no elliptical-distribution or Gelbrich-hull infrastructure exists elsewhere on the platform, so this mission's definitions are original contributions reusable by any later extension (Theorem 16/17, Lemma 1/2's SDP representations) of this series.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Gelbrich, M. (1990). On a formula for the L2 Wasserstein metric between measures on Euclidean and Hilbert spaces. Mathematische Nachrichten, 147(1), 185–203.
• Mohajerin Esfahani, P., & Kuhn, D. (2018). Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations. Mathematical Programming, 171(1), 115–166.

Counting terms and comparing the resulting sums

Chapters III and IV formalize what it means for one random variable to be "more spread out" or "larger and more spread out" than another. Chapter VIII asks a different kind of question: if the number of terms in a sum of i.i.d. random variables is itself random, and one count is larger than another in one of these orders, does the resulting random sum inherit the comparison? This mission formalizes the chapter's own answer — Theorem 8.A.13 — a clean, self-contained closure result that needs only the icx/icv/cx orders from Chunks 03/04 (restated locally) and one nonnegative-integer-valued index, without the heavier parametric-family apparatus (SICX, SICV, SIL, and the stochastic-convexity-of-a-family notions) that occupies most of the rest of the chapter.

The icx/icv/cx orders, restated for this chapter

This chapter restates the univariate increasing convex, increasing concave and convex orders (Chunks 04 and 03's own subjects) locally, since drafts cannot import another mission's definitions: for random variables $X,Y$, $X\le_{icx}Y$ [$X\le_{icv}Y$] if $E[\varphi(X)]\le E[\varphi(Y)]$ for every increasing convex [concave] $\varphi:\mathbb{R}\to\mathbb{R}$ for which the expectations exist, and $X\le_{cx}Y$ if the same holds for every convex $\varphi$ (dropping "increasing"). Theorem 8.A.13 applies these same three orders to nonnegative-integer-valued random variables $M,N$ — a special case of the real-valued order (after the coercion $\mathbb{N}\to\mathbb{R}$), not a separate discrete order, per this chapter's own pitfall 1.

Formalization target

Goal: closure of the icx/icv/cx orders under random sums (Theorem 8.A.13)

Let $\{Y_k, k\in\mathbb{N}_{++}\}$ be i.i.d. nonnegative random variables, independent of the two nonnegative discrete random variables $M$ and $N$. Then

$$M\le_{icx}[\le_{icv}]\,N \implies \sum_{k=1}^{M}Y_k \le_{icx}[\le_{icv}]\sum_{k=1}^{N}Y_k, \qquad M\le_{cx}N \implies \sum_{k=1}^{M}Y_k \le_{cx}\sum_{k=1}^{N}Y_k.$$

Comparing the number of terms propagates to a comparison of the resulting random sums. This is "an application of these notions in establishing a stochastic inequality," in the book's own words right before the theorem — the formal content behind Example 8.A.2's claim that a homogeneous Poisson process is SIL, via the semigroup property of Example 8.A.7 (neither a numbered theorem, so neither is drafted as a milestone here — cited as background only, per CAPTAIN_BRIEF.md rule 5).

The book's proof defines $\psi(n) = E[\varphi(\sum_{k=1}^n Y_k)]$ for an increasing convex [concave] $\varphi$ and observes (via the unnumbered Example 8.A.4) that $\psi$ is itself increasing and convex [concave] in $n$; the icx/icv order on $M,N$ then transfers directly to $\psi(M)$ vs. $\psi(N)$, giving part (a). Part (b) follows from part (a) together with the equal-means fact $E[\sum_{k=1}^M Y_k]=E[\sum_{k=1}^N Y_k]$ under $M\le_{cx}N$ (Theorem 4.A.35, a Chapter 4 result not restated in this mission).

Significance

Random sums are the natural model for aggregate risk, total service time, or total demand when the number of contributing terms is itself uncertain — the number of claims in an insurance period, the number of customers served, the number of jobs in a batch. Theorem 8.A.13 is the tool that lets an analyst reduce a comparison of two such aggregates to a comparison of the (often much simpler) counting processes that generate them, without having to reason about the joint distribution of the sums directly. It is also the concrete instance, stripped of the rest of the chapter's parametric-family machinery, of a pattern that recurs throughout the book: an order on an index set (here, the count $M$ vs. $N$) transferring through a monotone/convex construction (here, summation) to an order on the resulting random variables — the same shape Chunk 06's Theorem 6.B.16(b) and Chunk 07's Theorem 7.A.9 each illustrate in their own settings.

No platform prior art exists: GET /theorems?q=random+sum, q=compound+distribution, q=Poisson+process, and q=renewal return nothing usable (the last returns only MarkovMixing/CLT-adjacent hits, not classical renewal or compound-sum results, confirmed at triage time and re-checked this session). This mission restates the icx/icv/cx orders and their random-sum closure as a self-contained result, independently drafted since drafts cannot import Chunks 03/04's Lean.

Difficulty

The chief formalization risk is treating $M\le_{icx}N$ as a separate "discrete" order rather than the same real-valued order applied to $\mathbb{N}$-valued random variables after coercion — this chapter's own pitfall 1. A second risk is drafting $\sum_{k=1}^{M}Y_k$ as a fixed-length sum with $M$ substituted in afterward, rather than a genuine random (randomly-stopped) sum where $M$ is itself random and independent of the $\{Y_k\}$ sequence — this chapter's own pitfall 2; the independence hypothesis has to be carried explicitly, not left as an unstated convention. A third risk, common to every bracketed theorem in this series, is conflating the icx and icv cases of part (a) into a single Or-joined statement rather than two clearly distinguished conjuncts — this chapter's own pitfall 3.

A different kind of risk, specific to this chapter, is scope creep into the parametric-family apparatus (SI, SCX, SICX, SIL, and the "family indexed by $\theta\in\Theta$" definitions) that occupies most of Chapter 8: as BRIEF.md's own Setup note observes, that apparatus is heavier than the rest of the book (a family, a parameter set, and several bracketed cases per definition), and a trivializing risk specific to it — flagged in this chapter's pitfall 4 — is a family predicate that is vacuously true for a degenerate parametrization (e.g. $\Theta$ a singleton). This mission avoids that risk entirely by choosing the one clean, self-contained closure theorem in the chapter that needs none of it.

Formalization scope

The icx/icv/cx orders are restated locally (IcxOrder, IcvOrder, ConvexOrder, univariate, real-valued), exactly matching Chunks 04 and 03's own shapes, since drafts cannot import another mission's definitions. $M,N:\Omega\to\mathbb{N}$ are nonnegative-integer-valued; the orders are applied to them via the coercion fun ω => (M ω : ℝ) (resp. N), matching pitfall 1 exactly — no separate discrete-order predicate is introduced. The i.i.d. sequence is drafted as Y : ℕ → Ω → ℝ (indexing Y 0, Y 1, … for the book's Y_1, Y_2, …, a one-step reindexing noted explicitly rather than left implicit), with iIndepFun Y μ for mutual independence and IdentDistrib (Y j) (Y k) μ μ for every j, k for identical distribution, plus 0 ≤ᵐ[μ] Y k for nonnegativity. The random sum itself is ∑ k ∈ Finset.range (M ω), Y k ω — a genuine randomly-stopped sum, per pitfall 2 — and independence of $\{Y_k\}$ from $(M,N)$ jointly is IndepFun (fun ω => (M ω, N ω)) (fun ω k => Y k ω) μ, treating the whole sequence as one ℕ → ℝ-valued random element, stated as an explicit hypothesis rather than an implicit convention. The theorem's three conjuncts (icx, icv, cx) mirror the book's own single Theorem 8.A.13, whose part (a) bundles the icx/icv brackets and whose part (b) states the cx case separately, per pitfall 3.

A trivializing formalization this mission rules out: substituting M into a fixed-length Finset.range n sum after the fact (erasing the random-stopping structure that makes this a random-sum theorem at all) rather than genuinely summing over Finset.range (M ω), and treating M ≤icx N as anything other than the same real-valued order Chunks 03/04 define, applied after coercion. This mission draws on no platform prior art (searches for "random sum", "compound distribution", "Poisson process" and "renewal" as of 2026-09-18 return nothing usable). Unlike every other chapter in this series so far, this mission has no milestone theorems: every other numbered result near the goal in this chapter needs the parametric-family apparatus this mission deliberately avoids, and the un-numbered facts the goal's own proof cites (Example 8.A.4's potential-function monotonicity, Example 8.A.7's semigroup property) cannot be milestones per CAPTAIN_BRIEF.md rule 5 — see STATUS.md for the full accounting.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 8 (Stochastic Convexity and Concavity), §8.A.1–8.A.2. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 03 (StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex), for the univariate convex and increasing convex/concave orders this chapter restates locally.

Motivation

A cooperative game with side payments models a set of economic agents who can form coalitions and split the proceeds. The central question is stability: is there a way to split the total payoff among all the players so that no subset of them would do better by breaking away and acting on its own? The set of such stable splits is the core, introduced by Gillies [1959] and studied extensively since (Shapley [1971], Shapley [1953]). Sharkey [1982c] surveys the core's role in the economics of natural monopoly, where "no coalition wants to secede" is exactly the condition that a cost-sharing scheme is defensible against any subgroup of customers.

The core of an arbitrary cooperative game can be empty — there may be no split that satisfies every coalition simultaneously — and even when nonempty it can be hard to exhibit a point in it, since it is cut out by $2^n$ linear inequalities. Shapley [1971] identified a large and economically natural class, the convex games (characteristic functions that are supermodular in the coalition), for which the core is always nonempty, and for which an explicit family of core points — one per ordering of the players — can be written down directly. This mission formalizes Shapley's theorem and its later sharpening: this book's central result of Chapter 5, together with a genuine converse (Moulin [1990], sharpening an observation of Sharkey [1982a]) and comparative-statics theorem (Topkis [1987]) showing how these core points move as the underlying economics changes.

Setting

Fix a finite set of players $N = \{1,\dots,n\}$. A characteristic function $f$ assigns a real number $f(S)$ to every coalition $S \subseteq N$, with $f(\emptyset) = 0$; $f(S)$ is the net return a coalition $S$ could earn on its own. The pair $(N,f)$ is a cooperative game, and throughout this chapter $f$ is assumed superadditive: $f(S') + f(S'') \le f(S' \cup S'')$ for disjoint $S', S''$. A payoff vector $y \in \mathbb{R}^N$ is feasible if $\sum_{i \in N} y_i = f(N)$, and acceptable if $\sum_{i \in S} y_i \ge f(S)$ for every coalition $S$. The core is the set of payoff vectors that are both:

$$\mathrm{Core}(N,f) = \Big\{ y \in \mathbb{R}^N : \sum_{i \in N} y_i = f(N) \text{ and } f(S) \le \sum_{i \in S} y_i \ \forall S \subseteq N \Big\}.$$

$(N,f)$ is a convex game if $f$ is supermodular on the Boolean lattice of coalitions: $f(S) + f(S') \le f(S \cup S') + f(S \cap S')$ for all $S, S'$. ("Convex" is the game-theory literature's name for this supermodularity property; it has no relation to convexity of sets or of real functions, a collision the book itself flags.) Equivalently, by Theorem 2.6.1/2.6.4, a game is convex exactly when the marginal value $f(S \cup \{i\}) - f(S)$ of any player $i$ to any coalition $S$ not containing $i$ increases as $S$ grows — the more players already committed to a project, the more valuable one more player is to it.

Given a permutation $\pi$ of $N$, let $S_\pi(j) = \{\pi(1),\dots,\pi(j)\}$. The greedy algorithm builds the payoff vector $y^\pi$ by paying each player its marginal contribution when added in the order $\pi$: $y^\pi_{\pi(j)} = f(S_\pi(j)) - f(S_\pi(j-1))$. The Shapley value pays player $i$ the average of $y^\pi_i$ over all $n!$ permutations $\pi$, equivalently $\sum_{S \subseteq N\setminus\{i\}} \frac{|S|!(n-|S|-1)!}{n!}(f(S\cup\{i\}) - f(S))$.

A core is large if every acceptable payoff vector is dominated, coordinatewise, by one in the core; a subgame $(N',f)$ restricts $f$ to subsets of $N' \subseteq N$; a core is totally large if the core of every subgame is large.

Formalization targets

Goal — Theorem 5.2.1 (Shapley [1971])

$$\text{if } (N,f) \text{ is a convex game, then for every permutation } \pi,\ y^\pi \in \mathrm{Core}(N,f); \quad \mathrm{Core}(N,f) \ne \emptyset; \quad \text{Shapley value} \in \mathrm{Core}(N,f).$$

The weakest stable statement here is already the union of these three claims: nonemptiness of the core (b) is a formal consequence of (a) for any single permutation, and (c) is a genuinely separate fact about the average of the $y^\pi$'s, not implied by (a) and (b) alone.

Milestones

• Lemma 5.2.1(a): $\sum_{i \in S_\pi(j)} y^\pi_i = f(S_\pi(j))$ for every $j = 1,\dots,n$ — the partial-sum identity the goal's proof of acceptability is built on.
• Theorem 5.2.6 (Moulin [1990]): a cooperative game is convex if and only if its core is totally large — the converse direction that a large core alone (Theorem 5.2.1's easy corollary) does not give.
• Theorem 5.2.7(a,b) (Topkis [1987]): if the characteristic function $f^t$ of a family of games has increasing differences in a parameter $t$ (a complementary parameter), the greedy payoff vector and the Shapley value both increase in $t$.

Significance

Theorem 5.2.1 is the reason convex games are the tractable case of cooperative game theory: it turns an existence question about $2^n$ linear inequalities into an explicit construction (any ordering of the players gives a point in the core), and it identifies the Shapley value — an axiomatically motivated but a priori only feasible payoff rule — as one that always respects every coalition's participation constraint on this class. Theorem 5.2.6 shows this is not an accident of the sufficient condition: total largeness of the core is a genuine characterization of convexity, so "does every subgame's core dominate every acceptable vector" is an equivalent, purely core-theoretic way to test convexity. Theorem 5.2.7 gives the comparative statics that make convex games useful in applied models (Chapter 5's later sections build monopoly, surplus sharing, and procurement games on exactly this apparatus): as a game's characteristic function improves in a complementary way with some parameter (a price, a technology level, a capacity), every player's greedy payoff and Shapley value improve monotonically, with no separate argument needed for each application.

Formalizing this mission produces, for the first time on the platform, machine-checked statements of the core, convex games, the greedy algorithm and the Shapley value — definitions that later missions in this series's own polyhedral-structure sections, and any future cooperative-game-theory mission, can reuse rather than re-derive. All three results already have a complete proof in the literature; this mission's remaining work is formalizing that known argument, not any open mathematics.

Difficulty

The routine first idea — check acceptability for the greedy vector one subset at a time using only the definition of supermodularity — does not directly work: Theorem 5.2.1(a)'s proof needs to compare a subset $S'$ against the initial coalitions $S_\pi(j)$ built by the particular permutation $\pi$, splitting $S'$ by the first and last time one of its elements appears in $\pi$'s order and applying supermodularity along the resulting chain, not a single inequality. Theorem 5.2.6's converse direction is the harder half: showing a totally large core forces supermodularity requires constructing an auxiliary characteristic function $g(S) = \max_{S \subseteq S' \subseteq N} \big(f(S') - \sum_{i \in S'} y''_i\big)$ from an arbitrary acceptable vector $y''$ and showing $g$ is itself supermodular (via Theorem 2.6.4 and Theorem 2.7.6, results from the earlier monotone-comparative-statics chapter this mission depends on) before the argument closes.

Formalization scope

Players are modeled as Fin n and a characteristic function as f : Finset (Fin n) → ℝ; a payoff vector is y : Fin n → ℝ, and the core's feasibility and acceptability conditions are stated with respect to Finset.univ (the whole player set) or a coalition U : Finset (Fin n) for a subgame, never approximated by a finite sample of coalitions or by feasibility alone — the acceptability condition genuinely quantifies over every subset. The Shapley value's coefficient is the exact rational weight S.card.factorial * (n - S.card - 1).factorial / n.factorial cast to ℝ, not a placeholder constant. The greedy algorithm's InitialCoalition σ j uses Lean's 0-indexed Equiv.Perm (Fin n) throughout, with the book's 1-indexed $S_\pi(j)$ absorbed into the definition rather than into the index j, so the definition and the goal read the same j consistently. Theorem 5.2.7(c), which needs Theorem 5.2.4's convex-combination-of-extreme-points machinery beyond this section, is out of scope for this mission.

A trivializing formalization would state acceptability only on singleton coalitions, or would let n = 0/an empty player set stand in for the general case; neither is used here — every Core/IsLargeCore statement quantifies over arbitrary subsets, and none of the theorems restrict n.

This mission reuses Supermodularity.Monotonicity.SupermodularOn and Supermodularity.Monotonicity.IncreasingDifferencesOn from this series's chunk II (02-monotonicity) rather than restating supermodularity or increasing differences for coalitions from scratch. InitialCoalition, Core, GreedyPayoff, IsConvexGame, IsLargeCore, IsTotallyLargeCore and ShapleyValue are new to this mission and reusable by any later mission on cooperative games, polymatroids, or the polyhedral structure of the core (Section 5.2.3 of this chapter). Contributions completing the sorrys — Theorem 5.2.1(a)'s chain-splitting argument, Theorem 5.2.6's auxiliary-function construction, and Theorem 5.2.7(a,b)'s direct comparison — are all welcome.

Selected references

• L. S. Shapley, "Cores of convex games," International Journal of Game Theory, 1(1), 1971, 11–26. https://doi.org/10.1007/BF01753431
• L. S. Shapley, "A value for n-person games," in Contributions to the Theory of Games II, Princeton University Press, 1953, 307–317.
• H. Moulin, "Cores and large cores when population varies," International Journal of Game Theory, 19(3), 1990, 219–232. https://doi.org/10.1007/BF01766437
• W. W. Sharkey, "Cooperative games with large cores," International Journal of Game Theory, 11(3-4), 1982, 175–182. https://doi.org/10.1007/BF01766193
• D. M. Topkis, "Activity optimization games with complementarity," European Journal of Operational Research, 28(3), 1987, 358–368. https://doi.org/10.1016/0377-2217(87)90232-5
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011, Chapter 5. https://doi.org/10.1515/9781400822539

Motivation

Which workers end up at which firms, and does higher quality always land at the more productive employer? This is the question of assortative matching: whether an efficient assignment pairs the best workers with the best firms, the second-best with the second-best, and so on down the line. The question has a long history in labor economics. Becker [1973] showed, for the simplest case of two-sided homogeneous firms and a single worker characteristic, that profit maximization under complementarity forces exactly this kind of sorting. Kremer [1993] extended the analysis to firms with many workers of a single type, under a specific Cobb–Douglas production function. What was missing was a general theory: one that covers firms hiring several types of workers simultaneously, firms that differ in efficiency, and labor markets of any degree of tightness, while still deriving sorting from a single primitive economic condition rather than from functional-form assumptions.

Topkis's Chapter 3, §3.2 supplies exactly that theory, as an application of the book's central tool — supermodularity — to the assignment problem. The condition that drives every result in this mission is a single complementarity hypothesis on the firms' profit functions: no concavity, no differentiability, no specific functional form. That a purely order-theoretic hypothesis pins down the qualitative shape of an optimal assignment is the mission's central content, and the platform currently has no lattice-theoretic treatment of matching at all — its one matching result formalizes Gale–Shapley two-sided stable matching by preference, an entirely different mechanism (see Formalization scope below).

Setting

Fix $n$ worker types, indexed $i = 1,\dots,n$, each with a lattice $X_i$ of available worker qualities, and $m$ firms, indexed $j = 1,\dots,m$. A matching assigns to each firm $j$ a vector of qualities $x^j = (x^j_1,\dots,x^j_n) \in \prod_{i=1}^n X_i$ — one worker of each type hired by that firm (a firm that hires no worker of some type, or several, is accommodated by adjoining an artificial "no worker" element to $X_i$, or by splitting a type into several, as Topkis notes on p. 97; the model itself needs neither device). If firm $j$ hires the quality vector $x$, it earns profit $f(x,j) \in \mathbb{R}$; the dependence on $j$ reflects differences among firms such as technology or management efficiency. A matching is optimal if it maximizes the total profit $\sum_{j=1}^m f(x^j,j)$ over every matching.

A matching is increasing if $x^1 \preceq x^2 \preceq \cdots \preceq x^m$ — a single chain, firm by firm, under the pointwise order on $\prod_i X_i$ — and ordered if every two of its firm-assignments are comparable (a weaker, only pairwise, condition). The labor market is loose if each firm's hiring problem can be solved by unconstrained maximization over the whole quality space $\prod_i X_i$, without regard to the other firms' decisions, and tight if the supply of each worker type is exactly $m$, so a feasible matching must assign every available worker to exactly one firm.

The hypothesis common to every result is that $f(x,j)$ is supermodular in the joint variable $(x,j)$ on $\bigl(\prod_i X_i\bigr) \times \{1,\dots,m\}$: for every $(x,j)$ and $(x',j')$, $f(x,j) + f(x',j') \le f(x\vee x', j\vee j') + f(x\wedge x', j\wedge j')$. By Theorem 2.6.1 of Chapter 2, this is equivalent to $f$ having increasing differences both between any two worker types' qualities (complementarity among the worker types) and between each worker type's quality and the firm index (complementarity between quality and firm efficiency).

Formalization targets

Goal — Theorem 3.2.3

$$f \text{ supermodular in } (x,j) \text{ on } \Bigl(\textstyle\prod_{i=1}^n X_i\Bigr)\times\{1,\dots,m\} \ \Longrightarrow\ \exists\, x \text{ increasing and optimal.}$$ $$\text{If, in addition, the labor market is tight, every increasing (tight) matching is optimal.}$$

Existence of an increasing optimal matching, with no loose-market hypothesis — the general case, and the harder of this mission's results to formalize, since its proof is a non-constructive lexicographic-minimization argument rather than a direct reduction to per-firm optimization.

Supporting milestones

• Theorem 3.2.1 (the loose case): under an unconstrained labor market, each firm's set of optimal hiring decisions is increasing in the firm index with respect to the induced set ordering, and an increasing optimal matching exists — proved directly from Chapter 2's monotone-comparative-statics theorems (mission II of this series).
• Theorem 3.2.4: joint supermodularity in $(x,j)$ together with strict supermodularity in $x$ alone, for each fixed $j$, forces every optimal matching to be ordered.
• Theorem 3.2.5: joint strict supermodularity in $(x,j)$ forces every optimal matching to be increasing, the stronger of the two conclusions.

Significance

The result gives a clean, hypothesis-light account of assortative matching: sorting by quality is a structural consequence of complementarity in the profit function, not an artifact of a particular production technology. It generalizes Becker's and Kremer's special cases to arbitrarily many worker types, heterogeneous firms, and any degree of labor-market tightness, identifying supermodularity in $(x,j)$ as the single condition doing all the work. Formalizing it contributes a genuinely new object to the platform: a firm-quality matching model driven by lattice-theoretic complementarity rather than by preference orderings, together with the four distinct comparative-statics conclusions (loose-market optimality, general existence, orderedness, increasingness) that the strength of the supermodularity hypothesis buys. No prior formalized proof of any of these four theorems exists on the platform or, to the author's knowledge, in any other proof assistant library.

Difficulty

The obvious approach — prove the goal (Theorem 3.2.3) by reducing to the loose case, firm by firm, as in Theorem 3.2.1 — does not work, because the loose-market argument crucially uses that each firm's decision does not constrain any other's; without that, a locally optimal per-firm choice need not combine into a globally optimal matching. Topkis's actual proof is non-constructive: among all optimal matchings, pick one that lexicographically minimizes the "latest" failure of the increasing property (a well-ordering argument over the finite but unbounded set of optimal matchings, not an inequality chase), then show that if it still fails to be increasing, exchanging the two offending firms' assignments via $\vee,\wedge$ strictly increases total profit — contradicting optimality by supermodularity. Formalizing this requires setting up the lexicographic minimization (over pairs $(j,i)$ ordered by $j$ then $i$) as a well-founded induction, not merely restating the inequality (3.2.3) at the end of the proof.

Formalization scope

Worker-type quality spaces $X_i$ are modeled as finite, nonempty lattices (Lattice, Fintype, Nonempty); firms are indexed by Fin m. A matching is Fin m → ∀ i, X i with no constraint beyond membership — the general matching problem (3.2.1) imposes no injectivity or supply constraint on its own, a modeling choice Topkis's own text supports (p. 96: the "$\{x^1_i,\dots,x^m_i\}\subseteq X_i$" representation of a matching "may not distinguish between all distinct assignments of workers to firms if the qualities of different workers of any given type are not all distinct, but that ambiguity is inconsequential"). Tightness is instead formalized as an explicit feasibility predicate (a bijection between firms and the $m$ available workers of each type) supplied as a hypothesis exactly where a tight-market theorem needs it, never folded into the general optimality predicate.

A trivializing formalization to avoid: collapsing Theorem 3.2.4's "ordered" conclusion and Theorem 3.2.5's "increasing" conclusion into the same statement, or conflating their two distinct supermodularity hypotheses (joint-non-strict-plus-per-firm-strict versus jointly strict) — the mission's four milestones are kept as four genuinely different claims with their own hypotheses, not variations proved once and restated. AGT.stable_matching_exists (Gale–Shapley) is not reused here, despite the shared word "matching": it produces a two-sided, preference-based stable matching with no notion of aggregate profit, a mechanism unrelated to this mission's profit-maximizing, supermodularity-driven assignment.

Reused from earlier missions in this series: the induced set ordering InducedSetOrder (mission I) and joint supermodularity SupermodularOn (mission II), both published platform definitions. Contributions most welcome on the goal theorem's lexicographic-minimization argument, the mission's hardest step.

Selected references

• G. S. Becker, A Theory of Marriage: Part I, Journal of Political Economy 81 (1973), 813–846. https://doi.org/10.1086/260084
• M. Kremer, The O-Ring Theory of Economic Development, Quarterly Journal of Economics 108 (1993), 551–575. https://doi.org/10.2307/2118400
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011 (orig. 1998). https://doi.org/10.1515/9781400822539

Motivation

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

Setting

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

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

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

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

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

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

Formalization targets

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

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

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Two-stage stochastic programs with recourse are already hard to optimize when the recourse problem is a linear program: Chapters 4–6 of this series show how the L-shaped method exploits the recourse function's convexity and polyhedrality to converge finitely by cutting planes. Adding integrality restrictions destroys both properties. Birge and Louveaux open Chapter 7 by naming the consequence directly: "properties of stochastic integer programs are scarce," duality is lost, and the recourse value $Q(x)$ for even a single first-stage point $x$ may itself require solving an integer program from scratch, with no warm start available across scenarios (Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 290).

Section 7.2 isolates the one structural feature that still buys finite convergence: first-stage variables restricted to $\{0,1\}$. Laporte and Louveaux's Integer L-shaped method (1993) exploits this by combining a branch-and-bound search over the finitely many binary first-stage points with a new family of optimality cuts, valid wherever a finite lower bound on the recourse value is available. This mission formalizes that method's specification and its finite-convergence guarantee, together with the two propositions its proof rests on.

Setting

A stochastic integer program (SIP) extends a two-stage stochastic linear program with fixed recourse (Chapter 3's Recourse.Instance: first-stage data $A, b, c$, fixed recourse matrix $W$, and $K$ scenarios of $(q_k, h_k, T_k)$ with probabilities $p_k$) by two further restrictions:

$$(\mathrm{SIP}) \quad \min_{x \in X} c^{\mathsf T}x + \mathbb E_\xi \min_y \{ q(\omega)^{\mathsf T} y \mid W(\omega)y = h(\omega) - T(\omega)x,\ y \in Y\} \quad \text{s.t. } Ax = b,$$

where $X$ restricts the first stage and $Y$ restricts the recourse variable — typically requiring integrality of $y$. Section 7.2's standing hypothesis narrows $X$ further: every coordinate of $x$ is binary. Write $Q(x)$ for the resulting recourse value (a possibly-infinite expectation, by the same convention as the continuous case) and $C(x)$ for the value of the continuous relaxation, obtained by dropping the restriction $Y$ and keeping only $y \ge 0$ — exactly the recourse value Chapter 3's Recourse.Instance already computes.

The method needs one further hypothesis, Assumption 2: a finite lower bound $L$ with $L \le \min_x \{Q(x) \mid Ax=b,\ x \in X\}$, not required to be tight. For a subset $S$ of the first-stage index set, write $\delta(x,S) = \sum_{i \in S} x_i - \sum_{i \notin S} x_i$, and let $\mathrm{indicator}(S)$ be the binary point with $x_i = 1$ for $i \in S$, $x_i = 0$ otherwise — $\delta(x,S)$ measures how far a binary point $x$ is from matching $S$ exactly, reaching its maximum $|S|$ only at $x = \mathrm{indicator}(S)$.

Formalization targets

Proposition 1 (continuous cuts survive integrality)

$$e - E^{\mathsf T}x \le C(x) \implies e - E^{\mathsf T}x \le Q(x)$$

Any L-shaped optimality cut valid for the continuous relaxation's value remains valid for the true, integrality-restricted recourse value, since $C(x) \le Q(x)$ pointwise.

Proposition 3 (a cut from one binary feasible solution)

$$\theta \ge (q_S - L)\Bigl(\sum_{i \in S} x_i - \sum_{i \notin S} x_i\Bigr) - (q_S-L)(|S|-1) + L$$

is a valid lower bound on $Q(x)$ for every binary first-stage-feasible $x$, given a binary feasible point $\mathrm{indicator}(S)$ with true recourse value $q_S$ and a lower bound $L$ satisfying Assumption 2.

Proposition 4 — the mission's goal

Under Assumption 2, the Integer L-shaped method — the branch-and-bound search over binary first-stage points, tightened at each iteration by a fresh cut of the Proposition 3 form — finitely converges to an optimal solution of an SIP with relatively complete recourse and binary first-stage variables, when one exists. "Finitely" is quantified explicitly: a bound of $2^{n_1}$ on the number of iterations, the number of distinct binary first-stage points.

Significance

Proposition 4 is the chapter's payoff: it turns "solve an SIP with binary first-stage variables" from an open-ended search into a procedure with a certified stopping point, at the cost of one additional hypothesis (a computable lower bound $L$) that is often easy to obtain by relaxing the second-stage integrality restriction, as the book's Example 1 illustrates directly. Propositions 1 and 3 are the two soundness facts the method's cuts rest on: Proposition 1 lets an implementation reuse the continuous L-shaped method's own optimality cuts as valid (if weaker) constraints, and Proposition 3 supplies the chapter's genuinely new cut, tailored to the binary structure and strong enough by itself to guarantee termination.

Formalizing this mission fixes, machine-checkably, the exact hypotheses under which the method is correct — in particular, that "binary" is load-bearing (the finiteness bound is literally $2^{n_1}$) and that "relatively complete recourse" cannot be dropped, since it is what keeps the recourse value from becoming $+\infty$ at a feasible point. No result here has, to the mission's knowledge, been formalized elsewhere; the propositions and the method's specification are drafted fresh.

Difficulty

The recourse function $Q$ is neither convex nor polyhedral once $y$ is integer-restricted, so the argument cannot follow the continuous L-shaped method's proof line for line — that proof leans on $Q$'s convexity to certify a cut from finitely many bases. Proposition 3's cut instead argues purely combinatorially: $\delta(x,S) \le |S|$ for every binary $x$, with equality forcing $x = \mathrm{indicator}(S)$, so the cut's right-hand side collapses to the true value $q_S$ exactly there and falls to at most $L$ everywhere else — a fact about the finitely many binary points of $\{0,1\}^{n_1}$, not about $Q$'s analytic structure. The natural first idea, adapting a continuous L-shaped cut by simply restricting its domain to binary $x$, fails: nothing forces such a cut to be tight at the current iterate, so it need not exclude a revisited point, and finite convergence (the content Proposition 4 actually asserts, not just "an optimum exists") would be lost.

Formalization scope

The mission represents first-stage points as Fin n1 → ℝ with a Binary predicate (∀ i, x i = 0 ∨ x i = 1) rather than a Fin n1 → Bool type, so that the master problem's feasible region and its binary-restricted subset share one ambient space, matching how the book moves between $X$ and its binary points. The second-stage restriction $Y$ is left an arbitrary Set (Fin n2 → ℝ); taking it to be all of $\mathbb R^{n2}$ recovers exactly Chapter 3's continuous recourse value, without a second definition. Flagged (moderator review, 2026-09-19): Proposition 1's own $C(x)$ is the book's $\overline Y$-based continuous/LP-relaxation of $Y$ (Eq. (1.3)-(1.4)), which can retain bounds $Y$ imposes beyond integrality — the book's own worked example on the same page gives binary $Y=\{0,1\}^{m_2}$, so $\overline Y=[0,e]$, not $y\ge0$ alone. This mission's prop1_cuts_valid_for_sip uses the dropped-$Y$ relaxation (only $y \ge 0$) rather than $\overline Y$, which coincides with the book's $C(x)$ only when $Y$ is itself an unbounded integrality restriction; the theorem is a narrower result than the book's Proposition 1 whenever $Y$ carries additional structure, though it remains true as stated because the dropped-$Y$ value is unconditionally $\le$ the book's $\overline Y$-based $C(x)$, which is itself $\le Q(x)$ — see the item's own Formalization Note for the full argument. The existential lower bound $L$ of Assumption 2 is kept a bare existentially-quantified real, never sharpened to a formula, matching the book's own "no requirement is made that the bound $L$ should be tight."

The Integer L-shaped method's branch-and-bound bookkeeping (Steps 0, 1, 3, 4: pendant-node list management, bound-based fathoming, and branching on a violated integrality restriction) is abstracted into a direct optimization over the binary first-stage feasible set at each iteration, since Proposition 3's cut is proved valid there without appeal to any specific branching order — the same level of abstraction the Chapter 5 mission uses for the continuous L-shaped method's own master-problem bookkeeping. What is retained explicitly is the part the finiteness bound actually depends on: Step 5's recourse-value computation and Step 6's binary choice between fathoming and adding a fresh cut, modeled as a state machine whose state is the finite set of binary points already excluded by a cut. A formalization that dropped this state machine — asserting only "if Assumption 2 and relatively complete recourse hold, an optimal solution exists" — would trivialize the proposition's actual content, the finite bound on the number of steps; this mission keeps that bound as an explicit, checkable part of the goal statement.

Definitions reused from earlier missions in this series: StochasticProg.Recourse.Instance (Chapter 3) for the underlying two-stage recourse data and its continuous-relaxation value. Contributions welcome on strengthening Proposition 4's proof to also derive Proposition 3 as a lemma, and on formalizing the improved cuts of Propositions 5–7 (out of scope here, left for a possible follow-up mission).

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer 2011, Chapter 7, §7.2. DOI: 10.1007/978-1-4614-0237-4
• G. Laporte and F. Louveaux, "The integer L-shaped method for stochastic integer programs with complete recourse," Operations Research Letters 13(3), 1993, 133–142.

Motivation

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

Setting

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

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

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

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

Formalization targets

Goal (Chapter 6, Theorem 1)

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal — the drift inequality behind Theorem 8.2

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

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

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

Supporting levels

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

Significance

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

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

Difficulty

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

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

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

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

Formalization scope

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

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

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

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

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

Selected references

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

Motivation

When a file is transferred over the Internet, no part of the network decides how fast it should go. The machines inside the network forward packets; when a resource is heavily loaded it drops or marks one; the destination reports that to the source; and the source slows down, then gradually speeds up again until the next signal. This end-to-end cycle of increase and decrease is TCP, and it is the mechanism by which the Internet discovers available capacity and divides it among competing flows.

Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such a scheme converges to. The answer is the chapter's organizing idea: the decentralized dynamics solve a global optimization problem that no participant can see. Each source knows only its own rate and the congestion signals it receives; no machine anywhere holds the link-route incidence matrix; and yet the flow rates converge to the unique maximizer of a concave network utility, and that maximizer is the proportionally fair allocation. This is the same phenomenon as the electrical network of Chapter 4, now with the local rule chosen so that the global objective is the one we want.

Setting

A network has $J$ resources and $R$ routes, with link-route incidence matrix $A$: $A_{jr}=1$ when route $r$ uses resource $j$. Route $r$ carries a time-varying flow rate $x_r(t)>0$, and the load on resource $j$ is $\sum_{s:j\in s}x_s(t)$.

Each resource $j$ generates congestion signals at rate

$$\mu_j(t)=p_j\Bigl(\sum_{s:j\in s}x_s(t)\Bigr),$$

where $p_j$ is non-negative, continuous, increasing and not identically zero — one may read $p_j(y)$ as the probability that a packet is dropped or marked at resource $j$ under load $y$. The primal algorithm is the response of the sources:

$$\frac{d}{dt}x_r(t)=\kappa_r\Bigl(w_r-x_r(t)\sum_{j\in r}\mu_j(t)\Bigr), \qquad r\in\mathcal{R}, \tag{7.5}$$

with $w_r,\kappa_r>0$: a steady increase proportional to the weight $w_r$, and a decrease proportional to the stream of congestion signals received. Both sums are local — over the resources on route $r$, and over the routes through resource $j$ — so nothing in the network needs to know $A$.

The network problem $\mathrm{network}(A,C;w)$ of section 7.1 is to maximize $\sum_r w_r\log x_r$ over $x\ge0$ with $Ax\le C$, and a feasible $x$ is weighted proportionally fair when every feasible $y$ satisfies $\sum_r w_r (y_r-x_r)/x_r\le0$.

Formalization targets

Goal — Theorem 7.6, global stability of the primal algorithm

$$U(x)=\sum_{r}w_r\log x_r-\sum_{j}\int_0^{\sum_{s:j\in s}x_s}p_j(y)\,dy$$

is a Lyapunov function for (7.5): the unique maximizer $\bar x$ of $U$ over the positive orthant is an equilibrium point, and every trajectory of the primal algorithm converges to it.

The goal asserts both halves of the book's last sentence: that $\bar x$ maximizes $U$, and that the trajectory converges to it. It fixes no rate of convergence and no basin restriction beyond starting in the interior, which is what "global" means here.

Supporting levels

Proposition 7.4, that solving $\mathrm{network}(A,C;w)$ and being weighted proportionally fair are the same condition; strict concavity of $U$ on the positive orthant; the partial derivative $\partial U/\partial x_r=w_r/x_r-\sum_{j\in r}p_j(\cdot)$ that identifies the maximizer; the equivalence between a stationary point of $U$ and an equilibrium of (7.5); and the Lyapunov identity (7.7),

$$\frac{d}{dt}U(x(t))=\sum_r\frac{\kappa_r}{x_r(t)}\Bigl(w_r-x_r(t)\sum_{j\in r}p_j(\cdot)\Bigr)^2\ \ge 0 .$$

Significance

The result itself. Theorem 7.6 is the statement that a decentralized rule solves a centralized problem. Its practical content is that the choice of $p_j$ and $w_r$ determines what is optimized, so a protocol designer who wants a particular notion of fairness can get it by choosing the local rule accordingly — the $\alpha$-fair family of Chapter 8 is exactly this dial. Its theoretical content is the identification of the limit: because $U$'s first term is $\sum_r w_r\log x_r$, the limit is the weighted proportionally fair allocation, which by Proposition 7.4 is the solution of the network problem and, by Remark 7.5, also the Nash bargaining solution and a market-clearing equilibrium. Three quite different notions of "the right allocation" coincide, and a simple end-to-end feedback rule finds it.

Formalizing it. Nothing here is open; the model and the theorem are from Kelly, Maulloo and Tan (1998). What the mission produces is a machine-checked congestion-control model — the network problem, proportional fairness, the primal dynamics and the Lyapunov function — and a statement of the convergence result in a form later work can cite. Mathlib has no network utility maximization and no congestion control.

Difficulty

The Lyapunov identity is a chain-rule computation and is not the hard part, and neither is $\frac{d}{dt}U\ge0$. The gap the book flags explicitly is between "$U$ increases along trajectories" and "$x(t)\to\bar x$": a strictly increasing Lyapunov function does not by itself force convergence, because the derivative could decay fast enough for the system to stall short of the maximum. The book closes it with a compactness argument — the trajectory is trapped in $\{x: U(x)\ge U(x(0))\}$, which is compact, and on the complement of an $\epsilon$-ball around $\bar x$ within that set the derivative (7.7) is continuous and therefore bounded away from zero, so only finite time can be spent there. Reproducing that argument is the substance of the goal, and it needs the compactness of the sublevel set, which comes from strict concavity and the growth of $-\int_0^{y}p_j$.

A second difficulty is one of representation rather than mathematics. The primal algorithm is an ODE, and a formal statement must say what a trajectory is. Here a trajectory is given as a differentiable function satisfying (7.5) pointwise, with positivity assumed rather than derived; deriving positivity from the dynamics is a separate (true, and welcome) result.

Formalization scope

Resources and routes are indexed by finite types and the incidence matrix is real-valued with entries constrained to $0$ or $1$, matching the book and the convention of mission IV of this series, whose linkFlow is reused here. Flow vectors live in the positive orthant, stated as ∀ r, 0 < x r: the utility contains $\log x_r$, which has no meaning at $x_r=0$, and the book's own maximum is interior to the positive orthant.

The network problem's objective is maximized over the intersection of the feasible set with the positive orthant rather than over $x\ge0$, since $\log 0$ is not a real number; the fairness condition, by contrast, is quantified over all feasible $y$ including boundary points, exactly as the book states it, and the inequality $\sum_r w_r(y_r-x_r)/x_r\le0$ is meaningful there.

A trajectory is a function of real time satisfying the derivative condition at each $t\ge0$, and staying in the positive orthant is a hypothesis. The equilibrium $\bar x$ is given by its stationarity condition $w_r=\bar x_r\sum_{j\in r}p_j(\cdot)$ rather than by an existence claim, so the goal is about the trajectory rather than about solving the fixed-point equation; that the stationary point is the maximizer is the first conjunct of the conclusion, so nothing is assumed about it that is not also proved.

The goal cannot be satisfied vacuously: the hypotheses are jointly satisfiable — for instance one resource, one route, $p(y)=y$, $w=\kappa=1$, $\bar x=1$ — and the conclusion is a genuine limit.

Contributions welcome beyond the listed items: that the positive orthant is invariant under (7.5); uniqueness and existence of the max-min fair allocation; Theorem 7.2 on problem decomposition into user and network problems; Theorem 7.8, the corresponding global stability result for the TCP-like system of section 7.4; and the dual algorithm of section 7.6.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 7 (pp. 151–185); Proposition 7.4, Theorem 7.6, equations (7.4)–(7.7). DOI 10.1017/cbo9781139565363
• F. P. Kelly, A. K. Maulloo and D. K. H. Tan, Rate control for communication networks: shadow prices, proportional fairness and stability, Journal of the Operational Research Society 49 (1998), 237–252. DOI 10.1057/palgrave.jors.2600523
• F. P. Kelly, Charging and rate control for elastic traffic, European Transactions on Telecommunications 8 (1997), 33–37. DOI 10.1002/ett.4460080106
• J. F. Nash, The bargaining problem, Econometrica 18 (1950), 155–162. DOI 10.2307/1907266
• S. H. Low and D. E. Lapsley, Optimization flow control I: basic algorithm and convergence, IEEE/ACM Transactions on Networking 7 (1999), 861–874. DOI 10.1109/90.811451