Optimization

Motivation

Earliness/tardiness (E/T) scheduling penalizes a job both for finishing late and for finishing early. It models just-in-time production, where an early job ties up inventory and a late one delays a customer. Baker and Scudder's review (Oper. Res. 38 (1990) 22–36) organized the single-machine E/T literature around a short list of structural properties of optimal schedules for a common due date shared by all jobs. For the problem without tolerances these properties go back to work the review surveys, beginning with Kanet (1981) for equal penalties.

The review then turns to due-date tolerances: a job pays nothing if it completes within a window around the due date, as in contracts that accept delivery within a few days of a target. Cheng (1988) studied a version in which the penalty is discontinuous at the window ends. Baker and Scudder state the continuous version and prove two generalized properties, III(G) and IV(G), in the paper's Appendix (pp. 34–35). They are the paper's own results; the rest of the review cites results proved elsewhere.

Setting

Fix $n \ge 1$ jobs, processed on one machine in a fixed order, one after another, starting at time $0$ with no idle time between them. The job in position $j$ has a processing time $p_j$, so it completes at $C_j = p_1 + \dots + p_j$. All jobs share a common due date $d \in \mathbb R$, which is a decision variable. Job $j$ has tolerances $u_j, v_j \ge 0$ and is free of penalty when $C_j \in [d - u_j,\ d + v_j]$. Outside its window it pays a unit earliness penalty $\alpha_j > 0$ or a unit tardiness penalty $\beta_j > 0$:

$$E_j = (d - C_j - u_j)^+,\qquad T_j = (C_j - d - v_j)^+,\qquad f(d) = \sum_{j=1}^n \bigl(\alpha_j E_j + \beta_j T_j\bigr).$$

The tolerances are small compared with the processing times: $p_j - v_j - u_i > 0$ for distinct jobs $i \ne j$. Under this condition at most one job can avoid penalty costs. A due date is optimal if it minimizes $f$ over $\mathbb R$, and the least optimal due date is the smallest optimal one. The paper minimizes $d$ as a secondary criterion when there are alternative optima.

In Lean the model is BakerScudder1990.Tolerance.Instance n, with fields p u v α β : Fin n → ℝ, completion times I.C, earliness I.earliness d, tardiness I.tardiness d, total penalty I.cost d, and the predicates I.IsOptimalDueDate and I.IsLeastOptimalDueDate.

Formalization targets

Goal: Property IV(G)

Let $d$ be the least optimal due date and let $b$ be the number of jobs with $T_j = 0$. Then a least optimal due date exists, and exactly one of the following holds:

$$\begin{aligned} C_b &= d + v_b \quad\text{with}\quad \textstyle\sum_{i<b}\alpha_i < \sum_{i\ge b}\beta_i,\ \ \sum_{i<b}\alpha_i \ge \sum_{i>b}\beta_i,\\ C_b &= d - u_b \quad\text{with}\quad \textstyle\sum_{i<b}\alpha_i < \sum_{i>b}\beta_i,\ \ \sum_{i\le b}\alpha_i \ge \sum_{i>b}\beta_i. \end{aligned}$$

The case labels follow the paper's proof. The printed statement swaps them (see Formalization scope).

Milestones

1. Case 1 of the proof of III(G). Between the window of job $j-1$ and the window of job $j$, $f$ is affine with slope $\sum_{i<j}\alpha_i - \sum_{i\ge j}\beta_i$. Before the first window and after the last, the slopes are $-\sum_i\beta_i$ and $\sum_i\alpha_i$.
2. Case 2 of the proof of III(G). Inside the window of job $j$, $f$ is affine with slope $\sum_{i<j}\alpha_i - \sum_{i>j}\beta_i$.
3. Property III(G). A least optimal due date exists, and at it some job completes at $d - u_j$ or at $d + v_j$.
4. The two optimality conditions. The first pair of inequalities above makes $C_j - v_j$ the least optimal due date, and the second pair makes $C_j + u_j$ the least optimal due date.

Significance

III(G) reduces the choice of an optimal common due date for a given sequence to $2n$ candidates. IV(G) goes further and names the candidate directly from prefix and suffix sums of the penalties. Baker and Scudder use this to say which V-shaped sequences remain candidates for optimality, so that an enumeration over sequences can discard the others. With $u_j = v_j = 0$ the two properties reduce to the classical common-due-date conditions: some job completes exactly at $d$, and which one is fixed by a weighted-median condition.

The results are proved in the paper, so the formalization does not settle an open question. It produces a machine-checked version of the Appendix, with two printed errors corrected, and a reusable model of single-machine E/T costs with tolerance windows. No earliness/tardiness model or result was formalized on Prove2Me as of October 2026.

Difficulty

Each linear piece of $f$ is elementary. The work lies in showing that the pieces are the claimed ones: the tolerance condition must imply that a job before position $j$ is early, and a job after it tardy, throughout each gap and window. That needs the ordering $C_i + u_i < C_j - v_j$ for every $i < j$, not only for consecutive jobs. The second point is the least optimal due date. Optimality alone does not determine $d$ on a flat stretch of $f$, where every point is optimal and only the left end satisfies the strict inequalities. Existence of a least minimizer also has to be shown, from the two outer slopes and finitely many breakpoints. Finally, the count $b$ of jobs without tardiness must be matched to the position of the critical job at both kinds of breakpoint.

Formalization scope

• Jobs are indexed by 0-based positions Fin n, so the paper's job $b$ is position $k = b - 1$ and the goal states the count of untardy jobs as $k+1$. Data are real numbers. $(x)^+$ is max 0 x.
• The sequence starts at time $0$ and $d$ ranges over all of $\mathbb R$; this is the unrestricted problem, which is the one where the paper asserts III(G) and IV(G). Shifting the start time is equivalent to shifting $d$.
• "In an optimal schedule" is read for a fixed sequence and its least optimal due date. If a sequence and due date are jointly optimal with $d$ least among such optima, then $d$ is the least optimal due date for that sequence, so this reading implies the paper's.
• The tolerance condition is assumed only for distinct jobs. That is a weaker hypothesis than the literal "for all pairs $(i,j)$", so the theorems are stronger.
• Errata, corrected and disclosed. (i) IV(G) is printed (p. 30 and p. 35) with its two case labels swapped relative to its own proof. One job with $u_1, v_1 > 0$ has least optimal due date $C_1 - v_1$, so $C_1 = d + v_1$ while the first condition pair holds. (ii) In Cases 1 and 2 the identity is printed as $f(S) - f(S') = [\dots]\varepsilon$; the correct one is $f(S') - f(S) = [\dots]\varepsilon$. The milestone texts are quoted as printed; the Lean states the corrected mathematics.
• Existence of a least optimal due date is a conjunct of III(G) and of IV(G), and both assume $n \ge 1$. A version quantifying only over least optimal due dates without existence would be vacuous. A version for every optimal due date would be false. Neither is acceptable.
• The optimality conditions are stated as sufficient. Their converse fails when $u_j = v_j = 0$.
• Properties I and II (no inserted idle time, V-shaped sequences) are quoted in the paper, not proved there, and are not formalized. Optimization over sequences is out of scope.
• Welcome contributions: proofs of the two slope identities (finite sums of max 0 terms with a sign determined on each piece), a general lemma that a convex piecewise-linear coercive function on $\mathbb R$ attains its least minimizer at a breakpoint, and the special cases $u = v = 0$ as corollaries.

Selected references

• K. R. Baker and G. D. Scudder, Sequencing with earliness and tardiness penalties: a review, Operations Research 38(1) (1990) 22–36. https://doi.org/10.1287/opre.38.1.22
• J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28 (1981) 643–651 (as cited in Baker and Scudder 1990).
• U. Bagchi, R. S. Sullivan and Y.-L. Chang, Minimizing mean absolute deviation of completion times about a common due date, Naval Research Logistics Quarterly 33 (1986) 227–240 (as cited in Baker and Scudder 1990).
• T. C. E. Cheng, Optimal common due date with limited completion time deviation, Computers & Operations Research 15 (1988) 91–96 (as cited in Baker and Scudder 1990).

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$, needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$. Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$, and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

• 1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
• 1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$-competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
• 1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
• 2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$-competitive deterministic algorithm from an LP relaxation.
• 2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$, integer processing times $p_j \ge 1$ and real weights $w_j > 0$. A schedule assigns each job an integer start time $S_j$. It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$.

Delayed SWPT runs over unit time slots $[t, t+1)$. When the machine is available at time $t$, it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$. Ties go to the smaller $p_j$, then to the smaller index. If $p_j \le t$, it starts $j$ at $t$ and the machine is busy until $t + p_j$. Otherwise the machine stays idle and the rule is applied again at $t+1$. The resulting schedule is written $\pi$, or dswpt I in Lean. In particular no job starts before time $p_j$.

The proof uses three auxiliary problems:

• the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$;
• the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$, where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
• one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$.

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$.

Formalization targets

Goal: Theorem 8

$$\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.$$

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

1. $\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
2. $\pi_E$ is feasible for (E) (§3.2).
3. Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$.
4. Lemma 2. $\pi_E$ is optimal for (E).
5. Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

$$\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}$$

then $C(\pi) \le 2\,C(S)$ for every feasible $S$. 6. Inequality (1) holds for some feasible $\sigma_E$, for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$. The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

• an executable, verified-terminating definition of an online scheduling rule;
• the doubling lemma for release-date problems;
• the optimality criterion behind Lemma 2;
• the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

• Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$.
• Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
• The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$. A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
• Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$, and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

• The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
• The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

• simulation invariants for the algorithm;
• exchange and left-shift arguments for single-machine schedules;
• the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

• E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
• J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
• L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
• H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106

Motivation

Many problems in signal processing, statistics and machine learning take the form

$$\min_{x\in\mathcal H}\ \Psi(x)+\Phi(x),$$

where $\Phi$ is smooth and convex (a data-fit term) and $\Psi$ is convex but possibly nonsmooth or infinite-valued (an $\ell^1$ penalty, the indicator function of a constraint set). The forward-backward method alternates a gradient step on $\Phi$ with a proximal step on $\Psi$ and reduces the objective gap at rate $O(k^{-1})$ after $k$ iterations. Combining it with Nesterov's extrapolation scheme gives the accelerated forward-backward method, best known as FISTA, which improves the guaranteed rate to $O(k^{-2})$. FISTA and its variants are standard solvers for sparse recovery and image reconstruction.

Timeline:

• 1983. Nesterov introduces the extrapolation scheme for smooth convex minimization, with an $O(k^{-2})$ rate for function values (Nesterov 1983).
• 2009. Beck and Teboulle extend it to the composite problem above (FISTA), with the $O(k^{-2})$ rate (doi:10.1137/080716542).
• 2014. Su, Boyd and Candès read the scheme as a discretization of the ODE $\ddot x+\frac{\alpha}{t}\dot x+\nabla\Theta(x)=0$ (arXiv:1503.01243).
• 2014–2015. Chambolle and Dossal (doi:10.1007/s10957-015-0746-4) and, independently, Attouch, Chbani, Peypouquet and Redont (arXiv:1507.04782) prove weak convergence of the iterates for the variant with parameter $\alpha>3$. Before that, convergence of the iterates had been open for about two decades.
• 2015. May shows that for $\alpha>3$ the continuous-time gap is $o(t^{-2})$ (arXiv:1509.05598).
• 2016. Attouch and Peypouquet prove the discrete analogue: for $\alpha>3$ the function gap of the algorithm is $o(k^{-2})$ and the velocity is $o(k^{-1})$ (arXiv:1510.08740, SIAM J. Optim. 26(3):1824–1834).

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let:

1. $\Psi:\mathcal H\to\mathbb R\cup\{+\infty\}$ be proper (finite somewhere), lower semicontinuous and convex;
2. $\Phi:\mathcal H\to\mathbb R$ be convex and continuously differentiable, with gradient $\nabla\Phi$ Lipschitz continuous with constant $L$;
3. $\Theta=\Psi+\Phi$, and assume the set of minimizers $S=\operatorname{argmin}\Theta$ is nonempty.

For $s>0$, the proximal map $\operatorname{prox}_{s\Psi}(z)$ is the unique minimizer of $u\mapsto\Psi(u)+\frac1{2s}\|u-z\|^2$. Given $\alpha>0$, a step size $0<s<1/L$ and starting points $x_0,x_1$, algorithm (2) generates

$$y_k=x_k+\frac{k-1}{k+\alpha-1}(x_k-x_{k-1}),\qquad x_{k+1}=\operatorname{prox}_{s\Psi}\big(y_k-s\nabla\Phi(y_k)\big),\qquad k\ge1.$$

The common choice is $\alpha=3$; this mission concerns $\alpha>3$.

The proofs use the operator $G_s(y)=\frac1s\big(y-\operatorname{prox}_{s\Psi}(y-s\nabla\Phi(y))\big)$, the sequence $z_k=x_k+\frac{k-1}{\alpha-1}(x_k-x_{k-1})$, a minimizer $x^*$, and the quantity

$$\mathcal E(k)=\frac{2s}{\alpha-1}(k+\alpha-2)^2\big(\Theta(x_k)-\Theta(x^*)\big)+(\alpha-1)\|z_k-x^*\|^2 .$$

Write $\theta_k=\Theta(x_k)-\Theta(x^*)$ and $d_k=\frac1{2s}\|x_{k+1}-x_k\|^2$.

Formalization targets

Goal: Theorem 1 (p. 2)

For $\alpha>3$ and $0<s<1/L$,

$$\lim_{k\to\infty}k^2\big(\Theta(x_k)-\min\Theta\big)=0\qquad\text{and}\qquad\lim_{k\to\infty}k\,\|x_{k+1}-x_k\|=0.$$

The statement fixes no constants, so it is unaffected by later improvements of the explicit bounds below.

Milestones (in attack order)

1. (9), p. 2. If $sL\le1$, then for all $x,y$: $\Theta(y-sG_s(y))\le\Theta(x)+\langle G_s(y),y-x\rangle-\frac s2\|G_s(y)\|^2$.
2. (13), p. 3. For $\alpha\ge3$ and $k\ge1$: $\mathcal E(k+1)+2s\frac{\alpha-3}{\alpha-1}k\,\theta_k\le\mathcal E(k)$.
3. Fact 1, p. 3. $(\mathcal E(k))$ is nonincreasing and has a finite limit.
4. Fact 2, p. 3. $\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(k+\alpha-2)^2}$ and $\|z_k-x^*\|^2\le\frac{\mathcal E(1)}{\alpha-1}$ for $k\ge1$.
5. Fact 3, p. 3. For $\alpha>3$: $\sum_{k\ge1}k\,\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(\alpha-3)}$.
6. (14), p. 4. $\Theta(x_{k+1})+d_k\le\Theta(x_k)+\frac{(k-1)^2}{(k+\alpha-1)^2}d_{k-1}$ for $k\ge1$.
7. Fact 4, p. 4. For $\alpha>3$: $\sum_{k\ge1}k\,d_k\le\frac{\alpha(3\alpha-5)\mathcal E(1)}{4s(\alpha-1)(\alpha-3)}$.
8. Lemma 2, p. 4. For $\alpha>3$, $\lim_k\big[k^2d_k+(k+1)^2\theta_{k+1}\big]$ exists and is finite.

Significance

The result. The $O(k^{-2})$ rate of FISTA is often quoted as optimal for first-order methods. Theorem 1 shows that for $\alpha>3$ the worst-case rate along every single run is strictly better, $o(k^{-2})$, and that the steps $\|x_{k+1}-x_k\|$ decay faster than $1/k$. No better power is possible: by Attouch et al., Example 2.13 there is no $p>2$ with an $O(k^{-p})$ rate for every $\Phi$ and $\Psi$. The intermediate estimates (Facts 2–4) give explicit, quantitative bounds that are reused in the analysis of inexact and perturbed variants (Theorem 4 of the paper) and in mission II of this series, which proves weak convergence of the iterates.

Formalizing it. The result is proved on paper. As far as we know, no machine-checked proof of the $O(k^{-2})$ rate of FISTA in this Hilbert-space, extended-valued setting exists in Mathlib or on this platform, and neither does the $o(k^{-2})$ refinement. A complete development would provide reusable statements about proximal-gradient steps for functions valued in $\mathbb R\cup\{+\infty\}$. The page also has a factor slip in Fact 4 and Lemma 2 (see Formalization scope); checking it mechanically is one of the outputs.

Difficulty

The $O(k^{-2})$ bound follows from the monotonicity of $\mathcal E$ alone. That argument cannot give $o(k^{-2})$: it controls $k^2\theta_k$ only by the constant $\mathcal E(1)$, and summability of $k\theta_k$ (Fact 3) gives a decay of $k^2\theta_k$ only along a subsequence, not of the whole sequence. The missing ingredient is convergence of a weighted combination of function gaps and velocities, which is Lemma 2. The bookkeeping is delicate: every step carries explicit coefficients in $k$ and $\alpha$, and the inequalities must hold in the extended reals because $\Psi$ may be $+\infty$ at the starting point.

Formalization scope

• Space and functions. $\mathcal H$ is a real inner product space that is complete. $\Psi$ takes values in EReal and satisfies the published predicate IsProperClosedConvex (never $-\infty$, finite somewhere, lower semicontinuous, convex epigraph). $\Phi:\mathcal H\to\mathbb R$ is ConvexOn and ContDiff ℝ 1, and gradient Φ is LipschitzWith L for some L : ℝ≥0.
• Step size. $0<s<1/L$ is written 0 < s and s * L < 1, so that $L=0$ is allowed (s < 1 / L would be unsatisfiable when $L=0$). Display (9) uses the page's $s\le1/L$, written s * L ≤ 1.
• Proximal map. It is a map P with the published predicate IsProx s Ψ P, which determines $P=\operatorname{prox}_{s\Psi}$ for proper closed convex $\Psi$ and $s>0$.
• The run. It is required to follow (2) for every $k\ge1$, with $x_0,x_1$ arbitrary; the coefficient of $x_0$ vanishes at $k=1$.
• Extended reals. $\Theta$, $\mathcal E$ and the function-value statements live in EReal. No value is ever converted to $\mathbb R$ with toReal, which would turn $+\infty$ into $0$. "The limit exists" (Fact 1, Lemma 2) means convergence to a real number, because in EReal every monotone sequence converges. Infinite series of nonnegative terms are stated as bounds on every partial sum. $\min\Theta$ in the goal is ⨅ y, Θ y together with the hypothesis that a minimizer exists.
• Corrected slips. Fact 2 is stated with $\mathcal E(1)$ for $k\ge1$; the page writes $\mathcal E(0)$ for $k\ge0$, which needs an iterate $x_{-1}$. Fact 4 is stated for $\sum k\,d_k$; the page prints $\sum k\|x_{k+1}-x_k\|^2$ with the same constant, which is off by the factor $2s$ and false in general. Lemma 2 is stated for the bracket $k^2d_k+(k+1)^2\theta_{k+1}$ of its proof (16).
• Ruled out. The goal assumes nothing about $\mathcal E$, $z_k$, $\theta_k$ or $d_k$. A statement of the first limit for toReal values, or with an extended-real "limit exists", would be trivially weaker and is not what is asked.
• Welcome contributions. Proofs of any milestone; general facts about proximal maps of EReal-valued convex functions and about the descent property of $L$-smooth convex functions, which are reusable well beyond this mission.

Selected references

• H. Attouch, J. Peypouquet, The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than $1/k^2$, SIAM J. Optim. 26(3):1824–1834, 2016. arXiv:1510.08740v4, doi:10.1137/15M1046095
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168:123–175, 2018. arXiv:1507.04782
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2(1):183–202, 2009. doi:10.1137/080716542
• A. Chambolle, C. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166:968–982, 2015. doi:10.1007/s10957-015-0746-4
• R. May, Asymptotic for a second order evolution equation with convex potential and vanishing damping term, 2015. arXiv:1509.05598
• Y. Nesterov, A method of solving a convex programming problem with convergence rate $O(1/k^2)$, Soviet Math. Dokl. 27:372–376, 1983. mathnet
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17(153):1–43, 2016. arXiv:1503.01243

Motivation

Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.

What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.

Setting

Fix one item. Time is counted in whole periods $t = 0, 1, 2, \dots$, and $J$ is the finite set of bases. For each base $j$:

• $T_{i0}$ is the repair lead time, so shipments are decided in periods $t = 0, \dots, T_{i0}$;
• $T^r_{ij}$ and $T^e_{ij}$ are the regular and expedited transportation times from the depot to base $j$, integers with $1 \le T^e_{ij} < T^r_{ij}$;
• $\tilde S_{i0t}$ is the known cumulative supply at the depot through period $t$ (stock on hand plus arrivals already in the pipeline), and $\tilde S_{ijt}$ the known cumulative supply at base $j$. The latter is constant for $t \ge T^r_{ij}$, since nothing not yet shipped can arrive earlier than $T^r_{ij}$ by regular transport;
• $X_{ijt}$ is the cumulative demand at base $j$ through period $t$, a nonnegative integer random variable, nondecreasing in $t$, with finite mean;
• $h_{ij} > 0$, $b_{ij} > 0$ and $e_{ij} \ge 0$ are the incremental holding, shortage and expediting costs.

If $S_{ijt}$ units have arrived at base $j$ by period $t$, the expected cost of that period is

$$G_{ijt}(S) = h_{ij}\,E[S - X_{ijt}]^+ + b_{ij}\,E[X_{ijt} - S]^+,$$

and stock left at the end of the horizon costs

$$Q_{ij}(S) = h_{ij}\sum_{t > T^r_{ij} + T_{i0}} E[S - X_{ijt}]^+ .$$

The stock allocation model $\mathrm{SAM}_i$ chooses nonnegative integer regular shipments $y^r_{ijt}$, $t = 0, \dots, T_{i0}$, with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base $j$ is $S_{ijt} = \tilde S_{ij(T^r_{ij}-1)} + \sum_{t' \le t - T^r_{ij}} y^r_{ijt'}$, and the model minimizes $\sum_j \{\sum_{t=T^r_{ij}}^{T^r_{ij}+T_{i0}} G_{ijt}(S_{ijt}) + Q_{ij}(S_{ij(T^r_{ij}+T_{i0})})\}$. The extended model $\mathrm{ESAM}_i$ adds expedited shipments $y^e_{ijt}$, which arrive after $T^e_{ij}$ periods at an extra cost $e_{ij}$ per unit.

The constrained newsvendor problem $\mathrm{CN}_{ijt}$ minimizes $G_{ijt}(S)$ over integers $S \ge \tilde S_{ijt}$. Its largest optimal solution is written $\hat S_{ijt}$.

Formalization targets

Goal: Theorem 15 (p. 237)

In every optimal solution of $\mathrm{SAM}_i$, for every base $j$ and every $t \in [T^r_{ij}, T^r_{ij} + T_{i0}]$,

$$\tilde S_{ij(T^r_{ij}-1)} \;\le\; S^*_{ijt} \;\le\; \hat S_{ijt}.$$

The bound is uniform over optimal solutions and uses nothing but the single-period problems.

Milestones

1. Separability (Section 10.4.1, p. 236). The multi-item problem $\mathrm{SAM}$ splits into the $\mathrm{SAM}_i$: its optimal solutions are exactly the tuples of optimal item solutions, and $Z^* = \sum_i Z^*_i$.
2. Convexity of $Q_{ij}$ (p. 234) and of $G_{ijt}$ (p. 237), in the discrete sense of nondecreasing first differences on $\mathbb Z$.
3. The newsvendor solution (10.19). $\hat S_{ijt} = \max(\tilde S_{ijt}, s^0)$ with $s^0$ the least integer such that $P(X_{ijt} \le s^0) > b_{ij}/(b_{ij}+h_{ij})$.
4. Monotonicity (10.20). $\hat S_{ij(t-1)} \le \hat S_{ijt}$ on $[T^r_{ij}, T^r_{ij} + T_{i0}]$.
5. Theorem 16, corrected (p. 244). In every optimal solution of $\mathrm{ESAM}_i$, $\tilde S_{ijt} \le S^*_{ijt}$. Writing $M_{jt} = \max_{k \in [T^e_{ij}, t]}(\hat S_{ijk} - \tilde S_{ijk})$, also $S^*_{ijt} \le \tilde S_{ijt} + M_{jt}$, provided $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$.

Two supporting items state that $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.

Significance

Theorem 15 is what allows the book (pp. 238–239) to rewrite $\mathrm{SAM}_i$ with 0–1 variables $\delta_{ijtk}$ indicating $S_{ijt} = k$. Only $k$ between $\tilde S_{ij(T^r_{ij}-1)}$ and $\hat S_{ijt}$ is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.

The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With $T^r_{ij} \ge T^e_{ij} + 2$, an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.

Difficulty

The central step is the exchange. Take the first period $k$ in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at $k$. This must be shown feasible, to change only $S_{ijk}$, and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums $\min(t - T^e_{ij}, T_{i0})$, and cumulative constraints across bases.

The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For $\mathrm{ESAM}_i$ even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.

Formalization scope

• One item at a time: ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space $(\Omega, P)$, [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.
• $G$ and $Q$ are defined from the demand as in the book: Bochner integrals of $(S - X)^+$ and $(X - S)^+$, and a tsum for $Q$. The item model requires finite means and convergence of the series for $Q$ at every stock level, so that no integral or sum takes Lean's junk value $0$.
• "The largest optimal solution" is the predicate IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take $\hat S$ as a function satisfying it. Milestone (10.19) shows it exists.
• "An optimal solution" means a feasible plan with objective at most that of every feasible plan. The theorems hold for every optimal plan.
• Pinned conventions and additions. The following are not written in the book: $h_{ij}, b_{ij} > 0$ and $e_{ij} \ge 0$; nonnegative, nondecreasing depot supply; nondecreasing base supply (used in the book's proof of Theorem 16); finite mean demand; convergence of $Q$'s series. (10.19) is read with the critical fractile "least $s$ with $F(s) > b/(b+h)$", the book's $\lceil F^{-1}\rceil$/$\lfloor F^{-1}\rfloor$ with ties broken upward. Theorem 16 carries the proviso "$T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$". Separability is stated both for optimal plans and for optimal values.
• Ruled out. The feasible sets of $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ impose no upper bound on the cumulative stock, and $\hat S$ is defined from $G$ alone, never from the allocation problem. The bounds are therefore not true by definition.
• Omitted. The LP reformulations (10.22)–(10.28) and (10.45)–(10.52) and the integrality of their relaxations, which the book asserts with a reference to [68]; the greedy algorithms and their optimality conditions (asserted); the book's claim that $Q_{ij}$ is strictly increasing (p. 238), which fails when $P(X_{ijt} \le S) = 0$ beyond the horizon and is not needed; the dynamic program of Section 10.3 and the repair model of Section 10.6.
• The discrete-convexity and newsvendor facts are reusable for any single-location inventory model on $\mathbb Z$. Contributions are welcome on the convexity lemmas, the critical-fractile characterization, and a reusable exchange lemma for cumulative-shipment models.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005, Chapter 10, pp. 225–246. DOI 10.1007/b138879
• K. J. Arrow, T. Harris, J. Marschak, "Optimal inventory policy", Econometrica 19(3), 1951, 250–272 (the newsvendor critical fractile). DOI 10.2307/1906813

Motivation

A stocking point that reviews its inventory once per period and must decide how much to order is the basic unit of every service parts supply chain: each warehouse, each repair depot and each forward location in the networks studied later in Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) faces this decision for thousands of items. The practical rule used everywhere is the order-up-to (base-stock) rule: bring the inventory position up to a fixed target level whenever it falls below it, and order nothing otherwise. Chapter 2 of the book justifies this rule for a single item with linear costs, following the dynamic-programming argument of Karlin and Scarf, and the rest of the book takes the rule as given.

Timeline. Arrow, Harris and Marschak posed the periodic-review inventory problem as a dynamic program in 1951 (Econometrica). Bellman, Glicksberg and Gross showed in 1955 that with linear ordering cost and convex expected holding and shortage costs the optimal policy has a critical-number form (Management Science). Karlin and Scarf (1958) extended the analysis to a positive lead time, the setting of the book's Theorems 1–3. Veinott (1965) gave conditions under which a base-stock policy is optimal in multi-product, nonstationary models (Management Science).

Setting

One item is stocked at one location. At the start of each period the inventory position $y$ is observed and a quantity $u \ge 0$ is ordered; with lead time one period it arrives at the start of the next period. Demand in each period is independent of other periods and has a density $g$ on $(0,\infty)$ that is positive and continuous. Unmet demand is backordered. Costs are linear: $c$ per unit ordered, $h$ per unit on hand at the end of a period, $b$ per unit backordered at the end of a period, and future costs are discounted by $\alpha \in (0,1)$. The one-period cost is

$$L(y) = \begin{cases} h\displaystyle\int_0^y (y-x)g(x)\,dx + b\int_y^\infty (x-y)g(x)\,dx, & y > 0,\\[1mm] b\displaystyle\int_0^\infty (x-y)g(x)\,dx, & y \le 0. \end{cases}$$

The book assumes throughout that $b > \frac{1-\alpha}{\alpha}\,c$: the backorder cost outweighs the saving from deferring a purchase.

The $n$-period value functions are $f_1 = L$ and, for $n \ge 2$,

$$f_n(y) = \min_{u \ge 0}\Big\{ c\,u + L(y) + \alpha\int_0^\infty f_{n-1}(y+u-x)\,g(x)\,dx \Big\}.$$

An order $u$ is optimal at $y$ if it attains this minimum over all $u \ge 0$. The order-up-to rule with level $s$ orders $u(y) = \max\{0, s-y\}$. The marginal function of eq. (2.8) is $F_n(w) = c + \alpha\int_0^\infty f_n'(w-x)\,g(x)\,dx$. In Lean these are Model, Model.L, Model.f, Model.IsOptimalOrder, Model.IsOrderUpToOptimal and Model.F in the namespace ServiceParts.BaseStock.

Formalization targets

Goal: Theorem 2 (p. 18) in its $n$-period form

For every horizon $n \ge 2$, either there is a real level $s_n^*$ with

$$u_n^*(y) = \max\{0,\ s_n^* - y\} \ \text{optimal for every } y,$$

or ordering nothing is optimal for every $y$ (level $-\infty$); and there is $N \ge 2$ such that the level is real for all $n \ge N$. No value of $s_n^*$ is fixed: the goal asserts the shape of the optimal policy only.

Milestones, in attack order

1. $L$ is convex (p. 21).
2. Every $f_n$, $n \ge 1$, is convex (p. 19, property (c)).
3. Every $f_n$ is differentiable with $-(c+b) \le f_n' \le h/(1-\alpha)$ (p. 20).
4. Property (b): given an optimal real level $s$ for horizon $n \ge 2$, $f_n' = -c + L'$ below $s$ and $f_n' = L' + \alpha\int_0^\infty f_{n-1}'(\cdot - x)g(x)\,dx$ from $s$ on (p. 19).
5. Given such a level, $F_n(w) \to (1-\alpha)c - b\alpha < 0$ as $w \to -\infty$ (p. 19).
6. Property (a): optimal real levels are nondecreasing in the horizon, $s_n^* \le s_{n+1}^*$ (p. 18).

Significance

The theorem reduces an infinite-dimensional control problem, a choice of order quantity for every possible inventory position, to one number per period. Every later chapter of the book (Palm's theorem for $(s-1,s)$ policies, METRIC-type stock level optimization, allocation in multi-echelon systems) parameterizes policies by such stock levels; this is where the book justifies that parameterization.

The result is classical and proved in many texts. On Prove2Me the mission produces a machine-checked finite-horizon version with a continuous demand density, including the calculus the proof needs: convexity of an expected cost defined by integrals against a density, differentiation under the integral sign in the recursion, and the one-sided behaviour of the value function at the order-up-to level. Existing platform results on base-stock optimality (Veinott's multi-product model, advance demand information) use different models and different arguments; none covers this recursion.

Difficulty

The argument is an induction on $n$ whose hypothesis carries convexity, the derivative formula (b), and bounds on $f_n'$. The delicate step is the existence of a finite root of $F_n$: its limit at $-\infty$ depends on whether the previous level was finite. For $n = 1$ nothing is ordered and the limit is $c - b\alpha$, which the assumption $b > \frac{1-\alpha}{\alpha}c$ does not make negative. The book's base case ("left to the reader") therefore fails when $c > \alpha b$: with $\alpha = \tfrac12$, $c = 1$, $b = \tfrac32$ the two-period problem never orders. The goal is corrected accordingly.

Two properties the book's induction also carries are not usable as printed. Property (d), $f_n' \le f_{n-1}'$, is false: for large $y$, $f_n'(y)$ approaches $h(1 + \alpha + \dots + \alpha^{n-1})$, which increases with $n$. The second-derivative clause of property (c) fails at $y = 0$ whenever $g(0^+) > 0$. A solver cannot follow the printed induction step for step; property (a), which the book derives from (d), is true and is a milestone in its own right.

Formalization scope

• Horizon. The book states Theorem 2 for "the optimal policy" without a horizon. Its proof is an induction on a finite horizon, and the passage $n \to \infty$ is left as a conjecture (p. 21). The goal is the finite-horizon theorem; no infinite-horizon value function is constructed.
• Lead time. The proof sets $\tau = 1$ "to simplify notation"; so does the formalization. Theorem 1 (dependence on the inventory position only) and Theorem 3 (general $\tau$, whose level equation is the conjectured infinite-horizon one) are not stated.
• Level $-\infty$. The goal allows "never order" as the order-up-to rule with level $-\infty$ and adds eventual finiteness; see Difficulty.
• Added hypotheses. $c \ge 0$, $h > 0$ (the book uses $\lim_{w\to\infty} f_n'(w - x) > 0$), $0 < \alpha$ (the book divides by $\alpha$), and a finite mean $\int_0^\infty x\,g(x)\,dx < \infty$ (without it $L$ is infinite). All are fields of Model, together with positivity and continuity of $g$ on $(0,\infty)$, $\int_0^\infty g = 1$, and $b > \frac{1-\alpha}{\alpha}c$.
• Minimum and derivatives. $f_n$ is defined with the infimum over $u \ge 0$ of a nonnegative quantity; optimality is always against every $u' \ge 0$. Statements about $f_n'$ assert differentiability (Differentiable, HasDerivAt) and do not read deriv as evidence of it.
• Levels. The book's $s_n^*$ is "the unique solution of (2.6)"; milestones take any real level at which the order-up-to rule is optimal.

A recursion in which ordering is restricted to order-up-to rules, or in which $f_n$ is defined through $s_n^*$, would make the goal a tautology; here $f_n$ is defined by minimization over all $u \ge 0$ and optimality is checked against all orders.

Needed infrastructure: convexity and differentiation of parametric integrals against a density on $(0,\infty)$, and minimization of a differentiable convex function over a half-line. Both are reusable for the other stochastic inventory missions on the platform. Proofs of individual milestones are welcome independently of the goal.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 2, Section 2.1. https://doi.org/10.1007/b138879
• S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in K. J. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958 (no DOI).
• K. J. Arrow, T. Harris and J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906814
• R. Bellman, I. Glicksberg and O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
• A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206

Why certify nonconvex scenario solutions

The scenario approach replaces an optimization problem with uncertain constraints $\theta\in\Theta_\delta$, $\delta\in\Delta$, by the program that enforces only $N$ constraints $\Theta_{\delta_1},\dots,\Theta_{\delta_N}$ drawn at random from the distribution $\mathbb P$ of the uncertainty. Its solution $\theta^*$ is then judged by its violation, the probability that a new instance $\delta$ is not satisfied. For convex programs in $\mathbb R^d$ the violation is controlled by the dimension $d$ alone (Calafiore and Campi 2006; Campi and Garatti 2008), because a convex program has at most $d$ support constraints. Many problems where the scenario approach is used in practice are not convex: control with quantized inputs, mixed-integer design, classification with nonconvex losses, and decisions over infinite-dimensional or unstructured sets. For those programs no a priori bound on the number of constraints that determine the solution exists.

Timeline, as recorded in Chapter 8 of Campi and Garatti's textbook:

• 2006–2008: the violation of convex scenario solutions is bounded, and then characterized exactly, in terms of $d$.
• 2018: the wait-and-judge theory (Campi and Garatti, Math. Programming 2018) evaluates the violation from the number of support constraints counted after solving the program; it extends to nonconvex programs but requires a nondegeneracy assumption.
• 2018: Campi, Garatti and Ramponi (IEEE TAC 2018) prove a bound in terms of the size of any support set, with no convexity and no nondegeneracy assumption. This is the result formalized here, stated in the book as Eq. (8.15).

Setting

Let $\Theta$ be a generic set; it may be an infinite-dimensional space or a set with no algebraic structure. Let $f:\Theta\to\mathbb R$ be a cost and $\Theta_\delta\subseteq\Theta$ constraint sets indexed by $\delta\in\Delta$, where $\Delta$ carries a probability $\mathbb P$. Neither $f$ nor the $\Theta_\delta$ is required to be convex. With a sample $\delta_1,\dots,\delta_N$ drawn independently from $\mathbb P$, the scenario program is

$$\min_{\theta\in\Theta} f(\theta)\quad\text{subject to}\quad \theta\in\bigcap_{i=1,\dots,N}\Theta_{\delta_i},\tag{8.12}$$

and $\theta^*$ denotes its solution, assumed to exist and be unique for every sample.

The violation of a decision is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$ (Definition 3.1).

A support set (Definition 8.8) is a subset $\{\Theta_{\delta_{i_1}},\dots,\Theta_{\delta_{i_k}}\}$ of the constraints such that the program with only these constraints in place has the same solution $\theta^*$ as the program with all constraints. The full set of constraints is always a support set; a support set need not be minimal (of smallest cardinality) or irreducible (with no removable element). Let $\sigma^*$ be the cardinality of the support set returned, for every sample, by some fixed algorithm.

Formalization targets

Goal: the support-set bound, Eq. (8.15)

For every function $\epsilon:\{0,1,\dots,N\}\to[0,1]$ with $\epsilon(N)=1$,

$$\mathbb P^N\{V(\theta^*)>\epsilon(\sigma^*)\}\le\sum_{k=0}^{N-1}\binom Nk\,(1-\epsilon(k))^{N-k}.$$

The level function $\epsilon$ is free: the statement is one inequality per admissible $\epsilon$, and it holds for any algorithm producing support sets. This is the weakest form that carries the whole result.

Milestone: the level function for a confidence $\beta$, Eq. (8.16)

For $\beta\in[0,1]$ let

$$\epsilon(k)=\begin{cases}1 & k=N,\\ 1-\sqrt[N-k]{\dfrac{\beta}{N\binom Nk}} & \text{otherwise.}\end{cases}$$

The arithmetic half states that $\epsilon$ maps $\{0,\dots,N\}$ into $[0,1]$, $\epsilon(N)=1$, and the right-hand side of (8.15) equals $\beta$ (for $N\ge1$). The probabilistic half states $\mathbb P^N\{V(\theta^*)>\epsilon(\sigma^*)\}\le\beta$.

Significance

The result turns the size of a support set, a quantity observed after the program is solved, into a certificate on the violation of the solution, for any optimization or decision problem whose solution is determined by a subset of the data. With the choice (8.16), a user who finds a support set of size $\sigma^*$ can assert $V(\theta^*)\le\epsilon(\sigma^*)$ with confidence $1-\beta$. The book's Figure 8.12 shows that $\epsilon(k)$ for $\beta=10^{-6}$ remains well below $1$ for $k$ up to a sizeable fraction of $N$. Because the algorithm that finds the support set is arbitrary, cheap heuristics that return non-minimal support sets still give valid, if weaker, guarantees. The result does not recover the tight convex bound (3.4); for convex programs the Chapter 3 theory remains sharper.

The statement is proved in [31] and is the probabilistic core of the sample-compression arguments of learning theory (Floyd and Warmuth 1995) in the form used by the scenario approach. To the best of available knowledge it has no machine-checked proof. The platform's UnderstandingML.compression_bound proves a sample-compression bound for a fixed compression size with a different constant; it does not cover a data-dependent size $\sigma^*$ or an arbitrary level function. A formal proof here provides a reusable bound for data-dependent support sets over arbitrary decision sets.

Difficulty

The natural first step is: condition on the support set being a particular index set $I$ with $|I|=k$, and argue that the solution is then a function of the $k$ sampled constraints in $I$ alone, while the other $N-k$ samples are independent of it and must all be satisfied. The difficulty is that the event "the algorithm returns $I$" depends on all $N$ samples, and the solution of the reduced program on $I$ is defined only where that program has a unique solution; the decomposition of the probability therefore has to be carried out on sections of the product space, with a measurability argument for each piece. A second point is that $\sigma^*$ is random and data-dependent: a bound for each fixed $k$ does not directly give a bound at the random level $\epsilon(\sigma^*)$, and the role of the condition $\epsilon(N)=1$ must be accounted for at $k=N$.

Formalization scope

Lean representation and committed conventions:

• $\Theta$ and $\Delta$ are arbitrary types with measurable structures; $\mathbb P$ is a probability measure on $\Delta$; a sample is ω : Fin N → Δ with law Measure.pi (fun _ : Fin N => P); indices run over $0,\dots,N-1$.
• A subset of constraints is a Finset (Fin N); the reduced program with index set $I$ has feasible set $\bigcap_{i\in I}\Theta_{\delta_i}$ (all of $\Theta$ for $I=\emptyset$).
• The solution map $\theta^*$ is a parameter with the hypothesis that $\theta^*(\omega)$ is the unique solution of the full program for every sample.
• "Has the same solution" in Definition 8.8 means: the reduced program has a unique solution and it equals the unique solution of the full program. Existence of solutions is not assumed for reduced programs in general, only for those that are support sets.
• The algorithm is an arbitrary map alg : (Fin N → Δ) → Finset (Fin N) returning a support set for every sample; $\sigma^*$ is the cardinality of its output. The goal is universal over such maps.
• $\epsilon$ is a real function on $\mathbb N$ with $\epsilon(k)\in[0,1]$ for $k\le N$ and $\epsilon(N)=1$.
• The violation is real-valued in $[0,1]$; the probability of the event is compared in $[0,\infty]$ with ENNReal.ofReal of the real right-hand side.

Implicit hypotheses of the page, made explicit (the book states on p. 33 that measurability issues are glossed over): the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is measurable in $\Theta\times\Delta$; the solution map is measurable; each event $\{\omega:\text{the algorithm returns }J\}$ is measurable; $\theta^*$ exists and is unique for every sample; $N\ge1$ in the arithmetic half of (8.16).

A trivializing formalization is ruled out: the algorithm is not existentially quantified and is not the minimal support set, the reduced programs are not all assumed solvable (which would be unsatisfiable when $f$ has no unconstrained minimizer), and the support-set property requires uniqueness of the reduced solution, without which the bound is false.

Needed infrastructure: product measures on Fin N → Δ, splitting of such products along a subset of coordinates, and Fubini/Tonelli for sections. These pieces are reusable for other compression-type bounds. Contributions welcome: proofs of the two milestones and of the goal, and lemmas on splitting Measure.pi over a Finset of coordinates.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018, §8.6, pp. 101–105. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, F. A. Ramponi, A general scenario theory for nonconvex optimization and decision making, IEEE Transactions on Automatic Control, 2018. https://doi.org/10.1109/TAC.2018.2808446
• M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. https://doi.org/10.1007/s10107-016-1056-9
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control, 2006. https://doi.org/10.1109/TAC.2006.875041
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization, 2008. https://doi.org/10.1137/07069821X
• S. Floyd, M. Warmuth, Sample compression, learnability, and the Vapnik–Chervonenkis dimension, Machine Learning, 1995. https://doi.org/10.1007/BF00993593