Operations Research

Convex Optimization Optimization·Captain: mikedeng1

An Exact Duality Theory for Semidefinite Programming and Its Complexity Implications: The Extended Lagrange–Slater Dual Has Zero Duality Gap and Attains Its OptimumResearch Paper

Motivation

Semidefinite programming (SDP) optimizes a linear function over the intersection of the cone of positive semidefinite matrices with an affine subspace. It contains linear programming as the diagonal case and is the computational core of relaxations in combinatorial optimization, control theory and polynomial optimization. Its standard duality theory, however, is weaker than that of linear programming. The Lagrangian dual of an SDP can have a strictly positive duality gap, can fail to attain its optimal value, and an infeasible semidefinite system need not have a certificate of infeasibility of the naive Farkas form. All the classical strong duality theorems for SDP therefore assume a constraint qualification such as Slater's condition (a strictly feasible point).

M. V. Ramana (1997, Math. Program. 77, 129–162) constructed a dual, the Extended Lagrange–Slater Dual (ELSD), whose size is polynomial in the data and which enjoys every property of linear programming duality for every SDP, with no constraint qualification. The same construction yields an exact theorem of the alternative for semidefinite feasibility and the complexity consequence that semidefinite feasibility lies in NP if and only if it lies in co-NP in the Turing model.

Timeline:

1980s–1990s: Lagrangian (Slater-type) duality for SDP, with strong duality under strict feasibility (see e.g. the surveys of Vandenberghe and Boyd, SIAM Rev. 38 (1996)).
1981: Borwein and Wolkowicz, facial reduction for general convex programs, which regularizes a problem by passing to the minimal face containing the feasible set; not of polynomial size in the SDP data (J. Math. Anal. Appl. 83 (1981)).
1997: Ramana, the ELSD, an explicit polynomial-size dual with zero gap and dual attainment for every SDP.
1997: Ramana, Tunçel and Wolkowicz relate the ELSD to facial reduction (SIAM J. Optim. 7 (1997)).

Setting

Let $n, m$ be natural numbers, $\mathcal M_n$ the space of real $n\times n$ matrices, and $\mathcal S_n\subseteq\mathcal M_n$ the symmetric ones. On $\mathcal M_n$ the inner product is $A\bullet B = \sum_{i,j}A_{ij}B_{ij}$ . For symmetric $A$ , $A\succeq 0$ means $A$ is positive semidefinite. The data are symmetric $Q_0, Q_1,\dots,Q_m\in\mathcal S_n$ and $c\in\mathbb R^m$ . The primal SDP is

(\mathrm P)\qquad \sup\ c^{\mathsf T}x\quad\text{s.t.}\quad Q(x) := Q_0-\sum_{i=1}^m x_iQ_i\succeq 0 ,

with feasible region $G = \{x\mid Q(x)\succeq 0\}$ , a spectrahedron. Define $Q^*:\mathcal M_n\to\mathbb R^m$ by $Q^*(U) = (U\bullet Q_i)_{i=1}^m$ and write $Q^\#(U) = 0$ for " $Q_0\bullet U = 0$ and $Q^*(U) = 0$ ".

For $k\ge 1$ let $\mathcal C_k$ be the set of tuples $(U_i, W_i)_{i=1}^k$ of real $n\times n$ matrices with $W_0 = 0$ and, for $i = 1,\dots,k$ ,

Q^\#(U_i+W_{i-1}) = 0,\qquad U_i\succeq W_iW_i^{\mathsf T}.

The $W_i$ need not be symmetric. $\mathcal U_k$ and $\mathcal W_k$ are the sets of last components $U_k$ and $W_k$ ; $\mathcal W_0 = \{0\}$ . The ELSD is

\inf\ (U+W)\bullet Q_0\quad\text{s.t.}\quad Q^*(U+W) = c,\quad W\in\mathcal W_m,\quad U\succeq 0,

and Weak-ELSD is the same program with $\mathcal W_{m-1}$ . For the milestones: the polar $G^\circ = \{y\mid x^{\mathsf T}y\le 1\ \forall x\in G\}$ , the algebraic polar $G^* = \{Q^*(U)\mid U\bullet Q_0\le 1,\ U\succeq 0\}$ , and $S_k = Q^*(\mathcal W_k)$ .

Formalization targets

Goal: Theorem 6 (Duality Theorem)

For all data $(Q_0,\dots,Q_m,c)$ :

weak duality: $c^{\mathsf T}x\le (U+W)\bullet Q_0$ for $x\in G$ and $(U,W)$ feasible for ELSD or Weak-ELSD;
if $G\neq\emptyset$ , then $\sup_{x\in G}c^{\mathsf T}x<\infty$ iff ELSD is feasible, iff Weak-ELSD is feasible;
if $G\ne\emptyset$ and ELSD (or Weak-ELSD) is feasible, there is $v\in\mathbb R$ with

v = \sup_{x\in G}c^{\mathsf T}x = \inf_{\mathrm{ELSD}}(U+W)\bullet Q_0 = \inf_{\mathrm{Weak\text{-}ELSD}}(U+W)\bullet Q_0;

if $G\ne\emptyset$ and the primal is bounded, ELSD attains $v$ .

Milestones

Propositions 7(vi) and 7(vii) (facts on PSD matrices), Lemma 9 (annihilation $Q(x)U = Q(x)W = 0$ ), weak duality over every $\mathcal W_k$ , Lemma 10 (nested subspaces), Lemma 13 ( $G^\circ = \mathrm{Cl}(G^*)$ ), Corollary 14, Claims 17 and 16, the central Theorem 12,

G^\circ = \{Q^*(U+W)\mid W\in\mathcal W_k,\ U\succeq 0,\ U\bullet Q_0\le 1\}\qquad(0\in G,\ k\ge m-1),

the translation invariance of $\mathcal C_k,\mathcal U_k,\mathcal W_k$ (§2.5), and system (14) (dual attainment at value 0). Theorems 19–21 (Farkas lemma for SDP, optimality condition, primal attainment) are further items stated on the same definitions.

Significance

The Duality Theorem gives SDP a dual with the full strength of linear programming duality for every instance, at polynomial size. Consequences in the paper: an exact theorem of the alternative for semidefinite feasibility (Theorem 19); semidefinite characterizations of optimality of a given point and of primal attainment (Theorems 20, 21); and the complexity results that semidefinite feasibility is in NP iff it is in co-NP in the Turing model and in NP ∩ co-NP in the Blum–Shub–Smale model (Theorem 25, not part of this mission). Theorem 12 separately gives an exact semidefinite description of the polar of any spectrahedron containing the origin.

The results are proved on paper and are classical. No machine-checked version is known to exist; the platform's existing SDP duality theorem assumes Slater's condition. A formalization would provide the first constraint-qualification-free SDP duality in Lean, together with reusable infrastructure on PSD matrices (range inclusion, $A\bullet B = 0\Rightarrow AB = 0$ ) and on polars of convex sets.

Difficulty

The obvious route to SDP strong duality separates the primal's value from the image of the PSD cone under a linear map and invokes a closed-cone Farkas lemma. That step fails: the linear image of the PSD cone need not be closed, which is exactly why Lagrangian duality has gaps. In this mission the obstruction reappears as the non-closedness of the algebraic polar $G^*$ (Lemma 13 only gives $G^\circ = \mathrm{Cl}(G^*)$ ). The difficulty is to show that finitely many, and at most $m-1$ , corrections by the sets $S_k$ close $G^*+S_k$ (Claims 16, 17), and to control dimensions in doing so. A proof by assuming closedness, strict feasibility or a Slater point is a different theorem.

Formalization scope

Everything lives in the namespace ExactSDPDuality.ELSD, in one definition file. Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin m → ℝ; " $\succeq 0$ " is Mathlib's PosSemidef (which over ℝ includes symmetry); $A\bullet B$ is the entrywise sum on all of $\mathcal M_n$ ; $c^{\mathsf T}x$ is the dot product. The data $Q_0,\dots,Q_m$ carry symmetry hypotheses in every statement, as the paper assumes throughout. $\mathcal C_k$ is encoded by sequences $U, W:\mathbb N\to\mathcal M_n$ with $U_0 = W_0 = 0$ , so $\mathcal U_0 = \mathcal W_0 = \{0\}$ ; for $m = 0$ the index $m-1$ is $0$ . Optimal values are least upper and greatest lower bounds of the value sets, never real sSup/sInf. The polar is the one-sided polar. In §2.4 statements the standing assumption $0\in G$ is a hypothesis. In Claim 16 the index satisfies $k+1\le m$ , the range where $S_{k+1}$ is introduced, and $\dim S_k$ is the rank of the span of $S_k$ .

Theorems 20 and 21 are printed with $Q^*(U+W) = 0$ ; both are false as printed (counterexamples in the items) and are stated with the corrected $Q^*(U+W) = c$ that the paper's derivation from Theorem 6 gives.

Trivializing formalizations are ruled out: no Slater or other constraint qualification appears; the dual is the ELSD built from the recursively defined $\mathcal W_m$ , not the Lagrangian dual or an arbitrary subspace; the $W_i$ range over all of $\mathcal M_n$ , not only symmetric matrices (the paper's Example 4 needs a nonsymmetric $W_2$ ).

Needed infrastructure: PSD matrix facts (Proposition 7), bipolar theorem for closed convex sets containing the origin (Proposition 11), closedness arguments for linear images of cones, and dimension counting of subspaces of $\mathbb R^m$ . Contributions of any milestone, of these general lemmas, and of alternative proofs (for instance via facial reduction) are welcome.

Selected references

M. V. Ramana, An exact duality theory for semidefinite programming and its complexity implications, Mathematical Programming 77 (1997) 129–162. https://doi.org/10.1007/BF02614433
M. V. Ramana, L. Tunçel, H. Wolkowicz, Strong duality for semidefinite programming, SIAM Journal on Optimization 7 (1997) 641–662. https://doi.org/10.1137/S1052623495288350
J. M. Borwein, H. Wolkowicz, Regularizing the abstract convex program, Journal of Mathematical Analysis and Applications 83 (1981) 495–530. https://doi.org/10.1016/0022-247X(81)90138-4
L. Vandenberghe, S. Boyd, Semidefinite programming, SIAM Review 38 (1996) 49–95. https://doi.org/10.1137/1038003
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

14 thms3 active usersReviewed

Completed

Analysis Numerical Analysis Optimization·Captain: mikedeng1

A Nonsmooth Version of Newton's Method I: local superlinear convergence of the generalized-Jacobian Newton method at a semismooth regular rootResearch Paper

Motivation

Many problems in optimization and equilibrium modelling reduce to a system of equations $F(x) = 0$ whose map $F : \mathbb R^n \to \mathbb R^n$ is Lipschitz but not differentiable: reformulations of nonlinear complementarity problems through the componentwise minimum or the Fischer–Burmeister function, Karush–Kuhn–Tucker systems of constrained programs, and gradients of augmented Lagrangians all have kinks. Newton's method, $x^{k+1} = x^k - F'(x^k)^{-1}F(x^k)$ , is the standard fast local solver for smooth systems, but it needs a derivative at every iterate.

Qi and Sun (Math. Programming 58, 1993) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and showed that the resulting method converges locally superlinearly under a regularity condition they called semismoothness, extending Mifflin's notion for functionals (Mifflin, SIAM J. Control Optim. 15, 1977) to vector-valued maps. This theorem is the foundation of the family of semismooth Newton methods used in complementarity, variational inequalities and PDE-constrained optimization.

Timeline. Robinson (1988) and Pang (Math. OR 15, 1990) studied Newton methods built on B-derivatives, with convergence proved under a strong Fréchet derivative at the solution; Kummer (1988) gave an abstract framework for Newton methods for nonsmooth equations; Qi and Sun (1993) proved local superlinear convergence for the generalized-Jacobian iteration under semismoothness and nonsingularity of $\partial F(x^*)$ , with order $1+p$ under $p$ -order semismoothness.

Setting

Let $F : \mathbb R^n \to \mathbb R^m$ be locally Lipschitz. By Rademacher's theorem $F$ is differentiable on a set $D_F$ of full measure; write $JF(y)$ for the Jacobian at $y \in D_F$ . The generalized Jacobian is

\partial F(x) = \mathrm{co}\Big\{\lim_{i\to\infty} JF(x_i) : x_i \to x,\ x_i \in D_F\Big\},

the convex hull of all limits of Jacobians along sequences of differentiability points converging to $x$ . The one-sided directional derivative is $F'(x;h) = \lim_{t\downarrow 0}(F(x+th)-F(x))/t$ .

$F$ is semismooth at $x$ if it is Lipschitz near $x$ and, for every $h$ , the limit of $Vh'$ over $V \in \partial F(x+th')$ , $h' \to h$ , $t \downarrow 0$ exists. For $0 < p \le 1$ , $F$ is $p$ -order semismooth at $x$ if in addition $Vh - F'(x;h) = O(\|h\|^{1+p})$ for $V \in \partial F(x+h)$ , $h \to 0$ .

For $m = n$ , the nonsmooth Newton method is

x^{k+1} = x^k - V_k^{-1}F(x^k), \qquad V_k \in \partial F(x^k), \tag{3.2}

where any element of $\partial F(x^k)$ may be chosen at each step. A run is a pair of sequences $(x^k)$ , $(V_k)$ with $V_k \in \partial F(x^k)$ and $V_k(x^{k+1}-x^k) = -F(x^k)$ for all $k$ . A root $x^*$ ( $F(x^*) = 0$ ) is regular when every $V \in \partial F(x^*)$ is nonsingular.

Formalization targets

Goal: Theorem 3.2, local superlinear convergence

Let $F$ be locally Lipschitz, $F(x^*) = 0$ , $F$ semismooth at $x^*$ , and every $V \in \partial F(x^*)$ nonsingular. Then there is $\delta > 0$ such that every $V \in \partial F(y)$ with $\|y - x^*\| < \delta$ is nonsingular, a Newton step from such a $y$ stays within $\delta$ of $x^*$ , and every run with $\|x^0 - x^*\| < \delta$ satisfies

x^k \to x^*, \qquad \|x^{k+1} - x^*\| = o(\|x^k - x^*\|).

The goal asserts only the shape of the convergence (superlinear) and fixes no constants.

Stronger: Theorem 3.2, order $1 + p$

If moreover $F$ is $p$ -order semismooth at $x^*$ , $0 < p \le 1$ , there are $\delta > 0$ and $C$ with

\|x^{k+1} - x^*\| \le C\|x^k - x^*\|^{1+p}

for every run started within $\delta$ of $x^*$ .

Milestones

The milestones follow the paper's route: Proposition 2.1 (the limit in the definition of semismoothness is the directional derivative), Lemma 2.2 (Lipschitz continuity of $F'(x;\cdot)$ and its realisation by an element of $\partial F(x)$ ), Theorem 2.3 (semismoothness is equivalent to $Vh - F'(x;h) = o(\|h\|)$ and to the corresponding condition at differentiability points), the Remark's expansion (2.17), Proposition 3.1 (uniform invertibility near a regular point), the order- $(1+p)$ sentence of Theorem 3.2, and Corollary 2.5 (strong Fréchet differentiability implies semismoothness).

Significance

The theorem gives a locally superlinearly convergent method for Lipschitz equations with no smoothness beyond semismoothness at the root. Convex, smooth and subsmooth functions are semismooth, as are sums and scalar products of semismooth functions (the paper, citing Mifflin), and later work showed that the complementarity and KKT reformulations on which semismooth Newton solvers are built are semismooth as well; the order- $(1+p)$ variant gives local quadratic convergence for strongly semismooth maps. Mission II of this series treats the paper's global convergence theorem on a ball, and Mission III the semismoothness of augmented Lagrangian gradients, which supplies the application.

The results are proved in the paper. No machine-checked version of the generalized Jacobian, of semismoothness or of the nonsmooth Newton method is known to exist in Mathlib or on this platform; the platform's formalized Newton results concern one-dimensional $C^2$ functions (MetodosNumericos.newton_local_convergence) and smooth convex minimization. A complete development would provide the first formal library for Clarke's generalized Jacobian and semismooth maps.

Difficulty

The classical Newton proof compares $F(x^k)$ with its linearization $JF(x^*)(x^k - x^*)$ and uses continuity of the Jacobian at $x^*$ . Here neither is available: $F$ need not be differentiable at $x^*$ or at any iterate, the element $V_k$ is chosen arbitrarily from a set, and $V_k$ need not be close to any fixed linear map. The comparison has to go through the directional derivative $F'(x^*; \cdot)$ , which is only positively homogeneous, not linear. The analytic content therefore sits in Section 2: showing that semismoothness, defined through a limit over a set-valued map, controls $Vh - F'(x;h)$ uniformly in the direction, and that $F(x+h) - F(x) - F'(x;h)$ is small. Both rest on Clarke's mean-value inclusion and on compactness and upper semicontinuity of $\partial F$ , none of which is in Mathlib. The superlinear rate also requires a uniform bound on $\|V^{-1}\|$ in a whole neighbourhood, not just at $x^*$ .

Formalization scope

Everything lives in the namespace NonsmoothNewton.Local. Section 2 results are stated for maps between finite-dimensional real normed spaces $E \to G$ (the paper's $\mathbb R^n \to \mathbb R^m$ is the Euclidean instance); Section 3 results use EuclideanSpace ℝ (Fin n). Conventions fixed by the Lean statements:

$JF$ is fderiv; the generalized Jacobian is the convex hull (no closure) of limits of fderiv along sequences $x_i \to x$ of differentiability points.
$F'(x;h)$ is the one-sided limit over $t \downarrow 0$ , never the two-sided lineDeriv; its value is a limUnder, used only where existence is a hypothesis or a consequence.
Nonsingular means IsUnit in the ring of continuous linear endomorphisms; $\|V^{-1}\| \le C$ is a two-sided inverse of operator norm at most $C$ .
A run of (3.2) is encoded by the linear equation $V_k(x^{k+1} - x^k) = -F(x^k)$ with $V_k \in \partial F(x^k)$ ; all choices of $V_k$ are quantified, and $\delta$ is chosen before the run.
Pinned asymptotics. The goal's rate is the proof's display (3.3), stated as IsLittleO along atTop; the printed Theorem 3.2 states only well-definedness and convergence. "Order $1+p$ " is pinned as $\|x^{k+1}-x^*\| \le C\|x^k-x^*\|^{1+p}$ with $\delta$ and $C$ uniform over runs. Every $o(\|h\|)$ in (2.8), (2.9) and (2.17) is its $\varepsilon$ – $\delta$ form with a non-strict inequality $\le \varepsilon\|h\|$ , and every $O(\|h\|^{1+p})$ is an explicit constant and radius.
The standing assumptions " $F$ locally Lipschitzian" of Sections 2 and 3 are hypotheses of every statement.
The strong Fréchet derivative of Corollary 2.5 is Mathlib's HasStrictFDerivAt, which corrects the misprint $F(x)$ for $F(z)$ in the paper's display (2.16).

A trivializing formalization is ruled out: the update is not written with a junk inverse (which would make a singular step "well defined"), the generalized Jacobian is the paper's nonempty set rather than one that could be empty, and the theorem quantifies over every run rather than asserting that some run converges.

A complete development needs Clarke's mean-value inclusion (2.2), compactness and upper semicontinuity of $\partial F$ for locally Lipschitz maps (via Rademacher's theorem, available in Mathlib), and perturbation bounds for inverses of linear maps. The generalized-Jacobian and semismoothness layer is reusable beyond this mission, in particular for Missions II and III of this series. Contributions of proofs of any milestone, and of general lemmas about $\partial F$ , are welcome.

Selected references

L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (SIAM reprint 1990). https://doi.org/10.1137/1.9781611971309
R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM Journal on Control and Optimization 15 (1977) 959–972. https://doi.org/10.1137/0315061
J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15 (1990) 311–341. https://doi.org/10.1287/moor.15.2.311
J. M. Ortega, W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970 (SIAM reprint 2000). https://doi.org/10.1137/1.9780898719468

14 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Optimization·Captain: mikedeng1

Shortest Connection Networks And Some Generalizations: Construction Principles P1 and P2 Yield a Shortest Spanning Subtree of Every Connected Labelled GraphResearch Paper

Motivation

Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.

Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.

Setting

Let $V$ be a finite set of $N$ terminals and $G$ a simple graph on $V$ , the labelled graph whose edges are the possible links. Each edge $e$ carries a real length $w(e)$ ; lengths may be negative, zero, or tie. For a finite set $F$ of links, $H(F)$ denotes the graph on $V$ whose edges are the links of $F$ .

A spanning subtree of $G$ is a set $F$ of edges of $G$ such that $H(F)$ is a tree on $V$ . Its length is $\ell_w(F) = \sum_{e \in F} w(e)$ .
A shortest spanning subtree (SSS) is a spanning subtree of least length among all spanning subtrees of $G$ . Prim's dictionary is "shortest connection network (SCN) ↔ shortest spanning subtree (SSS)". $L(G,w)$ denotes that least length.
Given the links $F$ made so far, the connected components of $H(F)$ are the isolated terminals (one terminal) and isolated fragments (two or more terminals).
Principle 1: any isolated terminal $t$ can be connected to a nearest neighbor, a $G$ -neighbor $n$ with $w(\{t,n\}) \le w(\{t,m\})$ for all $G$ -neighbors $m$ of $t$ .
Principle 2: any isolated fragment $C$ can be connected to a nearest neighbor $n \notin C$ by a shortest available link $\{u,n\}$ , $u \in C$ ; equivalently $\{u,n\}$ is a shortest edge of $G$ with one end in $C$ and the other outside.
A construction is a sequence of links $e_0, e_1, \dots$ , each an application of P1 or P2 with respect to the links before it. It is complete when it has $N-1$ links.

Only edges of $G$ are possible links; in Prim's distance table a missing edge has length $\infty$ .

Formalization targets

Goal (§IV, p. 1396)

For every finite connected graph $G$ and every $w$ ,

\Bigl(\exists\ \text{a complete construction}\Bigr) \ \wedge\ \Bigl(\forall\ \text{complete constructions } e_0,\dots,e_{N-2}:\ \{e_0,\dots,e_{N-2}\} \text{ is a SSS of } G\Bigr).

This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.

Milestones

Counting (§II, p. 1392): after any construction with $k$ links, $H(F)$ is acyclic with $N-k$ components; a complete construction is a spanning subtree; a construction with fewer than $N-1$ links can be extended.
Necessary Condition 1 (p. 1392): every terminal of a SSS is linked in it to at least one nearest neighbor.
Necessary Condition 2 (p. 1392): every fragment $S$ of a SSS, $\emptyset \ne S \ne V$ , is linked in it to a nearest neighbor by a shortest available link.
Distinct lengths (§III, p. 1393): if the edge lengths are pairwise distinct, every link of every construction belongs to every SSS.
Continuity (§III, p. 1394): $w \mapsto L(G,w)$ is continuous.

Significance

The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.

The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.

Difficulty

The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of $H(F)$ as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.

Formalization scope

Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:

$V$ is a Fintype with decidable equality; $G$ is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of $G$ matter.
Link sets are Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.
An isolated fragment is a whole connected component of linkGraph F; the P2 condition is a single inequality against every $G$ -edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.
A construction is a List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty $V$ ).
$L$ is sInf of the lengths of spanning subtrees; continuity is in the product topology.

Implicit hypotheses made explicit: $G$ connected (hence $V \ne \emptyset$ ) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; $S$ nonempty and $S \ne V$ for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.

The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.

Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.

Selected references

R. C. Prim, Shortest Connection Networks And Some Generalizations, Bell System Technical Journal 36 (1957), 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proceedings of the AMS 7 (1956), 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
V. Jarník, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 6 (1930), 57–63.
O. Borůvka, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 3 (1926), 37–58.
R. L. Graham, P. Hell, On the history of the minimum spanning tree problem, Annals of the History of Computing 7 (1985), 43–57. https://doi.org/10.1109/MAHC.1985.10011

10 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis Optimization·Captain: mikedeng1

Updating Quasi-Newton Matrices with Limited Storage: The Limited-Storage BFGS Method Reaches the Minimizer of a Strictly Convex Quadratic in at Most n StepsResearch Paper

Motivation

Quasi-Newton methods minimize a smooth function $f$ on $\mathbb{R}^n$ by moving along $d_k = -H_k g_k$ , where $g_k$ is the gradient and $H_k$ is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building $H_k$ , but it stores a dense $n \times n$ matrix, which is prohibitive for large $n$ .

Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last $m$ correction pairs and rebuilding the matrix from a simple initial matrix $H_0$ at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.

Timeline:

1970: Broyden, Fletcher, Goldfarb and Shanno introduce the BFGS update (references [1] and [5] of the paper).
1977: Nazareth relates BFGS to conjugate gradients (Argonne Tech. Memo 282, reference [7]); his form of preconditioned conjugate gradients is the one the paper uses.
1977–1978: Shanno studies the memoryless BFGS update, the case $m = 1$ (reference [11]; journal version Math. Oper. Res. 3, 1978).
1980: Nocedal defines the special BFGS matrices and the SQN method and states that on quadratics with exact line searches SQN is identical to preconditioned conjugate gradients, hence has quadratic termination.
1989: Liu and Nocedal (Math. Programming 45) study the method, now called L-BFGS, for large-scale problems.
1998: Kolda, O'Leary and Nazareth (SIAM J. Optim. 8) treat limited-memory and update-skipping BFGS variants with exact line searches on quadratics.

Setting

Let $A$ be a symmetric positive definite $n \times n$ matrix and $b \in \mathbb{R}^n$ , and let $f(x) = \tfrac12 x^T A x + b^T x$ , a strictly convex quadratic with gradient $g(x) = Ax + b$ and unique minimizer $x^\ast = -A^{-1} b$ .

Exact line search. Along a direction $d \neq 0$ from $x$ , the step $\alpha = -g(x)^T d / d^T A d$ minimizes $f(x + \alpha d)$ .

BFGS update. For a pair $(s, y)$ with $\rho = 1/y^T s$ and $v = I - \rho y s^T$ , the BFGS update of $H$ is

\bar H = v^T H v + \rho s s^T .

Special BFGS matrices. Fix $H_0$ symmetric positive definite and a number $m \ge 1$ of stored corrections. Given pairs $(s_j, y_j)$ , the special matrix $H_K$ is $H_0$ updated by the pairs $j = K - \min(K, m), \dots, K-1$ , oldest first (the paper's (4)–(5)). Only the $m$ most recent pairs enter, and the matrix is rebuilt from $H_0$ .

SQN. Starting from $x_0$ , with $g_i = g(x_i)$ :

d_i = -H_i g_i, \qquad x_{i+1} = x_i + \alpha_i d_i, \qquad s_i = x_{i+1} - x_i,\quad y_i = g_{i+1} - g_i,

with $\alpha_i$ the exact step and $H_{i+1}$ the special matrix built from the last $\min(i+1, m)$ pairs.

PCG with fixed preconditioner $H_0$ . $d_0 = -H_0 g_0$ , $x_{i+1} = x_i + \alpha_i d_i$ , $d_{i+1} = -H_0 g_{i+1} + \beta_{i+1} d_i$ with $\beta_{i+1} = y_i^T H_0 g_{i+1} / y_i^T d_i$ .

Formalization targets

Goal: quadratic termination of SQN

For every $n$ , every symmetric positive definite $A$ and $H_0$ , every $b$ , $x_0$ and every $m \ge 1$ ,

\exists\, k \le n : \quad A x_k + b = 0 ,

where $x_k$ are the SQN iterates. The statement fixes no constant beyond the dimension bound $n$ .

Milestones

Property (a): the special matrices are positive definite whenever $y_i^T s_i > 0$ for all $i$ .
Eq. (7): along conjugate steps, $v_i y_i = 0$ and $v_i y_j = y_j$ for $i > j$ .
Eq. (6): along conjugate steps, $H_k y_j = s_j$ for the $m$ most recent $j$ (when $k > m$ ).
Eq. (10): the special matrix equals $m$ sum-form BFGS corrections applied to $H_0$ .
Eq. (15): the PCG directions satisfy $d_i^T y_j = 0$ for $i \neq j$ .
Eq. (16): $g_i^T H_0 g_j = 0$ for $i \neq j$ and $g_i^T d_j = 0$ for $j < i$ .
The PCG with fixed preconditioner $H_0$ reaches the minimizer in at most $n$ steps.
SQN and this PCG produce identical iterates and directions at every step.

Significance

The result shows that storing only $m$ correction pairs costs nothing on quadratics: for any $m \ge 1$ , SQN terminates in at most $n$ steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small $m$ is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with $m$ : the matrix satisfies the secant equation on the $m$ most recent directions.

The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.

Difficulty

The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than $m$ steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, $x^T y$ is dotProduct, and $s y^T$ is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step $-g^T d / d^T A d$ . The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's $0/0 = 0$ ). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: $A \succ 0$ , $H_0 \succ 0$ , $m \ge 1$ and exact line searches. $H_0$ need not be diagonal.

Two misprints are corrected and flagged in the items: the denominator of $\beta$ in (13) is $y_{i-1}^T d_{i-1}$ (as in (12) and p. 778), and the second relation of (16) is stated for $j < i$ (as used on p. 778), since it fails for $i < j$ .

Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from $H_0$ and the last $m$ pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns $-A^{-1}b$ . The standing assumption $y_k^T s_k > 0$ is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With $m = 0$ SQN is steepest descent and the goal is false, so $m \ge 1$ is required.

Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that $n+1$ mutually $H_0$ -orthogonal vectors in $\mathbb{R}^n$ include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.

Selected references

J. Nocedal, Updating Quasi-Newton Matrices with Limited Storage, Mathematics of Computation 35(151), 1980, 773–782. https://doi.org/10.1090/s0025-5718-1980-0572855-7
D. F. Shanno, Conjugate gradient methods with inexact searches, Mathematics of Operations Research 3(3), 1978, 244–256. https://doi.org/10.1287/moor.3.3.244
L. Nazareth, A Relationship Between the BFGS and Conjugate Gradient Algorithms, ANL-AMD Tech. Memo 282 (rev.), Argonne National Laboratory, 1977 (reference [7] of Nocedal 1980; no online copy located).
T. G. Kolda, D. P. O'Leary, L. Nazareth, BFGS with update skipping and varying memory, SIAM Journal on Optimization 8(4), 1998, 1060–1083. https://doi.org/10.1137/S1052623496306450
D. C. Liu, J. Nocedal, On the limited memory BFGS method for large scale optimization, Mathematical Programming 45, 1989, 503–528. https://doi.org/10.1007/BF01589116

16 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Cubic Regularization of Newton Method and Its Global Performance I: Global Rate of Convergence to Second-Order Stationary PointsResearch Paper

Motivation

Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.

Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, $O(k^{-2/3})$ for the gradient norm, is better than the $O(k^{-1/2})$ of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that $O(\epsilon^{-3/2})$ iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.

This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.

Setting

Let $F \subseteq \mathbb{R}^n$ be a closed convex set with nonempty interior, and let $f$ be twice differentiable on $F$ with gradient $f'(x)$ and Hessian $f''(x)$ . A starting point $x_0 \in \operatorname{int} F$ is fixed, and $F$ is assumed to contain the level set $\mathcal{L}(f(x_0)) = \{x \in \mathbb{R}^n : f(x) \le f(x_0)\}$ in its interior. Assumption 1: the Hessian is Lipschitz continuous on $F$ in the spectral norm, $\|f''(x) - f''(y)\| \le L\|x - y\|$ for all $x, y \in F$ , with $L > 0$ .

For a parameter $M > 0$ the cubic model of $f$ at $x$ is

m_{M,x}(y) = \langle f'(x), y - x\rangle + \tfrac12 \langle f''(x)(y - x), y - x\rangle + \tfrac{M}{6}\|y - x\|^3 .

The cubic-regularized Newton step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb{R}^n$ ; it exists because the model is continuous and coercive. Write $r_M(x) = \|x - T_M(x)\|$ and $\bar f_M(x) = f(x) + \min_y m_{M,x}(y)$ .

The cubic regularization of Newton method (3.3) fixes $L_0 \in (0, L]$ , starts at $x_0$ and, for $k \ge 0$ , chooses $M_k \in [L_0, 2L]$ such that $f(T_{M_k}(x_k)) \le \bar f_{M_k}(x_k)$ , then sets $x_{k+1} = T_{M_k}(x_k)$ . The choice $M_k = L$ always passes the test.

Write $\lambda_n(A)$ for the smallest eigenvalue of a symmetric matrix $A$ . The measure of local optimality is

\mu_M(x) = \max\Big\{ \sqrt{\tfrac{2}{L + M}\,\|f'(x)\|},\ -\tfrac{2}{2L + M}\,\lambda_n(f''(x)) \Big\}.

It is nonnegative and vanishes exactly when $f'(x) = 0$ and $f''(x) \succeq 0$ .

Formalization targets

Goal: Theorem 1, inequality (3.4)

If $f(x) \ge f^*$ for all $x \in F$ , then every run of method (3.3) satisfies, for every $k \ge 1$ ,

\min_{1 \le i \le k} \mu_L(x_i) \le \frac{8}{3}\cdot\left(\frac{3\,(f(x_0) - f^*)}{2k\cdot L_0}\right)^{1/3}.

The constant $8/3$ and the exponent $1/3$ are the paper's; the statement holds for every admissible choice of the parameters $M_k$ and of the global minimizers $x_{k+1}$ .

Milestones, in attack order

Lemma 1 (2.2): $\|f'(y) - f'(x) - f''(x)(y - x)\| \le \tfrac12 L\|y - x\|^2$ on $F$ .
Eq. (2.5): $f'(x) + f''(x)(T - x) + \tfrac12 M\|T - x\|(T - x) = 0$ for $T = T_M(x)$ .
Proposition 1 (2.7): $f''(x) + \tfrac12 M r_M(x) I \succeq 0$ .
Lemma 2 (2.8): $\langle f'(x), x - T_M(x)\rangle \ge 0$ when $f(x) \le f(x_0)$ .
Lemma 4 (2.11): $f(x) - \bar f_M(x) \ge \tfrac{M}{12} r_M(x)^3$ .
Lemma 4 (2.12): for $M \ge L$ , $T_M(x) \in F$ and $f(T_M(x)) \le \bar f_M(x)$ .
Lemma 3 (2.9): $\|f'(T_M(x))\| \le \tfrac12(L + M) r_M(x)^2$ when $T_M(x) \in F$ .
Lemma 5: $\mu_M(T_M(x)) \le r_M(x)$ .
Theorem 1, first claim: $\sum_{i \ge 0} r_{M_i}(x_i)^3 \le \tfrac{12}{L_0}(f(x_0) - f^*)$ .
Theorem 1, second claim: $\lim_{i\to\infty} \mu_L(x_i) = 0$ .

Significance

Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, $\min_{1\le i\le k}\|f'(x_i)\| = O(k^{-2/3})$ , and the most negative curvature, $\max\{0, -\lambda_n(f''(x_i))\} = O(k^{-1/3})$ , along the best iterate, from a single scalar potential $f(x_0) - f^*$ . The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.

The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.

Difficulty

Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only $f''(x) + \tfrac12 M r I + \tfrac{M}{2r}(T - x)(T - x)^\top \succeq 0$ , which is weaker. The natural first attempt, "take the second-order optimality condition of the model at $T$ ", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.

The second is Lemma 2's second claim, used for (2.12): showing that $T_M(x)$ stays in $F$ requires a boundary argument along the segment from $x$ to $T_M(x)$ , since the Taylor bounds are only available inside $F$ . The remaining work is calculus in $\mathbb{R}^n$ : the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of $\mu$ .

Formalization scope

The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of $F$ this asks for two-sided derivatives, a mild strengthening of "twice differentiable on $F$ ". The Lipschitz condition uses the operator norm, which is the spectral norm. $T_M(x)$ is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes $\bar f_{M_k}(x_k)$ as $f(x_k)$ plus the model value at $x_{k+1}$ , which is the minimum because $x_{k+1}$ attains it. $\lambda_n$ is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound $f^*$ is required on $F$ only. The minimum over $1 \le i \le k$ is written as the existence of an index attaining the bound.

A stationary point of the cubic model is not an admissible step, and the run must keep the test $M_k \in [L_0, 2L]$ and the acceptance test. Replacing the step by any point with $f(x_{k+1}) \le f(x_k)$ makes the goal false, and dropping the square root in $\mu_M$ makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis $T_M(x) \in F$ , which its printed proof uses and which holds at every iterate.

A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.

Selected references

Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming, Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5
Y. Carmon, J. C. Duchi, O. Hinder and A. Sidford, Lower bounds for finding stationary points I, Mathematical Programming 184 (2020) 71–120. https://doi.org/10.1007/s10107-019-01406-y
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

16 thms3 active usersReviewed

Completed

Graph Theory·Captain: mikedeng1

Critical-Path Planning and Scheduling I: Critical Jobs Occur Only When the Completion Time Is the Earliest, and Then Form a Path from Origin to TerminusResearch Paper

Motivation

The Critical-Path Method (CPM) was introduced by J. E. Kelley, Jr. (Remington Rand) and M. R. Walker (du Pont) in Critical-Path Planning and Scheduling (Proc. Eastern Joint Computer Conference, 1959, pp. 160–173, doi:10.1145/1460299.1460318). Together with PERT, developed at the same time for the Polaris programme, it became the standard way to plan and schedule large projects in construction, maintenance and engineering, and it is taught in every introductory operations research course.

The paper reduces project scheduling to arithmetic on a directed acyclic graph: the earliest and latest times of the project's events are computed by two recursions, and the jobs whose timing has no slack, the critical jobs, are singled out by an equation. Its central structural claim is that critical jobs, when they exist, form a path from the start of the project to its end. The paper states this without proof ("a detailed development being reserved for a separate paper", p. 161). This mission formalizes that claim and the facts about the two recursions on which it rests.

Setting

A project network has $n+1$ events labelled $0,1,\dots,n$ with $n \ge 1$ : event $0$ is the origin and event $n$ the terminus. A job is an arrow from an event $i$ to an event $j$ , written job $(i,j)$ ; the jobs form a finite set $P$ of ordered pairs of events. Two standing assumptions of the paper (pp. 161–162) are part of the model:

every job has $i < j$ (events are labelled so that the head of an arrow has the larger label);
origin precedes and terminus follows every event: for every event $k$ there are chains of jobs from $0$ to $k$ and from $k$ to $n$ .

Each job has a real duration $y_{ij}$ . The earliest event times $t^{(0)}$ are given by display (1) of the paper,

t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,

and, for a project completion time $\lambda \ge t_n^{(0)}$ , the latest event times $t^{(1)}$ by display (2),

t_n^{(1)} = \lambda,\qquad t_i^{(1)} = \min\,[\,t_j^{(1)} - y_{ij} \mid i<j,\ (i,j)\in P\,],\quad 0\le i\le n-1.

The maximum time available for job $(i,j)$ is $t_j^{(1)} - t_i^{(0)}$ . The job is critical if this equals its duration, $t_j^{(1)} - t_i^{(0)} = y_{ij}$ , and a floater if it exceeds it. A critical path is a contiguous path of critical jobs from origin to terminus: events $0 = v_0, v_1, \dots, v_k = n$ with every $(v_{r-1}, v_r)$ a critical job of $P$ .

In the Lean development these are ProjectNetwork n (with field P), earliest N y, latest N y λ, maxTimeAvailable, IsCritical, IsFloater and IsCriticalPath, in the namespace CriticalPath.Events.

Formalization targets

Goal: critical jobs force $\lambda = t_n^{(0)}$ and a critical path (p. 163)

For every project network, durations $y$ and completion time $\lambda \ge t_n^{(0)}$ ,

\bigl(\exists (i,j)\in P,\ t_j^{(1)} - t_i^{(0)} = y_{ij}\bigr) \;\Longrightarrow\; \lambda = t_n^{(0)} \ \wedge\ \exists\ \text{a critical path}.

This is the paper's "A project will contain critical jobs only when $\lambda = t_n^{(0)}$ . If a project does contain critical jobs, then it also contains at least one contiguous path of critical jobs through the project diagram from origin to terminus." Only the "only when" direction is asserted, as on the page.

Milestones

Display (1), pp. 162–163. $t^{(0)}$ is the least vector $t$ with $t_0 = 0$ and $y_{ij} \le t_j - t_i$ for every job.
Display (2), p. 163. For $\lambda \ge t_n^{(0)}$ , $t_n^{(1)} = \lambda$ and $t^{(1)}$ is the greatest vector $t$ with $t_n \le \lambda$ and $y_{ij} \le t_j - t_i$ for every job.
Critical or floater, p. 163. For $\lambda \ge t_n^{(0)}$ , $t_i^{(0)} \le t_i^{(1)}$ for every event, and every job is critical or a floater: $t_j^{(1)} - t_i^{(0)} \ge y_{ij}$ .
Delay of a critical job, p. 163. Lengthening a critical job by $\delta \ge 0$ raises $t_n^{(0)}$ by exactly $\delta$ .

Significance

The result. The theorem is what makes the method's name meaningful: it says that the jobs without slack are not scattered but line up along an origin–terminus path, and that such jobs exist only when the project is scheduled at its earliest possible completion time. Project managers use this to decide which jobs to watch, which to expedite, and which may slip; the delay statement (milestone 4) is the quantitative form of that advice. The characterisations of (1) and (2) as least and greatest feasible schedules are the bridge between CPM and linear programming: they identify $t^{(0)}$ and $t^{(1)}$ with extreme solutions of the system of difference constraints $y_{ij} \le t_j - t_i$ , which the paper's own §3 uses to build the project cost curve.

Formalizing it. The results are classical and folklore, but the paper proves none of them, and textbook treatments usually define the critical path as a longest path, which makes the goal a tautology. This mission states the claims with the paper's own definitions: criticality by the float equation, event times by the recursions. To the best of current knowledge no machine-checked version of these statements for activity-on-arrow networks exists; the platform has a related activity-on-node development (Brucker and Knust, Complex Scheduling) in which the critical path is defined as a longest path.

Difficulty

The recursions (1) and (2) are local: each event looks only at its immediate predecessors or successors. The goal is global: from one critical job it asserts a statement about the whole completion time and a whole origin–terminus path. The float equation $t_j^{(1)} - t_i^{(0)} = y_{ij}$ mixes a quantity computed forward from the origin with one computed backward from the terminus, and neither recursion alone says anything about the other. The naive reading "a critical job lies on a longest path" is not available as a definition: it is, in substance, what has to be established from the recursions. The formal overhead is the well-founded recursion on the labels, in both directions, and the bookkeeping of lists of events forming a path.

Formalization scope

Events are Fin (n + 1), origin 0, terminus Fin.last n, with 1 ≤ n. Jobs are a Finset of ordered pairs, so there is at most one job per ordered pair. The standing assumptions (labels increase along jobs; origin precedes and terminus follows every event, via Relation.ReflTransGen) are fields of the structure ProjectNetwork and are never dropped. Durations and times are real numbers; durations are a function Fin (n+1) → Fin (n+1) → ℝ read only on jobs of P, with no sign condition, as in the paper's deterministic case.

The event times are defined by the recursions (1) and (2) themselves, by well-founded recursion on the label with Finset.sup'/Finset.inf' over the predecessor/successor set; these sets are nonempty by the standing assumptions, so no fallback value exists. The latest times are defined for every real $\lambda$ ; the paper's assumption $\lambda \ge t_n^{(0)}$ is a hypothesis of every theorem that uses them.

Disclosed readings: "earliest time occurance" (milestone 1) and "latest time … relative to a fixed project completion time" (milestone 2) are read as least and greatest vectors satisfying the job constraints $y_{ij} \le t_j - t_i$ (the paper's constraint (8), p. 165); milestone 3 is the fact implicit in the dichotomy "critical or floater"; "comparable delay" (milestone 4) is read as an exact delay of $\delta$ in $t_n^{(0)}$ for $\delta \ge 0$ .

A trivializing formalization is ruled out: defining a critical job or path through longest paths, or taking $t^{(0)}$ and $t^{(1)}$ as arbitrary functions satisfying (1) and (2), would make the goal a restatement of its definitions; here criticality is the float equation and the times are computed by the recursions. Dropping the reachability assumptions would make (2) ill-defined at events without successors.

Contributions welcome: proofs of the milestones, general lemmas on longest paths in finite labelled DAGs and on difference constraints $y_{ij} \le t_j - t_i$ , which are reusable for the companion mission on the project cost curve.

Selected references

J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Papers presented at the December 1–3, 1959, Eastern Joint IRE-AIEE-ACM Computer Conference, pp. 160–173, 1959. doi:10.1145/1460299.1460318
J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), pp. 296–320, 1961. doi:10.1287/opre.9.3.296
P. Brucker and S. Knust, Complex Scheduling, 2nd ed., Springer, 2012. doi:10.1007/978-3-642-23929-8

7 thms3 active usersReviewed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 4: First-Fit Decreasing Uses at Most 71/60 L* + 5 Bins When No Item Exceeds 1/2Research Paper

Motivation

Bin packing asks how to place a list of items with sizes in $(0,1]$ into as few unit-capacity bins as possible. It models the cutting of stock material, the packing of files onto tracks of a disc and the assignment of jobs to machines with a common deadline. Deciding the optimum is NP-hard, so in practice simple rules are used, and the question is how far they can stray from the optimum in the worst case.

Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3(4), 1974) gave the first sharp worst-case bounds for the four classical rules. For First-Fit Decreasing (FFD), the rule that sorts the items into nonincreasing order and then places each into the first bin with room, they announced the bound $FFD(L)\le\frac{11}{9}L^*+4$ , whose full proof in Johnson's thesis exceeds 75 pages. To show the method, Section 4 of the paper proves a simpler bound in detail: when no item exceeds $1/2$ , FFD uses at most $\frac{71}{60}L^*+5$ bins. That result is the subject of this mission.

Timeline:

1973: D. S. Johnson's MIT thesis, Near-optimal bin packing algorithms, contains the complete proofs of the $11/9$ and $71/60$ bounds.
1974: Johnson, Demers, Ullman, Garey and Graham publish the $71/60$ bound for lists in $(0,1/2]$ (Theorem 4.1) with a proof that is complete except for parts of two lemmas, and show by example that $71/60$ cannot be lowered.
1985: B. S. Baker gives a shorter proof of the $11/9$ bound for FFD (J. Algorithms 6, 1985).
2007: G. Dósa determines the tight additive constant $6/9$ in the $11/9$ bound (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$ ; values may repeat. A bin has capacity $1$ ; its level is the sum of the numbers in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed with no bin level exceeding $1$ .

First-Fit places $a_1,a_2,\dots$ in order into bins $B_1,B_2,\dots$ , each initially at level $0$ : $a_i$ goes into the bin of least index whose level $\beta$ satisfies $\beta\le 1-a_i$ . First-Fit Decreasing first arranges $L$ into nonincreasing order and then runs First-Fit. $FFD(L)$ is the number of bins it uses.

The proof uses a weight $W$ on finite sets of elements. For an integer $k\ge1$ , $x$ is a $k$ -piece if $x\in(\frac1{k+1},\frac1k]$ , and a $k$ -bin is a bin whose largest element is a $k$ -piece. Set $w_1(x)=\lfloor 1/x\rfloor^{-1}$ . A pair $(x,y)$ obeys relation $k$ if $x$ is a $k$ -piece and $kx+y\le1$ ; then $w_2(x,y)=w_1(x)+\frac{k-1}{k}w_1(y)$ , and otherwise $w_2(x,y)=w_1(x)+w_1(y)$ . For a partition $\pi$ of $X$ into one- and two-element sets, with each pair ordered (earlier, later) in the nonincreasing order,

w_{12}(\pi)=\sum_{\{x\}\in\pi}w_1(x)+\sum_{(x,y)\in\pi}w_2(x,y),\qquad W(X)=\min_\pi w_{12}(\pi).

BASIC is the set of elements of $L$ that are $k$ -pieces lying in a $k$ -bin of the FFD packing of $L$ , for some $k$ ; SURPLUS is the rest of $L$ .

Formalization targets

Goal: Theorem 4.1

\text{for every list } L\subseteq(0,\tfrac12]:\qquad FFD(L)\le\frac{71}{60}L^*+5 .

The constants are those printed in the paper. The multiplicative constant $71/60$ is best possible.

Milestones

Lemma 3.3 (FFD part): if $FFD(L)>rL^*+d$ with $r,d\ge1$ , the list $L'$ of the elements of $L$ exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$ .
Claim 4.2.1: for $N\ge4$ and $L\subseteq(\frac1N,\frac12]$ , $\sum_{x\in\mathrm{BASIC}}w_1(x)\ge FFD(L)-\sum_{j=2}^{N-1}\frac{j-1}{j}$ .
Claim 4.2.2: for $N\ge4$ , $L\subseteq(\frac1N,\frac12]$ and every partition $\pi$ of $L$ into one- and two-element sets, $w_{12}(\pi)\ge w_1(\mathrm{BASIC})-\sum_{j=3}^{N-1}\frac1j$ .
Lemma 4.2: for $N\ge4$ and $L\subseteq(\frac1N,\frac12]$ , $W(L)\ge FFD(L)-N+2$ .
Subadditivity: $W(X_1\cup\dots\cup X_k)\le\sum_i W(X_i)$ .
Lemma 4.3: if $X\subseteq(\frac17,\frac12]$ and $\sum_{x\in X}x\le1$ , then $W(X)\le\frac{71}{60}$ .

A companion item states the Remark after Theorem 4.1: for every $N\ge1$ there is a list with all elements below $1/3$ , $L^*=60N$ and $FFD(L)=71N$ .

Significance

Theorem 4.1 shows the weighting-function method in its simplest nontrivial form: a weight whose total is within a constant of the algorithm's bin count, and which no feasible bin can exceed by more than the target ratio. The same method, with more elaborate weights, gives the $11/9$ bound for FFD, and it is the model for later worst-case analyses of packing heuristics. The Remark shows that $71/60$ is exact for items in $(0,1/2]$ , and the Corollary on p. 322 extends the analysis to the asymptotic ratio $R^\alpha_{FFD}$ when items are bounded by $\alpha\in(8/29,1/2]$ .

The source proof is partial. The billing argument behind Claim 4.2.2 is given only when two auxiliary conditions (G1) and (G2) hold ("The more intricate argument here omitted", p. 321), and Lemma 4.3 is checked in four of about seventy-four cases ("leaving the remaining 70-odd, more or less routine, cases to the ambitious reader", p. 321). Complete details are in Johnson's thesis. The theorem itself is established. A formalization therefore gives the first complete, checked proof in a single place. The finite case analysis of Lemma 4.3 is well suited to machine checking. No machine-checked proof of any FFD bound is known to exist.

Difficulty

The obvious weight $w_1$ alone fails. Claim 4.2.1 shows that $w_1(\mathrm{BASIC})$ covers the FFD bins, but many sets $X$ of elements with sum at most $1$ have $w_1(X)>71/60$ , for example two $2$ -pieces, a $5$ -piece and a $6$ -piece. The pair discounts of $w_2$ repair Lemma 4.3, but they must then be paid for in Lemma 4.2, for every partition. That is Claim 4.2.2: a charge from each discounted pair to distinct SURPLUS elements that are no larger. The charge is straightforward only when no member of a pair obeying relation $k$ lies in a bin of type $k'<k$ . In general a pair's larger element may already have been charged by a smaller relation, and the paper omits the argument that handles this. Lemma 4.3 is elementary but has many cases, each determined by the piece types in $X$ and the relations they obey.

Formalization scope

A list is L : List ℝ with IsList L ( $0<a\le1$ for each element) in every statement. $L^*$ is optBins L, the least $b$ such that some map from positions to Fin b has every bin sum at most $1$ . The First-Fit run keeps the nonempty bins as a List (List ℝ), and opens a new bin at the end exactly when no existing bin fits, which is the paper's "least $j$ ". The fit test is $\beta+a\le1$ . FFD is First-Fit on sortDesc L, the mergeSort into nonincreasing order; ties do not affect the bin count. Indices are $0$ -based.

$W(X)$ sorts $X$ into nonincreasing order and minimises $w_{12}$ over the involutions of its positions: fixed points are singletons, and a pair $i<\sigma(i)$ is oriented (larger, smaller). The minimum is over a finite nonempty set, so it is attained. BASIC is a set of positions of sortDesc L, and each position's bin is its bin in the final FFD packing. In $w_2$ , $k=\lfloor1/x\rfloor$ is the piece type of the first element. Sums $\sum_{j=2}^{N-1}$ are over Finset.Icc 2 (N - 1) with $N\ge4$ .

The goal's range is $(0,1/2]$ . The restriction to $(1/7,1/2]$ belongs only to the proof, through Lemma 3.3. Stating the goal for $(1/7,1/2]$ , weakening $71/60$ or $5$ , or making $W$ an unattained infimum would each change the theorem. Only the FFD half of Lemma 3.3 is stated. Claim 4.2.1 is stated with Lemma 4.2's standing hypothesis $N\ge4$ . The Remark's printed range $0<\varepsilon\le5/87$ is a misprint: its FFD packing needs $\varepsilon<1/174$ , and the companion item states only the existence claim.

Infrastructure needed: a usable API for the First-Fit run (the invariants of the fold, bin levels, the order of bins), a lemma that FFD bins receive items in nonincreasing order, and a decision procedure for Lemma 4.3's case analysis over piece types. The model file and the weight file are reusable for the $11/9$ bound (mission 3 of this series) and for the bounded- $\alpha$ corollaries. Contributions of proofs of Lemma 4.3 by computer-checked case enumeration, and of the missing general case of Claim 4.2.2, are especially welcome.

Selected references

D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3(4):299–325, 1974. https://doi.org/10.1137/0203025
D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper).
B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, J. Algorithms 6, 1985.
G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, Lecture Notes in Computer Science 4614, 2007.

9 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Stochastic Systems·Captain: mikedeng1

Markov-Renewal Programming. I: Formulation, Finite Return Models: Policy Iteration Finds an Optimal Stationary Policy for the Discounted Infinite-Horizon Markov-Renewal ProgramResearch Paper

Motivation

Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.

Timeline:

1954: Lévy, Smith and Takács independently introduce Markov-renewal and semi-Markov processes; Pyke later surveys them.
1960: Howard, Dynamic Programming and Markov Processes, introduces policy iteration for finite discrete-time Markov decision processes.
1962: Blackwell, Discrete Dynamic Programming, shows that for the discounted discrete-time problem a stationary policy is optimal among all policies.
1963: Jewell formulates Markov-renewal programming, with a continuous discount factor α, and carries Howard's algorithm and Blackwell's stationarity result over to it. Part II of the paper treats the undiscounted (infinite-return) models.

Setting

A Markov-renewal program has a finite set of states $S$ (the paper's $i = 1, \dots, N$ ) and a finite, nonempty set of alternatives (the paper's $z = 1, \dots, Z$ ), each available in every state. For each alternative $z$ and states $i, j$ it specifies:

a transition probability $p^z_{ij} \ge 0$ , with $\sum_j p^z_{ij} = 1$ ;
a sojourn-time distribution $F^z_{ij}$ , the law of the time $\tau$ between entering $i$ and moving to $j$ , with $\tau \ge 0$ and $F^z_{ij}(0) = 0$ ;
for each continuous discount factor $\alpha > 0$ , a real number $\rho^z_{ij}(\alpha)$ , the expected discounted return earned during that transition.

The Laplace–Stieltjes transform $\tilde f^z_{ij}(s) = \int_0^\infty e^{-st}\,dF^z_{ij}(t)$ is the expected discount $\mathbb E[e^{-s\tau}]$ over one interval. The average one-step return is $\rho^z_i(\alpha) = \sum_j p^z_{ij}\rho^z_{ij}(\alpha)$ , and for a vector of returns $v$ the test quantity is

\rho^z_i(\alpha) + \sum_j p^z_{ij}\,\tilde f^z_{ij}(\alpha)\,v_j .

A stationary policy is a map $d : S \to A$ ; a nonstationary policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of such maps, $\pi_k$ being used at the $k$ -th transition. The $n$ -step return $V^\pi_i(n)$ of a policy, with boundary rewards $V_i(0,\alpha)$ , is the test quantity of $\pi_0(i)$ applied to the $(n-1)$ -step return of the shifted policy; the optimal $n$ -step return $V_i(n,\alpha)$ of equation (6) replaces $\pi_0(i)$ by a maximum over $z$ . The value-determination equations (15) of a stationary policy $d$ are $v_i = \rho^{d(i)}_i(\alpha) + \sum_j p^{d(i)}_{ij}\tilde f^{d(i)}_{ij}(\alpha) v_j$ .

The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.

Formalization targets

Goal (p. 947)

For every $\alpha > 0$ : (15) has a unique solution for every stationary policy, and every run $(d_k, v_k)$ of Fig. 1 reaches $d_{K+1} = d_K$ with $K < Z^N$ , where

\lim_{n\to\infty} V^{d_K}_i(n) = (v_K)_i,\qquad \lim_{n\to\infty} V^\pi_i(n) \le (v_K)_i \ \ \forall \pi,\qquad \lim_{n\to\infty} V_i(n,\alpha) = (v_K)_i ,

for every state $i$ and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".

Milestones

p. 945: $0 \le p^z_{ij}\tilde f^z_{ij}(s) < 1$ for $s > 0$ .
Claim (a): (15) has exactly one solution for each stationary policy.
Eq. (15): the $n$ -step return of a stationary policy converges to a solution of (15).
p. 946: $I - \tilde q(\alpha)$ is invertible and $([I-\tilde q(\alpha)]^{-1})_{ii} \ge 1$ .
Claim (b): a change of policy raises the return of some state and lowers none.
Claim (c): a policy reproduced by the improvement step is optimal among stationary policies.
Claim (d): a run of Fig. 1 terminates within $Z^N$ cycles.
Eq. (14): $V_i(n,\alpha)$ converges, independently of the boundary rewards, to a solution of $v_i = \max_z\{\rho^z_i(\alpha) + \sum_j p^z_{ij}\tilde f^z_{ij}(\alpha) v_j\}$ .
p. 946: some stationary policy's return dominates the limiting return of every nonstationary policy.

Significance

The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers $\tilde f^z_{ij}(\alpha)$ , so the same algorithm serves any sojourn-time law. For fixed $\alpha$ the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).

The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.

Difficulty

The discount over one transition, $\tilde f^z_{ij}(\alpha)$ , varies with $i$ , $j$ and $z$ , so the problem is not a constant- $\gamma$ contraction of textbook form; the relevant bound is that every row of $\tilde q(\alpha)$ sums to less than one, which rests on $F^z_{ij}(0) = 0$ . Entries in $[0, 1)$ alone, the paper's stated justification of Claim (a), do not make $I - \tilde q(\alpha)$ invertible: the $2 \times 2$ matrix with every entry $1/2$ has entries in $[0,1)$ , yet $I$ minus it is singular.

Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.

Formalization scope

States and alternatives are finite types; alternatives are nonempty. Every alternative is available in every state.
$F^z_{ij}$ is a probability measure on $\mathbb R$ with no mass on $(-\infty, 0]$ . The transform is integrated over $(0, \infty)$ , which carries all the mass.
The one-transition returns $\rho^z_{ij}(\alpha)$ are arbitrary real numbers, a generalization of the paper's Stieltjes integral (4), which is not formalized. The reward functions $R^z_{ij}(t\mid\tau)$ do not appear.
Returns of policies are defined by the one-step recursion (the policy form of (6)); the Markov-renewal process is not built as a stochastic process.
Policies are the paper's: deterministic and Markov, nonstationary ones indexed by the number of transitions made. Randomized and history-dependent policies are not in the comparison class.
The following informal words are read as follows. "Solve the set of simultaneous equations": (15) has exactly one solution. "Strictly increases the expected return of at least one state": no state's return decreases and one strictly increases, under the hypothesis that the policy changed. "No other policy can lead to higher expected returns" in Claim (c): no stationary policy. "Terminates in a finite number of cycles": two successive policies coincide at some cycle $K < Z^N$ . "If there is no improvement in the test quantity, retain the same alternative": the old alternative is kept whenever it attains the maximum. "Optimal" and "as good as any nonstationary policy": the limiting return of the returned policy dominates that of every policy from every state, for all boundary rewards. " $\lim_{n\to\infty} V_i(n,\alpha)$ ": the limit is proved to exist. " $\max_z$ ": a maximum over the finite nonempty set of alternatives.
Eq. (14) is printed with $v_i(\alpha)$ inside the sum over $j$ ; the formalization uses $v_j(\alpha)$ , as (6), (15) and Fig. 1 do.
Every statement fixes one $\alpha > 0$ . The undiscounted models (16)–(19), the finite-time and mixed-horizon models (9)–(13), and the infinite-time case of the stationarity result are out of scope.
The return of a policy is never defined through a matrix inverse, whose Mathlib value for a singular matrix is $0$ ; (15) is a predicate, and the goal asserts unique solvability, so a vacuous reading through junk inverses or assumed limits is excluded.

Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.

Selected references

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
W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2), 719–726, 1962. https://doi.org/10.1214/aoms/1177704593
R. Pyke, Markov Renewal Processes: Definitions and Preliminary Properties, Annals of Mathematical Statistics 32(4), 1231–1242, 1961. https://doi.org/10.1214/aoms/1177704863
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 7.2–7.3.

12 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis Optimization·Captain: mikedeng1

Methods of Conjugate Gradients for Solving Linear Systems II: Each Conjugate Gradient Step Shortens the Error VectorResearch Paper

Motivation

The conjugate gradient method (cg-method) of Hestenes and Stiefel is the standard iterative solver for linear systems $Ax=k$ with a symmetric positive definite matrix $A$ . It is used for the large sparse systems of finite-element and finite-difference discretizations, as the inner solver of Newton-type and interior-point methods in optimization, and as the prototype of the Krylov subspace methods. Its original 1952 paper (Hestenes and Stiefel, J. Res. NBS 49(6), 1952) already presented it as two things at once: a direct method that reaches the exact solution in at most $n$ steps, and a method of successive approximations whose intermediate estimates are useful in their own right.

The second view needs a guarantee that the intermediate estimates actually approach the solution. The method is built to decrease the $A$ -weighted error $f(x)=(h-x,A(h-x))$ , and the residual $|k-Ax_i|$ need not decrease (Section 18 of the paper, p. 432, notes that it can increase at every step). Theorem 6:3 of the paper supplies the guarantee in the plain Euclidean length: the distance $|h-x_i|$ from the estimate to the solution decreases strictly at every step, by an exactly computable amount. This mission formalizes that theorem together with the relations from Sections 5 and 6 of the paper on which its proof rests.

Timeline:

1952: Hestenes and Stiefel introduce the method and prove, in one paper, finite termination (Theorems 4:2 and 5:2), the monotone decrease of the error function $f$ (Theorem 6:1), and the monotone decrease of the Euclidean error (Theorem 6:3). The later literature on cg as an iterative method for large sparse systems takes these properties as its starting point.

Setting

Let $A$ be a real $n\times n$ matrix that is symmetric and positive definite, let $k\in\mathbb{R}^n$ , and let $h$ be the solution of $Ah=k$ . Write $(x,y)=x_1y_1+\cdots+x_ny_n$ and $|x|^2=(x,x)$ . From an arbitrary starting point $x_0$ , the cg-method (5:1) computes estimates $x_i$ , residuals $r_i$ and direction vectors $p_i$ by

p_0=r_0=k-Ax_0,\quad a_i=\frac{|r_i|^2}{(p_i,Ap_i)},\quad x_{i+1}=x_i+a_ip_i,\quad r_{i+1}=r_i-a_iAp_i,\quad b_i=\frac{|r_{i+1}|^2}{|r_i|^2},\quad p_{i+1}=r_{i+1}+b_ip_i .

The error vector of $x_i$ is $y_i=h-x_i$ . The error function (4:5) is $f(x)=(h-x,A(h-x))$ , which is nonnegative and vanishes only at $x=h$ . The Rayleigh quotient (4:12) of a vector $z\neq 0$ is $\mu(z)=(z,Az)/|z|^2$ . The Lean development names these cgIter A k x₀ i (with fields .x, .r, .p), cgAlpha for $a_i$ , errorFun A h x and rayleigh A z.

Formalization targets

Goal: Theorem 6:3

For every step that the method performs, that is, every $i$ with $r_i\neq 0$ ,

|y_i|^2-|y_{i+1}|^2=\frac{f(x_{i+1})+f(x_i)}{\mu(p_i)}\qquad\text{and}\qquad |y_{i+1}|<|y_i| .

The paper writes the step from $x_{i-1}$ to $x_i$ ; the Lean statement shifts the index by one. The goal holds for every dimension $n$ , every symmetric positive definite $A$ , every $k$ and every $x_0$ .

Milestones

Theorems 4:2 and 5:2: some $m\le n$ has $x_m=h$ .
Theorem 5:3, (5:6a): $(p_i,p_j)=|r_j|^2|p_i|^2/|r_i|^2$ for $i\le j$ .
Theorem 6:1, (6:1): $f(x_i)-f(x_{i+1})=a_i|r_i|^2=\mu(p_i)|x_i-x_{i+1}|^2$ .
Theorem 6:1, (6:2): $f(x_i)-f(x_j)=\sum_{l=i}^{j-1}a_l|r_l|^2$ for $i<j$ .
Section 6, (6:6): $(y_{i+1},x_{i+1}-x_i)=f(x_{i+1})/\mu(p_i)$ .

Significance

The theorem is what makes an early stop of the cg-method safe in the norm a user usually cares about. Every intermediate estimate is closer to the solution, in Euclidean distance, than the previous one, and the identity (6:5) states by how much. It also separates the cg-method from methods that minimize the residual: the $A$ -norm error, the Euclidean error and the residual behave differently, and only the first two are monotone along cg.

The results are proved in the 1952 paper. They have not been formalized: the Prove2Me library has no statement of the conjugate gradient recursion (5:1), and Mathlib has none either. What this mission adds is a machine-checked version of the paper's Section 6 argument for the recursion exactly as printed, including the case analysis at termination that the paper leaves implicit, and a reusable Lean definition of the cg iteration with its basic identities.

Difficulty

The obvious argument does not reach the conclusion. The method decreases $f(x)=(y,Ay)$ at every step, but a decrease in this $A$ -weighted norm does not imply a decrease in the Euclidean norm: for a single step along an arbitrary direction, even the best step for $f$ can lengthen the Euclidean error. So the theorem cannot be proved one step at a time from the local minimization property. It depends on how the current direction relates to all the later directions of the same run, and those relations in turn rest on the mutual orthogonality of the residuals and the conjugacy of the directions, which are established by an induction over the whole run.

A second difficulty is bookkeeping at the end of the run. The recursion divides by $|r_i|^2$ and by $(p_i,Ap_i)$ , which vanish after termination. Every milestone has to hold, or be guarded, past that point, and the goal needs the hypothesis $r_i\neq 0$ exactly because the strict inequality fails once $x_i=h$ .

Formalization scope

Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), $Ax$ is Matrix.mulVec (*ᵥ), and the standing assumption is A.PosDef, which in Mathlib includes symmetry. The solution $h$ is a variable with the hypothesis A *ᵥ h = k. Indices are 0-based. The cg recursion is the definition cgIter, which computes (5:1b)–(5:1f) literally and in order; it has no stopping rule, and Lean's convention $t/0=0$ makes it stay at $h$ with $r_i=p_i=0$ once $r_m=0$ . Lengths appear squared, as $(y,y)$ . The milestones are stated for every index without a termination guard, because both sides of each identity vanish after termination; only the goal carries $r_i\neq 0$ .

Two formalizations would trivialize the goal and are ruled out. The goal does not assume termination ( $x_m=h$ ) or any bound on $i$ : it quantifies over every cg run and every step that takes place. And it is about the Euclidean length $|h-x_i|$ , not the error function $f$ (that is Theorem 6:1, a different and weaker statement) and not the residual.

A complete development needs Theorem 5:1 (orthogonality of residuals, conjugacy of directions) for the literal recursion, the identities (5:2) and (5:3c), and the positivity of $(p,Ap)$ for $p\neq 0$ . These are reusable for any further work on the cg-method, including the sister mission on finite termination. Proofs of any milestone, and alternative proofs of Theorem 6:3 through the Krylov-subspace characterization, are welcome.

Selected references

M. R. Hestenes and E. Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, J. Res. Natl. Bur. Stand. 49(6), 409–436, 1952. https://doi.org/10.6028/jres.049.044 (publisher's scan: https://nvlpubs.nist.gov/nistpubs/jres/049/jresv49n6p409_A1b.pdf)

9 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis Optimization·Captain: mikedeng1

Methods of Conjugate Gradients for Solving Linear Systems I: Finite Termination of the Conjugate Gradient MethodResearch Paper

Motivation

Solving a linear system $Ax = k$ with a large symmetric positive definite matrix $A$ is a basic task of scientific computing: it arises from discretized elliptic equations, least-squares problems and the Newton steps of optimization methods. In 1952 Magnus Hestenes and Eduard Stiefel published the conjugate gradient method (cg-method) (J. Res. Natl. Bur. Stand. 49 (1952) 409–436). The method uses $A$ only through matrix–vector products and stores a few vectors. The paper's abstract states its central property in one sentence: "The solution is given in $n$ steps."

The paper obtains this property from a more general scheme, the method of conjugate directions (cd-method), which also contains Gaussian elimination as a special case. Its argument has two parts. Every cd-method with nonzero directions reaches the solution within $n$ steps (Theorem 4:2). The cg-method is a cd-method (Theorem 5:2), which follows from the orthogonality and conjugacy relations of Theorem 5:1. This mission formalizes that chain.

Setting

Vectors are real $n$ -tuples, with scalar product $(x, y) = x_1y_1 + \cdots + x_ny_n$ and squared length $|x|^2 = (x, x)$ . The matrix $A$ is real, $n \times n$ , symmetric and positive definite, which is the paper's standing assumption (p. 410). The solution $h$ satisfies $Ah = k$ . The residual of an estimate $x$ is $r = k - Ax$ . Two vectors $x, y$ are conjugate when $(x, Ay) = 0$ .

The cg-method (eq. (3:1), p. 411) starts from an arbitrary estimate $x_0$ and sets $p_0 = r_0 = k - Ax_0$ . Given $x_i$ , $r_i$ , $p_i$ , it computes

a_i = \frac{|r_i|^2}{(p_i, Ap_i)},\quad x_{i+1} = x_i + a_i p_i,\quad r_{i+1} = r_i - a_i Ap_i,\quad b_i = \frac{|r_{i+1}|^2}{|r_i|^2},\quad p_{i+1} = r_{i+1} + b_i p_i.

In Lean the iterates are cgIter A k x₀ i, a structure with fields x, r, p. The step length is cgA.

The cd-method (Section 4, p. 412) chooses an arbitrary first direction $p_0$ and then sets $x_{i+1} = x_i + a_i p_i$ with $a_i = (p_i, r_i)/(p_i, Ap_i)$ and $r_i = k - Ax_i$ . Each new direction $p_{i+1}$ may be any vector conjugate to $p_0, \dots, p_i$ . Because the directions are free, a cd-run is a property of sequences: IsCDRun A k x r p.

Formalization targets

Goal: finite termination of the cg-method

For every $n$ , every symmetric positive definite $A$ , every $k$ and $h$ with $Ah = k$ , and every initial estimate $x_0$ ,

\exists\, m \le n:\quad x_m = h,

where $x_m$ is the $m$ -th cg iterate. This is the statement of the abstract and of Section 3 (p. 410): "one will reach an estimate $x_m$ ( $m \le n$ ) at which $r_m = 0$ . This estimate is the desired solution $h$ ."

Milestones

Theorem 4:1 (p. 412). For every cd-run, the directions are mutually conjugate (4:3a). The residual $r_i$ is orthogonal to $p_0, \dots, p_{i-1}$ (4:3b). The products $(p_i, r_j)$ are the same for all $j \le i$ (4:3c). Hence $a_i = (p_i, r_0)/(p_i, Ap_i)$ (4:4).
Theorem 4:2 (p. 412). Every cd-run whose directions $p_0, \dots, p_{n-1}$ are nonzero has $x_m = h$ for some $m \le n$ .
Theorem 5:1 (p. 414), in four items. For the cg-method:
- (5:3a) $(r_i, r_j) = 0$ for $i \ne j$ ;
- (5:3b) $(p_i, Ap_j) = 0$ for $i \ne j$ ;
- (5:3c) $(p_i, r_j) = 0$ for $i < j$ and $(p_i, r_j) = |r_i|^2$ for $i \ge j$ ;
- (5:3d) $(r_i, Ap_i) = (p_i, Ap_i)$ , and $(r_i, Ap_j) = 0$ for $i \ne j, j + 1$ .
Theorem 5:5, eq. (5:10) (p. 416):

a_i = \frac{|r_i|^2}{(p_i, Ap_i)} = \frac{(p_i, r_i)}{(p_i, Ap_i)} = \frac{(p_i, r_0)}{(p_i, Ap_i)}.

Theorem 5:2, first sentence (p. 415). The cg-method is a cd-method: its iterates satisfy IsCDRun.

Significance

Finite termination is the property that distinguishes the conjugate gradient method from stationary iterations such as Jacobi or Gauss–Seidel. It explains why the method can be used as a direct solver in exact arithmetic. It is the starting point for the later theory of Krylov subspace methods. The relations of Theorem 5:1 are the checks the paper recommends for monitoring a computation (eq. (3:3)). They are also the input to the paper's further results on the monotone decrease of the error (Section 6) and on the connection with orthogonal polynomials (Sections 14–18).

The result has been proved since 1952 and appears in every numerical linear algebra textbook. As far as a search of the Prove2Me catalog shows (September 2026), it has no machine-checked proof there. The only conjugate gradient material on the platform is a Hilbert-space convergence result for a different recurrence. This mission adds a faithful formal version of the original recursion (3:1) and of the cd-method. It also adds the complete termination argument, organized as in the paper. The definitions and the Theorem 5:1 relations are reusable by any later formalization of Krylov methods, including the second mission of this series on the decrease of the error $|h - x_i|$ .

Difficulty

The obvious argument says that the residuals are mutually orthogonal, so at most $n$ of them are nonzero. That argument is only as good as the orthogonality, and Theorem 5:1 must be established by a simultaneous induction over four families of relations. The recursion defines $r_{i+1}$ by an update, not as $k - Ax_{i+1}$ , so even $r_i = k - Ax_i$ needs a proof. Orthogonality of $r_{i+1}$ to the earlier residuals needs the conjugacy of the earlier directions, and conjugacy of $p_{i+1}$ needs the orthogonality of the earlier residuals. Neither family can be proved first.

A second obstacle is the passage from orthogonality to termination. A cd-run with a zero direction stalls, so Theorem 4:2 needs the directions $p_0, \dots, p_{n-1}$ to be nonzero. The cg directions become zero exactly when the solution is reached, so applying Theorem 4:2 to cg needs a case split at the first vanishing residual.

Formalization scope

Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), and $Ax$ is Matrix.mulVec (*ᵥ). The hypothesis on $A$ is Mathlib's Matrix.PosDef, which includes symmetry. The solution enters only through the hypothesis A *ᵥ h = k. Indices are 0-based, as in the paper.

The cg iteration is total and has no stopping test. Once $r_m = 0$ , Lean's convention $x/0 = 0$ gives $p_m = 0$ and $a_m = 0$ . From then on the iteration stays at $x_m$ , with zero residuals and directions. For this reason the relations of Theorem 5:1 are stated for all indices without guards: after termination they hold trivially.

Two formulations would make the goal trivial, and neither is used. One is a stopping test or step that refers to $h$ or to $A^{-1}k$ . The other replaces (3:1b), (3:1d) or (3:1e) by the equivalent formulas (3:2a), (3:2b) or $r_{i+1} = k - Ax_{i+1}$ , which would move Theorem 5:5 and part of Theorem 5:2 into the definition. The iteration is (3:1) literally.

The cd-method's implicit hypothesis, that the directions $p_0, \dots, p_{n-1}$ are nonzero, is an explicit binder of Theorem 4:2. Without it the statement fails (take $p_0 = 0$ ). The hypothesis is satisfiable: the cg run with nonzero residuals is one example.

A complete development needs the standard facts that mutually conjugate nonzero vectors are linearly independent and that $n$ independent vectors span $\mathbb{R}^n$ . It also needs the induction behind Theorem 5:1. Contributions welcome beyond the milestones include the converse half of Theorem 5:2, the relation (5:2) expressing $p_k$ through $r_0, \dots, r_k$ , and Theorem 4:5 (the cd-method computes $A^{-1}$ ).

Selected references

M. R. Hestenes and E. Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, Journal of Research of the National Bureau of Standards 49(6), 409–436, 1952. https://doi.org/10.6028/jres.049.044
L. Fox, H. D. Huskey and J. H. Wilkinson, Notes on the solution of algebraic linear simultaneous equations, Quarterly Journal of Mechanics and Applied Mathematics 1(1), 149–173, 1948 (the cd-method from a different point of view; cited in the paper's Section 4 footnote). https://doi.org/10.1093/qjmam/1.1.149
G. H. Golub and C. F. Van Loan, Matrix Computations, 4th ed., Johns Hopkins University Press, 2013, §11.3 (textbook account of the method).

11 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Logarithmic Regret Algorithms for Online Convex Optimization 4: Logarithmic Regret of Exponentially Weighted Online OptimizationResearch Paper

Motivation

In online convex optimization a player repeatedly chooses a point $x_t$ from a convex set $P \subseteq \mathbb{R}^n$ , after which an adversary reveals a convex cost function $f_t$ and the player pays $f_t(x_t)$ . The player's regret after $T$ rounds is its total cost minus the cost of the best fixed point in hindsight. The model covers online portfolio selection, online regression and prediction with expert advice, and it underlies the analysis of stochastic and adaptive optimization methods (Zinkevich 2003; Cesa-Bianchi and Lugosi 2006).

For general convex costs the best achievable regret is of order $\sqrt{T}$ . Hazan, Agarwal and Kale (Mach Learn 69, 2007) showed that a curvature condition, $\alpha$ -exp-concavity, brings the regret down to order $\log T$ , and gave several algorithms that achieve it. This mission concerns the simplest of them, Exponentially Weighted Online Optimization (EWOO), which needs nothing beyond exp-concavity: no bound on gradients and no bound on the diameter of $P$ .

Timeline.

1991: Cover's universal portfolio algorithm attains regret $O(n \log T)$ for online portfolio selection, whose log-loss is $1$ -exp-concave (Cover 1991).
1997: Blum and Kalai give a short analysis of the universal portfolio with transaction costs, using a shrinking argument around the best portfolio (Blum and Kalai 1997/1999).
2003: Kalai and Vempala give a polynomial-time randomized implementation of Cover's algorithm via random walks (JMLR 3, 2003).
2007: Hazan, Agarwal and Kale state EWOO for general $\alpha$ -exp-concave costs and prove the regret bound of Theorem 7, alongside the Online Newton Step and Follow the Approximate Leader.

Setting

Fix $n \ge 0$ and a set $P \subseteq \mathbb{R}^n$ that is nonempty, closed, bounded and convex, with positive Lebesgue volume $\mathrm{vol}(P)$ . Fix $\alpha > 0$ . The cost functions are $f_1, f_2, \dots : \mathbb{R}^n \to \mathbb{R}$ , each continuous on $P$ and $\alpha$ -exp-concave on $P$ : the function $h_t(x) = e^{-\alpha f_t(x)}$ is concave on $P$ (LogRegretOCO.EWOO.IsExpConcave).

EWOO keeps the weights

w_t(x) = \exp\Bigl(-\alpha \sum_{\tau=1}^{t-1} f_\tau(x)\Bigr) = \prod_{\tau=1}^{t-1} h_\tau(x),

and on round $t$ plays the $w_t$ -weighted mean of $P$ ,

x_t = \frac{\int_P x\, w_t(x)\, dx}{\int_P w_t(x)\, dx}

(LogRegretOCO.EWOO.ewooPoint). In particular $x_1$ is the centroid of $P$ , and each $x_t$ depends only on $f_1, \dots, f_{t-1}$ . The regret against a comparator $u \in P$ is $\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr)$ .

Formalization targets

Goal: Theorem 7

For every $T \ge 1$ and every $u \in P$ ,

\sum_{t=1}^{T} f_t(x_t) - \sum_{t=1}^{T} f_t(u) \;\le\; \frac{1}{\alpha}\, n\, \bigl(1 + \log(T+1)\bigr).

This is the paper's printed constant. The paper's proof yields the slightly sharper $\frac{1}{\alpha}\bigl(1 + n\log(T+1)\bigr)$ ; the printed form is the goal.

Milestones

The proof in §3.4 (p. 187) passes through five displays, each a milestone:

Jensen for the weighted mean (first display on p. 187): $h_t(x_t) \ge \int_P h_t\, w_t \,/ \int_P w_t$ .
Eq. (18): $\prod_{\tau=1}^t h_\tau(x_\tau) \ge \int_P \prod_{\tau=1}^t h_\tau \,/\, \mathrm{vol}(P)$ .
The nearby set $S = \{\frac{T}{T+1}x^* + \frac{1}{T+1}y : y \in P\}$ : for $x \in S$ , $h_t(x) \ge \frac{T}{T+1}h_t(x^*)$ and $\prod_{\tau=1}^T h_\tau(x) \ge \frac1e \prod_{\tau=1}^T h_\tau(x^*)$ .
Volume of $S$ : $\mathrm{vol}(S) = \mathrm{vol}(P)/(T+1)^n$ .
Multiplicative regret bound (last display on p. 187): $\prod_{\tau=1}^T h_\tau(x_\tau) \ge \frac{1}{e(T+1)^n}\prod_{\tau=1}^T h_\tau(x^*)$ .

Significance

The result. Theorem 7 shows that exp-concavity alone suffices for logarithmic regret, with a constant $n/\alpha$ that does not depend on the size of $P$ or on the gradients of the costs. Specialised to the log-loss $f_t(x) = -\log(r_t^\top x)$ on the simplex, where $\alpha = 1$ , it recovers the $O(n\log T)$ regret of Cover's universal portfolio. The bound is the benchmark against which the computationally cheaper second-order methods of the same paper (Online Newton Step, Follow the Approximate Leader) are compared: those need a gradient bound $G$ and diameter $D$ and pay a factor $(1/\alpha + GD)$ .

Formalizing it. The theorem is proved in the paper, and a textbook version with a different constant, $(n/\alpha)\log T + 2/\alpha$ , appears in Hazan's Introduction to Online Convex Optimization (Theorem 4.4). No machine-checked proof of either is known. The work here is to formalize the paper's proof: Jensen's inequality for a weighted Lebesgue average in $\mathbb{R}^n$ , the change of volume under homothety, and the elementary inequality $(1 + 1/T)^T \le e$ . A companion draft of the textbook version exists on the platform as a private item (OnlineConvexOpt.SecondOrder.ewoo_regret) with another constant; it is not reused.

Difficulty

The pieces are classical, but they have to be assembled in measure-theoretic form. The point $x_t$ is a Bochner integral of a vector-valued function over $P$ , and its membership in $P$ and the Jensen inequality both require the normalised weight $w_t\,dx/\int_P w_t$ to be a genuine probability measure on $P$ , with every integrand integrable. The obvious one-dimensional intuition — "the weighted mean of a convex set lies in the set" — hides the requirement that $P$ be closed and have positive volume.

The second obstacle is that Eq. (18) compares the algorithm with an average of the product $\prod h_\tau$ over all of $P$ , while the regret compares it with a single point. The natural attempt, bounding the average below by the value at the comparator, fails: the average can be far smaller than the maximum, and a lower bound that loses more than a factor polynomial in $T$ destroys the logarithmic rate. Controlling this loss in $n$ dimensions, with a constant independent of the shape and size of $P$ , is the heart of the argument.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n) with its Lebesgue (Haar) measure volume. Rounds are numbered from $1$ : the weights sum over Finset.Ico 1 t, the regret over Finset.Icc 1 T. Cost functions are defined on all of $\mathbb{R}^n$ ; only their values on $P$ enter. The algorithm is the total function ewooPoint P α f t, and the goal is stated for $x_t$ equal to it — not for an arbitrary sequence satisfying a Jensen-type inequality.

Conventions and corrections relative to the printed text:

Regret against every comparator. The regret is stated as $\sum_t (f_t(x_t) - f_t(u)) \le$ bound for every $u \in P$ , never through a real-valued ⨅ or sInf over $P$ , which in Lean would return a junk value off its intended domain and trivialize the statement.
Positive volume volume P ≠ 0 is added: the algorithm divides by $\int_P w_t$ , which the paper leaves implicit. Without it Lean's convention $0^{-1} = 0$ would set $x_t = 0$ .
Continuity of each $f_t$ on $P$ is the paper's standing assumption (§2.2: costs twice differentiable and convex) weakened to what the argument uses; it makes every integral in the development an integral of an integrable function.
Typos. Theorem 7's " $f_t : P \to \mathbb{R}^n$ " is read as real-valued, and its " $\exp(-\alpha f(x))$ " as $\exp(-\alpha f_t(x))$ . The set-builder " $S = \{x \in S \mid \dots\}$ " defines $S$ in terms of itself and is read as the set of all $\frac{T}{T+1}x^* + \frac{1}{T+1}y$ , $y \in P$ ; the printed " $S = x^* + \frac{1}{T+1}P$ " is a translate of that set with the same volume.
Comparator. The paper's $x^*$ is a minimizer of $\sum_t f_t$ ; milestones 3 and 5 are stated for every $x^* \in P$ , which implies the minimizer case.
Constant. The printed $\frac{1}{\alpha}n(1+\log(T+1))$ is stated, although the proof gives the sharper $\frac{1}{\alpha}(1 + n\log(T+1))$ .
Not in scope. The randomized variant (sampling $x_t$ with density proportional to $w_t$ , "in expectation") and the running-time discussion of §3.4.1 have no separate proof in the paper.

Infrastructure that a complete development needs, and that is reusable beyond this mission: Jensen's inequality for concave functions under a probability measure with a continuous density on a compact convex set (Mathlib has ConcaveOn.le_map_integral and Convex.integral_mem); the scaling identity for Haar measure (MeasureTheory.Measure.addHaar_smul); and the elementary bound $(T/(T+1))^T \ge 1/e$ . Proofs of any milestone, and a general weighted-Jensen lemma usable across the milestones, are welcome.

Selected references

E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
A. Blum, A. Kalai, Universal portfolios with and without transaction costs, Machine Learning 35 (1999), 193–205 (COLT 1997). https://doi.org/10.1023/A:1007530728748
A. Kalai, S. Vempala, Efficient algorithms for universal portfolios, Journal of Machine Learning Research 3 (2003), 423–440. https://www.jmlr.org/papers/v3/kalai02a.html
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022; arXiv:1909.05207, Theorem 4.4. https://arxiv.org/abs/1909.05207

9 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Logarithmic Regret Algorithms for Online Convex Optimization 3: Logarithmic Regret of Follow the Approximate LeaderResearch Paper

Motivation

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

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

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

Setting

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

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

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

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

Formalization targets

Goal: Theorem 6

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Corrections and conventions relative to the printed paper:

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

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

Selected references

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

9 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Logarithmic Regret Algorithms for Online Convex Optimization 2: Logarithmic Regret of the Online Newton StepResearch Paper

Motivation

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

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

Timeline:

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

Setting

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

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

The Online Newton Step fixes

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

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

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

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

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

Formalization targets

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

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

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

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

Milestones

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Corrections and added hypotheses:

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

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

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

Selected references

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

8 thms3 active usersReviewed

Optimization Probability·Captain: mikedeng1

Optimizing Strategic Safety Stock Placement in Supply Chains: Binding Base Stocks Are Optimal in a Serial System without Guaranteed Internal ServiceResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: the Result, Eq. (A6)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

The page's informal words are read as follows:

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

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

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

Selected references

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

9 thms3 active usersReviewed

Completed

Combinatorics Optimization Probability+1·Captain: mikedeng1

Maximizing Non-Monotone Submodular Functions I: A Uniformly Random Set Achieves 1/4 of the Optimum, and 1/2 for Symmetric FunctionsResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2.1

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

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

and if $f$ is in addition symmetric,

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

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

Milestones

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

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

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

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

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

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

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

Significance

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

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

Difficulty

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

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

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

Formalization scope

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

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

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

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

Selected references

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

8 thms3 active usersReviewed

Completed

Linear Optimization Optimal Transport·Captain: mikedeng1

Scenario Reduction in Stochastic Programming: The Optimal Redistribution Rule and the Explicit Kantorovich Distance of a Reduced MeasureResearch Paper

Motivation

Stochastic programs are solved in practice on a finite set of scenarios: a discrete probability distribution $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ that approximates the true distribution of the uncertain data. The size of the resulting deterministic problem grows with $N$ , and for multistage models it grows very fast, so $N$ is often reduced before solving. The question is which scenarios to delete and how to reweight the remaining ones so that the optimal value and solutions of the stochastic program change as little as possible.

Dupačová, Gröwe-Kuska and Römisch (Math. Program. Ser. A 95 (2003) 493–511) answered this with probability metrics. Stability results for stochastic programs bound the change of the optimal value by a Fortet–Mourier type distance, which is in turn bounded by a Kantorovich functional $\hat\mu_c$ (an optimal transport cost). Scenario reduction then becomes: find a measure $Q$ supported on a subset of the scenarios with $\hat\mu_c(P,Q)$ small. Section 3 of the paper solves the weight part of this problem in closed form. That result, together with the heuristics built on it (backward reduction and forward selection), became the standard scenario-reduction method, implemented for example in the GAMS tool SCENRED.

Setting

Let $\Omega$ be a set and $c:\Omega\times\Omega\to\mathbb R_+$ a cost function with $c(\omega,\tilde\omega)=0$ if and only if $\omega=\tilde\omega$ , and $c(\omega,\tilde\omega)=c(\tilde\omega,\omega)$ (conditions (C1)–(C2), p. 498). The original distribution has scenarios $\omega_1,\dots,\omega_N\in\Omega$ with weights $p_i>0$ and $\sum_i p_i=1$ . Write $c_{ij}=c(\omega_i,\omega_j)$ .

A set $J\subset\{1,\dots,N\}$ of scenarios is deleted. The reduced measure is $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$ with reduced weights $q_j\ge0$ , $\sum_{j\notin J}q_j=1$ . A transport plan from $P$ to $Q$ is a nonnegative matrix $(\eta_{ij})_{i\le N,\,j\notin J}$ with row sums $\sum_{j\notin J}\eta_{ij}=p_i$ and column sums $\sum_i\eta_{ij}=q_j$ . The Kantorovich functional (10) is the value of this transportation problem,

D(J;q)=\min\Big\{\sum_{i}\sum_{j\notin J}c_{ij}\eta_{ij}:\ \eta\ \text{a transport plan from }P\text{ to }Q\Big\},

and $D_J=\min\{D(J;q): q\ \text{reduced weights}\}$ is the best distance achievable once $J$ is fixed. The optimal deletion problem (13) asks for $\min\{D_J:\#J=k\}$ for a given $1\le k<N$ .

In the Lean development these objects are IsReducedWeight, IsTransportPlan, transportCost, transportValue ( $D(J;q)$ ), optWeightsValue ( $D_J$ ) and optimalDeletionValue (the value of (13)), all in the namespace ScenarioReduction.Redistribution.

Formalization targets

Goal: Theorem 2 (optimal weights), p. 500

For every $J\neq\{1,\dots,N\}$ ,

D_J=\min\Big\{D(J;q): q_j\ge0,\ \sum_{j\notin J}q_j=1\Big\}=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j),

and the minimum is attained at the optimal redistribution rule $\bar q_j=p_j+\sum_{i\in J_j}p_i$ , where $J_j=\{i\in J: j(i)=j\}$ and $j(i)\in\arg\min_{j\notin J}c(\omega_i,\omega_j)$ , for every such choice of $j(\cdot)$ .

Milestones

Primal–dual representation of $D(J;q)$ (first display of the proof, p. 501): the transportation problem and its linear-programming dual both attain $D(J;q)$ .
Lower bound (p. 501): $\sum_{i\in J}p_i\min_{k\notin J}c_{ik}\le D(J;q)$ for every feasible $q$ .
Upper bound at $\bar q$ (p. 501): $\bar q$ is feasible and $D(J;\bar q)\le\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$ .
Theorem 3 (p. 501): for weights prescribed by $q_j=p_j+\lambda_jp_J$ , $D(J;q)\le\sum_{i\in J}p_i\sum_{j\notin J}\lambda_jc(\omega_i,\omega_j)$ , with equality if $\#J=1$ and $c$ satisfies the triangle inequality.
Theorem 4 (p. 503): the greedy recursions (16) and (17) give a lower and an upper bound for $\min\{D_J:\#J=k\}$ , and the backward set $\{l_1,\dots,l_k\}$ is optimal under a nonemptiness condition.

Significance

Theorem 2 reduces the continuous part of scenario reduction to a formula: once the set of kept scenarios is chosen, the best reweighting is to move the mass of every deleted scenario to a nearest kept scenario, and the resulting distance is an explicit sum. This leaves only the combinatorial choice of $J$ , which Theorem 4 brackets by two greedy procedures; these are the backward-reduction and forward-selection algorithms of the paper and of later work by Heitsch and Römisch. Theorem 3 covers the case in which the reduced weights are fixed by the modeller, for instance to keep a uniform distribution uniform.

The results are proved in the paper by elementary linear-programming arguments. As far as is known, none of them has a machine-checked proof. Formalizing them produces a verified finite transportation-problem layer with a general (not necessarily metric) cost and a deleted index set, and verified correctness certificates for the two standard scenario-reduction heuristics.

Difficulty

The upper bound of Theorem 2 is a direct construction. The content lies in the lower bound, which must hold for every reweighting $q$ simultaneously; this needs the dual side of the transportation problem, and the full primal–dual representation (Milestone 1) requires strong duality for a transportation problem with only the kept columns, which Mathlib does not provide in this form. A naive argument that bounds each plan row by row gives the lower bound directly for plans, but relating it to $D(J;q)$ as an infimum also requires that plans exist and that the infimum is attained. In Theorem 4, the recursions (16) and (17) are greedy and do not in general produce optimal sets; the lower bound works only because its inner minimum ranges over all $j\neq l$ , not over the kept scenarios.

Formalization scope

Scenarios are indexed by Fin N (0-based), scenarios are a function ω : Fin N → Ω into an arbitrary type Ω, the cost is c : Ω → Ω → ℝ, and weights, plans and dual variables are real-valued functions on Fin N and Fin N × Fin N. Only the entries at kept indices $j\notin J$ enter any constraint, cost or objective. No measure theory is used: the index-level transportation problem is the paper's own representation of $\hat\mu_c$ for discrete measures (p. 495). Every theorem carries the standing assumptions of Section 3: $c\ge0$ , (C1), (C2), $p_i>0$ and $\sum_ip_i=1$ . Measurability of $c$ and conditions (C3) and (C4) concern $\Omega\subset\mathbb R^s$ and play no role for finitely supported measures; they are dropped, so the statements are more general than the page. The hypothesis $J\neq\{1,\dots,N\}$ , implicit in Theorem 2, is stated explicitly; in Theorem 4, $1\le k<N$ plays this role.

$D(J;q)$ and $D_J$ are real infima (sInf) of transport costs and are only asserted about where the underlying sets are nonempty and bounded below; "min" is stated as attainment (IsLeast), not as an equality of infima. $D(J;q)$ is defined as the transportation problem and is not defined by the closed form $\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$ ; under that definition Theorem 2 would be trivial, and it is ruled out here. Likewise the reduced-weight constraint does not force $q=\bar q$ .

Needed infrastructure: finite transportation problems with nonnegativity and marginal constraints, existence of optimal plans (compactness of the feasible polytope), and LP duality for transportation problems. The transportation-problem layer is reusable beyond this mission. Contributions welcome: proofs of the milestones, a general strong-duality result for finite transportation problems, and the examples of p. 502 (single scenario deletion, keeping one scenario).

Selected references

J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Math. Program. Ser. A 95 (2003) 493–511. https://doi.org/10.1007/s10107-002-0331-0
S. T. Rachev, Probability Metrics and the Stability of Stochastic Models, Wiley, 1991.
H. Heitsch, W. Römisch, Scenario reduction algorithms in stochastic programming, Comput. Optim. Appl. 24 (2003) 187–206. https://doi.org/10.1023/A:1021805924152
W. Römisch, R. Schultz, Stability analysis for stochastic programs, Ann. Oper. Res. 30 (1991) 241–266. https://doi.org/10.1007/BF02204819

7 thms3 active usersReviewed

Algorithmic Game Theory Topology·Captain: mikedeng1

A Social Equilibrium Existence Theorem: Equilibrium Points Exist When Actions Are Contractible Polyhedra and Constrained Best Responses Are ContractibleResearch Paper

Motivation

Nash's equilibrium existence theorem assumes that each player's set of available strategies is fixed. Many social and economic systems do not work that way: a consumer's budget set depends on prices, which are the choices of another agent, and a firm's feasible production may depend on what other firms do. Gerard Debreu's A Social Equilibrium Existence Theorem (PNAS 38(10), 1952) proves that an equilibrium exists in such a system, called a social system or abstract economy (today also a generalized game). Here each agent's feasible actions depend on the actions of all the others.

Arrow and Debreu used this theorem to prove the existence of a competitive equilibrium (Econometrica 22(3), 1954). It is the standard existence result for generalized Nash equilibrium problems in operations research, where the feasible sets are coupled by shared constraints.

Timeline.

1928: von Neumann proves the minimax theorem for matrix games.
1941: Kakutani proves a fixed-point theorem for convex-valued maps with closed graphs on compact convex sets (Duke Math. J. 8, 1941).
1946: Eilenberg and Montgomery extend fixed-point theory to acyclic-valued maps on acyclic absolute neighbourhood retracts (Amer. J. Math. 68, 1946).
1950: Nash proves the existence of equilibrium points for finite games (PNAS 36, 1950).
1952: Debreu proves the theorem of this mission. He requires contractibility instead of convexity, and his payoffs take values in the completed real line.

Setting

There are finitely many agents $\iota=1,\dots,\nu$ . Agent $\iota$ chooses an action $a_\iota$ in a set $\mathfrak A_\iota$ , a subset of a finite-dimensional real space. A profile $a=(a_1,\dots,a_\nu)$ lies in $\mathfrak A=\mathfrak A_1\times\cdots\times\mathfrak A_\nu$ . For each agent, $\bar a_\iota$ denotes the actions of the others, ranging over $\bar{\mathfrak A}_\iota=\prod_{j\ne\iota}\mathfrak A_j$ .

Given $\bar a_\iota$ , agent $\iota$ may only choose from a nonempty set $A_\iota(\bar a_\iota)\subseteq\mathfrak A_\iota$ , a multi-valued function of the others' actions. Its graph is $G_\iota=\{(\bar a_\iota,a_\iota)\mid a_\iota\in A_\iota(\bar a_\iota)\}$ . The payoff $f_\iota(\bar a_\iota,a_\iota)$ takes values in the completed real line $\overline{\mathbb R}=\mathbb R\cup\{-\infty,+\infty\}$ . The best value available to agent $\iota$ and the set of constrained best responses are

\varphi_\iota(\bar a_\iota)=\max_{a_\iota\in A_\iota(\bar a_\iota)}f_\iota(\bar a_\iota,a_\iota),\qquad M_{\bar a_\iota}=\{a_\iota\in A_\iota(\bar a_\iota)\mid f_\iota(\bar a_\iota,a_\iota)=\varphi_\iota(\bar a_\iota)\}.

An equilibrium point is a profile $a^*$ such that, for every $\iota$ , $a^*_\iota\in A_\iota(\bar a^*_\iota)$ and $f_\iota(a^*)=\varphi_\iota(\bar a^*_\iota)$ .

The topological vocabulary is Debreu's §1:

a convex cell is the convex hull of finitely many points;
a geometric polyhedron is a finite union of convex cells;
a polyhedron is a set homeomorphic to a geometric polyhedron;
a nonempty set $Z$ is contractible if there is a continuous $H:[0,1]\times Z\to Z$ with $H(0,z)=z$ and $H(1,z)=z^0$ for a fixed $z^0\in Z$ .

A multi-valued function is semicontinuous if its graph is closed.

Formalization targets

Goal: the THEOREM (p. 888)

Assume that for every $\iota$ , $\mathfrak A_\iota$ is a contractible polyhedron, $G_\iota$ is closed, $f_\iota$ is continuous on $G_\iota$ , $\varphi_\iota$ is continuous on $\bar{\mathfrak A}_\iota$ , and $M_{\bar a_\iota}$ is contractible for every $\bar a_\iota$ . Then

\exists\,a^*\in\mathfrak A\ \ \forall\iota:\quad a^*_\iota\in A_\iota(\bar a^*_\iota)\ \text{ and }\ f_\iota(\bar a^*_\iota,b)\le f_\iota(a^*)\ \text{ for all } b\in A_\iota(\bar a^*_\iota).

Milestones on the path of the proof

§1: products of two convex cells, of two geometric polyhedra, of two polyhedra and of two contractible sets are of the same kind.
$\mathfrak A$ is a contractible polyhedron, and $\phi(a)=M_{\bar a_1}\times\cdots\times M_{\bar a_\nu}$ is contractible for every $a$ .
The LEMMA (p. 889): a semicontinuous multi-valued function $\phi:Z\to Z$ on a contractible polyhedron with contractible values has a fixed point $z^*\in\phi(z^*)$ .
The set $M_\iota=\{(\bar a_\iota,a_\iota)\mid a_\iota\in M_{\bar a_\iota}\}$ is closed, and so is the graph $\Gamma$ of $\phi$ .
$a^*\in\phi(a^*)$ holds exactly when $a^*$ is an equilibrium point.

Further results of the paper

The Remark (p. 889) and its steps (α) and (β) (p. 890). If $G_\iota$ is compact and $f_\iota$ is continuous on it, then $\varphi_\iota$ is upper semicontinuous. If $A_\iota$ is moreover continuous at a point, $\varphi_\iota$ is lower semicontinuous, and hence continuous, there.
The COROLLARY (p. 890). A continuous $f:X\times Y\to\overline{\mathbb R}$ on contractible polyhedra whose argmin sets $U_{x^0}$ and argmax sets $V_{y^0}$ are contractible has a saddle point, $\min_y f(x^0,y)=f(x^0,y^0)=\max_x f(x,y^0)$ .

Significance

The result. The theorem gives an equilibrium for games in which one agent's choices constrain another's. This is the step that makes competitive equilibrium an equilibrium of a game: the market participant's price choice constrains the consumers' budget sets. The same result gives existence for generalized Nash equilibrium problems, including games with shared constraints. Replacing convexity by contractibility also admits non-convex best-response sets: a contractible set such as a star-shaped region or an arc qualifies. Nash's theorem for finite games and von Neumann's minimax theorem are special cases. With values in $\overline{\mathbb R}$ , payoffs may take infinite values.

The formalization. The theorem was proved in 1952. None of it is formalized on the platform: neither the theorem itself, nor the LEMMA, nor the topological vocabulary of polyhedra and contractible sets used here. Brouwer's theorem is available on the platform as AGT.brouwer_fixed_point. Nash's existence theorem for finite games (AGT.nash_existence) and Sion's minimax theorem are also formalized. All of these assume convexity. The mission produces a machine-checked existence theorem for generalized games, together with a fixed-point theorem for set-valued maps with contractible values on polyhedra.

Difficulty

Most of the argument reduces to the LEMMA, which is a particular case of the Eilenberg–Montgomery fixed-point theorem. The usual route to Kakutani's theorem does not carry over: it approximates a convex-valued map by continuous selections and applies Brouwer's theorem on a convex set. Contractible values do not admit convex combinations of nearby values, and a contractible polyhedron need not be convex, so neither the selection step nor Brouwer on a simplex applies directly. Debreu cites the LEMMA without proof, and Mathlib has no fixed-point theorem for set-valued maps and none of the algebraic topology of polyhedra that the classical results rest on.

The remaining steps are point-set topology. The product milestones require building homeomorphisms and deformations on products of subspaces, and the closed-graph steps require care with continuity on $G_\iota$ as opposed to continuity everywhere.

Formalization scope

Spaces and agents. Each $\mathfrak A_\iota$ is a subset of a finite-dimensional real normed space $E_\iota$ , standing in for Debreu's "finite Euclidean spaces". The agents form a Fintype. Profiles live in $\prod_\iota\mathfrak A_\iota$ . The others' actions $\bar a_\iota$ range over the product over the subtype $\{j\mid j\ne\iota\}$ , so $A_\iota$ cannot depend on agent $\iota$ 's own action. With a single agent this product is a point, and the theorem becomes the one-agent statement.
Payoffs. The completed real line is Mathlib's EReal with its order topology. $\varphi_\iota$ is a supremum (sSup) in EReal; under the hypotheses it is attained, so it is Debreu's Max. No arithmetic in EReal is used anywhere.
Polyhedra and contractible sets. A polyhedron is a subspace homeomorphic to a finite union of convex hulls of nonempty finite sets in some $\mathbb R^m$ ; polyhedra are therefore compact. Contractibility is Debreu's definition verbatim, and it includes nonemptiness.
Hypotheses. Non-void values of $A_\iota$ are Debreu's standing assumption and are stated explicitly. Continuity of $f_\iota$ is required on $G_\iota$ only, and continuity of $\varphi_\iota$ on all of $\bar{\mathfrak A}_\iota$ .

Three formalizations would be easier but are not this theorem: one that replaces contractible by convex (that is the Kakutani–Nash setting), one that maximizes over all of $\mathfrak A_\iota$ instead of $A_\iota(\bar a_\iota)$ , and one that assumes a fixed point of $\phi$ or states only the closed-graph step. None of these is acceptable, and the LEMMA may not be weakened to convex domains or convex values.

The work needed includes a small library of polyhedra and contractible subsets, and closed-graph correspondences on products. The largest piece is a proof of the LEMMA, a fixed-point theorem that is reusable well beyond this mission. Proofs of any milestone, alternative routes to the LEMMA, and supporting lemmas on polyhedra, such as compactness, triangulation or being absolute neighbourhood retracts, are all welcome.

Selected references

G. Debreu, A Social Equilibrium Existence Theorem, Proc. Natl. Acad. Sci. USA 38(10), 886–893, 1952. https://doi.org/10.1073/pnas.38.10.886
S. Eilenberg and D. Montgomery, Fixed Point Theorems for Multi-Valued Transformations, Amer. J. Math. 68(2), 214–222, 1946. https://doi.org/10.2307/2371832
E. G. Begle, A Fixed Point Theorem, Ann. of Math. 51(3), 544–550, 1950. https://doi.org/10.2307/1969367
S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Math. J. 8(3), 457–459, 1941. https://doi.org/10.1215/S0012-7094-41-00838-4
J. F. Nash, Equilibrium Points in N-Person Games, Proc. Natl. Acad. Sci. USA 36(1), 48–49, 1950. https://doi.org/10.1073/pnas.36.1.48
K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 265–290, 1954. https://doi.org/10.2307/1907353

19 thms3 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Techniques for Average Completion Time Scheduling IV: List Scheduling from an Optimal One-Machine Schedule Is a 2-Approximation for In-TreesResearch Paper

Motivation

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

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

Timeline of the relevant results:

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4.17

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

6 thms3 active usersReviewed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Techniques for Average Completion Time Scheduling III: From One Machine to Many with Delay ListResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4.13

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

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

Milestones, in the order the proof uses them

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

12 thms3 active usersReviewed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Techniques for Average Completion Time Scheduling II: A 2.83-Approximation for Parallel Machines with Release DatesResearch Paper

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

Formalization targets

Goal: Lemma 4.19

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

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

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

Milestones

In the order the proof uses them:

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

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

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

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

Significance

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

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

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

Difficulty

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

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

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

Formalization scope

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

Committed conventions:

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

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

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

Selected references

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

11 thms3 active usersReviewed

Combinatorics Optimization Probability+1·Captain: mikedeng1

Approximation Techniques for Average Completion Time Scheduling I: Best-α on One Machine with Release DatesResearch Paper

Motivation

Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written $1|r_j|\sum C_j$ ), the problem is strongly NP-hard, so research has focused on approximation algorithms whose guarantees are stated against every feasible schedule.

The standard route runs through the preemptive relaxation. When jobs may be interrupted and resumed, the shortest-remaining-processing-time rule (SRPT) produces an optimal schedule, and its value is a lower bound for every nonpreemptive schedule. The question is how to turn that preemptive schedule into a nonpreemptive one without losing too much.

Timeline:

1995, Phillips, Stein and Wein (WADS 1995, pp. 86–97): order the jobs by their SRPT completion times and schedule them nonpreemptively in that order. This gives a 2-approximation. Later 2-approximations are by Hoogeveen and Vestjens (IPCO 1996), Stougie (1995), and Goemans (SODA 1997). Hoogeveen and Vestjens also showed that deterministic on-line algorithms cannot beat 2.
2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1)): order by $\alpha$ -points instead of completion times, choose $\alpha$ at random, and take the best $\alpha$ off-line. This gives the $e/(e-1)\approx1.58$ bound for Best- $\alpha$ that is the goal of this mission, and an optimal randomized on-line algorithm.
1999, Afrati et al. (FOCS 1999): a polynomial-time approximation scheme for $1|r_j|\sum w_jC_j$ . This settled the approximability of the problem, but the resulting algorithms are far from simple.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$ . Job $J_j$ has a processing time $p_j>0$ , a release date $r_j\ge0$ , and, where the objective is weighted, a weight $w_j>0$ . There is one machine.

A nonpreemptive schedule assigns each job a start time $S_j\ge r_j$ such that the intervals $[S_j,S_j+p_j)$ are pairwise disjoint. Its completion times are $C_j=S_j+p_j$ .

A preemptive schedule $P$ specifies, for each time $t$ , which job runs at $t$ , if any. Job $J_j$ runs only at times $t\ge\max(0,r_j)$ , receives exactly $p_j$ units of processing in total, and finishes by some finite time. Its completion time $C^P_j$ is the first time by which all of $J_j$ has been processed. For $\alpha\in(0,1]$ , its $\alpha$ -point $C^P_j(\alpha)$ is the first time by which $\alpha p_j$ units have been processed.

For a job $J_i$ , $T_i$ denotes the idle time of $P$ before $C^P_i$ . $x_{ij}$ denotes the fraction of $J_j$ processed before $C^P_i$ . The paper writes $S^P_i(\beta)$ for the set of jobs with $x_{ij}=\beta$ , and also for their total processing time.

One-machine list scheduling in a given order runs the jobs nonpreemptively in that order. Each job starts at the later of its release date and the completion of the previous job in the list. An $\alpha$ -schedule is list scheduling in nondecreasing order of the $\alpha$ -points $C^P_j(\alpha)$ . $C^\alpha_j$ denotes the completion times of an $\alpha$ -schedule.

Random- $\alpha$ draws $\alpha$ from a distribution on $(0,1]$ and outputs the $\alpha$ -schedule. Best- $\alpha$ outputs the $\alpha$ -schedule of smallest total completion time $\min_\alpha\sum_j C^\alpha_j$ .

Formalization targets

Goal: Corollary 2.7

Let $P$ be optimal among preemptive schedules for $\sum_j C_j$ . Then there is $\alpha\in(0,1]$ such that every $\alpha$ -schedule derived from $P$ satisfies

\sum_j C^\alpha_j\;\le\;\frac{e}{e-1}\sum_j C_j\qquad\text{for every feasible nonpreemptive schedule } (C_j)_j .

Since Best- $\alpha$ returns a schedule no worse than this $\alpha$ -schedule, Best- $\alpha$ is an $e/(e-1)$ -approximation.

Milestones

The calculus behind the constant. For $f(\alpha)=e^\alpha/(e-1)$ and every $\beta\in(0,1]$ ,

\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha=\frac1{e-1}.

Lemma 2.2: $C^P_i=T_i+\sum_{0<\beta\le1}\beta S^P_i(\beta)$ .
Lemma 2.3: $C^\alpha_i\le T_i+(1+\alpha)\sum_{\beta\ge\alpha}S^P_i(\beta)+\sum_{\beta<\alpha}\beta S^P_i(\beta)$ .
Lemma 2.5: if $\alpha$ has density $f$ on $(0,1]$ , then $E[C^\alpha_i]\le(1+\delta)C^P_i$ with $\delta=\max_{0<\beta\le1}\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha$ .
Theorem 2.6, for the weighted objective with $P$ optimal among preemptive schedules: the expected approximation ratio of Random- $\alpha$ is at most $2$ for uniform $\alpha$ , at most $1.8$ for $\alpha=1$ w.p. $3/5$ and $\alpha=1/2$ w.p. $2/5$ , and at most $e/(e-1)$ for the density $e^\alpha/(e-1)$ .

Companion statements, not milestones:

the upper bound of Theorem 2.1, $\sum_jC^\alpha_j\le(1+1/\alpha)\sum_jC^P_j$ ;
the existence of an optimal preemptive schedule.

Significance

The $e/(e-1)$ bound shows that conversion from the preemptive relaxation can beat the factor 2 of the natural ordering. It does so by exploiting that no single instance is bad for many values of $\alpha$ at once. The $\alpha$ -point technique was also used with LP relaxations, for example by Goemans (SODA 1997) and by Schulz and Skutella. The randomized version is an optimal randomized on-line algorithm for $1|r_j|\sum C_j$ . Lemma 2.3 is a statement about any preemptive schedule, so it applies wherever a good preemptive or fractional schedule is available.

All results of the mission are proved in the paper, except that the proof of Theorem 2.6, part 2 is omitted there. No machine-checked proof of them is known. A complete development would give a verified model of preemptive one-machine schedules, $\alpha$ -points and list scheduling, together with the averaging argument over $\alpha$ . These are reusable for the later results of the same paper and for the $\alpha$ -point literature.

Difficulty

The obvious argument bounds each job's $\alpha$ -schedule completion time directly against its preemptive completion time. That argument loses a factor $1+1/\alpha$ (Theorem 2.1), which is at least 2 for every fixed $\alpha$ . The improvement needs Lemma 2.3. There the charge to each job depends on how much of it was done by $C^P_i$ relative to $\alpha$ , and the idle time $T_i$ is not inflated at all. Proving Lemma 2.3 requires reasoning about a preemptive schedule as a measure on time, and about how moving pieces of jobs changes completion times. A proof that treats the preemptive schedule as a finite list of pieces must first show that nothing is lost by this discretization.

The averaging step needs the expectation over $\alpha$ to be an honest integral. The map $\alpha\mapsto C^\alpha_i$ must be shown integrable, which requires a fixed rule for ties between equal $\alpha$ -points.

Formalization scope

Model. Jobs are Fin n, time is real, $p_j>0$ $p_{j} > 0$ and $r_j\ge0$ $r_{j} \geq 0$ . The paper admits $p_j=0$ $p_{j} = 0$ only in its tightness instances.
- A preemptive schedule is a function $\sigma:\mathbb R\to$ Option (Fin n) (none = idle). Each job's run set is measurable, lies in $[\max(0,r_j),\infty)$ , is bounded above, and has Lebesgue measure $p_j$ .
- Completion times and $\alpha$ -points are infima of nonempty sets that are bounded below.
- $T_i$ is the measure of the idle set in $[0,C^P_i)$ .
- The paper's sums over $\beta$ are sums over jobs, weighted by the fraction $x_{ij}$ .
List scheduling is strict: jobs never overtake the list order, and the machine is free from time $0$ $0$ .
- Lemma 2.3, Theorem 2.1, Theorem 2.6.2 and the goal hold for every tie-break among equal $\alpha$ -points.
- The expectations (Lemma 2.5, Theorem 2.6.1 and 2.6.3) use the tie-break by job index. They assert integrability as part of the conclusion.
Optimality. "Approximation ratio $c$ $c$ " is stated as an inequality against every feasible nonpreemptive schedule, never against an infimum.
- The optimality of $P$ among preemptive schedules is the paper's standing assumption for its upper bounds (p. 151). It appears as a hypothesis of Theorem 2.6 and of the goal.
- The lemmas hold for arbitrary $P$ and do not carry it.
- An existence statement shows the hypothesis can be met.
Lemma 2.5's $\delta$ is replaced by any upper bound of the integrals over $\beta\in(0,1]$ . This is equivalent, and it avoids assuming that the maximum is attained.
Not stated:
- the running time $O(n^2)$ of Best- $\alpha$ and the optimality of SRPT;
- the tightness parts of Theorem 2.1 and Corollary 2.4, and the lower bounds of Theorem 2.9, which use zero-length jobs;
- the on-line Theorem 2.8, which needs a model of on-line algorithms.
Trivializing formalization ruled out. Dropping the optimality of $P$ from the goal would turn it into a statement about arbitrary preemptive schedules, which is Lemma 2.5, not Corollary 2.7. Comparing against $\sum_jC^P_j$ instead of every nonpreemptive schedule would likewise remove the content of the corollary.

Contributions are welcome at every level. The calculus milestone and Lemma 2.2 are good first targets.

Selected references

C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
C. Phillips, C. Stein, J. Wein, Scheduling jobs that arrive over time, Proc. 4th Workshop on Algorithms and Data Structures (WADS), 1995, pp. 86–97 (reference [25] of the paper; no link verified).
J. A. Hoogeveen, A. P. A. Vestjens, Optimal on-line algorithms for single-machine scheduling, Proc. 5th IPCO, 1996, pp. 404–414 (reference [21]; no link verified).
M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 1997, pp. 591–598 (reference [12]; no link verified).
F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th FOCS, 1999 (reference [2]; no link verified).

9 thms3 active usersReviewed

Algorithmic Game Theory Optimization Probability·Captain: mikedeng1

The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts 3: Advance-Purchase Discounts Pareto-Improve Pull Contracts under At-Once Shipping CostsResearch Paper

Motivation

A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.

In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.

Setting

Demand $D$ for the season has law $\mu$ on $\mathbb R$ , distribution function $F$ and density $f$ . As in §3 of the paper, $F(0) = 0$ , $F$ is strictly increasing on $[0,\infty)$ , $F' = f$ on $(0,\infty)$ , and the generalized failure rate $g(x) = x f(x)/(1 - F(x))$ is strictly increasing (IGFR). The expected sales from $q$ available units are

S(q) = q - \int_0^q F(x)\,dx .

The retail price is $p$ , the unit production cost $c$ , the salvage value $v$ , with $v < c < p$ .

A contract is a pair of wholesale prices $\{w_1, w_2\}$ . Before production the retailer submits a prebook order of $y \ge 0$ units at $w_1$ . The supplier then produces $q \ge y$ . During the season, after running out of prebooked stock, the retailer places at-once orders at $w_2$ , filled from the supplier's remaining stock. Pull is $w_1 = w_2 < p$ ; an advance-purchase discount is $w_1 < w_2$ . In §5.1 the supplier pays an extra shipping and handling cost $\tau > 0$ per at-once unit. The profits are

\pi_r(y,q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)\bigl(S(q) - S(y)\bigr),

\pi_s(y,q) = (w_1 - v)y + (w_2 - \tau - v)\bigl(S(q) - S(y)\bigr) - (c - v)q .

A supplier best response to $y$ maximizes $\pi_s(y,\cdot)$ over $q \ge y$ . An outcome of $\{w_1, w_2\}$ is a pair $(y, q)$ with $q$ a best response to $y$ and $y \ge 0$ maximizing $\pi_r$ when every alternative prebook is followed by a best response to it.

Formalization targets

Goal: Theorem 8

Fix $w_2 < p$ and $\tau > 0$ , and suppose the retailer does not prebook under the pull contract $\{w_2, w_2\}$ : $y = 0$ is his unique best reply, followed by the supplier's best response $q_0$ . Then there is $w_1$ with

c < w_1 < w_2

such that $\{w_1, w_2\}$ has an outcome, and every outcome $(y, q)$ of it satisfies

\pi_r^{\{w_1,w_2\}}(y,q) > \pi_r^{\{w_2,w_2\}}(0,q_0), \qquad \pi_s^{\{w_1,w_2\}}(y,q) > \pi_s^{\{w_2,w_2\}}(0,q_0).

Milestones

Eq. (22): for $v < w_1 \le w_2 \le p$ the retailer's profit is concave in $y$ and uniquely maximized at $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$ , whatever $q$ .
Eqs. (20)–(21) with $w_2 - \tau$ : the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - \tau - c)/(w_2 - \tau - v)$ , independent of $w_1$ , and $q_s$ is smaller than without the shipping cost.
§5.1: for fixed $w_2$ the retailer is never worse off with $w_1 \le w_2$ than with $w_1 = w_2$ .
$y_r(w_1) > 0$ for every $w_1 < w_2$ .
The derivative of $w_1 \mapsto \pi_s(y_r(w_1), q)$ , where the density at $y_r(w_1)$ is positive:

\frac{d\pi_s(y_r(w_1), q)}{dw_1} = y_r(w_1) - \frac{(w_1 - v) - (w_2 - \tau - v)(1 - F(y_r(w_1)))}{(w_2 - v) f(y_r(w_1))}.

$y_r(w_1) \to 0$ as $w_1 \to w_2$ , and, when $f$ has a positive right limit $f(0)$ at $0$ , the derivative in 5 tends to $-\tau/((w_2 - v) f(0)) < 0$ .

Significance

Without shipping costs, advance-purchase discounts with $w_2 = p$ coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.

The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at $0$ is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.

Difficulty

The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as $w_1 \to w_2$ . That limit involves $f(0)$ , which the model does not provide: $F$ is differentiable only on $(0, \infty)$ , and for gamma demand with shape above $1$ the density vanishes at $0$ , so the paper's limit is $-\infty$ . A proof of the goal must therefore not rest on the limit display alone.

The second obstacle is the retailer's global choice. The calculus concerns prebooks $y_r(w_1)$ below the supplier's production $q_s$ . Once $w_1 < w_2$ , the retailer might instead prefer a prebook at least $q_s$ , turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for $w_1$ close to $w_2$ requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at $y_r$ .

Formalization scope

Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on $(0,\infty)$ only, so the exponential law is admitted. Quantities range over $[0, \infty)$ . Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for $w_2 \le p$ , and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue $w_2 - \tau$ . The prebook function $y_r$ in milestones 5 and 6 is a function pinned on $(v, w_2)$ by Eq. (22), which determines it uniquely.

Readings of the paper's words:

"the retailer does not prebook when $w_1 = w_2$ " is read as " $y = 0$ is the retailer's unique best reply" (every $y > 0$ gives strictly less); with a tie the conclusion can fail;
"profit increases for both" is read as a strict increase for both firms, in every outcome of the discounted contract;
the conclusion $c < w_1$ strengthens "advance-purchase discount" ( $w_1 < w_2$ );
"reduces the supplier's optimal production" (milestone 2) is a strict decrease; its formula is stated for $c \le w_2 - \tau$ ;
" $f(0)$ " in milestone 6 is the right limit of $f$ at $0$ , assumed positive there only; the positivity of $f(y_r(w_1))$ in milestone 5 is the hypothesis of the implicit-function step;
"never worse off" (milestone 3) compares every outcome of $\{w_1, w_2\}$ with every outcome of $\{w_2, w_2\}$ .

A version of the goal that assumed $f(0) > 0$ , assumed $y_r(w_1) < q_s$ , compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with $\ge$ , would be weaker than Theorem 8 and is not the target.

A complete development needs the concavity and first-order conditions for $S$ , the inverse-function derivative for $F$ , and the regime comparison between prebooks below and above $q_s$ . The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.

Selected references

G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
M. A. Lariviere, E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971

9 thms3 active usersReviewed

Algorithmic Game Theory Optimization Probability·Captain: mikedeng1

The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts 2: Advance-Purchase Discounts Coordinate the Supply ChainResearch Paper

Motivation

A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.

The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.

Setting

Demand is a random variable with distribution function $F$ and density $f$ . The paper assumes $F(0) = 0$ , $F$ strictly increasing, and an increasing generalized failure rate (IGFR): $g(x) = x f(x)/(1 - F(x))$ has $g'(x) > 0$ . Production costs $c$ per unit, the retail price is $p$ , and leftover units are salvaged for $v$ , with $v < c < p$ . Expected sales with $q$ units available are

S(q) = q - \int_0^q F(x)\,dx,

and the integrated supply chain's expected profit is $\Pi(q) = (p - v)S(q) - (c - v)q$ . It is maximized at $q^o$ with $F(q^o) = (p-c)/(p-v)$ ; write $\Pi^o = \Pi(q^o)$ . The efficiency of a contract is $\Pi(q)/\Pi^o$ , where $q$ is the quantity produced.

A contract is a pair of wholesale prices $\{w_1, w_2\}$ with $w_1 \le w_2$ . The retailer first prebooks $y \ge 0$ units at $w_1$ each. The supplier, seeing $y$ , produces $q \ge y$ . During the season the retailer sells the prebook and, once it runs out, places at-once orders at $w_2$ per unit from the supplier's remaining stock, provided $w_2 \le p$ . The supplier's and retailer's expected profits are

\pi_s(y, q) = (w_1 - v)y + (w_2 - v)(S(q) - S(y)) - (c - v)q,

\pi_r(y, q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)(S(q) - S(y)),

with the at-once terms absent when $w_2 > p$ . An outcome of a contract is a pair $(y, q)$ where $q$ maximizes the supplier's profit given $y$ , and $y$ maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push ( $w_1 < p < w_2$ ), pull ( $w_1 = w_2 \le p$ ) and advance-purchase discount ( $w_1 < w_2 \le p$ ). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).

Formalization targets

Goal: Theorem 7

For every $w_1$ with $c \le w_1 \le p$ , the contract $\{w_1, p\}$ has an outcome and is Pareto; every outcome $(y, q)$ of every Pareto contract satisfies

\Pi(q) = \Pi^o;

and for every $r \in [0, \Pi^o]$ some contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome with payoffs

\bigl(\pi_r, \pi_s\bigr) = \bigl(r,\ \Pi^o - r\bigr).

Milestones

Eq. (2): $\Pi$ is concave on $[0, \infty)$ and maximized exactly where $F(q^o) = (p-c)/(p-v)$ .
Eqs. (20)–(21): for $c \le w_2 \le p$ , the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - c)/(w_2 - v)$ .
Eq. (22): for $c \le w_1 \le w_2 \le p$ , $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$ is the unique maximizer of $\pi_r(\cdot, q)$ .
Eq. (3): in push mode the retailer's optimal prebook solves $F(q) = (p - \hat w_1)/(p - v)$ .

A further draft theorem states the step of the proof in which the retailer's outcome profit along $\{w_1, p\}$ falls strictly from $\Pi^o$ to $0$ as $w_1$ rises from $c$ to $p$ .

Significance

The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces $q^o$ ; the prebook price then acts as a pure transfer. Every division of $\Pi^o$ is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.

The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.

Difficulty

The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when $w_2 = p$ . Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook $y = 0$ always being available and on $w_1 \ge c$ . Third, the division claim is surjectivity of the retailer's equilibrium payoff over $w_1 \in [c, p]$ , which needs the solution of $F(y_r) = (p - w_1)/(p - v)$ to vary continuously with $w_1$ , including at both ends ( $y_r = q^o$ at $w_1 = c$ , $y_r = 0$ at $w_1 = p$ ).

Formalization scope

Demand is a probability measure $\mu$ on $\mathbb R$ with $F$ = ProbabilityTheory.cdf μ. The standing assumptions are a structure: $F(0) = 0$ , $F$ strictly increasing on $[0, \infty)$ , $F' = f$ on $(0, \infty)$ , and $g' > 0$ on $(0, \infty)$ . Differentiability is required only on $(0, \infty)$ , so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over $[0, \infty)$ . $q^o$ is a parameter with the hypothesis $F(q^o) = (p-c)/(p-v)$ ; its existence is part of milestone 1.

Readings of informal words: "includes all" means every contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the $w_2 = p$ family; "any division is achievable" is surjectivity onto $[0, \Pi^o]$ ; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is $\max\{y, q_s\}$ " is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when $w_2 \le p$ (p. 226, "with push $w_2 > p$ , so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires $w_1 \ge c$ (p. 228 sets aside $\hat w_1 < c$ as Pareto inferior); pull includes $w_1 = w_2 = p$ (the paper's remark in the proof) and advance-purchase discounts include $w_2 = p$ (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.

Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of $\{w_1, p\}$ as $(y_r, q^o)$ would turn the goal into algebra, and is ruled out.

Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of $S$ , and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.

Selected references

G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971
B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
G. P. Cachon and M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445

7 thms3 active usersReviewed

Optimization Probability·Captain: mikedeng1

The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts 1: The Pareto Set of Push and Pull ContractsResearch Paper

Who bears the inventory risk

A supplier and a retailer trade a product with a single selling season and uncertain demand. Someone has to decide, before demand is known, how many units exist, and someone has to be left holding the units that do not sell. With a push contract the retailer orders (prebooks) before the season and bears all of this risk; with a pull contract the supplier produces to stock and the retailer only orders during the season, so the supplier bears it. Both are single wholesale price contracts, the simplest and most common contracts in practice. Cachon (Management Science 50(2), 2004) asks which of these contracts two negotiating firms could plausibly agree on, independently of how they bargain, and answers it by computing the Pareto set of push and pull contracts together.

Push alone is the "selling to the newsvendor" problem studied by Lariviere and Porteus (MSOM 2001), whose unimodality result this mission uses. The novelty of §4 of Cachon's paper is to put push and pull contracts in one contract space and to show that the Pareto set then contains contracts of both kinds.

Setting

Demand has distribution function $F$ and density $f$ . The paper's standing assumptions (§3, p. 225) are: $F(0) = 0$ , $F$ strictly increasing, and the generalized failure rate $g(x) = x f(x)/(1 - F(x))$ strictly increasing (IGFR); the normal, exponential, gamma and Weibull laws qualify. Units cost $c$ to produce, sell at the retail price $p > c$ , and are salvaged at $v < c$ .

Expected sales with $q$ units available are $S(q) = q - \int_0^q F(x)\,dx$ , and the integrated chain earns $\Pi(q) = (p - v)S(q) - (c - v)q$ . It is maximized at the newsvendor quantity $q^o$ , $F(q^o) = (p - c)/(p - v)$ , with $\Pi^o = \Pi(q^o)$ ; the efficiency of a contract is $\Pi(q)/\Pi^o$ .

A contract is described by the quantity $q$ it induces.

Push at wholesale price $\hat w_1$ : the retailer prebooks $q$ and earns $\hat\pi_r = (p - v)S(q) - (\hat w_1 - v)q$ ; the supplier earns $\hat\pi_s = (\hat w_1 - c)q$ . The price inducing $q$ is $\hat w_1(q) = p - (p - v)F(q)$ , and $\hat\pi_r(q)$ , $\hat\pi_s(q)$ are the payoffs at that price.
Pull at wholesale price $w_1 = w_2$ : the supplier produces $q$ and earns $\pi_s = (w_1 - v)S(q) - (c - v)q$ ; the retailer earns $\pi_r = (p - w_1)S(q)$ . The inducing price is $w_1(q) = (c - vF(q))/(1 - F(q))$ .

Write $j(q) = S(q)/(1 - F(q))$ and $h(q) = f(q)/(1 - F(q))$ (the hazard rate). The retailer's preferred pull contract is $q^* = \arg\max \pi_r$ and the supplier's preferred push contract is $\hat q^* = \arg\max \hat\pi_s$ .

A contract $k'$ Pareto dominates $k$ if no firm is worse off and one firm is strictly better off; the Pareto set consists of the contracts no other contract dominates.

A pull contract is only played as pull if the retailer does not prefer to prebook anyway. In the prebook game (§4.5) the retailer prebooks $y \ge 0$ and the supplier then chooses her production $Q \ge y$ to maximize $(w_1 - v)y + (w_2 - v)(S(Q) - S(y)) - (c - v)Q$ . A pull contract survives the push challenge if the retailer's profit is strictly highest at $y = 0$ .

Formalization targets

Goal: Theorem 6 with Lemma 5

There is a quantity $q^P$ , $0 < q^P < q^o$ , the unique positive quantity at which each firm is indifferent between the pull and the push contract, such that

\text{Pareto set} = \{\text{push}, \text{pull}\} \times [q^P, q^o],

and every pull contract with $q \in [q^P, q^o]$ survives the push challenge.

Milestones, in the order the proof uses them

Eqs. (1)–(2), (3), (7): the newsvendor quantity $q^o$ ; the prices $\hat w_1(q)$ , $w_1(q)$ induce $q$ .
Eqs. (5), (9) and Lariviere–Porteus: $\hat\pi_r$ and $\pi_s$ are increasing, $\hat\pi_s$ is unimodal.
Lemma 1: $j(q)h(q)$ is increasing for $q > 0$ . Theorem 2: $\pi_r$ is concave.
Theorem 3: $\pi_r(q^*) > \hat\pi_s(\hat q^*)$ , $q^* > \hat q^*$ , $\Pi(q^*) > \Pi(\hat q^*)$ .
Lemma 4: $q^P$ exists, is the unique positive root of $\pi_r = \hat\pi_r$ and of $\pi_s = \hat\pi_s$ , the unique maximizer of $\pi_r - \hat\pi_s$ , and $q^P > q^*$ .
Eqs. (20)–(21) and Lemma 5: the supplier's reply to a prebook $y$ is $\max\{y, q_s\}$ ; pull contracts with $q \ge q^P$ survive the push challenge.

Significance

The theorem says that when both allocations of inventory risk are on the table, neither firm's preferred contract ( $\hat q^*$ for the supplier, $q^*$ for the retailer) is Pareto, and the least efficient Pareto contract, $q^P$ , is more efficient than the least efficient contract of either push-only or pull-only negotiation. In the Pareto set the supplier prefers every pull contract to every push contract and the retailer the reverse, so each firm earns more by bearing the risk itself. The results are proved in the paper, with the calculus informal, the unimodality of $\hat\pi_s$ cited, and half of Theorem 6's proof called "analogous". The mission produces a machine-checked version under exactly stated hypotheses; the IGFR concavity and single-crossing facts (Lemma 1, Theorem 2, Lemma 4) are reusable for other contract analyses. No part of this paper is formalized elsewhere; a related platform statement, Snyder–Shen Theorem 14.3 (SupplyChainTheory.wholesale_supplier_unimodal), is the Lariviere–Porteus lemma under stronger assumptions (nonnegative salvage value, finite mean, a continuous positive density, and only a weakly increasing failure rate).

Difficulty

The comparisons are between functions of different shapes: the supplier's push profit is a margin times a quantity, the retailer's pull profit a margin times expected sales. Signing derivatives needs the monotonicity of $j(q)h(q)$ (Lemma 1), and that fails to be routine at $q \to 0$ , where $F$ need not be differentiable. The set equality compares four profit curves at once, and survival of the push challenge is a statement about a different game, the supplier's best reply to every prebook.

Formalization scope

Demand is a probability measure $\mu$ on $\mathbb R$ with $F$ = ProbabilityTheory.cdf μ. The predicate DemandModel μ f records $F(0) = 0$ , $F$ strictly increasing on $[0, \infty)$ , $F' = f$ on $(0, \infty)$ , and $g'(x) > 0$ for $x > 0$ . Differentiability is not required at $0$ : the exponential law has a kink there, and it is the paper's own IGFR example. Prices satisfy $v < c < p$ ; no sign is imposed on $v$ . Quantities range over $[0, \infty)$ . The paper's $q^o$ is a parameter characterized by $F(q^o) = (p - c)/(p - v)$ , and the first milestone proves it exists and is unique.

Profits are defined in the paper's primitive (quantity, price) forms composed with the inducing prices; the closed forms are milestones, not definitions.

Readings of informal words, each named in the item concerned:

"increasing" in Lemma 1 and in Eqs. (2), (5), (9) is strict, as the proofs show; "concave" in Theorem 2 is strict concavity, as the proof shows via Lemma 1.
"unimodal" means strictly increasing on $[0, \hat q]$ and strictly decreasing on $[\hat q, \infty)$ for some $\hat q > 0$ .
Uniqueness in Lemma 4 (i)–(ii) is over $q > 0$ , since all profits vanish at $0$ . Theorem 3 and Lemma 4 (v) hold for every maximizer, and the maximizers' existence is stated.
Theorem 6's "includes all" is set equality, which its proof establishes. The survival conjunct comes from Lemma 5, which the proof's last sentence invokes.
"prefers to prebook zero … rather than any positive amount" is strict preference.
The contract space is the admissible contracts, $q \ge 0$ with wholesale price in $[c, p]$ (equivalently $0 \le q \le q^o$ in both modes). This is an explicit addition. The paper restricts prices to $\hat w_1 < p$ and $w_1 = w_2 < p$ and states that contracts with $q > q^o$ are Pareto inferior; but $\hat w_1 < p$ admits push with $q > q^o$ ( $\hat w_1 < c$ ), where the retailer earns over $\Pi^o$ and nothing dominates.
Eqs. (20)–(21) are stated for $w_2 > c$ , which is what makes (21) solvable.

The statement does not follow trivially from a degenerate encoding. The demand assumptions are satisfiable, since the exponential law meets them. $q^o$ , $q^P$ , $q^*$ and $\hat q^*$ are shown to exist inside the statements that use them, and the Pareto set is taken over both modes and every admissible quantity, not only over the claimed interval.

Welcome contributions: basic facts about $S$ , $j$ and $jh$ under the demand assumptions, reusable across the series' other two missions.

Selected references

G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971

15 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Generalization Bounds in the Predict-then-Optimize Framework III: Strongly Convex Sets Satisfy the Strength PropertyResearch Paper

Motivation

In the predict-then-optimize framework, a machine-learning model predicts the cost vector $\hat c$ of a linear optimization problem $\min_{w\in S}\hat c^\top w$ , and a decision is made by solving that problem with the prediction. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed judging predictions by the SPO loss, the excess cost of the decision induced by $\hat c$ when the true cost is $c$ . El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) develop generalization bounds for learning with the SPO loss.

The SPO loss is discontinuous in $\hat c$ : its value jumps where the optimization problem has several optimal solutions. The paper's sharper bounds (its Theorems 4 and 5) therefore replace the SPO loss by a margin SPO loss that is Lipschitz, and they hold whenever the feasible region satisfies a geometric condition called the strength property. This mission formalizes the paper's first class of feasible regions for which that condition holds: strongly convex sets, such as Euclidean balls and $\ell_q$ balls with $q\in(1,2]$ .

Setting

Let $E$ be a finite-dimensional real vector space with a norm $\|\cdot\|$ (the paper's $\mathbb R^d$ with a generic norm). A cost vector is a linear functional $c$ on $E$ ; its value at $w$ is written $c^\top w$ , and its dual norm is $\|c\|_*=\max_{\|w\|\le1}c^\top w$ . The closed ball of radius $r$ around $\bar w$ is $B(\bar w,r)=\{w:\|w-\bar w\|\le r\}$ .

The feasible region $S\subseteq E$ is nonempty, compact and convex. An optimization oracle is any map $w^*$ with $w^*(\hat c)\in S$ and $\hat c^\top w^*(\hat c)\le\hat c^\top w$ for all $w\in S$ ; no tie-breaking rule is fixed.

The degenerate set $\mathcal C^\circ$ consists of the cost vectors $\hat c$ for which $\min_{w\in S}\hat c^\top w$ has more than one optimal solution.
The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$ .
$S$ satisfies the strength property with parameter $\mu>0$ if, for all cost vectors $\hat c$ and all $w\in S$ ,

\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \Big(\frac{\mu\,\nu_S(\hat c)}{2}\Big)\|w-w^*(\hat c)\|^2 .

The normal cone of $S$ at $\bar w\in S$ is $N_S(\bar w)=\{c: c^\top(w-\bar w)\le0 \text{ for all } w\in S\}$ .
For $\bar\mu\ge0$ , a convex set $S$ is $\bar\mu$ -strongly convex if for all $w_1,w_2\in S$ and $\lambda\in[0,1]$ ,

B\Big(\lambda w_1+(1-\lambda)w_2,\ \Big(\frac{\bar\mu}{2}\Big)\lambda(1-\lambda)\|w_1-w_2\|^2\Big)\subseteq S .

Formalization targets

Goal: Theorem 7, strength claim (p. 23)

If $S$ is compact, not a singleton, and $\bar\mu$ -strongly convex for some $\bar\mu>0$ , then for every oracle $w^*$ ,

\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \Big(\frac{\bar\mu\,\nu_S(\hat c)}{2}\Big)\|w-w^*(\hat c)\|^2\qquad\text{for all } w\in S,\ \hat c .

The strength parameter equals the strong convexity constant.

Milestones

Maximum over a ball (Appendix D.1, p. 35): for $r\ge0$ , $\max_{\tilde w\in B(\hat w,r)}c^\top\tilde w=c^\top\hat w+r\|c\|_*$ .
Proposition 1 (Vial 1983; p. 23): for a $\bar\mu$ -strongly convex set with $\bar\mu\ge0$ and every $\bar w\in S$ ,

N_S(\bar w)=\Big\{c: c^\top(w-\bar w)\le-\Big(\frac{\bar\mu}{2}\Big)\|c\|_*\|w-\bar w\|^2\ \text{for all } w\in S\Big\}.

Degenerate set (proof of Theorem 7, p. 24): under the hypotheses of the goal, $\mathcal C^\circ=\{0\}$ .
Theorem 7, first claim (p. 23): under the same hypotheses, $\nu_S(\hat c)=\|\hat c\|_*$ for every $\hat c$ .

Significance

Theorem 7 is what makes the paper's margin-based bounds usable for a concrete family of feasible regions. It says two things: the strength property holds with $\mu=\bar\mu$ , so the Lipschitz constants in the margin analysis are explicit; and $\nu_S(\hat c)=\|\hat c\|_*$ , so the margin of a prediction, and with it the empirical margin SPO loss, is as easy to compute as a dual norm. Combined with bounds on the multivariate Rademacher complexity, this gives generalization bounds for strongly convex regions whose dependence on the dimension improves on the paper's Natarajan-dimension bound. In dimension one it recovers the classical margin bounds for binary classification (Example 7, p. 24).

The results are proved in the paper; Proposition 1 is due to Vial (1983). None of them has a machine-checked proof known to this mission, and Mathlib has no notion of a strongly convex set (its StrongConvexOn concerns functions). The mission produces a formal definition of strongly convex sets for a general norm, the normal-cone characterization, and the connection to the predict-then-optimize strength property. It is one of four missions on this paper; the margin-based generalization bound itself is the subject of mission II, and polyhedral regions of mission IV.

Difficulty

Definition 5 speaks about balls around convex combinations, while Proposition 1 is a pointwise inequality with the exact constant $\bar\mu/2$ . Evaluating the ball inclusion at any single convex combination loses that constant, since the admissible radius and the displacement of the centre both shrink with the mixing weight. Relating a ball to a linear functional also requires the maximum of $c^\top w$ over a ball to be attained and equal to $c^\top\hat w+r\|c\|_*$ , a fact about dual norms whose attainment depends on finite dimensionality.

For $\nu_S(\hat c)=\|\hat c\|_*$ , comparing $\hat c$ with $0\in\mathcal C^\circ$ gives only the inequality $\nu_S(\hat c)\le\|\hat c\|_*$ ; equality needs every nonzero cost vector to have a unique minimizer over $S$ . The oracle minimizes, whereas the normal cone is written for maximizers, so the signs in (5) and (8) do not match directly and are a common source of error.

Formalization scope

$E$ is a finite-dimensional real normed space with an arbitrary norm. Cost vectors are continuous linear functionals (StrongDual ℝ E), so $c^\top w$ is c w and the operator norm is the dual norm; balls are Metric.closedBall.
The feasible region carries the paper's standing assumptions (§2, p. 5): compact, and convex (as part of the strongly convex set predicate). Nonemptiness follows from the hypothesis that $S$ is not a singleton, stated as S.Nontrivial. Proposition 1 and the ball identity carry no compactness hypothesis, as in the paper.
The oracle is quantified over: the goal holds for every map selecting a minimizer.
$\nu_S$ is Metric.infDist to the degenerate set; the parameter conditions $\mu>0$ and $\bar\mu\ge0$ are hypotheses of the theorems, not parts of the predicates.
The strongly convex set predicate includes convexity and quantifies $\lambda$ over $[0,1]$ only. Without the non-singleton hypothesis the theorem is false: a singleton is strongly convex for every $\bar\mu$ , has no degenerate cost vector, and has $\nu_S\equiv0\ne\|\hat c\|_*$ . A formalization that drops that hypothesis, quantifies $\lambda$ over all reals (which empties the ball for $\lambda\notin[0,1]$ ), or fixes a specific oracle is not this theorem.
Reusable beyond this mission: the strongly convex set predicate and the normal-cone characterization (relevant to Frank–Wolfe analyses over strongly convex sets), and the identity for the maximum of a linear functional over a ball. Proofs of any milestone, and lemmas giving examples of strongly convex sets (Euclidean balls), are welcome.

Selected references

O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022 (Mathematics of Operations Research, 2023). https://arxiv.org/abs/1905.11488
A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
J.-P. Vial, Strong and weak convexity of sets and functions, Mathematics of Operations Research 8(2), 1983. https://doi.org/10.1287/moor.8.2.231
D. Garber, E. Hazan, Faster rates for the Frank–Wolfe method over strongly-convex sets, ICML 2015. https://arxiv.org/abs/1406.1305
M. Journée, Y. Nesterov, P. Richtárik, R. Sepulchre, Generalized power method for sparse principal component analysis, JMLR 11, 2010. https://www.jmlr.org/papers/v11/journee10a.html

7 thms3 active usersReviewed

Operations Research

Missions

An Exact Duality Theory for Semidefinite Programming and Its Complexity Implications: The Extended Lagrange–Slater Dual Has Zero Duality Gap and Attains Its OptimumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6 (Duality Theorem)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Nonsmooth Version of Newton's Method I: local superlinear convergence of the generalized-Jacobian Newton method at a semismooth regular rootResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2, local superlinear convergence

Stronger: Theorem 3.2, order 1+p1 + p1+p

Milestones

Significance

Difficulty

Formalization scope

Selected references

Shortest Connection Networks And Some Generalizations: Construction Principles P1 and P2 Yield a Shortest Spanning Subtree of Every Connected Labelled GraphResearch Paper

Motivation

Setting

Formalization targets

Goal (§IV, p. 1396)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Updating Quasi-Newton Matrices with Limited Storage: The Limited-Storage BFGS Method Reaches the Minimizer of a Strictly Convex Quadratic in at Most n StepsResearch Paper

Motivation

Setting

Formalization targets

Goal: quadratic termination of SQN

Milestones

Significance

Difficulty

Formalization scope

Selected references

Cubic Regularization of Newton Method and Its Global Performance I: Global Rate of Convergence to Second-Order Stationary PointsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1, inequality (3.4)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Critical-Path Planning and Scheduling I: Critical Jobs Occur Only When the Completion Time Is the Earliest, and Then Form a Path from Origin to TerminusResearch Paper

Motivation

Setting

Formalization targets

Goal: critical jobs force λ=tn(0)\lambda = t_n^{(0)}λ=tn(0)​ and a critical path (p. 163)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 4: First-Fit Decreasing Uses at Most 71/60 L* + 5 Bins When No Item Exceeds 1/2Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov-Renewal Programming. I: Formulation, Finite Return Models: Policy Iteration Finds an Optimal Stationary Policy for the Discounted Infinite-Horizon Markov-Renewal ProgramResearch Paper

Motivation

Setting

Formalization targets

Goal (p. 947)

Milestones

Significance

Stronger: Theorem 3.2, order $1 + p$

Goal: critical jobs force $\lambda = t_n^{(0)}$ and a critical path (p. 163)

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