Optimization

Why deteriorating jobs need a scheduling rule

On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.

The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.

Jobs, schedules, and cost

There are $N$ jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule $\pi$ is a permutation of the jobs: $\pi(k)$ is the job processed in position $k$. The paper labels positions and jobs from $1$ to $N$; the Lean development labels them from $0$ to $N-1$. The identity schedule $\pi_0$ processes jobs in label order.

For job $i$, $X_i$ is its random initial processing requirement, $\alpha_i$ its deterministic growth rate, and $c_i$ its waiting cost rate. If the job starts at time $t$, its actual processing time is $Y_i(t)=X_i+\alpha_i t$. Deterioration stops once processing starts. Write $S_k(\pi)$ for the time at which the first $k$ scheduled jobs have all finished. The model sets $S_0(\pi)=0$ and

$$S_{k+1}(\pi)=S_k(\pi)+X_{\pi(k+1)}+\alpha_{\pi(k+1)}S_k(\pi)$$

in the paper's one-based position notation. Thus the completion time of the job in position $k$ is $S_k(\pi)$. Its cost is its own rate $c_{\pi(k)}$ times that completion time, giving

$$C(\pi)=\sum_{k=1}^{N}c_{\pi(k)}S_k(\pi).$$

All of these are random quantities until an expectation is taken. Equation (2) of the paper writes $S_k$ as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into $C(\pi_0)$. Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in $C$ from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.

Formalization targets

The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,

$$\frac{E(X_1)}{\alpha_1}<\cdots<\frac{E(X_N)}{\alpha_N}, \qquad \frac{\alpha_1}{c_1(1+\alpha_1)} <\cdots< \frac{\alpha_N}{c_N(1+\alpha_N)},$$

then, for every permutation $\sigma$,

$$E[C(\pi_0)]\le E[C(\sigma)].$$

The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.

The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.

What the result establishes

The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only $E(X_i)/\alpha_i$, enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.

The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.

Where the argument is difficult

Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.

The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.

Formalization scope

Jobs are $\mathrm{Fin}\,N$, and a policy is an equivalence permutation with $\pi(k)$ equal to the job in position $k$. Completion time is defined by the processing rule $Y_i(t)=X_i+\alpha_i t$, not by the closed form (2). At positions beyond the $N$ jobs it stays constant, and theorems about the closed form restrict $k$ to $0\le k\le N$. The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.

The proposition uses a probability space and the Bochner integral of the real-valued cost. Every $X_i$ is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.

The two strict orderings are over the labels of jobs in $\pi_0$, not positions of an arbitrary schedule. The conclusion compares $\pi_0$ with every permutation, not only with schedules obtained by one adjacent swap. The $N=0$ and $N=1$ cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.

Selected references

• Browne, Sid, and Uri Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 495–498 (1990). DOI: 10.1287/opre.38.3.495.

Motivation

Minimizing a smooth function over a closed convex set is the basic problem of constrained continuous optimization. When the constraint set is simple enough that the nearest point of the set to any given point can be computed (a ball, a box, an orthant, an affine subspace), the most direct method is the gradient projection method: take a gradient step and project back onto the set. The method is the ancestor of the projected gradient and proximal gradient algorithms used today in signal processing, machine learning, and optimal control, where the variable is often a function, so that the natural setting is an infinite-dimensional Hilbert space rather than $\mathbb R^n$.

A. A. Goldstein's 1964 note in the Bulletin of the AMS (Goldstein 1964) is one of the two founding papers of the method, alongside the independent work of Levitin and Polyak (1966). It states, in a Hilbert space and with an explicit step-size window, that the iterates stay in the initial level set, that the objective values converge, and that under convexity they converge to the optimal value, with weak and strong convergence of the iterates under further hypotheses. Goldstein motivates the method by applications to control theory (Balakrishnan 1963; Goldstein, Minimizing functionals on Hilbert space, 1964).

Timeline.

• 1959: Cheney and Goldstein study proximity maps (metric projections) onto convex sets and a fixed-point construction for the distance between two convex sets (Cheney–Goldstein 1959, cited by the note as [1]).
• 1964: Goldstein, this note: the gradient projection method in Hilbert space with steps in $[\sigma, 2\rho_0 - \sigma]$.
• 1966: Levitin and Polyak give the same method and convergence rates for constrained minimization.
• 1987: Calamai and Moré extend the analysis to Armijo-type step rules and identification of the active constraints in $\mathbb R^n$ (Calamai–Moré 1987).

Setting

Let $H$ be a real Hilbert space with inner product $[x, y]$ and norm $\|x\|$. Let $C \subseteq H$ be closed and convex, and let $P : H \to H$ be the projection onto $C$: $P(x)$ is the point of $C$ closest to $x$. In Lean, IsProjection C P says that $P(x) \in C$ and $\|x - P(x)\| \le \|x - y\|$ for all $y \in C$.

Let $f : H \to \mathbb R$, $x_0 \in C$, and let

$$S = \{x \in C : f(x) \le f(x_0)\}$$

be the level set (levelSet f C x0). Let $\hat S$ be an open set containing the convex hull of $S$. Write $f'(x, h)$ for the Fréchet derivative of $f$ at $x$ applied to $h$, $\nabla f(x)$ for the gradient (so $f'(x, h) = [\nabla f(x), h]$), and

$$f''(x, h, h) = \frac{d}{dt}\Big|_{t=0} f'(x + th, h)$$

for the directional second derivative in the sense of Gâteaux (d2 f x h). The curvature hypothesis is that for some $\rho_0 > 0$, at every $x \in \hat S$ and for every $h \in H$, these derivatives exist and

$$|f''(x, h, h)| \le \frac{\|h\|^2}{\rho_0}.$$

Choose $0 < \sigma \le \rho_0$ and step sizes $\sigma \le \rho_k \le 2\rho_0 - \sigma$. The method is

$$x_{k+1} = P\big(x_k - \rho_k \nabla f(x_k)\big), \qquad k \ge 0.$$

A point $z \in C$ is stationary if $P(z - \rho \nabla f(z)) = z$ for every $\rho > 0$.

Formalization targets

Goal: the THEOREM, parts (i)–(v)

Assume $f$ is bounded below and continuous on $C$. There is $L \in \mathbb R$ such that

1. (i) $x_k \in S$ for all $k$, $x_{k+1} - x_k \to 0$, and $f(x_k)$ decreases to $L$;
2. (ii) if $S$ is compact, every cluster point $z$ of $(x_k)$ near which $\nabla f$ is continuous is stationary, and a unique cluster point is the limit of $(x_k)$;
3. (iii) if $S$ is convex and $f''(x, h, h) \ge \mu \|h\|^2$ on $S$ for some $\mu \ge 0$, then

$$L = \inf\{f(x) : x \in C\};$$

4. (iv) under (iii) with $S$ bounded, every weak cluster point of $(x_k)$ minimizes $f$ on $C$;
5. (v) under (iii) with $\mu > 0$ and $\nabla f$ bounded on $S$, there is $z \in S$ with $f(z) = L$, $x_k \to z$ in norm, and $z$ is the unique minimizer of $f$ on $C$.

The goal is the whole theorem, because its five parts share one limit $L$ and one standing setting.

Milestones

The projection inequality $[x - y, P(x) - y] \ge \|P(x) - y\|^2$ for $y \in C$; the Lipschitz property of $P$; the characterization of stationarity for convex $f$ at a differentiability point; the one-step Taylor estimate; the step lemma (for $\sigma \le \rho \le 2\rho_0 - \sigma$ the new point stays in $S$ and the decrease is at least $\|x_{k+1} - x_k\|^2 \sigma / 4\rho_0^2$); parts (i) and (ii); the strong-convexity bound $f(x) \ge f(y) + [\nabla f(y), x - y] + \frac12\mu\|x - y\|^2$ on $S$; the supporting-hyperplane inequality of the proof of (iii); parts (iii), (iv) and (v). A companion item states the last clause of (ii) under convexity of $f$ on $C$.

Significance

The result. The theorem gives a step-size rule that needs only a curvature bound near the level set, not a global Lipschitz constant of the gradient, and it covers the infinite-dimensional case directly: (iii) gives convergence of the objective values to the optimal value without assuming that a minimizer exists, (iv) yields minimizers as weak cluster points when the level set is bounded, and (v) gives strong convergence of the iterates under strong convexity on the level set. These are the prototypes of the convergence statements now proved for projected and proximal gradient methods.

Formalizing it. The result is classical and proved on paper; it has no machine-checked proof. The note is two pages long and its proof is terse ("The proof of (ii) being straightforward"), and checking it in Lean exposes two places where the printed statement needs repair (see Formalization scope). A complete development also produces reusable infrastructure: the variational inequality and Lipschitz property of the metric projection in a Hilbert space, a one-dimensional Taylor estimate from a Gâteaux second derivative along a segment, and weak lower semicontinuity of convex continuous functions on closed convex sets used through cluster points in WeakSpace.

Difficulty

The obvious argument for (i) applies a quadratic upper bound for $f$ along the segment from $x_k$ to $x_{k+1}$. That bound is only available where the curvature hypothesis holds, on $\hat S$, and nothing guarantees in advance that $x_{k+1}$, or the segment, lies in $\hat S$. Ruling this out requires control of $f$ up to the boundary of the level set, which the printed hypotheses do not give; this is where the added continuity hypothesis enters. In (iii) the iterates may be unbounded and no minimizer need exist, so compactness arguments are unavailable. In (iv) the cluster points are weak, so norm-closedness arguments do not apply directly.

Formalization scope

• $H$ is a real Hilbert space: [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. The inner product $[x, y]$ is ⟪x, y⟫_ℝ, and $\nabla f$ is Mathlib's gradient f.
• $P$ is any map with IsProjection C P; there is no chosen projection and no junk value.
• $f''(x, h, h)$ is the derivative at $t = 0$ of $t \mapsto f'(x + th, h)$. The hypothesis on $\hat S$ (SecondDerivBound) states both differentiabilities before the bound, so the bound is never on a junk zero.
• The run starts at $x_0$, and $0 < \sigma \le \rho_0$ makes the step window nonempty.
• "$L = \inf$" is IsGLB (f '' C) L. Weak cluster points are cluster points in WeakSpace ℝ H.
• Added hypothesis: $f$ is continuous on $C$. Part (i) as printed is false without it: on $H = C = \mathbb R$ with $P = \mathrm{id}$, $f(x) = (x - 2)^2$ for $x < 1$ and $f(x) = 100$ for $x \ge 1$, $x_0 = 0$, $\hat S = (-1, 1)$, $\rho_0 = 1/2$, $\sigma = 1/4$, $\rho_k = 1/2$, the first step lands at $x_1 = 2$ with $f(x_1) = 100 > f(x_0)$.
• Moved clause. The last clause of (ii), "$z$ minimizes $f$ on $C$", is false for nonconvex $f$ (a unique cluster point can be a stationary point that is not a minimizer). The goal omits it, and a companion item states it under convexity of $f$ on $C$.
• The goal assumes nothing about the step decrease, the step size $\hat\rho$ of the proof, or the iterates beyond the run's definition. A formalization that adds such facts as hypotheses, or that proves only one of the five parts, does not count as closing the goal.

Contributions welcome: proofs of any milestone, in particular the projection inequality and Lipschitz property (independent of the rest), the Taylor estimate from the Gâteaux second derivative, and the weak-closedness argument of (iv).

Selected references

• A. A. Goldstein, Convex programming in Hilbert space, Bull. Amer. Math. Soc. 70 (1964), 709–710. https://doi.org/10.1090/s0002-9904-1964-11178-2
• E. W. Cheney and A. A. Goldstein, Proximity maps for convex sets, Proc. Amer. Math. Soc. 10 (1959), 448–450.
• A. V. Balakrishnan, An operator theoretic formulation of a class of control problems and a steepest descent method of solution, J. SIAM Control Ser. A 1 (1963), 109–127.
• E. S. Levitin and B. T. Polyak, Constrained minimization methods, USSR Comput. Math. Math. Phys. 6(5) (1966), 1–50.
• P. H. Calamai and J. J. Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), 93–116. https://doi.org/10.1007/BF02592073

Why consensus and sharing

Many large optimization problems arising in statistics, machine learning, signal processing and resource allocation have an objective that is a sum of terms, each depending on data held by a different processor, or a coupling term that depends on the sum of the agents' decisions. Chapter 7 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) introduces two templates that turn such problems into distributed algorithms: consensus and sharing. Nearly every distributed application in the rest of the monograph (distributed lasso, distributed logistic regression, splitting across examples and across features in Chapter 8) is an instance of one of the two. Consensus problems in the context of ADMM go back to Bertsekas and Tsitsiklis (Parallel and Distributed Computation, 1989).

The value of the templates lies in a handful of exact algebraic facts about the ADMM subproblems: the global update is an average, the dual variables average to zero, and the sharing update, which looks like a problem in $Nn$ variables, is really a problem in $n$ variables. These facts are what this mission formalizes.

Setting

There are $N\ge1$ agents. Vectors live in $\mathbb R^n$ with the Euclidean inner product, and an overline denotes an average over agents, $\bar v=\frac1N\sum_{i=1}^N v_i$. Each local cost $f_i$ and the shared cost $g$ are functions into $\mathbb R\cup\{+\infty\}$. The penalty parameter is $\rho>0$.

Global variable consensus (§7.1) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)\quad\text{subject to } x_i-z=0,\ i=1,\dots,N,$$

with local variables $x_i\in\mathbb R^n$ and a global variable $z$. ADMM alternates a parallel $x_i$-update, an averaging $z$-update and a dual update of the multipliers $y_i$. With a regularizer $g(z)$ added (7.2), the $z$-update (7.4) becomes a minimization involving $g$.

General form consensus (§7.2) lets local variable $x_i\in\mathbb R^{n_i}$ copy only some entries of $z$: entry $j$ of $x_i$ corresponds to entry $z_{\mathcal G(i,j)}$, and $\tilde z_i\in\mathbb R^{n_i}$ is defined by $(\tilde z_i)_j=z_{\mathcal G(i,j)}$. The number of local entries copying $z_g$ is $k_g$.

Sharing (§7.3) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)+g\Big(\sum_{i=1}^N x_i\Big),\tag{7.11}$$

written for ADMM with copies $z_i$ of the $x_i$ (7.12). In scaled form, with $a_i=u_i^k+x_i^{k+1}$, its $z$-update is

$$(z_1^{k+1},\dots,z_N^{k+1})\in\operatorname*{argmin}_{z_1,\dots,z_N}\ g\Big(\sum_{i=1}^N z_i\Big)+(\rho/2)\sum_{i=1}^N\|z_i-a_i\|_2^2,$$

followed by $u_i^{k+1}=u_i^k+x_i^{k+1}-z_i^{k+1}$.

Formalization targets

Goal: the sharing $z$-update reduction (§7.3, p. 57)

For every $a_1,\dots,a_N$: $(z_1,\dots,z_N)$ solves the $Nn$-variable $z$-update iff $\bar z$ solves

$$\operatorname*{minimize}_{\bar z\in\mathbb R^n}\ g(N\bar z)+(\rho/2)\sum_{i=1}^N\|\bar z-\bar a\|_2^2$$

and

$$z_i=a_i+\bar z-\bar a\quad (7.13);$$

and along every run of sharing ADMM,

$$u_i^{k+1}=\bar u^k+\bar x^{k+1}-\bar z^{k+1}\quad(7.14),$$

so all scaled dual variables agree after one step.

Milestones

• §7.1: the consensus $z$-update is $z^{k+1}=\bar x^{k+1}+(1/\rho)\bar y^k$; then $\bar y^{k+1}=0$, $z^k=\bar x^k$ and the simplified iteration.
• (7.4), §7.1.1: with a regularizer, the $z$-update is averaging followed by a proximal step with weight $N\rho$; the soft-threshold ($g=\lambda\|\cdot\|_1$) and positive-part ($g$ the indicator of $\mathbb R^n_+$) examples.
• §7.2: the general form $z$-update is local averaging, and the dual entries attached to each global index sum to zero after the first iteration.
• (7.13): with $\bar z$ fixed, $z_i=a_i+\bar z-\bar a$ is the unique minimizer.

Significance

The reduction is what makes sharing ADMM scale: the central step needs only the averages $\bar x^{k+1}$, $\bar u^k$ and one $n$-dimensional proximal problem, regardless of the number of agents, and the dual state collapses to a single vector. The same reduction underlies exchange ADMM (§7.3.2) and the splitting-across-features algorithms of §8.3. The consensus facts explain why the fusion center only averages and why the dual variables can be dropped from its update.

All results of the chapter are proved, informally, in the monograph; they are elementary. To our knowledge none has a machine-checked proof. The mission produces checked statements of the update formulas that later chapters of the series and distributed-optimization developments can cite instead of re-deriving.

Difficulty

The statements are exact identities between minimizer sets of nonsmooth problems in which $g$ may be any extended-real-valued function: there is no first-order condition to use, so each step must be argued by comparing objective values, and the iff requires producing, for an arbitrary competitor, a competitor of the reduced problem with no larger value. The index bookkeeping is the other half: averages of sums of sequences indexed by agents and by iterations, the off-by-one in "after the first iteration", and in §7.2 sums over the fibres $\{(i,j):\mathcal G(i,j)=g\}$ of an index map between local vectors of different dimensions.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin n); agents are indexed by Fin N, so the book's $i=1,\dots,N$ is Lean's $i-1$; components are 0-based as well.
• An extended-real-valued function is encoded by its effective domain (a set) and its finite values; every minimization is over the domain. Convexity is not assumed: none of the stated identities needs it, so the statements are slightly more general than the chapter's standing assumption that each $f_i$ is convex.
• Iterates are hypotheses: a run is any sequence satisfying the update rules (argmin properties, not chosen minimizers). The consensus run uses the averaging formula exactly as printed on p. 49; the general form and sharing runs use the argmin form printed on pp. 55–56.
• Explicit hypotheses that the book leaves implicit: $N\ge1$, $\rho>0$, $\lambda>0$ (named lam), $k_g\ge1$ for every global index $g$ in §7.2, and the index ranges $k\ge1$ for $\bar y^{k}=0$ and $k\ge2$ for $z^k=\bar x^k$ (the starting $y^0$ is arbitrary).
• Corrected misprints: p. 52 prints $\bar x^{k+1}-(1/\rho)\bar y^k$ in the soft-threshold and positive-part examples, while the proximal form gives $\bar x^{k+1}+(1/\rho)\bar y^k$; p. 55 prints $\sum_{i=1}^m$ for $\sum_{i=1}^N$; p. 57 writes $u\in\mathbf R^m$ for a vector of $\mathbb R^n$.
• The goal is about minimizers of the $Nn$-variable $z$-subproblem, not the algebraic identity (7.13) alone, and (7.14) is derived for every run rather than built into a single-dual-variable definition; either shortcut would make the goal trivial.
• Not included: the consensus residual norms (p. 51), the duality discussion of §7.3.1 and exchange ADMM (§7.3.2). Contributions formalizing them on top of these definitions are welcome.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 1–122, 2011. https://doi.org/10.1561/2200000016
• D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://web.mit.edu/dimitrib/www/pdc.html

Motivation

In two-stage optimization under uncertainty, a first-stage decision $x$ is taken before the data are known, and a second-stage decision $y$ is taken after a scenario $\omega$ is revealed. The fully adaptive formulation lets $y$ depend on $\omega$ and minimizes the worst-case cost. It is the natural model of recourse, but it optimizes over policies, one decision per scenario, and is computationally hard in general. The static robust formulation fixes one $y$ in advance that must be feasible in every scenario. It is a single deterministic mixed integer program and is the standard tractable surrogate (Ben-Tal, Goryashko, Guslitzer, Nemirovski 2004; Bertsimas & Sim 2004).

The question is how much is lost by the surrogate. Bertsimas and Goyal (2010) bound the gap by $2$ against the stochastic problem and by $4$ against the adaptive problem when the uncertainty set is symmetric. Their §5.3 identifies a case with no gap at all: when the uncertainty set is a hypercube (a box), the static robust optimum equals the adaptive optimum, and this holds even when the constraint matrices themselves are uncertain. Box uncertainty is the simplest and most common uncertainty model in practice (interval data on every coefficient), so the result says that for it, adaptivity buys nothing.

This mission formalizes that theorem, Theorem 5.4, together with Theorem 2.4, which shows that under right-hand-side uncertainty the robust problem is a single deterministic problem with the coordinatewise worst right-hand side.

Setting

Fix dimensions $m,n_1,n_2$ and sets $I_1,I_2$ of integer coordinates. The decision domains are

$$D_{I}=\{x\in\mathbb R^n : x\ge0,\ x_i\in\mathbb Z\ \text{for } i\in I\},$$

which is $\mathbb R_+^{n-p}\times\mathbb Z_+^{p}$ up to relabelling coordinates, $p=|I|$.

A scenario set $\Omega$ is given. In scenario $\omega$ the data are a constraint matrix $A(\omega)\in\mathbb R^{m\times n_1}$, a recourse matrix $B(\omega)\in\mathbb R^{m\times n_2}$, a right-hand side $b(\omega)\in\mathbb R^m$ and a second-stage cost $d(\omega)\in\mathbb R^{n_2}_+$. The first-stage cost $c\in\mathbb R^{n_1}_+$ is fixed.

• The adaptive problem $\Pi_{\mathrm{Adapt}}(A,B,b,d)$ (5.6) chooses $x\in D_{I_1}$ and $y(\omega)\in D_{I_2}$ for every $\omega$ with $A(\omega)x+B(\omega)y(\omega)\ge b(\omega)$ for all $\omega$, and has value

$$z_{\mathrm{Adapt}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega).$$

• The robust problem $\Pi_{\mathrm{Rob}}(A,B,b,d)$ (5.7) chooses one $x\in D_{I_1}$, $y\in D_{I_2}$ with $A(\omega)x+B(\omega)y\ge b(\omega)$ for all $\omega$, and has value

$$z_{\mathrm{Rob}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty.$$

The uncertainty set is $\mathcal U=\{(A(\omega),B(\omega),b(\omega),d(\omega)) : \omega\in\Omega\}$, a subset of $\mathbb R^N$ with $N=mn_1+mn_2+m+n_2$. Following Definition 1.1, $\mathcal U$ is a hypercube if $\mathcal U=[l_1,u_1]\times\cdots\times[l_N,u_N]$ for some $l_i\le u_i$.

For Theorem 2.4, $A$, $B$ and $d$ are fixed and only $b(\omega)\in\mathbb R^m_+$ varies; $\Pi_{\mathrm{Rob}}(b)$ (1.2) is the robust problem above, and $\Pi$ is the deterministic problem with right-hand side $b^h_j=\max_\omega b_j(\omega)$.

Formalization targets

Goal: Theorem 5.4 (p. 31)

If $\mathcal U$ is a hypercube, then

$$z_{\mathrm{Rob}}(A,B,b,d)=z_{\mathrm{Adapt}}(A,B,b,d).$$

The integer coordinates $I_1,I_2$ are arbitrary, and nothing is assumed about the signs of $A$, $B$, $b$.

Milestones

1. Theorem 2.4 (p. 17). Under right-hand-side uncertainty, $(x,y)$ is feasible for $\Pi_{\mathrm{Rob}}(b)$ if and only if $Ax+By\ge b^h$; hence $z_{\mathrm{Rob}}(b)=z(\Pi)$.
2. p. 31 display. $z_{\mathrm{Adapt}}(A,B,b,d)\le z_{\mathrm{Rob}}(A,B,b,d)$ for every uncertainty set.
3. Eqs. (5.8)–(5.10). If $\mathcal U$ is a hypercube, some scenario $\bar\omega$ has $A(\bar\omega)$, $B(\bar\omega)$ entrywise minimal and $b(\bar\omega)$, $d(\bar\omega)$ entrywise maximal over $\Omega$.
4. Eqs. (5.11)–(5.13). For such $\bar\omega$, if $(x,y(\cdot))$ is adaptive feasible, then $(x,y(\bar\omega))$ is robust feasible.
5. Eq. (5.14). For such $\bar\omega$, the robust worst-case cost of $(x,y(\bar\omega))$ is at most the adaptive worst-case cost of $(x,y(\cdot))$.

Significance

The result. Theorem 5.4 says that for interval uncertainty on every coefficient, the static robust program, whose size does not grow with the number of scenarios, solves the adaptive problem exactly. Combined with Theorem 2.4 for right-hand-side uncertainty, the adaptive problem collapses to one deterministic mixed integer program with worst-case data. It marks the boundary case of the paper's adaptability-gap bounds: the gap is at most $4$ for symmetric sets, and exactly $1$ for boxes.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean model of two-stage robust and adaptive mixed integer programs with uncertain constraint matrices, with values as extended-real infima, which other formalizations of adjustable robust optimization can build on.

Difficulty

The mathematics is elementary; the care is in the statement. The step that fails for a general uncertainty set is the existence of a single worst scenario $\bar\omega$ that is simultaneously entrywise smallest in $A$, $B$ and entrywise largest in $b$, $d$. For a set that is only contained in a box, the box's worst corner need not be realized. With two scenarios $b=(1,0)$ and $b=(0,1)$, $B=I$, $d=(1,1)$, the adaptive value is $1$ and the robust value is $2$. A formalization therefore has to state the hypercube hypothesis as an equality of sets. A second point is the arithmetic of extended reals: the paper argues from optimal solutions, which need not exist, so the inequalities must be transported through infima over feasible sets that may be empty and through suprema that may be infinite.

Formalization scope

• Decisions are vectors Fin n → ℝ; matrices are Matrix (Fin m) (Fin n) ℝ; constraints use Mathlib's componentwise order and mulVec.
• Mixed-integer domains are "nonnegative, integer on a designated coordinate set $I$", the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$ up to relabelling.
• Optimal values are EReal infima over the feasible set, $+\infty$ when infeasible; worst-case costs are EReal suprema over $\Omega$. No optimal solution is assumed.
• A scenario datum is a structure with the four blocks $(A,B,b,d)$; the box and the hypercube predicate are written entrywise on these blocks, which is Definition 1.1 in $\mathbb R^N$.
• The hypercube hypothesis is IsHypercube (uncertaintySet A B b d), i.e. the realized data are exactly a box. Assuming only that the data lie inside a box would make the statement false (example above); assuming fixed $A$, $B$ would state Corollary 5.1 instead of Theorem 5.4.
• Typos corrected in the Lean: (5.6)–(5.7) print $\mathbb Z^{n_2}_+$ for the second-stage integer block, read as $\mathbb Z^{p_2}_+$; §5.3's opening sentence names $\Pi_{\mathrm{Adapt}}(b,d)$ twice where the first is $\Pi_{\mathrm{Rob}}(b,d)$.
• In Theorem 2.4 the paper's $\max_\omega b_j(\omega)$ is a real supremum under the hypothesis that the right-hand sides are bounded above, and the second stage is continuous ($p_2=0$), as in the problem $\Pi$ on the page.

Contributions welcome: proofs of the milestones and of the goal, and lemmas on monotonicity of mulVec for nonnegative vectors and on EReal infima over feasible sets, which are reusable across the other missions of this series.

Selected references

• D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace).
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task $T_i$ has a length $l_i \ge 0$ and a preferred starting time $a_i \ge 0$, and the discrepancy of a task started at time $s_i$ is $|s_i - a_i|$. The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an $O(N \log N)$ algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy $\max_i |s_i - a_i|$: a linear-time test for a given bound $\gamma$ after an $O(N \log N)$ sort, combined with a search over $\gamma$.

This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).

Setting

Fix a bound $\gamma \ge 0$. A schedule has maximum discrepancy at most $\gamma$ exactly when every task starts no earlier than its release time $r_i = \max\{0, a_i - \gamma\}$ and finishes no later than its deadline $d_i = a_i + l_i + \gamma$ (p. 342). These release times and deadlines are in special form: with $\alpha = 2\gamma$, for every task

$$d_i - r_i = l_i + \alpha \quad\text{or}\quad \big(r_i = 0 \text{ and } d_i < l_i + \alpha\big).$$

From here on the data are arbitrary reals $l_i \ge 0$, $r_i \ge 0$, $d_i$ in special form for some $\alpha \ge 0$.

A schedule is an execution order $\sigma$ ($\sigma(p)$ is the task in position $p$) with starting times $s_i$, such that a task finishes no later than any later-positioned task starts: $s_{\sigma(p)} + l_{\sigma(p)} \le s_{\sigma(q)}$ for $p < q$. It is feasible if $r_i \le s_i$ and $s_i + l_i \le d_i$ for every $i$. Its makespan is $\max_i (s_i + l_i)$, and it is optimum if it is feasible and no feasible schedule has a smaller makespan.

Let $T_N$ be a task of largest deadline. A schedule has the release time property if every task executed after $T_N$ has release time strictly later than the starting time of $T_N$. When the tasks are indexed with $d_1 \le \dots \le d_N$, a schedule is in standard form with split index $j$, $0 \le j \le N-1$, if it begins with an optimum schedule of $T_1, \dots, T_j$, followed by $T_N$ started at the maximum of $r_N$ and the completion time of that first part, followed by $T_{j+1}, \dots, T_{N-1}$ in this order without idle time.

Formalization targets

Goal: Corollary 2 (p. 344)

$$\exists\ \text{a feasible schedule} \;\Longrightarrow\; \exists\ \text{an optimum schedule that is in standard form and has the release time property.}$$

Milestones

1. Theorem 4 (pp. 342–343): if a feasible schedule exists, some optimum schedule has the release time property with respect to any task of largest deadline.
2. The deadline split (proof of Corollary 1, p. 344): in every feasible schedule with the release time property, a task $T_i \neq T_N$ precedes $T_N$ if and only if $d_i \le s_N + \alpha$.
3. Corollary 1 (p. 344): some optimum schedule executes before $T_N$ exactly the tasks of deadline at most $\beta$, for some $\beta \ge 0$.
4. Release before finish (p. 344): every task executed after $T_N$ has $r_i \le s_N + l_N$.
5. Normalization after $T_N$ (p. 344): an optimum schedule with the release time property can be changed, without moving $T_N$ later and without touching the tasks before it, so that there is no idle time from the start of $T_N$ on and the later tasks run in deadline order.

Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with $\alpha = 2\gamma$.

Significance

Corollary 2 reduces the search for an optimum schedule of $T_1, \dots, T_n$ to $n$ candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in $O(N)$ time after an $O(N \log N)$ sort; combined with a search over $\gamma$ it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.

The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.

Difficulty

The obvious argument fails in Theorem 4. Exchanging a straggler (a task after $T_N$ released no later than $T_N$ starts) with $T_N$ shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after $T_N$ starts has $r_i > 0$, hence $d_i - r_i = l_i + \alpha$ exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after $T_N$, then fewest tasks between $T_N$ and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after $T_N$ and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.

Formalization scope

Tasks are indexed by Fin N (0-based: the paper's $T_1, \dots, T_N$ are $0, \dots, N-1$; the paper's $T_N$ in Corollary 2 is the index $N-1$). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.

The standing hypotheses on every structural item are $\alpha \ge 0$, $r_i \ge 0$, $l_i \ge 0$ (from $\gamma \ge 0$, the $\max\{0, \cdot\}$ in $r_i$, and nonnegative lengths); since $s_i \ge r_i$, start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task $T_0$ ($r_0 = d_0 = l_0 = 0$) is not a task; an empty first part completes at time $0$. Corollary 1's "the set of all tasks with deadline $\beta$ or less" is read as excluding $T_N$, the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.

A trivializing formalization is excluded: the standard form pins $T_N$'s start to $\max(r_N, C)$ and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.

Running times ($O(N \log N)$, $O(N)$) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (reference [4] of the paper, cited on p. 342 for the NP-completeness of one-processor scheduling with release times and deadlines). ISBN 0-7167-1045-5

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.

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 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