Operations Research

Motivation

PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with $m$ jobs each taking two values, $2^m$ deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.

Setting

A project network has events $0,1,\dots,n$ with $n\ge1$, origin $0$ and terminal $n$. Its arcs are ordered pairs $(i,j)$ with $i<j$, at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes $1,\dots,n$; his node $i$ is event $i-1$ here. The bundle $B_j$ of an event $j$ is the set of arcs entering $j$, and $\operatorname{pred}(j)$ the set of their tails; the origin's bundle is empty.

For arc lengths $t$, let $\ell_i(t)$ be the length of a longest (critical) path from the origin to $i$; equivalently $\ell_0=0$ and $\ell_j=\max_{i\in\operatorname{pred}(j)}(\ell_i+t_{ij})$.

The lengths of the arcs of each bundle $B_j$ form a random vector with a finite distribution: a finite set $S_j$ of bundle vectors $v$, where $v_i$ is the length of arc $(i,j)$, with probabilities $p_j(v)\ge 0$ summing to $1$. Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment $\omega=(\omega_j)_j$ of one bundle vector per event has probability $p(\omega)=\prod_j p_j(\omega_j)$. Three numbers are attached to each event $i$:

1. the expected critical path length $e_i=\sum_\omega p(\omega)\,\ell_i(t(\omega))$;
2. the mean-length estimate $g_i=\ell_i(\bar t)$, where $\bar t_{ij}=\sum_{v\in S_j}p_j(v)\,v_i$ is the expected length of arc $(i,j)$;
3. Fulkerson's numbers $f_0=0$ and, for $j\neq0$,

$$f_j=\sum_{v\in S_j}p_j(v)\,\max_{i\in\operatorname{pred}(j)}\bigl(f_i+v_i\bigr).$$

Formalization targets

Goal: (4.4)

$$g_i\;\le\;f_i\;\le\;e_i\qquad\text{for every event } i .$$

Milestones

In the order of Fulkerson's induction (pp. 10–12):

1. the recursion for $\ell$ computes the greatest path length (§3, (3.6), and the display on p. 11);
2. $\ell_i(t)$ depends only on the arcs of the bundles $B_0,\dots,B_i$ (p. 6);
3. (4.8): $\max_{i\in\operatorname{pred}(j)}(f_i+\bar t_{ij})\le f_j$;
4. (4.5)/(4.9): if $g_k\le f_k$ for all $k<j$, then $g_j\le f_j$;
5. (4.13): $\sum_{v\in S_j}p_j(v)\max_{i\in\operatorname{pred}(j)}(e_i+v_i)\le e_j$;
6. (4.10)/(4.14): if $f_k\le e_k$ for all $k<j$, then $f_j\le e_j$.

Companion statements

• $g_i\le e_i$ under an arbitrary joint distribution of all arc lengths (remark, p. 12).
• Fig. 4.2: with correlated bundles, $e_3=g_3=1$ but $f_3=5/4$, so (4.4) fails without bundle independence.
• (4.17): an independent example with $g_3=f_3=1<e_3=5/4$.
• Fig. 4.1: explicit values $g_4=3/2$, $f_2=1/2$, $f_3=9/8$, $f_4=55/32$, and $f_i=e_i$.

Significance

The chain (4.4) says that the classical PERT estimate $g$ never overstates the expected project duration, and that the numbers $f$ are a lower bound at least as tight. The $f$ computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation $e$ requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality $g\le e$ survives arbitrary dependence.

The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.

Difficulty

The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: $f_j$ averages over the bundle entering $j$, while $e_j$ averages over assignments to every bundle. Taking expectations in $\ell_j=\max_i(\ell_i+t_{ij})$ yields $e_j\ge\max_i(e_i+\bar t_{ij})$, which gives the weaker bound $g\le e$. Fig. 4.2 shows that $f\le e$ can fail when the bundles are dependent. In Lean, $e$ is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for $f$ is the central technical difficulty.

Formalization scope

• Network: the published CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires $n\ge1$. Fulkerson's numbering condition "$i\le j$" on p. 3 is read as the strict $i<j$ (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).
• Critical path length: the published CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of $0$ or $-\infty$.
• Distributions: finite, given as data (a support Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to $1$, for every event including the origin). Bundle vectors are functions on all events, and coordinates outside $\operatorname{pred}(j)$ are never read.
• Arc lengths are arbitrary reals. §3 assumes nonnegative lengths, but its footnote on p. 4 states that nonnegativity "is not essential in this or the following section"; the statements are given in this more general form.
• No trivialization: $e_i$ is the sum over every assignment of bundle vectors, weighted by the product probability (3.5). It is not defined by a recursion, and the goal assumes none of the milestones. $f$ at node $j$ uses only the distribution of the bundle of $j$.

Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.

Selected references

• D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks, RAND Memorandum RM-3075-PR, March 1962; published in Operations Research 10(6):808–817, 1962. doi:10.1287/opre.10.6.808
• J. E. Kelley Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proceedings of the Eastern Joint Computer Conference, 1959, pp. 160–173. doi:10.1145/1460299.1460318
• D. G. Malcolm, J. H. Roseboom, C. E. Clark and W. Fazar, Application of a Technique for Research and Development Program Evaluation, Operations Research 7(5):646–669, 1959. doi:10.1287/opre.7.5.646

Motivation

A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).

This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.

Setting

There are $n$ tasks, indexed $i=0,\ldots,n-1$. Task $i$ has a nonnegative length $l_i$, a nonnegative preferred starting time $a_i$, and an actual starting time $s_i$. Once started, it occupies the one processor until $s_i+l_i$. Each start must be nonnegative. For the fixed-order problem, task $i$ must finish before task $i+1$ starts, so $s_i+l_i\le s_{i+1}$. This permits idle time when the inequality is strict. The task's discrepancy is $|s_i-a_i|$; because its preferred completion is $a_i+l_i$, this is also its absolute completion-time discrepancy. The total discrepancy is

$$\operatorname{cost}_n(s)=\sum_{i=0}^{n-1}|s_i-a_i|.$$

A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule $S_n$ for the first $n$ tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).

For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.

Formalization targets

Fixed-order optimality

The main target is the paper's Theorem 2. For all nonnegative task data and every $n$, the actual schedule $S_n$ produced by the block-shifting algorithm is feasible and satisfies

$$\operatorname{cost}_n(S_n)\le\operatorname{cost}_n(s) \qquad\text{for every feasible fixed-order schedule }s.$$

This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of $S_n$ has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).

Equal-length schedules

The companion target is Theorem 3. If every task has a common length $L\ge0$ and the preferred starts are indexed so that $a_i\le a_{i+1}$, then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:

$$\exists s\;\bigl[ \operatorname{cost}_n(s)\le\operatorname{cost}_n(t) \text{ for every feasible }t \bigr] \quad\text{with }s_i\le s_{i+1}\text{ whenever }i+1<n.$$

The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).

Significance

Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).

The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.

Difficulty

Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).

Formalization scope

The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below $n$ count. Task $i$ in Lean is the paper's $T_{i+1}$. Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's $l_i\ge0$ model.

The algorithm is defined by its stated insertion and single-block-shift operations. Defining $S_n$ as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.

Selected references

• Michael R. Garey, Robert E. Tarjan, and Gordon T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2), 330–348, 1988. DOI: 10.1287/moor.13.2.330.

Why priority queues with cheap decrease key matter

Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with $n$ vertices and $m$ edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in $O(\log n)$ worst-case time.

Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take $O(\log n)$ amortized time and every other operation, decrease key included, takes $O(1)$ amortized time. This brings Dijkstra's algorithm to $O(n \log n + m)$ and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.

Setting

An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank $r(x)$ of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.

Linking two trees with roots $x$ and $y$ makes $y$ the last child of $x$ if the key of $x$ is smaller, and otherwise makes $x$ the last child of $y$; the root that becomes a child is unmarked. The operations act as follows:

• make heap adds an empty heap; find min acts on a nonempty heap and returns a root of minimum key; insert adds a one-node tree for a new item; meld concatenates two root lists.
• delete min removes a root $x$ of minimum key, adds the children of $x$ to the roots, then repeats the linking step, "find any two trees whose roots have the same rank, and link them", in any order, until all root ranks are distinct.
• decrease key $(\Delta, i, h)$, $\Delta \ge 0$, lowers the key of $i$ and, if the node $x$ of $i$ is not a root, cuts $x$ from its parent, making its subtree a new tree. delete $(i, h)$ cuts $x$ the same way, destroys it and adds its children to the roots; a minimum root is deleted as in delete min.
• After every cut of a child of $p$, if $p$ is not a root it is marked if unmarked and cut from its own parent if marked: a cascading cut, which may repeat upwards.

The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential $\Phi$ of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of $\Phi$.

Formalization targets

Goal: THEOREM 1 (p. 604)

There is an absolute constant $C > 0$ such that for every sequence of $T$ operations started from no heaps, with $n_t$ the number of items in the heap that operation $t$ acts on, just before it acts,

$$\sum_{t<T} \mathrm{cost}_t \;\le\; \sum_{t<T} b_t, \qquad b_t = \begin{cases} C(\log_2 n_t + 1) & \text{delete min or delete},\\ C & \text{otherwise.}\end{cases}$$

The paper's wording is "the total time is at most the total amortized time, where the amortized time is $O(\log n)$ for each delete min or delete operation and $O(1)$ for each of the other operations"; the goal pins the $O(\cdot)$ to one constant and does not name the potential.

Milestones

1. LEMMA 1: the $i$th child of a node, in linking order, has rank at least $i - 2$.
2. $F_{k+2} \ge \varphi^k$, with $F_k$ the Fibonacci numbers and $\varphi = (1+\sqrt5)/2$.
3. COROLLARY 1: a node of rank $k$ has at least $F_{k+2} \ge \varphi^k$ descendants, itself included.
4. A node of rank $k$ in an $n$-item heap has $\varphi^k \le n$, hence $k \le \log n / \log\varphi$.
5. make heap, find min and meld leave $\Phi$ unchanged; insert raises it by one.
6. delete min raises $\Phi$ by at most $\log n / \log \varphi$ minus the number of linking steps.
7. decrease key raises $\Phi$ by at most three minus the number of cascading cuts.
8. From no heaps, the total amortized time bounds the total actual time.

Significance

THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in $O(n\log n + m)$, all-pairs shortest paths and the assignment problem in $O(n^2 \log n + nm)$, and minimum spanning trees in $O(m\,\beta(m,n))$.

The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.

Difficulty

The obvious argument, that every tree is a binomial tree and so every rank is at most $\log_2 n$, fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank $k$ can be left with only $k+1$ descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.

Formalization scope

All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.

Logarithms in the goal are base 2 (footnote 1, p. 600), with a $+1$ so that one-item heaps have positive budget. The paper's constant "$\le 1.4404 \log n$" on p. 604 is a rounding slip ($1/\log_2 \varphi = 1.44042\ldots$); milestones use the exact $\log_\varphi n$.

The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, $C$ is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.

Selected references

• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, J. ACM 34(3):596–615, 1987. https://doi.org/10.1145/28869.28874
• J. Vuillemin, A data structure for manipulating priority queues, Comm. ACM 21(4):309–315, 1978. https://doi.org/10.1145/359460.359478
• R. E. Tarjan, Amortized computational complexity, SIAM J. Algebraic Discrete Methods 6(2):306–318, 1985. https://doi.org/10.1137/0606031
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1:269–271, 1959. https://doi.org/10.1007/BF01386390

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

Motivation

In data-driven stochastic optimization a decision maker knows the distribution of an uncertain parameter $\xi$ only through $N$ samples $\hat\xi_1,\dots,\hat\xi_N$. Wasserstein distributionally robust optimization hedges against this ignorance by evaluating a loss $\ell$ under the worst distribution in a ball, measured in the Wasserstein metric, around the empirical distribution of the samples. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) showed that for piecewise concave losses the worst-case expectation is the optimal value of a finite convex program (their Theorem 4.2), which made the approach computationally practical.

Knowing the worst-case value is often not enough. Stress tests of a candidate decision require the extremal distributions themselves: the distributions inside the ball that (nearly) achieve the worst case. Section 4.2 of the paper answers this question. Its Theorem 4.4 shows that the worst case is approached by discrete distributions with at most $NK$ atoms, read off from near-optimal solutions of a second finite convex program, and its Example 2 shows that a worst-case distribution need not exist at all. This mission formalizes that section. The source is the arXiv preprint version 3 (13 June 2017); all numbering below refers to it.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbb R^m$), equipped with its Borel $\sigma$-algebra. Linear functionals $z$ on $E$ act by $\langle z,\xi\rangle$, and the dual norm is $\|z\|_* = \sup_{\|\xi\|\le 1}\langle z,\xi\rangle$. Extended reals $\overline{\mathbb R} = [-\infty,+\infty]$ follow the paper's conventions $0\cdot\infty = 0/0 = 0$ and $\infty - \infty = \infty$.

• Samples and empirical distribution. $\hat\xi_1,\dots,\hat\xi_N$ lie in a set $\Xi\subseteq E$, and $\widehat{\mathbb P}_N = \frac1N\sum_i\delta_{\hat\xi_i}$.
• Wasserstein ball. $d_W(\mathbb Q_1,\mathbb Q_2)$ is the infimum of $\int\|\xi_1-\xi_2\|\,\Pi(d\xi_1,d\xi_2)$ over couplings $\Pi$ of $\mathbb Q_1$ and $\mathbb Q_2$, and $\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ is the set of probability distributions supported on $\Xi$ within distance $\varepsilon$ of $\widehat{\mathbb P}_N$.
• Loss. $\ell(\xi) = \max_{k\le K}\ell_k(\xi)$ for measurable pieces $\ell_k : E\to\overline{\mathbb R}$, and $\mathbb E^{\mathbb Q}[\ell(\xi)] = \mathbb E^{\mathbb Q}[\max\{\ell,0\}] + \mathbb E^{\mathbb Q}[\min\{\ell,0\}]$.
• Worst-case expectation (10). $\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)]$.
• Assumption 4.1. $\Xi$ is convex and closed; every $-\ell_k$ is proper, convex and lower semicontinuous; and no $\ell_k$ is identically $-\infty$ on $\Xi$.
• Program (13). Over weights $\alpha_{ik}\ge 0$ and displacements $q_{ik}\in E$,

$$\sup_{\alpha_{ik},q_{ik}}\ \frac1N\sum_{i=1}^N\sum_{k=1}^K\alpha_{ik}\,\ell_k\Big(\hat\xi_i-\frac{q_{ik}}{\alpha_{ik}}\Big)\quad\text{s.t.}\quad\frac1N\sum_{i,k}\|q_{ik}\|\le\varepsilon,\ \ \sum_k\alpha_{ik}=1,\ \ \hat\xi_i-\frac{q_{ik}}{\alpha_{ik}}\in\Xi .$$

When $\alpha_{ik}=0$ the last constraint forces $q_{ik}=0$ and the $ik$-th objective term is $0$.

• Candidate distributions. $\mathbb Q = \frac1N\sum_{i,k}\alpha_{ik}\,\delta_{\xi_{ik}}$ with $\xi_{ik} = \hat\xi_i - q_{ik}/\alpha_{ik}$.

Formalization targets

Goal: Theorem 4.4 (worst-case distributions)

Under Assumption 4.1 and for every $\varepsilon\ge 0$,

$$\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)] = \text{optimal value of (13)},$$

and for every feasible sequence $(\alpha_{ik}(r),q_{ik}(r))_r$ of (13) whose objective values converge to that optimal value, the distributions $\mathbb Q_r$ lie in $\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ and

$$\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)] = \lim_{r\to\infty}\mathbb E^{\mathbb Q_r}[\ell(\xi)] = \lim_{r\to\infty}\frac1N\sum_{i,k}\alpha_{ik}(r)\,\ell(\xi_{ik}(r)).$$

The limits may be $+\infty$; no finiteness is assumed.

Milestones, in the order of the proof

The proof starts from (10) = (12f) (proof of Theorem 4.2, p. 13), which is posed in mission I of this series, Wasserstein Worst-Case Expectations as Finite Convex Programs, and is not restated here; it will be linked as a milestone once that mission is live.

1. Lemma 4.5: $\inf_z\langle z,q-\alpha\hat\xi\rangle+\alpha f^*(z)$ is the extended perspective of $q\mapsto -f(\hat\xi-q)$ for proper, convex, lower semicontinuous $f$.
2. (14d)–(14f): the $ik$-th dual term equals $\alpha\ell_k(\hat\xi-q/\alpha)-\chi_\Xi(\hat\xi-q/\alpha)$ under the extended-arithmetic conventions.
3. (12f) = (13), the first part of the proof of Theorem 4.4.
4. $\mathbb Q_r\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ for every feasible point of (13).
5. $\mathbb E^{\mathbb Q_r}[\ell(\xi)]$ equals $\frac1N\sum_{i,k}\alpha_{ik}\ell(\xi_{ik})$ and is at least the objective of (13) for every feasible point.

Companion results

Corollary 4.6: if $\Xi$ is compact or $K=1$, the sequence has an accumulation point that defines a worst-case distribution. Example 2: for $\Xi=\mathbb R$, $N=1$, $\hat\xi_1=0$, $\ell=\max\{0,\xi-1\}$, the worst-case expectation is $\varepsilon$ and, for $\varepsilon>0$, is attained by no distribution in the ball.

Significance

Theorem 4.4 turns the abstract supremum over an infinite-dimensional ball of distributions into a finite-dimensional convex program whose near-optimal solutions are near-worst-case distributions. The atoms $\xi_{ik}$ sit within total weighted distance $\sum_{i,k}\alpha_{ik}\|\xi_{ik}-\hat\xi_i\|\le N\varepsilon$ of the data, and they may lie off the data, which distinguishes Wasserstein balls from ambiguity sets based on the total variation distance or the Kullback–Leibler divergence. Example 2 marks the boundary: the theorem cannot be upgraded to the existence of a maximizer in general, while Corollary 4.6 names two cases where it can.

The results are proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a precise account of the extended-arithmetic conventions the paper relies on ($0\cdot\infty=0$, $q/0\notin E$, $\infty-\infty=\infty$), each of which is made explicit in the definitions, and a reusable Lean treatment of extended-valued conjugates and perspective functions on a normed space with an arbitrary norm.

Difficulty

The first claim goes through Lagrangian duality for program (12f), whose constraints involve conjugates that may take the value $+\infty$; the strong duality and the minimax interchange (14c) must be justified for extended-valued convex functions, not just finite ones. Lemma 4.5 needs the Fenchel–Moreau theorem $f^{**}=f$ for proper, convex, lower semicontinuous $\overline{\mathbb R}$-valued functions on a finite-dimensional normed space, together with its degenerate case $\alpha=0$. The second claim is a squeeze argument, but it rests on computing an extended expectation of an $\overline{\mathbb R}$-valued function under a discrete measure and on an explicit coupling for the Wasserstein distance. A tempting shortcut, attaining the supremum by a limit distribution, fails: Example 2 shows the maximizing atoms can escape to infinity.

Formalization scope

• The space is a finite-dimensional real normed space E with [BorelSpace E]; the dual space is StrongDual ℝ E, and the dual norm is the operator norm. All values are in EReal.
• The Wasserstein distance, the ball (6) and $\widehat{\mathbb P}_N$ are the published WassersteinDRO.Duality.wassersteinDistance, ambiguitySet (with $p=1$) and empiricalDistribution.
• The extended expectation is the published DupacovaWets.Consistency.expect; it integrates the positive and negative parts separately and returns $+\infty$ when the positive part is infinite; there is no integrability guard, so a distribution with infinite expected loss pushes (10) to $+\infty$ as in the paper.
• Program values are infima or suprema over feasibility predicates, so an empty feasible set gives $\pm\infty$, never a junk $0$. Program (13) encodes $\alpha_{ik}=0$ by the clauses "$q_{ik}=0$" and "objective term $=0$" (p. 14).
• Standing assumptions carried as hypotheses: $N\ge1$, $K\ge1$, $\hat\xi_i\in\Xi$ (§2), measurability of each $\ell_k$ (p. 11).
• A trivializing formalization is ruled out: dropping the clause $\alpha_{ik}=0\Rightarrow q_{ik}=0$ or the hypothesis $\hat\xi_i\in\Xi$ would change program (13) or make the ball empty, and both are kept explicitly.
• The objects shared with mission I (extended expectation, worst-case expectation, conjugate, Assumption 4.1, program (12f)) are restated verbatim in this mission's namespace; they will be merged with mission I's copies. Contributions to the convex-analysis groundwork (extended-valued Fenchel–Moreau, perspective functions) are welcome and reusable beyond this mission.

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. Version formalized: arXiv:1505.05116v3.
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (Propositions 1.6.1 and 5.5.4, used in the proofs).
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Motivation

A postal route that must traverse every street and return to its starting point is a Chinese postman tour. In a street network, crossings are nodes, streets are edges, and the cost of a route is the sum of the lengths of the streets it traverses, counted with repetition. The practical question is which streets must be repeated, and how often. Edmonds and Johnson's 1973 paper separates that question from constructing the resulting tour: choose the repeated edges first, then find an Euler tour of the resulting multigraph. This mission concerns their reduction of the first question to a minimum-weight matching of the odd-degree nodes.

The reduction matters because it turns a route problem with arbitrary repeated edge traversals into a finite pairing problem. The graph of odd nodes is complete, with the weight of a pair given by its shortest-path distance in the original network. A matching chooses which odd nodes to pair, and paths realizing those pairs identify edges to repeat. The paper also explains why overlapping paths can be replaced so that no edge needs to be repeated by this construction more than once (§3, pp. 92–93).

Setting

A graph $G=(N,E)$ has finite node and edge sets. Each edge has two distinct endpoints. Different edges may join the same pair of nodes, so parallel streets remain distinct. The graph is connected when every pair of nodes is joined by an edge-labelled walk. A walk records both its node sequence and its edge sequence; a tour is a closed walk. An Euler tour uses each edge exactly once, while a postman tour uses each edge at least once. Edge lengths $c_e$ are real and nonnegative, as in §2, p. 89.

The degree of $v$ is the number of named edges meeting it. Let $T$ be the set of nodes of odd degree. For every edge $e$, let $x_e\in\mathbb N$ be the number of additional traversals. The parity equations require a nonnegative integer $w_v$ at each node such that

$$\sum_{e\ni v}x_e=2w_v+b_v,\qquad b_v=\begin{cases}1&v\in T,\\0&v\notin T.\end{cases}$$

Their objective is $z(x)=\sum_{e\in E}c_ex_e$. These are the paper's (3.1)–(3.4), with natural-number values encoding integrality and nonnegativity (§3, pp. 90–91). The equations express the even-degree condition after adding $x_e$ copies of each original edge.

For nodes $u,v$, write $d(u,v)$ for the length of a shortest path in $G$. This distance is backed by an attaining edge-simple path and is a lower bound on the length of every walk from $u$ to $v$. Connectivity and nonnegative edge lengths make that specification meaningful. Let $G_p$ be the complete graph on $T$, with edge $\{u,v\}$ of weight $d(u,v)$. A 1-matching $M$ pairs every node of $T$ with exactly one distinct node. Its length is $L(M)=\sum_{\{u,v\}\in M}d(u,v)$, equivalently half the sum of $d(v,f(v))$ over $v\in T$ for the pairing involution $f$ (§3, p. 92).

Formalization targets

Odd-node matching reduction

The goal asserts the existence of a 1-matching of the odd nodes and both directions of the cost comparison:

$$\forall M\;\exists x\text{ satisfying the parity equations}:\quad x_e\in\{0,1\},\ z(x)\le L(M),$$ $$\forall x\text{ satisfying the parity equations}\;\exists M:\quad L(M)\le z(x).$$

The existence conclusion and these comparisons identify the two attained minimum values. The goal does not prescribe a particular matching algorithm. Its supporting targets are the paper's uncrossing of overlapping shortest paths, parity of their union, reduction of multiplicities to zero or one, and decomposition of a parity solution into paths between odd nodes (§3, pp. 92–93).

Postman-tour reduction

The companion target relates a tour's edge counts to the parity equations. A postman tour traverses edge $e$ exactly $1+x_e$ times, and its length is

$$\sum_{e\in E}c_e(1+x_e) =\sum_{e\in E}c_e+z(x).$$

Conversely, positive integer edge counts with even incidence at every node can be ordered into a postman tour of a connected graph. The supporting Euler theorem handles a connected even multigraph (§2, p. 89).

Significance

The matching result characterizes the optimal additional cost of an undirected postman route. It says that the parity correction can be chosen from paths pairing odd nodes, and that no feasible choice of repeated traversals can beat the best such pairing. The companion identifies how that correction becomes an actual tour. The distinction is useful when one wants to change the matching method while retaining the mathematical guarantee on route length.

A formal development would provide a reusable account of finite multigraph walks whose edge names distinguish parallel edges, of shortest-path distances with explicit attainment, and of parity subgraphs decomposed into odd-to-odd paths and even-degree residual tours. These pieces support later formal work on route inspection, $T$-joins, and matching-based graph algorithms. The paper proves the mathematical result. The exact multigraph and cost statements drafted here are open formalization targets; the local prior-art search found related results for simple graphs and metric traveling-salesman models, but no published statement with this paper's objects and conclusion.

Difficulty

A direct shortest-path construction can assign the same original edge to two matching pairs. Simply setting $x_e=1$ for the union then loses the additivity of path lengths, and setting $x_e=2$ loses the promised zero-or-one form. The uncrossing claim must control both the matching cost and the number of times each original edge appears. In the converse direction, an arbitrary feasible $x$ may contain repeated edges and cycles; the argument must account for these without assuming that every supported edge belongs to a path between odd nodes (§3, pp. 92–93).

Formalization scope

Lean uses the published EdmondsMatching65.Polyhedron.Graph for $G$: finite node and edge types and an endpoint map into unordered node pairs. A proof field excludes loops; distinct edge names may have identical endpoints. Walks use lists of nodes and named edges with zero-based indices, and the one-node, zero-edge walk is allowed. Edge multiplicities and parity witnesses are natural numbers. Costs and shortest-path lengths are real. The distance relation requires both an attaining edge-simple path and a bound against all walks; no real infimum over a possibly empty family is used. The matching is a fixed-point-free involution on the odd nodes, extended by the identity elsewhere, and each pair contributes half of its two directed distance terms.

The goal assumes a connected graph and nonnegative edge lengths, exactly as the section does. The tour-only results require a nonempty node type because a list-based tour must have a starting node; without it an edgeless graph on no nodes would satisfy connectivity and even degree vacuously. The path-decomposition statement permits unused even-degree cycles. No independent set of “odd nodes” is accepted as input: it is computed from the degree of $G$.

The development needs finite multigraph incidence, edge-labelled walks, shortest paths, finite matchings, parity arithmetic, path uncrossing, and Euler tours. Proofs or useful intermediate results for these objects are welcome, including results applicable to multigraphs beyond the postman setting.

Selected references

• Jack Edmonds and Ellis L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973), 88–124. DOI: 10.1007/BF01580113.

Motivation

A decision maker who must minimize an expected cost $\mathbb E^{\mathbb P}[h(x,\xi)]$ rarely knows the distribution $\mathbb P$ of the uncertain parameter $\xi$; usually only $N$ samples $\hat\xi_1,\dots,\hat\xi_N$ are available. Replacing $\mathbb P$ by the empirical distribution (sample average approximation) tends to produce decisions that perform poorly out of sample when $N$ is small. Distributionally robust optimization instead minimizes the worst 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 that set to be a ball in the Wasserstein metric around the empirical distribution. Such balls give finite-sample and asymptotic guarantees, but each evaluation of the robust objective is an optimization over infinitely many probability distributions. Section 4.1 of the paper shows that, for a large class of losses, this inner problem is a finite convex program. That result, Theorem 4.2, is the subject of this mission.

Timeline. Wasserstein ambiguity sets for portfolio selection were proposed by Pflug and Wozabal (2007); before this paper, robust problems over such sets were solved with global optimization algorithms (Pflug and Pichler 2014). Strong duality for conic linear and moment problems (Shapiro 2001) underlies the reduction. Mohajerin Esfahani and Kuhn (preprint 2015, journal 2018) proved the convex reduction for piecewise concave losses; Gao and Kleywegt (arXiv:1604.02199) and Blanchet and Murthy (arXiv:1604.01446) proved strong duality for general transport costs in 2016.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbb R^m$) and its Borel σ-algebra. Its dual norm is $\|z\|_* = \sup_{\|\xi\|\le 1}\langle z,\xi\rangle$, where $\langle z,\xi\rangle$ is the value of the linear functional $z$ at $\xi$. Let $\Xi\subseteq E$ be the support set and $\hat\xi_1,\dots,\hat\xi_N\in\Xi$ the samples, with empirical distribution $\widehat{\mathbb P}_N=\frac1N\sum_{i=1}^N\delta_{\hat\xi_i}$.

The 1-Wasserstein distance between two distributions is the least transport cost $\int\|\xi-\xi'\|\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ with the given marginals. The Wasserstein ball $\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ is the set of probability distributions on $\Xi$ within distance $\varepsilon\ge 0$ of $\widehat{\mathbb P}_N$.

The loss is a pointwise maximum $\ell(\xi)=\max_{k\le K}\ell_k(\xi)$ of measurable functions $\ell_k:E\to\overline{\mathbb R}=\mathbb R\cup\{\pm\infty\}$. Its expectation is $\mathbb E^{\mathbb Q}[\ell]=\mathbb E^{\mathbb Q}[\max\{\ell,0\}]+\mathbb E^{\mathbb Q}[\min\{\ell,0\}]$ with $\infty-\infty=\infty$. The worst-case expectation is

$$\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)].\tag{10}$$

The conjugate of $f:E\to\overline{\mathbb R}$ is $f^*(z)=\sup_\xi\langle z,\xi\rangle-f(\xi)$, the characteristic function $\chi_\Xi$ is $0$ on $\Xi$ and $+\infty$ off it, and the support function is $\sigma_\Xi(z)=\sup_{\xi\in\Xi}\langle z,\xi\rangle$. Assumption 4.1 requires $\Xi$ to be convex and closed, each $-\ell_k$ to be proper, convex and lower semicontinuous, and no $\ell_k$ to be identically $-\infty$ on $\Xi$.

Formalization targets

Goal: Theorem 4.2 (convex reduction)

Under Assumption 4.1, for every $\varepsilon\ge0$, (10) equals

$$\inf_{\lambda,s_i,z_{ik},\nu_{ik}}\ \lambda\varepsilon+\frac1N\sum_{i=1}^N s_i\quad\text{s.t.}\quad [-\ell_k]^*(z_{ik}-\nu_{ik})+\sigma_\Xi(\nu_{ik})-\langle z_{ik},\hat\xi_i\rangle\le s_i,\ \ \|z_{ik}\|_*\le\lambda\quad\forall i,k.\tag{11}$$

Milestones, in the order of the paper's proof

1. (12a)–(12c). Without any convexity, (10) is at most the value of (12c): $\inf\{\lambda\varepsilon+\frac1N\sum_i s_i:\ \sup_{\xi\in\Xi}(\ell(\xi)-\lambda\|\xi-\hat\xi_i\|)\le s_i,\ \lambda\ge0\}$.
2. Corollary 4.3. Without Assumption 4.1, (10) is at most the value of (12f), the program with constraints $[-\ell_k+\chi_\Xi]^*(z_{ik})-\langle z_{ik},\hat\xi_i\rangle\le s_i$ and $\|z_{ik}\|_*\le\lambda$.
3. (12a) is an equality for $\varepsilon>0$ under Assumption 4.1.
4. The case $\varepsilon=0$. (10) is the sample average $\frac1N\sum_i\ell(\hat\xi_i)$, the objective of (12b) converges to it as $\lambda\to\infty$, and (12a) is again an equality.
5. (12e) is an equality. For each constraint, $\sup_{\xi\in\Xi}(\ell_k(\xi)-\lambda\|\xi-\hat\xi_i\|)=\min_{\|z\|_*\le\lambda}\sup_{\xi\in\Xi}(\ell_k(\xi)-\langle z,\xi-\hat\xi_i\rangle)$.
6. (10) equals (12f) under Assumption 4.1.
7. (12f) equals (11) under Assumption 4.1, as optimal values.

Significance

Theorem 4.2 is what makes Wasserstein distributionally robust optimization computable. Once the worst-case expectation is a convex program in $(\lambda,s,z,\nu)$, minimizing over the decision $x$ becomes one larger convex program. Section 5 of the paper derives linear and conic programs from it for piecewise affine losses, uncertainty quantification and two-stage problems. Theorem 4.4 of the same paper (mission II of this series) builds worst-case distributions from the same program. Corollary 4.3 gives a conservative convex bound for losses that are not piecewise concave.

The result is proved on paper; no machine-checked proof of it is known. A formal development needs a working theory of extended-valued conjugates, support functions and inf-convolution in a normed space, Kantorovich-type couplings of an empirical measure, and a minimax theorem over a compact dual ball. Each of these is reusable well beyond this paper.

Difficulty

The weak inequality, (10) $\le$ (12f), is the elementary direction: integrate a pointwise bound against a near-optimal coupling. The difficulty lies in the two equalities. Equality in (12a) is strong duality for an infinite-dimensional moment problem whose loss may take the values $\pm\infty$ and may be unbounded on an unbounded $\Xi$. A Slater point exists only for $\varepsilon>0$, so $\varepsilon=0$ needs a separate limit argument. The equality (12f) $=$ (11) is subtle as well. The conjugate of $-\ell_k+\chi_\Xi$ is only the closure of the inf-convolution of $[-\ell_k]^*$ and $\sigma_\Xi$, so the two constraint sets differ and only the optimal values agree. The paper's sentence "cl$[f]\le 0$ iff $f\le0$" is false pointwise and cannot be formalized as written.

Formalization scope

• Space. $E$ is a finite-dimensional real normed space with its Borel σ-algebra. The pairing $\langle z,\xi\rangle$ is application of a continuous linear functional $z$, and $\|z\|_*$ is the operator norm. These choices keep the paper's arbitrary norm; §5 of the paper uses the 1- and ∞-norms.
• Extended reals. Values are in EReal. Mathlib's EReal has $\top+\bot=\bot$, whereas the paper has $\infty-\infty=\infty$, so the expectation treats an infinite positive part separately, and $[-\ell_k+\chi_\Xi]^*(z)$ is written as $\sup_{\xi\in\Xi}(\langle z,\xi\rangle+\ell_k(\xi))$, with no addition at all. The one EReal sum, $[-\ell_k]^*+\sigma_\Xi$ in (11), never meets $\top+\bot$ under Assumption 4.1.
• Programs. Each optimal value is an infimum over a feasibility predicate with real epigraph variables, so an infeasible program has value $+\infty$.
• Ball. The ball is the published WassersteinDRO.Duality.ambiguitySet with $p=1$ around empiricalDistribution. Its condition $\mathbb Q(\Xi^{\mathrm c})=0$ encodes $\mathbb Q\in\mathcal M(\Xi)$. The finite first moment is automatic at finite distance from $\widehat{\mathbb P}_N$.
• Standing assumptions. Every statement carries $N\ge1$, $K\ge1$, $\hat\xi_i\in\Xi$ (§2, p. 5) and measurability of each $\ell_k$ (p. 11). The radius condition is $\varepsilon\ge0$, or $\varepsilon>0$ in milestone 3.
• Assumption 4.1. Convexity of $-\ell_k$ is stated through its real epigraph, because ConvexOn cannot take an EReal codomain.
• Not trivializable. The statements cannot be made vacuous by an empty ball, because the samples lie in $\Xi$. They cannot be trivialized by a junk expectation either: the expectation is not guarded by integrability, so a distribution with infinite expected loss makes (10) infinite, exactly as in the paper.

Welcome contributions are reusable lemmas on EReal-valued conjugates and support functions, the decomposition of a coupling with an empirical marginal into conditional distributions, the dual-norm identity $\max_{\|z\|_*\le\lambda}\langle z,v\rangle=\lambda\|v\|$, and a Sion-type minimax theorem.

Selected references

• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, arXiv:1505.05116v3, 2017; Math. Program. 171 (2018) 115–166. https://arxiv.org/abs/1505.05116v3
• A. Shapiro, On duality theory of conic linear problems, in M. A. Goberna, M. A. López (eds.), Semi-Infinite Programming, Kluwer, 2001.
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 2010 (Theorem 11.23(a), p. 493).
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (Proposition 5.5.4).
• G. Ch. Pflug, A. Pichler, Multistage Stochastic Optimization, Springer, 2014.
• G. Ch. Pflug, D. Wozabal, Ambiguity in portfolio selection, Quantitative Finance 7 (2007) 435–442.
• R. Gao, A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, arXiv:1604.01446, 2016. https://arxiv.org/abs/1604.01446