The OR Formalization Drive

Motivation

Assortment optimization asks which products a retailer should offer when customers choose among the offered products according to a probabilistic choice model, so as to maximize expected revenue. Under the nested logit model the products are grouped into nests: a customer first picks a nest, then a product inside it. The model is the standard relaxation of the independence of irrelevant alternatives property of the multinomial logit, and it is used throughout revenue management and transportation demand modelling.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) classify the complexity of the assortment problem under four variants of the nested logit model, according to whether the dissimilarity parameters are at most one and whether a customer who picks a nest always buys there. The problem is NP-hard as soon as some dissimilarity parameter exceeds one (their Theorem 5), and also when the nests have positive no-purchase weights (Theorem 8), so for the general variant approximation is the realistic aim. §6.2 of the paper gives an approximation scheme for the most general variant: for any $\delta > 1$ it restricts each nest to a short list of candidate assortments indexed by the powers of $\delta$, solves a small linear program, and loses at most a factor $\delta^{2\bar\gamma+1}$ of the optimal revenue. This mission formalizes the guarantee behind that scheme, Theorem 12.

Setting

There are nests $M$ and products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$; the products are ordered so that $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$, and $v_0 \ge 0$ is the weight of leaving without choosing a nest. Offering $S_i \subseteq N$ in nest $i$ gives

$$V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j \in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \qquad \Pi(S_1, \dots, S_m) = \frac{\sum_i V_i(S_i)^{\gamma_i} R_i(S_i)}{v_0 + \sum_i V_i(S_i)^{\gamma_i}}.$$

The optimal expected revenue $Z^* = \max \Pi$ is the optimal value of the linear program (3): minimize $x$ subject to $v_0 x \ge \sum_i y_i$ and $y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - x)$ for every nest $i$ and every $S_i \subseteq N$. Problem (4) keeps the second family of constraints only for a candidate collection of assortments in each nest.

Let $\bar\gamma = \max_i \gamma_i$, assumed $> 1$ throughout §6, and fix $\delta > 1$. Put $v^L_i = v_{i0} + \min_j v_{ij}$, $v^U_i = v_{i0} + \sum_j v_{ij}$, and let $l^L_i$, $l^U_i$ be the least integers with $\delta^{l} \ge v^L_i$, $\delta^l \ge v^U_i$. For each level $l = l^L_i, \dots, l^U_i$, problem (15) maximizes $\sum_{j \in S} r_{ij} v_{ij}$ over the assortments with $\delta^{l-1} \le V_i(S) \le \delta^l$; its value is $\hat G_{il}$. An assortment $\hat S_{il}$ is feasible for (15) and satisfies $\delta \sum_{j \in \hat S_{il}} r_{ij} v_{ij} \ge \hat G_{il}$. The candidate collection of nest $i$ is $\{\hat S_{il} : l = l^L_i, \dots, l^U_i\} \cup \{\emptyset\}$.

Formalization targets

Goal: Theorem 12 (p. 28)

If $(\hat x, \hat y)$ is an optimal solution of problem (4) over the candidate collections $\{\hat S_{il}\} \cup \{\emptyset\}$, then

$$\big(\delta^{2\bar\gamma+1}\hat x,\ \delta^{\bar\gamma+1}\hat y\big) \text{ is feasible for problem (3).}$$

Milestones (Appendix A.6, pp. 53–54)

1. $\hat x \ge 0$.
2. Every nonempty assortment of nest $i$ lies in some level $l^L_i \le l \le l^U_i$.
3. If $\delta^{l-1} \le a \le \delta^l$, then $a^{\gamma-1} \ge (\delta^l)^{\gamma-1}\delta^{-[\gamma-1]^+}$.
4. Under the same hypothesis, $(\delta^l)^{\gamma-1} \ge \delta^{-[1-\gamma]^+} a^{\gamma-1}$.
5. $\delta^{\bar\gamma}\delta^{-[\gamma_i-1]^+}\delta^{-[1-\gamma_i]^+} \ge 1$ and $\delta^{\bar\gamma+\gamma_i+1} \le \delta^{2\bar\gamma+1}$.
6. The scaled pair satisfies $\delta^{\bar\gamma+1}\hat y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - \delta^{2\bar\gamma+1}\hat x)$ for every nonempty $S_i$.
7. The same inequality for $S_i = \emptyset$.

Companions

• The guarantee stated after Theorem 12: with $v_0 > 0$, the assortment assembled from the candidates solving problem (5) earns at least $Z^*/\delta^{2\bar\gamma+1}$.
• Proposition 15 (p. 51): when (15) is feasible, one of the explicit assortments $\hat S(J_L, J_S)$, built from at most $q = \lceil \delta/(\delta-1)\rceil$ large and at most $q$ small products by a greedy continuous knapsack, is feasible for (15) and within a factor $\delta$ of $\hat G_{il}$.
• The count $l^U_i - l^L_i \le 1 + \log_\delta(v^U_i/v^L_i)$ (p. 28).

Significance

Theorem 12 is the analytical half of the approximation scheme. Together with the paper's Theorem 1 it shows that a linear program with $1 + m$ variables and at most $1 + m(2 + \log_\delta(v^U_i/v^L_i))$ constraints yields an assortment within a factor $\delta^{2\bar\gamma+1}$ of the optimum, for the most general variant, which is NP-hard, and Proposition 15 makes the candidate assortments computable. Letting $\delta \downarrow 1$ trades accuracy for running time, so the result is the paper's answer to how well the general problem can be approximated by this LP approach.

The result is proved in the paper; the work here is to formalize the known proof. To the best of a search of the Prove2Me library (local index and platform mirror, October 2026), no nested logit approximation result, and no knapsack lemma matching Proposition 15, has a machine-checked statement or proof. The definitions of the shared model (the instance, $V_i$, $R_i$, $\Pi$, the linear programs (3) and (4)) are common to the six missions of this series.

Difficulty

The obvious argument compares an arbitrary assortment $S_i$ with the candidate of its level and uses the candidate's constraint in (4). This fails as a direct comparison because the nest weight $V_i(\cdot)^{\gamma_i}$ enters twice with different exponents, $\gamma_i - 1$ in front of the revenue and $\gamma_i$ in front of $\hat x$, and within one level $V_i$ may vary by a factor $\delta$. When $\gamma_i > 1$ and when $\gamma_i \le 1$ the monotonicity of $t \mapsto t^{\gamma_i - 1}$ goes in opposite directions, so the losses must be tracked separately by $[\gamma_i - 1]^+$ and $[1 - \gamma_i]^+$, and they are absorbed by the common factor $\delta^{\bar\gamma}$ only because $\bar\gamma > 1$. The other half, Proposition 15, concerns a knapsack with both a lower and an upper bound on the total weight, where a feasible solution must be produced as well as a good objective value.

Formalization scope

Products are Fin n ($0, \dots, n-1$ for $1, \dots, n$), nests a finite type, powers $V^{\gamma}$ real powers, and $x/0 = 0$, which gives $R_i(\emptyset) = 0$. The shared model carries the standing assumptions of §1 with the disclosed pins $v_{ij} > 0$, $r_{ij} \ge 0$ and $\gamma_i > 0$ (the page allows $\gamma_i = 0$ and zero-weight padding products, under which its convention $0^{\gamma_i} = 0$ and its proofs fail). Every statement of the mission also assumes $n \ge 1$ (for $v^L_i$), $\bar\gamma$ is the greatest of the $\gamma_i$ (so at least one nest exists) with $\bar\gamma > 1$, and $\delta > 1$. Integer powers $\delta^l$ are zpow, and $l^L_i$, $l^U_i$ are written $\lceil \log_\delta v^L_i\rceil$, $\lceil \log_\delta v^U_i\rceil$, which equal the minima of the paper. An optimal solution of (4) is a feasible pair whose $x$ is minimal among feasible pairs. The companion guarantee adds $v_0 > 0$, the pin of Theorem 1. In Proposition 15 the capacity row of (33) includes $v_0$, correcting a printed slip, and the running-time claim is not stated.

The assortments $\hat S_{il}$ enter Theorem 12 as an arbitrary family with the two properties of p. 28; the theorem is stated for every such family. A level at which (15) has no feasible assortment imposes nothing on $\hat S_{il}$, as on the page. Requiring $\hat S_{il}$ to lie in its level unconditionally would make the hypothesis unsatisfiable for most instances and the goal vacuous; that encoding, and any goal that assumes displays (34)–(36) or the exponent bounds, is ruled out.

Contributions welcome: proofs of the real-power milestones (3)–(5), which are self-contained, of the two cases (6)–(7), and of Proposition 15, whose fractional knapsack lemma (the greedy solution of a continuous knapsack sorted by ratio is optimal) is reusable beyond this mission.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014; cited from the revised manuscript of June 18, 2013. https://doi.org/10.1287/opre.2014.1256
• A. M. Frieze, M. R. B. Clarke, Approximation algorithms for the m-dimensional 0–1 knapsack problem: worst-case and probabilistic analyses, European Journal of Operational Research 15(1), 1984. (cited on p. 50 of the paper for the continuous knapsack (33); link not verified here)
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

Motivation

Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).

Timeline:

• 1944. von Neumann and Morgenstern axiomatize expected utility. A utility is determined up to a positive affine transformation $au+b$. Nash quotes this on p. 157.
• 1950. Nash introduces the two-person bargaining problem and the axioms of Pareto efficiency, independence of irrelevant alternatives and symmetry, the solution being invariant under the choice of utility scales. He proves that they force the maximizer of the product $u_1u_2$ (doi:10.2307/1907266).
• 1953. Nash's Two-Person Cooperative Games adds the threat game that fixes the disagreement point.
• 1975. Kalai and Smorodinsky replace independence of irrelevant alternatives by monotonicity and obtain a different solution.
• 1986. Binmore, Rubinstein and Wolinsky show that the Nash solution is the limit of equilibria of alternating-offers bargaining as the time between offers vanishes.

Setting

A bargaining problem is a pair $\langle S,d\rangle$. Here $S\subseteq\mathbb R^2$ is the set of utility pairs $u=(u_1,u_2)$ the two players can reach by agreement, including lotteries over agreements. $d\in S$ is the disagreement point, the utilities of no cooperation. As in the platform goal, $S$ is compact and convex, and some $s\in S$ has $s_1>d_1$ and $s_2>d_2$ (both individuals could gain). Write $\mathcal B$ for the set of such pairs.

A bargaining solution is a map $g$ from $\mathcal B$ to $\mathbb R^2$. Nash requires:

• Selection. $g(S,d)\in S$.
• PAR (Nash's assumption 6). If $s,t\in S$ and $t$ is strictly better than $s$ for both players, then $g(S,d)\neq s$.
• IIA (assumption 7). If $S\subseteq T$ and $g(T,d)\in S$, then $g(S,d)=g(T,d)$.
• SYM (assumption 8). If $d_1=d_2$ and $S$ is symmetric in the line $u_1=u_2$, then $g(S,d)$ lies on that line.
• INV. For $L(s)=(\alpha_1s_1+\beta_1,\ \alpha_2s_2+\beta_2)$ with $\alpha_1,\alpha_2>0$, $g(L(S),L(d))=L(g(S,d))$.

The paper has no separate INV axiom. It normalizes the disagreement utility to $0$ and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.

Formalization targets

Goal

The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by Nickrobbins95 and currently Open. This mission references it and does not restate it. It asserts that there is a solution $f$ such that a solution $g$ satisfies selection, INV, SYM, IIA and PAR if and only if $g=f$, and that for every $\langle S,d\rangle\in\mathcal B$

$$f(S,d)\ge d,\qquad (s_1-d_1)(s_2-d_2)<(f_1-d_1)(f_2-d_2)\ \text{ for all } s\in S,\ s\ge d,\ s\neq f(S,d).$$

Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.

Milestones

1. On a compact convex $S\ni(0,0)$ that contains a point where both players gain, $u_1u_2$ has exactly one strict maximizer $p$ in the closed first quadrant, and $p_1,p_2>0$.
2. Multiplying the utilities by positive constants maps the maximizer to the maximizer, so $p$ may be moved to $(1,1)$.
3. If $S$ is convex and $(1,1)$ maximizes $u_1u_2$, then $u_1+u_2\le2$ on all of $S$.
4. A compact $S$ under that line lies in a square $Q_h=\{2-2h\le u_1+u_2\le2,\ |u_1-u_2|\le h\}$.
5. $(1,1)$ is the only point of $Q_h$ on the diagonal that no point of $Q_h$ strictly dominates.
6. Necessity. Under the five conditions, $g(S,d)$ is the strict maximizer of $(s_1-d_1)(s_2-d_2)$ over $S\cap\{s\ge d\}$.

Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex $(12,5)$ reached by exactly one exchange, and trade with money, where the solution gives equal money profits.

Significance

The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.

The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.

Difficulty

Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class $\mathcal B$, and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of $S$ under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality $d=0$ and $p=(1,1)$". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of $d$ inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.

Formalization scope

Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work at $d=(0,0)$, the paper's normalization. Milestone 6 has a general $d$ and the goal's encoding. Milestones 1–5 make the following readings explicit:

• "First quadrant" is the closed quadrant $u_1\ge0,\ u_2\ge0$.
• "The point where $u_1u_2$ is maximized" is the strict maximizer over $S$ in that quadrant, in the goal's form. Milestone 1 also states $p_1,p_2>0$, which follows from the point where both gain (p. 158).
• Milestone 3's hypothesis is the weak maximum $s_1s_2\le1$. Its conclusion covers every point of $S$, not only first-quadrant points.
• The square is the explicit set $Q_h$. Its compactness, convexity and literal symmetry $(a,b)\in Q_h\iff(b,a)\in Q_h$ are part of milestone 4's conclusion.
• "Satisfying assumptions (6) and (8)" in the square means lying on $u_1=u_2$ and being strictly dominated by no point of the square.

Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given $g$. It does not restate the goal: it has no existence claim and no "if and only if".

Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of $u_1u_2=0$. The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class $\mathcal B$, which is nonempty.

The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.

Related platform work treats other bargaining models. These are Rubinstein's alternating-offers game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction (ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.

Selected references

• J. F. Nash, Jr., The Bargaining Problem, Econometrica 18(2), 155–162, 1950. doi:10.2307/1907266
• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
• J. F. Nash, Jr., Two-Person Cooperative Games, Econometrica 21(1), 128–140, 1953. doi:10.2307/1906951
• E. Kalai, M. Smorodinsky, Other Solutions to Nash's Bargaining Problem, Econometrica 43(3), 513–518, 1975. doi:10.2307/1914280
• K. Binmore, A. Rubinstein, A. Wolinsky, The Nash Bargaining Solution in Economic Modelling, RAND Journal of Economics 17(2), 176–188, 1986. doi:10.2307/2555382
• M. J. Osborne, A. Rubinstein, Bargaining and Markets, Academic Press, 1990, Theorem 2.3.

Motivation

Delivering goods from one depot to many customers with a fleet of trucks is the vehicle routing problem. Dantzig and Ramser formulated it in 1959 as the "truck dispatching problem" (Management Sci. 6 (1959), doi:10.1287/mnsc.6.1.80). Five years later Clarke and Wright proposed the savings procedure (Oper. Res. 12 (1964), 568–581, doi:10.1287/opre.12.4.568): start with one truck per customer and repeatedly join two routes where joining saves the most distance, as long as the trucks can still carry the loads. On the twelve-customer example of Dantzig and Ramser it reached 290 units against their 294.

The savings procedure became the standard construction heuristic for vehicle routing. It appears in every textbook treatment of the problem, is the initial solution of many metaheuristics, and is the benchmark against which later construction methods are compared. The paper states the procedure and its bookkeeping (the half matrix, the vector $Q$, Table II) but proves nothing about it. That every run of the procedure ends, and ends in a feasible allocation, is left to the reader.

Setting

A depot $P_0$ serves customers $P_1,\dots,P_M$. The distance $d_{y,z}$ between every two points is given, and customer $P_j$ requires a load $q_j$. Trucks come in $n$ capacity classes: $x_i$ trucks of capacity $C_i$ are available, with $C_1<\dots<C_n$, and the trucks of the smallest capacity are unlimited, $x_1=\infty$ (p. 569).

A run is the ordered list of customers $P_{a_1},\dots,P_{a_k}$ served by one truck, which drives $P_0P_{a_1}\cdots P_{a_k}P_0$. Its load is $\sum_i q_{a_i}$. A state of the procedure is a list of runs; its mileage is the total length of its runs. A list of runs is an allocation if every customer lies on exactly one run, and it is feasible if each run can be given a truck of capacity at least its load without using more trucks of any class than are available.

The saving of the cell $(y:z)$ is $d_{0,y}+d_{0,z}-d_{y,z}$. The half matrix records $t_{y,z}=1$ if $P_y$ and $P_z$ are adjacent on a run, and $t_{y,0}\in\{0,1,2\}$ counts how many ends of runs lie at $P_y$. Table II counts, for each capacity level $C_i$, the runs with load above $C_i$ and the trucks with capacity above $C_i$.

The procedure starts with the runs $[P_1],\dots,[P_M]$, so $t_{y,0}=2$ for every customer. A cell $(y:z)$ is admissible if (I) $t_{y,0}>0$ and $t_{z,0}>0$; (II) $P_y$ and $P_z$ are on different runs; (III) after replacing those two runs by one run of load $Q_y+Q_z$, no column of Table II has more runs than trucks. A step links an admissible cell of maximum saving, ties broken arbitrarily, by joining the two runs end to end at $P_y$ and $P_z$. The procedure stops when no cell is admissible.

Formalization targets

Goal: correctness of the procedure

Assume symmetric distances, $C_1<\dots<C_n$, $x_1=\infty$, and that the initial one-truck-per-customer allocation passes the Table II test. Then every run of the procedure is finite whatever the tie-breaks; at every reachable state from which a link is possible a step exists; and every final state $S$ is a feasible allocation satisfying relation (A), $\sum_{z\ne y}t_{y,z}=2$ for every customer, with

$$\text{mileage}(S)=2\sum_{j=1}^M d_{0,j}-\sum_{\substack{1\le y<z\le M\\ t_{y,z}=1}}\bigl(d_{0,y}+d_{0,z}-d_{y,z}\bigr).$$

Milestones

$$\text{mileage}(\text{link}(S,y,z))=\text{mileage}(S)-(d_{0,y}+d_{0,z}-d_{y,z})\quad\text{for admissible }(y:z),$$

relation (A) at every reachable state, the permanence of links between customers, and

$$\#\{\text{runs with load}>C_i\}\le\sum_{k>i}x_k\ \ (i=1,\dots,n)\iff\text{the runs can be allocated to trucks},$$

which together give feasibility of every reachable state. Two further milestones: when $C_n\ge\sum_j q_j$ and the distances are a metric, the optimum equals the traveling salesman optimum (p. 569); and on the data of Table I every run of the procedure ends with total distance 290.

Significance

The goal is the specification the paper's procedure meets: it always terminates, never gets stuck, and outputs routes the fleet can actually drive, with the mileage the half-matrix bookkeeping predicts. The equivalence of the Table II test with truck feasibility is the reason the procedure can check capacities by counting columns instead of solving an assignment problem; it is a nested-class instance of Hall's marriage condition and is reusable for any routing or bin-assignment problem with ordered vehicle classes.

None of these statements is formalized anywhere, and the paper does not prove them. The paper makes no claim of optimality ("near-optimal", p. 568, is not quantified), and the mission does not either. A formal model of the procedure as a nondeterministic transition system is a base on which later results about savings heuristics (worst-case ratios, parallel and sequential variants) can be stated.

Difficulty

The obvious argument for termination, "each link removes a run", needs the invariant that every reachable state is a partition of the customers into runs; the procedure manipulates ordered lists and reverses runs, so the invariant must be carried through every step. Feasibility is not preserved by an arbitrary link but only by one that passes condition (III), and turning the column test into an actual assignment of runs to trucks is a matching argument that fails without both $x_1=\infty$ and the ordering of the capacities. Because ties are broken arbitrarily, every statement must hold for all runs of a nondeterministic procedure, not for one canonical execution. The worked example requires following every tie-break.

Formalization scope

Points are Fin (M+1) with depot 0, and a run's length is SupplyChainTheory.routeCost from the referenced module SupplyChainTheory_vrp. Capacity class i : Fin (n+1) is the paper's $C_{i+1}$; availabilities are in ℕ∞; loads and capacities are real. A state is a list of runs, each an ordered list of customers; the matrix $t$ and the vector $Q$ are computed from the state. The procedure is a step relation, and every invariant is stated for reachable states. Termination is Acc of the step relation at the initial state.

Choices committed to:

• distances are arbitrary real, symmetric numbers (the half matrix, p. 573); no nonnegativity or triangle inequality is assumed in the goal, and savings may be negative;
• every run: ties are free, as the paper suggests choosing randomly;
• reachable states: invariants are not claimed for arbitrary lists of runs;
• Table II is read cumulatively: column "Over $C_i$" compares runs with load $>C_i$ against all trucks of capacity $>C_i$, as the printed Tables II, IV and VI show;
• $x_1=\infty$ and $C_1<\dots<C_n$ are hypotheses; $q_j\le C_n$ is not separately assumed, since it follows from the initial Table II test;
• the initial one-truck-per-customer allocation is assumed feasible (p. 572);
• the metric hypotheses enter only the traveling-salesman milestone.

A correctness claim only about final states, without termination and progress, would hold for a procedure with no moves; a step relation with a fixed tie-break would prove less than the paper; invariants for arbitrary states are false; and a mileage identity for an arbitrary partition says nothing about the procedure's output. None of these is the target.

Not formalized: the informal $C_1\ll\sum q_j$, the shadow-cost reading of p. 571, the decomposition savings (2)–(5) of the general scheme, the load-splitting reduction of pp. 572–573, the Dantzig–Ramser methods, and the empirical comparisons and appendices.

Contributions welcome: proofs of the milestones, in particular the Table II equivalence, which needs a Hall-type argument for nested classes, and a decision procedure for the worked example.

Selected references

• G. Clarke and J. W. Wright, Scheduling of vehicles from a central depot to a number of delivery points, Operations Research 12(4) (1964), 568–581. https://doi.org/10.1287/opre.12.4.568
• G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6(1) (1959), 80–91. https://doi.org/10.1287/mnsc.6.1.80
• P. Hall, On representatives of subsets, Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26

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

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

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

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