All missions

Motivation

Open shops model production and service systems in which every job must visit every machine, but the order of the visits is free: a car that needs an inspection, a wash and a tyre change, a patient who needs several tests, a student who sits several exams. The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) fixed the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it can express. Among the polynomially solvable cases, the preemptive open shop with makespan objective, $O|pmtn|C_{\max}$, is one of the few multi-machine problems whose optimal value has a closed form for any number of machines and jobs.

Timeline.

• 1976: Gonzalez and Sahni (J. ACM 23) prove that the optimal preemptive open-shop makespan is the largest machine load or job length, and give a polynomial algorithm. In the same paper they solve $O2\|C_{\max}$ in linear time and show $O3\|C_{\max}$ NP-hard.
• 1978: Lawler and Labetoulle (J. ACM 25) give a linear-programming treatment of preemptive scheduling on unrelated machines and reformulate the open-shop construction in terms of decrementing sets, found by an assignment problem through the Birkhoff–von Neumann theorem.
• 1979: the survey (§5.2.2, p. 313) presents this construction as the standard argument and records the $O(r+\min\{m^4,n^4,r^2\})$ bound of Gonzalez (1976), where $r$ is the number of nonzero processing times.

Setting

There are $m$ machines $M_1,\dots,M_m$ and $n$ jobs $J_1,\dots,J_n$. Job $J_j$ consists of operations $O_{1j},\dots,O_{mj}$; operation $O_{ij}$ must be processed on machine $M_i$ for $p_{ij}\ge 0$ time units. The processing-time matrix is $P=(p_{ij})$: its rows are machines and its columns are jobs. Every job is available at time $0$.

Preemption is allowed: an operation may be interrupted and resumed later. A schedule is a finite list of pieces $(i,j,s,e)$, each meaning that $M_i$ processes $J_j$ during $[s,e)$. A schedule is feasible if

1. every piece satisfies $0\le s\le e$;
2. each machine processes at most one job at a time, and each job is processed on at most one machine at a time: two pieces that share a machine or a job do not overlap;
3. for every pair $(i,j)$ the pieces of $O_{ij}$ have total length exactly $p_{ij}$.

The makespan $C_{\max}$ is the time at which the last piece ends, and $C^*_{\max}$ is its minimum over feasible schedules. The load of machine $M_i$ is the row sum $\sum_j p_{ij}$, the length of job $J_j$ is the column sum $\sum_i p_{ij}$, and

$$C=\max\Big\{\max_j \sum_i p_{ij},\ \max_i \sum_j p_{ij}\Big\}.$$

A row or column is tight if its sum equals $C$ and slack otherwise. A decrementing set is a set $S$ of strictly positive entries of $P$ with exactly one element in each tight row and each tight column and at most one in each slack row and each slack column.

Formalization targets

Goal: $C^*_{\max}=C$

For every $T\ge 0$,

$$\big(\exists \text{ feasible schedule with } C_{\max}\le T\big)\iff \Big(\sum_j p_{ij}\le T\ \forall i\ \text{ and }\ \sum_i p_{ij}\le T\ \forall j\Big).$$

This says that the optimal makespan is exactly the largest machine load or job length, and that it is attained.

Milestones (all from §5.2.2, p. 313)

1. Lower bound $C^*_{\max}\ge C$.
2. Existence of a decrementing set for every nonzero nonnegative $P$.
3. Positive step: for a decrementing set, the largest $\delta$ satisfying the constraints (1)–(3) of the survey exists and is positive.
4. Step property: after replacing each $p_{ij}\in S$ by $\max\{0,p_{ij}-\delta\}$, the largest line sum is exactly $C-\delta$.
5. Partial schedule: for each $p_{ij}\in S$, $M_i$ processes $J_j$ for $\min\{p_{ij},\delta\}$ time units, with no machine or job used twice.
6. Termination: every run of the procedure reaches $P'=(0)$ within a bounded number of stages.
7. Joining: the concatenated partial schedules form a feasible schedule with $C_{\max}\le C$.

Significance

The result. The theorem turns an optimization over continuous-time schedules into the computation of $m+n$ sums. It certifies optimality by a counting argument, it is the base case for preemptive open shops with release dates and due dates, and it is used elsewhere in the survey (§4.4.6) to reduce problems on unrelated machines with preemption to open-shop instances. Because a nonnegative matrix whose row and column sums are all equal is a multiple of a doubly stochastic matrix, the theorem is a scheduling form of the Birkhoff–von Neumann decomposition. It also underlies timetabling and edge-colouring results for bipartite multigraphs.

Formalizing it. The theorem has been proved since 1976 and is textbook material. No machine-checked proof is known to exist: Mathlib has the Birkhoff–von Neumann theorem for doubly stochastic matrices but no model of open-shop schedules. A formalization adds a reusable model of preemptive multi-machine schedules with both disjointness requirements, a checked proof of the decrementing-set construction, and a termination argument the survey asserts without proof.

Difficulty

The lower bound is a one-line counting argument. The difficulty is the construction of a schedule of length exactly $C$. Scheduling each machine's operations back to back gives length $\max_i\sum_j p_{ij}$, but may run one job on two machines at once. Scheduling job by job has the symmetric defect. A greedy list schedule that only respects both constraints can leave machines idle and overshoot $C$. The construction must keep every tight line busy at every moment while never letting a slack line fall behind. The existence of the decrementing set at each stage is the combinatorial core: it is a Hall-type matching condition, not a local choice. Termination is also not automatic, because a careless choice of step length can produce infinitely many shrinking steps.

Formalization scope

All objects live in the namespace SchedSurvey.OPmtn. Machines and jobs are Fin m and Fin n, both 0-based, and processing times and piece endpoints are real numbers; integer data are a special case. A schedule is a List of pieces. Feasibility requires nonnegative start times, disjointness for pieces sharing a machine or a job (touching intervals allowed), and exactly $p_{ij}$ units of processing for every pair $(i,j)$. Every theorem assumes $p_{ij}\ge 0$.

"$C$ is the maximum" is the predicate IsMaxLoad P C: all line sums are at most $C$ and one equals $C$. The goal is stated in threshold form and mentions no maximum at all. The display defining $C$ on p. 313 prints $\max_i\{\sum_i p_{ij}\}$ for the second term; the following sentence shows it means the row sums $\sum_j p_{ij}$, and the formalization uses those. The hypothesis $T\ge 0$ matters only for $P=0$, where the empty schedule finishes by every $T$.

A trivializing formalization is ruled out: the goal mentions neither decrementing sets nor $\delta$. Its "if" direction asserts that a schedule exists. Feasibility counts work per pair (machine, job), not per job, and forbids a job from running on two machines at once. Without either requirement the statement would be a different and easier theorem.

A complete development needs: list sums of interval lengths over disjoint intervals, the existence of decrementing sets (via Birkhoff–von Neumann, König's theorem or Hall's theorem on the bipartite graph of positive entries), the step and termination lemmas, and concatenation of schedules. The schedule model and the decrementing-set lemma are reusable for other preemptive shop problems. Contributions of alternative proofs of any milestone, for example a direct Hall-theorem proof of the existence of decrementing sets, are welcome.

Selected references

• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23 (1976) 665–679. https://doi.org/10.1145/321978.321985
• E. L. Lawler, J. Labetoulle, On preemptive scheduling of unrelated parallel processors by linear programming, Journal of the ACM 25 (1978) 612–619. https://doi.org/10.1145/322077.322090

Motivation

Shop scheduling asks how to sequence jobs that each need processing on several machines. In an open shop, a job's operations may be executed in any order, as in testing stations, repair bays, or classroom and examination timetables, where the order in which a candidate visits the stations is irrelevant. The objective studied here is the makespan $C_{\max}$, the time at which the last operation finishes.

The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) introduced the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it names. For the open shop, its §5.2.1 presents a simplified exposition of the result of Gonzalez and Sahni (J. ACM 23, 1976): with two machines and no preemption, the obvious lower bound on the makespan is always achieved. The same page records that the three-machine case $O3\|C_{\max}$ is binary NP-hard, so two machines is exactly where the problem is easy.

Timeline. Gonzalez and Sahni (1976) gave the linear-time algorithm for $O2\|C_{\max}$, proved NP-hardness for $O3\|C_{\max}$, and gave a polynomial algorithm for the preemptive problem $O|pmtn|C_{\max}$. Graham et al. (1979, §5.2.1) gave the shorter construction formalized here, and observed (§5.2.2) that it implies preemption brings no advantage for $m = 2$. Lenstra (cited as forthcoming in the survey) showed $O2|r_j|C_{\max}$, $O2|tree|C_{\max}$ and $O\|C_{\max}$ unary NP-hard.

Setting

There are $n$ jobs $J_1, \dots, J_n$ and two machines $M_1$, $M_2$. Job $J_j$ has an operation on $M_1$ of length $a_j \ge 0$ and an operation on $M_2$ of length $b_j \ge 0$. There is no preemption, and every job is available at time $0$. A schedule assigns start times $s_1(j)$ and $s_2(j)$ to the two operations of $J_j$, which then occupy $[s_1(j), s_1(j)+a_j)$ on $M_1$ and $[s_2(j), s_2(j)+b_j)$ on $M_2$.

A schedule is feasible if

1. all start times are nonnegative;
2. each machine processes at most one job at a time: the intervals of distinct jobs on the same machine do not overlap;
3. each job is processed on at most one machine at a time: the two intervals of the same job do not overlap, in either order.

Write $T_1 = \sum_j a_j$ and $T_2 = \sum_j b_j$ for the two machine loads. The survey's construction uses the sets

$$A = \{J_j \mid a_j \ge b_j\}, \qquad B = \{J_j \mid a_j < b_j\},$$

two distinct jobs $J_r$, $J_l$ with $a_r \ge \max_{J_j \in A} b_j$ and $b_l \ge \max_{J_j \in B} a_j$, and $A' = A - \{J_r, J_l\}$, $B' = B - \{J_r, J_l\}$.

Formalization targets

Goal: the optimal makespan

$$C^*_{\max} = \max\Big\{T_1,\ T_2,\ \max_j\,(a_j + b_j)\Big\},$$

and the optimum is attained. Formally, for every $T \ge 0$: a feasible schedule completing every operation by $T$ exists if and only if $T_1 \le T$, $T_2 \le T$ and $a_j + b_j \le T$ for all $j$. The goal mentions neither $A$, $B$, $J_r$, $J_l$ nor the case analysis; those are the milestones.

Milestones (in the order of the argument)

1. Two distinct jobs $J_r$, $J_l$ with the required bounds exist when $n \ge 2$.
2. Fig. 5.1: the blocks $B' \cup \{J_l\}$ and $A' \cup \{J_r\}$, with $A'$ and $B'$ in arbitrary order, have feasible staircase schedules without idle time.
3. Fig. 5.2: if $T_1 - a_l \ge T_2 - b_r$, the blocks combine into a feasible schedule of all jobs ending by $T_1 + b_r$.
4. Case (1): if moreover $a_r \le T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, T_2\}$.
5. Case (2): if moreover $a_r > T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, a_r + b_r\}$.
6. The symmetric case $T_1 - a_l < T_2 - b_r$: some feasible schedule has length at most $\max\{T_1, T_2, a_l + b_l\}$.
7. The lower bound: every feasible schedule has $C_{\max} \ge \max\{T_1, T_2, \max_j(a_j + b_j)\}$.

Significance

The result. The theorem gives a closed form for the optimal makespan of a two-machine open shop, together with a linear-time construction of an optimal schedule. The survey uses it immediately: since the bound is also a lower bound for preemptive schedules, $O2|pmtn|C_{\max}$ is solved by the same schedules, so preemption gives no advantage on two machines (§5.2.2). It is the standard example of a shop problem whose trivial lower bound is tight, and the contrast with the binary NP-hard $O3\|C_{\max}$ marks the complexity boundary for nonpreemptive open shops.

Formalizing it. The result is classical and proved on paper; no machine-checked proof is known to exist on this platform. The mission produces a reusable model of nonpreemptive two-machine open-shop schedules with real processing times, a verified lower bound, and a verified constructive argument. Unlike many existence-of-schedule results, the survey's construction is explicit (orders and start times), so it can be formalized directly rather than through an abstract existence argument.

Difficulty

The lower bound is the easy half. The difficulty is the construction: a schedule must meet the bound simultaneously on both machines and for every job. The natural first idea, running every job on $M_1$ then $M_2$ in some order (a flow-shop schedule), fails: Johnson's rule then gives a makespan that can exceed $\max\{T_1, T_2, \max_j(a_j+b_j)\}$, because the open shop needs some job to visit $M_2$ first. The survey's construction moves exactly one job, $J_r$, to the front of $M_2$, and its correctness depends on the choice of $J_r$ and $J_l$ and on the case split on $T_1 - a_l$ versus $T_2 - b_r$. Figures 5.3 and 5.4 are drawn for $T_1 \ge T_2$; in the other subcases the start times shown in the figures need adjustment, and the formal statements of the cases assert lengths rather than the figures' exact start times.

Formalization scope

All declarations live in the namespace SchedSurvey.O2. Jobs are Fin n, 0-based ($J_j$ is index $j-1$). Processing times and start times are real numbers with $a_j, b_j \ge 0$; the survey's integer data are a special case, and every claim of §5.2.1 holds over the reals. A schedule is a pair of start-time functions s₁ s₂ : Fin n → ℝ. Interval non-overlap is s + p ≤ s' ∨ s' + p' ≤ s, so touching intervals are allowed and a zero-length operation occupies nothing. Feasibility (IsFeasible) contains both disjointness constraints of §2.1, the machine constraint and the job constraint, with the two operations of a job in either order. The job constraint is essential: without it the optimum would be $\max\{T_1, T_2\}$ and the goal false.

"Length at most $L$" is CompletesBy a b S L: every operation ends by $L$. Optimality is stated in threshold form, which avoids taking a supremum or infimum over a possibly empty set and is equivalent to "$C^*_{\max}$ equals the maximum and is attained". A maximum over $A$ or $B$ appears as a bound on every member, which is also correct for empty $A$ or $B$. The orders of $A'$ and $B'$ are duplicate-free lists whose members are exactly those sets; back-to-back start times are given by contigStart.

The milestone on the choice of $J_r$, $J_l$ assumes $n \ge 2$, which the page presupposes; the goal does not, and covers $n \le 1$ as well. The lower bound assumes $T \ge 0$, which matters only for $n = 0$.

A trivializing formalization is ruled out: feasibility includes both disjointness constraints and nonnegative start times, the threshold is quantified over all $T \ge 0$, and no constant is fixed.

Contributions welcome: proofs of the lower bound (a sum of disjoint intervals inside $[0, T]$), of the list-based block lemmas, of the case lemmas, and of the goal from them. The interval and back-to-back-schedule lemmas are reusable for other shop problems.

Selected references

• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
• S.M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110

Motivation

Queueing results often relate an average accumulated over customers to an average accumulated over time. In the familiar relation $L=\lambda W$, the long-run average number in a system equals the arrival rate times the average time spent there. Glynn and Whitt study a broader relation, $H=\lambda G$, that can represent queue lengths and waiting times but also costs, work, and other cumulative inputs. Their framework is deterministic: a stochastic model may supply a sample path, yet the central comparison is a statement about functions on that path. This lets the same theorem apply to different queueing models without choosing a probability law for each one. Glynn and Whitt (1989)

The paper asks for more than the usual forward implication from a customer average to a time average. Its main theorem identifies conditions under which either average has a finite limit exactly when the other does. It also compares lim inf and lim sup when ordinary limits fail to exist. Both questions matter when sample paths fluctuate: convergence of one average cannot simply be inferred from a visual similarity between the two ways of indexing the input. Glynn and Whitt (1989), §§1–2

Setting

A cumulative input is a real-valued function $F(s,t)$ on $[0,\infty)\times[0,\infty)$, nondecreasing separately in the customer coordinate $s$ and the time coordinate $t$. Its marginal limits $F(s,\infty)$ and $F(\infty,t)$ are finite for every fixed argument. The first counts all eventual input associated with customers through index $s$; the second counts all input accumulated through time $t$. The marginal averages are

$$G(s)=\frac{F(s,\infty)}{s},\qquad H(t)=\frac{F(\infty,t)}{t}.$$

The paper permits cumulative inputs that are not distribution functions of measures on rectangles. In particular, it does not require a rectangle-increment inequality or nonnegative values of $F$. The finite marginal limits and monotonicity are the actual assumptions of its general framework. Glynn and Whitt (1989), p. 635, (1)

A time change $T_i(s)$, for $i=1,2$, is finite, nonnegative, nondecreasing, and right-continuous, and tends to infinity with $s$. Its right-continuous inverse is $S_i(t)=\inf\{s\geq0:T_i(s)>t\}$. The two time changes may differ. Both have the same asymptotic rate $T_i(s)/s\to\lambda^{-1}$ for a positive finite $\lambda$. The paper's two approximation conditions are

$$\frac{F(s,T_1(s-))-F(\infty,T_1(s-))}{s}\longrightarrow0 \quad(14), \qquad \frac{F(s,\infty)-F(s,T_2(s))}{s}\longrightarrow0 \quad(15),$$

as $s\to\infty$, where $T_1(s-)$ is the left limit. Condition (14) concerns input already present by a left-limit time; condition (15) concerns input not yet present by a right-limit time. Glynn and Whitt (1989), p. 638, (3), (14)–(15)

Formalization targets

One-sided asymptotic bounds

With only (14) and the rate for $T_1$, the corrected upper bounds are

$$\liminf H\leq\liminf \lambda G,\qquad \limsup H\leq\limsup \lambda G.$$

With only (15) and the rate for $T_2$, the corrected lower bounds reverse both inequalities. The two bounds remain useful separately when only one approximation condition holds. Their lim inf and lim sup may be infinite. Glynn and Whitt (1989), p. 639, Theorem 1(a)–(b) and Remark 2

Equality of asymptotic bounds and finite limits

Under both conditions, Theorem 1(c) asserts equality of the respective lim inf and lim sup. The mission goal is Theorem 1(f): for finite real limits,

$$H(t)\to h\quad\Longleftrightarrow\quad G(s)\to g, \qquad\text{and whenever these limits exist, }h=\lambda g.$$

Here the equivalence means existence of finite limits, with the second clause identifying their values. The lim inf and lim sup statement is retained as a milestone because it also covers nonconvergent paths. Glynn and Whitt (1989), p. 639, Theorem 1(c), (f)

Significance

The goal gives a two-way transfer between customer-indexed and time-indexed long-run averages. If an application establishes one finite average, the theorem supplies the other and fixes its value. The one-sided milestones give meaningful bounds when only one approximation condition is available; the lim inf and lim sup milestone retains information when neither average converges. These outcomes are stated for a general cumulative input, so applications can supply their own $F$, $T_1$, and $T_2$ without changing the theorem. Glynn and Whitt (1989), §§2–4

The paper proves these results on paper. The formalization target is a machine-checked interface for the paper's deterministic framework, its inversion lemmas, its asymptotic inequalities, and the two-way limit theorem. At this drafting stage the Lean theorem statements compile with proof placeholders; no machine-checked proofs of these new statements are claimed. The definitions and inverse-rate lemma can be reused in other sample-path results.

Difficulty

The two marginal averages examine different slices of $F$, and a time change may jump or have flat intervals. A direct substitution of $t=T_i(s)$ does not give an equality between $F(s,\infty)$ and $F(\infty,t)$ under the paper's assumptions. The left limit in (14) and the value in (15) also behave differently at jumps. The inverse $S_i$ connects the coordinates, but its boundary behavior and rate must be handled before comparing the averages. These issues are present even without stochastic randomness. Glynn and Whitt (1989), pp. 638–639

Formalization scope

Lean represents $s,t$ by nonnegative real numbers and $F$ by a real-valued function with separate monotonicity and bounded marginal ranges. Real suprema represent $F(s,\infty)$ and $F(\infty,t)$; the boundedness fields ensure those suprema are the paper's finite limits. The inverse is an infimum of a nonempty set because $T_i\to\infty$. The left limit is the supremum over earlier nonnegative arguments, with $T(0-)=0$. Ratios at zero use Lean's total division convention, but every ratio assertion is asymptotic at infinity.

Lim inf and lim sup are taken in the extended reals so an unbounded average retains an infinite limit. Multiplication by $\lambda$ happens in the reals before conversion. Ordinary limits in Theorem 1(f) are finite real limits. The two time changes are independent and share only the positive rate $\lambda$. The goal assumes only (14), (15), and the stated time-change rates; it does not assume its own inverse-rate or asymptotic conclusions. No nonnegativity or rectangle inequality is imposed on $F$.

Theorem 1(a) and (b) have their hypothesis pairing reversed in print. The formalized one-sided bounds use the corrected pairing, and the milestone text preserves the printed source for audit. The intermediate expressions involving $G(S_i(t))$ are excluded from the corrected statements because the framework does not assume customer-coordinate right continuity. Theorem 1(c) and (f) use both conditions and are true as printed. The scope includes the definitions, Lemmas 1–2, corrected parts (a)–(b), and parts (c) and (f). Contributions toward their proofs and reusable time-change lemmas are welcome. Glynn and Whitt (1989), p. 639, Theorem 1

Selected references

• P. W. Glynn and W. Whitt, Extensions of the Queueing Relations L = λW and H = λG, Operations Research 37(4):634–644, 1989. DOI: 10.1287/opre.37.4.634

Motivation

An integer program is a linear program whose variables must take integer values. Its linear relaxation can be solved efficiently, while the integer program itself is NP-hard in general, so a recurring question in integer programming is how much the optimal solution of the relaxation says about the integer optimum. Simple rounding of the fractional optimum does not answer it: examples show that the integer optimum need not lie within distance one of the LP optimum, even when the right-hand side is large.

R. E. Gomory's 1965 note in the Proceedings of the National Academy of Sciences (doi:10.1073/pnas.53.2.260) showed that, for right-hand sides lying deep inside the cone of an optimal LP basis, the integer program is solved exactly by the LP solution plus a correction computed in a finite abelian group. The resulting group relaxation (the "corner polyhedron" of Gomory's later work, Gomory 1969) underlies a large body of work on cutting planes, the master group problem, Gomory–Johnson functions and asymptotic integer programming.

Timeline. Gomory's fractional cutting-plane algorithm (Gomory 1958) introduced the "fractional rows" of the simplex tableau; the 1965 note identifies the group they generate with $M(I)/M(B)$ and proves the asymptotic theorem formalized here. Gomory 1969 develops the corner polyhedron; Gomory and Johnson (1972) study the continuous valid functions of the corner polyhedron.

Setting

Let $A$ be an integer $m\times(m+n)$ matrix of the form $(A',I)$, let $b\in\mathbb Z^m$ and $c\in\mathbb R^{m+n}$. Problem P1 is

$$\max\ z_1=cx\quad\text{s.t.}\quad Ax=b,\ x\ge0,$$

and P2 is P1 with $x$ integer. A basis is a nonsingular $m\times m$ submatrix $B$ of $A$; after rearranging, $A=(B,N)$ with $B=(\alpha_1,\dots,\alpha_m)$ and $N=(\alpha_{m+1},\dots,\alpha_{m+n})$, and $c=(c_B,c_N)$. The relative cost of a nonbasic column is $c^*_i=c_i-c_BB^{-1}\alpha_i$, and $B$ is an optimal basis when all $c^*_i\le0$. The cone of the basis is $K^B=\{\beta\in\mathbb R^m: B^{-1}\beta\ge0\}$; removing from it all points within Euclidean distance $d$ of its boundary gives the reduced cone $K^B(d)$.

Let $M(I)=\mathbb Z^m$ and $M(B)=\mathfrak L_B$ the lattice of integer combinations of $\alpha_1,\dots,\alpha_m$. The factor module $M(I)/M(B)$ is a finite abelian group with $D=|\det B|$ elements; write $\bar\alpha_i$, $\bar b$ for the classes of $\alpha_i$, $b$. The group problem (4) is

$$\max\ \sum_{i=1}^n c^*_{i+m}y_i\quad\text{s.t.}\quad\sum_{i=1}^n\bar\alpha_{i+m}y_i=\bar b,\quad y_i\ge0\text{ integer},$$

with optimal value $\varphi^B(b)$. Finally $l=\max_{i>m}\|\alpha_i\|$.

Formalization targets

Goal: THEOREM 1 (p. 261)

If $b\in K^B(l(D-1))$, then P1, P2 and (4) attain their optima, the value $z_2(b)$ of P2 is

$$z_2(b)=z_1(b)+\varphi^B(b),$$

an optimal solution of P2 is

$$x(b)=\big(B^{-1}(b-Ny^B(b)),\ y^B(b)\big)$$

for an optimal solution $y^B(b)$ of (4) with $\sum_iy^B_i(b)\le D-1$, and $\varphi^B$, $y^B$ are $m$-periodic: $\varphi^B(b+\alpha_i)=\varphi^B(b)$.

Milestones

In the order of the paper's proof: $|M(I)/M(B)|=D$ (p. 262); periodicity of (4) (p. 263); the cost identity (5)–(6); "$c_BB^{-1}b$ is $z_1(b)$", the simplex optimality criterion (a published, proved theorem); the projection of a solution of P2 to a solution of (4); the bound (7), $z_2(b)\le z_1(b)+\varphi(b)$; the extension of a solution of (4) to an integer solution; the LEMMA (an optimal solution of (4) with $\sum y_i\le D-1$); and the bound $\|Ny\|\le(D-1)l$ that places $b-Ny$ in $K^B$.

Companions

THEOREM 2: the optimal $x(b)$ satisfies $\sum_{i>m}x_i=\sum_iy_i\le D-1$. THEOREM 4 (with the bound corrected, see below): if an optimal $y$ of (4) has $\prod_i(y_i+1)>D$, the optimum of (4) is not unique.

Significance

THEOREM 1 reduces integer programming, for right-hand sides far from the boundary of an optimal cone, to a shortest-path-type problem over a group of order $D$: the integer optimum is determined by the LP optimum and a periodic correction, and it can be computed in time polynomial in $n$ and $D$ (THEOREM 3, not formalized here). It explains why rounding fails while a structured correction succeeds, and it is the starting point of the corner-polyhedron and cutting-plane theory built on the group relaxation. THEOREM 2 bounds how far the integer optimum lies from a lattice point of $\mathfrak L_B$, an early proximity result.

The results are classical and proved in the paper; none of them has a machine-checked proof that this mission is aware of. The mission produces a Lean statement and proof of the asymptotic theorem, together with reusable statements about the group $\mathbb Z^m/B\mathbb Z^m$ and the zero-sum shortening argument of the LEMMA.

Difficulty

The decomposition $z_2\le z_1+\varphi$ is a direct computation. The difficulty is the converse: an optimal solution $y$ of the group problem extends to an integer point $x_B=B^{-1}(b-Ny)$, but nothing in (4) forces $x_B\ge0$. Optimality of $y$ alone does not bound $y$: an optimal solution may carry zero-cost cycles of arbitrary length, and then $b-Ny$ can leave the cone $K^B$. The theorem therefore depends on choosing the right optimal solution of (4), one whose total size is bounded by the group order, and on relating that combinatorial bound to the Euclidean geometry of the cone.

Formalization scope

• The basis is fixed: $B$ is an integer $m\times m$ matrix and $N$ an integer $m\times n$ matrix; column $j$ of $N$ ($0$-based) is the paper's $\alpha_{m+1+j}$. The costs $c_B$, $c_N$ are real.
• The standing assumptions of pp. 260–262 are hypotheses of the goal: $\det B\neq0$; every unit vector of $\mathbb Z^m$ is a column of $B$ or of $N$ (the paper's $A=(A',I)$, without which P2 can be infeasible); all relative costs $c^*_i\le0$ ($B$ is optimal, without which (4) is unbounded).
• P2's variables are natural numbers (integer and nonnegative). The group problem is written as "$b-Ny\in B\mathbb Z^m$", which is equivalent to $\sum\bar\alpha_{i+m}y_i=\bar b$.
• Optimal values are greatest elements of the sets of objective values, never suprema; the goal asserts that they are attained.
• The norm in $l$ and in $K^B(d)$ is Euclidean. $K^B(d)$ is the set of points whose closed ball of radius $d$ lies in $K^B$. $l=0$ when $n=0$.
• In part (3) of the goal, $y^B(b)$ ranges over optimal solutions of (4) with $\sum_iy_i\le D-1$, the solutions the paper's LEMMA and dynamic program produce.
• THEOREM 4 is stated with the hypothesis $\prod(y_i+1)>D$: the printed $>D-1$ is false ($m=n=1$, $B=(2)$, $N=(1)$, $c=(2,0)$, $b=1$ has the unique optimum $y=1$ with $\prod(y_i+1)=2$).
• A trivializing formalization is ruled out: the goal assumes none of the LEMMA, the inequality (7), integrality of $B^{-1}(b-Ny)$ or the norm bound, and it states the existence of the optima instead of assuming them.
• Not in scope: the operation counts of THEOREM 3 and the recursion (8), which need a machine model the paper does not define.

Needed infrastructure: the cardinality of $\mathbb Z^m/B\mathbb Z^m$ (available in Mathlib through determinants of basis changes), a zero-sum/pigeonhole argument in a finite abelian group, the simplex optimality criterion (published), and elementary Euclidean estimates. The group-theoretic lemmas are reusable for other group-relaxation and proximity missions. Proofs of the milestones, alternative arguments and the extension to the open-ball reading of $K^B(d)$ are welcome.

Selected references

• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53(2):260–265, 1965. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bull. Amer. Math. Soc. 64:275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2:451–558, 1969. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Math. Programming 3:23–85, 1972.
• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer, 2007 (simplex optimality criterion). https://doi.org/10.1007/978-3-540-30717-4

Motivation

The maximal multi-commodity flow problem asks how much total flow several commodities, each travelling from its own sources to its own sinks, can send through a network whose arcs have shared capacities. It arises in communication and transportation planning: Kalaba and Juncosa's 1956 study of communication networks (Management Science 3(1)) leads to linear programs of this form. For a single commodity the problem has a clean combinatorial theory: the max-flow min-cut theorem of Ford and Fulkerson (1956, doi:10.4153/CJM-1956-045-5) and the labeling algorithm. With several commodities both fail: the min-cut equality is false, and simplex bases are no longer triangular.

In a short note received in October 1957 and published in Management Science in 1958, L. R. Ford Jr. and D. R. Fulkerson proposed a way to solve the multi-commodity problem with the simplex method anyway (doi:10.1287/mnsc.1040.0269, reprinted 2004). They use the arc-chain formulation, which has one variable per chain from a source to a sink of a commodity. That formulation has far too many variables to write down. The note's point is that the simplex method never needs them explicitly. The "pricing" step (finding a variable to enter the basis, or recognizing that none exists) can be carried out by one shortest-chain computation per commodity, with the simplex multipliers as arc lengths.

Timeline. Ford (1956, RAND P-923) gave the label-correcting shortest-chain procedure the note uses. Ford and Fulkerson (1958) applied it to price the columns of the arc-chain program. Dantzig and Wolfe (1960) generalized the idea into the decomposition principle. Gilmore and Gomory (1961) applied the same pattern to the cutting-stock problem, and it is now called column generation.

Setting

A network has finitely many nodes $P_1,\dots,P_N$ and arcs $A_1,\dots,A_m$. Each arc $A_r$ joins two nodes, has a capacity $b_r$, and is either directed (traversable one way only) or undirected (traversable both ways). There are finitely many commodities; commodity $k$ has a set of sources $S_k$ and a set of sinks $T_k$.

A chain from $u$ to $w$ is the arc set of a path $u = v_0, v_1, \dots, v_p = w$ with distinct nodes, each arc traversable from $v_{i-1}$ to $v_i$. A commodity chain of $k$ is a chain from a node of $S_k$ to a node of $T_k$. List the commodity chains, for all commodities, as $C_1,\dots,C_n$, and let $A = (a_{rs})$ be the incidence matrix: $a_{rs} = 1$ if $C_s$ contains $A_r$ and $0$ otherwise. With $x_s$ the flow along $C_s$ and $x_{n+r}$ the slack of arc $A_r$, the problem is the linear program

$$\text{maximize } \sum_{s=1}^{n} x_s \quad\text{subject to}\quad \sum_{s=1}^{n} a_{rs}x_s + x_{n+r} = b_r,\qquad x_1,\dots,x_{n+m} \ge 0. \tag{2–3}$$

A basis is a set of $m$ columns of $[A \mid I]$ forming an invertible matrix $B = (b_{rj})$. Its simplex multipliers $\alpha_1,\dots,\alpha_m$ satisfy, for every basic column $j$,

$$\sum_{r=1}^{m} \alpha_r b_{rj} = \begin{cases} 1 & j \le n,\\ 0 & j > n.\end{cases} \tag{4}$$

Read as arc lengths, the $\alpha_r$ give each chain $C_s$ the length $\sum_r \alpha_r a_{rs}$. The labeling process for a source set $S$ starts with labels $\pi_i = 0$ on $S$ and $\pi_i = \infty$ elsewhere. It repeatedly finds an arc traversable from $P_i$ to $P_j$ with $\pi_i + l_{ij} < \pi_j$ and replaces $\pi_j$ by $\pi_i + l_{ij}$. In Lean the labels are lab : V → WithTop ℝ, the multipliers are α : E → ℝ, and all objects live in the namespace FordFulkerson58.ArcChain.

Formalization targets

Goal: the shortest-chain pricing test (§3, pp. 1779–1780)

Let $B$ be a basis with basic feasible solution $z$ and multipliers $\alpha \ge 0$. Then:

$$\begin{aligned} &\text{(a) for every commodity, every run of the labeling process with lengths } \alpha \text{ is finite;}\\ &\text{(b) if all final sink labels are } \ge 1, \text{ then } \textstyle\sum_s x_s \le \sum_s z_s \text{ for every feasible } x;\\ &\text{(c) if a final sink label } \pi_t < 1, \text{ some non-basic chain column to } t \text{ has length } \pi_t \text{ and } 1 - \textstyle\sum_r \alpha_r a_{rs} > 0. \end{aligned}$$

Milestones (§3, the labeling process and the test)

1. Termination of the labeling process for non-negative lengths (p. 1780).
2. Final labels are shortest-chain lengths from $S$; the smallest label on $T$ is the $S$-to-$T$ distance (p. 1780).
3. The trace-back: a chain of tight arcs from $S$ to every labeled node, of length its label (p. 1780).
4. If $\alpha \ge 0$ and every commodity chain has length $\ge 1$, the basis is optimal (p. 1779).

Further items state the remarks of §3–§4: a negative multiplier lets a slack enter; the slack basis is a feasible start; dominated chains can be ignored; limited supplies reduce to the same problem by adding new directed source arcs; Figure 2 is the incidence matrix of Figure 1; with negative lengths the labeling process may not terminate.

Significance

The result. The test turns a linear program with exponentially many columns into one whose pricing step costs one shortest-path computation per commodity. Only the $m \times m$ basis is ever stored. This is the first instance of column generation, which now underlies solvers for multi-commodity flow, cutting stock, vehicle routing, crew scheduling and many other set-partitioning models, typically inside branch-and-price. Part (a) together with milestones 2–3 also gives the correctness of Ford's label-correcting algorithm with non-negative lengths, started from a source set and with any order of arc scans.

Formalizing it. The results are classical and proved in the paper's informal style. None of them is formalized: the platform has no arc-chain LP, no column pricing, and no formal statement of Ford's label-correcting process. The general LP facts are on the platform (the simplex optimality criterion and weak duality, both proved) and are included as references. This mission adds the network-specific layer: chains as arc sets of simple paths, the labeling process as a relation on labelings, and the link from final labels to reduced costs. One sentence of the paper is corrected. The trace-back "eventually" reaches $S$ only along some backward path, because zero-length cycles can trap a naive backward search, and milestone 3 states the true version.

Difficulty

The obvious argument for termination says each step lowers a label and there are finitely many chains. It fails: labels are lengths of walks, not chains, and with zero-length arcs (multipliers are often $0$) there are infinitely many walks. Termination needs the finiteness of the set of walk lengths below a bound, not positivity. The correctness of the final labels needs both properties of the labeling: it is produced by the process (so every label is the length of a walk from $S$), and it is terminal. A terminal labeling alone, such as all labels $0$, is not a distance labeling. Finally, the optimality claim is an LP statement about the full, never-enumerated column set. It must be derived from (4), $\alpha \ge 0$ and the shortest-chain lengths, with the chain columns indexed abstractly.

Formalization scope

Nodes, arcs and commodities are finite types V, E, ι. Each arc has tail, head, a per-arc directed flag and a capacity b : E → ℝ; commodities have src snk : ι → Finset V. Parallel arcs and mixed directed/undirected networks are allowed. No sign of the capacities and no disjointness of sources and sinks is assumed, except 0 ≤ b in the zero-flow item, where it is disclosed. Chains are arc sets of simple paths. The null chain at a source is a chain, so sources have distance $0$. Columns are pairs (commodity, chain), so one arc set used by two commodities gives two columns. The columns of $[A \mid I]$ are indexed by Col N ⊕ E. A basis is β : E → Col N ⊕ E with IsUnit (basisMatrix N β).det; its basic feasible solution and multipliers (4) are hypotheses about this β. Labels are in WithTop ℝ with ⊤ for $\infty$. Shortest-chain lengths are finite infima (Finset.inf), equal to ⊤ when there is no chain. The process scans arcs, not node pairs, which handles parallel arcs and the undirected case $l_{ij} = l_{ji}$.

The standing assumption of §3 ("a stage has been reached in the computation where all $\alpha_r$ are non-negative", p. 1779) is a hypothesis of the goal and of milestones 1–4. Milestones 1–3 are stated for any non-negative length function. The paper has no numbered theorems; every milestone is an unnumbered sentence of §3, cited by page and position.

A trivializing formalization is ruled out: the goal does not assume shortest-chain lengths, the trace-back, or any reduced-cost fact beyond (4). Statements about final labels require labelings that are both reachable from the initial labels and terminal, and part (a) shows such labelings exist.

Reusable beyond this mission: the chain and labeling layer (a label-correcting shortest-path algorithm from a source set over mixed networks) and the arc-chain LP. Contributions to the LP layer, which can import the referenced Matoušek–Gärtner results after reindexing, are particularly welcome.

Selected references

• L. R. Ford Jr., D. R. Fulkerson, A suggested computation for maximal multi-commodity network flows, Management Science 5(1):97–101, 1958; reprinted Management Science 50(12S):1778–1780, 2004. https://doi.org/10.1287/mnsc.1040.0269
• L. R. Ford Jr., D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
• L. R. Ford Jr., Network Flow Theory, RAND Corporation Paper P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• G. B. Dantzig, P. Wolfe, Decomposition principle for linear programs, Operations Research 8(1):101–111, 1960. https://doi.org/10.1287/opre.8.1.101
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6):849–859, 1961. https://doi.org/10.1287/opre.9.6.849
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007. https://doi.org/10.1007/978-3-540-30717-4

Motivation

Dynamic traffic assignment models how commuters choose routes and departure times when travel times change over the day. In the model of Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41 (1993)), the time to traverse a path is built recursively from arc exit-time functions: a vehicle that enters an arc at time $t$ leaves it at time $\tau(t)$. The equilibrium conditions of that model refer to the inverses of these functions, so the model is only well defined when every arc exit-time function is invertible.

Invertibility has a direct traffic meaning. A strictly increasing exit time is the first-in-first-out (FIFO) property: a vehicle that enters later cannot leave earlier, so no overtaking occurs on the arc. Whether a given delay model respects FIFO was an active question in the early 1990s, because several delay functions used in practice violate it for some inflow patterns.

Timeline:

• 1969. Vickrey's bottleneck model introduces deterministic queueing at a single bottleneck (Vickrey 1969).
• 1986. Ben-Akiva and De Palma show (Trans. Sci. 20 (1986)), for uniform entry rates and deterministic queueing delays, that it is not possible to "arrive earlier by departing later".
• 1993. Friesz et al. prove (Theorem 1, p. 185) that for every linear arc delay $D = \alpha x + \beta$ the exit time is strictly increasing, extending the 1986 result to all continuous entry-rate patterns (remark, p. 186).

Setting

Consider one arc. Vehicles enter it at the entry rate $u(t) \ge 0$, a continuous function of time $t \ge 0$; the first vehicle enters at time $0$. For an exit-time function $\tau$, the arc volume at time $t \ge 0$ is the inflow mass of the vehicles that entered during $[0,t]$ and have not left by time $t$:

$$x(t) = \int_{\{s \in [0,t]\,:\,\tau(s) > t\}} u(s)\,ds .$$

The linear delay function (18) of the paper is

$$D(t) = \alpha\, x(t) + \beta, \qquad \alpha, \beta > 0,$$

a fixed free-flow travel time $\beta$ plus a queueing time determined by the service rate $1/\alpha$. The exit time is entry time plus delay, so $\tau$ is pinned by the exit-time equation

$$\tau(t) = t + \alpha\, x(t) + \beta \qquad (t \ge 0).$$

The equation is implicit: $\tau$ appears on the right through the volume. The proof partitions time at $t_0 = 0$, $t_{n+1} = \tau(t_n)$; in particular $t_1 = \tau(0) = \beta$ is the exit time of the first vehicle. In Lean these objects are linearDelay, arcVolume, IsLinearExitTime and tSeq in FrieszDUE.FIFO.

Formalization targets

Goal: Theorem 1 (p. 185)

For $\alpha, \beta > 0$ and a nonnegative continuous entry rate $u$, every $\tau$ satisfying the exit-time equation is strictly increasing on $[0, \infty)$:

$$0 \le s < t \implies \tau(s) < \tau(t),$$

and hence injective there, so $\tau^{-1}$ exists.

Milestones

1. Lemma 1 (19): for a differentiable invertible $f$, $[f^{-1}]'(z) = 1/f'[f^{-1}(z)]$.
2. First interval (21)–(24): $t_1 = \beta$; on $[0, t_1]$, $x(t) = \int_0^t u$, $\tau(t) = t + \alpha\int_0^t u + \beta$, and $\tau' = 1 + \alpha u > 0$.
3. Second interval (25)–(28): on $[t_1, t_2]$, $\tau(t) = t + \alpha\int_{\tau^{-1}(t)}^t u + \beta$ and $\tau'(t) = \alpha u(t) + 1/(1 + \alpha u[\tau^{-1}(t)]) > \alpha u(t)$.
4. Induction (29)–(34): the same representation and $\tau'(t) > \alpha u(t)$ on every $[t_{n+1}, t_{n+2}]$, with $\tau$ strictly increasing there.
5. Covering: $t_{n+1} - t_n \ge \beta$ and $\mathbb R_+ = \bigcup_{n \ge 0}[t_n, t_{n+1}]$.

A supporting, non-milestone item states that the exit-time equation has a solution for every admissible $u$.

Significance

The result makes the path exit-time functions of the dynamic network model invertible whenever the arc delays are linear in volume. That invertibility is what allows the path costs, and through them the variational inequality of Theorem 2 of the same paper, to be written down. In traffic terms it certifies that linear volume-based delays never let a later entrant overtake an earlier one, whatever the continuous inflow profile.

The theorem is proved in the paper. As far as is known it has no machine-checked proof. The mission produces one, together with a formal model of a single arc whose exit time is defined implicitly through the volume, which is reusable for other delay functions and for FIFO questions in dynamic traffic assignment.

Difficulty

The obvious argument differentiates $\tau(t) = t + \alpha x(t) + \beta$ and bounds the outflow rate. But the volume can only be written as $\int_{\tau^{-1}(t)}^t u$ once $\tau$ is known to be invertible, which is the conclusion. The paper breaks the circularity by working forward in time: on $[t_n, t_{n+1}]$ the volume depends only on $\tau$ restricted to the earlier interval, whose invertibility is already established. A formal proof must make this forward dependence rigorous for an exit time given only by the implicit equation, handle one-sided derivatives at the junctions $t_n$, where $\tau$ is generally not differentiable, and show that the junctions do not accumulate.

Formalization scope

Time is real; the entry rate is a function $u : \mathbb R \to \mathbb R$ with $u(t) \ge 0$ and $u$ continuous on $[0, \infty)$. Both are added hypotheses: Theorem 1 names none, nonnegativity is implicit in "entry rate", and the remark after the proof covers "all continuous entry rate patterns". Integrals are Lebesgue integrals. Monotonicity is claimed on $[0,\infty)$ only, the entry times that the equation constrains. Derivative claims in the milestones are taken within the closed interval $[t_n, t_{n+1}]$. The paper's separate pieces $\tau_k$ are one global function here, so the junction identities (27), (30), (33) are automatic. Lemma 1 adds the hypothesis $f'[f^{-1}(z)] \ne 0$, without which it is false.

The exit time τ is pinned by the implicit equation τ(t) = t + αx(t) + β, where x(t) is the inflow mass of vehicles that entered by time t and have not exited by time t; no monotonicity or invertibility of τ is assumed. A formalization that defined the volume through $\tau^{-1}$ or assumed $\tau$ monotone would assume the conclusion and is ruled out.

The development needs one-sided derivatives of parametric integrals, the inverse-function derivative on an interval, and a forward induction over the partition. Contributions of proofs for any milestone, of the existence item, and of a uniqueness result for the exit-time equation are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• M. Ben-Akiva and A. de Palma, Some circumstances in which vehicles will reach their destinations earlier by starting later: revisited, Transportation Science 20(1):52–55, 1986. https://doi.org/10.1287/trsc.20.1.52
• M. Ben-Akiva, A. de Palma and P. Kanaroglou, Dynamic model of peak period traffic congestion with elastic arrival rates, Transportation Science 20(3):164–181, 1986. https://doi.org/10.1287/trsc.20.3.164
• W. S. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–261, 1969. https://www.jstor.org/stable/1823678

Motivation

Many decisions in operations research and machine learning minimize an expected cost $\mathbb E^{P}[h(x,\xi)]$ whose distribution $P$ is unknown and is seen only through $N$ independent samples. The sample-average approximation replaces $P$ by the empirical distribution and is known to produce decisions with poor out-of-sample performance when $N$ is small. Distributionally robust optimization instead minimizes the worst-case expected cost over a set of distributions that are plausible given the data. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) take this set to be a ball in the Wasserstein metric around the empirical distribution, and show that such balls deliver both finite-sample certificates and asymptotic consistency. This mission formalizes the statistical half of that paper: Section 3 and Appendix A.

A data-driven method should, at a minimum, be consistent: as the sample grows, its optimal value and decisions should approach those of the true problem. For Wasserstein balls this requires a measure concentration inequality for empirical distributions in the Wasserstein metric, which was supplied by Fournier and Guillin (PTRF 2015). The paper combines that inequality with the Kantorovich–Rubinstein duality and the Borel–Cantelli lemma.

Setting

Let $E$ be $\mathbb R^m$ with an arbitrary norm $\|\cdot\|$ and its Borel $\sigma$-algebra. A decision $x$ ranges over a feasible set $X\subseteq\mathbb R^n$; the random vector $\xi$ has distribution $P$, supported on the uncertainty set $\Xi\subseteq E$; the loss is $h:\mathbb R^n\times E\to\mathbb R$. The true problem (1) has optimal value

$$J^\star=\inf_{x\in X}\mathbb E^P[h(x,\xi)].$$

The Wasserstein distance between distributions $Q_1,Q_2$ with finite first moment is

$$d_W(Q_1,Q_2)=\inf\Big\{\int\|\xi_1-\xi_2\|\,\Pi(d\xi_1,d\xi_2):\ \Pi\text{ a coupling of }Q_1\text{ and }Q_2\Big\}.$$

Given samples $\hat\xi_1,\dots,\hat\xi_N$ drawn independently from $P$ (joint law $P^N$, and $P^\infty$ for the infinite sequence), the empirical distribution is $\widehat P_N=\frac1N\sum_{i=1}^N\delta_{\hat\xi_i}$, and the Wasserstein ball $\mathbb B_\varepsilon(\widehat P_N)$ is the set of distributions $Q$ on $\Xi$ with $d_W(\widehat P_N,Q)\le\varepsilon$. The distributionally robust program (5) has optimal value

$$\widehat J_N=\inf_{x\in X}\ \sup_{Q\in\mathbb B_\varepsilon(\widehat P_N)}\mathbb E^Q[h(x,\xi)],$$

and an optimizer of it is written $\widehat x_N$.

The light-tail condition (Assumption 3.3) asks for an exponent $a>1$ with $A=\mathbb E^P[\exp(\|\xi\|^a)]<\infty$. Under it, and for $m\ne2$, Theorem 3.4 (Fournier–Guillin) gives constants $c_1,c_2>0$ with

$$P^N\{d_W(P,\widehat P_N)\ge\varepsilon\}\le\begin{cases}c_1e^{-c_2N\varepsilon^{\max\{m,2\}}},&\varepsilon\le1,\\ c_1e^{-c_2N\varepsilon^{a}},&\varepsilon>1,\end{cases}\tag{7}$$

for all $N\ge1$, $\varepsilon>0$. Solving the right-hand side $=\beta$ for $\varepsilon$ gives the radius

$$\varepsilon_N(\beta)=\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/\max\{m,2\}}\text{ if }N\ge\frac{\log(c_1\beta^{-1})}{c_2},\qquad\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/a}\text{ otherwise}.\tag{8}$$

Formalization targets

Goal: Theorem 3.6 (asymptotic consistency)

Let $\beta_N\in(0,1)$ with $\sum_N\beta_N<\infty$ and $\varepsilon_N(\beta_N)\to0$, and use the radius $\varepsilon_N(\beta_N)$ in (5).

(i) If $h(x,\cdot)$ is upper semicontinuous on $\Xi$ and $|h(x,\xi)|\le L(1+\|\xi\|)$ on $X\times\Xi$, then $P^\infty$-almost surely

$$\widehat J_N\ge J^\star\ \text{for all large }N\quad\text{and}\quad\widehat J_N\to J^\star.$$

(ii) If moreover $X$ is closed and $h(\cdot,\xi)$ is lower semicontinuous on $X$, then $P^\infty$-almost surely every accumulation point of $(\widehat x_N)$ is an optimal solution of (1).

Milestones

1. Theorem 3.5 (finite sample guarantee). For fixed $N\ge1$ and $\beta\in(0,1)$, with radius $\varepsilon_N(\beta)$,

$$P^N\big\{\mathbb E^P[h(\widehat x_N,\xi)]>\widehat J_N\big\}\le\beta.$$

2. Lemma A.1. An upper semicontinuous $h$ on $\Xi$ with $h(\xi)\le L(1+\|\xi\|)$ is the pointwise limit on $\Xi$ of a non-increasing sequence of Lipschitz functions.
3. Lemma 3.7 (convergence of distributions). Any data-dependent $\widehat Q_N\in\mathbb B_{\varepsilon_N(\beta_N)}(\widehat P_N)$ satisfies

$$P^\infty\Big\{\lim_{N\to\infty}d_W(P,\widehat Q_N)=0\Big\}=1.$$

Theorem 3.2 (Kantorovich–Rubinstein duality, $d_W(Q_1,Q_2)=\sup\{\int f\,dQ_1-\int f\,dQ_2:\ f\ 1\text{-Lipschitz}\}$), which the proof of (i) uses, enters as a reference item: the open platform theorem WassersteinDRO.Duality.kantorovich_rubinstein, stated on the whole space for all Borel probability measures. It is not a milestone, because that statement is more general than the paper's version on $\mathcal M(\Xi)$ (the two agree for distributions in $\mathcal M(\Xi)$ by extending Lipschitz functions from $\Xi$ to the whole space).

A companion item, Example 1 (1), records that upper semicontinuity cannot be dropped in (i): for $\Xi=[0,1]$, $P=\delta_0$ and $h=\mathbb 1_{(0,1]}(\xi)$ one has $J^\star=0$ but $\widehat J_N\ge1$ for every radius $\varepsilon>0$.

Significance

Theorem 3.5 makes the robust optimal value an upper confidence bound on the out-of-sample cost of the robust decision. Theorem 3.6 shows that this protection does not cost consistency: with radii shrinking at a rate governed by summable confidence levels, such as $\beta_N=e^{-\sqrt N}$, both the certificate and the decisions converge to their true counterparts. Together they are the statistical justification for the Wasserstein ambiguity sets that the rest of the paper reformulates as finite convex programs, and they are cited as the reference consistency results for Wasserstein distributionally robust optimization.

All results here are proved in the paper. None of them, nor the Fournier–Guillin inequality, is formalized on Prove2Me or in Mathlib to our knowledge. The mission adds machine-checked versions of the finite-sample and consistency statements, a monotone Lipschitz approximation lemma for semicontinuous functions with linear growth (useful wherever Lipschitz duality has to be extended to semicontinuous integrands), and a convergence lemma for measures in shrinking Wasserstein balls.

Difficulty

The obvious argument for (i) bounds the worst-case expectation by the true expectation plus a Lipschitz constant times the radius. That fails, because $h$ is only upper semicontinuous in $\xi$, not Lipschitz, and has no Lipschitz constant to multiply. The expectations of a merely semicontinuous loss must be controlled uniformly over every distribution in the ball, including data-dependent worst-case distributions, and the almost-sure convergence of the empirical distribution alone does not give this. Example 1 of the paper shows that each regularity hypothesis is needed. On the formal side, the Wasserstein distance is an infimum over couplings on a Polish space; even its triangle inequality (gluing of couplings) and the Kantorovich–Rubinstein duality are substantial.

Formalization scope

$E$ is a finite-dimensional real normed space with its Borel $\sigma$-algebra (BorelSpace), and $m$ is its dimension; decisions live in EuclideanSpace ℝ (Fin n). The definitions $d_W$ (type $p=1$), $\widehat P_N$, $\mathbb B_\varepsilon(\widehat P_N)$, $\mathbb E^Q$ and the worst-case expectation are the published WassersteinDRO.Duality definitions. The optimal values $J^\star$ and $\widehat J_N$ are extended reals. Standing conventions and pinned hypotheses:

• "Supported on $\Xi$" is $P(\Xi^c)=0$; $\Xi$ is neither closed nor convex in general. The samples lie in $\Xi$ almost surely, and optimizers and ball selections are required only for samples in $\Xi$.
• The constants $c_1,c_2>0$ enter as any constants for which (7) holds, which is how (8) is defined from Theorem 3.4. The theorem of Fournier and Guillin is not part of this mission, and $m\ne2$ is assumed because (7) and (8) are printed only for $m\ne2$.
• The loss is real-valued. In Theorem 3.5 it is assumed $P$-integrable on $X$, because the worst-case expectation counts only distributions under which the loss is integrable. In Theorem 3.6 the linear growth bound makes this automatic.
• Probabilities "at least $1-\beta$" are stated as bounds on the outer measure of the failure event, and "$P^\infty$-almost surely" as an almost-everywhere statement for the product measure on sequences.
• The paper's "$\widehat J_N\downarrow J^\star$" is stated as eventual domination $\widehat J_N\ge J^\star$ plus convergence, which is what its proof establishes; monotonicity in $N$ is not claimed.

A statement in which (7) could not hold for any constants would make the goal vacuous. The concentration inequality is satisfiable (for instance by a Dirac distribution with any constants), and $\varepsilon_N(\beta)$ is defined by the paper's formula, not chosen freely.

Welcome contributions: the triangle inequality and Kantorovich–Rubinstein duality for $d_W$, the Borel–Cantelli step for product measures, Lemma A.1, and the Fatou argument of (ii).

Selected references

• P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018); source version arXiv:1505.05116v3. https://arxiv.org/abs/1505.05116v3
• N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• L. V. Kantorovich and G. S. Rubinstein, On a space of totally additive functions, Vestnik Leningrad. Univ. 13 (1958).
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• D. Bertsimas, V. Gupta and N. Kallus, Robust sample average approximation, Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445