Optimization

Motivation

Many optimization problems of operations research have objectives that are convex but not differentiable: Lagrangian duals of integer and combinatorial programs, maxima of finitely many affine or smooth functions, penalty functions for systems of inequalities, and the value functions produced by decomposition. For such functions the gradient method and steepest descent fail. Constant steps cannot work because the subgradients need not tend to zero at a nondifferentiable minimum, and exact line search along the negative gradient can converge to a point that is not a minimizer (the example on pp. 22–23 of the source).

The subgradient method replaces the gradient by an arbitrary subgradient and gives up monotone decrease of the objective. Its convergence theory is the foundation of nondifferentiable optimization and of Lagrangian relaxation in integer programming.

Timeline. N. Z. Shor proposed the method with normalized steps in 1962 (Kiev). Yu. M. Ermoliev proved convergence in finite dimensions with divergent-series stepsizes (Kibernetika, 1966), and B. T. Polyak proved it for constrained problems in Hilbert space (Doklady Akad. Nauk SSSR, 1967). Held, Wolfe and Crowder (Mathematical Programming, 1974) brought the method to large combinatorial problems through Lagrangian relaxation. This mission formalizes the exposition of Section 2.1–2.2 of Shor's monograph (Springer, 1985), which gives self-contained proofs of these results.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. Let $f : E_n \to \mathbb{R}$ be a convex function finite everywhere. A vector $g$ is a subgradient of $f$ at $x_0$ if

$$f(x) - f(x_0) \ge (g, x - x_0) \quad \text{for all } x \in E_n.$$

Every convex $f$ has at least one subgradient at every point. Let $M^* = \{x : f(x) \le f(y) \ \forall y\}$ be the set of minimum points and, when it is nonempty, $f^* = \min f$.

A subgradient selection $g_f$ assigns to each $x$ some subgradient $g_f(x)$ of $f$ at $x$. No particular choice is made: every result holds for every selection. Given stepsizes $h_1, h_2, \dots > 0$ and a starting point $x_0$, the normalized subgradient method is

$$x_{k+1} = x_k - h_{k+1}\, \frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, \dots \tag{2.4}$$

If $g_f(x_k) = 0$, then $x_k$ is a minimizer and the computation stops. The unnormalized method is $x_{k+1} = x_k - h_{k+1} g_f(x_k)$ (2.5), and the method with restarts takes that step when $h_{k+1}\|g_f(x_k)\| \le c$ and returns to $x_0$ otherwise.

Formalization targets

Goal: Theorem 2.2 (p. 25)

If $M^*$ is nonempty and bounded, $h_k > 0$, $h_k \to 0$ and $\sum_{k \ge 1} h_k = +\infty$, then for every $x_0$ and every subgradient selection, the method (2.4) either reaches $M^*$ at some index $\bar k$ or

$$\lim_{k \to \infty} \min_{y \in M^*} \|x_k - y\| = 0, \qquad \lim_{k \to \infty} f(x_k) = f^*.$$

Milestones

1. Eq. (2.3), the one-step inequality $\|x_{k+1} - x^*\|^2 \le \|x_k - x^*\|^2 + h^2 - 2h\,\rho(x^*, U_k)$, where $U_k = \{x : f(x) = f(x_k)\}$.
2. Theorem 2.1: with constant step length $h$, some level surface $\{f = f(x_{k^*})\}$ passes within $h(1+\varepsilon)/2$ of any $x^* \in M^*$.
3. Corollaries 1 and 2: a suitable constant step length yields a subsequence with $f(x_{k_i}) - f^* < \delta$. If $M^*$ contains a ball of radius $r > h/2$, the method terminates in $M^*$.
4. Theorem 2.5: if $M^*$ contains a ball of radius $r$, $\sum h_k = \infty$ and $\limsup h_k < 2r$, then (2.4) terminates in $M^*$.
5. Theorem 2.3: for the unnormalized method (2.5), bounded subgradients along the trajectory imply convergence, and unbounded subgradients rule it out.
6. Theorem 2.4: the method with restarts converges for every $c > 0$.

Significance

Theorem 2.2 is the basic convergence guarantee for first-order methods on general nonsmooth convex functions. It needs no Lipschitz constant, no bound on the subgradients and no smoothness: normalizing the step makes the step length independent of the size of the subgradient. The divergent-series rule $h_k \to 0$, $\sum h_k = \infty$ is the standard stepsize condition of stochastic approximation and of Lagrangian relaxation codes. Theorems 2.3–2.5 mark its boundaries. The unnormalized method needs bounded subgradients (Theorem 2.3), restarts remove that need (Theorem 2.4), and a solution set with nonempty interior gives finite termination (Theorem 2.5). The last result is the basis of the finite methods for systems of convex inequalities and for the dual of an assignment problem with a unique solution (pp. 28–29).

All of these results are classical and proved in the source. None of them is formalized in Lean's Mathlib. The platform has neighbouring results that are not the same statements: Poljak's divergent-series theorem for concave piecewise-linear maximization (in Validation of Subgradient Optimization I), and rate bounds for Lipschitz objectives (First-Order and Stochastic Optimization Methods for ML II, Understanding Machine Learning X). This mission adds the general convex case with normalized steps, the dichotomy for unnormalized steps, and finite termination.

Difficulty

The standard rate analysis of the subgradient method bounds $\|x_{k+1} - x^*\|^2 - \|x_k - x^*\|^2$ by $-2h_{k+1}(f(x_k) - f^*)/\|g_f(x_k)\| + h_{k+1}^2$. It then needs a uniform bound on $\|g_f(x_k)\|$, which is exactly what is not assumed here. Nothing a priori keeps the iterates in a bounded set, and the subgradients of a general convex function (for instance $f(x) = x^4$, the source's example on p. 26) grow without bound away from $M^*$; with unnormalized steps this makes the method diverge. Even with normalized steps, the distance to a minimizer decreases only outside a neighbourhood of $M^*$ whose size is of the order of the current step, so a monotone decrease argument gives at best a subsequence with small function values. Convergence of the whole sequence $\min_{y \in M^*}\|x_k - y\|$ to zero is a stronger statement, and boundedness of $M^*$ is essential to it.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere) with ConvexOn ℝ Set.univ f.
• The subgradient selection g is arbitrary, with the hypothesis ∀ x, IsSubgradient f x (g x). The starting point is arbitrary.
• The iterations are defined recursively (normalizedIter, plainIter, resetIter); the stepsize sequence is h : ℕ → ℝ with h (k+1) used at step $k$. In (2.4), a zero subgradient is handled by an explicit branch that repeats the current iterate (which is then in $M^*$). No statement relies on Lean's convention $x/0 = 0$.
• $M^*$ is required to be nonempty wherever the book writes $\min_{y \in M^*}$ or $f^* = \min f$. $\min_{y \in M^*}\|x_k - y\|$ is Metric.infDist, and $f^*$ is ⨅ y, f y.
• $\sum_{k \ge 1} h_k = +\infty$ is Tendsto (fun N => ∑ k ∈ Finset.range N, h (k+1)) atTop atTop. $\limsup h_k < 2r$ is "for some $q < 2r$, eventually $h_k \le q$", so it cannot hold vacuously for an unbounded sequence.
• Corollary 1's step length $h_\delta$ is quantified before the selection and the starting point: it depends only on $f$ and $\delta$.
• Theorem 2.3 is stated as two implications, (bounded subgradients ⇒ convergence) and (unbounded ⇒ no convergence), not as a disjunction that one case could satisfy trivially.
• A formalization of Theorem 2.2 that assumes bounded subgradients, a Lipschitz $f$, or a specific subgradient choice (such as the minimal-norm one) proves a different and weaker theorem, and does not close the goal.

Needed infrastructure: continuity of convex functions on $E_n$ (in Mathlib), compactness of sublevel sets when $M^*$ is bounded, and the geometry of level surfaces relative to supporting hyperplanes. The one-step inequality (2.3) and the level-set compactness lemma are reusable by the later missions of this series (linear rate, Polyak's stepsize, stochastic subgradient). Contributions that prove Eq. (2.3) or Theorem 2.1 first are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Chapter 2, pp. 22–30. https://doi.org/10.1007/978-3-642-82118-9
• B. T. Polyak, A general method for solving extremal problems, Doklady Akademii Nauk SSSR 174 (1967), 33–36 (the source's reference [64]).
• Yu. M. Ermoliev, Methods for solving nonlinear extremal problems, Kibernetika (Kiev), no. 4 (1966), 1–17 (the source's reference [24]).
• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223

Motivation

Gradient methods assume a continuous gradient; subgradient methods assume convexity. Many objective functions met in practice satisfy neither. Shor's example is economic planning, where components of the objective are piecewise-smooth, not necessarily convex functions of a parameter describing the productivity of a unit, and where minimax formulations produce kinks as a rule (Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, §1.4, p. 17, DOI 10.1007/978-3-642-82118-9). Such problems need a class of functions wide enough to contain piecewise-smooth and minimax functions and narrow enough to carry a usable replacement for the gradient.

Shor's answer is the class of almost differentiable functions, introduced in his 1972 work and presented in §1.4 of the book, together with the almost-gradient, a limit of gradients taken at nearby points of differentiability. The capstone of the section, Theorem 1.15, connects this class with convex analysis: every convex function on $E_n$ is almost differentiable, and its almost-gradients are subgradients. This is what lets the later chapters treat convex minimization and almost-differentiable minimization with one set of tools. Clarke's generalized gradient of locally Lipschitz functions (Clarke 1975) is the closest relative; Shor's definition differs in requiring the gradient to be continuous on its domain (p. 19).

Setting

Let $E_n$ denote $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. For $f : E_n \to \mathbb{R}$, write $M = \{x \in E_n : f \text{ is differentiable at } x\}$ and $\nabla f(x)$ for the gradient at $x \in M$.

A function $f$ is almost differentiable if

1. on every bounded set $S$ it is Lipschitz: $|f(x) - f(y)| \le L_S \|x - y\|$ for $x, y \in S$, with a constant $L_S$ depending on $S$;
2. it is differentiable at Lebesgue-almost every point of $E_n$;
3. the map $x \mapsto \nabla f(x)$, restricted to $M$, is continuous.

An almost-gradient of $f$ at $x_0$ is a vector $g$ that is an accumulation point of a sequence $\nabla f(x_1), \nabla f(x_2), \dots$ with $x_k \in M$ and $x_k \to x_0$. The set of almost-gradients is $G(x_0)$. A generalized almost-gradient is a point of the closure of the convex hull of $G(x_0)$.

A vector $g$ is a subgradient of $f$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x \in E_n$; for convex $f$ the set of subgradients is the subdifferential $G_f(x_0)$.

In Lean these objects are AlmostDifferentiable f, almostGradients f x₀ and IsSubgradient f x₀ g in the namespace ShorNonsmooth.AlmostDiff, with $E_n$ = EuclideanSpace ℝ (Fin n).

Formalization targets

Goal: Theorem 1.15 (p. 18)

For convex $f : E_n \to \mathbb{R}$,

$$f \text{ is almost differentiable} \quad\text{and}\quad G(x_0) \subseteq G_f(x_0) \ \text{ for every } x_0 \in E_n .$$

The printed statement says the almost-gradients "coincide with" the subgradients. As a set equality this is false (for $f(x) = |x|$ on $E_1$, $G(0) = \{-1, 1\}$ while $G_f(0) = [-1, 1]$), and the book's proof establishes the inclusion. The goal is the inclusion.

Milestones

1. Proof of Theorem 1.15, display (p. 18). For convex $f$ differentiable at $x_k$: $f(x) - f(x_k) \ge (\nabla f(x_k), x - x_k)$ for all $x$.
2. Proof of Theorem 1.15 (p. 18). For convex $f$ and bounded $S$ there is $C$ with $|f'_v(x)| \le C\|v\|$ for all $x \in S$ and all $v$, the one-sided directional derivatives existing.
3. Proof of Theorem 1.15 (p. 18). A convex $f$ is differentiable almost everywhere and $\nabla f$ is continuous on $M$.
4. Theorem 1.14 (p. 18). For almost differentiable $f$, $G(x)$ is nonempty, bounded and closed at every $x$.
5. p. 19. For almost differentiable $f$, $\overline{\operatorname{conv}}\, G(x)$ is convex, bounded and closed.

Significance

The result. Theorem 1.15 embeds convex functions into the almost differentiable class and identifies each almost-gradient of a convex function as a subgradient. Consequently any method that only needs almost-gradients (limits of gradients at nearby differentiable points, which is what a numerical procedure can actually compute) produces valid subgradients when applied to a convex function. Theorem 1.14 supplies the compactness that makes $G(x)$ usable as a set-valued substitute for the gradient.

Formalizing it. All results here are classical and proved on paper. Mathlib contains Rademacher's theorem for Lipschitz functions (LipschitzWith.ae_differentiableAt) and local Lipschitz continuity of convex functions on open sets; it does not contain the continuity of the gradient of a convex function on its domain of differentiability, nor any notion of almost-gradient. The mission produces those, together with a formal record that the printed "coincide" is an inclusion. A formal proof of the true equality $G_f(x_0) = \overline{\operatorname{conv}}\, G(x_0)$ would be a welcome further contribution.

Difficulty

Two parts of the goal carry real content. The first is condition (c): the gradient of a convex function, restricted to the set where it exists, is continuous. The book cites this from the literature; it is not a consequence of Rademacher's theorem, which gives differentiability almost everywhere and says nothing about how gradients at nearby points relate. The second is condition (b) in a form Lean accepts: Rademacher's theorem in Mathlib is stated for globally Lipschitz functions, while a convex function on $E_n$ is only Lipschitz on bounded sets, so the almost-everywhere statement has to be assembled from local pieces. The passage from gradients to subgradients in the second conjunct is comparatively routine.

The analogous closure properties claimed on the same pages for sums, products and maxima of almost differentiable functions (Theorems 1.16 and 1.17) are false as printed and are not targets; see the formalization scope.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $n = 0$ is allowed and harmless. Functions are total and real-valued; convexity is ConvexOn ℝ Set.univ f.
• The gradient is Mathlib's gradient f x; condition (c) is ContinuousOn (gradient f) {x | DifferentiableAt ℝ f x}, continuity of the restriction in the subspace topology.
• Condition (a) is quantified over every bounded set with a set-dependent constant: ∀ S, Bornology.IsBounded S → ∃ L, LipschitzOnWith L f S. Condition (b) is ∀ᵐ x ∂volume, DifferentiableAt ℝ f x.
• An almost-gradient is a cluster point (MapClusterPt) of the gradient sequence, not its limit; the points $x_k$ may equal $x_0$.
• Subgradients are taken relative to the whole space, the domain of every function in this mission.
• The goal states the inclusion $G(x_0) \subseteq G_f(x_0)$ proved in the book. Stating the printed set equality would make the goal false; weakening the first conjunct to "locally Lipschitz and differentiable almost everywhere" would drop condition (c) and with it the substance of the theorem. Neither is acceptable.
• Theorem 1.16 (sums, differences, products) and Theorem 1.17 (maxima) are omitted: both are false for the class as defined. With $h(x) = x^2 \sin(1/x)$, the functions $h + |x|$ and $-|x|$ are almost differentiable but their sum $h$ is differentiable everywhere with a derivative discontinuous at $0$; and $\max(h - |x|,\, h - |x| + 2x) = h + x$. Theorem 1.18 (Mifflin's superposition theorem for semismooth functions) is cited from the literature without proof and rests on Clarke's generalized gradient; it is outside this mission.

Infrastructure that is reusable beyond this mission: continuity of the gradient of a convex function on its domain; Rademacher's theorem for locally Lipschitz functions on $E_n$; the almost-gradient set and its compactness. Contributions that prove these as standalone lemmas are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 25.5 (continuity of the gradient of a convex function). https://doi.org/10.1515/9781400873173
• F. H. Clarke, Generalized gradients and applications, Transactions of the American Mathematical Society 205 (1975), 247–262. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• H. Rademacher, Über partielle und totale Differenzierbarkeit von Funktionen mehrerer Variabeln und über die Transformation der Doppelintegrale, Mathematische Annalen 79 (1919), 340–359. https://doi.org/10.1007/BF01498415

Motivation

Service parts networks (spare parts for aircraft, military systems, industrial equipment) hold stock at several echelons: a depot, intermediate stocking facilities, and bases or warehouses that face demand. Two questions recur in their planning. First, how should a given amount of stock be split among locations whose expected costs are convex in the stock they hold? Second, does adding an echelon, a depot that pools the demand of several warehouses, raise or lower the stock the system needs?

Chapter 7 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879), treats both. For the second it follows Eppen and Schrage (1981, reference [78] of the book): with normal demands, a depot that places orders every period and allocates stock so that all warehouses face the same stockout probability reduces the choice of system stock to a single critical-fractile equation. For the first, the chapter's multi-echelon pooling model (Section 7.3) evaluates nested cost functions of the form "holding and shortage cost plus the minimum over allocations of a sum of convex costs", and its appendix (Section 7.4) gives the marginal allocation algorithm AllocOpt that computes these minima exactly for every stock level at once.

Marginal analysis for separable convex resource allocation is classical (Fox, Management Science, 1966); the monograph of Ibaraki and Katoh (MIT Press, 1988) surveys it.

Setting

Allocation data (Section 7.4). There is a set $M = \{1, \dots, \bar M\}$ of locations and an augmented set $M_0 = \{0\} \cup M$. Each location $m \in M_0$ has integer gridpoints $0 = r^m_0 < r^m_1 < \dots < r^m_{n(m)}$. For $m \in M$, the value $c^m_n$ of a convex function is given at each gridpoint. The slopes (7.19) are $\hat c^m_n = (c^m_{n+1} - c^m_n)/(r^m_{n+1} - r^m_n)$ for $n < n(m)$, and $\hat c^m_{n(m)}$ repeats the last one. The piecewise linear approximation $\tilde C_m$ of (7.20)–(7.21) interpolates the values $c^m_n$ at the gridpoints and continues with slope $\hat c^m_{n(m)}$ beyond the last one. A convex function $f$ on $\mathbb R_+$ is also given.

The allocation optimization (7.22) asks, for each $n \in N_0 = \{0, \dots, n(0)\}$, for

$$c^0_n = f(r^0_n) + \min\Bigl\{ \sum_{m \in M} \tilde C_m(r_m) : r_m \ge 0 \text{ integer},\ \sum_{m \in M} r_m = r^0_n \Bigr\}.$$

Algorithm AllocOpt (Definition 4) keeps a current gridpoint index $n^*(m)$ and allocation $r^*(m)$ per location. For each increment $r^0_n - r^0_{n-1}$ of the target, it repeatedly gives units to a location $m^*$ whose current slope $\hat c^{m^*}_{n^*(m^*)}$ is minimal, up to that location's next gridpoint, and records the accumulated cost.

Pooling system (Section 7.2.1). One depot supplies $m$ warehouses. The demand $d_{jt}$ at warehouse $j$ in period $t$ is normal with mean $\mu_j$ and variance $\sigma_j^2$, independent across periods and warehouses. The supplier-to-depot lead time is $D$ periods, the depot-to-warehouse lead time $A$ periods, and holding and backorder costs $h, b$ are equal at all warehouses. Positions $I_j$ are in balance when $\Phi((I_j - A\mu_j)/(\sqrt A\,\sigma_j))$ is the same for all $j$. For system inventory position $s$, with $Y_0$ the system demand over $D$ periods and $Y_j$ the demand at $j$ over the next $A + 1$ periods, the balanced allocation gives each warehouse a share proportional to $\sigma_j$, and $z_j$ is its end-of-period net inventory.

Formalization targets

Goal: Proposition 2 (correctness)

For every tie-breaking rule in its arg min steps, AllocOpt returns values $c^0_n$ that satisfy (7.22) for every $n \in N_0$: some feasible integer allocation attains $c^0_n - f(r^0_n)$, and no feasible integer allocation does better.

Milestones

1. Slope monotonicity (p. 178): $\hat c^m_n \ge \hat c^m_{n-1}$ for $0 < n \le n(m)$.
2. Convexity of $\tilde C_m$ on $[0, \infty)$ (proof of Proposition 2, p. 179).
3. Remark 2 (p. 179): with the inner loop run only while the current slope is $\le 0$, AllocOpt solves (7.22) with $\sum_m r_m \le r^0_n$.
4. Lemma 3 (p. 152): if the positions are in balance and

$$\sum_{j} d_{j,t-1} \ge \max_{i} \Bigl\{ \sum_{j \ne i} d_{j,t+D-1} + d_{i,t+D-1}\Bigl(1 - \frac{\sum_j \sigma_j}{\sigma_i}\Bigr)\Bigr\},$$

then a nonnegative allocation of the arriving $\sum_j d_{j,t-1}$ units restores balance. 5. Net inventory law (pp. 156–157): $z_j$ is normal with mean $(s - (D + A + 1)\sum_i \mu_i)\,\sigma_j / \sum_i \sigma_i$ and variance $(A + 1)\sigma_j^2 + (\sigma_j / \sum_i \sigma_i)^2 D \sum_i \sigma_i^2$. 6. Critical fractile (pp. 157–158): $s$ minimizes $\sum_j E[h (z_j)^+ + b (z_j)^-]$ if and only if $\Phi(z) = b/(b+h)$, where

$$z = \frac{s - (D + A + 1)\sum_i \mu_i}{\bigl[(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2\bigr]^{1/2}}.$$

Significance

The goal certifies an algorithm that the chapter uses as a subroutine three times: in the pool cost (7.14), the subsystem cost (7.15) and the system cost (7.17), and hence in the claim of Section 7.3 that the system-wide cost function can be computed in time $n \log n$ in the number of locations. Because AllocOpt produces the whole vector $(c^0_n)_{n \in N_0}$ in one pass, its correctness gives the nested value functions at every gridpoint of the next echelon, which is what allows the recursion up the echelons. The Eppen–Schrage milestones give the classical quantitative form of risk pooling: the system stock is set by one critical fractile, and the standard deviation term $(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2$ is what the book compares with the single-warehouse and the decentralized systems.

On formalization: the book states Proposition 2 with a two-sentence argument and Remark 2 without proof. The Eppen–Schrage computations are displayed derivations. None of these results has a machine-checked proof on the platform. A verified AllocOpt, stated for an explicit algorithm rather than for an abstract greedy procedure, is reusable for any separable convex integer allocation with a sum constraint.

Difficulty

The usual greedy exchange argument assumes that units are allocated one at a time. AllocOpt allocates in blocks, up to the next gridpoint of the chosen location, and it carries its state across successive targets $r^0_{n-1} \to r^0_n$ without restarting. The proof must therefore show that the state after each outer step is itself an optimal allocation for the current target, and that block moves never step past a breakpoint where the arg min would change. The slopes can be negative, and the equality constraint forces allocation even when every marginal cost is positive. Remark 2 needs an additional argument: under the inequality constraint the loop may stop before $u$ reaches zero, and that point is optimal only because the slopes are nondecreasing.

For the pooling results, the balanced allocation mixes the depot-lead-time demand $Y_0$ of all warehouses with the local demand $Y_j$, and the Gaussian law of $z_j$ rests on the independence of disjoint blocks of periods. The fractile statement requires strict monotonicity of each warehouse's expected cost derivative in $s$, not only a first-order condition.

Formalization scope

• Indices and types. Locations of $M$ are Fin Mbar; gridpoints are integers, values and slopes real numbers; allocations are functions Fin Mbar → ℕ. The standing assumptions of Section 7.4 form the predicate WellFormed: $\bar M \ge 1$, $n(m) \ge 1$ for $m \in M$ (a slope (7.19) needs two gridpoints), gridpoints starting at $0$ and strictly increasing at every location of $M_0$, each $c^m_n$ the value of a function convex on $[0, \infty)$, and $f$ convex on $[0, \infty)$.
• The minimum in (7.22) is stated as attainment plus a lower bound over the finite, nonempty set of feasible integer allocations, never as an unconstrained infimum.
• Ties. The book's arg min fixes no tie-breaking rule. Results are stated for every selection rule that returns a minimizing location.
• Termination. AllocOpt is a total Lean function. The inner loop is given more passes than it can use, so it always exits through its own condition.
• Not stated. The operation count of Proposition 2, $O((1 + \log_2 \bar M)\sum_{m \in M_0} n(m))$, and Proposition 1 and Remark 1 (p. 177) are operation counts with no machine model and are left out.
• Corrections. The first expected-cost display on p. 157 has $+\,b\int_{-\infty}^0 z\,dF_{z_j}(z)$, which is negative. The formalization uses $b\,E[(z_j)^-]$, as in the book's next display.
• Pinnings. Lemma 3 is deterministic: the demands are arbitrary reals, and "in balance following the allocation" means that some $x_j \ge 0$ with $\sum_j x_j = \sum_j d_{j,t-1}$ exists. The critical-fractile milestone is the characterization "minimizer if and only if $\Phi(z) = b/(b+h)$" of the book's "can be found by setting".
• Trivialization ruled out. The allocation problem (7.22) is defined independently of the algorithm, as a minimum over explicit integer allocations, and the $\tilde C_m$ are built from the data by (7.19)–(7.21). Neither (7.22) nor the $\tilde C_m$ are defined as, or required to agree with, what AllocOpt returns.
• Welcome contributions. Lemmas on the invariants of AllocOpt, in particular that after each outer step the allocation $r^*$ is feasible for $r^0_n$ with cost $z$ and all slopes to the left of $n^*(m)$ are at most those to the right. Also Gaussian sum lemmas over finite index sets and a general newsvendor first-order characterization.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005. DOI 10.1007/b138879
• G. D. Eppen and L. Schrage, "Centralized ordering policies in a multi-warehouse system with lead times and random demand", in L. B. Schwarz (ed.), Multi-Level Production/Inventory Control Systems: Theory and Practice, Studies in the Management Sciences, North-Holland, Amsterdam, 1981, pp. 51–67.
• G. D. Eppen, "Effects of centralization on expected costs in a multi-location newsboy problem", Management Science 25(5), 1979, 498–501. DOI 10.1287/mnsc.25.5.498
• B. Fox, "Discrete optimization via marginal analysis", Management Science 13(3), 1966, 210–216. DOI 10.1287/mnsc.13.3.210
• T. Ibaraki and N. Katoh, Resource Allocation Problems: Algorithmic Approaches, MIT Press, 1988.

Motivation

Two-stage stochastic integer programs combine the two hardest features of mathematical programming: uncertainty in the data and integrality of the decisions. Even evaluating the objective of such a program at a single first-stage decision requires the expected optimal value of an NP-hard combinatorial problem. Chapter 8 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by A. H. G. Rinnooy Kan and L. Stougie, argues that for many such problems the way forward is probabilistic analysis: the random optimal value of the second-stage problem often converges, after normalization, to a simple function of the problem parameters, and that function can replace the intractable expectation.

The chapter illustrates this on the machine investment problem: first buy $m$ identical machines at cost $c$ each, knowing only the distribution of the processing times of $n$ jobs, then schedule the jobs once their processing times are revealed so as to minimize the makespan. This mission formalizes the chapter's analysis of that example: the almost sure asymptotics of the optimal makespan (8.13), its expectation version, and the asymptotic clairvoyance of the resulting two-stage heuristic.

Setting

Let $p_1, p_2, \dots$ be processing times: independent, identically distributed, nonnegative random variables on a probability space $(\Omega, \mathcal F, P)$ with mean $\mu = \mathbb E p_1 > 0$ and finite second moment $\mathbb E p_1^2 < \infty$. The instance with $n$ jobs uses the first $n$ of them.

An assignment of the $n$ jobs to $m \ge 1$ identical machines is a map $\sigma : \{1, \dots, n\} \to \{1, \dots, m\}$. The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ and the makespan of $\sigma$ is its largest load. The minimum makespan is

$$C^*_n(m) = \min_{\sigma} \max_{i=1,\dots,m} \sum_{j:\ \sigma(j) = i} p_j ,$$

and the machine investment problem is to minimize $Z_n(m) = cm + \mathbb E\, C^*_n(m)$ over integers $m$ (8.9).

List scheduling takes the jobs in the order $1, \dots, n$ and assigns each to the first available machine, a machine of least current load (lowest index on ties). Its makespan is $C^H_n(m)$. Write $S_n = \sum_{j=1}^n p_j$ and $p_{\max} = \max_{j \le n} p_j$.

For §8.3, the estimate $Z'_n(m) = cm + n\mu/m$ is minimized over integers by the heuristic first-stage decision $m^{H1}_n$, the better of $\lfloor\sqrt{n\mu/c}\rfloor$ and $\lceil\sqrt{n\mu/c}\rceil$. A clairvoyant decision maker who sees the processing times first chooses $m^\circ_n(\omega) \ge 1$ minimizing $cm + C^*_n(m)$.

Formalization targets

Goal: Eq. (8.13)

For machine counts $m = m(n) \ge 1$ with $m(n) = O(\sqrt n)$,

$$P\Bigl\{ \lim_{n\to\infty} \frac{C^*_n(m)}{n\mu/m} = 1 \Bigr\} = 1 .$$

The machine count is allowed to grow with $n$; this is the regime the first-stage heuristic lives in, since $m^{H1}_n$ is of exact order $\sqrt n$.

Milestones

1. Eq. (8.10): the deterministic sandwich $S_n/m \le C^*_n(m) \le C^H_n(m) \le S_n/m + p_{\max}$, divided by $n\mu/m$.
2. Eq. (8.11): the strong law of large numbers, $(S_n - n\mu)/(n\mu) \to 0$ almost surely (a published platform theorem).
3. Lemma 8.1 (i): $p_{\max}/\sqrt n \to 0$ almost surely.
4. Eq. (8.12): $m\, p_{\max}/(n\mu) \to 0$ almost surely when $m = O(\sqrt n)$.
5. Lemma 8.1 (ii): $\mathbb E\, p_{\max}/\sqrt n \to 0$.
6. p. 207: $\mathbb E\, C^*_n(m)/(n\mu/m) \to 1$ when $m = O(\sqrt n)$.
7. p. 211, asymptotic clairvoyance: almost surely

$$\lim_{n\to\infty} \frac{c\, m^{H1}_n + C^{H2}_n(m^{H1}_n)}{c\, m^\circ_n + C^*_n(m^\circ_n)} = 1 ,$$

where $C^{H2}_n$ is the list-scheduling makespan.

Significance

Result (8.13) says that the optimal value of an NP-hard problem, rescaled, is almost surely asymptotic to the elementary function $n\mu/m$ of the data and the first-stage decision. Its expectation version replaces the intractable term $\mathbb E\,C^*_n(m)$ in (8.9) by $n\mu/m$, and the clairvoyance statement shows that the heuristic built on that replacement loses asymptotically nothing, not even against a decision maker with full information. The chapter presents the example as the template for vehicle routing and location problems preceded by an investment decision.

All results here are classical and proved in the literature cited by the chapter (Lemma 8.1 is quoted from Feller without proof; the chapter refers to Dempster et al. for the asymptotic optimality of the two-stage heuristic and to Lenstra et al. for the notion of asymptotic clairvoyance). None of them has, to our knowledge, a machine-checked proof. The mission produces a formal model of identical-machine makespan scheduling and of list scheduling, the extreme-value estimates of Lemma 8.1 for square-integrable i.i.d. sequences, and the full chain from the strong law to (8.13).

Difficulty

The deterministic part is elementary on paper, but list scheduling is a recursively defined procedure, and its makespan bound has to be established for that recursion rather than for a picture like the chapter's Figure 8.3. The probabilistic core is Lemma 8.1: the strong law controls $S_n/n$, but the error term $m\, p_{\max}/(n\mu)$ is of order $p_{\max}/\sqrt n$ once $m$ grows like $\sqrt n$, and the strong law says nothing about maxima. With a fixed number of machines the whole statement would reduce to the strong law; the growth $m(n) = O(\sqrt n)$ is exactly where the second moment is needed. For the clairvoyance statement, the clairvoyant choice $m^\circ_n$ is a random, unstructured minimizer, so its value must be bounded below without knowing where the minimum is attained.

Formalization scope

Processing times are one sequence p : ℕ → Ω → ℝ, 0-based (the book's $p_j$ is p (j-1)), with each p j measurable, the family mutually independent (iIndepFun), identically distributed with p 0, pointwise nonnegative, p 0 ^ 2 integrable and ∫ p 0 = μ with μ > 0. Nonnegativity and $\mu > 0$ are not printed in the book; they are implicit in "processing times" and in the division by $n\mu$. Machines are Fin m; a schedule is an assignment Fin n → Fin m, which is faithful because jobs are non-preemptive, machines identical and there are no precedence constraints.

The book writes "$m = 0(\sqrt n)$"; this is read as $m$ a function of $n$ with $m(n) \ge 1$ and (fun n => (m n : ℝ)) =O[atTop] (fun n => √n). Stating (8.13) for a fixed $m$ would trivialize it into the strong law and is ruled out. "$\Pr\{\lim \dots = 1\} = 1$" means that almost surely the limit exists and equals $1$. Expectations are Bochner integrals of functions that are measurable and bounded by $S_n$, hence integrable. List scheduling uses the index order and breaks ties towards the lowest machine index; both are admissible instances of the book's "arbitrary fixed order" and "first available machine". In the clairvoyance statement the minimum is over $m \ge 1$ (the book writes $m \in \mathbb N$; no machine cannot process any job, and the Lean value $C^*_n(0)$ is an empty-infimum convention). No explicit constants replace an O(·): the statements are limits and the O-hypothesis is carried as stated.

Out of scope: (8.14) and the p. 210 expectation statement, which need a positive density at $0$ and whose proof the book calls "far from easy", and the dynamic programming recursion of §8.3.

Needed infrastructure: finite maxima and minima of measurable functions, extreme-value estimates for square-integrable i.i.d. sequences (Lemma 8.1), and Mathlib's strong law. The makespan and list-scheduling definitions are reusable for other identical-machine scheduling results; alternative proofs of Lemma 8.1 and sharper forms of the clairvoyance statement are welcome.

Selected references

• A. H. G. Rinnooy Kan, L. Stougie, "Stochastic Integer Programming", in Yu. Ermoliev, R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 8, pp. 201–213. https://doi.org/10.1007/978-3-642-61370-8
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, 3rd edition, Wiley, 1968 (cited by the chapter for Lemma 8.1).
• M. A. H. Dempster, M. L. Fisher, L. Jansen, B. J. Lageweg, J. K. Lenstra, A. H. G. Rinnooy Kan, "Analysis of heuristics for stochastic programming: results for hierarchical scheduling problems", Mathematics of Operations Research 8 (1983) 525–537. https://doi.org/10.1287/moor.8.4.525
• J. K. Lenstra, A. H. G. Rinnooy Kan, L. Stougie, "A framework for the design and analysis of hierarchical planning systems", Annals of Operations Research 1 (1984) 23–42. https://doi.org/10.1007/BF01874451
• R. L. Graham, "Bounds on multiprocessing timing anomalies", SIAM Journal on Applied Mathematics 17 (1969) 416–429. https://doi.org/10.1137/0117039

Motivation

Many optimization problems in operations research have an objective that is an expectation, $F^0(x)=E f^0(x,\omega)$, over a random parameter $\omega$ whose distribution is known only through samples or is too complex to integrate. Two-stage stochastic programs, inventory and reliability models, and simulation-based design all have this form. Neither $F^0$ nor its subgradients can be evaluated exactly, but a random vector whose conditional mean is close to a subgradient is often cheap to compute: a sample subgradient of $f^0(\cdot,\omega)$, or a finite-difference quotient of two sampled values.

Stochastic quasigradient (SQG) methods, developed by Ermoliev and co-workers in Kiev from the late 1960s, use such vectors in place of subgradients. They extend the stochastic approximation procedures of Robbins–Monro (1951) and Kiefer–Wolfowitz (1952) to nonsmooth convex objectives, general convex constraints, and directions whose conditional mean is biased by a vanishing amount. This mission formalizes the basic convergence theory of the simplest SQG method, the projection method, as presented by Yu. Ermoliev in Chapter 6 of the IIASA volume Numerical Techniques for Stochastic Optimization (Springer 1988).

Timeline (as cited in the chapter's bibliography).

• 1951–1954: Robbins and Monro, Kiefer and Wolfowitz, Dvoretzky and Blum prove convergence of stochastic approximation for unconstrained smooth problems.
• 1962–1967: Shor introduces the generalized gradient (subgradient) method; Ermoliev (Kibernetika 4, 1966) and Polyak (Soviet Math. Doklady 8, 1967) prove its convergence.
• 1967–1969: Ermoliev and Nekrylova introduce stochastic subgradients; Ermoliev ("On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2, 1969) introduces stochastic quasi-Féjer sequences.
• 1976: Ermoliev's monograph Stochastic Programming Methods (Nauka) contains the proof of Theorem 6.1 (p. 98).
• 1988: the survey chapter formalized here presents the projection method, Theorems 6.1 and 6.2, and an efficiency estimate for the averaged iterate.

Setting

Let $X\subseteq\mathbb R^n$ be a nonempty convex compact set and $F^0:\mathbb R^n\to\mathbb R$ convex and continuous on $X$. The optimal set is $X^*=\{x\in X: F^0(x)\le F^0(y)\ \forall y\in X\}$. The projection onto $X$ is $\pi_X(y)=\operatorname{argmin}\{\|y-x\|^2:x\in X\}$.

On a probability space, the stochastic quasigradient projection method produces random vectors $x^0,x^1,\dots$ by

$$x^{s+1}=\pi_X\big[x^s-\rho_s\,\xi^0(s)\big],\qquad s=0,1,\dots \tag{6.11}$$

where $\rho_s\ge0$ is a step size and $\xi^0(s)$ a random direction. Write $E\{\cdot\mid x^0,\dots,x^s\}$ for conditional expectation given the history $\sigma(x^0,\dots,x^s)$. The direction is a stochastic quasigradient if, for every $x^*\in X^*$,

$$F^0(x^*)-F^0(x^s)\ge\big\langle E\{\xi^0(s)\mid x^0,\dots,x^s\},\,x^*-x^s\big\rangle+\gamma_0(s)\quad\text{a.s.}, \tag{6.12}$$

where the error $\gamma_0(s)$ is a function of the history. If the conditional mean of $\xi^0(s)$ is a subgradient plus a bias $b^0(s)$, then (6.12) holds with $\gamma^0(s)=-\langle b^0(s),x^*-x^s\rangle$ (6.13).

A sequence of random vectors $z^0,z^1,\dots$ is a stochastic quasi-Féjer sequence for $Z\subseteq\mathbb R^n$ if $E\|z^0\|^2<\infty$ and there are random $r_s\ge0$ with $\sum_s E r_s<\infty$ such that for all $z\in Z$

$$E\{\|z-z^{s+1}\|^2\mid z^0,\dots,z^s\}\le\|z-z^s\|^2+r_s. \tag{6.14}$$

Formalization targets

Goal: Theorem 6.2

If, with probability 1, $\rho_s\ge0$ and $\sum_s\rho_s=\infty$, and

$$\sum_{s=0}^\infty E\{\rho_s|\gamma_0(s)|+\rho_s^2\|\xi^0(s)\|^2\}<\infty, \tag{6.15}$$

then with probability 1 the iterates converge and $\lim_s x^s\in X^*$.

Milestones

1. Theorem 6.1 (a)–(c). For a stochastic quasi-Féjer sequence for $Z$: $\|z-z^{s+1}\|^2$ converges a.s. and $E\|z-z^s\|^2$ is bounded, for each $z\in Z$; accumulation points exist a.s. (for $Z\ne\emptyset$); and a.s. $Z$ lies in the hyperplane equidistant from any two distinct accumulation points outside $Z$.
2. Eq. (6.13). Biased stochastic subgradients satisfy (6.12).
3. One-step inequality (p. 145): $E\{\|x^*-x^{s+1}\|^2\mid\cdot\}\le\|x^*-x^s\|^2+2\rho_s\langle E\{\xi^0(s)\mid\cdot\},x^*-x^s\rangle+E\{\rho_s^2\|\xi^0(s)\|^2\mid\cdot\}$ for $x^*\in X$.
4. Quasi-Féjer property (p. 145): the iterates of (6.11) form a stochastic quasi-Féjer sequence for $X^*$.
5. Efficiency estimate (p. 147), for deterministic $\rho_k$ and $\bar x^s=\sum_{k\le s}\rho_kx^k/\sum_{k\le s}\rho_k$:

$$E F^0(\bar x^s)-F^0(x^*)\le\Big(2\sum_{k=0}^s\rho_k\Big)^{-1}\Big[E\|x^*-x^0\|^2+\sum_{k=0}^s E\big(2\rho_k|\gamma_0(k)|+\rho_k^2\|\xi^0(k)\|^2\big)\Big].$$

Significance

Theorem 6.2 is the prototype convergence theorem for SQG methods. Its hypotheses allow random step sizes chosen from the history, nonsmooth objectives, and directions with a bias that vanishes fast enough; its conclusion is convergence of the iterates themselves to a single optimal point, not only convergence of function values or of $\operatorname{dist}(x^s,X^*)$. The later chapters of the same volume (adaptive step sizes, Chapters 17–18; nonstationary problems, §6.4) reuse the same framework. Theorem 6.1 isolates the probabilistic content in a form that applies to any algorithm with a quasi-Féjer inequality. The efficiency estimate gives a non-asymptotic accuracy bound for the averaged iterate.

The results are classical and proved in the literature: Theorem 6.1 in Ermoliev (1976, p. 98), Theorem 6.2 in this chapter (pp. 145–146). To our knowledge none of them has a machine-checked proof. Mathlib has conditional expectations and the a.s. martingale convergence theorem, but no Robbins–Siegmund-type almost-supermartingale lemma and no stochastic subgradient method. A formal proof of this mission would supply both.

Difficulty

The deterministic argument for projected subgradient methods compares $\|x^*-x^{s+1}\|$ with $\|x^*-x^s\|$ for a fixed $x^*$. In the stochastic setting this comparison holds only in conditional mean, with a perturbation $r_s$ that is random, and the distances converge only almost surely, with an exceptional null set that depends on $x^*$. Since $X^*$ is typically uncountable, "for every $x^*$, almost surely" does not immediately give "almost surely, for every $x^*$", and it is the second form that identifies a single limit. A second difficulty is that $\sum\rho_s(F^0(x^s)-F^0(x^*))<\infty$ only yields a subsequence along which $F^0$ approaches its minimum; passing from there to convergence of the whole sequence is exactly what part (c) of Theorem 6.1 is for.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The probability space is an arbitrary measurable space with a probability measure. $\pi_X$ is a chosen minimizer of $\|y-x\|^2$ over $X$ (unique for nonempty closed convex $X$). The history is the $\sigma$-algebra generated by $x^0,\dots,x^s$; $\rho_s$ and $\gamma_0(s)$ are measurable with respect to it.
• Directions $\xi^0(s)$ are integrable and random vectors are measurable; conditional expectations are Mathlib's condExp. The quasi-Féjer definition requires square integrability of every $z^s$ (implied by the book's definition when $Z\ne\emptyset$), so no conditional expectation is taken of a non-integrable function.
• $X\ne\emptyset$ and $x^0\in X$ are stated; $Z\ne\emptyset$ is added in Theorem 6.1 (b), which is false without it.
• $\gamma_0(s)$ does not depend on $x^*$; the $x^*$-dependent error of (6.13) is dominated on a bounded $X$ by $\|b^0(s)\|\operatorname{diam}X$.
• (6.15) keeps its mixed form: $\rho_s\ge0$ and $\sum\rho_s=\infty$ almost surely, and a deterministic sum of expectations (lower Lebesgue integrals) finite.
• Explicit constants. The book's "$C$" in the efficiency estimate is instantiated from its proof: $2$ on $\rho_k|\gamma_0(k)|$ and $1$ on $\rho_k^2\|\xi^0(k)\|^2$. The unspecified $C$ before the quasi-Féjer sentence is replaced by the existence of summable $r_s$.
• Typo corrections. The one-step inequality on p. 145 prints $\rho_sE\{\|\xi^0(s)\|^2\mid\cdot\}$; it is $\rho_s^2$. The efficiency estimate on p. 147 omits $E$ before the last sum; it is restored. "$\rho_k$ independent of $(x^0,\dots,x^k)$" is read as deterministic step sizes.
• A trivializing formalization is excluded: the goal does not replace $\xi^0(s)$ by an exact subgradient, does not set $\gamma_0\equiv0$, and concludes convergence of $x^s$ to a point of $X^*$ rather than $\operatorname{dist}(x^s,X^*)\to0$.
• Reusable infrastructure: a Robbins–Siegmund lemma for nonnegative almost-supermartingales, the nonexpansiveness of $\pi_X$, and Theorem 6.1 itself, which applies to any quasi-Féjer algorithm (Chapter 6 §6.4 and Chapters 17–18 of the same book). Contributions of these general lemmas are welcome.

Selected references

• Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, §6.1–6.2 (pp. 141–147). https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, "On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2 (1969) (in Russian; English translation in Cybernetics). Reference [3] of the chapter.
• Yu. Ermoliev, Stochastic Programming Methods, Nauka, Moscow, 1976 (in Russian); Theorem 6.1 is on p. 98. Reference [5] of the chapter.
• H. Robbins and D. Siegmund, "A convergence theorem for non negative almost supermartingales and some applications", in J. S. Rustagi (ed.), Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• H. Robbins and S. Monro, "A stochastic approximation method", Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

Scheduling tasks on machines owned by self-interested parties is the running example of Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001), the paper that introduced the study of mechanisms whose allocation rule is an algorithm with a computational objective. Each machine (agent) privately knows how long it needs for each task; the designer wants to minimize the make-span, the completion time of the last machine, and can only influence the agents through payments.

Without further information the designer is in a weak position: the paper shows that no mechanism approximates the optimal make-span within a factor below 2 (Theorem 4.6), and that the natural truthful mechanism, MinWork, only achieves a factor $n$. Section 5 of the paper observes that in many applications the designer learns more than the agents' reports: it can pay after the work is done and observe how long each task actually took. It introduces mechanisms with verification and shows that, with this extra information, the make-span can be minimized exactly by a strongly truthful mechanism. This mission formalizes that result, Theorem 5.1, together with the steps of its proof and the participation variant, Theorem 5.4.

Setting

There are $k$ tasks and $n$ agents. The type of agent $i$ is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive numbers, $t^i_j$ being the least time in which agent $i$ can perform task $j$. An allocation $x$ gives each task to one agent; $x^i$ is the set of tasks of agent $i$. For a type vector $t$ and for a vector $\tilde t$ of actual execution times the make-spans are

$$g(x,t) = \max_i \sum_{j\in x^i} t^i_j, \qquad g(x,\tilde t) = \max_i \sum_{j\in x^i} \tilde t_j .$$

A mechanism with verification is a pair $(x, p)$. The allocation $x(d)$ is computed from the agents' declarations $d = (d^1,\dots,d^n)$ only. Each agent then performs its tasks, in any times $\tilde t_j \ge t^i_j$ it chooses, and the mechanism pays agent $i$ the amount $p^i(d, \tilde t)$, which may depend on the declarations and on the observed actual times. Agent $i$'s utility is $p^i(d,\tilde t) - \sum_{j \in x^i} \tilde t_j$. A strategy of agent $i$ therefore has two parts: a declaration $d^i$ and an execution plan $e^i$ that says, for every allocation, how long the agent takes on each of its tasks.

A strategy is dominant if it maximizes the agent's utility against all declarations and all execution plans of the other agents. The mechanism is truthful if, for every agent and type, declaring the true type (with a suitable execution plan) is dominant, and strongly truthful if the only dominant strategy is to declare the true type and to execute every task in minimal time.

The Compensation-and-Bonus mechanism uses an optimal allocation algorithm $x(\cdot)$ and pays

$$p^i(d,\tilde t) = \underbrace{\sum_{j \in x^i(d)} \tilde t_j}_{\text{compensation } c^i} \;\underbrace{-\, g\big(x(d), \mathrm{corr}^i(x(d), d, \tilde t)\big)}_{\text{bonus } b^i},$$

where the corrected time vector $\mathrm{corr}^i$ lists agent $i$'s own tasks at their actual times and every other task at the time declared by the agent it was given to.

Formalization targets

Goal: Theorem 5.1

For $n \ge 2$ agents and every optimal allocation algorithm (ties broken arbitrarily), the Compensation-and-Bonus mechanism is a strongly truthful implementation of task scheduling:

$$\text{strongly truthful} \quad\text{and}\quad g\big(x(D), \tilde t\big) \le \min_y g(y, t) \text{ whenever every agent plays a dominant strategy for its true type.}$$

Milestones (proof of Claim 5.2)

1. The utility of every agent equals its bonus.
2. For every allocation, the bonus of agent $i$ is maximized by executing its tasks in minimal time.
3. With $t = (d^{-i}, t^i)$, for every declaration $t'^i$,

$$-g\big(x(t), \mathrm{corr}^*(x(t), t)\big) \ge -g\big(x(t'^i, d^{-i}), \mathrm{corr}^*(x(t'^i, d^{-i}), t)\big).$$

4. Declaring the true type and executing in minimal time is dominant.
5. Claim 5.2: the mechanism is strongly truthful.

Further target: Theorem 5.4

For $n \ge 2$ there is a strongly truthful mechanism with an optimal allocation algorithm that satisfies participation constraints: an agent that performs its tasks in its declared times never ends with negative utility.

Significance

The result. Theorem 5.1 shows that the lower bound of 2 for task scheduling (Theorem 4.6) is an artefact of the information structure, not of incentives as such: once execution times are observable, the exact optimum is achievable in dominant strategies, and the agents have a unique rational behaviour. The construction also isolates a general principle, used again in §5.6 of the paper: an agent paid by the global objective value, computed with the others' declarations, has the designer's incentives. Theorem 5.4 shows that the bonus can be shifted to make participation individually rational, which the plain mechanism violates (its bonus is negative).

Formalizing it. The theorem is proved in the paper, in a few lines, and has no machine-checked version. A formalization has to settle what the paper leaves informal: what a strategy with an execution part is, over which strategies of the others dominance is quantified, what "the only dominant strategy" demands of the execution plan on allocations that seem never to arise, and which hypotheses on the number of agents the uniqueness needs. The model built here is also the base of two companion missions of the same series (Compensation-and-Bonus with a non-optimal allocation algorithm, and the rounding mechanism with verification).

Difficulty

Truthfulness (milestones 1–4) is short once the model is right. The difficulty is uniqueness. For a misreport or a slow execution to be excluded, one must exhibit, for every alternative strategy, declarations of the other agents under which that strategy is strictly worse. The declarations must be positive, the optimal allocation algorithm breaks ties arbitrarily, and agent $i$'s slower execution only hurts it when agent $i$ is the bottleneck. The paper's proof dismisses this step with "clearly, … there are circumstances"; the naive reading ("the others declare $+\infty$ elsewhere") is not available in a model with finite positive times, and the uniqueness clause must also cover the execution plan on every allocation, not only on the allocation produced by truthful play.

Formalization scope

• Agents are Fin n, tasks Fin k, allocations functions Fin k → Fin n; both make-spans are Finset.sup' over the nonempty set of agents ([NeZero n]).
• Types and declarations are positive real vectors; declarations range over this type space (Definition 18's "unrestricted" declaration is any element of it).
• An execution plan is a function from allocations to actual times; feasibility for type $t^i$ requires $\tilde t_j \ge t^i_j$ on the agent's own tasks only. In the dominance quantifier the other agents' plans are arbitrary.
• Payments are amounts handed to the agent; utility is quasi-linear.
• The optimal allocation algorithm is a parameter with the hypothesis that it minimizes $g(\cdot, d)$ on every positive $d$; every theorem holds for every such algorithm.
• Strong truthfulness constrains both parts of the strategy: the declaration equals the type, and the plan executes every task in minimal time under every allocation.
• Thresholds made explicit: $n \ge 2$ in Claim 5.2, Theorem 5.1 and Theorem 5.4 (not printed; with one agent every declaration is dominant, and the construction of Theorem 5.4 needs a second agent).
• Printed slips: the displayed inequality prints >=; Theorem 5.4 prints "strongly truthfulmechanism"; Definition 28 writes $\tilde t_j = t_j$ for $\tilde t_j = t^i_j$.
• Running time is out of scope.
• A formalization in which dominance is checked only against truthful other agents, in which the mechanism ignores executions, in which strong truthfulness constrains only the declaration, or in which the implementation clause is stated only at the truthful profile, is not the theorem and is ruled out by the statements.

Welcome contributions: proofs of the milestones, the uniqueness witnesses as reusable lemmas, and the contribution-based mechanism behind Theorem 5.4. Theorem 5.3 (generalized Compensation-and-Bonus) is not stated in this mission.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995.

Motivation

Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) asks how well a computational task can be carried out when its inputs are held by self-interested agents who may lie about them. Their test case is scheduling on unrelated machines: tasks must be assigned to agents (machines), each agent privately knows how long it needs for each task, and the planner wants to minimize the time at which the last agent finishes. The paper shows that the mechanism MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is truthful and loses a factor of at most $n$ against the optimum, and that no truthful mechanism can do better than a factor $2$. It then conjectures (Conjecture 4.9) that the factor $n$ cannot be improved by any truthful mechanism.

That conjecture became the Nisan–Ronen conjecture, one of the central questions of algorithmic mechanism design. A sequence of papers raised the general lower bound from $2$ to $1 + \sqrt 2$ (Christodoulou, Koutsoupias and Vidali), to $1 + \varphi \approx 2.618$ (Koutsoupias and Vidali) and to larger constants, and Christodoulou, Koutsoupias and Kovács (STOC 2023) finally proved the conjecture for all deterministic truthful mechanisms. In the original paper, Nisan and Ronen confirm the conjecture for two restricted classes of mechanisms, with short direct arguments. This mission concerns the second class, local mechanisms (Theorem 4.12).

Setting

There are $k$ tasks $j \in \{1, \dots, k\}$ and $n$ agents $i \in \{1, \dots, n\}$. A type vector $t$ records, for every agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks of agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j \in X} t^i_j$. The make-span of $x$ is $g(x, t) = \max_i t^i(x^i)$.

A direct mechanism $(x, p)$ asks every agent for its type, computes an allocation $x(t)$ from the declarations, and hands agent $i$ the payment $p^i(t)$. Agent $i$'s utility is $p^i(t) - t^i(x^i(t))$ measured with its true times. The mechanism is truthful if declaring the true type maximizes each agent's utility whatever the other agents declare. The allocation rule is a $c$-approximation if $g(x(t), t) \le c \cdot g(y, t)$ for every type vector $t$ and every allocation $y$.

For a truthful mechanism the payment to agent $i$ depends only on the set it receives and on the declarations $t^{-i}$ of the others (Proposition 4.4). This gives the price offered to agent $i$ for a set $X$ (Definition 12):

$$p^i(X, t^{-i}) = \begin{cases} p^i(t'^i, t^{-i}) & \text{if some } t'^i \text{ gives } x^i(t'^i, t^{-i}) = X, \\ 0 & \text{otherwise.} \end{cases}$$

A mechanism is local (Definition 14) if $p^i(X, t^{-i})$ depends only on the other agents' times $\{t^l_j : l \ne i, j \in X\}$ on the tasks of $X$. MinWork is local: its price for $X$ is $\sum_{j \in X} \min_{l \ne i} t^l_j$.

Formalization targets

Goal: Theorem 4.12

For every $n \ge 1$, every $k \ge n^2$ and every real $c < n$, no truthful local mechanism is a $c$-approximation:

$$\forall (x, p) \text{ truthful and local},\ \forall c < n:\quad \exists\, t,\ y \quad g(x(t), t) > c \cdot g(y, t).$$

The bound holds for every $c < n$, so together with MinWork it shows that $n$ is the exact best ratio for local truthful mechanisms.

Milestones

1. Proposition 4.4 (Independence). Payments depend only on the allocated set and on $t^{-i}$.
2. Proposition 4.5 (Maximization). $x^i(t)$ maximizes $p^i(X, t^{-i}) - t^i(X)$ over the sets $X$ that agent $i$ can obtain.
3. Lemma 4.13. Every type vector has type vectors arbitrarily close to it at which each agent's maximizing set is unique.
4. Claim 4.14, first step. If $x^i(t)$ is the unique maximizer, lowering agent $i$'s times on $x^i(t)$ keeps $x^i(t)$.
5. Ratio step. An allocation that gives one agent $n$ tasks of time about $1$, while every other agent's own tasks are nearly free, has make-span about $n$, while splitting those $n$ tasks gives make-span about $1$.

Significance

The result. Theorem 4.12 settles the Nisan–Ronen conjecture for a natural class of mechanisms. Locality captures the mechanisms in which the price for a bundle of tasks is set only by the competition for those tasks. It includes MinWork and, more generally, every mechanism that prices tasks separately using the other agents' bids on them. The theorem says that for this class the trivial per-task auction is already optimal, so any improvement over the ratio $n$ must use prices that depend on the other agents' times on tasks outside the bundle.

Formalizing it. The statement is not open: it follows from the 2023 proof of the Nisan–Ronen conjecture, and Nisan and Ronen's own argument is much shorter. That argument is a sketch, though. Lemma 4.13 rests on an informal measure-theoretic appeal, and the core claim relies on a maximization property stated over all sets of tasks. A machine-checked proof pins down exactly which properties of truthful mechanisms the short argument needs. None of these results is known to have been formalized. The definitions (type vectors, truthful mechanisms, prices, locality) are shared with the other missions of this series.

Difficulty

An argument that looks at one agent at a time does not go through. Changing one agent's declaration changes the prices offered to every other agent, so an allocation that is stable for one agent can shift for another. The argument needs a type vector at which every agent's choice is strict, and only then can it lower times agent by agent and follow the allocation. Producing such a type vector is Lemma 4.13. The printed argument for it applies a "for almost every type vector" statement to sets defined by the price functions of an arbitrary mechanism, which need not be measurable. A proof must therefore work without any regularity of the mechanism. A second difficulty is Definition 12's convention that a set the agent cannot obtain has price $0$. Locality constrains these zero prices too, and the argument has to account for sets that are obtainable at one type vector and not at a nearby one.

Formalization scope

Agents are Fin n, tasks Fin k. An allocation is a function Fin k → Fin n, a type vector is Fin n → Fin k → ℝ, and a mechanism is a pair of functions alloc (declarations to allocation) and pay (declarations to the payment handed to each agent). Utilities are quasi-linear. All types, declarations and misreports are positive, and every truthfulness, locality and approximation quantifier ranges over positive type vectors. The make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]).

Conventions and explicit thresholds:

• $k \ge n^2$. The theorem is printed without a bound on the number of tasks, and its proof begins "Let $k \ge n^2$". The goal carries $k \ge n^2$ as a hypothesis.
• Truthfulness is assumed. §4.3 assumes throughout that the mechanism is truthful (by the revelation principle this is no loss). The goal quantifies over all truthful local mechanisms.
• Prices use Definition 12 literally, including the value $0$ for sets the agent cannot obtain, and locality is Definition 14 applied to that price function over all sets $X$, not only single tasks. When several declarations give the same set, the price uses one chosen witness; by Proposition 4.4 the choice does not matter for truthful mechanisms.
• Proposition 4.5 is stated over the sets the agent can obtain. As printed, over all subsets, it is false for a truthful mechanism that never leaves an agent idle and pays it negative amounts. Uniqueness of maximizers (Lemma 4.13, Claim 4.14) refers to the same family.
• Lemma 4.13 uses Mathlib's norm on Fin n → Fin k → ℝ, the sup norm. No measurability of the mechanism is assumed.
• Claim 4.14 is printed at $t^i_j = 1$ with $0 < \varepsilon < 1$. The first step is stated at any type vector, with $0 < \varepsilon \le t^i_j$ on the lowered tasks.
• Running time and computability are out of scope.

Ruled-out trivializations: locality is not restricted to single tasks; the goal does not assume that maximizers are unique at every type vector (that is Lemma 4.13's conclusion at one point, not a hypothesis); and the bound holds for every $c < n$, not for some.

Needed infrastructure: finite sums over allocation fibres, sup norms on function spaces, and a genericity argument for finitely many affine functions (Lemma 4.13). The model file and the price and locality definitions are reusable in the other missions of the series. Proofs of individual milestones are welcome independently.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (pp. 876–880, basic properties of truthful mechanisms).
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.