Optimization

Motivation

Online convex optimization models repeated decision making against an adversary: in each round a player chooses a point of a convex set, and only then learns the convex cost of that round. It covers online portfolio selection, online regression and routing, and it is the standard lens for analysing learning algorithms that must commit before seeing data. The figure of merit is regret, the player's total cost minus the cost of the best fixed decision in hindsight. For general convex costs regret $\Theta(\sqrt T)$ over $T$ rounds is optimal; for costs with curvature it can be logarithmic.

Hazan, Agarwal and Kale (Mach Learn 69 (2007) 169–192) gave several algorithms with $O(\log T)$ regret for $\alpha$-exp-concave costs, the class that contains the log-loss of portfolio selection. This mission formalizes one of them, Follow the Approximate Leader (FTAL). It connects to the oldest online algorithm, Follow the Leader (FTL), which plays the minimiser of all past costs: FTAL is FTL run on quadratic lower models of the costs, and the paper's analysis shows that FTL itself has logarithmic regret on a class of curved costs.

Timeline. Zinkevich (2003) proved $O(\sqrt T)$ regret for online gradient descent on convex costs. Cover (1991) gave a universal portfolio with logarithmic regret for the log-loss, at a running time exponential in the dimension. Kalai and Vempala (2005) analysed perturbed Follow the Leader through the "be the leader" argument. Hazan, Agarwal and Kale (2007) gave efficient algorithms (Online Newton Step, FTAL, EWOO) with $O(n \log T)$ regret for exp-concave costs.

Setting

The decision set $P \subseteq \mathbb{R}^n$ is nonempty, convex, closed and bounded, and $D$ bounds its diameter: $\|y - z\|_2 \le D$ for $y, z \in P$. In rounds $t = 1, 2, \dots$ the player picks $x_t \in P$ and then pays $f_t(x_t)$, where $f_t$ is a cost function differentiable at the points of $P$ with gradient norm $\|\nabla f_t(x)\| \le G$ on $P$. The cost $f_t$ is $\alpha$-exp-concave ($\alpha > 0$) if $x \mapsto \exp(-\alpha f_t(x))$ is concave on $P$. The regret over $T$ rounds against a comparator $u \in P$ is $\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr)$.

Follow the Leader plays $x_t \in \arg\min_{x \in P} \sum_{\tau=1}^{t-1} f_\tau(x)$ (any point of $P$ in round 1). Follow the Approximate Leader (version 1 of the paper's Fig. 3) with parameter $\beta$ plays FTL on the approximate costs

$$\tilde f_\tau(x) = f_\tau(x_\tau) + \nabla_\tau^\top(x - x_\tau) + \frac{\beta}{2}(x - x_\tau)^\top \nabla_\tau\nabla_\tau^\top (x - x_\tau), \qquad \nabla_\tau = \nabla f_\tau(x_\tau).$$

In the Lean development these are IsFTLRun P f x and IsFTALRun P β f x, predicates on a whole trajectory $x$.

Formalization targets

Goal: Theorem 6

With $\beta = \tfrac12 \min\{1/(4GD), \alpha\}$, every FTAL run on $\alpha$-exp-concave costs satisfies, for every $T \ge 1$ and $u \in P$,

$$\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr) \le 64\left(\frac1\alpha + GD\right) n\,(\log T + 1).$$

This is the paper's statement with its constant, stated for the algorithm as defined, and for every adversarial sequence of costs.

Milestones

1. Lemma 3: an $\alpha$-exp-concave cost with gradients bounded by $G$ lies above the paraboloid $f(y) + \nabla f(y)^\top(x-y) + \frac\beta2 (\nabla f(y)^\top (x - y))^2$ on $P$.
2. Lemma 9: regret on lower surrogates that touch the costs at the played points dominates the true regret.
3. Lemma 10: $\sum_t f_t(x_{t+1}) \le \sum_t f_t(u)$ for an FTL run ("be the leader").
4. Lemma 12: $A^{-1} \bullet (A - B) \le \log(|A|/|B|)$ for $A \succeq B \succ 0$.
5. Lemma 11: $\sum_{t=1}^T u_t^\top V_t^{-1} u_t \le n\log(r^2T/\varepsilon + 1)$ with $V_t = \sum_{\tau \le t} u_\tau u_\tau^\top + \varepsilon I$.
6. Theorem 5 (corrected constant): FTL on costs $g_t(v_t^\top x)$ with $\|v_t\| \le R$, $|g_t'| \le b$, $g_t'' \ge a$ has regret at most $\frac{nb^2}{a}\log\bigl(\frac{a^2D^2R^2T^2}{b^2} + 1\bigr) + \frac{b^2}{a}$.

Significance

Theorem 6 shows that a simple rule, re-solving a convex quadratic program over all past linearized costs, achieves $O(n\log T)$ regret on exp-concave costs, matching the Online Newton Step up to constants. Theorem 5 is of independent interest: it shows that unmodified Follow the Leader, which has linear regret on linear costs, has logarithmic regret whenever each cost is a strongly curved function of one linear form. Portfolio selection is such a case. The appendix lemmas (log-determinant potential, elliptical potential) are standard tools reused throughout the bandit and online-learning literature.

On formalization: the results are proved on paper; none is formalized. The Lean development provides a reusable encoding of Follow the Leader as a trajectory predicate, the "be the leader" reduction, the surrogate reduction for regret, and the matrix potential inequalities, which the Online Newton Step analysis also needs. The paper's printed statements of Theorem 5 and Lemma 10 contain errors (see below); this mission states corrected versions that suffice for the goal.

Difficulty

The obvious attempt, bounding each term $f_t(x_t) - f_t(x_{t+1})$ by how far the leader moves, requires knowing how far the minimiser of a constrained problem moves when one cost is added. For unconstrained strongly convex quadratics this is an explicit Newton step, but here the minimiser lies in a general convex set and each cost contributes curvature in only one direction, so the accumulated curvature can be singular for many rounds and no per-round strong convexity is available. Turning the per-round movement into a sum that grows only like $\log T$, with the paper's explicit constant, is the core of the work; the printed Theorem 5 bound is negative for small $T$, so the constants must be tracked exactly rather than asymptotically.

Formalization scope

Points are in EuclideanSpace ℝ (Fin n) so that $\|\cdot\|$ is the Euclidean norm; cost functions are functions on all of $\mathbb{R}^n$, differentiable at the points of $P$, with Mathlib's gradient. Rounds are $1$-based; $x_0$ and $f_0$ are unused. $D$ is any upper bound on pairwise distances in $P$. Exp-concavity is ConcaveOn ℝ P (fun x => Real.exp (-α * f t x)). Algorithms are predicates on the trajectory, required at every round, so every tie-breaking rule is covered and adaptive adversaries are included.

Regret is always stated against every comparator $u \in P$. A formalization with a real-valued ⨅/sInf over $P$, or one that bounds the regret of an arbitrary sequence of points rather than of an FTAL run with the paper's $\beta$, would be trivial or false, and is excluded: the goal carries IsFTALRun with $\beta = \frac12\min\{1/(4GD),\alpha\}$.

Corrections and conventions relative to the printed paper:

• Theorem 5: the printed bound $\frac{2nb^2}{a}[\log(DRaT/b) + 1]$ is false when $DRaT/b < 1/e$. The milestone states the bound the paper's proof gives, $\frac{nb^2}{a}\log(\frac{a^2D^2R^2T^2}{b^2} + 1) + \frac{b^2}{a}$, which implies the printed one when $DRaT \ge b$. Derivatives are deriv with explicit differentiability at the points $v_t^\top x$, $x \in P$.
• Lemma 10: printed with $x_t = \arg\min \sum_{\tau=1}^{t} f_\tau$, under which it is false at $T = 1$; the proof and its use require the FTL index $\sum_{\tau=1}^{t-1}$, which is stated.
• Lemma 11: the typo $\sum_\tau u_t u_t^\top$ is read as $\sum_\tau u_\tau u_\tau^\top$, and $\varepsilon > 0$ is stated.
• Lemma 3: $\beta > 0$ is added (the proof divides by $\beta$), and $G, D > 0$ so that $1/(4GD)$ is meaningful.
• Theorem 6: "$f_t : P \to \mathbb{R}^n$" is read as $\mathbb{R}$-valued; only first-order differentiability is assumed; $G, D > 0$. The theorem is true as printed, although the paper's route through the printed Theorem 5 is invalid for $T < 16$.
• Only version 1 of FTAL is formalized; Lemma 4 (equivalence with the pseudoinverse form) is out of scope.

Needed infrastructure: first-order optimality for convex minimisation over a convex set, a mean-value theorem along segments, determinants and eigenvalues of symmetric positive definite matrices (Mathlib has most of this), and the matrix inequality $|A| \le (\operatorname{tr} A/n)^n$. Contributions welcome: proofs of any milestone, and a proof of the goal from the milestones.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71 (2005), 291–307. https://doi.org/10.1016/j.jcss.2004.10.016
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization 2 (2016). https://arxiv.org/abs/1909.05207

Motivation

Online convex optimization models repeated decision making against an unknown, possibly adversarial environment: in each round $t=1,\dots,T$ a player picks a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$, and only then learns a convex cost function $f_t$ and pays $f_t(x_t)$. Performance is measured by regret, the excess of the total cost over that of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that online gradient descent has regret $O(\sqrt T)$ for arbitrary convex costs with bounded gradients, and this rate cannot be improved in general.

Many costs met in practice have more curvature than bare convexity. The log-loss $f(x)=-\log(x^\top a)$ of universal portfolio management (Cover, Math. Finance 1991) is not strongly convex, but it is exp-concave. Hazan, Agarwal and Kale (Mach Learn 69, 2007) gave the first efficient algorithms with regret logarithmic in $T$ for exp-concave costs. This mission formalizes the second of their algorithms, the Online Newton Step (ONS), and its regret bound (Theorem 2 of the paper). ONS is the basis of later second-order online methods and appears as a standard algorithm in textbooks on online learning.

Timeline:

• 2003 — Zinkevich: $O(\sqrt T)$ regret for general convex costs by online gradient descent.
• 2006–2007 — Hazan, Agarwal, Kale (COLT 2006; Mach Learn 2007): $O(\log T)$ regret for strongly convex costs by gradient descent, and $O(n\log T)$ regret for exp-concave costs by ONS, Follow the Approximate Leader, and exponentially weighted online optimization.
• 2016 — Hazan, Introduction to Online Convex Optimization (Found. Trends Optim., arXiv:1909.05207): textbook treatment of ONS with modified parameters.

Setting

The decision set $\mathcal P\subseteq\mathbb R^n$ is nonempty, closed, bounded and convex, and $D$ bounds its diameter: $\|x-y\|\le D$ for all $x,y\in\mathcal P$, with the Euclidean norm. The costs $f_1,f_2,\dots$ are real functions, differentiable at every point of $\mathcal P$, with gradient bound $\|\nabla f_t(x)\|\le G$ on $\mathcal P$. A cost is $\alpha$-exp-concave ($\alpha>0$) if $x\mapsto\exp(-\alpha f_t(x))$ is concave on $\mathcal P$.

For a matrix $A$, the generalized projection $\Pi^A_{\mathcal P}(y)$ is a point of $\mathcal P$ minimising $(y-x)^\top A(y-x)$ over $x\in\mathcal P$.

The Online Newton Step fixes

$$\beta=\tfrac12\min\Big\{\frac1{4GD},\alpha\Big\},\qquad \varepsilon=\frac1{\beta^2D^2},$$

writes $\nabla_t=\nabla f_t(x_t)$ and $A_t=\sum_{i=1}^t\nabla_i\nabla_i^\top+\varepsilon I_n$, plays an arbitrary $x_1\in\mathcal P$, and then

$$x_{t+1}=\Pi^{A_t}_{\mathcal P}\Big(x_t-\frac1\beta A_t^{-1}\nabla_t\Big).$$

The regret after $T$ rounds against a comparator $u\in\mathcal P$ is $\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)$; the paper's regret is its maximum over $u\in\mathcal P$.

In Lean the objects are LogRegretOCO.ONS.onsBeta, onsEps, onsMatrix, IsGenProj and IsONSRun, with the regularised Gram matrix regGram and the quadratic form quadForm.

Formalization targets

Goal: Theorem 2 with $n\log T\ge4$

For every run of ONS, every horizon $T$ with $n\log T\ge 4$, and every $u\in\mathcal P$,

$$\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le 5\Big(\frac1\alpha+GD\Big)\,n\log T.$$

The added condition $n\log T\ge4$ is what makes the printed constant correct (see Formalization scope).

Milestones

1. Lemma 3 (p. 177): for $0<\beta\le\frac12\min\{1/(4GD),\alpha\}$ and $x,y\in\mathcal P$,

$$f(x)\ge f(y)+\nabla f(y)^\top(x-y)+\tfrac\beta2\big(\nabla f(y)^\top(x-y)\big)^2 .$$

2. Lemma 8 (p. 188): for convex $\mathcal P$, $A\succeq0$, $z=\Pi^A_{\mathcal P}(y)$ and $a\in\mathcal P$: $(y-a)^\top A(y-a)\ge(z-a)^\top A(z-a)$.
3. The display on p. 178: for every run of ONS and $u\in\mathcal P$,

$$\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le\frac1{2\beta}\sum_{t=1}^T\nabla_t^\top A_t^{-1}\nabla_t+\frac1{2\beta}.$$

4. Lemma 12 (p. 191): for $A\succeq B\succ0$, $A^{-1}\bullet(A-B)\le\log(|A|/|B|)$.
5. Lemma 11 (p. 190): if $\|u_t\|\le r$, $\varepsilon>0$ and $V_t=\sum_{\tau\le t}u_\tau u_\tau^\top+\varepsilon I_n$, then $\sum_{t=1}^Tu_t^\top V_t^{-1}u_t\le n\log(r^2T/\varepsilon+1)$.

Significance

Theorem 2 shows that exp-concavity alone, without strong convexity, suffices for regret logarithmic in $T$, at a per-round cost of one rank-one matrix update and one generalized projection. Its consequences include logarithmic regret for universal portfolio selection with a polynomial-time algorithm, and, by online-to-batch conversion, fast rates for stochastic exp-concave optimization. Lemma 11 (the elliptical potential bound) is used well beyond this paper, in linear bandits and online regression.

The result has been proved on paper since 2007. The remaining work is its machine-checked proof: the potential argument, the log-determinant inequality and the generalized-projection inequality for positive semidefinite matrices. As far as is known, none of these results is formalized in Mathlib. Prove2Me holds a related elliptical potential lemma for linear bandits (BanditAlgorithm.elliptical_potential_lemma, with $V_{t-1}$ and a $\min(1,\cdot)$, a different statement) and the Euclidean case $A=I$ of Lemma 8 (UnderstandingML.projection_lemma). The textbook version of ONS (OnlineConvexOpt.SecondOrder.online_newton_step_regret, with $\gamma=\frac12\min\{1/(GD),\alpha\}$ and bound $2(1/\alpha+GD)n\log T$) is an open private draft with different parameters.

Difficulty

The obvious route to logarithmic regret, the gradient-descent argument of Theorem 1 with step sizes $1/(Ht)$, needs a uniform lower bound $H>0$ on the Hessians. Exp-concave costs such as the log-loss have no such bound: their curvature vanishes in directions orthogonal to the gradients seen so far. The analysis therefore has to track curvature only along the observed gradient directions. This requires a matrix-valued potential $\sum_t\nabla_t^\top A_t^{-1}\nabla_t$ and a projection in the norm of $A_t$ rather than the Euclidean norm. The Euclidean projection inequality does not transfer to this norm, which changes from round to round. Bounding the potential requires determinant inequalities for positive definite matrices. The analytic facts are elementary, but their Lean statements involve the interaction of EuclideanSpace, Matrix.mulVec, Matrix.inv and Matrix.det.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), so all norms are Euclidean; matrices are Matrix (Fin n) (Fin n) ℝ acting on coordinate vectors. Rounds are 1-based: sums run over Finset.Icc 1 T and the index $0$ is unused. Cost functions are ambient functions $\mathbb R^n\to\mathbb R$, differentiable at the points of $\mathcal P$, with $\nabla f_t$ given by Mathlib's gradient. The paper's standing assumptions of convexity and twice differentiability are not needed and are omitted. $D$ enters only as an upper bound on distances in $\mathcal P$. The generalized projection is a predicate that every minimiser satisfies, and ONS is the predicate IsONSRun on the whole trajectory, so the goal covers every tie-break and every adaptive adversary.

Corrections and added hypotheses:

• Theorem 2 is false as printed at $T=1$. Take $n=1$, $\mathcal P=[-1,1]$, $f_1(x)=x^2$, $\alpha=\frac12$, $G=D=2$ and $x_1=1$: the regret is $1$ and the bound is $0$. The paper's proof gives $4(1/\alpha+GD)(n\log T+1)$ for $T\ge2$; the final sentence drops the additive $1/(2\beta)$ of the p. 178 display. The goal adds $n\log T\ge4$, under which the printed constant $5$ follows.
• $G,D,\alpha>0$ are assumed wherever $\beta$ or $\varepsilon$ appear: they are the non-degeneracy the formulas presuppose (in Lean, $1/0=0$).
• Lemma 3 adds $0<\beta$; the proof divides by $\beta$.
• Lemma 11 adds $\varepsilon>0$ and reads the printed $\sum_{\tau=1}^tu_tu_t^\top$ as $\sum_{\tau=1}^tu_\tau u_\tau^\top$.
• Lemma 12's product $\bullet$ is the entrywise inner product $\sum_{i,j}C_{ij}E_{ij}$, written out as a double sum.
• The printed "$f_t:\mathcal P\to\mathbb R^n$" is read as $f_t:\mathcal P\to\mathbb R$, and "$\Pi^{A_t}_{S_n}$" on p. 177 as $\Pi^{A_t}_{\mathcal P}$.

Regret is stated against every comparator $u\in\mathcal P$, never as a real infimum ⨅ over $\mathcal P$, which is junk-valued in Lean on unbounded or empty sets. The goal is a statement about runs of the paper's algorithm with the paper's $\beta$, $\varepsilon$ and $A_t$. A bound for an arbitrary sequence satisfying the p. 178 display would be a milestone, not Theorem 2. The hypotheses are jointly satisfiable: the closed unit ball with $f_t(x)=\|x\|^2/2$, $\alpha=1$, $G=1$, $D=2$ is a model.

A complete development needs: first-order conditions for concave functions on convex sets at boundary points; the optimality condition for minimising a convex quadratic over a convex set; spectral facts about symmetric positive definite matrices (square roots, eigenvalues, $\operatorname{tr}$ and $\det$); and the telescoping of log-determinants. Lemmas 8, 11 and 12 are reusable beyond this mission, in the sibling missions of this series (Follow the Approximate Leader) and in linear-bandit analyses. Proofs of any milestone are welcome, as are alternative proofs of Lemma 12 through concavity of $\log\det$.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization 2 (2016); 2nd ed. arXiv:1909.05207. https://arxiv.org/abs/1909.05207

Motivation

Where to hold safety stock in a multi-stage supply chain is a basic question of inventory planning. Graves and Willems (MSOM 2(1), 2000) optimize safety-stock placement under the guaranteed-service assumption: each stage quotes a service time to its customers and always meets it. That assumption makes the placement problem tractable, and it is the basis of the dynamic program in the body of the paper and of later work built on it. It also has a price. A stage that promises a service time must hold enough stock to keep the promise even when it would be cheaper to let a downstream stage absorb an occasional delay.

The paper's Appendix measures that price in the simplest setting where it can be computed exactly. The setting is a serial chain in which internal stages promise nothing and only the external customer is guaranteed 100% service. Its one theorem, called the Result, characterizes the optimal base stocks of this relaxed model in closed form. The paper then compares that policy with the guaranteed-service optimum on 36 test instances. The guaranteed-service counterpart of this serial model, Simpson's all-or-nothing property of optimal service times, is on Prove2Me as a separate statement (SupplyChainTheory.gs_all_or_nothing, from Snyder and Shen's textbook). This mission formalizes the other side of the comparison.

Setting

A serial supply chain has $N$ stages. Stage $1$ is the demand node and stage $i$ supplies stage $i-1$ for $i = 2, \dots, N$. Time is discrete, with periods $t \in \mathbb{Z}$. Stage $i$ has a deterministic lead time $T_i \in \mathbb{N}$ and a base stock $B_i \in \mathbb{R}$. It follows a base-stock policy: in each period it observes end-item demand and orders that amount from its supplier.

The end-item demand in period $t$ is $d(t)$. The window demand is $d(a, b] = d(a+1) + \dots + d(b)$, which is $0$ when $a \ge b$. The demand bound $D : \mathbb{N} \to \mathbb{R}$ gives $D(\tau)$, the maximum possible end-item demand over $\tau$ periods, with $D(0) = 0$.

The backlog $Q_i(t)$ is the amount the customer of stage $i$ has ordered but not yet received. It satisfies the recursion (A1):

$$Q_i(t) = \bigl[d(t - T_i, t] + Q_{i+1}(t - T_i) - B_i\bigr]^+, \qquad Q_{N+1} \equiv 0 .$$

Unrolling it gives the closed max-form (A2). The external customer receives 100% service when $Q_1(t) = 0$ for all $t$. When demand never exceeds its bound, this is ensured by the service constraints

$$B_1 + \dots + B_i \ge D(T_1 + \dots + T_i), \qquad i = 1, \dots, N. \tag{A3}$$

Let $h_i$ be the holding cost at stage $i$ and $e_i = h_i - h_{i+1}$ the echelon holding cost. After constant terms are dropped, the expected holding cost gives program $\mathbf P^*$:

$$\min_B\ \sum_{i=1}^N h_i B_i - \sum_{i=2}^N e_{i-1} E[Q_i] \quad\text{s.t. (A3) and } B_i \ge 0 .$$

Demand is random, and $E[Q_i]$ is the expected backlog at stage $i$ in a period $t$.

Formalization targets

Goal: the Result, Eq. (A6)

If the echelon holding costs are nonnegative and $D$ is nondecreasing, then an optimal solution of $\mathbf P^*$ is

$$B_1 = D(T_1), \qquad B_i = D(T_1 + \dots + T_i) - D(T_1 + \dots + T_{i-1}), \quad i = 2, \dots, N. \tag{A6}$$

Formally, (A6) is feasible, and for every period $t$ its objective value is at most that of every feasible vector. The goal names this vector and compares it with every feasible $B$. The weaker claim that "some optimal solution binds all of (A3)" would not be enough.

Milestones

1. Eq. (A2). The closed max-form of $Q_i(t)$, derived from the recursion (A1).
2. Eq. (A3). Under the demand bound $d(a, a+s] \le D(s)$, the constraints (A3) force $Q_1 \equiv 0$ (sufficiency).
3. (A6) is feasible and is the unique binding solution of (A3).
4. Backlog bounds under a transfer. Moving $\Delta \ge 0$ units of base stock from stage $k$ to stage $k+1$ leaves $E[Q_i]$ unchanged for $i > k+1$ and raises it by at most $\Delta$ for $i \le k$. It lowers $E[Q_{k+1}]$ by at most $\Delta$.
5. Eqs. (A7)–(A8). For $k < N$, the transfer that makes the $k$-th constraint binding keeps the vector feasible and does not raise the objective.
6. The case $k = N$. Lowering $B_N$ until the $N$-th constraint binds does not raise the objective.

Significance

The Result shows that, without guaranteed internal service, the optimal base stocks do not depend on the holding costs, provided the echelon costs are nonnegative. Each stage then covers exactly the increment of maximal demand that its own lead time adds. This closed form is the benchmark against which the paper measures the cost of guaranteed service: 26% more safety-stock holding cost on average over its test problems. The paper also remarks, without proof, that Rosling's transformation extends the Result to assembly systems.

The Result is proved in the paper. As far as is known, neither it nor the backlog identity (A2) has been machine-checked. A complete development would yield a verified model of serial base-stock backlogs under bounded demand. It would also verify an exchange argument that recurs in multi-echelon inventory theory: moving stock toward the customer, with echelon costs controlling the sign of the change.

Difficulty

The objective is not linear in $B$. Each $E[Q_i]$ is a convex, nonsmooth function of $B_i, \dots, B_N$ through the maximum in (A2), and the objective subtracts these terms, so $\mathbf P^*$ minimizes a concave function over a polyhedron. The obvious approaches are linear-programming duality and convex first-order optimality conditions on $\mathbf P^*$, and neither applies. The result is a comparison of objective values between arbitrary feasible vectors and (A6). It has to hold pathwise under every demand distribution, and it then has to be carried through expectations. The hypotheses the Result leaves implicit must be recovered from the rest of the paper. Two of them, stated below, are necessary.

Formalization scope

Stages are natural numbers read on the range $\{1, \dots, N\}$. Lead times are natural numbers cast to $\mathbb{Z}$. Base stocks, holding costs and the demand bound are real-valued. A base-stock vector is a function $\mathbb{N} \to \mathbb{R}$, and only indices $1, \dots, N$ are read. The backlog is defined by the recursion (A1), computed in $N + 1 - i$ steps, with $Q_i \equiv 0$ for $i > N$. The closed form (A2) is a theorem. Randomness is a probability space $(\Omega, \mu)$ with a demand path $d(\omega, \cdot)$ whose value in each period is integrable. The integrability of the backlog is not assumed; it follows from the integrability of demand.

The page's informal words are read as follows:

• "The echelon holding costs are nonnegative" means $h_i - h_{i+1} \ge 0$ for $1 \le i < N$, and $h_N \ge 0$, i.e. $e_N \ge 0$ with $h_{N+1} := 0$. The case $k = N$ of the proof uses $h_N \ge 0$. Without it the Result is false ($N = 1$, $h_1 < 0$).
• $D(0) = 0$ is the paper's convention (§2, p. 70) and is added as a hypothesis. Without it (A6) can be infeasible ($D \equiv -1$ is nondecreasing).
• "$D(\,)$ is a nondecreasing function" means Monotone D on $\mathbb{N}$.
• "An optimal solution to $\mathbf P^*$" means feasible, with objective at most that of every feasible vector.
• "$E[Q_i]$" means the expectation of $Q_i(t)$ at a fixed period $t$. Every statement holds for all $t$, and stationarity is not assumed. The paper writes $E[Q_i]$ without $t$ because its demand is stationary, and this reading is at least as strong.
• The demand bound $d(a, a+s] \le D(s)$ appears only in milestone 2. The Result does not use it, so it is not a hypothesis of the goal.
• Eq. (A3) is formalized in the sufficiency direction only. The page's necessity remark ("as we assume that the demand bounds can be realized") is not stated.

A non-integrable backlog would make its Bochner integral $0$ and erase the backlog terms of the objective. The formalization rules this out by assuming integrable demand, which makes the backlogs integrable; it does not assume the backlogs themselves integrable. Out of scope: the spanning-tree dynamic program of §5, the unproved remarks of §§3–4, the Rosling extension, the Kodak application and the computational study.

Useful contributions include a proof of (A2) by downward induction on stages, the integrability of $Q_i(t)$, the pathwise version of milestone 4, and the iteration argument that assembles milestones 3, 5 and 6 into the goal.

Selected references

• S. C. Graves and S. P. Willems, Optimizing Strategic Safety Stock Placement in Supply Chains, Manufacturing & Service Operations Management 2(1):68–83, 2000. https://doi.org/10.1287/msom.2.1.68.23267
• K. F. Simpson, In-Process Inventories, Operations Research 6(6):863–873, 1958. https://doi.org/10.1287/opre.6.6.863
• K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed., 2019. https://doi.org/10.1002/9781119584445

Motivation

Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.

For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.

Setting

Let $X$ be a finite set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every subset $S \subseteq X$. It is submodular if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,$$

equivalently if the marginal value $f(B \cup \{x\}) - f(B)$ of an element $x$ does not increase as the set $B$ grows. It is symmetric if $f(X \setminus S) = f(S)$ for every $S \subseteq X$; the cut function of an undirected graph is the standard example. The optimum is

$$OPT = \max_{S \subseteq X} f(S).$$

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; similarly $A(p)$ is the random subset of a fixed $A \subseteq X$. The Random Set Algorithm (RS) returns $R = X(1/2)$, a uniformly random subset of $X$, without querying $f$. Its expected value is the average of $f$ over all subsets,

$$\mathbf{E}[f(R)] = F(\tfrac12, \dots, \tfrac12) = \frac{1}{2^n} \sum_{S \subseteq X} f(S),$$

where $F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{i \notin S} (1 - x_i)$ is the multilinear extension of $f$, the expectation of $f$ on a random set that includes element $i$ independently with probability $x_i$.

Formalization targets

Goal: Theorem 2.1

For every nonnegative submodular $f : 2^X \to \mathbb{R}_+$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14\, OPT,$$

and if $f$ is in addition symmetric,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac12\, OPT.$$

Both parts form the goal, stated as one theorem. The constants $\tfrac14$ and $\tfrac12$ are exact, not asymptotic, and they are tight: the directed cut of a single arc attains $\tfrac14$, and the cut of a single edge attains $\tfrac12$.

Milestones

1. Lemma 2.2. For submodular $g : 2^X \to \mathbb{R}$, $A \subseteq X$ and $p \in [0,1]$,

$$\mathbf{E}[g(A(p))] \ge (1-p)\, g(\emptyset) + p\, g(A).$$

2. Lemma 2.3. For submodular $f : 2^X \to \mathbb{R}$, sets $A, B \subseteq X$ that need not be disjoint, independent samples $A(p)$, $B(q)$, and $p, q \in [0,1]$,

$$\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B).$$

3. The display in the proof of Theorem 2.1. For submodular $f : 2^X \to \mathbb{R}$ and every $S \subseteq X$, with $\bar S = X \setminus S$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14 f(\emptyset) + \tfrac14 f(S) + \tfrac14 f(\bar S) + \tfrac14 f(X).$$

The milestones need no sign on the function; nonnegativity enters only in the goal.

Significance

The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive $\tfrac13$-algorithm and its local search algorithms with factors $\tfrac13$ and $\tfrac25$, followed by later work culminating in the tight $\tfrac12$-approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that $\tfrac14$ is optimal among nonadaptive algorithms required to return one of the queried sets, and that $\tfrac12$ is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.

Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.

Difficulty

The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.

Lemma 2.2 is not a pointwise statement: the random set $A(p)$ can be any subset of $A$, and $g$ can be smaller on it than both $g(\emptyset)$ and $g(A)$. The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets $A$ and $B$ may overlap, and on $A \cap B$ the union $A(p) \cup B(q)$ contains an element with probability $1 - (1-p)(1-q)$, so it is not the product distribution with probability $p$ on $A$ and $q$ on $B$. Finally, the third milestone requires identifying the uniform random subset $X(1/2)$ with the union of independent half-samples of $S$ and of its complement, as a statement about finite sums.

The obvious attempt at the goal, comparing $f(R)$ with $f(S^*)$ for an optimal $S^*$ set by set, fails: $f$ is not monotone, so a random set that contains most of $S^*$ may still have small value, and a random set can pick up elements that hurt.

Formalization scope

The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption $f : 2^X \to \mathbb{R}_+$, is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. $OPT$ is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.

Expectations are written as exact finite sums, not as integrals. $\mathbf{E}[f(X(1/2))]$ is the multilinear extension F f (fun _ => 1/2). $\mathbf{E}[g(A(p))]$ is $\sum_{T \subseteq A} p^{|T|}(1-p)^{|A \setminus T|} g(T)$, and $\mathbf{E}[f(A(p) \cup B(q))]$ is the double sum over independent samples $S \subseteq A$, $T \subseteq B$ with the product of the two weights. The ranges $0 \le p \le 1$ and $0 \le q \le 1$, implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.

Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all $2^n$ subsets, $OPT$ is the true maximum rather than the value at one fixed set, and $f$ is required to be both nonnegative and submodular.

Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of $X(1/2)$ along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM Journal on Computing 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing non-monotone submodular functions, Proceedings of the 48th IEEE Symposium on Foundations of Computer Science (FOCS), 2007, pp. 461–471. https://doi.org/10.1109/FOCS.2007.29
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5):1384–1402, 2015 (FOCS 2012). https://doi.org/10.1137/130929205
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14:265–294, 1978. https://doi.org/10.1007/BF01588971

Motivation

Minimizing the sum of weighted completion times of jobs on identical parallel machines is one of the basic objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. When the jobs are subject to precedence constraints (a job may start only after certain other jobs have finished), the problem is strongly NP-hard already in very restricted cases, and the question becomes how close to optimal a polynomial-time algorithm can guarantee to be.

Chekuri, Motwani, Natarajan and Stein, Approximation Techniques for Average Completion Time Scheduling (SIAM J. Comput. 31(1), 2001, doi:10.1137/S0097539797327180), develop a general way to turn a good schedule for a single machine into a good schedule for $m$ machines. For arbitrary precedence constraints their conversion (Delay List, §4.1–4.3) loses a factor $(1+\beta)\rho+(1+1/\beta)$ over a $\rho$-approximate one-machine schedule, which is $4$ when the one-machine schedule is optimal. In §4.4 they show that for in-tree precedence without release dates, the plain list-scheduling rule of Graham, fed with an optimal one-machine schedule, already achieves ratio $2$. In-trees are the precedence structures of assembly processes: every job feeds into at most one later job.

Timeline of the relevant results:

• 1966–1969: Graham introduces list scheduling on parallel machines and analyzes it for makespan (Graham 1969).
• 1972: Horn gives a polynomial-time optimal one-machine algorithm for weighted completion time under treelike precedence (Horn 1972).
• 1977: Adolphson gives $O(n\log n)$ one-machine algorithms for tree and series-parallel precedence (Adolphson 1977, the paper's reference [1]).
• 2001: Chekuri, Motwani, Natarajan and Stein prove the ratio-$2$ bound for in-trees on $m$ machines (Theorem 4.17).

Setting

There are $n$ jobs $J_0,\dots,J_{n-1}$ and $m\ge 1$ identical machines. Job $J_j$ has a processing time $p_j>0$ and a weight $w_j>0$; every job is available at time $0$ (there are no release dates).

The precedence constraints form an in-tree (more generally, an in-forest): every job $j$ has at most one immediate successor $\operatorname{succ}(j)$, and following successors never returns to the start. Write $i\prec j$ if $j$ is reached from $i$ by following successors one or more times.

A feasible schedule $S^m$ on $m$ machines gives each job a start time $S_j\ge 0$ and a machine; a job runs without interruption for $p_j$ time units; two jobs on the same machine do not overlap; and $i\prec j$ implies that $j$ starts no earlier than $i$ completes. The completion time is $C^m_j=S_j+p_j$ and the value of the schedule is $\sum_j w_jC^m_j$.

The critical-path length $\kappa_j$ (Definition 4.1 with no release dates) is $\kappa_j=p_j$ if $j$ has no predecessors and $\kappa_j=p_j+\max_{i\prec j}\kappa_i$ otherwise.

A list is an ordering $\pi$ of the jobs that obeys the precedence constraints. It defines the one-machine schedule $S^1$ that runs the jobs in list order without idle time; its completion times are $C^1_j$, the total processing time of the jobs up to and including $j$ in the list. An optimal one-machine schedule is a list minimizing $C^1=\sum_j w_jC^1_j$.

List scheduling (Graham's rule, footnote 3 of the paper) on $m$ machines with list $\pi$: whenever a machine is free, start on it the first job of the list that is ready, i.e. whose predecessors have all completed.

Formalization targets

Goal: Theorem 4.17

Let $\pi$ be an optimal one-machine schedule and $G$ the list schedule on $m$ machines with list $\pi$. Then for every feasible $m$-machine schedule $N$,

$$\sum_j w_jC^G_j\ \le\ 2\sum_j w_jC^N_j .$$

Milestones

Lemma 4.16 (any precedence-respecting list $\pi$, with its idle-free one-machine schedule $S^1$): for every job $i$,

$$C^G_i\ \le\ \kappa_i+\frac{C^1_i}{m}.$$

Lemma 4.10: $C^m_{\mathrm{OPT}}\ge C^1_{\mathrm{OPT}}/m$, i.e. $\sum_j w_jC^1_j/m\le\sum_j w_jC^N_j$ for an optimal list and every feasible $N$.

Lemma 4.11: $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$, i.e. $\sum_i w_i\kappa_i\le\sum_i w_iC^N_i$ for every feasible $N$ on any number of machines, and the value $\sum_i w_i\kappa_i$ is attained by a feasible schedule on $n$ machines.

Significance

The result. Theorem 4.17 gives a simple, fast algorithm with a guaranteed factor $2$ for a strongly NP-hard problem, halving the factor $4$ that the general Delay List conversion gives for the same class. The per-job bound of Lemma 4.16 is stronger than the aggregate statement: every single job completes within its critical-path length plus a $1/m$ share of its one-machine completion time, so the same bound applies to other objectives built from completion times.

Formalizing it. The paper's proof is complete and short, but it argues about events at a time $t$ (jobs that finish exactly at $t$, jobs that become ready at $t$, machines freed at $t$) and runs an induction over jobs ordered by start time with an invariant about idle time. A machine-checked version fixes what "list scheduling" means precisely, pins down the counting argument that uses the in-tree structure, and yields reusable definitions of nonpreemptive parallel-machine schedules, critical paths and list schedules. To the knowledge of this mission, none of these results has a machine-checked proof.

Difficulty

List scheduling may start a job that is late in the list before an earlier one, because the earlier job is not yet ready; so the one-machine order is not preserved and the obvious comparison with $S^1$ fails. Idle machines are the other obstacle: a machine can stay idle while a job waits for its predecessors, and a per-job bound of the form $\kappa_i+C^1_i/m$ holds only if such idle time can be accounted for by $J_i$'s own chain of predecessors. For general precedence constraints, and for out-trees (every job has at most one immediate predecessor), the paper's accounting breaks down, and the paper states the per-job bound only for in-trees; the in-tree structure is essential to the argument. Events with several jobs finishing at the same instant, and ties in start times, have to be handled without loss.

Formalization scope

• Jobs are Fin n, machines Fin m, times real numbers. Processing times and weights are strictly positive. There are no release dates: start times are nonnegative. The paper admits $p_j=0$ only in lower-bound instances elsewhere; the bounds here assume $p_j>0$.
• In-trees are encoded by an immediate-successor map succ : Fin n → Option (Fin n) with no cycles; this covers in-forests, the reading of "in-trees" in Theorem 4.17. The precedence relation is its transitive closure.
• $\kappa$ is defined by well-founded recursion on the precedence order, exactly as Definition 4.1 with $r\equiv 0$.
• One-machine schedules are represented by their precedence-respecting order and are idle-free; with no release dates and positive processing times idle time only delays jobs, so optimality among orders is optimality among one-machine schedules. The optimal one-machine schedule is a hypothesis of the goal; the paper's $O(n\log n)$ algorithm for computing it (reference [1]) is not formalized, and the running-time claim of Theorem 4.17 is not stated. A separate item asserts that an optimal order exists.
• List scheduling is specified by two properties that determine Graham's rule up to machine labels: no machine is idle while a ready job waits, and among jobs ready at a start time the earlier one in the list starts first. A separate item asserts that such a schedule exists for every precedence-respecting list, so the goal is not vacuous.
• Optima are never formed as infima: the approximation ratio is stated against every feasible schedule. A statement of the form "there is an algorithm with ratio 2" would be trivial (an optimal schedule exists) and is ruled out: the goal is about the paper's algorithm.
• The equality $\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$ in Lemma 4.11 is stated as attainment on $n$ machines (as many machines as jobs), which together with the lower bound on every number of machines is the optimum with unboundedly many machines.

Welcome contributions: proofs of the two existence items (Graham's list schedule by event-driven construction; an optimal order over the finite set of linear extensions), of Lemmas 4.10 and 4.11, and of Lemma 4.16. The schedule and list-scheduling definitions are reusable for other parallel-machine results with precedence constraints.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• R. L. Graham, Bounds on multiprocessing timing anomalies, SIAM J. Appl. Math. 17(2):416–429, 1969. https://doi.org/10.1137/0117039
• W. A. Horn, Single-machine job sequencing with treelike precedence ordering and linear delay penalties, SIAM J. Appl. Math. 23(2):189–202, 1972. https://doi.org/10.1137/0123021
• D. L. Adolphson, Single machine job sequencing with precedence constraints, SIAM J. Comput. 6(1):40–54, 1977. https://doi.org/10.1137/0206002

Motivation

Minimizing the sum of weighted completion times $\sum_j w_jC_j$ is one of the standard objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. With release dates or precedence constraints the problem is NP-hard already on one machine, and on $m$ identical parallel machines it is harder still, so the literature of the 1990s concentrated on approximation algorithms. Many of these, including LP-based ones, are naturally designed for a single machine, where an order of the jobs determines the schedule.

Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) gave a generic way to move from one machine to many. Their §4 describes an algorithm, Delay List, that takes any one-machine schedule as a priority list and produces an $m$-machine schedule, and proves that a $\rho$-approximate one-machine schedule yields a $\bigl((1+\beta)\rho+1+1/\beta\bigr)$-approximate $m$-machine schedule for every $\beta>0$. The guarantee holds with release dates and arbitrary precedence constraints simultaneously, which at the time gave the best bounds known for several special cases, for example a factor 4 for series-parallel precedence without release dates.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has processing time $p_j>0$, release date $r_j\ge 0$ and weight $w_j>0$. Precedence constraints form a strict partial order $\prec$: $i\prec j$ means that $J_j$ may start only after $J_i$ completes.

A feasible nonpreemptive schedule on $m$ machines assigns each job a start time $S_j$ and a machine; each job runs uninterrupted for $p_j$ time units on its machine, two jobs on one machine do not overlap, $S_j\ge r_j$, and $S_i+p_i\le S_j$ whenever $i\prec j$. The completion time is $C_j=S_j+p_j$ and the value of the schedule is $\sum_j w_jC_j$. A one-machine schedule is the case $m=1$.

The critical-path length $\kappa_j$ (Definition 4.1) is $p_j+r_j$ for a job without predecessors and $p_j+\max\{\max_{i\prec j}\kappa_i,\,r_j\}$ otherwise; it is the earliest time $J_j$ could complete with unlimited machines.

A list is an ordering $\pi$ of the jobs. Delay List with parameter $\beta>0$ processes time continuously. A job is ready once it is released and all its predecessors have completed; $q^m_j$ is the time it becomes ready. The head is the first unscheduled job of the list. Idle machine-time is recorded as charged to jobs. Whenever a machine is idle:

1. if the head is ready, it is started, and charged all uncharged idle time in $(q^m_j,s^m_j)$;
2. otherwise the first ready job $J_k$ of the list is started as soon as at least $\beta p_k$ units of uncharged idle time have accumulated, and is charged $\beta p_k$ of it;
3. otherwise nothing happens.

For a job $J_i$, $B_i$ is the set of jobs up to and including $J_i$ in the list, $A_i$ the set after it, $O_i\subseteq A_i$ the set of jobs of $A_i$ started before $J_i$, and $p(A)=\sum_{k\in A}p_k$. Definition 4.4 builds from the schedule a backward path $P'_i$ ending at $J_i$, whose length is $\kappa'_i$.

Formalization targets

Goal: Theorem 4.13

Let $S^1$ be a feasible one-machine schedule of the instance with $\sum_j w_jC^1_j\le\rho\sum_j w_jC'_j$ for every feasible one-machine schedule $C'$. Let $m\ge 2$ and $\beta>0$. Every Delay List schedule $S^m$ built on the completion order of $S^1$ satisfies, for every feasible $m$-machine schedule $N$,

$$\sum_j w_jC^m_j\le\Bigl((1+\beta)\rho+1+\frac1\beta\Bigr)\sum_j w_jC^N_j .$$

Milestones, in the order the proof uses them

• Fact 4.5: $\kappa'_i\le\kappa_i$.
• Fact 4.6: the idle time charged to $J_i$ is at most $\beta p_i$.
• Lemma 4.7: no uncharged idle time remains in $(q^m_i,s^m_i)$, and that idle time is charged only to jobs in $B_i$.
• Lemma 4.8: the idle time charged to $A_i$ within $(0,s^m_i)$ is at most $m(\kappa'_i-p_i)$, so $p(O_i)\le m(\kappa'_i-p_i)/\beta\le m(\kappa_i-p_i)/\beta$.
• Theorem 4.9: $C^m_i\le(1+\beta)p(B_i)/m+(1+1/\beta)\kappa'_i-p_i/\beta$ for any list obeying precedence.
• Lemma 4.10: $C^m_{\mathrm{OPT}}\ge C^1_{\mathrm{OPT}}/m$.
• Lemma 4.11: $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$.
• Corollary 4.12: $C^m_i\le(1+\beta)C^1_i/m+(1+1/\beta)\kappa_i$ when the list is the completion order of $S^1$.

A further item states that a Delay List schedule exists for every instance and every list, so that the goal does not hold vacuously.

Significance

The result. Theorem 4.13 turns every one-machine approximation algorithm for weighted completion time with release dates and precedence into an $m$-machine algorithm at a bounded loss. With an optimal one-machine schedule and $\beta=1$ the factor is $4$ (Corollary 4.14, for series-parallel orders), and the bounds are job-by-job (Theorem 4.9, Corollary 4.12), which the paper uses in Remark 4.15 to extend the method to other metrics and to one-machine schedules that ignore release dates. The same algorithm is the engine of the paper's $2\sqrt2$-approximation for parallel machines with release dates (§4.5).

Formalizing it. The theorem has been proved since 1997 (SODA) and 2001 (journal). There is no machine-checked version of it or of any of its lemmas, and the platform currently has no model of scheduling with release dates and precedence constraints. A formalization produces a precise specification of Delay List, whose informal description is given in discrete time and repaired in a remark; a checked proof of the charging argument; and reusable lower bounds (Lemmas 4.10 and 4.11) for any later work on parallel-machine scheduling with precedence.

Difficulty

The obvious attempt, list scheduling (start the first available job of the list whenever a machine is free), fails with non-identical processing times: a long job taken out of order can occupy a machine and delay a more valuable job that becomes ready shortly afterwards. Delay List allows out-of-order jobs only against accumulated idle time, and the analysis rests on a charging invariant. Stating it needs care about time (the paper's discrete-time exposition can over-charge by a time unit), about which idle time a charge consumes, and about many jobs being scheduled at one instant. The bound must hold simultaneously for release dates and arbitrary precedence constraints, where idle machines can be forced both by jobs that are not yet released and by chains of predecessors, and it must hold for every tie-breaking choice of the algorithm.

Formalization scope

Jobs are Fin n, machines Fin m, and times are real numbers. Processing times are positive, release dates nonnegative and weights positive, as in §1. Precedence is a strict partial order, the transitive closure of the paper's DAG; $\kappa$, readiness and feasibility are unchanged by taking the closure. The optimum is never a real infimum: "within a factor $\rho$ of an optimal one-machine schedule" and "within a factor $c$ of an optimal $m$-machine schedule" are inequalities against every feasible schedule of the same instance, with the same release dates and precedence constraints.

Delay List is formalized in the continuous-time version described in the proof of Fact 4.6, as a predicate on runs that records start times, machines, the order in which jobs are scheduled at equal times, and charge windows. A case-2 charge takes the most recent uncharged idle time, and idle time is charged by whole time slices. Every guarantee is claimed for every run satisfying the predicate. The ties in Definition 4.4 are broken arbitrarily, so statements involving $\kappa'_i$ hold for every admissible path. Lemma 4.10 uses nonpreemptive one-machine schedules. Lemma 4.11's $C^\infty_{\mathrm{OPT}}$ is modelled by $n$ machines.

It would be trivializing to assume the conclusions of Fact 4.6 or Lemma 4.7 as properties of the run, or to measure $\rho$ against a relaxation without release dates or precedence; both are ruled out. The algorithm's rules are the only hypotheses on the run.

Not stated: the running time of Delay List; the discrete-time algorithm; Corollary 4.14 (it needs a formal class of series-parallel orders and the external one-machine algorithm of Adolphson for them); Remark 4.15 (release-date-free one-machine schedules), whose hypotheses the paper does not pin down; and the extension to delays between jobs. Contributions of general infrastructure, such as idle-time accounting for step functions and lemmas about list schedules under precedence, are welcome and reusable beyond this mission.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM Journal on Computing 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45:1563–1581, 1966. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
• D. Adolphson, Single machine job sequencing with precedence constraints, SIAM Journal on Computing 6(1):40–54, 1977. https://doi.org/10.1137/0206002

Motivation

Minimizing the average completion time of jobs that arrive over time is a basic objective in machine scheduling. It measures how long a job spends in the system on average. With several identical machines, release dates and no preemption (written $P|r_j|\sum C_j$), the problem is strongly NP-hard already on one machine. Research has therefore looked for approximation algorithms: polynomial-time rules whose total completion time is provably within a constant factor of every feasible schedule.

A common approach solves a relaxation that is easy to optimize and converts its solution into a feasible schedule. Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) use a relaxation that needs neither linear programming nor dynamic programming: pretend that the $m$ machines are one machine that is $m$ times as fast, and allow preemption.

Timeline:

• 1996, Chakrabarti, Phillips, Schulz, Shmoys, Stein and Wein (ICALP 1996, LNCS 1099, pp. 646–657): a $(2.89+\epsilon)$-approximation for $P|r_j|\sum C_j$.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), §3 and §4.5). §3 gives a simple $(3-1/m)$-approximation by list scheduling from the one-machine relaxation. §4.5 combines it with the Delay List conversion to obtain $2\sqrt2\approx2.83$. This mission's goal is the §4.5 result.
• 1999, Afrati, Bampis, Chekuri, Karger, Kenyon, Khanna, Milis, Queyranne, Skutella, Stein and Sviridenko (FOCS 1999, pp. 32–43): polynomial-time approximation schemes for $P|r_j|\sum w_jC_j$. These settle the approximability, but the algorithms are far more involved than the ones formalized here.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$ and $m\ge1$ identical machines. Job $J_j$ has a processing time $p_j>0$ and a release date $r_j\ge0$.

A feasible schedule gives each job a start time $S_j\ge r_j$ and a machine. Job $J_j$ runs without interruption on its machine during $[S_j,S_j+p_j)$, and two jobs on the same machine never overlap. The completion times are $C_j=S_j+p_j$ and the objective is $\sum_j C_j$. $C^*_j$ denotes the completion times of an arbitrary feasible schedule, against which every bound is stated.

The one-machine relaxation $I1$ has the same jobs and a single machine. Job $J_j$ has processing time $p_j/m$ and release date $r_j$ in $I1$, and may be preempted. A preemptive schedule $P1$ of $I1$ gives each job a processing rate $\rho_j(t)\ge0$. The rates sum to at most $1$ at each time, and no job is processed before its release date. Each job receives $p_j/m$ units in total. Its completion time $C^{P1}_j$ is the first time by which all of it has been processed. $P1$ is optimal if $\sum_j C^{P1}_j$ is minimal among all such schedules.

A list is an ordering $\pi$ of the jobs, and the completion order of $P1$ lists the jobs by nondecreasing $C^{P1}_j$. Two ways of turning a list into an $m$-machine schedule are compared.

• Strict-order list scheduling gives the schedule $N$. The jobs start in the order of the list. Each job starts at the earliest time that is no earlier than its release date, no earlier than the previous job's start, and at which some machine is free.
• Delay List with parameter $\beta>0$ gives the schedule $D$. When a machine is idle, Delay List starts the first unscheduled job of the list if it has been released. If that job has not been released, the first released job of the list may jump ahead, but only once at least $\beta p_j$ units of idle time (machine × time) have accumulated that no earlier job has charged. The job then charges exactly that amount. A job started in list order charges all uncharged idle time since its release.

Formalization targets

Goal: Lemma 4.19

With $P1$ optimal, $\pi$ its completion order, $N$ the strict-order list schedule of $\pi$ and $D$ a Delay List schedule of $\pi$ with $\beta_0=\sqrt{3-2\sqrt2}$, every feasible schedule satisfies

$$\min\Bigl(\sum_j C^N_j,\ \sum_j C^D_j\Bigr)\le 2\sqrt2\,\sum_j C^*_j .$$

The printed lemma says $2.83$. Its proof gives $2\sqrt2\approx2.8284$, which is stated here.

Milestones

In the order the proof uses them:

1. (4.2): if $\sum_j p_j>\alpha\sum_j C^*_j$ then $\sum_j r_j\le(1-\alpha)\sum_j C^*_j$.
2. Lemma 3.1: $\sum_j C^{P1}_j\le\sum_j C^*_j$ for $P1$ optimal.
3. (3.3): $\sum_j C^N_j\le 2\sum_j C^{P1}_j+(1-1/m)\sum_j p_j$ for any $P1$.
4. Lemma 3.2: $\sum_j C^N_j\le(3-1/m)\sum_j C^*_j$.
5. Theorem 4.9, specialised to no precedence constraints. With $B_i$ the jobs at or before $J_i$ in the list,

$$C^D_i\le\frac{(1+\beta)p(B_i)}{m}+\Bigl(1+\frac1\beta\Bigr)(r_i+p_i)-\frac{p_i}{\beta}.$$

6. Lemma 4.18: $\sum_j C^D_j\le(2+\beta)\sum_j C^*_j+\frac1\beta\sum_j r_j$.
7. The balanced bound: under (4.2)'s hypothesis, $\sum_j C^D_j\le(2+\beta+(1-\alpha)/\beta)\sum_j C^*_j$.
8. The constants: at $\alpha=2\sqrt2-2$ and $\beta=\sqrt{3-2\sqrt2}$, $2+\alpha=2+\beta+(1-\alpha)/\beta=2\sqrt2$.

Two existence statements accompany them. One says an optimal $P1$ exists. The other says a Delay List schedule exists for every list and every $\beta>0$.

Significance

The result gives a $2\sqrt2$-approximation for $P|r_j|\sum C_j$ that is simple to state and runs in $O(n\log n)$ time. It improves the $2.89+\epsilon$ bound of Chakrabarti et al. Neither of its two algorithms achieves the ratio alone. It comes from an analysis in which each algorithm is good exactly when the other is bad. List scheduling is good when processing times are small relative to the optimum. Delay List is good when release dates are small. The inequality (4.2) connects the two cases.

The component results are reusable beyond this paper. The one-machine relaxation lower bound (Lemma 3.1) and the $(3-1/m)$ bound for list scheduling from it (Lemma 3.2) apply to any conversion from a fast single machine. The per-job bound of Theorem 4.9 is the core of the Delay List technique. Its general form, with precedence constraints, drives the paper's results for precedence-constrained scheduling.

All results are proved in the paper. None of them has a machine-checked proof that this mission knows of. A formalization would check the Delay List charging argument, which the paper states only in discrete time and adapts to continuous time in one sentence. It would also produce reusable Lean definitions of parallel-machine schedules with release dates and of list scheduling.

Difficulty

The arithmetic of the goal is routine once the milestones are in place. The substance lies in two places.

The first is Lemma 3.1 together with the "standard makespan argument" behind (3.2). The one-machine relaxation must be related to the $m$-machine schedule, and to the list schedule, with care about release dates. In particular, in the list schedule every machine is busy between the last release among the first $j$ jobs of the list and the start of the $j$-th job. Proving this needs the strict order.

The second, and harder, is Theorem 4.9. The obvious argument bounds the waiting time of job $J_i$ by the work of the jobs ahead of it, but Delay List lets later jobs jump ahead. The idle time before $J_i$ starts and the work of the jobs that jump ahead of it must both be controlled, and the paper's charging argument for this depends on where charged idle time lies on the time axis and on which jobs charged it. Making that bookkeeping precise for a continuous-time algorithm is the main formalization cost.

Formalization scope

Jobs are Fin n and machines Fin m with $m\ge1$. Times are real, processing times are positive and release dates nonnegative. There are no weights and no precedence constraints. "Optimal" is never an infimum. Every bound is stated against every feasible nonpreemptive schedule, and $P1$'s optimality is the hypothesis that its total completion time is at most that of every preemptive schedule of $I1$.

Committed conventions:

• Preemptive schedules of $I1$ are rate functions, so the machine of $I1$ may be shared. The paper's one-job-at-a-time schedules are a special case.
• Lists are bijections Fin n ≃ Fin n. A list of $P1$ may break ties in completion time in any way, and every such list is covered.
• $N$ is the strict-order variant of list scheduling, which footnote 3 of the paper contrasts with the greedy variant used in §4. It is a recursive definition over list positions.
• Delay List is the continuous-time algorithm, as adopted in the proof of Fact 4.6. It is a predicate on start times, machines, the scheduling order and charge windows. A job scheduled out of order takes its charge from the most recent uncharged idle time; the paper leaves this placement open. Theorem 4.9 and Lemma 4.18 assume $m\ge2$, the setting of §4.1. The goal assumes only $m\ge1$.
• The printed Lemma 4.18 lacks a $\sum_j$ on the $C^*$ term. The summed form of its proof's last display is stated.

The statement cannot be made easy by the hypotheses. Two existence items show that an optimal $P1$ and a Delay List schedule always exist, so no statement is vacuous. The bound is against every feasible schedule, not against the relaxation's value.

Not stated: the $O(n\log n)$ running time, the on-line version of §3's algorithm, and Delay List with precedence constraints (Theorem 4.9 in general, which is the subject of mission III of this series). Contributions welcome: proofs of the milestones, and reusable lemmas on list scheduling with release dates.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• S. Chakrabarti, C. A. Phillips, A. S. Schulz, D. B. Shmoys, C. Stein, J. Wein, Improved scheduling algorithms for minsum criteria, in Proceedings of ICALP 1996, LNCS 1099, Springer, pp. 646–657 (reference [3] of the paper).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, in Proceedings of the 40th IEEE FOCS, 1999, pp. 32–43 (reference [2] of the paper).