Optimization

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Optimal Policies for a Multi-Echelon Inventory Problem: The Two-Echelon Optimal Cost Splits into the Isolated Installation-1 Cost Plus a Function of Echelon StockResearch Paper

Motivation

Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.

Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.

Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.

Setting

Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density $\varphi$ on $(0,\infty)$ , independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost $c_1\ge0$ . The system orders $z\ge0$ units from outside at cost $c(z)=K+cz$ for $z>0$ and $c(0)=0$ (eq. (5)); these arrive at installation 2 one period later. Costs $n$ periods ahead are discounted by $\alpha^n$ , $\alpha\ge0$ .

The state at the start of a period is $(x_1,w_1,x_2)$ : $x_1$ is the stock on hand at installation 1, $w_1$ the stock that reaches installation 1 next period, and $x_2$ the echelon-2 stock (on hand at both installations plus in transit), so $x_1+w_1\le x_2$ . Installation 1 pays the expected holding and shortage cost (1),

L(x)=\begin{cases}hx+p\int_x^\infty(t-x)\varphi(t)\,dt,&x>0,\\ p\int_0^\infty(t-x)\varphi(t)\,dt,&x\le0,\end{cases}

and echelon 2 pays a natural one-period cost $\tilde L(x_2)$ (Assumption 3).

With $n$ periods remaining, the optimal system cost $C_n(x_1,w_1,x_2)$ satisfies, with $C_0\equiv0$ ,

C_n(x_1,w_1,x_2)=\min_{\substack{x_1+w_1\le y\le x_2\\0\le z}}\Big\{c(z)+c_1(y-x_1-w_1)+\tilde L(x_2)+L(x_1)+\alpha\int_0^\infty C_{n-1}(x_1+w_1-t,\,y-x_1-w_1,\,x_2+z-t)\varphi(t)\,dt\Big\}\qquad(14)

where $y$ is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost $c_1$ with a two-period lag, has optimal cost $\hat C_n(x_1,w_1)$ , $\hat C_0\equiv0$ :

\hat C_n(x_1,w_1)=\min_{y\ge x_1+w_1}\Big\{c_1(y-x_1-w_1)+L(x_1)+\alpha\int_0^\infty\hat C_{n-1}(x_1+w_1-t,\,y-x_1-w_1)\varphi(t)\,dt\Big\}.\qquad(15)

In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by $n$ for the problem with $n+1$ periods remaining.

Formalization targets

Goal: Theorem 1 (p. 482)

There are functions $g_n$ with $g_1=\tilde L$ such that, for all $n\ge1$ and $x_1+w_1\le x_2$ ,

C_n(x_1,w_1,x_2)=\hat C_n(x_1,w_1)+g_n(x_2),\qquad(16)

and installation 1 acts optimally by aiming at an isolated-optimal target $\hat y$ and taking $\min(x_2,\hat y)$ , as much as installation 2 can supply. The goal fixes no form for $g_n$ and needs no critical numbers.

Milestones

Convexity of $y\mapsto\alpha\int\!\!\int L(y-t_1-t_2)\varphi(t_1)\varphi(t_2)$ (§2 item 2, p. 478).
The isolated decomposition $\hat C_n(x_1,w_1)=L(x_1)+\alpha\int_0^\infty L(x_1+w_1-t)\varphi(t)\,dt+f_n(x_1+w_1)$ for $n\ge2$ , with $f_n$ of (7) (p. 480).
Convexity of every $f_n$ (§2 item 3, p. 478).
Eqs. (18)–(19) (p. 483): the system cost when echelon-2 stock is above or below the isolated critical number $\bar x_n$ .
Eqs. (21)–(25) (pp. 483–484): the shortfall cost $\Lambda_n$ depends on $x_2$ alone,

\Lambda_n(x_2)=c_1(x_2-\bar x_n)+\alpha^2\int_0^\infty\!\!\int_0^\infty[L(x_2-t-y)-L(\bar x_n-t-y)]\varphi(t)\varphi(y)\,dy\,dt+\alpha\int_0^\infty[f_{n-1}(x_2-t)-f_{n-1}(\bar x_n-t)]\varphi(t)\,dt.

Theorem 2 (p. 484), the explicit form: given critical numbers, $g_n$ is computed by (26), $g_n(x_2)=\min_{z\ge0}\{c(z)+\tilde L(x_2)+\Lambda_n(x_2)+\alpha\int g_{n-1}(x_2+z-t)\varphi(t)\,dt\}$ .

Significance

The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in $x_2$ with one-period cost $\tilde L+\Lambda_n$ . When $\tilde L$ is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of $(S,s)$ type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" $\Lambda_n$ is the prototype of the penalty functions used in the multi-echelon literature.

Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.

Difficulty

The obvious induction on $n$ substitutes (16) into (14) and separates the minimizations over $y$ and $z$ . The separation is immediate; the hard step is that the constrained minimum over $x_1+w_1\le y\le x_2$ differs from the unconstrained one by an amount that a priori depends on $(x_1,w_1)$ . Showing that it depends on $x_2$ alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on $(x_1,w_1)$ . On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against $\varphi$ . Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.

Formalization scope

Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:

The model is a structure Model whose fields carry the data and the standing hypotheses: $h,p,\alpha,c_1,K,c\ge0$ ; $\varphi\ge0$ with $\int_0^\infty\varphi=1$ ; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for $x\le0$ ) and $\tilde L$ non-negative, continuous and of at most linear growth (Assumption 3 leaves $\tilde L$ unspecified; these make every expectation in (14) finite and measurable). No discount bound $\alpha<1$ , no convexity of $\tilde L$ , no $K=0$ and no sign condition on $w_1$ is assumed.
Expectations are set integrals $\int_{(0,\infty)}F(t)\varphi(t)\,dt$ ; "Min" is a real infimum over a nonempty feasible set of a non-negative objective.
Every statement about $C_n$ is restricted to the state domain $x_1+w_1\le x_2$ ; outside it the feasible set of (14) is empty.
The horizon index counts periods remaining, $C_0\equiv\hat C_0\equiv0$ , and $f_n\equiv0$ for $n\le2$ .

A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which $g_n$ may depend on $(x_1,w_1)$ would make (16) trivial; the domain restriction, the integrability conditions and the order $\exists g\,\forall x_1,w_1,x_2$ rule these out. A sorry-free check (not part of the mission) verifies $C_1=L(x_1)+\tilde L(x_2)$ and $\hat C_1=L(x_1)$ and exhibits a model with exponential demand satisfying all hypotheses.

Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection $u\mapsto\inf_{y\ge u}$ and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases $n=1,2$ , and of any milestone are welcome.

Selected references

A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
S. Karlin and H. Scarf, Inventory Models of the Arrow-Harris-Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
F. Chen and Y.-S. Zheng, Lower Bounds for Multi-Echelon Stochastic Inventory Systems, Management Science 40(11):1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426

8 thms2 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time: Minimal Optimal Predecessor Lists Are Characterized by Strictly Increasing BreakpointsResearch Paper

Motivation

The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of $n$ periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.

Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with $O(n^2)$ running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained $O(n \log n)$ in general and $O(n)$ under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration $j$ it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.

Setting

For periods $i = 1, 2, \dots$ let $d_i$ be the demand, $K_i$ the setup cost, $c_i$ the variable per unit order cost and $h_i$ the cost of carrying a unit of inventory at the end of period $i$ . Write $D(i) = \sum_{k=1}^{i} d_k$ and $H(i) = \sum_{k=1}^{i} h_k$ , so $D(0) = H(0) = 0$ . For $i < j$ let $c_{ij} = c_i + h_i + \dots + h_{j-1}$ , let $\tilde C(i) = c_i - H(i-1)$ , and let

S(i, j) = \sum_{r=i}^{j-1} h_r\,\bigl(D(j) - D(r)\bigr)

be the carrying cost of an order placed in period $i$ that covers the demands of periods $i, \dots, j$ .

The costs are given by the zero-inventory recursion (2): $F(0) = 0$ and, for $1 \le l \le t$ ,

F(l, t) = F(l-1) + K_l + S(l, t) + c_l\,[D(t) - D(l-1)], \qquad F(t) = \min_{1 \le l \le t} F(l, t).

$F(l, t)$ is the cost of the first $t$ periods when the last setup is in period $l$ .

For two periods $k < l$ the difference $\Delta_{k,l}(t) = F(k,t) - F(l,t)$ is affine in $D(t)$ , with intercept $A(k,l)$ given by (4) and slope $c_{k,l} - c_l = \tilde C(k) - \tilde C(l)$ . Its root $G(k,l)$ is defined by (5): $A(k,l)/(\tilde C(l) - \tilde C(k))$ when the slopes differ, and $+\infty$ or $-\infty$ according to the sign of $A(k,l)$ when they agree. It is extended symmetrically, $G(l,k) = G(k,l)$ .

At iteration $j$ the future demands are unknown, so a future horizon has a potential cumulative demand $x \ge D(j)$ . The $j$ th Minimal Optimal Predecessors list $\Omega(j)$ is the set of periods $l \le j$ that are the lowest-index optimal last setup period, among $\{1, \dots, j\}$ , for every potential cumulative demand in some open interval above $D(j)$ .

Formalization targets

Goal: Theorem 1(a)

Let $j \ge 1$ and let $S = \{i_1, \dots, i_r\}$ with $\Omega(j) \subseteq S \subseteq \{1, \dots, j\}$ , ranked so that $\tilde C(i_1) \ge \dots \ge \tilde C(i_r)$ , with equal $\tilde C$ -values in ascending order of index. Put $g(1) = D(j)$ and $g(l) = G(i_l, i_{l-1})$ for $l = 2, \dots, r$ . Then

S = \Omega(j) \iff g(1) < g(2) < \dots < g(r) < \infty. \tag{6}

Milestones

In attack order:

identity (1a) for the carrying costs;
Lemma 2(a)–(d), the linearity of $\Delta_{k,l}$ and the sign test against its root $G(k,l)$ ;
the claim that $\Omega(j)$ contains an optimal last setup period for the horizon $j$ ;
the strict chains (7)–(8) of the Appendix;
Theorem 1(b), that under (6) the first entry $i_1$ is an optimal last setup period $l(j)$ ;
Theorem 1(c)(i)–(iii), the three elimination rules: $g(2) \le D(j)$ removes $i_1$ , $g(k+1) \le g(k)$ removes $i_k$ , and $g(r) = \infty$ removes $i_r$ .

A supporting item potCost_spec certifies that the potential costs used to define $\Omega(j)$ agree with the paper's $F(l,t)$ , up to a term that does not depend on $l$ .

Significance

Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, $\Omega(j)$ is maintained by deletions at the ends and in the interior of a list ordered by $\tilde C$ , and each period is inserted and deleted at most once; the $O(n \log n)$ bound, and the $O(n)$ bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.

The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).

Difficulty

Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:

equal slopes, where $G = \pm\infty$ ;
several lines meeting at one point;
the lowest-index tie-breaking that makes $\Omega(j)$ minimal.

The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of $\Omega(j)$ , read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.

Formalization scope

Data and costs. The data are four functions $\mathbb N \to \mathbb R$ bundled in a structure; values at index $0$ are unused, and no sign conditions are imposed. $F$ is defined by the recursion (2) with $F(0) = 0$ . Its identification with the minimum cost over all feasible policies is the paper's Lemma 1 (Wagner–Whitin), which is not part of this mission. The horizon $n$ is not a parameter.
Breakpoints. $G$ and the critical values $g(\cdot)$ take values in EReal, so $\pm\infty$ are kept distinct from every real number. The final " $< \infty$ " of (6) is part of the condition.
Ranked lists. A ranked set is a duplicate-free List ℕ. Lean lists are 0-based, so the paper's $i_{m+1}$ and $g(m+1)$ are entry $m$ and gval j L m.
Disclosed change 1, $\Omega(j)$ . The page asks for a single potential cumulative demand $D \ge D(j)$ at which $l$ is the lowest-index optimum. With that reading, Theorem 1(a) "only if" and Theorem 1(c) fail when two lines tie exactly at a breakpoint (an explicit five-period instance is in the definition's note). The formalization requires $l$ to be the lowest-index optimum on a nondegenerate open interval of potential demands above $D(j)$ . This is the paper's own description of the list on p. 915: "the unique optimal last setup period for any horizon … with potential cumulative demand $g(k) < D < g(k+1)$ ".
Disclosed change 2, Lemma 2(d). The printed hypothesis " $c_{k,l} < c_l$ " duplicates part (c) and is read as " $c_{k,l} = c_l$ ". The equivalence " $\Delta_{k,l} \ge 0$ iff $D(t) \ge G(k,l)$ " is stated under $A(k,l) \ne 0$ , since $A(k,l) = 0$ gives $G = +\infty$ by (5).
Ruling out trivial formalizations. The hypotheses of the goal are satisfiable for every $j \ge 1$ : rank $\{1, \dots, j\}$ itself. $\Omega(j)$ is nonempty (a milestone). $F(t)$ for $t \ge 1$ is a minimum over the nonempty set $\{1, \dots, t\}$ , never a default value. $G$ is never replaced by a real-valued junk value at equal slopes.
Out of scope. Lemma 1, Lemma 3, Corollaries 1–5, Theorem 2, the Algorithm's pseudo-code and its complexity analysis, and the submodularity discussion of §5.
Reusable infrastructure. The model, the recursion (2), $A$ , $G$ and $\Omega(j)$ can be reused for the paper's algorithmic results and for related lot-sizing papers. Proofs of the milestones, in any order, are welcome.

Selected references

A. Federgruen and M. Tzur, A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time, Management Science 37(8):909–925, 1991. https://doi.org/10.1287/mnsc.37.8.909
H. M. Wagner and T. M. Whitin, Dynamic Version of the Economic Lot Size Model, Management Science 5(1):89–96, 1958. https://doi.org/10.1287/mnsc.5.1.89
A. Wagelmans, S. van Hoesel and A. Kolen, Economic Lot-Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40(1-supplement-1):S145–S156, 1992. https://doi.org/10.1287/opre.40.1.S145
A. Aggarwal and J. K. Park, Improved Algorithms for Economic Lot Size Problems, Operations Research 41(3):549–571, 1993. https://doi.org/10.1287/opre.41.3.549

16 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems: Algorithm OPT Returns an Optimal Reorder Point and Order QuantityResearch Paper

Motivation

(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$ , an order of size $Q$ is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.

For decades, computing an optimal pair $(r, Q)$ exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).

Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity $Q^*$ . It rests only on the form of the cost, not on a particular demand model.

Setting

Inventory positions are integers (demand arrives unit by unit). A fixed cost $\kappa>0$ is charged per order, and $G:\mathbb Z\to\mathbb R$ is the expected holding and backlogging cost rate as a function of the inventory position $y$ . In all the models of the paper the long-run average cost of the $(r,Q)$ policy, for an integer $r$ and an integer $Q\ge1$ , has the form

C(r,Q)=\Big[\kappa+\sum_{y=r+1}^{r+Q}G(y)\Big]\Big/Q. \tag{1}

The paper's standing assumptions on $G$ are:

$-G$ is unimodal: there is an integer $m$ with $G$ nonincreasing on $\{y\le m\}$ and nondecreasing on $\{y\ge m\}$ (flat stretches allowed);
$\lim_{|y|\to\infty}G(y)=\infty$ .

The sequence $y_Q$ . Let $y_1$ be an integer minimizing $G$ . Given $y_1,\dots,y_Q$ , let $L(Q)=\min\{y_1,\dots,y_Q\}$ and $R(Q)=\max\{y_1,\dots,y_Q\}$ , and set

y_{Q+1}=\begin{cases}L(Q)-1 & \text{if } G(L(Q)-1)\le G(R(Q)+1),\\ R(Q)+1 & \text{otherwise.}\end{cases}

So the window $[L(Q),R(Q)]$ grows by one point at a time towards the smaller neighbouring value, ties going left. Write $r^*(Q)$ for an optimal reorder point for a given $Q$ , and

C^*(Q)=\Big[\kappa+\sum_{i=1}^{Q}G(y_i)\Big]\Big/Q .

Algorithm OPT, Step 1. Variables $S,Q,C^*,r,R$ start at $S=\kappa+G(y_1)$ , $Q=1$ , $C^*=S$ , $r=y_1-1$ , $R=y_1+1$ . Each pass compares $G(r)$ and $G(R)$ ; on the smaller side (left on ties) it stops if $C^*$ is at most that value, and otherwise adds the value to $S$ and moves $r$ one step left or $R$ one step right; then $Q:=Q+1$ and $C^*:=S/Q$ . The output is the final $(r,Q)$ .

Formalization targets

Goal: Theorem 1

Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer $y_1$ of $G$ , stops after finitely many passes, and its output $(r,Q)$ satisfies $Q\ge1$ and

C(r,Q)\le C(r',Q')\qquad\text{for all integers } r' \text{ and all integers } Q'\ge 1 .

The goal fixes no constants and no demand model: it is a statement about every $G$ satisfying the standing assumptions.

Milestones, in proof order

§2, p. 811: $\{y_1,\dots,y_Q\}$ is the contiguous block $[L(Q),R(Q)]$ of $Q$ integers and carries the $Q$ smallest values of $G$ .
Figure 1 (p. 809): $y_{Q+1}$ has the least $G$ -value outside the window; in particular $G(y_1)\le G(y_2)\le\cdots$ .
Lemma 1: $L(Q)-1$ is an optimal reorder point for $Q$ .
Corollary 1: $r^*(Q)-1\le r^*(Q+1)\le r^*(Q)$ .
Display before (6): $\min_r C(r,Q)=C^*(Q)$ .
(6): $C^*(Q+1)=[QC^*(Q)+G(y_{Q+1})]/(Q+1)$ , and $C^*(Q+1)<C^*(Q)$ iff $G(y_{Q+1})<C^*(Q)$ .
Lemma 2: the smallest $q$ with $C^*(q)\le G(y_{q+1})$ exists and is an optimal order size.
Step 1 tracks the sequence: from the state $(\kappa+\sum_{i\le Q}G(y_i),\,Q,\,C^*(Q),\,L(Q)-1,\,R(Q)+1)$ one pass stops with $(L(Q)-1,Q)$ exactly when $C^*(Q)\le G(y_{Q+1})$ and otherwise moves to the same state for $Q+1$ .

Significance

The result turns the joint minimization of (1) over $(r,Q)\in\mathbb Z\times\mathbb Z_{\ge1}$ , an unbounded two-dimensional integer problem, into a single scan whose length is $Q^*$ plus the distance to the minimizer of $G$ . Because it uses only the form (1) and the unimodality of $-G$ , it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to $(r,nQ)$ policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of $Q$ .

The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general $G$ under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with $C(Q)$ and $Q^*$ given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal $-G$ .

Difficulty

The obvious argument says: for fixed $Q$ the sum in (1) should cover the $Q$ smallest values of $G$ , and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of $G$ : "the $Q$ smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on $y_1$ being a global minimizer together with the unimodality of $-G$ , not on convexity.

The stopping rule is the second point. Lemma 2 looks like a first-order condition, but $C^*(\cdot)$ need not be convex; optimality of the first stopping $q$ for all larger $Q$ uses that the values $G(y_i)$ are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs $G\to\infty$ , and fails for constant $G$ .

Finally, the goal is about an imperative loop. Connecting its five variables to $y_Q$ , $C^*(Q)$ and $L(Q)$ is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.

Formalization scope

Types. $G:\mathbb Z\to\mathbb R$ , $\kappa\in\mathbb R$ with $\kappa>0$ , reorder points in $\mathbb Z$ , order quantities in $\mathbb N$ with $Q\ge1$ required wherever a cost appears. Lean's $x/0=0$ makes $C(r,0)=0$ , so optimality is always quantified over $Q'\ge1$ and the goal asserts that the returned $Q$ is $\ge1$ .
Assumptions. " $-G$ unimodal" is NegUnimodal G: $\exists m$ , $G$ antitone on $(-\infty,m]$ and monotone on $[m,\infty)$ . " $\lim_{|y|\to\infty}G=\infty$ " is Coercive G: $G\to+\infty$ along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over $\mathbb Z$ -weights it holds for every function.
The sequence. $L(Q),R(Q)$ are defined by recursion on the window, and $y$ is 1-based with an unused value at index 0; that $L,R$ are the minimum and maximum of $\{y_1,\dots,y_Q\}$ , as the paper defines them, is the first milestone.
The algorithm. Step 1 is transcribed literally, including $G(r)\le G(R)$ → left and the non-strict tests $C^*\le G(r)$ , $C^*\le G(R)$ ; $G$ is evaluated directly instead of through the $\Delta G$ bookkeeping. The loop runs with a pass budget and returns nothing when the budget runs out; the goal states that for every large enough budget it returns an optimal pair.
Step 0 is not formalized. It scans $L=0,1,\dots$ for the first $L$ with $\Delta G(L)\ge0$ , under the paper's simplification $y_1>0$ ; under unimodality alone it can stop on a plateau before the minimum. The goal starts Step 1 from a given global minimizer $y_1$ , which is the paper's own §2 setup and matches its p. 812 remark that Step 0 may be replaced by a bisection search.
Not formalized: Theorem 1's second sentence (the operation count), the derivations of (1) for specific demand models, and (5).
Corrected slips. The printed proof of Lemma 2 writes $C(Q)-C(Q^*)$ with $C^*(Q)$ inside the bracket; the correct identity has $C^*(Q)-C^*(Q^*)$ and $C^*(Q^*)$ . Lemma 2's " $Q^*$ " is formalized as existence of the smallest $q$ with the property plus its optimality, since minimizers need not be unique; likewise " $r^*(Q)=L(Q)-1$ " means $L(Q)-1$ is an optimal reorder point.
Ruled out. Defining the algorithm's output as an argmin of $C$ , or by searching for Lemma 2's $q$ , would make the goal trivial; the algorithm is defined by its steps. A statement of the form "if the run returns a pair, it is optimal" would be vacuous for a loop that never stops; termination is part of the goal.

Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.

Selected references

A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
S. Browne and P. Zipkin, Inventory Models with Continuous, Stochastic Demands, Annals of Applied Probability 1(3):419–435, 1991. https://doi.org/10.1214/aoap/1177005875
H. L. Lee and S. Nahmias, Single-Product, Single-Location Models, in Handbooks in OR & MS vol. 4, 1993 (cited by the paper as a 1989 working paper).
I. Sahin, On the Objective Function Behavior in (s, S) Inventory Models, Operations Research 30(4):709–724, 1982. https://doi.org/10.1287/opre.30.4.709

10 thms2 active usersReviewed

Convex Optimization Linear algebra Operations Research·Captain: mikedeng1

A Nonlinear Programming Algorithm for Solving Semidefinite Programs via Low-rank Factorization: A Regular Local Minimum That Stays Locally Minimal After Adding a Zero Column Solves the SDPResearch Paper

Motivation

Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense $n\times n$ matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable $X\succeq 0$ by a factorization $X=RR^{T}$ with $R$ having only $r$ columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with $m$ linear constraints has an optimal solution of rank $r$ with $r(r+1)/2\le m$ , so a small number of columns suffices.

Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.

Setting

For real $p\times q$ matrices, the trace inner product is $A\bullet B=\operatorname{trace}(A^{T}B)$ . The data are symmetric matrices $C, A_1,\dots,A_m\in\mathcal S^n$ and a vector $b\in\mathbb R^m$ . The primal SDP and dual SDP are

\text{(1)}\quad \min\{C\bullet X : A_i\bullet X=b_i,\ i=1,\dots,m,\ X\succeq0\},\qquad \text{(3)}\quad \max\Big\{b^{T}y : S=C-\sum_{i=1}^m y_iA_i,\ S\succeq0\Big\}.

The standing assumptions of the paper are that $A_1,\dots,A_m$ are linearly independent and that there are feasible $X^*$ and $(S^*,y^*)$ with $C\bullet X^*=b^{T}y^*$ .

For a positive integer $r\le n$ , the low-rank program is

(N_r)\qquad \min\{C\bullet(RR^{T}) : A_i\bullet(RR^{T})=b_i,\ i=1,\dots,m,\ R\in\mathbb R^{n\times r}\}.

Its Lagrangian is $L(R,y)=C\bullet(RR^{T})-\sum_i y_i(A_i\bullet(RR^{T})-b_i)$ , and $S(y)=C-\sum_i y_iA_i$ . A feasible $R$ is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if $A_1R,\dots,A_mR$ are linearly independent; it is a stationary point with multiplier $y$ if $\nabla_RL(R,y)=0$ . The injection of $R\in\mathbb R^{n\times r}$ is $\hat R=[\,R\ \ 0\,]\in\mathbb R^{n\times(r+1)}$ , obtained by appending a zero column.

Formalization targets

Goal: Proposition 2.5

Let $r<n$ and let $R^*$ be a regular local minimum of $(N_r)$ with multiplier $y^*$ , $S^*=S(y^*)$ , $S^*R^*=0$ . If $\hat R$ is a local minimum of $(N_{r+1})$ , then

X^*=R^*(R^*)^{T}\ \text{solves (1)}\quad\text{and}\quad (S^*,y^*)\ \text{solves (3)}.

Milestones

The derivative formulas (9): $\nabla_R(A_i\bullet(RR^T)-b_i)=2A_iR$ , $\nabla_RL(R,y)=2SR$ , and $L''_{RR}(R,y)[D,D]=2S\bullet(DD^T)$ .
Proposition 2.3: at a regular local minimum of $(N_r)$ there is a unique $y^*$ with $S^*R^*=0$ , and $S^*\bullet(DD^T)\ge0$ for every $D$ with $A_iR^*\bullet D=0$ for all $i$ .
Proposition 2.1: feasible $X$ and $(S,y)$ are simultaneously optimal if and only if $X\bullet S=0$ .
Proposition 2.4: a stationary point of $(N_r)$ whose $S^*$ is positive semidefinite gives optimal $X^*=R^*R^{*T}$ and $(S^*,y^*)$ .

Significance

Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of $(N_r)$ for a small $r$ ; if the zero-column extension is still a local minimum of $(N_{r+1})$ , the current point solves the SDP; otherwise a better point of $(N_{r+1})$ exists and $r$ is increased. Proposition 2.4 gives the companion test, valid for every $r$ : positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).

The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.

Difficulty

The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of $(N_r)$ is a variety cut out by $m$ quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of $R^*$ alone does not make $S^*$ positive semidefinite (when $r$ is below the minimal optimal rank, it is not); the hypothesis on $(N_{r+1})$ is indispensable.

Formalization scope

Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over $\mathbb R$ includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about $(N_r)$ carries $0<r$ and $r\le n$ (or $r<n$ ). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of $(N_r)$ together with feasibility. The injection appends the zero column as the last column.

The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained $(N_r)$ (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes $S\succeq0$ , and an injection other than the zero-column extension.

A complete development needs the matrix calculus of $R\mapsto RR^{T}$ , a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.

Selected references

S. Burer and R. D. C. Monteiro, A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization, Mathematical Programming 95 (2003), 329–357. https://doi.org/10.1007/s10107-002-0352-8 (statements cited from the authors' manuscript of March 9, 2001)
A. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13 (1995), 189–202. https://doi.org/10.1007/BF02574037
G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23 (1998), 339–358. https://doi.org/10.1287/moor.23.2.339
R. D. C. Monteiro and M. Todd, Path-following methods for semidefinite programming, in Handbook of Semidefinite Programming, Kluwer, 2000 (source of Proposition 2.1).
S. Burer and R. D. C. Monteiro, Local minima and convergence in low-rank semidefinite programming, Mathematical Programming 103 (2005), 427–444. https://doi.org/10.1007/s10107-004-0564-1
N. Boumal, V. Voroninski and A. S. Bandeira, The non-convex Burer–Monteiro approach works on smooth semidefinite programs, NeurIPS 2016. https://arxiv.org/abs/1606.04970

10 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

On Sequential Decisions and Markov Chains 3: A Deterministic Stationary Procedure Minimizes the Ratio of Two Long-Run Average CostsResearch Paper

Motivation

Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.

The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.

Timeline, as far as it bears on this mission:

1960: Manne, Linear Programming and Sequential Decisions, shows that linear programming applies to the average-cost problem, in the context of an inventory problem; Wagner, On the Optimality of Pure Strategies, shows by linear programming that a deterministic stationary procedure is optimal for it.
1960: Howard, Dynamic Programming and Markov Processes, gives policy iteration for the average-cost problem over stationary procedures.
1962: Derman proves that a deterministic stationary procedure is optimal over all procedures for the average-cost criterion (Theorem 1), formulates the average and total cost problems as linear programs under irreducibility assumptions (Theorem 2), and extends the optimality of deterministic stationary procedures to the ratio criterion (Theorem 3).
1962: Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, gives a problem of the ratio type (cited by Derman, p. 18).
1963: Jewell, Markov-renewal programming, treats the gain rate (reward per unit sojourn time) of semi-Markov decision processes, over stationary policies.

Setting

A system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$ . After each observation one of the decisions $d_1, \dots, d_K$ is made, all of them available in every state. If the system is in state $i$ and decision $d_k$ is made, the next state is $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ .

A procedure $R$ chooses the decision at time $t$ at random, with probabilities $D_k(X_0, \Delta_0, \dots, X_t)$ that may depend on the whole past; the class of all procedures is $C$ . The class $C'$ consists of the stationary randomized procedures, for which the probability of $d_k$ in state $i$ is a fixed number $D_{ik}$ , whatever the past and the time. The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with every $D_{ik} \in \{0, 1\}$ ; it is finite. A procedure of $C'$ turns the states into a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$ .

Let $w'_{ik} > 0$ and $w''_{ik} > 0$ be two sets of costs incurred when decision $d_k$ is made in state $i$ . For a fixed procedure $R$ started at $X_0 = i$ , let $W'_t$ and $W''_t$ be the expected costs at time $t$ . The ratio criterion is

\psi_R(i) = \limsup_{T\to\infty} \frac{\sum_{t=0}^{T} W'_t}{\sum_{t=0}^{T} W''_t}.

For a single cost set $w$ with expected costs $W_t$ , the average cost per unit time is $Q_R(i) = \limsup_{T\to\infty} \frac1T \sum_{t=0}^{T} W_t$ .

Assumption A says that for every procedure of $C'$ all states $0, \dots, L$ belong to the same class of the induced Markov chain.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumption A, for every initial state $i$ there is a deterministic stationary procedure $R_3 \in C''$ with

\psi_{R_3}(i) = \min_{R \in C} \psi_R(i),

that is, $\psi_{R_3}(i) \le \psi_R(i)$ for every procedure $R \in C$ .

Steps of the proof (milestones)

Theorem 1 (1) for costs of either sign: for every real cost $w$ there is $R_1 \in C''$ with $Q_{R_1}(i) \le Q_R(i)$ for all $R \in C$ and all $i$ .
For any procedure $R$ , $\psi_R(i) \le m$ implies $Q_R(i) \le 0$ for the costs $w_{ik} = w'_{ik} - m\, w''_{ik}$ .
Under Assumption A, for $R^* \in C''$ , $Q_{R^*}(i) \le 0$ for those costs implies $\psi_{R^*}(i) \le m$ .
For $R \in C'$ under Assumption A, $\psi_R(i) = \dfrac{\sum_{s}\sum_k \pi_s D_{sk} w'_{sk}}{\sum_s\sum_k \pi_s D_{sk} w''_{sk}}$ , with $\pi$ the stationary distribution of $(p_{sj})$ .

Significance

Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing $w' - m w''$ and adjusting $m$ , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.

All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.

Difficulty

The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages $\frac1T\sum_{t\le T} W'_t$ and $\frac1T\sum_{t \le T} W''_t$ need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.

Formalization scope

The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class $C$ is Policy M, history-dependent and randomized; $C''$ is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs $w'$ , $w''$ and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.

The local definitions are: the expected cost at time $t$ for a real cost, as a finite sum over histories of length $t+1$ ; $Q_R(i)$ with Derman's normalization ( $T+1$ terms divided by $T$ ); $\psi_R(i)$ as the limit superior of the ratio of partial sums; the induced matrix $p_{ij}$ ; Assumption A as Matrix.IsIrreducible of $p$ for every row-stochastic $D \ge 0$ ; and membership of a procedure in $C'$ with probabilities $D$ . All limits superior are real, of bounded sequences; positivity of $w'$ and $w''$ is a hypothesis of every statement involving $\psi$ , which keeps the denominators positive.

The goal quantifies "for every initial state there is $R_3$ ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.

Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class $C''$ .

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
M. Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, Management Science 9(1), 1962.
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 1960.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6):938–948, 1963. https://doi.org/10.1287/opre.11.6.938
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037

7 thms2 active usersReviewed

Convex Optimization Operations Research·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources VII: A Locally Quasiconcave Objective Always Has a Quasistable Optimal ScheduleTextbook

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project that respect precedence-type time lags and the capacities of renewable resources (machines, crews, equipment). Classical project scheduling minimizes the project duration, a regular objective: delaying an activity never helps. Many objectives met in practice are not regular. The resource investment problem minimizes the cost of the resource capacities that must be procured; resource levelling problems minimize fluctuations of resource usage over time; the resource renting problem trades fixed procurement against time-dependent renting costs; net present value and earliness–tardiness objectives reward late as well as early starts. For such objectives the familiar fact that "some active schedule is optimal" fails, and algorithms need another finite set of candidate schedules that is guaranteed to contain an optimum.

Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2), organizes the objective functions of project scheduling into seven classes and pairs each class with a class of schedules that contains an optimal schedule. This mission formalizes §3.3 of that chapter. The classification goes back to Neumann, Nübel and Schwindt (2000) and Zimmermann (2001); the two locally defined classes, and the matching schedule classes of quasiactive and quasistable schedules, are the book's device for covering discontinuous resource-based objectives.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ , $n\ge 1$ , where $0$ and $n+1$ are fictitious activities marking the project beginning and completion. Activity $i$ has an integer duration $p_i$ ( $p_0=p_{n+1}=0$ , $p_i>0$ otherwise). The project network has an arc set $E$ with integer weights $\delta_{ij}$ ; a schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ , $S\ge 0$ , and it is time-feasible if $S_j-S_i\ge\delta_{ij}$ for all $\langle i,j\rangle\in E$ . A maximum project duration $\bar d\in\mathbb N$ is prescribed through a backward arc $\langle n+1,0\rangle$ of weight $-\bar d$ , so $S_{n+1}\le\bar d$ . Each renewable resource $k$ has capacity $R_k$ , activity $i$ uses $r_{ik}$ units while in progress, and $r_k(S,t)$ is the total usage at time $t$ . The feasible region $\mathcal S$ consists of the time-feasible schedules with $r_k(S,t)\le R_k$ for all $k$ and $t$ .

For an objective function $f:\mathbb R^{n+2}_{\ge 0}\to\mathbb R$ , problem $PS|temp,\bar d|f$ asks for an optimal schedule: some $S\in\mathcal S$ with $f(S)\le f(S')$ for all $S'\in\mathcal S$ .

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$ of precedences it realizes. The equal-order set of $S$ is

\mathcal S_T^{=}(O(S))=\{S'\text{ time-feasible}\mid S'_j\ge S'_i+p_i\ \forall (i,j)\in O(S),\ O(S')=O(S)\},

a polytope with part of its boundary removed. The distinct equal-order sets partition $\mathcal S$ into finitely many pieces.

Schedule classes are defined through shifts. A shift from a feasible $S$ to a feasible $S'\ne S$ is order-preserving if $O(S)\subseteq O(S')$ ; it is a left-shift if $S'\le S$ . Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$ . A feasible schedule is active if no feasible left-shift exists, quasiactive if no order-preserving left-shift exists, stable if no pair of opposite shifts to feasible schedules exists, and quasistable if no pair of opposite order-preserving shifts exists.

Objective classes: $f$ is regular if $S\le S'$ implies $f(S)\le f(S')$ ; quasiconcave on a set $M$ if $f(\lambda S+(1-\lambda)S')\ge\min[f(S),f(S')]$ for $S,S'\in M$ , $\lambda\in[0,1]$ ; lower semicontinuous if $f(S)\le\liminf_{S'\to S}f(S')$ on $\mathbb R^{n+2}_{\ge 0}$ . Then $f$ is locally regular (class 6) if it is lower semicontinuous and regular on every equal-order set $\mathcal S_T^{=}(O(S))$ , $S\in\mathcal S$ , and locally quasiconcave (class 7) if it is lower semicontinuous and quasiconcave on every such set.

Formalization targets

Goal: Theorem 3.3.13

For every locally quasiconcave $f$ ,

\mathcal S\ne\emptyset\ \Longrightarrow\ \exists\,S\ \text{quasistable with}\ f(S)=\min_{S'\in\mathcal S}f(S').

Milestones

Class 1 (§3.3.2): every regular $f$ has an active optimal schedule when $\mathcal S\ne\emptyset$ .
Class 5 (§3.3.6): every quasiconcave $f$ has a stable optimal schedule when $\mathcal S\ne\emptyset$ .
Eq. (3.3.11): the equal-order sets form a finite partition of $\mathcal S$ .
Propositions 3.3.5 and 3.3.6: the resource investment objective $\sum_k c_k\max_t r_k(S,t)$ with $c_k\ge 0$ is constant on each equal-order set and lower semicontinuous, hence locally regular.
Theorem 3.3.9: every locally regular $f$ has a quasiactive optimal schedule when $\mathcal S\ne\emptyset$ .

Significance

Quasiactive and quasistable schedules are finite in number: they are the minimal points and the vertices of the finitely many schedule polytopes. Theorem 3.3.13 therefore turns the minimization of any locally quasiconcave objective over a disconnected, non-convex feasible region into a finite search. Class 7 contains the resource levelling objectives $\sum c_k\sum r_{kt}^2$ and $\sum c_k\sum o_{kt}$ , the total variation of the resource profiles, and the resource renting objective (Propositions 3.3.10 and 3.3.12, and Nübel 2001). The enumeration schemes and decision sets of §3.5–3.7 rest on this result, and Theorem 3.3.9 plays the same role for class 6 (resource investment, changeover times).

The results are proved in the book and the cited papers. As far as a search of the platform shows, none of them, and none of the schedule classes, has a machine-checked formalization; Mathlib supplies lower semicontinuity and quasiconcavity but nothing about schedules. The mission produces a checked version of the classification theorems in the book's exact generality: general time lags (cycles in the network allowed), real start times, and arbitrary objectives given only by their class.

Difficulty

The optimum need not exist a priori: objectives of classes 6 and 7 are discontinuous, and the feasible region is a finite union of polytopes that is in general disconnected. Existence of a minimizer needs compactness of $\mathcal S$ (which depends on the deadline arc and the network's path structure) together with lower semicontinuity.

The main obstacle is that the objective is only controlled piecewise. Quasiconcavity holds on each equal-order set separately, and an equal-order set is not closed: a schedule polytope $\mathcal S_T(O(S))$ also contains schedules inducing strictly larger orders, where the hypothesis on $f$ says nothing about its relation to the values on $\mathcal S_T^{=}(O(S))$ . The obvious argument, taking an optimal schedule and invoking quasiconcavity along the segment of a pair of opposite order-preserving shifts, only relates $f$ at points of one equal-order set, and it does not by itself produce a schedule that admits no such pair at all. The same issue arises for Theorem 3.3.9 with order-preserving left-shifts, which may cross from one equal-order set into another.

Formalization scope

Activities are Fin (n + 2), with 0 and Fin.last (n + 1) fictitious. Start times are real; objective functions are total functions (Fin (n + 2) → ℝ) → ℝ whose regularity, quasiconcavity and lower semicontinuity are required only on the nonnegative orthant (lower semicontinuity is Mathlib's LowerSemicontinuousOn on the orthant). The deadline $S_{n+1}\le\bar d$ is the network's backward arc, as in §3.1. The project structure records the book's standing property (p. 8) that from each node $i$ there is a path to $n+1$ of length at least $p_i$ ; this bounds every activity by $\bar d$ . The resource constraints are imposed for all $t\ge 0$ , which under that property is the book's $0\le t\le\bar d$ . The peak $\max_t r_k(S,t)$ in the resource investment objective is a supremum in $\mathbb N$ over $t\ge 0$ of a nonempty finite set, hence attained.

"Optimal" always means minimizing $f$ over the whole feasible region $\mathcal S$ , and the theorems quantify over every function in the class; a formalization with a fixed objective, or with optimality over a single polytope or a single equal-order set, would be a different and weaker statement. The schedule classes are defined through shifts, never as minimal or extreme points, so no statement is true by definition. The only hypothesis besides the class of $f$ is $\mathcal S\ne\emptyset$ .

The mission restates locally the project model, the induced orders and the shift classes also drafted by the companion missions on schedule classes of this series. Useful contributions beyond the milestones: compactness of $\mathcal S$ and closedness of the schedule polytopes, the representation of $\mathcal S$ as a finite union of feasible order polytopes, and the finiteness of the sets of quasiactive and quasistable schedules.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.3. doi:10.1007/978-3-540-24800-2
K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), cited in the book as Neumann et al. (2000).
J. Zimmermann, Ablauforientiertes Projektmanagement: Modelle, Verfahren und Anwendungen, Gabler, 2001.

11 thms2 active usersReviewed

Bandit Algorithms Convex Optimization Machine Learning+1·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems V: Bandit Convex Optimization with One-Point FeedbackTextbook

Motivation

In bandit convex optimization a forecaster repeatedly picks a point $x_t$ of a convex set $\mathcal K\subseteq\mathbb R^d$ , and an adversary picks a convex loss $\ell_t$ . The forecaster pays $\ell_t(x_t)$ and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.

Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an $\mathcal O(n^{3/4})$ regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow $\mathcal O(\sqrt n)$ . Whether one-point feedback admits $\sqrt n$ regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained $\sqrt n$ regret up to logarithmic and polynomial-in- $d$ factors for convex losses, with a different and much more involved algorithm.

Setting

Let $\mathbb B=\{x\in\mathbb R^d:\|x\|\le1\}$ be the closed Euclidean unit ball and $\mathbb S=\{x:\|x\|=1\}$ the unit sphere, with unnormalized spherical measure $\sigma$ , so that $\sigma(\mathbb S)=d\,\mathrm{Vol}(\mathbb B)$ . Fix $\delta>0$ . For a loss $\ell$ , the smoothed loss is $\widetilde\ell(x)=\mathbb E\,\ell(x+\delta B)$ with $B$ uniform on $\mathbb B$ .

The set $\mathcal K$ is closed and convex with $r\mathbb B\subseteq\mathcal K\subseteq R\mathbb B$ . The losses $\ell_1,\ell_2,\dots:\mathbb R^d\to\mathbb R$ are $G$ -Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).

OSGD (Online Stochastic Gradient Descent) on a set $\mathcal K'$ with learning rate $\eta$ starts at $x_1=0$ and sets $x_{t+1}=\operatorname{argmin}_{y\in\mathcal K'}\|y-(x_t-\eta\widetilde g_t(x_t))\|$ , where $\widetilde g_t$ is a gradient estimate. With $S_1,S_2,\dots$ independent and uniform on $\mathbb S$ :

the two-point estimate (6.1) is $\widetilde g_t(x_t)=\frac d{2\delta}\big(\ell_t(X_t^+)-\ell_t(X_t^-)\big)S_t$ with $X_t^\pm=x_t\pm\delta S_t$ ; the played point is $X_t^+$ or $X_t^-$ by a fair coin;
the one-point estimate (6.3) is $\widetilde g_t(x_t)=\frac d\delta\,\ell_t(\widetilde X_t)S_t$ with played point $\widetilde X_t=x_t+\delta S_t$ .

OSGD runs on the shrunken set $\mathcal K'=(1-\delta/r)\mathcal K$ , so that the perturbed points stay in $\mathcal K$ . The pseudo-regret is

\overline R_n=\mathbb E\sum_{t=1}^n\ell_t(\widetilde X_t)-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t(x).

Formalization targets

Goal: Theorem 6.2, tuned

If in addition $|\ell_t|\le L$ on $\mathcal K$ , and $\delta=(2n)^{-1/4}\sqrt{RdL/((3+R/r)G)}$ , $\eta=(2n)^{-3/4}\sqrt{R^3/(dL(3+R/r)G)}$ , then one-point OSGD satisfies

\overline R_n\le 4n^{3/4}\sqrt{RdL\,(3+R/r)\,G}.

Milestones

Lemma 6.1: $\nabla\int_{\mathbb B}\ell(x+\delta b)\,db=\frac1\delta\int_{\mathbb S}\ell(x+\delta s)s\,d\sigma(s)$ .
Lemma 6.2: $\frac d\delta\mathbb E[\ell(x+\delta S)S]=\nabla\mathbb E\,\ell(x+\delta B)$ .
Eq. (6.2): $|\ell(x)-\widetilde\ell(x)|\le\delta G$ .
Lemma 6.3: the queried points' regret against $x$ is at most the smoothed regret of the iterates against $(1-\xi)x$ , plus $3\delta Gn+\xi GRn$ .
Theorem 6.1: two-point OSGD has $\overline R_n\le R^2/\eta+\eta(Gd)^2n+\delta(3+R/r)Gn$ , and $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ .
Theorem 6.2, first display: one-point OSGD has $\overline R_n\le R^2/\eta+\frac{(dL)^2}{\delta^2}\eta n+\delta(3+R/r)Gn$ for every $0<\delta\le r$ and $\eta>0$ .

Significance

The $n^{3/4}$ bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the $\sqrt n$ benchmark for two-point methods.

All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.

Difficulty

Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in $x$ requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate $x_t$ is a function of $S_1,\dots,S_{t-1}$ , and unbiasedness $\mathbb E[\widetilde g_t\mid x_t]=\nabla\widetilde\ell_t(x_t)$ holds only conditionally, via independence of $S_t$ from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of $\ell_t$ fails: it is a gradient of $\widetilde\ell_t$ , and the gap is handled only by Eq. (6.2) and Lemma 6.3.

Formalization scope

Points are in EuclideanSpace ℝ (Fin d) with $d\ge1$ ; rounds are $t=1,2,\dots$ , sums run over Finset.Icc 1 n. $\sigma$ is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions $S_t$ are measurable, mutually independent (iIndepFun) and uniform on $\mathbb S$ , and in Theorem 6.1 the pairs $(S_t,C_t)$ are independent with $C_t$ a fair sign independent of $S_t$ . A run of OSGD is a predicate (start at $0$ , each iterate a Euclidean projection onto $(1-\delta/r)\mathcal K$ ), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of $\mathbb R^d$ ; the bound $|\ell_t|\le L$ is on $\mathcal K$ , because a convex function bounded on $\mathbb R^d$ is constant. The minimum over $\mathcal K$ is an infimum over the subtype $\mathcal K$ , attained in every theorem.

Conventions and corrections, each stated in the item's Formalization Note:

Lemma 6.1 carries the factor $1/\delta$ that the printed statement omits and the proof contains (corrected misprint).
Theorem 6.1's second display prints $\eta=R/(GD\sqrt n)$ and a limit "for $\delta\to0$ "; the item states $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ and every admissible $\delta$ , which implies the limit (corrected misprint).
Theorems 6.1 and 6.2 add $0<\delta\le r$ , which the proofs need for $X_t^\pm,\widetilde X_t\in\mathcal K$ ; for the tuned $\delta$ of the goal it is a condition on $n$ .
The goal adds $G,L>0$ and $n\ge1$ , which its formulas for $\delta,\eta$ need; the constant $4$ is the book's rounding of $2\cdot2^{3/4}$ and is kept, as is the form $R^2/\eta$ .

The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact $\mathcal K$ . Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.

Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
A. Flaxman, A. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. arXiv:cs/0408007
A. Agarwal, O. Dekel, L. Xiao, Optimal algorithms for online convex optimization with multi-point bandit feedback, COLT 2010. link
S. Bubeck, R. Eldan, Y. T. Lee, Kernel-based methods for bandit convex optimization, STOC 2017. arXiv:1607.03084

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Dimensioning Large Call Centers I: The Rationalized Staffing Function Is Asymptotically OptimalResearch Paper

Motivation

A call center with $N$ agents facing Poisson arrivals at rate $\lambda$ and exponential service at rate $\mu$ is the M/M/N (Erlang-C) queue. Choosing $N$ trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule $N \approx R + y\sqrt R$ , where $R = \lambda/\mu$ is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor $y$ that makes the rule asymptotically optimal as the arrival rate grows.

Timeline of the asymptotic regime the paper builds on:

1917. Erlang's delay formula $\pi(N,\nu)$ for the M/M/N queue.
1981. Halfin and Whitt (Oper. Res. 29(3)) show that with $N = R + \beta\sqrt R$ servers the probability of waiting converges to a limit $P(\beta) \in (0,1)$ , the quality-and-efficiency-driven regime.
2000/2004. Borst, Mandelbaum and Reiman classify cost structures into a rationalized, an efficiency-driven and a quality-driven regime, and prove asymptotic optimality of an explicit staffing rule in each.

This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.

Setting

The service rate $\mu > 0$ is fixed and the arrival rate $\lambda$ grows. A staffing cost $F$ , defined on $(0,\infty)$ , is convex and strictly increasing; it does not depend on $\lambda$ . For each $\lambda > 0$ a waiting-cost function $D_\lambda$ satisfies $D_\lambda(0)=0$ , is strictly increasing on $[0,\infty)$ , and makes

G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)\,e^{-(N\mu-\lambda)t}\,dt

finite for every $N > \lambda/\mu$ . With the Erlang-C formula

\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{\big(1-\tfrac{\nu}{N}\big)\sum_{n=0}^{N-1}\frac{\nu^n}{n!}+\frac{\nu^N}{N!}\Big\}^{-1},

the expected total cost of staffing $N > \lambda/\mu$ agents is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$ , and $N^*_\lambda$ is any integer $N > \lambda/\mu$ minimizing it (7).

In normalized units $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ the paper defines $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$ , $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$ , the continuous delay probability $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with

H(M,\alpha) = \Big\{\alpha\int_0^\infty e^{-\alpha t}\,t\,(1+t)^{M-1}\,dt\Big\}^{-1},

and $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$ , minimized at $x^*_\lambda$ (8). A surrogate $C[z;\hat F,\hat\pi,\hat G] = \hat F(z)+\hat\pi(z)\hat G(z)$ approximates it. Rounding is measured by

S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda),\,C(\lceil N_\lambda(x)\rceil,\lambda)\}. \tag{10}

The Halfin–Whitt delay function is $P(x) = \big(1 + x/h(-x)\big)^{-1}$ , with $h = \phi/(1-\Phi)$ the standard normal hazard rate (11). Asymptotic equality $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ as $\lambda\to\infty$ .

Formalization targets

Goal: Theorem 5.1

Assume the rationalized condition (18): for some $\kappa > 0$ , $F_\lambda(\kappa)/G_\lambda(\kappa) \to \gamma \in (0,\infty)$ . Let $y^*_\lambda$ minimize $F_\lambda(y) + P(y)G_\lambda(y)$ over $y>0$ (19). Then

\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.

The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.

Milestones

Lemma C.1: $G_\lambda$ is strictly convex and strictly decreasing on $(0,\infty)$ .
Section 3, p. 12: $H(N,\nu) = \pi(N,\nu)$ at integers $N > \nu > 0$ .
Lemma 3.1, Lemma 3.2, Corollary 3.3: the approximation principle. If the surrogate approximates $C_\lambda$ at both $x^*_\lambda$ and its own minimizer $z^*_\lambda$ , then rounding $N_\lambda(z^*_\lambda)$ is asymptotically optimal.
Eqs. (13)–(14): $F_\lambda$ preserves $\limsup$ -separation of ratios.
Lemma 4.1 (Halfin & Whitt): for bounded $x_\lambda$ , $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$ .

Significance

The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost $c$ per agent, linear waiting cost $a$ per unit time) it gives $N^* \approx R + y^*(a/c)\sqrt R$ , with $y^*(r)$ the minimizer of $y + rP(y)/y$ , a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.

The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension $\pi_\lambda$ , is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.

Difficulty

The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of $C_\lambda$ is available, but unimodality rests on convexity of $\pi_\lambda$ , which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while $\pi_\lambda$ is evaluated at non-integer $N_\lambda(x_\lambda)$ ; a proof needs a uniform Laplace-type asymptotic for the integral defining $H$ . A further obstacle is bounding $x^*_\lambda$ : the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).

Formalization scope

All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on $\mathbb R$ with $\mu$ fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost $C(N,\lambda)$ , and so are these. Committed conventions:

The standing assumptions are a structure WaitModel ( $\mu>0$ ; $D_\lambda(0)=0$ ; $D_\lambda$ strictly increasing on $[0,\infty)$ ; $t\mapsto D_\lambda(t)e^{-\theta t}$ integrable on $(0,\infty)$ for every $\theta>0$ , which is the paper's finiteness of $G$ ). $F$ is convex and strictly increasing on $(0,\infty)$ .
Staffing levels in $C(N,\lambda)$ are natural numbers; $G$ and $H$ take real $N$ .
Argmins ( $N^*_\lambda$ , $x^*_\lambda$ , $z^*_\lambda$ , $y^*_\lambda$ ) are hypotheses that a given function is a minimizer, for every $\lambda>0$ ; ties are allowed and the theorems hold for every choice.
In $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ , where $C$ is undefined.
$\limsup$ and $\liminf$ relations are written with ∃ᶠ/∀ᶠ, not Filter.limsup on $\mathbb R$ .
Added hypothesis. The goal assumes $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$ . The paper asserts this limit on p. 12, but it does not follow from its assumptions (it fails for bounded $D_\lambda$ ); it is equivalent to $D_\lambda$ being unbounded and is what makes the continuous optimum exist.

The hypotheses are met by linear staffing and waiting costs ( $F(N)=cN$ , $D_\lambda(t)=at$ ), for which (18) holds with $\gamma = c\kappa^2/a$ , so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every $\lambda>0$ , and $S_\lambda$ never evaluates $C$ at an unstable level.

Needed infrastructure: Laplace asymptotics for $\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt$ , differentiation under the integral sign for $G$ , and convexity of $\pi_\lambda$ . All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].

Selected references

S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917.

21 thms2 active usersReviewed

Linear Optimization Operations Research·Captain: mikedeng1

A Multicut Algorithm for Two-Stage Stochastic Linear Programs 2: Multicut for Simple Recourse Stops Within J·m2 + 1 IterationsResearch Paper

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.

The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of $Jm_2+1$ iterations quoted below. This mission formalizes that section.

Setting

First-stage data are $c\in\mathbb R^{n_1}$ , $A\in\mathbb R^{m_1\times n_1}$ , $b\in\mathbb R^{m_1}$ , and the first-stage feasible set is $K_1=\{x\mid Ax=b,\ x\ge0\}$ . A deterministic technology matrix $T\in\mathbb R^{m_2\times n_1}$ , with rows $T_i$ , maps $x$ to the tender $\chi=Tx\in\mathbb R^{m_2}$ . Problem (3) of the paper is

\min\ z(x)=cx+\Psi(Tx)\quad\text{s.t. } x\in K_1 .

For each row $i=1,\dots,m_2$ the random vector $\xi_i=(q_i^+,q_i^-,h_i)$ takes $J$ values $\xi_{ij}=(q^+_{ij},q^-_{ij},h_{ij})$ with probabilities $p_{ij}$ . The simple recourse cost (20) of row $i$ is the optimal value of a one-row LP,

\psi_i(\chi_i,\xi_{ij})=\min\{q^+_{ij}y^+ + q^-_{ij}y^- \mid y^+-y^-=h_{ij}-\chi_i,\ y^+,y^-\ge0\},

and by separability (19) the expected recourse function is $\Psi(\chi)=\sum_i\Psi_i(\chi_i)$ with $\Psi_i(\chi_i)=\sum_j p_{ij}\psi_i(\chi_i,\xi_{ij})$ . Write $q_{ij}=q^+_{ij}+q^-_{ij}$ .

The multicut algorithm for simple recourse problems (p. 389) keeps a set $I$ of identified pairs $l=(i,j)$ , initially empty. Step 1 solves the master program (26),

\min\ cx+\sum_{i,j}p_{ij}q^-_{ij}(T_ix)+\sum_{l\in I}u_l\quad\text{s.t. } Ax=b,\ x\ge0,\ u_l\ge e_l-E_lx,\ u_l\ge0\ (l\in I),

with $E_l=p_{ij}q_{ij}T_i$ and $e_l=p_{ij}q_{ij}h_{ij}$ . Step 2 adds to $I$ every pair for which the constraint $0\ge p_{ij}q_{ij}(h_{ij}-T_ix^\nu)$ (27) is violated at the master's solution $x^\nu$ , and returns to Step 1; when no pair is added the algorithm stops.

Formalization targets

Goal: the $Jm_2+1$ bound, with correctness

The paper states (p. 389): "The initial problem (26) involves $m_1$ constraints and $n_1$ variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is $Jm_2+1$ ." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):

\nu\text{-th solve of Step 1 takes place}\ \Longrightarrow\ \nu\le Jm_2+1,

and, when the algorithm stops at $x^\nu$ , $x^\nu\in K_1$ and $cx^\nu+\Psi(Tx^\nu)\le cx+\Psi(Tx)$ for all $x\in K_1$ .

Milestones

(22)–(23): for $q^++q^-\ge0$ the LP (20) attains its minimum $\max\{q^-(\chi-h),q^+(h-\chi)\}$ , so each $\theta_{ij}$ has only two cuts.
(24)–(25): the simple recourse problem is equivalent to the LP (25): same optimal $x$ , and the value of (25) at $x$ with the best slacks is $z(x)$ .
Relaxation and stopping: (26) is a relaxation of (25), and if no unidentified pair violates (27) at an optimum of (26), that optimum (extended by zero slacks) is optimal for (25).
Facets: each $\Psi_i$ is a maximum of $J+1$ affine functions, so $\Psi$ is a maximum of at most $(J+1)^{m_2}$ affine functions.

Significance

The bound is linear in $m_2$ and $J$ , while the L-shaped method may need as many iterations as $\Psi$ has facets, up to $(J+1)^{m_2}$ (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in $m_2J$ , a fact used throughout the later literature on simple and integrated recourse.

The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.

Difficulty

The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of $J$ convex functions, each with one breakpoint, is a maximum of exactly $J+1$ affine functions, which is not a consequence of convexity alone.

Formalization scope

All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs $(i,j)$ by Fin m2 × Fin J. The second-stage value $\psi$ is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by $p_{ij}\ge0$ with $\sum_jp_{ij}=1$ .

Readings pinned down, each recorded in the item statements:

$q_{ij}\ge0$ . The paper never states it, but without it (20) is unbounded below and (25) is not equivalent to (3). It is a field of the model.
$x\ge0$ belongs to (3) and is omitted in the displays of (25) and (26); it is kept in both.
Step 2 ranges over unidentified pairs. The paper writes "for each $i$ and $j$ "; read literally, an identified pair whose $u_l$ already covers it could be re-added forever. The paper's remark that (27) "identifies any constraints in (25) that are not met" fixes the reading. The state of the algorithm is the set of identified pairs; the order of identification, and so the index $t$ , is immaterial.
Stopping rule. It is implicit in the paper: stop when (27) is violated for no pair.
Counting. The paper writes "the maximal number of iterations is $Jm_2+1$ "; we count solves of Step 1, the stopping solve included, which is what its argument counts.
Constant. The objective of (26) omits the constant $-\sum p_{ij}q^-_{ij}h_{ij}$ of (25), as printed.
Facets. " $\Psi_i$ contains $J+1$ facets" is read as "is a maximum of $J+1$ (not necessarily distinct) affine functions".

A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.

Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on $\mathbb R$ . Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.

Selected references

J.R. Birge and F.V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
R.M. Van Slyke and R. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
J.R. Birge and F.V. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

7 thms2 active usersReviewed

Analysis Operations Research·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems I: The Łojasiewicz Inequality at Critical Points of Continuous Subanalytic FunctionsResearch Paper

Motivation

For a real-analytic function $f : U \to \mathbb{R}$ on an open set $U \subseteq \mathbb{R}^n$ and a critical point $a$ (so $\nabla f(a) = 0$ ), the Łojasiewicz gradient inequality says that there is an exponent $\theta \in [0,1)$ such that $|f - f(a)|^{\theta} / \|\nabla f\|$ stays bounded near $a$ . It is the standard tool for proving that bounded gradient trajectories $\dot x = -\nabla f(x)$ have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value $+\infty$ and are not differentiable.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.

Timeline.

1963: Łojasiewicz proves the inequality for real-analytic functions (Une propriété topologique des sous-ensembles analytiques réels), and in 1984 derives convergence of bounded analytic gradient trajectories.
1998: Kurdyka (Ann. Inst. Fourier 48) extends it to $C^1$ functions definable in an o-minimal structure, with a desingularizing function in place of the power.
2006: Bolte, Daniilidis and Lewis prove a nonsmooth Sard theorem (J. Math. Anal. Appl. 321): a subanalytic function continuous on its closed domain is constant on each connected component of its critical set.
2007: The present paper proves the nonsmooth inequality for continuous subanalytic functions (Theorem 3.1) and for lower semicontinuous convex ones (Theorem 3.3).
2007: Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18) extend it to lower semicontinuous functions definable in o-minimal structures (the KL property).

Setting

Write $\mathbb{R}^n$ with its Euclidean norm. A function $f : \mathbb{R}^n \to \mathbb{R} \cup \{+\infty\}$ has domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ .

Subanalytic sets (Definition 2.1). A set $A \subseteq \mathbb{R}^n$ is semianalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ on which $A \cap V = \bigcup_{i=1}^{p}\bigcap_{j=1}^{q}\{x \in V : f_{ij}(x) = 0,\ g_{ij}(x) > 0\}$ with $f_{ij}, g_{ij}$ real-analytic on $V$ . It is subanalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ such that $A \cap V$ is the projection onto $\mathbb{R}^n$ of a bounded semianalytic subset of $\mathbb{R}^n \times \mathbb{R}^m$ , $m \ge 1$ . A function $f$ is subanalytic if its graph $\{(x,\lambda) \in \mathbb{R}^n \times \mathbb{R} : f(x) = \lambda\}$ is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.

Subdifferentials (Definition 2.10). The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y \to x,\, y \ne x} \frac{f(y) - f(x) - \langle x^*, y - x\rangle}{\|y - x\|} \ge 0$ (empty off $\operatorname{dom} f$ ). The limiting subdifferential $\partial f(x)$ is the set of limits of $x^*_k \in \hat\partial f(x_k)$ along $x_k \to x$ with $f(x_k) \to f(x)$ .

Slope and critical points. The nonsmooth slope is $m_f(x) = \inf\{\|x^*\| : x^* \in \partial f(x)\}$ , equal to $+\infty$ when $\partial f(x) = \emptyset$ (equation (4)). The critical set is $\operatorname{crit} f = \{x : 0 \in \partial f(x)\}$ (Definition 2.11).

Formalization targets

Goal: Theorem 3.1

Let $f$ be subanalytic with closed domain and $f|_{\operatorname{dom} f}$ continuous, and let $a \in \operatorname{crit} f$ . Then there is $\theta \in [0,1)$ such that

\frac{|f - f(a)|^{\theta}}{m_f} \ \text{ is bounded around } a,

with the conventions $0^0 = 1$ and $\infty/\infty = 0/0 = 0$ . In division-free form: there are $C$ and a neighbourhood $U$ of $a$ with $|f(x) - f(a)|^{\theta} \le C\|x^*\|$ for all $x \in U$ and $x^* \in \partial f(x)$ . The exponent is existential; the goal fixes no value of $\theta$ or $C$ .

Milestones

Remark 2.12, for $f$ continuous on a closed domain: the graph of $\partial f$ is closed; $\operatorname{crit} f$ is closed; $m_f$ is lower semicontinuous; $\operatorname{crit} f = m_f^{-1}(0)$ .
Proposition 2.13(ii), its clause on the critical set: if $f$ is subanalytic and relatively bounded on its domain, then $\operatorname{crit} f$ is subanalytic.
Equation (6), recalled from the nonsmooth Sard theorem: $f$ is constant on the connected component of $\operatorname{crit} f$ containing $a$ .
The curve selection lemma, recalled from Bierstone–Milman: a boundary point of a subanalytic set is the origin of an analytic arc entering the set.

Significance

The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems $\dot x \in -\partial f(x)$ (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.

Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.

Difficulty

The obvious argument restricts $f$ and $m_f$ to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of $m_f$ ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that $f$ is not smooth: the classical proof differentiates $f$ along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of $f$ on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes $f$ real-valued and $C^1$ , proves a different and much weaker statement.

Formalization scope

Space and values. The space is EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.
Subdifferentials. $\hat\partial f$ and $\partial f$ are the published platform definitions NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to $-\infty$ .
Subanalyticity. It is defined on any finite-dimensional real normed space, so that the same definition covers $\mathbb{R}^n$ , $\mathbb{R}^n \times \mathbb{R}$ and $\mathbb{R}^n \times \mathbb{R}^m$ . Analyticity is AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.
Slope. The slope is valued in $[0,+\infty]$ , with $+\infty$ on points without subgradients.
The inequality. It is the predicate LojIneqAt f a θ: one constant $C$ and one neighbourhood of $a$ , quantified over all limiting subgradients. Under $0^0 = 1$ the value $\theta = 0$ never works at a critical point, as under the paper's conventions.
Not assumed. The goal does not assume lower semicontinuity, real values, global subanalyticity, compactness of the critical set, or $f(a) = 0$ . These are reductions inside the paper's proof. Any formalization that adds them, fixes $\theta$ , or replaces the class of $f$ by semialgebraic or $C^1$ functions trivializes the target.
Infrastructure. A complete proof needs: curve selection; the monotonicity lemma and Puiseux expansions for one-variable globally subanalytic functions; the projection theorem or an equivalent definability argument; the nonsmooth Sard theorem (6); and a chain rule for Fréchet subgradients along analytic curves. Each of these is welcome as a separate contribution, and the subanalytic-geometry results are reusable well beyond this mission.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. https://doi.org/10.1137/050644641
J. Bolte, A. Daniilidis, A. Lewis, A Sard theorem for non-differentiable functions, J. Math. Anal. Appl. 321 (2006) 729–740.
E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007) 556–572. https://doi.org/10.1137/060670080
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, 87–89.
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

12 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

A Multicut Algorithm for Two-Stage Stochastic Linear Programs 1: Worst-Case Bound on Multicut Major IterationsResearch Paper

Motivation

Two-stage stochastic linear programs with recourse are a standard model for planning under uncertainty: a first-stage decision $x$ is taken before a random outcome $\xi$ is observed, and a second-stage (recourse) decision $y$ corrects for it afterwards at a cost. When $\xi$ has finitely many realizations, the problem is a large but structured linear program, and the classical way to solve it is the L-shaped method of Van Slyke and Wets (1969), a Benders-type outer linearization of the expected recourse cost.

Birge and Louveaux (1988) proposed the multicut L-shaped algorithm: instead of one cut on the expected recourse function per iteration, it adds one cut per realization. They compared the two methods by worst-case counts of major iterations (the operations between two returns to the master problem), and showed that the multicut count grows linearly in the number $K$ of realizations, while their bound for the single-cut method grows like $K^{m_2}$ . The multicut idea is now part of every textbook treatment of decomposition for stochastic programming (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 5) and of most production implementations of Benders decomposition.

Setting

The data are a matrix $A\in\mathbb R^{m_1\times n_1}$ , vectors $b$ , $c$ , a fixed recourse matrix $W\in\mathbb R^{m_2\times n_2}$ , and $K$ realizations $k=1,\dots,K$ , each with a cost $q_k\in\mathbb R^{n_2}$ , a right-hand side $h_k\in\mathbb R^{m_2}$ , a technology matrix $T_k\in\mathbb R^{m_2\times n_1}$ and a probability $p_k$ . Row vectors are written without transposes, as in the paper. The second-stage value of realization $k$ is

Q_k(x)=\min\{\,q_k y\mid Wy=h_k-T_kx,\ y\ge 0\,\}\in\mathbb R\cup\{\pm\infty\},

the expected recourse is $\Omega(x)=\sum_k p_kQ_k(x)$ , and the deterministic equivalent (2) minimizes $cx+\Omega(x)$ over $K_1\cap K_2$ , where $K_1=\{x\mid Ax=b,\ x\ge 0\}$ and $K_2$ is the set of $x$ for which every second-stage problem is feasible.

The multicut algorithm keeps feasibility cuts $(D_l,d_l)$ and, for each $k$ , optimality cuts $(E_{l(k)},e_{l(k)})$ . Step 1 solves the master

\min\ cx+\sum_{k}\theta_k\quad\text{s.t. } Ax=b,\ x\ge0,\ D_lx\ge d_l,\ E_{l(k)}x+\theta_k\ge e_{l(k)},

ignoring $\theta_k$ when scenario $k$ has no cut. Step 2 tests feasibility of each scenario at the master solution $x^\nu$ and, at the first infeasible one, adds a feasibility cut $(\sigma T_k,\sigma h_k)$ from the simplex multiplier $\sigma$ of a phase-one LP. Step 3 solves each second-stage problem at $x^\nu$ with simplex multiplier $\pi_k$ ; for every $k$ with $\theta_k<p_k\pi_k(h_k-T_kx^\nu)$ (condition (14)) it adds the optimality cut $(p_k\pi_kT_k,\ p_k\pi_kh_k)$ . If no $k$ satisfies (14) the algorithm stops.

The cut set $\mathcal C_k$ is the finite set of all optimality cuts that Step 3 can produce for scenario $k$ : the cuts of simplex-optimal bases of the scenario- $k$ problem at points of $K_1$ .

Formalization targets

Goal: the iteration bound (17)

The paper states (Theorem, p. 388):

Let b be the slope number of the second stage of (2). Then, the maximum number of iterations for the multicut algorithm is 1 + K(b^{m₂} − 1) (17) while the maximum number of iterations for the L-shaped algorithm is [1 + K(b − 1)]^{m₂} (18) where K is the number of the different realizations of ξ.

The goal is (17) with the number of facets replaced by the number of distinct cuts: if $|\mathcal C_k|\le M$ for every $k$ and $M\ge1$ , then in every run of the algorithm, for every choice of optimal master solutions and optimal bases,

\#\{\text{returns to Step 1 from Step 3}\}\ \le\ 1+K(M-1).

Milestones

The feasibility cuts determine $K_2$ (a point lies in $K_2$ exactly when it satisfies every feasibility cut, §2, p. 385), and each optimality cut is an affine minorant of $p_kQ_k$ touching it where it was generated (the multicut algorithm outer-linearizes each $Q_k$ , p. 387).
Aggregating one cut per scenario gives a valid L-shaped cut, and $z(\text{multi})\ge z(\text{L-shaped})$ (proof of the Proposition, p. 387).
When (14) holds for no $k$ , $x^\nu$ is optimal for (2) (stopping rule, p. 387).
The first return from Step 3 records one cut for each scenario, and every return records at least one cut not recorded before (proof of the Theorem, p. 388).

Significance

The bound explains why the multicut method needs few major iterations: the information sent to the master grows additively over scenarios, while the facets of $\Omega$ are combinations of facets of the $Q_k$ and their number can grow multiplicatively. The paper itself notes the trade-off this creates against master size ( $m_1+K$ rows instead of $m_1+1$ ), which is the basis of later work on partial aggregation of cuts.

The mission produces a formal model of the multicut algorithm as a transition system over all admissible choices, valid-cut lemmas for both cut types with dual feasibility made explicit, the correctness of the stopping rule, and the counting argument. These results are proved on paper but, to our knowledge, no machine-checked version of the multicut L-shaped algorithm or its iteration bound exists. The model is reusable for other results on Benders-type methods for stochastic programs.

Difficulty

The counting argument is short once the right invariants are in place; the difficulty is the invariants. A cut recorded earlier must still be satisfied by the current master solution, while the cut added for a scenario satisfying (14) is violated by it, so the new cut differs from every recorded one. This uses that every recorded cut comes from a basis whose multiplier is dual feasible: a basis that merely attains the optimal value under degeneracy can produce a cut that is not valid. The stopping rule needs strong duality at the final bases and weak duality at all earlier ones, together with extended-real bookkeeping of $Q_k$ on points where a scenario is infeasible.

Formalization scope

The model is the published StochasticProg_Recourse_Instance ( $Q_k$ in EReal, $+\infty$ when infeasible) with simplex bases and multipliers from StochasticProg_LShaped_Bases. Vectors are Fin n → ℝ, scenarios Fin K. A simplex-optimal basis is defined locally: invertible basic submatrix, nonnegative basic solution, and dual-feasible multiplier ( $\pi W\le q_k$ ; for the phase-one LP, $\sigma W\le 0$ and $|\sigma_i|\le 1$ ). The algorithm is an inductive step relation on states (feasibility cuts, per-scenario cut lists, return counter); a run is any finite sequence of steps from the empty state. Master optima are attained optimal solutions, not infima.

Pinned-down readings:

The paper writes the bound with $b^{m_2}$ , from its slope number $b$ , and asserts without derivation that each $Q_k$ has at most $b^{m_2}$ facets. We state the bound for any $M$ bounding the number of distinct cuts of each scenario, which is what the paper's proof counts. The L-shaped bound (18) is not stated.
"Iterations" are returns to Step 1 from Step 3. The final, stopping solve is not counted, consistent with Appendix A (four facets of $\Omega$ , five L-shaped solves; two multicut returns), and Step-2 (feasibility) returns are not counted, as in the paper's bound.
Positive probabilities $p_k>0$ are assumed where $K_2$ or optimality appears (the paper's realizations form the support of $\xi$ ).
A scenario with no optimality cut has $\theta_k$ omitted from the objective and always satisfies (14).

The transition relation allows every choice the paper allows; a relation that fixed, say, a particular basis or a particular master solution would prove a bound for fewer runs, and one that required the cut set to be smaller than the paper's would make the bound easy. Neither is done here.

Contributions welcome: proofs of the milestones, a sorry-free proof of the goal from them, and a worked check that the definitions admit the run of Appendix A.

Selected references

J. R. Birge and F. V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
R. M. Van Slyke and R. J.-B. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4 (1962) 238–252. https://doi.org/10.1007/BF01386316
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

12 thms2 active usersReviewed

Convex Optimization Probability·Captain: mikedeng1

The Entropic Barrier: A Simple and Optimal Universal Self-Concordant Barrier: The Entropic Barrier of a Convex Body in ℝⁿ Is a (1 + εₙ)n-Self-Concordant Barrier with εₙ ≤ 100√(log n / n)Research Paper

Motivation

Interior-point methods minimize a linear function $x\mapsto\langle c,x\rangle$ over a convex set $\mathcal K\subset\mathbb R^n$ by following the minimizers of $\langle c,x\rangle+\frac1t g(x)$ as $t\to\infty$ , where $g$ is a self-concordant barrier for $\mathcal K$ . Each Newton step of such a method shrinks $1/t$ by a factor $1-1/\sqrt\nu$ , where $\nu$ is the self-concordance parameter of $g$ , so $\nu$ controls the iteration count of every interior-point method built on $g$ (Nesterov and Nemirovski 1994; Nesterov 2004).

Timeline:

1994. Nesterov and Nemirovski construct the universal barrier for any convex body and show it is a $\nu$ -self-concordant barrier with $\nu\le Cn$ for a universal constant $C$ . They also show that $\nu\ge n$ is necessary for some bodies (the simplex, the cube).
2014–2015. Hildebrand (Math. Oper. Res. 2014) and Fox (Ann. Mat. Pura Appl. 2015) show that the canonical barrier of a convex cone has parameter equal to the dimension, which gives parameter $n+1$ for convex bodies.
2015. Bubeck and Eldan (arXiv:1412.1587, COLT 2015) show that the Fenchel dual of the log-Laplace transform of the uniform measure on $\mathcal K$ , which they call the entropic barrier, is a $(1+o(1))n$ -self-concordant barrier, with an explicit $o(1)$ term.

Beyond optimization, the entropic barrier is the mirror map that pairs naturally with the exponential-family sampling scheme in bandit linear optimization, which the paper discusses in its §3.1.

Setting

Let $\mathcal K\subset\mathbb R^n$ be a convex body: compact, convex, with non-empty interior $\operatorname{int}(\mathcal K)$ . The log-Laplace transform of $\mathcal K$ is

f(\theta)=\log\left(\int_{x\in\mathcal K}\exp(\langle\theta,x\rangle)\,dx\right),\qquad\theta\in\mathbb R^n,

and the entropic barrier is its Fenchel dual

f^*(x)=\sup_{\theta\in\mathbb R^n}\ \langle\theta,x\rangle-f(\theta),\qquad x\in\operatorname{int}(\mathcal K).

For a function $g:\operatorname{int}(\mathcal K)\to\mathbb R$ write $\nabla g(x)[h]$ , $\nabla^2g(x)[h,h]$ , $\nabla^3g(x)[h,h,h]$ for its directional derivatives. Following Definition 1 of the paper:

$g$ is a barrier for $\mathcal K$ if $g(x)\to+\infty$ as $x\to\partial\mathcal K$ ;
a $C^3$ convex $g$ is self-concordant if $\nabla^3g(x)[h,h,h]\le2(\nabla^2g(x)[h,h])^{3/2}$ for all $x\in\operatorname{int}(\mathcal K)$ , $h\in\mathbb R^n$ ;
it is $\nu$ -self-concordant if moreover $\nabla g(x)[h]\le\sqrt{\nu\cdot\nabla^2g(x)[h,h]}$ for all such $x,h$ .

The proof works with the canonical exponential family $p_\theta$ , the probability measure with density $\exp(\langle\theta,x\rangle-f(\theta))\mathbb 1\{x\in\mathcal K\}$ , its mean $x(\theta)$ , covariance $\Sigma(\theta)$ and third central moment $T(\theta)$ ; with $Y=\langle\theta/\|\theta\|,X\rangle$ for $X\sim p_\theta$ and its density $\rho$ ; and with the section marginal $\lambda(y)=\mathrm{Vol}_{n-1}(\mathcal K\cap\{y\theta/\|\theta\|+\theta^\perp\})/\mathrm{Vol}(\mathcal K)$ .

Formalization targets

Goal: Theorem 1

For every $n\ge80$ and every convex body $\mathcal K\subset\mathbb R^n$ , $f^*$ is a $\nu$ -self-concordant barrier for $\mathcal K$ with

\nu=(1+\varepsilon_n)\,n,\qquad\varepsilon_n=100\sqrt{\frac{\log n}{n}}.

Milestones, in attack order

Lemma 1 (p. 5): strict convexity of $f$ , $f^*$ ; $\nabla f^*:\operatorname{int}(\mathcal K)\to\mathbb R^n$ is a bijection; $\nabla^2f=\Sigma$ , $\nabla^3f=T$ (eqs. (4)–(5)); $\nabla^2f^*(x)=\Sigma(\theta(x))^{-1}$ (eq. (6)).
$f^*$ is a barrier (§4, p. 6).
Lemma 2 (p. 7): $\mathbb EX^3\le2(\mathbb EX^2)^{3/2}$ for a real centered log-concave $X$ ; its consequence $\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^3\le2(\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^2)^{3/2}$ ; $f^*$ is self-concordant (§4, pp. 6–7).
Reduction of (3) (p. 7): $f^*$ satisfies (3) with parameter $\nu$ iff $\langle\Sigma(\theta)\theta,\theta\rangle\le\nu$ for all $\theta$ .
$\lambda$ is $n$ -concave on its support (p. 9) and Lemma 5 (p. 9): $\varphi$ is $n$ -concave iff $(\log\varphi)''\le-\frac1n((\log\varphi)')^2$ .
Lemma 3 (p. 8): $\rho(y+y_0)=\rho(y_0)\zeta(y)e^{-y^2/(2\sigma^2)}$ on $[-M,M]$ , with $\zeta\in[0,1]$ unimodal, $M=\sqrt{7n\log n}/\|\theta\|$ , $\sigma^2=\frac{n}{\|\theta\|^2}\frac{1}{1-\sqrt{7\log(n)/n}}$ ; and its consequence (9): $\mathbb E(|Y-y_0|^2\mid|Y-y_0|\le M)\le\sigma^2$ .
Lemma 4 (p. 8): $(1-2c(\varepsilon)\varepsilon\log^2(1/\varepsilon))\mathrm{Var}(X)\le\int_{x_1}^{x_2}(x-x_0)^2\lambda(x)dx\le\mathbb E(|X-x_0|^2\mid X\in[x_1,x_2])$ for log-concave $X$ .
(7) (p. 7): $\mathrm{Var}(Y)\le\frac{n}{\|\theta\|^2}(1+\varepsilon_n)$ .

Significance

The result. Theorem 1 gives, for every convex body, an explicit barrier whose parameter is $n$ up to a second-order term, against the $Cn$ of the universal barrier, and it is optimal up to that term because $\nu\ge n$ is necessary for some bodies. The barrier is defined by a single formula, its derivatives are moments of an explicit probability measure, and its parameter bound reduces to a variance bound for one-dimensional log-concave marginals. Lemmas 2 and 4 are self-contained facts about log-concave laws on $\mathbb R$ (a sharp third-moment bound and a variance-localization bound) that are usable outside this paper.

Formalizing it. The theorem is proved in the paper; nothing here is formalized elsewhere. The platform has a definition of self-concordance (reused here) and results for given self-concordant functions, but no universal or entropic barrier, no exponential family over a convex body, and no moment bounds for log-concave laws. A complete development produces machine-checked versions of the duality facts of Lemma 1, of the two log-concave lemmas, and of the Brunn–Minkowski consequence for section volumes. Two steps of the paper are sketched rather than proved in full: the end of the proof of Lemma 2 ("We omit further details of this proof", p. 12) and, in Lemma 4, a normalization step that cites a lemma stated for isotropic densities. A formal proof either fills or replaces them.

Difficulty

Self-concordance of $f^*$ reduces to self-concordance of $f$ by a general duality fact, and that reduces to Lemma 2; the difficulty there is the sharp constant $2$ , since generic moment comparisons for log-concave laws give a worse constant. The parameter bound is the hard part. The obvious bound $\langle\Sigma(\theta)\theta,\theta\rangle\le Cn$ follows from standard concentration for log-concave measures, but any argument that loses a constant factor proves only the 1994 result. The $1+o(1)$ requires the one-dimensional marginal of the tilted measure to be compared with a Gaussian of variance $n/\|\theta\|^2$ to within a factor $1+O(\sqrt{\log n/n})$ , using the fact that $\lambda$ is $n$ -concave and not merely log-concave. The paper does this pointwise near the mode (Lemma 3) and controls the tails separately (Lemma 4). The pointwise argument assumes $\rho$ smooth, which holds for smooth bodies, and an approximation argument passes to general convex bodies.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so $n$ is the dimension, not a separate parameter. A convex body is compact, convex, with non-empty interior; a lower-dimensional set is excluded, which rules out a formalization in which the barrier and self-concordance clauses hold vacuously.
$f^*$ is a real supremum. On $\operatorname{int}(\mathcal K)$ it is the true supremum; elsewhere Lean returns a junk value that no statement reads. The barrier property is a limit within $\operatorname{int}(\mathcal K)$ at every frontier point.
Self-concordance (2) is the published ConvexOptimization.IsSelfConcordantOn on interior K, stated by line restrictions with an absolute value. It is equivalent to (2), because $h\mapsto-h$ flips the sign of the third derivative.
The goal states the parameter as the explicit number $\nu=(1+100\sqrt{\log(n)/n})\,n$ . The page says $\varepsilon_n\le100\sqrt{\log(n)/n}$ , and (3) is monotone in $\nu$ , so this is the same claim. An existential $\nu$ is not used.
Corrections and implicit hypotheses:
- Lemma 4 is stated for $0<\varepsilon<1$ . The page says $\varepsilon>0$ , but the statement is false for $\varepsilon\ge1$ and the paper applies it only with $\varepsilon<1$ .
- Lemma 5 assumes $\varphi>0$ , which is implicit in $\zeta=\log\varphi$ .
- The reduction of (3) assumes $\nu\ge0$ .
- Lemma 3 and (9) carry the smoothness of $\rho$ (the paper's own without-loss-of-generality step on p. 7) as a hypothesis, and the theorem's range $n\ge80$ .
Section volumes use Mathlib's unnormalized $(n-1)$ -dimensional Hausdorff measure. The normalization constant cancels in $\rho$ and does not affect $n$ -concavity. $\lambda$ and $\rho$ are fixed pointwise functions, because Lemma 3 evaluates $\rho$ at a maximizer.
Log-concavity on $\mathbb R$ is the published ConvexOptimization.LogConcaveOn on the whole line.
Needed infrastructure that is reusable beyond this mission:
- differentiation under the integral sign for exponential families on compact sets;
- Fenchel duality for smooth strictly convex functions;
- Brunn's concavity theorem for sections of convex bodies;
- moment and tail bounds for log-concave densities on $\mathbb R$ .
Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

S. Bubeck, R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, COLT 2015; arXiv:1412.1587v3. https://arxiv.org/abs/1412.1587
Y. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
R. Hildebrand, Canonical barriers on convex cones, Mathematics of Operations Research 39:841–850, 2014.
D. Fox, A Schwarz lemma for Kähler affine metrics and the canonical potential of a proper convex cone, Annali di Matematica Pura ed Applicata 194:1–42, 2015.
B. Klartag, On convex perturbations with a bounded isotropic constant, Geometric and Functional Analysis 16(6):1274–1290, 2006.
C. Borell, Convex set functions in d-space, Periodica Mathematica Hungarica 6(2):111–136, 1975.

21 thms2 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 3: Fractional Double Greedy on the Multilinear Extension Achieves 1/2 of the OptimumResearch Paper

Motivation

Unconstrained submodular maximization (USM) asks for a subset $S$ of a finite ground set $\mathcal N$ maximizing a nonnegative submodular function $f$ . It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because $f$ is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.

Timeline of the approximation ratio for USM in the value oracle model:

Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) showed that a uniformly random set achieves $1/4$ , local search achieves $1/3$ and $2/5$ , and that no algorithm making polynomially many queries achieves $1/2 + \varepsilon$ for any fixed $\varepsilon > 0$ .
Oveis Gharan and Vondrák (SODA 2011) reached $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) reached $0.42$ .
Buchbinder, Feldman, Naor and Schwartz (FOCS 2012) closed the gap with the double greedy algorithms: a deterministic $1/3$ -approximation and a randomized $1/2$ -approximation, both linear in the number of oracle calls. Their Appendix A gives a third, fractional variant, which is the subject of this mission.

This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.

Setting

Let $\mathcal N$ be a finite ground set with $n$ elements and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ . The function $f$ is submodular if

f(A) + f(B) \ge f(A \cup B) + f(A \cap B) \qquad \text{for all } A, B \subseteq \mathcal N .

Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ and let $OPT$ be a maximizing set.

The multilinear extension of $f$ is the function on vectors $x \in [0,1]^{\mathcal N}$

F(x) = \sum_{S \subseteq \mathcal N} f(S) \prod_{u \in S} x_u \prod_{u \notin S} (1 - x_u) = \mathbb E\bigl[f(R(x))\bigr],

where the random set $R(x)$ contains each element $u$ independently with probability $x_u$ . A set is identified with its characteristic vector, so $F$ agrees with $f$ on $\{0,1\}^{\mathcal N}$ , and $\{u\}$ also denotes the unit vector at $u$ . For vectors, $x \vee y$ and $x \wedge y$ are the coordinate-wise maximum and minimum.

Algorithm 4 (MultilinearUSM). Fix an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and start from $x_0 = \emptyset$ and $y_0 = \mathcal N$ (the vectors $\mathbf 0$ and $\mathbf 1$ ). In iteration $i = 1, \dots, n$ compute

a_i = F(x_{i-1} + \{u_i\}) - F(x_{i-1}), \qquad b_i = F(y_{i-1} - \{u_i\}) - F(y_{i-1}),

set $a_i' = \max\{a_i, 0\}$ , $b_i' = \max\{b_i, 0\}$ , and update

x_i = x_{i-1} + \frac{a_i'}{a_i' + b_i'} \{u_i\}, \qquad y_i = y_{i-1} - \frac{b_i'}{a_i' + b_i'} \{u_i\},

with the convention that the two fractions are $1$ and $0$ when $a_i' = b_i' = 0$ . The output is the random set $R(x_n)$ . Every choice before the output is deterministic; the algorithm queries $F$ at four points per element.

For the analysis, $OPT_i = (OPT \vee x_i) \wedge y_i$ .

Formalization targets

Goal: Theorem A.1, oracle-access clause

For every nonnegative submodular $f$ and every order of the ground set,

x_n = y_n \qquad\text{and}\qquad f(OPT) \le 2\,F(x_n) = 2\,\mathbb E\bigl[f(R(x_n))\bigr].

Milestones, in the order the proof uses them

$a_i + b_i \ge 0$ at every iteration (proof of Lemma A.2; the page cites Lemma II.1).
Endpoints: $OPT_0 = OPT$ with $F(OPT) = f(OPT)$ , and $OPT_n = x_n = y_n$ .
(4) and (5): if $a_i \ge 0$ and $b_i > 0$ , then $F(x_i) - F(x_{i-1}) = a_i^2/(a_i+b_i)$ and $F(y_i) - F(y_{i-1}) = b_i^2/(a_i+b_i)$ .
(6): in the same case, $F(OPT_{i-1}) - F(OPT_i) \le a_i b_i/(a_i + b_i)$ , whether or not $u_i \in OPT$ .
Lemma A.2: for every $1 \le i \le n$ ,

F(OPT_{i-1}) - F(OPT_i) \le \tfrac12\bigl[F(x_i) - F(x_{i-1}) + F(y_i) - F(y_{i-1})\bigr].

Telescoped display: $F(OPT_0) - F(OPT_n) \le \tfrac12[F(x_n) - F(x_0)] + \tfrac12[F(y_n) - F(y_0)] \le \tfrac12(F(x_n) + F(y_n))$ .

Significance

The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor $1/2$ is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.

Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: $F$ is affine in each coordinate, its coordinate increments are antitone in the other coordinates on $[0,1]^{\mathcal N}$ , and $F$ restricted to characteristic vectors is $f$ . These are the standard tools of every continuous-relaxation argument for submodular maximization.

Difficulty

The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies $a_i + b_i \ge 0$ "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of $F$ along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining $F$ . Second, inequality (6) is written out only for $u_i \notin OPT$ , and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that $x_{i-1}(u_i) = 0$ and $y_{i-1}(u_i) = 1$ when it is touched, that $x_i \le OPT_i \le y_i$ , and that every state stays in $[0,1]^{\mathcal N}$ , where the antitonicity applies.

Formalization scope

The ground set is a Fintype $X$ with decidable equality; sets are Finset X; $f$ is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ ; $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT; $F$ is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every $x : X \to \mathbb R$ .
The order $u_1, \dots, u_n$ is a duplicate-free list containing every element; $u_i$ is the entry at index $i-1$ , and $n$ is the list's length. The state after $i$ iterations is obtained by folding one step over the first $i$ entries from $(\mathbf 0, \mathbf 1)$ . Statements hold for every such order.
The footnote's convention $a_i'/(a_i'+b_i') = 1$ , $b_i'/(a_i'+b_i') = 0$ when $a_i' = b_i' = 0$ is an explicit case split; with Lean's $0/0 = 0$ it would otherwise be reversed and the run would no longer end with $x_n = y_n$ .
Corrected slips of the page: lines 3–4 of Algorithm 4 assign $a_i', b_i'$ but define $a_i, b_i$ ; " $f : \mathcal N \to \mathbb R^+$ " means $f : 2^{\mathcal N} \to \mathbb R^+$ ; " $F(x) \triangleq \mathbb E[R(x)]$ " means $\mathbb E[f(R(x))]$ ; "NSM" in Theorem A.1 means USM. The main text's one-line definition of submodularity, read literally, forces monotonicity; the footnote's lattice form is used.
Not formalized: the sampling clause of Theorem A.1 (ratio $(1/2) - o(1)$ without oracle access to $F$ , whose proof the paper refers to Calinescu, Chekuri, Pál and Vondrák) and the running time. The guarantee is stated for the algorithm as printed, so the trivial existence of a $1/2$ -approximation by exhaustive search does not satisfy it. A statement in which $x_n$ is an arbitrary point, or the state any process with $x_i \le y_i$ , would not be this theorem.
Contributions welcome: the multilinear-extension facts above as general lemmas, the run invariants, and proofs of the milestones in any order.

Selected references

N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012, 649–658. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205; its numbering differs and is not used here).
U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, 1133–1153. https://doi.org/10.1137/090779346
S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011, 1098–1117. https://doi.org/10.1137/1.9781611973082.83
M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011, 342–353. https://doi.org/10.1007/978-3-642-22006-7_29
G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6), 2011, 1740–1766. https://doi.org/10.1137/080733991

11 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management III: Gaussian EMSR Protection Levels and Their SensitivityTextbook

Why protection levels and their inputs matter

An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.

This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.

Setting

Let $r$ be the number of requests for a fare class, a real random variable with law $\mu$ . For a seat level $S \in \mathbb R$ the tail probability is

\bar P(S) = P[r \ge S],

and for the fare $f$ of the class the expected marginal seat revenue is $\mathrm{EMSR}(S) = \bar P(S)\cdot f$ (Eqs. (6.1)–(6.2)).

There are two classes: class 1 with fare $f_1$ and class 2 with fare $f_2$ , where $0 < f_2 < f_1$ . Requests for class 1 are Gaussian with estimated mean $\bar r$ and estimated standard deviation $\hat\sigma > 0$ , written $r_1 \sim N(\bar r, \hat\sigma^2)$ . A real number $S$ is an EMSR protection level for class 1 against class 2 when

\bar P_1(S) = P[r_1 \ge S] = \frac{f_2}{f_1} \qquad \text{(Eq. (6.10))}.

The standardized level $Z$ is the value "which has a probability of $f_2/f_1$ of being exceeded" by a standard normal variable:

P[N(0,1) \ge Z] = \frac{f_2}{f_1}.

In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.

Formalization targets

Goal: the Gaussian protection level and its sensitivity to $\hat\sigma$

For $\hat\sigma > 0$ and $0 < f_2 < f_1$ :

Eq. (6.10) has exactly one solution $S$ , and the standard normal equation has exactly one solution $Z$ ;
they satisfy

S = \bar r + Z\hat\sigma \qquad \text{(Eq. (6.12))};

$Z < 0$ if $f_2/f_1 > 1/2$ , $Z > 0$ if $f_2/f_1 < 1/2$ , $Z = 0$ if $f_2/f_1 = 1/2$ (Eq. (6.14)), and $S = \bar r$ in the last case;
if $\hat\sigma' > \hat\sigma$ and $S'$ solves (6.10) for $N(\bar r, \hat\sigma'^2)$ , then $S' < S$ , $S' > S$ or $S' = S$ according as $f_2/f_1$ is above, below or equal to $1/2$ .

The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.

Milestones, in attack order

Eq. (6.1)–(6.2): for any request law, $\bar P$ and $\mathrm{EMSR}$ are non-increasing in $S$ .
Eq. (6.10): the Gaussian protection level exists and is unique.
Eq. (6.11)–(6.12): $S = \bar r + Z\hat\sigma$ .
p. 154: with $\hat\sigma$ and the fares fixed, replacing $\bar r$ by $\bar r + c$ replaces $S$ by $S + c$ .
Eq. (6.14): the sign of $Z$ , and $S = \bar r$ at fare ratio $1/2$ for every $\hat\sigma$ .
p. 154: the effect of $\hat\sigma$ on $S$ (part 4 of the goal on its own).
p. 157: $Z$ and $S$ decrease strictly as the fare ratio $f_2/f_1$ increases.

The dissertation's constant-coefficient-of-variation form, Eq. (6.13), $S = \bar r(1 + Zk)$ with $k = \hat\sigma/\bar r$ , follows from (6.12) by substitution and is not stated separately.

Significance

The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.

All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto $(0,1)$ . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.

Difficulty

Most of the work is in the existence and uniqueness of the two tail solutions. The tail $S \mapsto P[r_1 \ge S]$ must be shown continuous, strictly decreasing, and to take every value in $(0,1)$ . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation $S = \bar r + Z\hat\sigma$ then requires transporting the tail of $N(\bar r,\hat\sigma^2)$ to that of $N(0,1)$ through the affine map $x \mapsto (x - \bar r)/\hat\sigma$ , and the sign of $Z$ requires the symmetry of $N(0,1)$ , namely $P[N(0,1) \ge 0] = 1/2$ . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading $S = \bar r + Z\hat\sigma$ as a definition is ruled out below.

Formalization scope

Continuous seats. Protection levels and $Z$ are real numbers, as in the dissertation's own Gaussian example ( $Z = -0.675$ at fare ratio $0.75$ ). This differs from the first two missions of the series, which count seats in $\mathbb N$ . For a continuous law $P[r \ge S] = P[r > S]$ , so the two definitions of $\bar P$ the dissertation uses (Eq. (5.2) and Eq. (6.2)) coincide here.
Gaussian law. $N(\bar r, \hat\sigma^2)$ is Mathlib's gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes $\hat\sigma > 0$ ; at $\hat\sigma = 0$ the law is a Dirac mass and (6.10) has no solution.
Fares. $0 < f_2 < f_1$ , so $f_2/f_1 \in (0,1)$ . This is the dissertation's " $f_2 < f_1$ " together with positive fares.
Relational sensitivity. The sensitivity statements compare any two solutions of (6.10) under the two input values. Together with uniqueness, this is the same as monotonicity of the solution map. No function is defined by a choice operator.
Tail as a real number. $\bar P(S)$ is the measure of $[S,\infty)$ as a real number. The law is a probability measure, so nothing is truncated.
No trivialization. $S$ is defined only by the tail equation (6.10) for $N(\bar r, \hat\sigma^2)$ , and $Z$ only by the tail equation for $N(0,1)$ . Neither is defined by the formula $S = \bar r + Z\hat\sigma$ , which would make Eq. (6.12) true by definition.
Not covered. The revenue optimality of the level defined by (6.10) belongs to the second mission. The multi-class EMSR rules (5.19)–(5.29) are not optimal for three or more classes and are not stated. The empirical analysis of Sect. 6.1 is out of scope.

Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.

Selected references

P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987. (no DOI; the source PDF of this mission).
P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4:111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

9 thms2 active usersReviewed

Operations Research·Captain: mikedeng1

Sequencing with Earliness and Tardiness Penalties: With Due-Date Tolerances, the Least Optimal Common Due Date Puts One Job at an End of Its Tolerance WindowResearch Paper

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

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$ .
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$ .
Property III(G). A least optimal due date exists, and at it some job completes at $d - u_j$ or at $d + v_j$ .
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).

6 thms2 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time: Delayed SWPT Has Competitive Ratio 2Research Paper

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

$\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
$\pi_E$ is feasible for (E) (§3.2).
Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$ .
Lemma 2. $\pi_E$ is optimal for (E).
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

11 thms2 active usersReviewed

Dynamic Programming Machine Learning Reinforcement Learning·Captain: mikedeng1

Reinforcement Learning: An Introduction III: The Policy Improvement Theorem and Policy IterationTextbook

Why policy improvement matters

Reinforcement learning methods search for good behaviour by alternating two activities: estimating how good the current behaviour is, and changing the behaviour in the direction those estimates suggest. Sutton and Barto call this pattern generalized policy iteration and use it as the organizing idea of their textbook (Sutton & Barto 2018, §4.6). Its mathematical justification is a single result of Chapter 4, the policy improvement theorem (p. 78): a comparison made one step ahead, at each state separately, certifies that a changed policy is at least as good everywhere. Policy iteration, value iteration, Monte Carlo control with ε-greedy policies (Chapter 5), Sarsa and Q-learning are all motivated by it.

The chapter's results go back to the foundations of dynamic programming: the Bellman optimality equation (Bellman 1957), and policy iteration with its finite termination for discounted finite Markov decision processes (Howard 1960). Standard modern treatments are Puterman 1994, Ch. 6, and Bertsekas 2012, Vol. II, Ch. 1.

Setting

A finite Markov decision process has a finite state set $\mathcal S$ , a finite nonempty action set $\mathcal A$ , a finite reward set $\mathcal R\subset\mathbb R$ and dynamics $p(s', r\mid s, a)$ : for each state $s$ and action $a$ , a probability distribution over the next state $s'$ and reward $r$ (Eqs. (3.2)–(3.3)). A policy $\pi$ gives probabilities $\pi(a\mid s)$ of choosing each action in each state; a deterministic policy is a map $\pi:\mathcal S\to\mathcal A$ .

Fix a discount rate $0\le\gamma<1$ . The state-value function of $\pi$ is the expected discounted return

v_\pi(s) = E_\pi\Big[\sum_{k=0}^\infty \gamma^k R_{t+k+1}\ \Big|\ S_t=s\Big],

and the action-value function is defined from it by (4.6):

q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)\,\big[r+\gamma v_\pi(s')\big],

the value of taking $a$ once in $s$ and following $\pi$ afterwards. A policy is optimal if its value is at least that of every policy at every state, and the optimal value function is $v_*(s)=\max_\pi v_\pi(s)$ . A deterministic policy $\pi'$ is greedy with respect to $q_\pi$ if $\pi'(s)\in\operatorname{argmax}_a q_\pi(s,a)$ for all $s$ (4.9).

Formalization targets

Goal: the policy improvement theorem, (4.7)–(4.8), p. 78

For deterministic policies $\pi,\pi'$ ,

\big(\forall s,\ q_\pi(s,\pi'(s))\ge v_\pi(s)\big)\ \Longrightarrow\ \big(\forall s,\ v_{\pi'}(s)\ge v_\pi(s)\big),

and at every state where the hypothesis is strict, the conclusion is strict at that same state.

Milestones

Iterative policy evaluation (4.5), p. 74. From any $v_0$ , the iterates $v_{k+1}(s)=\sum_a\pi(a\mid s)\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_\pi$ .
Greedy improvement (4.9), p. 79. A greedy $\pi'$ with respect to $q_\pi$ satisfies (4.7), hence $v_{\pi'}\ge v_\pi$ .
The stochastic case, p. 79. For stochastic $\pi,\pi'$ , with $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ as in (5.2), the theorem holds as stated, strictness included.
Equality forces optimality, p. 79. If a greedy $\pi'$ has $v_{\pi'}=v_\pi$ , then $v_{\pi'}$ solves the Bellman optimality equation (4.1), $v_{\pi'}=v_*$ , and $\pi$ and $\pi'$ are optimal.
Policy iteration, p. 80. For every sequence of deterministic policies with $\pi_{k+1}$ greedy with respect to $q_{\pi_k}$ : each step is a strict improvement unless $\pi_k$ is optimal, and from some $K$ on every $\pi_k$ is optimal with $v_{\pi_k}=v_*$ .
Value iteration (4.10), p. 83. $v_*$ is attained by one policy at all states, and from any $v_0$ the iterates $v_{k+1}(s)=\max_a\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_*$ .

Significance

The results. The policy improvement theorem turns a local test into a global guarantee: it is enough to check, state by state, that one step of the new policy followed by the old one does no worse than the old one. Combined with the finiteness of the set of deterministic policies, it yields the finite termination of policy iteration and, with the equality case, the existence of a deterministic optimal policy. The stochastic form is what Chapter 5 invokes for ε-greedy control. Value iteration is the other classical way to compute $v_*$ .

Formalizing them. All of these results are classical and proved in the literature cited above; they are not open. The textbook presents them informally ("we chose not to produce a rigorous formal treatment", p. xiii): the improvement theorem is argued by an unbounded chain of expansions, and the policy evaluation and value iteration convergence claims are stated without proof. The mission makes each claim precise with explicit hypotheses and asks for machine-checked proofs against the book's own model with four-argument dynamics and stochastic policies. Related platform results use different models (cost minimization with deterministic policies in Bertsekas's Dynamic Programming; an expected-reward kernel and an assumed fixed point in Foundations of Machine Learning), and none states the policy improvement theorem itself.

Difficulty

The book's proof expands $q_\pi$ with (4.6) and reapplies (4.7) indefinitely, ending with " $\le\cdots=v_{\pi'}(s)$ ". Made rigorous, the chain is an inequality between truncated returns plus a remainder $\gamma^n E_{\pi'}[v_\pi(S_{t+n})]$ , and the passage to the limit needs the remainder to vanish and the truncated returns to converge to $v_{\pi'}$ . Since $v_\pi$ is defined here as a series of expected rewards under the induced Markov chain, connecting it to the one-step quantities requires first establishing the Bellman equation for $v_\pi$ from that series. The strictness part does not follow from the weak inequality alone: strictness at one state must be shown to survive the averaging over later states, which requires tracking the contribution of the first step exactly. The policy iteration statement additionally requires handling ties: a greedy step taken from an optimal policy can move to a different optimal policy, so the sequence need not become constant.

Formalization scope

All objects live in the namespace SuttonBartoRL.DP. States and actions are finite types, actions nonempty where a maximum is taken; one action set serves all states (footnote 3, p. 48). Rewards form a finite set $\mathcal R\subset\mathbb R$ , and the dynamics are a function $p(s',r\mid s,a)$ whose values off $\mathcal R$ are never used. Policies are stochastic; deterministic policies are embedded as policies that choose one action with probability one.

Committed conventions:

Discount $0\le\gamma<1$ throughout. The book also allows $\gamma=1$ when "eventual termination is guaranteed" (p. 74) but never states that hypothesis precisely; the episodic case with a terminal state is out of scope. This is the only restriction relative to the text.
$v_\pi$ from returns. $v_\pi(s)=\sum_k\gamma^k(P_\pi^k r_\pi)(s)$ , with $P_\pi$ the state transition matrix of $\pi$ and $r_\pi$ its expected one-step reward. $q_\pi$ is defined by (4.6), as the book does. The Bellman equation (4.4) is not assumed. Defining $v_\pi$ as the fixed point of a Bellman operator would make the goal an order property of that operator and is excluded.
$v_*$ is the real supremum over all stochastic policies; the value iteration item also asserts it is attained. Optimality of a policy means dominance over all stochastic policies.
Greedy means $\pi'(s)$ is any maximizer of $q_\pi(s,\cdot)$ ; tie-breaking is arbitrary and may differ between iterations.
Stochastic case. The book only says the theorem "carries through as stated"; the meaning $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ is taken from the book's (5.2), p. 101.
Policy iteration is the idealized sequence with exact evaluation. The item does not claim that the boxed pseudocode on p. 80 stops, which it may fail to do under ties (Exercise 4.4, p. 82).
Convergence of iterates is in the product topology on $\mathbb R^{\mathcal S}$ , equivalent to the sup norm for finite $\mathcal S$ .

In-place (asynchronous) sweeps (§4.5) and truncated policy iteration are not formalized.

Needed infrastructure: summability of discounted series of bounded expected rewards, the Bellman equation for $v_\pi$ derived from the return definition, contraction arguments in the sup norm on $\mathbb R^{\mathcal S}$ , and finiteness of the set of deterministic policies. The definitions here duplicate those of the series' Chapter 3 mission and are intended to be merged with them; lemmas about $v_\pi$ , the Bellman equation and contraction are reusable by every later mission of the series, and contributions of such lemmas are welcome.

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 4. http://incompleteideas.net/book/the-book-2nd.html
R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/dynamic-programming-and-markov-processes/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012. http://www.athenasc.com/dpbook.html

9 thms2 active usersReviewed

Bandit Algorithms Machine Learning Reinforcement Learning·Captain: mikedeng1

Reinforcement Learning: An Introduction I: The Gradient Bandit Algorithm Is Stochastic Gradient AscentTextbook

Motivation

The multi-armed bandit is the simplest setting in which a learner must trade off exploiting what it knows against exploring what it does not: one situation, $k$ actions, and a reward drawn from an unknown distribution each time an action is taken. Chapter 2 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses it to introduce, in the smallest possible setting, ideas that run through the rest of the book: incremental estimation with a step size, the bias introduced by the initial estimate, soft-max policies over learned preferences, and learning by following the gradient of expected reward.

The chapter ends with the gradient bandit algorithm (§2.8), which learns a numerical preference for each action instead of a value estimate. A shaded box on pp. 38–40 shows that its expected update is exactly a gradient-ascent step on the expected reward, so the algorithm is an instance of stochastic gradient ascent. The same argument, a score-function (likelihood-ratio) identity with a baseline, reappears in Chapter 13 as the REINFORCE algorithm and the policy gradient theorem. The bandit case is where the book first carries it out in full.

Setting

Actions are $1, \dots, k$ . Each action $x$ has a reward distribution $\nu_x$ on $\mathbb R$ with finite mean $q_*(x)$ , the true action value. At each step the learner holds a vector of action preferences $H = (H(1), \dots, H(k)) \in \mathbb R^k$ and selects action $A$ with the soft-max probability

\pi(a) = \frac{e^{H(a)}}{\sum_{b=1}^k e^{H(b)}} \qquad (2.11).

Given $A = x$ , a reward $R \sim \nu_x$ is received. The expected reward is $\mathbb E[R] = \sum_x \pi(x)\, q_*(x)$ , a smooth function of $H$ . With a step size $\alpha > 0$ and a baseline $B \in \mathbb R$ , the gradient bandit update (2.12) is

H'(A) = H(A) + \alpha (R - B)(1 - \pi(A)), \qquad H'(a) = H(a) - \alpha (R - B)\,\pi(a) \ \ (a \ne A).

The chapter's estimation sections use a single action's rewards $R_1, R_2, \dots$ . The sample average after $n-1$ selections is $Q_n = (R_1 + \cdots + R_{n-1})/(n-1)$ , with an arbitrary initial value $Q_1$ . A constant step size $\alpha \in (0,1]$ updates $Q_{n+1} = Q_n + \alpha [R_n - Q_n]$ (2.5). The trace of one $\bar o_0 = 0$ , $\bar o_n = \bar o_{n-1} + \alpha (1 - \bar o_{n-1})$ defines the step size $\beta_n = \alpha / \bar o_n$ (2.8)–(2.9).

Formalization targets

Goal: the expected update is the gradient step

For every action $a$ , with $A \sim \pi$ and $R \mid A = x \sim \nu_x$ ,

\mathbb E\bigl[H'(a)\bigr] = H(a) + \alpha\, \frac{\partial\, \mathbb E[R]}{\partial H(a)} ,

that is, the update (2.12) equals the exact gradient-ascent step (2.13) in expected value, for every baseline $B$ that does not depend on the selected action.

Milestones

(2.3): $Q_{n+1} = Q_n + \tfrac1n [R_n - Q_n]$ for $n \ge 1$ , including $Q_2 = R_1$ for arbitrary $Q_1$ .
(2.6): $Q_{n+1} = (1-\alpha)^n Q_1 + \sum_{i=1}^n \alpha(1-\alpha)^{n-i} R_i$ , with weights summing to one.
Exercise 2.7: with $\beta_n = \alpha/\bar o_n$ , $Q_{n+1} = \sum_{i=1}^n \frac{\alpha(1-\alpha)^{n-i}}{\bar o_n} R_i$ for $n \ge 1$ , weights summing to one, and no dependence on $Q_1$ .
Shift invariance (p. 37): adding a constant $c$ to every preference leaves $\pi$ unchanged.
Exercise 2.9: for $k = 2$ , $\pi(1) = \sigma(H(1) - H(2))$ with $\sigma(x) = 1/(1+e^{-x})$ .
Soft-max derivative (p. 40): $\partial \pi(x)/\partial H(a) = \pi(x)(\mathbb 1_{a=x} - \pi(a))$ .
Zero-sum gradient (p. 39): $\sum_x \partial \pi(x)/\partial H(a) = 0$ .
Performance gradient as an expectation (p. 39): $\partial \mathbb E[R]/\partial H(a) = \mathbb E[(R - B)(\mathbb 1_{a=A} - \pi(a))]$ .

Significance

The result. The identity makes a model-free algorithm, which uses only the sampled action and reward, an unbiased estimator of the gradient of a quantity that depends on the unknown $q_*$ . It therefore places the gradient bandit algorithm within stochastic approximation, where convergence theory for stochastic gradient methods applies. It also explains the role of the baseline: any baseline independent of the action leaves the expected update unchanged, so the choice of baseline can only affect the variance of the update, as Figure 2.5 shows empirically. The estimation milestones make precise two claims the chapter uses repeatedly: sample averages can be maintained incrementally, and constant step sizes produce an exponentially recency-weighted average biased by $Q_1$ . Exercise 2.7 removes that bias.

Formalizing it. All of these results are elementary and proved (or left as routine exercises) in the book. None of them is formalized on Prove2Me or, as far as is known, in Mathlib. What this mission adds is a machine-checked version of the book's argument with the reward model and baseline condition stated precisely, and a reusable soft-max layer (definition, partial derivatives, shift invariance) for later missions of this series, in particular the policy gradient theorem of Chapter 13.

Difficulty

The mathematics is beginning calculus, as the book says. The formal difficulty lies elsewhere. The goal is an identity between an expectation over a two-stage random experiment (an action from $\pi$ , then a reward from $\nu_A$ ) and a partial derivative in one coordinate of a vector-valued parameter. A proof has to justify exchanging the finite sum with the derivative and splitting the reward integral, and it has to use integrability of each $\nu_x$ . It also needs the fact that the baseline term vanishes because $\sum_x \partial\pi(x)/\partial H(a) = 0$ . A scalar-parameter version of the log-sum-exp derivative does not suffice: the book differentiates in one coordinate $H(a)$ while all other preferences are held fixed. For Exercise 2.7 the obvious unrolling of (2.6) does not apply directly, because the step size $\beta_n$ varies with $n$ and the book states neither the weights nor the range of $\alpha$ .

Formalization scope

Actions are Fin k. Every statement quantifies over some action, so $k \ge 1$ whenever it has content. Preferences are vectors Fin k → ℝ. The partial derivative in coordinate $a$ is the derivative of $h \mapsto f(\text{update } H\ a\ h)$ at $H(a)$ . The soft-max derivative milestone is stated with HasDerivAt, so it also asserts differentiability.
Rewards: each $\nu_x$ is a probability measure on $\mathbb R$ with Integrable identity and mean $q_*(x)$ . The expectation of a function of $(A, R)$ is $\sum_x \pi(x) \int \cdot \, d\nu_x$ . The book's normal-distribution testbed is only an example.
The baseline is a fixed real $B$ , the book's "any scalar that does not depend on" the action (pp. 39–40). The book's $B_t = \bar R_t$ , the average of past rewards, is covered once one conditions on the past. Footnote 1 on p. 37 states that the chapter's experiments used a $\bar R_t$ that also included $R_t$ . That baseline depends on $A_t$ , and the identity does not cover it.
Rewards of one action are a sequence indexed from $1$ . $Q_1$ is arbitrary, and $0^0 = 1$ as in the book (p. 33), so $\alpha = 1$ is included in (2.6).
Exercise 2.7 speaks of "a conventional constant step size $\alpha > 0$ ". The formalization takes $\alpha \in (0,1]$ , the range of the constant step size in (2.5). For $\alpha = 2$ the trace $\bar o_n$ vanishes at every even $n$ and $\beta_n$ is undefined. "Without initial bias" is read as "for $n \ge 1$ , $Q_{n+1}$ is the displayed weighted average of $R_1, \dots, R_n$ with weights summing to one", which in particular does not involve $Q_1$ .
Exercise 2.9 is read as the two equalities $\pi(1) = \sigma(H(1)-H(2))$ and $\pi(2) = \sigma(H(2)-H(1))$ .
A trivializing formalization is ruled out: the goal is about the expected value of the algorithm's update (2.12) under the joint law of action and reward, not the soft-max derivative alone and not a version in which the reward is replaced by its mean or the expectation is taken over $A$ only.
Not formalized: the UCB rule (2.10) and the 10-armed testbed, which carry no provable claim in the chapter, and the stochastic-approximation conditions (2.7), which the book cites without proof.
Welcome contributions: a general soft-max library (derivatives, Jacobian, log-sum-exp) over a finite type, reusable for Chapter 13, and proofs of the milestones in the listed order.

Selected references

R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 2, pp. 25–46. http://incompleteideas.net/book/the-book-2nd.html
R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8 (1992) 229–256. https://doi.org/10.1007/BF00992696
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

11 thms2 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources IX: Deciding Feasibility with Cumulative Resources Is NP-Complete Even for Acyclic Project NetworksTextbook

Motivation

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.

Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.

The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$ ; activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has a duration $p_i\in\mathbb N$ , with $p_0=p_{n+1}=0$ . The project network $N$ has arc set $E$ ; an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ on the start times. A schedule is a real vector $S=(S_i)_{i\in V}$ with $S_0=0$ and $S_i\ge0$ ; it is time-feasible if it meets every temporal constraint.

Cumulative resources $k\in\mathcal R^\gamma$ carry integer demands $r_{ik}$ : $r_{ik}<0$ depletes $-r_{ik}$ units at the start $S_i$ , $r_{ik}>0$ replenishes $r_{ik}$ units at the completion $S_i+p_i$ , and $r_{0k}$ is the initial stock. The inventory at time $t$ is

r_k(S,t)=\sum_{i:\ r_{ik}<0,\ S_i\le t} r_{ik}+\sum_{i:\ r_{ik}>0,\ S_i+p_i\le t} r_{ik}.

With safety stock $\underline R_k$ and storage capacity $\overline R_k$ (integers, $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ by (2.12.1)), $S$ is feasible if it is time-feasible and $\underline R_k\le r_k(S,t)\le\overline R_k$ for every $k$ and every $t\ge0$ . The decision problem of $PSc|temp|C_{\max}$ asks whether a feasible schedule exists.

For renewable resources $k\in\mathcal R$ with capacities $R_k$ and requirements $r_{ik}\in\mathbb N$ , a set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$ . A delaying alternative for $F$ is a set $B\subseteq F$ such that $F\setminus B$ is not forbidden; it is minimal if no proper subset of $B$ is one.

In $PS\infty|temp,\bar d|f$ there are no resources, schedules must also satisfy $S_{n+1}\le\bar d$ , and the objective here is $f(S)=-\sum_{i\in V}\sum_{j>i}w_{ij}|S_j-S_i|$ with weights $w_{ij}\ge0$ .

NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.

Formalization targets

Goal: Theorem 2.12.1

Assuming PARTITION is NP-complete,

L=\{\text{codes of instances of }PSc|temp|C_{\max}\text{ with a feasible schedule}\}\ \text{ and }\ L_{\mathrm{acyc}}=L\cap\{N\text{ acyclic}\}

are both NP-complete.

Milestones

Membership (proof of Theorem 2.12.1): $L\in\mathrm{NP}$ and $L_{\mathrm{acyc}}\in\mathrm{NP}$ .
Reduction correctness (proof of Theorem 2.12.1): for sizes $s(1),\dots,s(\nu)$ with even sum, the project with $r_0=r_{n+1}=-\sum s(i)/2$ , $r_i=s(i)$ , $\underline R=\overline R=0$ , $d^{\min}_{0,n+1}=1$ has an acyclic network, and it has a feasible schedule iff the sizes split into two parts of equal sum.
Polynomial transformation: $\mathrm{PARTITION}\le_p L_{\mathrm{acyc}}$ .
Proof of Proposition 2.5.4, one resource: for $j^*\in B\subseteq F$ , $B$ is a minimal delaying alternative iff $R-\min_{j\in B}r_j<\sum_{i\in F\setminus B}r_i\le R$ .
Proof of Proposition 2.5.4, with $r_{j^*}=1$ : a minimal delaying alternative contains $j^*$ iff some $A\subseteq F\setminus\{j^*\}$ has $\sum_{i\in A}r_i=R$ .
Proposition 2.5.4: assuming SUBSET SUM is NP-complete, deciding whether some minimal delaying alternative for a forbidden set $F$ contains $j^*\in F$ is NP-complete.
Proof of Proposition 3.4.2: a graph has a cut of at least $M$ edges iff the constructed instance has a schedule with $S_i\in\{0,1\}$ and $\sum_{i<j}w_{ij}|S_j-S_i|\ge M$ .
Proposition 3.4.2: assuming SIMPLE MAX CUT is NP-complete, the decision version of $PS\infty|temp,\bar d|-\sum\sum w_{ij}|S_j-S_i|$ is NP-hard.

The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along $\le_p$ (on the platform as CookPvsNP.npComplete_of_polyReducible).

Significance

The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.

Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.

Difficulty

The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.

First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.

Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.

Formalization scope

The Lean development fixes the following conventions.

Activities are Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.
The inventory constraints hold for every $t\ge0$ , not only for $0\le t\le\bar d$ as (2.12.2) is printed; the book's proofs use this reading.
Real activities may have duration $0$ in $PSc|temp|C_{\max}$ : the reduction of Theorem 2.12.1 uses only such activities.
Instances are coded as lists of integers written in binary over the alphabet $\{0,1,-,\#\}$ ; arc weights are listed for every ordered pair of activities together with an arc indicator. Well-formedness (standing assumptions such as $n\ge1$ , $p_0=p_{n+1}=0$ , no loops, (2.12.1), $r_{ik}\le R_k$ ) is part of each language.
"Acyclic" means the nodes admit a numbering increasing along every arc.
The NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT (Karp, 1972) enters as a hypothesis of the corresponding theorem; these are not results of the book.
Proposition 3.4.2 is stated for the decision version of the optimization problem, with natural-number weights and threshold.

A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.

A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of $\le_p$ , and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. doi:10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16, 1988.
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. doi:10.1007/978-1-4684-2001-2_9
S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. claymath.org

14 thms2 active usersReviewed

Combinatorics Operations Research·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources V: A Schedule Is Inventory-Feasible iff It Resolves Every Minimal Surplus and Shortage SetTextbook

Motivation

In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.

A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem $PSc|temp|C_{\max}$ .

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ with $n\ge 1$ , where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i\ge 0$ , with $p_0=p_{n+1}=0$ and $p_i>0$ for the real activities.

For each cumulative resource $k$ in a set $\mathcal R^\gamma$ , every activity $i$ has an integer demand $r_{ik}$ . If $r_{ik}<0$ , activity $i$ withdraws $-r_{ik}$ units of $k$ at its start; if $r_{ik}>0$ , it deposits $r_{ik}$ units at its completion; $r_{ik}=0$ means $k$ is not used. The demand $r_{0k}$ of the project beginning is the initial stock. Write $V_k^-=\{i\mid r_{ik}<0\}$ and $V_k^+=\{i\mid r_{ik}>0\}$ . Each resource has a safety stock $\underline R_k\in\mathbb Z$ and a storage capacity $\overline R_k\in\mathbb Z$ .

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge 0$ . The active set and the inventory of $k$ at time $t\ge 0$ are

\mathcal A_k(S,t)=\{i\in V_k^-\mid S_i\le t\}\cup\{i\in V_k^+\mid S_i+p_i\le t\},\qquad r_k(S,t)=\sum_{i\in\mathcal A_k(S,t)} r_{ik}.

The schedule is inventory-feasible if $\underline R_k\le r_k(S,t)\le\overline R_k$ for all $k$ and all $t\ge 0$ .

Two standing assumptions of the section are used throughout: (2.12.1) $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ , so the final inventory is admissible; and Remark 2.12.2, $\underline R_k\le 0\le\overline R_k$ .

A nonempty $F\subseteq V$ is a $k$ -surplus set if $\sum_{i\in F}r_{ik}>\overline R_k$ , and a $k$ -shortage set if $\sum_{i\in F}r_{ik}<\underline R_k$ . A $k$ -surplus set $F$ is minimal if no $k$ -surplus set arises from $F$ by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal $k$ -shortage sets are defined with the roles of replenishing and depleting activities exchanged. $\mathcal F_k^+$ and $\mathcal F_k^-$ denote the minimal $k$ -surplus and $k$ -shortage sets.

Formalization targets

Goal: Theorem 2.12.4

A schedule $S$ is inventory-feasible if and only if

\forall k,\ \forall F\in\mathcal F_k^+\ \exists j\in F,\ i\notin F:\ r_{jk}>0,\ r_{ik}<0,\ S_j+p_j\ge S_i,

\forall k,\ \forall F\in\mathcal F_k^-\ \exists j\in F,\ i\notin F:\ r_{jk}<0,\ r_{ik}>0,\ S_j\ge S_i+p_i.

Milestones

The invariance claim after Remark 2.12.2 (p. 131): adding the same integer $a_k$ to $r_{0k}$ , $\underline R_k$ and $\overline R_k$ does not change the set of inventory-feasible schedules.
Lemma 2.12.3 (a): for every $k$ -surplus set $F$ there is a minimal $k$ -surplus set $F'$ with $\emptyset\ne F'\cap V_k^+\subseteq F\cap V_k^+$ and $F'\cap V_k^-\supseteq F\cap V_k^-$ .
Lemma 2.12.3 (b): the shortage counterpart.
Theorem 2.12.4 (a) on its own: the upper constraints $r_k(S,t)\le\overline R_k$ hold for all $t\ge 0$ iff condition (a) holds.
Theorem 2.12.4 (b) on its own: the lower constraints hold for all $t\ge 0$ iff condition (b) holds.

Significance

The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation $S_j+p_j\ge S_i$ (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation $S_j\ge S_i+p_i$ . Consequences stated in the book: the feasible region of $PSc|temp|C_{\max}$ is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.

The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.

Difficulty

The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family $\mathcal F_k^+$ and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at $t$ , so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock $r_{0k}$ is handled by the same active-set rule as any other demand, which matters for the invariance claim.

Formalization scope

Activities are Fin (n + 2), activity $n+1$ is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.
The inventory constraints are required for every $t\ge 0$ . The book prints (2.12.2) for $0\le t\le\bar d$ , but its proof of Theorem 2.12.4 works with an arbitrary $t\ge 0$ (the necessity half uses the last completion time of a replenishing activity, which need not be at most $\bar d$ ). The two readings coincide for schedules with $S_{n+1}\le\bar d$ whose activities all finish by $S_{n+1}$ .
A schedule satisfies $S_0=0$ and $S_i\ge 0$ and is not required to be time-feasible; time lags play no role in this section's results and are not part of the model.
(2.12.1) and Remark 2.12.2 are explicit hypotheses (TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.
A formalization in which $\mathcal F_k^+$ is empty or trivial (for instance, minimality with non-strict inclusions, which no set satisfies) makes condition (a) vacuous; the definitions here follow p. 131 exactly, and a concrete instance with a nonempty $\mathcal F_k^+$ has been checked locally.

Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of $PSc|temp|C_{\max}$ (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.12.1, pp. 128–135. https://doi.org/10.1007/978-3-540-24800-2
K. Neumann, C. Schwindt, Project scheduling with inventory constraints, Mathematical Methods of Operations Research 56 (2003) 513–533 (cited in the book as 2002). https://doi.org/10.1007/s001860200251

7 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Linear Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming XI: The KKT Conditions and the Unique Smallest Enclosing BallTextbook

Motivation

The smallest enclosing ball problem asks, for finitely many points $p_1,\dots,p_n\in\mathbb{R}^d$ , for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.

This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.

Setting

A function $f:\mathbb{R}^n\to\mathbb{R}$ is convex if $f((1-t)x+ty)\le(1-t)f(x)+tf(y)$ for all $x,y\in\mathbb{R}^n$ and $t\in[0,1]$ . A convex program in equational form is

\text{minimize } f(x)\quad\text{subject to } Ax=b,\ x\ge 0,

with $A$ a real $m\times n$ matrix with columns $a_1,\dots,a_n$ , $b\in\mathbb{R}^m$ and $f$ convex. A vector $x$ is feasible if $Ax=b$ and $x\ge 0$ componentwise, and optimal if it is feasible and $f(x)\le f(x')$ for every feasible $x'$ . For differentiable $f$ , $\nabla f(x)$ is the row vector of partial derivatives, so $\nabla f(x^*)(x-x^*)$ is a scalar.

For points $p_1,\dots,p_n\in\mathbb{R}^d$ , write $P=\{p_1,\dots,p_n\}$ and let $Q$ be the $d\times n$ matrix whose $j$ th column is $p_j$ . The program studied is

\text{(8.15)}\qquad \text{minimize } f(x)=x^TQ^TQx-\sum_{j=1}^n x_j\,p_j^Tp_j\quad\text{subject to } \sum_{j=1}^n x_j=1,\ x\ge 0 .

A ball is a closed Euclidean ball $B(c,r)=\{z\in\mathbb{R}^d:\|z-c\|\le r\}$ . The ball $B(c,r)$ is the unique smallest enclosing ball of a set $S$ if $r\ge 0$ , $S\subseteq B(c,r)$ , every ball containing $S$ has radius at least $r$ , and every ball containing $S$ of radius at most $r$ has center $c$ .

Formalization targets

Goal: Theorem 8.7.4

For $n\ge 1$ points $p_1,\dots,p_n\in\mathbb{R}^d$ , the objective $f$ of (8.15) is convex, and

(8.15) has an optimal solution $x^*$ ;
there is a point $p^*$ with $p^*=Qx^*$ for every optimal $x^*$ , and for every optimal $x^*$

-f(x^*)\ge 0\quad\text{and}\quad B\big(p^*,\sqrt{-f(x^*)}\big)\ \text{is the unique smallest enclosing ball of } P .

Milestones

Fact 8.7.1. For $C\subseteq\mathbb{R}^n$ convex, $f$ differentiable and convex, and $x^*\in C$ : $x^*$ minimizes $f$ over $C$ iff $\nabla f(x^*)(x-x^*)\ge 0$ for all $x\in C$ .
Proposition 8.7.2 (KKT conditions). For $f$ convex with continuous partial derivatives and $x^*$ feasible: $x^*$ is optimal iff there is $\tilde y\in\mathbb{R}^m$ with

\nabla f(x^*)_j+\tilde y^Ta_j\ \begin{cases}=0&\text{if } x^*_j>0,\\ \ge 0&\text{otherwise,}\end{cases}\qquad j=1,\dots,n.

Lemma 8.7.3. If $s_1,\dots,s_k$ lie on the boundary of the ball $B$ with center $s^*$ , then $B$ is the unique smallest enclosing ball of $\{s_1,\dots,s_k\}$ iff for every $u\in\mathbb{R}^d$ some $j$ has $u^T(s_j-s^*)\le 0$ .

Significance

The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination $Qx^*$ of the input points, the squared radius is the negated optimum value, and the points $p_j$ with $x^*_j>0$ lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.

Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in $\mathbb{R}^n$ ; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.

Difficulty

Existence of an optimum and convexity of $f$ are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by $x\ge 0$ . For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to $p^*$ — and uniqueness of the ball does not follow from uniqueness of the optimizer $x^*$ , which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal $x^*$ and asserts that they all yield the same center.

Formalization scope

Vectors of $\mathbb{R}^n$ are Fin n → ℝ, so the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Points of $\mathbb{R}^d$ are EuclideanSpace ℝ (Fin d), so $\|\cdot\|$ and $p^Tq$ are Euclidean. The matrix $Q$ is Matrix (Fin d) (Fin n) ℝ.
Optimality is stated against every feasible point; no infimum or supremum is taken. $\nabla f(x^*)(x-x^*)$ is the Fréchet derivative applied to $x-x^*$ , and $\nabla f(x^*)_j$ its value on the $j$ th unit vector. "Continuous partial derivatives" is ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.
Balls are closed. The squared radius $-f(x^*)$ is expressed by asserting $-f(x^*)\ge 0$ and taking the radius $\sqrt{-f(x^*)}$ . "Unique ball of smallest radius" is written out as minimality of the radius among all enclosing closed balls plus equality of centers for every enclosing ball of radius at most the optimum; merely stating that the ball encloses $P$ would not be the theorem.
The goal assumes $n\ge 1$ (for $n=0$ the feasible set is empty). In Fact 8.7.1 the minimizer $x^*$ is assumed to lie in $C$ , as "minimizes $f$ over $C$ " presupposes. In Lemma 8.7.3 the radius is nonnegative and each $s_j$ is at distance exactly $r$ from $s^*$ .
Needed infrastructure: gradients of quadratic forms on Fin n → ℝ, LP duality for the pair (maximize $c^Tx$ , $Ax=b$ , $x\ge0$ ) / (minimize $b^Ty$ , $A^Ty\ge c$ ), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.7, pp. 184–191. https://doi.org/10.1007/978-3-540-30717-4
S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
N. Megiddo, Linear-time algorithms for linear programming in $\mathbb{R}^3$ and related problems, SIAM J. Comput. 12(4), 1983. https://doi.org/10.1137/0212052
E. Welzl, Smallest enclosing disks (balls and ellipsoids), in New Results and New Trends in Computer Science, LNCS 555, Springer, 1991. https://doi.org/10.1007/BFb0038202
J. J. Sylvester, A question in the geometry of situation, Quarterly Journal of Pure and Applied Mathematics 1, 1857.

6 thms2 active usersReviewed

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Understanding and Using Linear Programming III: The Simplex Method with Bland's Rule Never CyclesTextbook

Motivation

The simplex method, introduced by G. B. Dantzig in 1947, is the standard algorithm for linear programming and remains the core of commercial solvers. It moves from one basic feasible solution to another by pivot steps, and at each step a pivot rule chooses which variable enters and which leaves the basis. For several natural rules, including Dantzig's original largest-coefficient rule, the method can cycle: on a degenerate linear program it can return to a basis it has already visited and repeat forever without improving the objective. Hoffman (1953) and Beale (1955) gave cycling examples.

R. G. Bland (New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2), 1977) showed that a simple combinatorial rule, choosing the smallest eligible index for both the entering and the leaving variable, never cycles. This makes the simplex method a finite algorithm on every linear program in equational form, and it gives an algorithmic proof of the duality theorem. Chapter 5 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), develops the general theory of simplex tableaus and proves Bland's theorem as Theorem 5.8.1. This mission is the third of a series formalizing that book.

Setting

A linear program in equational form is

\text{maximize } c^{T}x \quad\text{subject to}\quad Ax=b,\ x\ge 0,

with $A$ a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ . Following §4.2 of the book, $A$ has $n\ge m$ columns and rank $m$ . For an $m$ -element set $B=\{k_1<\dots<k_m\}\subseteq\{1,\dots,n\}$ let $N=\{\ell_1<\dots<\ell_{n-m}\}$ be its complement, and $A_B$ , $A_N$ the matrices of the columns of $A$ indexed by $B$ and $N$ . $B$ is a feasible basis if $A_B$ is nonsingular and $A_B^{-1}b\ge0$ ; its basic feasible solution is the unique $x$ with $Ax=b$ and $x_j=0$ for $j\notin B$ .

A simplex tableau $T(B)$ is a system

x_B=p+Q\,x_N,\qquad z=z_0+r^{T}x_N

in the variables $x_1,\dots,x_n,z$ with the same solutions as $Ax=b$ , $z=c^Tx$ . A nonbasic variable $x_v$ , $v=\ell_\beta$ , may enter if $r_\beta>0$ ; a basic variable $x_u$ , $u=k_\alpha$ , may then leave if

q_{\alpha\beta}<0\quad\text{and}\quad-\frac{p_\alpha}{q_{\alpha\beta}}=\min\Bigl\{-\frac{p_i}{q_{i\beta}}: q_{i\beta}<0\Bigr\}.\tag{5.3}

The pivot step replaces $B$ by $B'=(B\setminus\{u\})\cup\{v\}$ . Bland's rule takes the entering variable of smallest index among those with $r_\beta>0$ , and the leaving variable of smallest index among those satisfying (5.3).

Formalization targets

Goal: Theorem 5.8.1 (p. 73)

There is no infinite sequence of bases

B_0\to B_1\to B_2\to\cdots

in which each $B_{t+1}$ is obtained from the feasible basis $B_t$ by a pivot step obeying Bland's rule. Since there are finitely many bases and a Bland step is determined by its starting basis, this is the book's "always finite; i.e., cycling is impossible".

Milestones

Lemma 5.5.1 (p. 66): a feasible basis has exactly one simplex tableau, with $Q=-A_B^{-1}A_N$ , $p=A_B^{-1}b$ , $z_0=c_B^TA_B^{-1}b$ , $r=c_N-(c_B^TA_B^{-1}A_N)^T$ .
Optimality criterion (§5.6, p. 67): if $r\le0$ , the basic feasible solution of $B$ is optimal.
Lemma 5.6.1 (p. 68): a pivot step leads to a feasible basis; if no leaving variable exists, the program is unbounded along an explicit ray.
Claim in the proof of Theorem 5.8.1 (p. 73): for any pivot rule, all bases of a cycle have the same basic feasible solution, and every variable that enters during the cycle is $0$ in it.

Significance

With the optimality criterion and Lemma 5.6.1, Theorem 5.8.1 turns the simplex method into an algorithm: started from any feasible basis, it stops after finitely many pivot steps at an optimal basic feasible solution or with a ray certifying unboundedness. Combined with the auxiliary program of §5.6 for finding a first feasible basis, this yields a constructive proof that every feasible, bounded linear program has an optimal basic feasible solution, and the book remarks that the duality theorem follows easily. Bland's rule is also the model for later combinatorial anticycling rules in oriented matroid programming.

The theorem is classical and fully proved in the book. What the mission adds is a machine-checked version stated in the book's own tableau notation. On Prove2Me the simplex method is formalized in the Bertsimas–Tsitsiklis series (Introduction to Linear Optimization IV), for minimization with reduced costs, with termination proved under nondegeneracy and for the lexicographic rule; Bland's rule is not formalized there.

Difficulty

The obvious termination argument is that the objective value strictly increases at each step, so no basis repeats. That argument fails exactly at degenerate pivot steps, where the minimum in (5.3) is $0$ : the basis changes, the basic feasible solution and the objective value do not. Along a degenerate stretch the objective gives no progress measure, and for general pivot rules the method does cycle there. Any proof must therefore use the specific tie-breaking of Bland's rule, which is a statement about indices, not about values, and relate the tableaus of two different bases in the cycle to each other. Counting bases or tracking the objective value alone does not suffice.

Formalization scope

Vectors are Fin n → ℝ and the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Bases are Finset (Fin n); the sorted enumerations $k_1<\dots<k_m$ and $\ell_1<\dots<\ell_{n-m}$ are Finset.orderEmbOfFin, tableau rows are indexed by Fin m and nonbasic columns by Fin (n - m). Nonsingularity of $A_B$ is IsUnit A_B.det, so the Mathlib inverse is the true inverse wherever it appears. The tableau parameters used by the pivot rules are the explicit formulas of Lemma 5.5.1; the tableau itself is also defined as in the book (same solution set) so that Lemma 5.5.1 is a genuine statement. "Smallest index" compares variable indices, not row positions. Optimality and unboundedness are stated against feasible points, not through a supremum. Every theorem assumes $n\ge m$ and $\operatorname{rank}A=m$ , the standing assumption of §4.2.

A formalization in which any improving variable may enter proves a different, false statement, since cycling examples exist for such rules; the step relation here fixes both choices by Bland's rule. The step relation is not empty: it holds whenever the current tableau has a positive last-row coefficient and a negative entry in the entering column, so the goal is not vacuous.

The development needs basic linear algebra over Matrix, the uniqueness of basic feasible solutions, and bookkeeping for sorted index enumerations. Lemma 5.5.1 and Lemma 5.6.1 are reusable for any later formalization of the simplex method in this notation. Contributions are welcome for each milestone, for the cycle-form corollary, and for a sorry-free proof of the goal.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 5. https://doi.org/10.1007/978-3-540-30717-4
R. G. Bland, New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2):103–107, 1977. https://doi.org/10.1287/moor.2.2.103
E. M. L. Beale, Cycling in the dual simplex algorithm, Naval Research Logistics Quarterly 2(4):269–275, 1955. https://doi.org/10.1002/nav.3800020407
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 3.

7 thms2 active usersReviewed

Convex Optimization Operations Research Probability·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization IV: Nonstationary Optimization and a Convergence Criterion for Nonmonotone SequencesTextbook

Motivation

Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective $f^0$ directly: $f^0$ may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces $f^0$ by a sequence of "good" approximations $F^0(\cdot, s)$ (smoothed versions, sample averages, perturbations) that converge to $f^0$ , and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective $F^0(\cdot, s)$ and the feasible set $X_s$ change with the iteration number $s$ , and the iterates $x^s$ are required to follow the time path of the optimal solutions,

\lim_{s\to\infty}\bigl[F^0(x^s, s) - \min\{F^0(x, s) \mid x \in X_s\}\bigr] = 0 .

Such procedures are essentially nonmonotone: a step on $F^0(\cdot, s)$ gives no guarantee of decrease of $F^0(\cdot, t)$ for $t \ge s+1$ , nor of $f^0$ . Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).

Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which $F^0(\cdot, s)$ and $X_s$ both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.

Setting

Throughout, points are vectors of $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$ .

The projection onto a nonempty closed convex set $X \subseteq \mathbb R^n$ is $\pi_X(y) = \arg\min\{\|y - x\|^2 : x \in X\}$ , the unique nearest point of $X$ to $y$ .
A subgradient of a convex function $F : \mathbb R^n \to \mathbb R$ at $x$ is a vector $g$ with $F(y) \ge F(x) + \langle g, y - x\rangle$ for all $y$ . The book writes $F^0_x(x, s)$ for a subgradient of $F^0(\cdot, s)$ at $x$ .
The nonstationary projected subgradient method (6.41) starts from any $x^0 \in \mathbb R^n$ and sets

x^{s+1} = \pi_X\bigl[x^s - \rho_s g_s\bigr], \qquad g_s \text{ a subgradient of } F^0(\cdot, s) \text{ at } x^s,\quad s = 0, 1, \dots

with step sizes $\rho_s \ge 0$ .

For a closed set $X^*$ (in the application, the set of minimizers of $f^0$ on $X$ ) and a sequence $(x^s)$ , the exit time from the $\varepsilon$ -ball around $x^{s_k}$ is $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ .
The Lyapunov function of the proof is $V(x) = \min_{x^* \in X^*}\|x^* - x\|^2$ , the squared distance to $X^*$ .

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Let $F^0(\cdot, s)$ and $f^0$ be convex continuous on $\mathbb R^n$ , $X$ a nonempty convex compact set, $F^0(\cdot, s) \to f^0$ uniformly on $X$ , $\|g_s\| \le C$ , $\rho_s \ge 0$ , $\rho_s \to 0$ and $\sum_s \rho_s = \infty$ . Then the iterates of (6.41) satisfy

F^0(x^s, s) \longrightarrow \min\{f^0(x) \mid x \in X\} \qquad (s \to \infty).

The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.

Milestones

p. 155 — the one-step recursion $V(x^{s+1}) \le V(x^s) + 2\rho_s\langle g_s, x^*(s) - x^s\rangle + \rho_s^2\|g_s\|^2$ , with $x^*(s)$ a point of $X^*$ nearest to $x^s$ .
p. 156 — the travel bound $\|x^b - x^a\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s$ along (6.41) once $x^a \in X$ .
p. 155 — conditions (1) and (2)(a) of Theorem 6.4 for (6.41): the iterates stay in a compact set and $\|x^{s+1} - x^s\| \to 0$ .
Theorem 6.4 (p. 155) — if $X^*$ is closed, $(x^s)$ lies in a compact set, steps vanish along subsequences converging into $X^*$ , the sequence leaves every small ball around a subsequential limit outside $X^*$ , and it leaves with a strictly lower value of a continuous $V$ that takes countably many values on $X^*$ , then $V(x^s)$ converges and all accumulation points lie in $X^*$ .
pp. 155–156 — conditions (2)(b) and (3) of Theorem 6.4 for (6.41) with $X^* = \arg\min_X f^0$ and $V = \operatorname{dist}(\cdot, X^*)^2$ :

\limsup_{k\to\infty} V(x^{\tau_k}) < \lim_{k\to\infty} V(x^{s_k}).

Significance

Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which $f^0$ is replaced by $F^0(x, s) = \mathbb E f^0(x + h(s))$ with a vanishing perturbation $h(s)$ (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.

Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.

Difficulty

The obvious argument for projected subgradient methods tracks $V(x^s) = \operatorname{dist}(x^s, X^*)^2$ and shows that it decreases whenever $x^s$ is far from $X^*$ . Here that argument fails at two points. First, the subgradient is taken on $F^0(\cdot, s)$ , not on $f^0$ , so the decrease of $V$ holds only up to an error controlled by $\sup_X|F^0(\cdot, s) - f^0|$ , and only while the iterate stays away from $X^*$ ; near $X^*$ , $V$ may increase. Second, a decrease of $V$ over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point $x' \notin X^*$ infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that $V$ takes only countably many values on $X^*$ is what separates it from a monotone-descent statement.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from $s = 0$ as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of $\mathbb R^n$ , and $F^0(\cdot, s)$ , $f^0$ are convex and continuous on all of $\mathbb R^n$ .
projX X y is a minimizer of $\|y - x\|^2$ over $X$ (junk value $y$ when none exists; every statement assumes $X$ nonempty, closed and convex). optimalSet f X is the set of minimizers of $f$ on $X$ ; $V$ is Metric.infDist · X* ^ 2.
Added hypotheses the page does not print: $\rho_s \ge 0$ (step sizes are nonnegative throughout the chapter) and $X \ne \varnothing$ (the minimum over $X$ must exist). The limit $\min_X f^0$ is written sInf (f '' X); $\sum_s\rho_s = \infty$ is divergence of the partial sums.
Constants. The only unspecified constant is the $C$ of the travel bound on p. 156 ("where $C$ is a constant"); the proof yields $C$ = the bound of hypothesis (d), $\|g_s\| \le C$ , and that is the constant in milestone 2. All other results are qualitative.
Corrections of the page. (i) Theorem 6.4 (2)(b) is printed as " $\tau_k = \min\{s \mid s \ge s_k, \|x^{s_k} - x^s\| < \varepsilon\} > \infty$ ", which no sequence satisfies; following the proof of Theorem 6.3 it is read as: $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ is finite. "For $\varepsilon$ sufficiently small and for any $s_k$ " is read as "there is $\varepsilon_0 > 0$ such that for all $\varepsilon \in (0,\varepsilon_0)$ and all $k$ ", and condition (3) is imposed for the same $\varepsilon$ . (ii) The left limit in (3) is read as $\limsup$ (the proof prints $\overline{\lim}$ ); the right limit is $V(x')$ . (iii) The display on p. 155 prints " $=$ " where the projection gives " $\le$ ". (iv) The proof on p. 155 prints " $x^{s_k} \to x' \in X^*$ " where $x' \notin X^*$ is meant.
Theorem 6.5 (the stochastic version, p. 156) is not formalized: the chapter states it without proof, citing [19], its moment hypothesis $E\|\xi^0(s)\| < \mathrm{const}$ and the measurability of the random step sizes $\rho_s$ are not pinned down on the page, and it is not used by Theorem 6.3.
A trivializing formalization is ruled out: the goal is about the iteration (6.41) itself, not a statement that assumes $x^s \to X^*$ and derives the limit of the values, and no hypothesis forces the sequence or the functions to be constant.
Contributions welcome: properties of projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.

Selected references

Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, pp. 141–185 (§6.4, pp. 152–156). https://doi.org/10.1007/978-3-642-61370-8
Yu. M. Ermoliev, Stochastic Programming Methods (in Russian), Nauka, Moscow, 1976 (the chapter's [5]; Theorem 6.4 is on p. 181).
Yu. M. Ermoliev and E. A. Nurminski, "Limit extremal problems", Kibernetika 1 (1973) (the chapter's [14]).
E. A. Nurminski, "Convergence conditions of algorithms of stochastic programming", Kibernetika 3 (1973) (the chapter's [11]).
E. A. Nurminski, "The problem of nonstationary optimization", Kibernetika 2 (1977) (the chapter's [16]).
A. A. Gaivoronski, "Nonstationary stochastic programming problems", Kibernetika 4 (1978) (the chapter's [19]).
W. I. Zangwill, Nonlinear Programming: A Unified Approach, Prentice-Hall, 1969.

8 thms2 active usersReviewed

Completed

Combinatorics Discrete Geometry Linear Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming X: Pairwise Intersecting d-Intervals Have a Transversal of Size 2d²Textbook

Motivation

A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.

This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of $d$ intervals can always be pierced by $2d^2$ points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.

Timeline.

1970: Gyárfás and Lehel prove that a bound depending only on $d$ exists; their bound is exponential in $d$ (A Helly-type problem in trees, in Combinatorial Theory and its Applications, North-Holland).
1992: Alon and Kleitman solve the Hadwiger–Debrunner $(p,q)$ -problem with a method combining fractional transversals and LP duality (Adv. Math. 96).
1997: Kaiser proves the bound $d^2$ using algebraic topology (Discrete Comput. Geom. 18).
1998: Alon gives the short LP-duality proof of the bound $2d^2$ formalized here (Discrete Comput. Geom. 19).
2001: Matoušek shows that the transversal number cannot in general be below a constant multiple of $d^2/\log d$ (Discrete Comput. Geom. 26).

Setting

Fix an integer $d \ge 1$ . A $d$ -interval is a union of $d$ closed intervals on the real line,

J = [a_1,b_1] \cup \dots \cup [a_d,b_d], \qquad a_k \le b_k .

The numbers $a_k$ and $b_k$ are the endpoints of $J$ . A finite family $\mathcal J$ of $d$ -intervals is pairwise intersecting if $J_1 \cap J_2 \ne \emptyset$ for all $J_1, J_2 \in \mathcal J$ . A set $X$ of real numbers is a transversal of $\mathcal J$ if every $J \in \mathcal J$ contains a point of $X$ .

More generally, for a finite set $V$ and a system $\mathcal F$ of subsets of $V$ : a transversal is a set $X \subseteq V$ meeting every member; the transversal number $\tau(\mathcal F)$ is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The fractional transversal number $\tau^*(\mathcal F)$ is the optimal value of the linear program

\min \sum_{v\in V} x_v \quad \text{s.t.} \quad \sum_{v \in F} x_v \ge 1 \ (F \in \mathcal F),\ x \ge 0,

and the fractional matching number $\nu^*(\mathcal F)$ is the optimal value of

\max \sum_{F\in\mathcal F} y_F \quad \text{s.t.} \quad \sum_{F :\, v \in F} y_F \le 1 \ (v \in V),\ y \ge 0 .

Formalization targets

Goal: Theorem 8.6.1

\mathcal J \text{ finite, pairwise intersecting family of } d\text{-intervals} \;\Longrightarrow\; \exists X \subset \mathbb R,\ |X| \le 2d^2,\ X \cap J \ne \emptyset \ \ \forall J \in \mathcal J .

This is the book's theorem with its constant $2d^2$ .

Milestones

Lemma 8.6.2. If $J_1,\dots,J_n$ ( $n \ge 1$ , repetitions allowed) are $d$ -intervals with $J_i \cap J_j \ne \emptyset$ for all $i,j$ , then some endpoint of some $J_i$ lies in at least $n/2d$ of the $J_j$ .
§8.6, p. 182. For every finite set system with nonempty members,

\nu(\mathcal F) \le \nu^*(\mathcal F) = \tau^*(\mathcal F) \le \tau(\mathcal F).

Lemma 8.6.3. If $\mathcal J$ is a finite pairwise intersecting family of $d$ -intervals and $P$ its set of endpoints, there are weights $x_p \ge 0$ , $p \in P$ , with $\sum_{p \in J \cap P} x_p \ge 1$ for every $J \in \mathcal J$ and $\sum_{p\in P} x_p \le 2d$ .

Significance

The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting $d$ -intervals is bounded by a function of $d$ alone, and that this function is polynomial. The section also states, without proof, the extension $\tau(\mathcal J) \le 2d^2\,\nu(\mathcal J)$ for arbitrary finite families of $d$ -intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain $\nu \le \nu^* = \tau^* \le \tau$ is the standard frame in which such bounds are proved.

Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of $d$ -intervals.

Difficulty

The obvious generalization of the one-dimensional argument fails: for $d \ge 2$ no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.

Formalization scope

A $d$ -interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet $= \bigcup_k [a_k,b_k]$ . Components are indexed $0,\dots,d-1$ . Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses $d \ge 1$ (the book's definition) and, in Lemma 8.6.2, $n \ge 1$ are explicit. The quantity $n/2d$ is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by $2d^2$ .

For set systems, $V$ is a finite type and $\mathcal F$ a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers $\tau^*$ and $\nu^*$ are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. $\tau$ is an sInf over $\mathbb N$ that is attained under the nonemptiness assumption, and $\nu$ is a maximum over the finite family of matchings.

A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets $J$ , not a representation artifact, and the bound $2d^2$ and $2d$ are the book's constants, not weakened ones.

Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.6. https://doi.org/10.1007/978-3-540-30717-4
N. Alon, Piercing d-intervals, Discrete Comput. Geom. 19 (1998) 333–334.
N. Alon, D. Kleitman, Piercing convex sets and the Hadwiger–Debrunner (p, q)-problem, Adv. Math. 96 (1992) 103–112.
T. Kaiser, Transversals of d-intervals, Discrete Comput. Geom. 18 (1997) 195–203.
J. Matoušek, Lower bounds on the transversal numbers of d-intervals, Discrete Comput. Geom. 26 (2001) 283–287.
A. Gyárfás, J. Lehel, A Helly-type problem in trees, in Combinatorial Theory and its Applications (P. Erdős, A. Rényi, V. T. Sós, eds.), North-Holland, 1970, 571–584.

6 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Random Matrix Theory·Captain: mikedeng1

Understanding and Using Linear Programming IX: Basis Pursuit Recovers Sparse Solutions Exactly iff the Kernel Misses the CrosspolytopeTextbook

Motivation

A deep-space probe sends a vector $w\in\mathbb{R}^k$ encoded as $z=Qw\in\mathbb{R}^n$ , and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system $Ax=b$ , and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.

Timeline, as recorded in the book's references:

1999: Chen, Donoho and Saunders introduce basis pursuit, minimizing the $\ell_1$ -norm subject to $Ax=b$ (SIAM J. Sci. Comput. 20).
2005: Candès, Rudelson, Tao and Vershynin prove that for every $\alpha\in(0,1)$ there is $\beta(\alpha)>0$ such that a random $\lfloor\alpha n\rfloor\times n$ matrix is exact for $\lfloor\beta n\rfloor$ -sparse vectors with probability exponentially close to 1 (FOCS 2005).
2006: Donoho, via neighborliness of centrally symmetric polytopes, obtains the constants $\alpha=0.75$ , $\beta=0.08$ used in the book, and shows that no $\lfloor 0.75n\rfloor\times n$ matrix is exact for $r>0.25n$ when $n$ is large (Discrete Comput. Geom. 35).
2006: Linial and Novik prove further upper bounds showing that these existence results are asymptotically optimal (Discrete Comput. Geom. 36).

Setting

Let $A$ be a real $m\times n$ matrix with $m<n$ and $b\in\mathbb{R}^m$ . The support of $x\in\mathbb{R}^n$ is $\operatorname{supp}(x)=\{i: x_i\ne 0\}$ . For an integer $r\ge 0$ , a sparse solution of $Ax=b$ is an $x$ with $Ax=b$ and $|\operatorname{supp}(x)|\le r$ . The $\ell_1$ -norm is $\|x\|_1=|x_1|+\dots+|x_n|$ .

Basis pursuit is the optimization problem

\text{(BP)}\qquad\text{minimize } \|x\|_1\ \text{ subject to } x\in\mathbb{R}^n,\ Ax=b,

which is equivalent to the linear program

\text{(BP}'\text{)}\qquad\text{minimize } u_1+\dots+u_n\ \text{ subject to } Ax=b,\ -u\le x\le u,\ u\ge 0 .

The matrix $A$ is BP-exact for $r$ if for every $b\in\mathbb{R}^m$ : whenever $Ax=b$ has a solution $\tilde x$ with at most $r$ nonzero components, $\tilde x$ is the unique optimal solution of (BP). The crosspolytope is $B^n_1=\{x:\|x\|_1\le 1\}$ , the kernel of $A$ is $L=\{x: Ax=0\}$ , and $L+z=\{\ell+z:\ell\in L\}$ . For $z$ with $\|z\|_1=1$ , the cone at $z$ is $C_z=\{t(x-z): t\ge 0,\ x\in B^n_1\}$ , and $L$ is good for $z$ if $(L+z)\cap B^n_1=\{z\}$ .

Formalization targets

Goal: Lemma 8.5.4 (reformulation of BP-exactness)

For $m<n$ and $r\le m$ :

A \text{ is BP-exact for } r\iff \forall z\in\mathbb{R}^n\ \text{with}\ \|z\|_1=1,\ |\operatorname{supp}(z)|\le r:\quad (L+z)\cap B^n_1=\{z\}.

This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.

Milestones

Observation 8.5.1: $Ax=b$ has at most one sparse solution for every $b$ if and only if every $2r$ or fewer columns of $A$ are linearly independent.
The remark after it (p. 169): under $m<n$ , that column condition forces $m\ge 2r$ .
Equivalence of (BP) and (BP′) (p. 170): in every optimal solution of (BP′), $u_i=|x_i|$ ; and $x$ is optimal for (BP) iff $(x,|x|)$ is optimal for (BP′).
From the proof of Lemma 8.5.4 (p. 173): if $Az=b$ , the solution set of $Ax=b$ is exactly $L+z$ .
From "Intuition for BP-exactness" (p. 174): for $\|z\|_1=1$ and $|\operatorname{supp}(z)|\le r$ , $L$ is good for $z$ iff $L\cap C_z=\{0\}$ .

Further draft item: Theorem 8.5.2

With $m=\lfloor 0.75n\rfloor$ , $r=\lfloor 0.08n\rfloor$ and $A$ an $m\times n$ matrix of independent $N(0,1)$ entries, there is a constant $c>0$ such that for every $n$

\Pr[A \text{ is BP-exact for } r]\ \ge\ 1-e^{-cm}.

The book states this without proof. It is included as a separate theorem, not a milestone of the goal.

Significance

Lemma 8.5.4 converts an algorithmic property, that an $\ell_1$ linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of $A$ relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that $L$ avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.

All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set $S$ rather than characterizing exactness for all $r$ -sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants $0.75$ and $0.08$ is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.

Difficulty

For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution $\tilde x$ and the boundary point $\tilde x/\|\tilde x\|_1$ , the case $\tilde x=0$ , and the fact that BP-exactness quantifies over all right-hand sides $b$ while the geometric side quantifies over boundary points of the crosspolytope.

Theorem 8.5.2 is of a different order. A union bound over the $\binom{n}{r}2^r$ faces of dimension $r-1$ reduces it to bounding the probability that a random $(n-m)$ -dimensional subspace meets one cone $C_F$ nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give $0.08$ at $\alpha=0.75$ .

Formalization scope

Vectors are functions Fin n → ℝ (the book's indices $1,\dots,n$ become $0,\dots,n-1$ ) and matrices are Matrix (Fin m) (Fin n) ℝ. The $\ell_1$ -norm is written out as $\sum_i|x_i|$ , since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every $2r$ or fewer columns" ranges over finsets of distinct column indices, column $j$ being Aᵀ j. The hypotheses $m<n$ and $r\le m$ of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; $m<n$ is also the standing assumption of §8.5 needed for $m\ge 2r$ .

In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant $c>0$ is quantified before $n$ , and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.

A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of $\tilde x$ , and the crosspolytope condition is an equality of sets, not an inclusion that $z$ alone would satisfy.

All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the $\ell_1$ and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.5. https://doi.org/10.1007/978-3-540-30717-4
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1), 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, M. Rudelson, T. Tao and R. Vershynin, Error correction via linear programming, Proc. 46th IEEE FOCS, 2005, 295–308. https://doi.org/10.1109/SFCS.2005.5464411
D. L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete Comput. Geom. 35, 2006, 617–652. https://doi.org/10.1007/s00454-005-1220-0
N. Linial and I. Novik, How neighborly can a centrally symmetric polytope be?, Discrete Comput. Geom. 36, 2006, 273–281. https://doi.org/10.1007/s00454-006-1235-1

7 thms2 active usersReviewed

Missions

Optimal Policies for a Multi-Echelon Inventory Problem: The Two-Echelon Optimal Cost Splits into the Isolated Installation-1 Cost Plus a Function of Echelon StockResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 482)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time: Minimal Optimal Predecessor Lists Are Characterized by Strictly Increasing BreakpointsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1(a)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems: Algorithm OPT Returns an Optimal Reorder Point and Order QuantityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones, in proof order

Significance

Difficulty

Formalization scope

Selected references

A Nonlinear Programming Algorithm for Solving Semidefinite Programs via Low-rank Factorization: A Regular Local Minimum That Stays Locally Minimal After Adding a Zero Column Solves the SDPResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.5

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Sequential Decisions and Markov Chains 3: A Deterministic Stationary Procedure Minimizes the Ratio of Two Long-Run Average CostsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 23)

Steps of the proof (milestones)

Significance

Difficulty

Formalization scope

Selected references

Project Scheduling with Time Windows and Scarce Resources VII: A Locally Quasiconcave Objective Always Has a Quasistable Optimal ScheduleTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.3.13

Milestones

Significance

Difficulty

Formalization scope

Selected references

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems V: Bandit Convex Optimization with One-Point FeedbackTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.2, tuned

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dimensioning Large Call Centers I: The Rationalized Staffing Function Is Asymptotically OptimalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Goal: the $Jm_2+1$ bound, with correctness

Goal: the Gaussian protection level and its sensitivity to $\hat\sigma$