Operations Research

Motivation

Exact methods for the resource-constrained project scheduling problem — branch-and-bound over activity lists or over start-time assignments, and the lower-bound computations inside them — live or die by how much of the search space can be discarded before it is enumerated. The standard tool is constraint propagation: deducing, from the precedence, resource and time-window data, new precedence relations $i\to j$ that every feasible schedule must satisfy, and tighter time windows for the activities. Brucker and Knust's Section 3.6 (doi:10.1007/978-3-642-23929-8) presents the family of interval consistency tests — input, output, input-or-output and their negations — that constraint-programming schedulers apply at every node of the search, following Carlier and Pinson (An algorithm for solving the job-shop problem, Management Science 35, 1989, doi:10.1287/mnsc.35.2.164) and Baptiste, Le Pape and Nuijten (Constraint-Based Scheduling, Kluwer, 2001, doi:10.1007/978-1-4615-1479-4). Every test is an instance of one theorem, Theorem 3.7, and its cumulative-resource analogue, Theorem 3.8. Those two theorems, and the tests as their corollaries, are this mission.

Setting

The instance is the RCPSP of mission I: activities $0,\dots,n-1$ with integer processing times $p_i$, renewable resources $k$ with capacities $R_k$ and demands $r_{ik}$, and precedence arcs; a schedule is an integer start-time vector $S$, feasible when it meets the precedences and never exceeds a capacity. Section 3.6 adds three things.

Relations. A conjunction $i\to j$ holds in $S$ when $S_i+p_i\le S_j$. Two activities are parallel, $i\parallel j$, when they overlap for at least one time unit, and a disjunction $i-j$ is the negation of that: $i\to j$ or $j\to i$. The instance carries a set $C$ of conjunctions and a set $D$ of disjunctions that every feasible schedule must satisfy; initially $C_0$ is the precedence relation and $D_0$ the pairs whose combined demand exceeds some capacity, and propagation adds to them.

Disjunctive sets. A set $I$ of at least two activities is disjunctive when any two of its members are related by a disjunction or a conjunction, so no two are ever processed together: the activities of a unit-capacity resource, the jobs of a single machine, the operations of one job in a shop. Its total processing time is $P(I)=\sum_{i\in I}p_i$.

Time windows. Each activity has a head $r_i$ and a deadline $d_i$, and a feasible schedule has $r_i\le S_i$ and $S_i+p_i\le d_i$. An activity starts first in a set $J$ when no activity of $J$ starts earlier, and ends last when none completes later.

For a cumulative resource $k$ the work of activity $i$ is $w_i=r_{ik}p_i$ and $W(J)=\sum_{i\in J}w_i$.

Formalization targets

Goal — Theorem 3.7 (printed p. 169)

Let $I$ be a disjunctive set, $J\subseteq I$, and $J',J''$ proper subsets of $J$ with $J'\cup J''\ne\emptyset$. If

$$\max_{\substack{\nu\in J\setminus J',\ \mu\in J\setminus J''\\ \nu\ne\mu}}\bigl(d_\mu-r_\nu\bigr)<P(J),$$

then in every feasible schedule an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

The first infeasibility test (printed p. 169)

If some nonempty $J\subseteq I$ has $\max_{\mu\in J}d_\mu-\min_{\nu\in J}r_\nu<P(J)$, no feasible schedule exists.

The input test (3.123) and the output test (3.124) (printed p. 171)

For $\Omega\subseteq I$ nonempty and $i\in I\setminus\Omega$: if $\max_{\mu\in\Omega\cup\{i\}}d_\mu-\min_{\nu\in\Omega}r_\nu<P(\Omega)+p_i$ then $i\to j$ for all $j\in\Omega$; symmetrically, if $\max_{\mu\in\Omega}d_\mu-\min_{\nu\in\Omega\cup\{i\}}r_\nu<P(\Omega)+p_i$ then $j\to i$ for all $j\in\Omega$.

The input-or-output test (printed p. 170)

For $i,j\in J\subseteq I$, $|J|\ge 2$: if $\max_{\mu\in J\setminus\{j\}}d_\mu-\min_{\nu\in J\setminus\{i\}}r_\nu<P(J)$ then $i$ starts first in $J$ or $j$ ends last in $J$, and $i\to j$ when $i\ne j$.

Theorem 3.8 (printed p. 186)

For a cumulative resource $k$, $J\subseteq I_k$ and proper subsets $J',J''$ of $J$: if $R_k\bigl(\max_{\mu\in J\setminus J''}d_\mu-\min_{\nu\in J\setminus J'}r_\nu\bigr)<W(J)$ then an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

Significance

Theorem 3.7 is the single statement behind a whole toolbox. Every interval consistency test in the literature — the input and output tests that fix a new conjunction, the input-or-output test, the negation tests that only shrink a window — is the theorem with a particular choice of $J'$ and $J''$, and the book's Section 3.6.4 derives them one by one. A propagation engine that applies these tests to a fixpoint is what makes branch-and-bound for the job shop and the RCPSP practical; Carlier and Pinson's solution of the 10×10 job-shop instance is the historical demonstration. Theorem 3.8 extends the same reasoning from disjunctive to cumulative resources by replacing "no overlap" with "at most $R_k$ units per time unit", the energetic-reasoning viewpoint that the rest of Section 3.6.5 develops.

The results are elementary and proved; formalizing them fixes, once, what "feasible" means in the presence of the relation sets $C$ and $D$ and time windows, on top of the RCPSP model of mission I. That layer is reusable: the start-start distance matrix of Section 3.6.2 and the symmetric-triple rules of Section 3.6.3 are statements about the same schedules and the same relations. Nothing here is on the platform or in Mathlib.

Difficulty

The obvious argument for Theorem 3.7 is the correct one, and its difficulty is in the bookkeeping. If no activity of $J'$ starts first and none of $J''$ ends last, the first starter is some $\nu\in J\setminus J'$ and the last finisher some $\mu\in J\setminus J''$, and every activity of $J$ is processed inside $[S_\nu,\,S_\mu+p_\mu]\subseteq[r_\nu,d_\mu]$. Since the activities of a disjunctive set are pairwise non-overlapping, their total length $P(J)$ fits in that interval, contradicting (3.121). The formal work is the packing lemma: pairwise disjoint integer intervals inside an interval of length $L$ have total length at most $L$, which requires ordering the activities by start time and an induction that Mathlib does not supply.

The subtle point is the restriction $\nu\ne\mu$ in (3.121). The book allows it because "an activity which starts first cannot complete also last" when there are at least two activities with positive durations. The formal statement reads "starts first" and "ends last" with $\le$, which makes the theorem true without a positivity hypothesis: when the restriction empties the index set, $J\setminus J'=J\setminus J''=\{x\}$, the conclusion holds because $x$ cannot be both the unique first starter and the unique last finisher of a disjunctive set with two or more members. A solver should expect to handle that corner separately.

For the tests the extra step is turning "starts first" into a conjunction $i\to j$, which uses the disjunction between $i$ and $j$ together with positive processing times: with $p_j=0$ an activity could start at the same instant as $i$ without violating the disjunction, so the tests carry the positivity hypothesis that Theorem 3.7 itself does not need. Theorem 3.8 replaces the packing lemma by a work-counting lemma: over an interval of length $L$ a resource of capacity $R_k$ supplies at most $R_kL$ units, and every activity of $J$ consumes $r_{ik}p_i$ of them.

Formalization scope

Schedules are integer start-time vectors on Fin n, as in missions I and II, and a feasible schedule of this mission is one that is FeasibleSchedule for the RCPSP instance (mission I), respects the arcs of $C$ (RespectsArcs, mission II), satisfies the disjunctions of $D$ and lies within the time windows; these four hypotheses are the book's "feasible schedule" in Section 3.6 and are carried on every statement, although the arguments use only the last two, or, for Theorem 3.8, the resource constraint and the windows. The sets $C$ and $D$ are parameters, not derived from the instance, since propagation enlarges them.

Every inequality "$\max(\cdot)-\min(\cdot)<P$" is stated as the family of inequalities $d_\mu<r_\nu+P$ over the same index pairs. This is equivalent, avoids natural-number subtraction, and gives an empty index set the value the convention $\max\emptyset=-\infty$ would: the hypothesis is then vacuous. "Starts first" and "ends last" use $\le$. Proper-subset hypotheses $J'\subset J$, $J''\subset J$ are the book's; the first infeasibility test needs $J$ nonempty, and the input-or-output test needs $|J|\ge 2$.

A trivializing reading is ruled out on the disjunctive side by the nonemptiness hypotheses (an empty $J$ would make the infeasibility test's family vacuous and its conclusion false) and on the cumulative side by the observation that Theorem 3.8 with $J'=J''=\emptyset$ asserts infeasibility, which is the book's intended reading. Welcome contributions beyond the milestones: the input-negation and output-negation tests, the window-tightening rules of Section 3.6.4, and the SSD-matrix results of Section 3.6.2.

Selected references

• Peter Brucker and Sigrid Knust, Complex Scheduling, 2nd ed., Springer, 2012, Section 3.6. doi:10.1007/978-3-642-23929-8
• Jacques Carlier and Eric Pinson, An algorithm for solving the job-shop problem, Management Science 35 (1989). doi:10.1287/mnsc.35.2.164
• Philippe Baptiste, Claude Le Pape and Wim Nuijten, Constraint-Based Scheduling, Kluwer, 2001. doi:10.1007/978-1-4615-1479-4
• Ulrich Dorndorf, Erwin Pesch and Toàn Phan-Huy, Constraint propagation techniques for the disjunctive scheduling problem, Artificial Intelligence 122 (2000). doi:10.1016/S0004-3702(00)00040-0

Motivation

When several processors share a workload, the first question is how long the workload takes if it is spread out as well as possible. If a job may be interrupted and resumed later, possibly on another processor — preemption, the setting of operating systems, of communication links and of any resource that can be time-shared — the answer is a closed formula, and it is one of the oldest results in scheduling: McNaughton's wrap-around rule of 1959 (Scheduling with deadlines and loss functions, Management Science 6, doi:10.1287/mnsc.6.1.1) shows that on identical machines the optimal makespan is the larger of the longest job and the average load. Horvath, Lam and Sethi (A level algorithm for preemptive scheduling, Journal of the ACM 24, 1977, doi:10.1145/321992.321995) extended this to machines of different speeds, and Gonzalez and Sahni (Preemptive scheduling of uniform processor systems, Journal of the ACM 25, 1978, doi:10.1145/322047.322055) gave the fast algorithm with few preemptions. Brucker's Chapter 5 (doi:10.1007/978-3-540-69516-5) presents the level-algorithm version, and this mission formalizes the statements it proves about schedules.

Setting

There are $n$ jobs with processing requirements $p_1,\dots,p_n>0$ and $m$ uniform machines with speeds $s_1,\dots,s_m>0$: running job $i$ on machine $j$ for a period of length $\ell$ performs $s_j\ell$ units of its requirement, so the whole job would take $p_i/s_j$ time units there. Identical machines are the case $s_1=\dots=s_m=1$.

A preemptive schedule is a finite list of pieces, each a job, a machine, a start time and a stop time. It is feasible for the data $(s,p)$ when every piece lies in $[0,\infty)$, no two pieces on the same machine overlap, no two pieces of the same job overlap (a job is on at most one machine at any instant), and every job $i$ receives total work exactly $p_i$ over its pieces. Its makespan $C_{\max}$ is the largest stop time; the completion time $C_i$ of job $i$ is the largest stop time of one of its pieces. A schedule is nonpreemptive when every job consists of a single piece.

Following Section 5.1.2 the data are sorted, $p_1\ge\dots\ge p_n$ and $s_1\ge\dots\ge s_m$, with $n\ge m$, and one writes $P_j=\sum_{i\le j}p_i$, $S_j=\sum_{i\le j}s_i$. For a set $A$ of jobs, $h(A)=S_{|A|}$ if $|A|\le m$ and $h(A)=S_m$ otherwise: the largest combined speed that $|A|$ jobs can use at one instant.

Formalization targets

Goal — Theorem 5.8 (printed p. 127)

The optimal makespan of $Q\mid pmtn\mid C_{\max}$ is the bound (5.5):

$$w \;=\; \max\Bigl\{\max_{j=1}^{m-1}\frac{P_j}{S_j},\ \frac{P_n}{S_m}\Bigr\} ,$$

in the sense that some feasible preemptive schedule has makespan exactly $w$ and no feasible preemptive schedule has a smaller makespan.

The lower bound (5.5) (printed p. 125)

Every feasible preemptive schedule has makespan at least $w$.

$P\mid pmtn\mid C_{\max}$ (printed p. 108)

On identical machines, $LB=\max\{\max_i p_i,\ \tfrac1m\sum_i p_i\}$ is a lower bound on the makespan and is attained by some feasible preemptive schedule.

Condition (5.8) (printed p. 129)

The jobs can be scheduled preemptively within $[0,T]$ if and only if $\sum_{i\in A}p_i\le T\,h(A)$ for every set $A$ of jobs.

Theorem 5.7 (printed p. 121)

For $P\mid pmtn\mid\sum w_iC_i$ with nonnegative weights there is an optimal schedule without preemption.

Significance

Theorem 5.8 turns an optimization over an infinite family of schedules into a formula in the data, and the formula is tight in both directions: each of its terms is a resource bound that some schedule meets exactly. That is what makes preemptive makespan minimization one of the few parallel-machine problems that is solvable at all — its nonpreemptive counterpart $P2\parallel C_{\max}$ is NP-hard (p. 124) — and it is why the preemptive relaxation appears as a bound inside branch-and-bound methods for the nonpreemptive problems.

Condition (5.8) is the form in which the result is reused. It is a Hall-type condition, one inequality per set of jobs, and it is exactly what Section 5.1.2 needs to prove Theorem 5.9, which decides $Q\mid pmtn; r_i\mid L_{\max}$ by a maximum flow in an expanded network. Theorem 5.7 is the complementary statement for the other classical objective: for total weighted completion time preemption buys nothing, so the nonpreemptive solutions of Section 5.1.1 are optimal in the larger class too.

On status: every statement here is classical and proved, and the formalization adds a checked model of preemptive schedules. Mathlib has no scheduling material, and the platform's SchedulingAlgorithms series so far models only single-machine sequences (missions I, II, IV) and two-machine permutation flow shops (mission III), none of which allow a job to be split. The piece-list model of this mission is the first reusable object for preemptive and parallel-machine problems, and the later sections of Chapter 5 — $Q\mid pmtn; r_i\mid L_{\max}$, $P\mid pmtn\mid L_{\max}$ — are stated in it.

Difficulty

The obvious first idea for the goal is to run McNaughton's rule with the speeds ignored. It fails on uniform machines: filling machines one after another does not respect the constraint that a long job on a slow machine is not done when a short job on a fast one is. The correct idea is the level algorithm — always process the jobs of highest remaining requirement on the fastest free machines, sharing machines among tied jobs — and the difficulty is in the analysis rather than the idea. The proof of Theorem 5.8 has to show that the schedule it produces ends exactly at one of the terms of $w$: either no machine idles before the end, giving $P_n/S_m$, or the machines finish in speed order with the first $j$ jobs busy from time $0$, giving $P_j/S_j$. Making that case analysis rigorous requires tracking that the order of remaining requirements is preserved over time (the invariant (5.6)) and that ties are broken consistently.

A second, formal difficulty is that the level algorithm's output is defined by continuous-time events (the next completion, the next time two levels coincide), so producing an explicit finite list of pieces with the required properties is itself a construction. Any proof must build a concrete schedule; "the infimum of makespans equals $w$" is not the goal.

For the lower bound the trap is the opposite: it is tempting to argue only with total capacity $S_mT$, which gives $P_n/S_m$ but not $P_j/S_j$. The latter needs the rule that a job is on at most one machine at a time, so that $j$ jobs run at combined speed at most $S_j$; a model that let a job be split across machines simultaneously would make the theorem false, and the definition of feasibility rules it out explicitly.

Formalization scope

A schedule is a List of Pieces over jobs Fin n and machines Fin m, with real start and stop times. Feasibility is the three-part condition of the Setting, disjointness of two pieces meaning one stops no later than the other starts. Work is measured with the machine's speed, so the same definitions cover identical machines as the constant speed $1$. Pieces of length zero and unsorted lists are allowed; both are harmless.

The sorted orders are hypotheses Antitone p and Antitone s, the speeds and requirements are positive, $m\ge 1$ and, where the book assumes it, $n\ge m$. The book's normalization $s_1=1$ is not assumed: every statement here is invariant under scaling all speeds, and the book uses the normalization only for a running-time estimate. The bound $w$ is defined as the maximum of an explicit nonempty finite set, so no supremum of an empty or unbounded set occurs; $LB$ takes a proof that $n\ge 1$ so that $\max_i p_i$ is meaningful.

Two things are deliberately not stated. The level algorithm itself is not transcribed: Theorem 5.8 is stated as the existence of an optimal schedule of makespan $w$, which is what its proof establishes. And Theorem 5.9, the flow characterization for $Q\mid pmtn; r_i\mid L_{\max}$, is left for a later mission, since it needs release times and the expanded network on top of this model.

A trivializing reading is excluded by the existential form of the goal and of Theorem 5.7: each asserts that an optimal schedule exists, not merely that any optimal schedule has a property. A proof of the goal has to construct a schedule; a proof of Theorem 5.7 has to construct a nonpreemptive one that beats every preemptive competitor. Contributions welcome beyond the milestones: a general lemma that a feasible schedule can be normalized to sorted, positive-length pieces, and a proof that (5.8) for the sets $\{1,\dots,j\}$ is equivalent to $w\le T$.

Selected references

• Peter Brucker, Scheduling Algorithms, 5th ed., Springer, 2007, Chapter 5. doi:10.1007/978-3-540-69516-5
• Robert McNaughton, Scheduling with deadlines and loss functions, Management Science 6 (1959). doi:10.1287/mnsc.6.1.1
• E. C. Horvath, S. Lam and R. Sethi, A level algorithm for preemptive scheduling, Journal of the ACM 24 (1977). doi:10.1145/321992.321995
• Teofilo Gonzalez and Sartaj Sahni, Preemptive scheduling of uniform processor systems, Journal of the ACM 25 (1978). doi:10.1145/322047.322055

Motivation

Chapter 4's framework (formalized in this series' 04-framework mission) solves the online covering-packing pair only in the restricted setting a(i,j) ∈ {0,1}, b(j) = 1 — every constraint is an unweighted "cover me with at least one of these" condition. Chapter 14 delivers the promise made at the very start of the survey (p. 115: "we show how to extend the ideas we present here to handle general (non-negative) values of a(i,j) and b(j)"): fully general non-negative coefficients, normalized so every constraint reads ∑_i a(i,j)x(i) ≥ 1. This mission formalizes both halves of that generalization — the packing scheme (Theorem 14.1, with a matching lower bound, Lemma 14.2, showing an extra additive term is unavoidable) and the covering scheme (Theorem 14.3, the goal).

Setting

Fix a finite set I of primal (covering) variables with positive costs c(i), and a finite set J of dual (packing) variables/covering constraints, with a(i,j) ≥ 0 for every pair (Fig. 14.1). The packing scheme (Section 14.1) is parameterized by a target competitive ratio B > 0: on each new dual variable y(j) and its coefficients a(i,j), the algorithm increases y(j) continuously and each x(i) by an explicit exponential increment function until the new primal constraint is satisfied, achieving B-competitiveness for the packing objective at the cost of an additive O(log(a_i(max)/a_i(min))) term (beyond the multiplicative O(log n)) in how much each dual constraint can be violated — qualitatively different from Chapter 4's purely multiplicative O(log d) bound, and Lemma 14.2 proves this additive term cannot be removed. The covering scheme (Section 14.2) instead works in phases: each phase assumes a doubling lower bound α(r) on OPT and "forgets" its primal/dual variables once the primal cost exceeds α(r), restarting with α(r+1) = 2α(r) — a structurally different mechanism from Chapter 4's direct algorithms, needed because with general coefficients a single monotone run can no longer be analyzed via one potential function alone.

Formalization targets

Theorem 14.3 (the goal, p. 253): for any B > 0, the phase-based covering scheme (each constraint normalized to ∑_i a(i,j)x(i) ≥ 1/B) is competitive with an explicit ratio 8 log(2n)/B, taken directly from the proof's own final displayed chain, 2α(r) ≤ 4α(r-1) ≤ (8 log(2n)/B) Y(r-1) ≤ (8 log(2n)/B) OPT (p. 253-254) — the theorem's own statement only gives O(log n/B), so this explicit constant is this mission's own instantiation from the proof, not an independent derivation and not a transcription of a displayed theorem-level formula (flagged, per this series' explicit-constants rule).

Two milestones, in attack order:

• Theorem 14.1 (p. 249): the packing scheme is B-competitive, and violates each dual constraint by at most the book's own exact displayed bound c(i)·2log(1 + n·a_i(max)/a_i(min))/B (Claim (3) — the exact constant the proof establishes, not the theorem headline's O(·) simplification).
• Lemma 14.2 (p. 251): a matching lower bound, on the book's own explicit single-constraint instance, showing the additive log(a(max)/a(min)) term of Theorem 14.1 is necessary.

Significance

This chapter is the survey's demonstration that the primal-dual framework's core technique survives its most natural generalization, at the price of an explicit extra term the chapter also proves is unavoidable — a tight characterization, not merely an upper bound. Every other online covering/packing chapter in this survey (set cover, routing, ad-auctions, bounded allocation) is technically a special case of this chapter's general model; Chapter 4's restricted framework is the pedagogical entry point, and this chapter is where the general theory actually lives. No formal development of the general packing-covering problem was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

Two distinct obstacles, mirroring this chapter's own two schemes. First, Theorem 14.1's proof (p. 249-251) establishes its per-round primal/dual derivative inequality via a direct calculus argument (differentiating the explicit increment function) — formalized here as a hypothesis (hX_le_BY) standing for that calculation, not reproduced, since the goal is a faithful statement of the resulting competitive ratio, and the increment function's own exponential form is transcribed in the theorem's docstring but the differentiation itself is out of scope. Second, Theorem 14.3's phase-based mechanism is genuinely stateful across an unbounded number of phases (each phase resets its own primal/dual variables while the LP's actual variables retain the running maximum) — modeling this process explicitly is comparable in complexity to Chapter 13's level-based algorithm, and this mission makes the same scope choice: the mechanism's output (the resulting cost/profit relationship, hX_le_ratio) is taken as a hypothesis standing for the book's own Claims (1) and (3) combined, rather than constructed phase-by-phase.

Formalization scope

GeneralInstance I J bundles Fig. 14.1's fully general LP data (a(i,j) ≥ 0, c(i) > 0) — restated locally (not importing 04-framework's CoveringInstance) per this series' rule against cross-draft imports, even though this chapter is the direct generalization of that one. aMax/aMin are the per-variable (not per-instance) maximum and minimum-non-zero coefficients Theorem 14.1 needs. harmonicNum is restated locally (duplicated from 13-bounded-allocation's own definition, for the same no-cross-draft-import reason). Both goal-adjacent theorems use this series' weak-duality "competitive against any feasible comparison solution" pattern (04-framework, reused as a convention, not re-derived): Theorem 14.1 against any feasible packing comparison (matching that it concerns the packing side), Theorem 14.3 against any feasible covering comparison (matching the covering side). Welcome contributions: completing the three sorrys (Theorem 14.1's calculus argument, Theorem 14.3's phase-based mechanism constructed explicitly, and Lemma 14.2's direct summation argument, which is the most tractable of the three to actually prove), and formalizing the sanity check that both schemes reduce to Chapter 4's Algorithm 1/2/3 when a(i,j) ∈ {0,1}, b(j) = 1 (checked by hand in SELF_REVIEW.md, not as a Lean lemma).

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024

Motivation

The classical online allocation (AdWords) problem has a tight 1 - 1/e competitive ratio in general, achieved by the water-level algorithm and matched by a lower bound in which the number of buyers interested in each item can be as large as the total number of buyers. Buchbinder and Naor's Chapter 13 observes that in many realistic settings each item's interested-buyer set is much smaller than the total buyer population, and shows this structural fact — an explicit bound d on interested buyers per item — provably beats 1 - 1/e for every finite d, via a deliberately non-water-level algorithm. This mission formalizes that algorithm's competitive ratio and its matching lower bound.

Setting

A seller offers items to n buyers one at a time; buyer i has budget B(i) > 0. Each item j has a fixed price b(j) > 0 and a set S(j) of interested buyers with |S(j)| ≤ d. The fractional LP relaxation (Fig. 13.1) allocates y(i,j) ∈ [0,1] of item j to buyer i, subject to each item being sold at most once in total and each buyer's spending never exceeding budget; the seller's objective is to maximize total revenue ∑_j ∑_{i∈S(j)} b(j)y(i,j). Buyers are partitioned into d+1 levels by the fraction of budget spent so far (level k = spent between k/d and (k+1)/d); on each new item, the allocation algorithm splits it equally among the interested buyers in the lowest non-empty level, moving to the next level once that level's buyers are exhausted or saturated — deliberately not the naive "water-level" rule of splitting among the least-spent buyers, which the book shows cannot beat 1-1/e even for small d. The analysis tracks a piecewise-linear trade-off potential function f_d, built from a geometric sequence, that relates each buyer's level to their contribution to a feasible primal (covering) solution.

Formalization targets

Theorem 13.1 (the goal, p. 240): the allocation algorithm is C(d)-competitive, with the book's own explicit closed form C(d) = 1 - (d-1)/(d(1+1/(d-1))^{d-1}) — strictly better than 1 - 1/e for every finite d, approaching it as d → ∞ (Table 13.1). Formalized via the survey's standard weak-duality pattern (as in 04-framework's Theorem 4.3): given the algorithm's per-item primal/dual cost changes satisfying the book's core inequality ΔX(j) ≤ (1/C(d))ΔY(j) (established there by a potential-function case analysis, not reproduced here), the algorithm's realized profit is C(d)-competitive against any feasible comparison allocation.

Lemma 13.2 (milestone, p. 244): a matching lower bound, C(d) ≤ 1 - (k - kH(d) + ∑_{i=1}^k H(d-i))/d, where H is the harmonic number and k is the largest value with H(d) - H(d-k) ≤ 1.

Significance

This chapter is the survey's demonstration that a structural restriction invisible to the classical 1-1/e lower bound — a bound on demand concentration, not on budgets or prices — can be exploited algorithmically, and the exploiting algorithm is not the naive generalization of the water-level rule but a genuinely different level-based, "who's-behind" allocation rule. No formal development of the bounded allocation problem was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

The chapter's own proof of Theorem 13.1 (p. 241-244) is a page-and-a-half case analysis on how an item's fractional allocation crosses level boundaries, bookkeeping the change in both the primal potential-function value and the dual profit through several sub-cases (an item fully absorbed by one level; an item that empties a level and continues into the next; a level exhausting every interested buyer's budget). This mission formalizes the resulting per-item inequality ΔX(j) ≤ (1/C(d))ΔY(j) as a hypothesis (the theorem's own headline claim, not a case-by-case re-derivation) rather than modeling the stateful, order-dependent level-allocation process itself — the same scope choice this series makes for Chapter 11's randomized rounding process, where the book similarly omits (there, entirely; here, gives but does not ask this mission to reproduce) the underlying case analysis. The potential function f_d and its connection to the algorithm's primal variable (allocX) are formalized precisely, since they are what the goal's proof and Lemma 13.2 both depend on structurally, even though the case analysis linking them to ΔX/ΔY is left as the theorem's sorry.

Formalization scope

AllocationInstance I J bundles the LP data of Fig. 13.1 (S, B, b, d ≥ 2, ∀j, |S(j)|≤d) — restated locally per this series' rule that concurrent drafts cannot import each other, even though the problem is a special case of Chapter 10's ad-auctions model (the two chapters' algorithms differ: Chapter 10's is proportional-to-remaining-budget, this chapter's is level-based). geomSeq/potential transcribe the geometric sequence a_t and the potential function f_d at its level grid points exactly (not extended to non-grid-point reals, since Theorem 13.1's and Lemma 13.2's own statements only need the grid values). allocX connects the potential function to the algorithm's primal variable via each buyer's final level t(i). packingFeasible/packingValue transcribe Fig. 13.1's dual/packing LP with a genuine two-index allocation y : I → J → ℝ (not collapsed to a single per-item variable, unlike Chapter 4's simpler 0/1-coefficient framework). harmonicNum is the ordinary harmonic number. The level-based algorithm's literal stateful per-item update rule (which buyers move between which levels, in what order, within a single item's allocation) is not modeled directly — a documented scope reduction (STATUS.md), not a substitution of the "water-level" algorithm the book explicitly warns against (this mission's theorem13_1 commits to neither algorithm's literal rule, only to the resulting invariant the book's own proof establishes for the level-based one). Welcome contributions: completing the two sorrys, and modeling the level-allocation process explicitly enough to derive hinvariant from first principles.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• B. Kalyanasundaram, K. Pruhs. An optimal deterministic algorithm for online b-matching. Theoretical Computer Science, 233(1-2):319-325, 2000 (cited as [73], the 1-1/e lower bound).

Motivation

Network routing is one of the paradigmatic applications of the online primal-dual method: requests for bandwidth between a source and target arrive one at a time, and the algorithm must commit bandwidth to paths without knowing future requests. Chapter 4 already gave a simple (3, O(log n))-competitive routing algorithm as an illustration of the general framework. This chapter asks for something qualitatively stronger: a uni-criteria (1, O(log n))-competitive algorithm — one that routes the full optimal bandwidth (no loss on the throughput side at all), paying only in a bounded edge-capacity violation. The chapter shows this exact-throughput guarantee is achievable, and is moreover the key building block for several other routing objectives (fair routing, max-min fairness) built on top of it in Section 9.2 — a (1, O(log n))-competitive algorithm composes into those richer objectives in a way a merely constant-factor-lossy algorithm does not.

Setting

Fix a graph $G=(V,E)$, $|V|=n$, $|E|=m$, with integer edge capacities $u: E \to \mathbb{N}$. Routing requests $r_i$ arrive online, each demanding one unit of bandwidth between a source and target; in the splittable model (this chapter's comparison class), a request's bandwidth may be divided across multiple paths. A $(c_1,c_2)$-competitive algorithm routes at least $1/c_1$ of the maximum possible bandwidth while guaranteeing every edge's load (bandwidth allocated divided by capacity) is at most $c_2$. The chapter's generic algorithm (Section 9.1) maintains, for each of $O(\log n)$ copies $G_0,\dots,G_k$ of the graph (copy $j$ keeping only edges of capacity at least $m^j$, each capped at $\min(u(e), m^{j+2})$), a primal-dual pair matching Chapter 4's own routing LP (Fig. 9.1, identical to Fig. 4.2): a request is routed on the shortest path (by the copy's current primal edge-lengths $x(e,j)$) if that length is below $1$, multiplicatively updating $x(e,j)$ on the path's edges; otherwise, subject to a capacity-limited fallback rule, on an arbitrary feasible path.

Formalization targets

Theorem 9.2 (goal, p. 204): the algorithm is (1, O(log n))-competitive with respect to all splittable routing solutions — exact throughput (ratio 1), edge load at most O(log n).

Lemma 9.1 (milestone, p. 202-204): a single copy $G_j$'s own guarantee, which Theorem 9.2's proof composes across all copies: the algorithm accepts at least $M$ (the maximum splittable bandwidth achievable in $G_j$, out of the requests introduced to it) and incurs load $O(\log n)$ on every edge of $G_j$.

Significance

This is the survey's demonstration that the online primal-dual method, in its most basic form (a single accumulating dual sum driving a multiplicative primal update, exactly Chapter 4's framework), scales to a genuinely harder bicriterion objective once composed across a carefully constructed family of graph copies — the copies are what let the algorithm avoid ever needing to reason about which of the exponentially many $s_i$-$t_i$ paths to consider, reducing routing to a sequence of independent shortest-path computations. The chapter's own Section 9.2 builds a coordinate-wise-competitive fair-routing algorithm directly on top of Theorem 9.2 (not formalized here), and its Notes section places $(1, O(\log n))$-competitiveness as "a crucial non-trivial step" the chapter needed before those richer objectives became tractable at all. No prior formalization of online routing, splittable or otherwise, was found on the platform as of 2026-09-20 (search below).

Difficulty

This is the most algorithmically intricate chapter in this series: the algorithm processes each request against every one of $O(\log n)$ graph copies, each copy running its own instance of the Chapter-4-style primal-dual update, and Theorem 9.2's own proof composes Lemma 9.1's per-copy guarantee via a combinatorial backward induction (partitioning the offline-optimal solution's paths into groups by bottleneck capacity, and showing group by group that the algorithm's cumulative routed bandwidth across the top levels dominates the cumulative optimal bandwidth in those groups) together with a separate geometric argument bounding how many copies any single edge can meaningfully appear in. Fully modeling the copy construction, the request-routing process, and both composition arguments from first principles was judged to exceed this mission's time budget without sacrificing the faithfulness of what does get stated (per CAPTAIN_BRIEF.md rule 6). Instead: Lemma 9.1 is formalized via the two facts its own proof isolates as doing the real work — a weak-duality contradiction bound (stepB ≥ M − uMin) and the step-(1c) fallback's own greedy-fill rule for part (i); the multiplicative-update invariant x(e,j) ≤ 2 for part (ii), whose consequence — the exact constant 2 + 6·log₂n — is re-derived from scratch in this mission (the displayed equation this derivation depends on was garbled by the PDF's text extraction; it was confirmed against the actual typeset page image before drafting, see SELF_REVIEW.md). Theorem 9.2 then composes Lemma 9.1 across copies via two explicit, clearly-labeled hypotheses standing for the book's own backward-induction accounting and edge-multiplicity argument, respectively — genuine mathematical content this mission does not re-derive, named honestly as hypotheses rather than silently assumed away or approximated by a weaker statement.

Formalization scope

No shared data structure was introduced: every quantity in both theorems (bandwidths, capacities, loads) is a plain real-number hypothesis-level parameter, since neither theorem's own content needs a reusable instance record (unlike the packing/covering CoveringInstance of 04-framework, this chapter's per-copy quantities are consumed once each, not threaded through a family of algorithms). per_copy_guarantee (Lemma 9.1) takes the weak-duality bound, the step-(1c) fill rule, and the x(e,j)≤2 invariant as hypotheses and derives both parts of the lemma's conclusion by real algebra (a sign case-split for part (i); Real.logb/rpow manipulation for part (ii)). routing_competitive (Theorem 9.2) takes Lemma 9.1's guarantee (universally quantified over the copy index J, a general Fintype) plus the two composition hypotheses described above, and derives the bicriterion conclusion by summation, transitivity, and scaling. This correctly rules out the trivializing formalization in which the composition hypotheses are strengthened to directly assert the theorem's own conclusion (each is a strictly weaker, independently-motivated fact — the backward-induction accounting identity and the geometric edge-multiplicity bound — checked in MODERATION_NOTES.md against this exact failure mode). Reals throughout; Real.logb 2 for log₂. Welcome contributions: completing the two sorrys (Lemma 9.1's part (i) is short algebra; part (ii) needs Real.rpow/Real.logb lemmas; Theorem 9.2's is transitivity/summation once its hypotheses are in hand), and — the natural follow-on — formalizing the copy construction and the backward-induction/edge-multiplicity arguments hquota/hload_aggregation currently stand in for, which would upgrade them from hypotheses to theorems in their own right; Section 9.2's coordinate-wise-competitive fair-routing algorithm (Theorem 9.3) and the matching lower bound (Lemma 9.5) are further natural follow-ons.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024

Motivation

Caching is a two-level memory-management problem — the fast level (cache) can hold only $k$ items, and the algorithm must decide, online, which item to evict whenever the current request misses — that is normally analyzed through the competitive ratio of ad hoc marking or LRU-style rules. Buchbinder and Naor's survey [1] instead recasts weighted caching (non-uniform fetching costs) as an instance of the covering/packing linear program, and derives a fractional online algorithm through the same primal-dual recipe formalized in this series' 04-framework mission (Chapter 4), but for a genuinely different LP shape: the caching LP's right-hand side varies from constraint to constraint, unlike Chapter 4's uniform $b(j)=1$. This mission covers Sections 7.1-7.2 of Chapter 7, "Generalized Caching": the fractional weighted-caching algorithm and its $2(1+\ln k)$-competitive analysis. Sections 7.3-7.4, which further generalize to non-uniform page sizes (not just costs), are out of scope — a natural follow-on mission, not attempted here (see Formalization scope).

Setting

Fix a finite set $V$ of primal variables $x(p,j)$ — one per page $p$ and each of its eviction intervals between its $j$-th and $(j{+}1)$-th request — with fetching cost $c(p,j) = c_p \ge 1$ (the book's standing weighted-caching assumption), and a finite set $\mathrm{Time}$ of online constraints, one per request time $t$, revealed in the order enumerated by $\mathrm{Time}$. The eviction-charged LP formulation (the book charges for evicting pages rather than fetching them, an equivalent reformulation up to an additive constant independent of the request sequence) constrains, at each time $t$: $\sum_{v \in S(t)} x_v \ge \mathrm{rhs}(t)$, where $S(t)$ is the set of currently-active eviction variables for pages present until $t$ (excluding the page just requested) and $\mathrm{rhs}(t) = |B(t)| - k$ is the amount of cache space those pages must collectively vacate. The Lagrangian dual has a variable $y(t)$ per request time and a variable $z(p,j)$ per eviction interval, with dual constraint $\big(\sum_{t \mid v \in S(t)} y(t)\big) - z_v \le c_v$. As in Chapter 4, primal variables may only increase and the algorithm sees each constraint only upon its arrival.

The Fractional Caching algorithm (p. 153-154) sets each $x(p,j)$ to jump from $0$ to $1/k$ the first time its dual constraint tightens, then increases continuously according to an exponential function of the accumulated dual sum until it saturates at $1$ (at which point $z(p,j)$ begins absorbing further dual increase at the same rate, freezing $x(p,j)$). This is a genuinely different LP shape from Chapter 4's framework (non-uniform, time-varying right-hand side) reusing the same complementary-slackness design pattern as that chapter's Algorithm 3.

Formalization targets

Theorem 7.1 (the goal, p. 154), given the algorithm's final dual values $y \ge 0$, $z \ge 0$ and primal feasibility:

$$\Big(\forall v,\ \textstyle\sum_{t \mid v \in S(t)} y_t - z_v \le c_v(1+\ln k)\Big) \ \Longrightarrow\ \Big(\forall x''\text{ feasible},\ \textstyle\sum_v c_v x_v \le 2(1+\ln k)\sum_v c_v x''_v\Big),$$

i.e. the algorithm is $2(1+\ln k)$-competitive, with the constant taken verbatim from the book's own theorem statement (no $O(\cdot)$ instantiation needed here, unlike most goals in this series). The antecedent is itself Eq. (7.2) (p. 155), formalized as the milestone dual_near_feasible: the algorithm's dual solution, scaled down by $1+\ln k$, is feasible — the book's own intermediate step, derived from the fact that every cachingX value is capped at $1$.

Significance

Chapter 7 is the first chapter in this survey to apply the online primal-dual method to an LP whose right-hand side is not uniformly $1$ (unlike Chapters 4 and 5), demonstrating the method's reach beyond the "simplified" 0/1-coefficient covering LP that 04-framework formalizes. The $2(1+\ln k)$ fractional guarantee is also the analytical core of the chapter's randomized rounding result (Theorem 7.3, not part of this mission — see Formalization scope), which converts it into an actual $O(\log k)$-competitive randomized algorithm against an adaptive adversary, and of the chapter's further generalization to non-uniform page sizes (Theorem 7.5, Sections 7.3-7.4). No formal development of weighted or generalized caching was found on the platform as of 2026-09-20 (searches below); the existing KServer.* namespace formalizes a different, unweighted, uniform $k$-server model and shares no substrate with this mission. This mission is the first.

Difficulty

As with 04-framework's Algorithm 3, the central obstacle is characterizing an online process by its final output alone: cachingX is defined as the algorithm's own closed-form update rule (threshold-then-exponential, capped once $x(p,j)=1$), evaluated at the run's final accumulated dual values, rather than as an independently-constrained free variable — the latter would let $x$ and $y$ be chosen to satisfy the conclusion's inequalities directly, trivializing the claim that a specific online algorithm achieves this ratio. Establishing that the capped closed form is faithful (not merely an invented convention) requires the same monotonicity argument 04-framework's alg3X uses, adapted to this chapter's extra $z(p,j)$ term inside the exponent (present here; absent from Chapter 4's Algorithm 3). The proof's own structure — splitting the primal cost into a $0\to1/k$ contribution ($C_1$) bounded via complementary slackness and a $1/k\to1$ contribution ($C_2$) bounded via a derivative/telescoping argument over the continuous accumulation process (Eqs. (7.6)-(7.10), p. 155-157) — is, as in Chapter 4, a genuinely dynamic fact about the trajectory, not encoded as a hypothesis; the mission states the theorem faithfully and leaves the sorry for that argument, per this series' documented-simplification convention.

Formalization scope

CachingInstance V Time bundles S : Time → Finset V, rhs : Time → ℝ (unlike 04-framework's CoveringInstance, whose right-hand side is fixed at $1$ throughout), c : V → ℝ with hc_pos : ∀v, 1 ≤ c v (the book's own literal cp ≥ 1, not a strengthening), and k : ℕ with hk_pos : 0 < k. dualSum inst y v := ∑_{t \mid v \in S(t)} y_t, matching 04-framework's pattern. cachingX inst y z v is a noncomputable def: 0 before activation, otherwise min 1 ((1/k) exp((dualSum - z - c v)/c v)), so "the algorithm's output" is genuinely a function of its dual trajectory. Reals throughout; Real.log for the book's natural log $\ln$. Explicitly out of scope: Section 7.3's rounding apparatus (Theorem 7.3, the map from fractional to randomized-integral cache states) and Section 7.4's non-uniform-page-size generalization (Theorem 7.5) — both are natural follow-on missions building on this one's CachingInstance and cachingX, not attempted here per this chunk's own BRIEF.md, which flags Theorem 7.1 alone as "a complete, self-contained mission goal" when the rounding apparatus proves too heavy for a single pass. Welcome contributions: completing the two sorrys, and the Section 7.3-7.4 follow-on mission.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024

Motivation

The metrical task system (MTS) problem is one of the earliest and most general online models: a server occupies a state in a metric space, requests arrive with per-state service costs, and the server may change state (paying the metric's transition cost) before serving each request. On a general metric, competitive algorithms are hard to design directly. Chapter 6 shows that on a weighted star metric — the simplest genuinely non-uniform metric, a hub with leaves at varying distances — the online primal-dual framework of Chapter 4 becomes applicable, but only after a change of rules: the chapter defines a new MTS model, in which the server may change state only at the boundary of a "phase" (an interval during which its accumulated service cost reaches the state's own transition charge), and shows this new model is cost-equivalent, up to a constant factor, to the standard model. This equivalence is what licenses recasting the (new-model) problem as a covering linear program with the online primal-dual framework directly applicable — the chapter's actual algorithmic payoff (an unnumbered $O(\log N)$-competitive result, Section 6.2) rests entirely on it.

Setting

Fix a set of leaves $V$ (the book's finite $\{1,\dots,N\}$) of a weighted star, each leaf $i$ at distance $d'(i) \ge 0$ from the center. The chapter immediately collapses the full star metric to a single per-state transition charge $d(i) := 2d'(i)$, since on a star every transition $i \to j$ costs at most $d'(i) + d'(j)$, and charging the doubled source leaf's distance alone (never charging for arriving) upper-bounds every transition cost independent of destination. A standard-model solution is a finite sequence of runs, each specifying a state $s_i$ occupied and the service cost $w_i \ge 0$ accumulated while in that state, ending with a transition (cost $d(s_i)$) to the next run's state; its total cost is $\sum_i (w_i + d(s_i))$. A new-model solution is a finite sequence of phases, each specifying a state visited; a phase's cost is exactly $d(\text{state})$ regardless of how much service actually occurred during it (a state change is only permitted once a phase's accumulated service reaches the phase's own $d$-value), so the new model's total cost is $\sum_i d(s_i)$.

Formalization targets

Lemma 6.1 (goal, p. 144): any standard-model solution's runs $(s, w)$ transform into a new-model solution whose cost is at most $2 \cdot \sum_i (w_i + d(s_i))$; in particular $OPT_n(\bar\sigma) \le 2 \cdot OPT_o(\bar\sigma)$.

Lemma 6.2 (milestone, p. 145): any new-model solution's phases $(s, w)$, with each phase's actual service $w_i \le d(s_i)$, are simultaneously a legal standard-model solution (the same trajectory, recosted) whose standard-model cost is at most $2 \cdot \sum_i d(s_i)$.

Together (stated in the book but not separately numbered, hence not a formalization target here): a $c$-competitive algorithm in the new model implies a $4c$-competitive algorithm in the standard model.

Significance

This is a model-equivalence result, a distinct and recurring pattern in online algorithm design from the competitive-ratio bounds formalized elsewhere in this series: rather than analyzing an algorithm directly, the chapter first shows that solving an easier, more restricted version of the problem (state changes only at phase boundaries) loses only a constant factor, and only then designs an algorithm for the restricted version. The technique generalizes (the chapter's own Notes section places it in the context of Borodin et al.'s original MTS bounds, and of later work on hierarchically well-separated trees for general metrics), but this chapter gives its cleanest, self-contained instance: two short, tight (factor-2 each direction) transformations between two formally distinct online cost models. No prior formalization of metrical task systems on a weighted star, or of this new/standard model equivalence, was found on the platform as of 2026-09-20 (search below); the platform's existing KServer.* campaign formalizes a different online problem (uniform-metric $k$-server) with a different metric structure and is not adjacent substrate for this chapter's weighted-star MTS model.

Difficulty

The central obstacle is representing "a solution" at a level of abstraction faithful to the book's own proof without committing to a full continuous-time process model (states as functions of a real time variable, phases as recursively-defined stopping times, requests as an explicit arriving sequence) that neither lemma's own proof actually needs. Both proofs work entirely at the granularity of a solution's runs (standard model) or phases (new model) — finite sequences of (state, cost) data — never referencing continuous time except to justify that this decomposition exists. This mission formalizes both lemmas at exactly that granularity: a run/phase sequence indexed by Fin k, with costStandard/costNewPhases the book's own displayed cost formulas. Lemma 6.1's proof genuinely constructs a new object (the delayed-transition solution $S'$) and only bounds its cost, never gives $S'$ a closed form — formalized here as an existential over a per-segment cost witness w', bounded above and below exactly as the proof's own argument does (with the lower bound d(s i) ≤ w' i serving as the guard against the vacuous witness w' = 0, since without it the existential is trivially satisfiable and asserts nothing). Lemma 6.2's proof, by contrast, reuses the same trajectory in both models with no construction at all, formalized directly as a cost comparison between costStandard and costNewPhases applied to the identical (s, w) data.

Formalization scope

WeightedStar V bundles centerDist : V → ℝ (the book's $d'$) with non-negativity; WeightedStar.d is the collapsed charge $d(i) = 2d'(i)$. costStandard/costNewPhases are literal transcriptions of the two models' displayed cost formulas over a Fin k-indexed run/phase sequence. standard_to_new (Lemma 6.1) is the existential described above; new_to_standard (Lemma 6.2) is the direct cost comparison. Reals throughout; V is left a general Type* (not assumed Fintype) since neither lemma's own statement needs the chapter's finiteness assumption $|V|=N$ — that assumption only matters for the unnumbered $O(\log N)$-competitive claim of Section 6.2, out of scope per BRIEF.md's explicit instruction (no numbered theorem to formalize it against). This correctly rules out the trivializing formalization in which "new-model solution" is left as an unconstrained free variable satisfying only the conclusion's own inequality, or in which the star structure is dropped entirely in favor of an arbitrary metric (the chapter's own reduction to a per-state charge $d(i)$, rather than a full metric $d: V\times V\to\mathbb R$, is precisely what the star's structure licenses, and is preserved here via WeightedStar.d rather than a bare hypothesis-level function). Welcome contributions: completing the two sorrys (Lemma 6.1's needs an explicit construction of $S'$ and its per-segment cost bound; Lemma 6.2's is a short termwise algebraic argument), and formalizing the Section 6.2 covering-LP algorithm and its $O(\log N)$-competitive claim as a follow-on mission once it can be stated against a numbered result.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• Bansal et al., reference [14] of this chapter's own bibliography (not independently verified by this mission), cited by the book as the source of the weighted-star MTS results this chapter presents ("The results in this chapter are based on the work of Bansal et al. [14]," p. 147).
• Borodin, Linial, Saks, reference [29] of this chapter's own bibliography (not independently verified by this mission), cited as the paper that originally formulated the standard MTS model and its tight $2N-1$ deterministic bound (p. 147).

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