Optimization

Operations Research·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization III: For Semi-Algebraic Problems the ADMM Sequence Converges and Has Finite LengthResearch Paper

Motivation

The alternating direction method of multipliers (ADMM) is a standard method for problems of the form $\min_x h(x)+P(\mathcal Mx)$ , in which a smooth loss $h$ is composed with a structured, possibly nonsmooth regularizer $P$ through a linear map $\mathcal M$ . Its convergence theory was developed for convex problems, yet it is routinely run on nonconvex ones: sparse recovery with the $\ell_0$ constraint, low-rank matrix problems, and total-variation-type models with nonconvex penalties. For such problems a practitioner wants a guarantee about the iterates actually produced, not only about the existence of good subsequences.

Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave the first such guarantee for the classical ADMM on nonconvex composite problems with a surjective $\mathcal M$ . Their Theorem 1 shows that cluster points of the (proximal) ADMM are stationary; their Theorem 3, the subject of this mission, shows that for semi-algebraic data the whole sequence converges. The argument adapts the Kurdyka–Łojasiewicz (KL) framework of Attouch, Bolte and Svaiter (Math. Program. 137, 2013) to a setting where the ADMM only decreases its merit function in the $x$ -block.

Setting

Fix $\mathcal M:\mathbb R^n\to\mathbb R^m$ linear, $h:\mathbb R^n\to\mathbb R$ twice continuously differentiable with bounded Hessian, and $P:\mathbb R^m\to(-\infty,+\infty]$ proper (finite somewhere) and closed (lower semicontinuous). For $\beta>0$ the augmented Lagrangian is

L_\beta(x,y,z)=h(x)+P(y)-\langle z,\mathcal Mx-y\rangle+\tfrac\beta2\|\mathcal Mx-y\|^2 .

The ADMM produces $(x^t,y^t,z^t)_{t\ge0}$ from arbitrary $(x^0,z^0)$ by

y^{t+1}\in\operatorname*{Arg\,min}_y L_\beta(x^t,y,z^t),\quad x^{t+1}\in\operatorname*{Arg\,min}_x L_\beta(x,y^{t+1},z^t),\quad z^{t+1}=z^t-\beta(\mathcal Mx^{t+1}-y^{t+1}).

Assumption 1 with $\mathcal T_1=0$ asks for $\sigma,\delta>0$ , $\gamma\in(0,1)$ and symmetric maps $\mathcal Q_1,\mathcal Q_2,\mathcal Q_3$ with $\mathcal M\mathcal M^*\succeq\sigma\mathcal I$ , $\mathcal Q_1\succeq\nabla^2h(x)\succeq\mathcal Q_2$ and $\mathcal Q_3\succeq[\nabla^2h(x)]^2$ for all $x$ , $\mathcal Q_2+\beta\mathcal M^*\mathcal M\succeq\delta\mathcal I$ , and $\delta\mathcal I\succ\frac{2}{\sigma\beta\gamma}\mathcal Q_3$ .

The limiting subdifferential $\partial f(x)$ of $f$ consists of limits $v$ of regular subgradients $v^t$ at points $x^t\to x$ with $f(x^t)\to f(x)$ . A point $x$ is stationary if $0\in\nabla h(x)+\mathcal M^*\partial P(\mathcal Mx)$ .

A set in $\mathbb R^N$ is semi-algebraic if it is a finite union of sets cut out by finitely many polynomial equations $p_i=0$ and strict inequalities $g_j<0$ ; a function is semi-algebraic if its graph is. A proper $f$ has the KL property at $\hat x\in\operatorname{dom}\partial f$ if there are $\eta>0$ , a neighbourhood $V$ of $\hat x$ and a continuous concave $\varphi:[0,\eta)\to\mathbb R_+$ with $\varphi(0)=0$ , $\varphi\in C^1(0,\eta)$ , $\varphi'>0$ , such that $\varphi'(f(x)-f(\hat x))\,\operatorname{dist}(0,\partial f(x))\ge1$ whenever $x\in V$ and $f(\hat x)<f(x)<f(\hat x)+\eta$ . A KL function is proper, closed, and KL at every point of $\operatorname{dom}\partial f$ .

In the Lean development $L_\beta$ is augLag h P M β x y z, and also augLagX h P M β as a single function on the triple space $\mathbb R^n\times\mathbb R^m\times\mathbb R^m$ with the Euclidean inner product.

Formalization targets

Goal: Theorem 3 (p. 13)

Under the standing assumptions and Assumption 1 with $\mathcal T_1=0$ , if $h$ and $P$ are semi-algebraic and the ADMM sequence has a cluster point $(x^*,y^*,z^*)$ , then

(x^t,y^t,z^t)\to(x^*,y^*,z^*),\qquad 0\in\nabla h(x^*)+\mathcal M^*\partial P(\mathcal Mx^*),\qquad \sum_{t}\|x^{t+1}-x^t\|<\infty .

No constants are fixed: every parameter is quantified exactly as in the paper.

Milestones

(35): some $w\in\partial L_\beta(x^{t+1},y^{t+1},z^{t+1})$ has $\|w\|\le C\|x^{t+1}-x^t\|$ for $t\ge1$ .
(36): $L_\beta(x^t,y^t,z^t)-L_\beta(x^{t+1},y^{t+1},z^{t+1})\ge D\|x^{t+1}-x^t\|^2$ for $t\ge1$ .
(39): $L_\beta(x^t,y^t,z^t)\to L_\beta(x^*,y^*,z^*)$ .
Finite termination when $L_\beta$ reaches its limit value.
(41): the one-step KL estimate.
Remark 4(1): the goal with " $L_\beta$ is a KL function" in place of semi-algebraicity.
$L_\beta$ is semi-algebraic when $h$ and $P$ are.
Proper closed semi-algebraic functions are KL functions, with $\varphi(s)=cs^{1-\theta}$ .

Milestones 6, 7 and 8 together imply the goal.

Significance

The result. Theorem 3 upgrades subsequential convergence to convergence of the whole iterate sequence, with finite length of the $x$ -trajectory, for a nonconvex ADMM without any convexity of $h$ or $P$ . Semi-algebraicity covers the paper's applications: polynomial losses, the $\ell_0$ constraint, and indicators of polyhedral or algebraic sets. Remark 4(1) isolates the only property actually used, the KL property of $L_\beta$ , so the result extends to any class of functions for which that property is known (for instance, globally subanalytic or o-minimal definable data).

Formalizing it. The result is proved in the paper and, as far as is known, formalized nowhere. The mission produces a machine-checked version of the paper's convergence argument, a Lean definition of the KL property with the correct convention for empty subdifferentials, and a semi-algebraic set predicate over MvPolynomial. Milestone 8 is a published theorem of real algebraic geometry and nonsmooth analysis (Bolte–Daniilidis–Lewis 2007) that the paper quotes without proof; it is part of what a complete development of the goal requires.

Difficulty

The obvious route is to invoke the abstract convergence theorem of Attouch–Bolte–Svaiter for descent methods. It does not apply: its sufficient-decrease hypothesis requires $L_\beta$ to drop by a multiple of $\|x^{t+1}-x^t\|^2+\|y^{t+1}-y^t\|^2+\|z^{t+1}-z^t\|^2$ , while the ADMM only guarantees a drop proportional to $\|x^{t+1}-x^t\|^2$ (Remark 4(2)). The relative-error bound (35) is likewise in terms of the $x$ -step alone, and relating the $y$ - and $z$ -blocks back to the $x$ -block uses the surjectivity of $\mathcal M$ and the specific structure of the multiplier update. The neighbourhood on which the KL inequality holds is a neighbourhood of the full triple, whereas the trajectory is controlled only in $x$ .

The semi-algebraic part has a separate difficulty: showing that $L_\beta$ is semi-algebraic needs closure of semi-algebraic sets under projection (the Tarski–Seidenberg theorem), and the KL property of semi-algebraic functions needs the Łojasiewicz inequality for subanalytic or semi-algebraic functions. Mathlib has neither.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin n); $\mathcal M$ is a continuous linear map and $\mathcal M^*$ its adjoint. $P$ and $L_\beta$ take values in EReal, never passed through toReal except where the value is provably finite. $\succeq$ is Mathlib's Loewner order on self-maps; the Hessian is fderiv ℝ (gradient h). The ADMM is the proximal-ADMM relation with $\phi=0$ ; argmin steps are "value at most the value anywhere", with no uniqueness; $y^0$ is unconstrained. The triple space is the nested $L^2$ product, so its inner product is the sum of the block inner products.

The KL inequality is stated for every $v\in\partial f(x)$ , which encodes $\operatorname{dist}(0,\emptyset)=+\infty$ . Writing it with Metric.infDist 0 (∂f x) would give $\operatorname{dist}(0,\emptyset)=0$ and make the KL property fail at every point with empty subdifferential, so that "semi-algebraic implies KL" becomes false and the goal becomes a statement about a different notion. The KL property is required only at points of $\operatorname{dom}\partial f$ , only on a neighbourhood and only for values in $(f(\hat x),f(\hat x)+\eta)$ ; $\varphi$ is differentiable only on the open interval. Semi-algebraicity of an extended-valued function is that of its graph over its real values. $\eta$ is a positive real, which is equivalent to the paper's $\eta\in(0,\infty]$ .

The hypotheses $\phi=0$ and $\mathcal T_1=0$ are part of the theorem, not a simplification: the analogous statement for the proximal ADMM is open (Remark 4(3)). The cluster point is assumed, not derived.

Needed infrastructure: calculus of the limiting subdifferential (a smooth-plus-separable sum rule), the Tarski–Seidenberg theorem, and the Łojasiewicz/KL inequality for semi-algebraic functions. The last two are reusable far beyond this mission; contributions toward them, and toward the analytic core (milestones 1–6), are welcome.

Selected references

G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. https://arxiv.org/abs/1407.0753 (v6 is the cited version)
H. Attouch, J. Bolte, P. Redont, A. Soubeyran, Proximal alternating minimization and projection methods for nonconvex problems: an approach based on the Kurdyka–Łojasiewicz inequality, Math. Oper. Res. 35(2), 2010. https://doi.org/10.1287/moor.1100.0449
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9
J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4), 2007. https://doi.org/10.1137/050644641
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

17 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization II: The Proximal ADMM Sequence Is Bounded Under CoercivityResearch Paper

Motivation

The alternating direction method of multipliers (ADMM) splits a problem of the form $\min_x h(x) + P(\mathcal M x)$ into a sequence of simpler subproblems, one in which the nonsmooth term $P$ enters only through its proximal map and one in which only the smooth term $h$ appears. For convex problems its convergence theory is classical. In signal processing and statistics, however, the method is routinely run on nonconvex models, such as $\ell_0$ - or $\ell_{1/2}$ -regularized least squares, where $P$ is nonconvex and possibly discontinuous and convex theory does not apply.

Li and Pong (arXiv:1407.0753, SIAM J. Optim. 25(4), 2015) gave a convergence analysis of a proximal variant of the ADMM for this nonconvex setting. Their Theorem 1 shows that every cluster point of the iterates is a stationary point. That statement is only informative if cluster points exist. Theorem 2, the subject of this mission, gives conditions on $h$ , $P$ and $\mathcal M$ under which the whole sequence of iterates is bounded, so that cluster points exist and Theorem 1 applies.

Setting

Let $n, m \ge 0$ . The data are:

$h : \mathbb{R}^n \to \mathbb{R}$ , twice continuously differentiable with bounded Hessian $\nabla^2 h$ ;
$P : \mathbb{R}^m \to (-\infty, +\infty]$ , proper (never $-\infty$ , finite somewhere) and closed (lower semicontinuous);
$\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ linear, with adjoint $\mathcal M^*$ ;
a penalty $\beta > 0$ and a convex, twice continuously differentiable $\phi : \mathbb{R}^n \to \mathbb{R}$ .

The augmented Lagrangian is

L_\beta(x, y, z) = h(x) + P(y) - \langle z, \mathcal M x - y\rangle + \frac{\beta}{2}\|\mathcal M x - y\|^2 ,

and the Bregman distance of $\phi$ is $D_\phi(x_1, x_2) = \phi(x_1) - \phi(x_2) - \langle\nabla\phi(x_2), x_1 - x_2\rangle$ . A sequence $(x^t, y^t, z^t)_{t\ge 0}$ is generated by the proximal ADMM if, from arbitrary $x^0, z^0$ ,

y^{t+1} \in \operatorname*{Arg\,min}_y L_\beta(x^t, y, z^t), \quad x^{t+1} \in \operatorname*{Arg\,min}_x \{L_\beta(x, y^{t+1}, z^t) + D_\phi(x, x^t)\}, \quad z^{t+1} = z^t - \beta(\mathcal M x^{t+1} - y^{t+1}).

For a linear self-map $\mathcal T$ , write $\|x\|^2_{\mathcal T} = \langle x, \mathcal T x\rangle$ , and write $\succeq$ , $\succ$ for the semidefinite and definite order of symmetric maps. Assumption 1 asks for $\sigma > 0$ with $\mathcal M\mathcal M^* \succeq \sigma\mathcal I$ (so $\mathcal M$ is surjective), bounds $\mathcal Q_1 \succeq \nabla^2 h \succeq \mathcal Q_2$ , maps $\mathcal T_1 \succeq \mathcal T_2 \succeq 0$ with $\mathcal T_1^2 \succeq [\nabla^2\phi]^2 \succeq \mathcal T_2^2$ , $\delta > 0$ with $\mathcal Q_2 + \beta\mathcal M^*\mathcal M + \mathcal T_2 \succeq \delta\mathcal I$ , a bound $\mathcal Q_3 \succeq [\nabla^2 h + \nabla^2\phi]^2$ , and $\gamma \in (0,1)$ with

\delta\mathcal I + \mathcal T_2 \succ \frac{2}{\sigma\beta}\Bigl(\frac1\gamma\mathcal Q_3 + \frac1{1-\gamma}\mathcal T_1^2\Bigr).

Formalization targets

Goal: Theorem 2 (p. 11)

Suppose Assumption 1 holds and, with the same $\sigma$ and $\gamma$ , there is $0 < \zeta < 2\beta\gamma$ with

h_0 := \inf_x\Bigl\{h(x) - \frac{1}{\sigma\zeta}\|\nabla h(x)\|^2\Bigr\} > -\infty. \tag{29}

Suppose that either (i) $\mathcal M$ is invertible and $\liminf_{\|y\|\to\infty} P(y) = \infty$ , or (ii) $\liminf_{\|x\|\to\infty} h(x) = \infty$ and $\inf_y P(y) > -\infty$ . Then

\sup_{t \ge 0}\ \bigl(\|x^t\| + \|y^t\| + \|z^t\|\bigr) < \infty .

Milestones

The milestones are the numbered displays of the paper's proof:

Eq. (13): $\mathcal M^* z^{t+1} = \nabla h(x^{t+1}) + \nabla\phi(x^{t+1}) - \nabla\phi(x^t)$ .
Eq. (20): the one-step estimate $L_\beta(w^{t+1}) \le L_\beta(w^t) + \tfrac12\|x^{t+1}-x^t\|^2_{\frac{2}{\sigma\beta\gamma}\mathcal Q_3 - \delta\mathcal I - \mathcal T_2} + \tfrac12\|x^t - x^{t-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}$ for $t \ge 1$ .
Eq. (30): the merit quantity $L_\beta(w^t) + \tfrac12\|x^t - x^{t-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}$ stays below its value at $t = 1$ .
Eq. (31): $\sigma\|z^t\|^2 \le \frac1\gamma\|\nabla h(x^t)\|^2 + \frac1{1-\gamma}\|x^t - x^{t-1}\|^2_{\mathcal T_1^2}$ for $t \ge 1$ .
Eq. (32): a lower estimate of that value at $t = 1$ by $\mu h(x^t) + (1-\mu)h_0 + \frac{c}{\sigma}\|\nabla h(x^t)\|^2 + P(y^t) + \frac\beta2\|\mathcal M x^t - y^t - z^t/\beta\|^2 + \ldots$ , where $c = \frac{1-\mu}{\zeta} - \frac{1}{2\beta\gamma} > 0$ .

Significance

The result. Theorem 2 supplies the existence of cluster points that Theorem 1 assumes. The two together give an unconditional statement: under Assumption 1, (29) and either coercivity condition, the proximal ADMM has a cluster point and every one of them is stationary. The hypotheses cover the models that motivate the paper. Least squares with a coercive nonconvex regularizer falls under case (i) with $\mathcal M = \mathcal I$ , and a strongly convex quadratic $h$ with a regularizer that is bounded below and a general surjective $\mathcal M$ falls under case (ii) (Examples 4–6 of the paper). Boundedness is also a standing hypothesis of the paper's Theorem 3, the Kurdyka–Łojasiewicz argument for convergence of the whole sequence.

Formalizing it. The result has been proved since 2015. As far as a search of the platform shows, neither it nor the underlying Lyapunov-type estimates for the ADMM has been machine-checked. This mission formalizes the known proof. The estimates (20), (30) and (31) are shared with the stationarity analysis of the same algorithm, so they serve any later formal work on nonconvex ADMM variants.

Difficulty

The obvious approach is to bound the iterates by the monotone quantity of Eq. (30). That quantity involves $L_\beta$ , which contains $-\langle z, \mathcal M x - y\rangle$ and is not bounded below a priori, so its decrease alone does not bound anything. The dual term has to be absorbed. It is controlled through $\nabla h(x^t)$ and the last primal step, and the part involving $\|\nabla h(x^t)\|^2$ is then paid for out of $h$ itself. Condition (29) exists to make exactly this trade possible, which is why it couples $\zeta$ to the $\gamma$ of Assumption 1. The two cases then extract boundedness in opposite orders: (i) goes from $y^t$ through $z^t$ to $x^t$ using invertibility of $\mathcal M$ , and (ii) goes from $x^t$ through $z^t$ to $y^t$ . In case (i) the lower bound on $P$ that the argument needs is not assumed and must itself be derived from coercivity and lower semicontinuity.

Formalization scope

Spaces and values. Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and $\mathcal M$ is a continuous linear map with Mathlib's adjoint. $P$ , $L_\beta$ and every inequality containing them live in EReal, stated additively so that no extended-real subtraction occurs.
Assumption 1 is one definition with its witnesses $\sigma, \delta, \gamma, \mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \mathcal Q_3$ as explicit parameters, and $\succeq$ is Mathlib's Loewner order on self-maps. $\|x\|^2_{\mathcal T}$ is $\langle x, \mathcal T x\rangle$ for every $\mathcal T$ , including indefinite ones.
Condition (29) takes $\zeta$ and a real lower bound $h_0$ as parameters, with the same $\sigma$ and $\gamma$ as Assumption 1.
The algorithm is a relation on sequences. An argmin is a global minimizer, not necessarily unique. $x^0$ and $z^0$ are free, and $y^0$ is unconstrained. No existence of minimizers is asserted.
Coercivity is stated in its $\forall r\,\exists R$ form, and "invertible" is bijectivity of $\mathcal M$ .
Boundedness means one radius for all three blocks and all $t \ge 0$ .

Ruling out trivial versions. A formalization that bounds only $x^t$ , fixes $\gamma$ or $\zeta$ to an example's values, lets (29) use a fresh $\gamma$ , adds a lower bound on $P$ in case (i), or assumes minimizers that make the sequence constant proves a different, weaker theorem, and is not the target.

Definitions needed. Proper and closed extended-valued functions, the Hessian as fderiv of gradient, the augmented Lagrangian, the Bregman distance, the proximal-ADMM relation and Assumption 1 are all provided. They mirror the definitions of the companion mission on cluster points of the same algorithm. A solver will need standard facts beyond them: first-order optimality for a differentiable function, the mean-value bound $\|\nabla\phi(a) - \nabla\phi(b)\|^2 \le \|a-b\|^2_{\mathcal T_1^2}$ from the Hessian sandwich, and strong convexity of the $x$ -subproblem. Proofs of individual milestones are welcome independently.

Selected references

G. Li and T. K. Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, SIAM J. Optim. 25(4), 2015; preprint arXiv:1407.0753v6. https://arxiv.org/abs/1407.0753 (DOI 10.1137/140998135)
S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Found. Trends Mach. Learn. 3(1), 2011. https://doi.org/10.1561/2200000016
H. Attouch, J. Bolte and B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Optimal Two- and Three-Stage Production Schedules with Setup Times Included 2: Johnson's Rule for Three MachinesResearch Paper

Motivation

Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: $n$ items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.

The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.

Timeline.

1954: Johnson proves the two-machine rule (Theorem 1) and, for three machines, the reduction to a common ordering (Lemma 3), a closed form for the elapsed time, and optimality of the rule on $A_i + B_i$ , $B_i + C_i$ when $\min A_i \ge \max B_j$ (Theorem 2), with the mirror case $\min C_i \ge \max B_j$ asserted.
1976: Garey, Johnson and Sethi show that minimizing makespan in a three-machine flow shop is strongly NP-hard in general, so some restriction of Theorem 2's kind is unavoidable for an exact ordering rule.

Setting

There are $n$ items and three machines. Item $i$ needs processing time $A_i > 0$ on machine 1, $B_i > 0$ on machine 2 and $C_i > 0$ on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.

A schedule assigns each item start times $s^1_i, s^2_i, s^3_i$ . It is feasible when all start times are at least $0$ on machine 1, the processing intervals of distinct items on the same machine do not overlap, and $s^1_i + A_i \le s^2_i$ , $s^2_i + B_i \le s^3_i$ . The three machines may process the items in different orders. The total elapsed time (makespan) is $\max_i (s^3_i + C_i)$ .

An ordering $\sigma$ lists the items, $\sigma(k)$ being the item in position $k$ . Its as-soon-as-possible schedule processes the items in the order $\sigma$ on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions $1, \dots, n$ , Johnson defines

K_u = \sum_{i=1}^{u} A_i - \sum_{i=1}^{u-1} B_i, \qquad H_v = \sum_{i=1}^{v} B_i - \sum_{i=1}^{v-1} C_i,

the sums running over the items in the first $u$ (resp. $v$ ) positions.

Johnson's three-stage rule says that item $i$ definitely precedes item $j$ when

\min(A_i + B_i,\ C_j + B_j) < \min(A_j + B_j,\ C_i + B_i) \tag{IV}

and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.

Formalization targets

Goal: Theorem 2 (p. 67)

If every $A_i$ is at least every $B_j$ , then an ordering consistent with (IV) exists, and for every such ordering $\sigma$ the as-soon-as-possible schedule of $\sigma$ is feasible and satisfies

\operatorname{makespan}(\text{as-soon-as-possible schedule of } \sigma) \le \operatorname{makespan}(s) \quad \text{for every feasible schedule } s .

Milestones

Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
Closed form (p. 66). For every ordering, the total idle time of machine 3 is $\sum_i Y_i = \max_{1 \le u \le v \le n}(H_v + K_u)$ , so that

\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} (K_u + H_v),

the "maximum walk" of p. 68. 3. Special case (p. 67). If $\min A_i \ge \max B_j$ then $\max_{u \le v} K_u = K_v$ , so the makespan is $\sum_i C_i + \max_v (H_v + K_v)$ . 4. (III) $\Leftrightarrow$ (IV) (p. 67). Interchanging the items in positions $j, j+1$ changes $H$ and $K$ only at $j, j+1$ , and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every $C_i$ is at least every $B_j$ .

Significance

The result. Theorem 2 gives an $O(n \log n)$ exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.

Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).

Difficulty

The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves $\max_{u \le v}(H_v + K_u)$ , and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis $\min A \ge \max B$ is what makes $K$ nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.

Formalization scope

Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with $0$ , so the empty instance has makespan $0$ . An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's $K_{u+1}$ , $H_{v+1}$ . Statements with maxima over positions assume $n \ge 1$ .

Hypotheses made explicit or corrected:

$\min A_i \ge \max B_i$ is read globally, $B_j \le A_i$ for all $i, j$ , as in the section heading. The pointwise reading $B_i \le A_i$ makes Theorem 2 false (an instance with five items is recorded in the Formalization Note of the goal).
Consistency with (IV) is required for all pairs of positions, not only adjacent ones.
Lemma 4 carries Lemma 2's exception for an item indifferent to both others; without it the statement is false.
Lemma 3's proof cites "Lemma 2" where Lemma 1 is meant.
The interchange equivalence (milestone 4) is stated for arbitrary reals, which is stronger than the page needs.

Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form $\sum C + \max(K_u + H_v)$ , would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.

A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.

Selected references

S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117

13 thms2 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

Robustness and Generalization IV: Robustness of the Lasso on a Compact Sample SpaceResearch Paper

Motivation

The Lasso (Tibshirani 1996, doi:10.1111/j.2517-6161.1996.tb02080.x) is $\ell_1$ -penalized least squares regression, one of the standard estimators of statistics and machine learning because it selects sparse coefficient vectors. Explaining why a learned Lasso predictor generalizes is less routine than it looks. The two classical routes are uniform convergence over the hypothesis class and algorithmic stability (Bousquet and Elisseeff 2002, JMLR 2:499–526). The stability route is closed for the Lasso: Xu, Caramanis and Mannor (IEEE Trans. Inf. Theory 56(7), 2010, doi:10.1109/TIT.2010.2048503) showed that its uniform stability bound does not decrease with the sample size, a fact reproduced as Theorem 7 of Xu and Mannor (2012).

Xu and Mannor, Robustness and Generalization (Mach Learn 86 (2012) 391–423, doi:10.1007/s10994-011-5268-1), propose a third route, algorithmic robustness: if the sample space can be split into $K$ cells such that a test point in the same cell as a training point has nearly the same loss, then the algorithm generalizes (their Theorem 1). Their Example 6 shows that the Lasso is robust in this sense, with a number of cells given by a covering number and a robustness level depending on the training responses. This mission formalizes Example 6 together with the general criterion it rests on (Theorem 6) and the Lipschitz estimate for the Lasso loss (Lemma 3).

Setting

A sample is a point $z = (z^{(y)}, z^{(x)})$ with a response $z^{(y)} \in \mathbb R$ and a feature vector $z^{(x)} \in \mathbb R^m$ , so the samples live in $\mathbb R^{m+1}$ . The sample space $\mathcal Z \subseteq \mathbb R^{m+1}$ is a compact set, and $\mathbb R^{m+1}$ carries the norm $\|z\|_\infty = \max(|z^{(y)}|, \max_j |z^{(x)}_j|)$ . A training set is $\mathbf s = (s_1, \dots, s_n) \in \mathcal Z^n$ .

A learning algorithm maps each training set $\mathbf s$ to a hypothesis $\mathcal A_{\mathbf s}$ ; with a loss $l(h, z)$ , it is $(K, \epsilon(\cdot))$ -robust (Definition 2, p. 396) if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$ , fixed independently of the data, such that for every $\mathbf s \in \mathcal Z^n$ , every training point $s \in \mathbf s$ , every $z \in \mathcal Z$ and every $i$ ,

s, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s).

For a metric $\rho$ on $\mathcal Z$ and $\epsilon > 0$ , a set $\hat T \subseteq \mathcal Z$ is an $\epsilon$ -cover of $\mathcal Z$ if every point of $\mathcal Z$ is within distance $\le \epsilon$ of a point of $\hat T$ ; the covering number $\mathcal N(\epsilon, \mathcal Z, \rho)$ is the least cardinality of such a cover (Definition 1, p. 394).

For a coefficient vector $w \in \mathbb R^m$ let $\|w\|_1 = \sum_j |w_j|$ . Given $c > 0$ , the Lasso is

\min_{w} \ \frac1n \sum_{i=1}^n \big(s_i^{(y)} - w^\top s_i^{(x)}\big)^2 + c\|w\|_1, \tag{5}

a Lasso algorithm returns a minimizer $\mathcal A_{\mathbf s} = w$ of (5) for each $\mathbf s$ , and the loss is the absolute prediction error $l(w, z) = |z^{(y)} - w^\top z^{(x)}|$ . Finally $Y(\mathbf s) = \frac1n \sum_{i=1}^n [s_i^{(y)}]^2$ .

Formalization targets

Goal: Example 6 (p. 404)

For every compact $\mathcal Z \subseteq \mathbb R^{m+1}$ , every $c > 0$ , every Lasso algorithm $\mathcal A$ and every $\gamma > 0$ ,

\mathcal A \text{ is } \Big(\mathcal N(\gamma/2, \mathcal Z, \|\cdot\|_\infty),\ \big(Y(\mathbf s)/c + 1\big)\gamma\Big)\text{-robust}.

The statement holds for every selection of a minimizer, since (5) need not have a unique solution.

Milestones

Optimality bound (proof of Lemma 3, p. 419): every Lasso solution satisfies $\|w^*\|_1 \le \frac{1}{nc} \sum_{i=1}^n [s_i^{(y)}]^2$ .
Lemma 3 (p. 419): for all $z_a, z_b \in \mathbb R^{m+1}$ ,

|l(w^*(\mathbf s), z_a) - l(w^*(\mathbf s), z_b)| \le \Big[\frac{1}{nc} \sum_{i=1}^n [s_i^{(y)}]^2 + 1\Big] \|z_a - z_b\|_\infty.

Theorem 6 (p. 402): for a metric $\rho$ on $\mathcal Z$ and $\gamma > 0$ , if $|l(\mathcal A_{\mathbf s}, z_1) - l(\mathcal A_{\mathbf s}, z_2)| \le \epsilon(\mathbf s)$ whenever $z_1 \in \mathbf s$ and $\rho(z_1, z_2) \le \gamma$ , and $\mathcal N(\gamma/2, \mathcal Z, \rho) < \infty$ , then $\mathcal A$ is $(\mathcal N(\gamma/2, \mathcal Z, \rho), \epsilon(\cdot))$ -robust.

Significance

Combined with Theorem 1 of the same paper, Example 6 yields a generalization bound for the Lasso of the form $\epsilon(\mathbf s) + M\sqrt{(2K\ln 2 + 2\ln(1/\delta))/n}$ with $K$ a covering number of the sample space, a bound that uses no stability of the algorithm and no uniqueness of the minimizer. Theorem 6 is the reusable part: it converts any data-dependent local Lipschitz or continuity estimate of the loss into robustness, and the paper derives its examples for the SVM, the Lasso, neural networks and PCA from it. The authors note (p. 404) that the resulting bound is weaker than VC-dimension bounds for linear predictors, since it depends exponentially on the dimension; the value of the example is the method, not the rate.

The results are proved in the paper, with short arguments. No machine-checked version of Theorem 6, Lemma 3 or Example 6 is known to exist. The formal work is to connect Mathlib's covering numbers to partitions of a set, to handle the $\ell_1$ / $\ell_\infty$ pairing on $\mathbb R \times \mathbb R^m$ , and to state robustness so that later missions of this series (the generalization bound of Theorem 1, mission I) can consume it.

Difficulty

The constant in the robustness level depends on the training set through $Y(\mathbf s)$ , while the partition in Definition 2 must be chosen before the training set is seen. A formalization that lets the cells depend on $\mathbf s$ proves a much weaker, nearly empty statement, so the data dependence has to be carried entirely by $\epsilon(\mathbf s)$ and the cells must depend only on $\mathcal Z$ and $\gamma$ . A cover by balls is not a partition, and the radius of the cover ( $\gamma/2$ ) and the closeness threshold in Theorem 6 ( $\gamma$ ) differ by the factor that the diameter of a cell requires. The Lipschitz estimate must bound a Lasso solution without any information beyond optimality, and the pairing between $\|w\|_1$ and $\|\cdot\|_\infty$ is the one that makes the constant come out as printed; a Euclidean norm on either side gives a different constant.

Formalization scope

$\mathbb R^{m+1}$ is ℝ × (Fin m → ℝ), a point being (z^{(y)}, z^{(x)}). Lean's norm on this product is the maximum of the absolute values of all coordinates, which is exactly $\|\cdot\|_\infty$ . $\|w\|_1$ is written out as $\sum_j |w_j|$ , since the default norm on Fin m → ℝ is the sup norm; $w^\top x$ is dotProduct w x.
The sample space is a set Z with IsCompact Z. Robustness (IsRobustOn) asks for cells C : Fin K → Set α that lie in Z, cover Z and are pairwise disjoint (empty cells allowed), chosen before the universally quantified training set; training sets are maps Fin n → α with all points in Z. No measurability is involved anywhere in this mission.
The covering number is Mathlib's Metric.coveringNumber at radius Real.toNNReal (γ / 2): closed balls, centres in Z (the metric space of Definition 1 is $\mathcal Z$ itself), value in ℕ∞, converted with toNat. Theorem 6 assumes its finiteness, as the paper does; without that hypothesis toNat would return $0$ and the statement would be false for nonempty Z. Example 6 does not assume it: it follows from compactness.
A Lasso algorithm is any function A with ∀ s, IsLassoSolution c s (A s); it is not defined by a choice of minimizer. The regularization parameter satisfies $c > 0$ , which the paper leaves implicit. The factor $1/n$ is a real division; for $n = 0$ it is $0$ in Lean, the objective reduces to $c\|w\|_1$ , and all statements remain true.
The robustness level is $(Y(\mathbf s)/c + 1)\gamma$ in Example 6 and $\frac{1}{nc}\sum_i [s_i^{(y)}]^2 + 1$ in Lemma 3, each in its printed form.

Useful infrastructure beyond this mission: a lemma turning a finite cover of a set into a partition of it with cells of diameter at most twice the radius, and finiteness of Mathlib's internal covering number for compact sets. Contributions of either as separate theorems are welcome.

Selected references

H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. doi:10.1007/s10994-011-5268-1
R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society, Series B 58(1) (1996) 267–288. doi:10.1111/j.2517-6161.1996.tb02080.x
H. Xu, C. Caramanis and S. Mannor, Robust Regression and Lasso, IEEE Transactions on Information Theory 56(7) (2010) 3561–3574. doi:10.1109/TIT.2010.2048503
O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. jmlr.org/papers/v2/bousquet02a

7 thms2 active usersReviewed

Algorithmic Game Theory Convex Optimization Operations Research·Captain: mikedeng1

Value of Information in Bayesian Routing Games II: Equilibrium Adoption Rates of Information Systems Are the Minimizers of the Equilibrium PotentialResearch Paper

Motivation

Traffic information systems (TIS) such as navigation apps send drivers private, noisy signals about the state of the road network: incidents, weather, closures. When several such systems coexist, their subscribers act on different information, and the congestion each population experiences depends on how all of them route. A question then arises for transport planners and for the information providers themselves: if travelers are free to choose which system to subscribe to, which market shares of the competing systems are stable?

Wu, Amin and Ozdaglar (Operations Research 69(1):148–163, 2021; preprint arXiv:1808.10590) model this situation as a Bayesian routing game with heterogeneous information and answer the question exactly: the equilibrium adoption rates are the minimizers of a convex function of the population sizes, the equilibrium value of a weighted potential. This mission formalizes that characterization (Theorem 4 of the paper) together with the results its proof rests on. A companion mission (Value of Information in Bayesian Routing Games I) formalizes the paper's other main result, the sign and monotonicity of the relative value of information between two populations.

Setting

A Bayesian routing game $\Gamma(\lambda)$ has a single origin–destination pair, a finite set of edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$ (each route a set of edges), and a finite set of network states $\mathcal S$ . Travelers of total demand $D>0$ are split into populations $i\in\mathcal I$ , one per TIS; population $i$ has size $\lambda^iD$ , where the size vector $\lambda$ lies in the simplex $\Delta=\{\lambda:\lambda^i\ge0,\ \sum_i\lambda^i=1\}$ . Each population receives a signal (its type) $t^i$ from a finite set $\mathcal T^i$ ; states and type profiles $t=(t^i)_i$ are drawn from a common prior $\pi\in\Delta(\mathcal S\times\mathcal T)$ . Edge $e$ in state $s$ has cost $c^s_e(w)$ at load $w$ , positive, strictly increasing and differentiable.

A strategy profile $q$ assigns to each population and type a split $q^i_r(t^i)\ge0$ of its demand over routes, with $\sum_rq^i_r(t^i)=\lambda^iD$ ; these form the polytope $\mathcal Q(\lambda)$ . It induces route flows $f_r(t)=\sum_iq^i_r(t^i)$ and edge loads $w_e(t)=\sum_{r\ni e}f_r(t)$ . A traveler of population $i$ with signal $t^i$ forms the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$ and evaluates the expected route cost $\mathbb E[c_r(q)\mid t^i]=\sum_{s,t^{-i}}\sum_{e\in r}\beta^i(s,t^{-i}\mid t^i)\,c^s_e(w_e(t))$ . A Bayesian Wardrop equilibrium (BWE) is a $q\in\mathcal Q(\lambda)$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is

C^{i*}(\lambda)=\sum_{t^i\in\mathcal T^i}\Pr(t^i)\min_{r\in\mathcal R}\mathbb E[c_r(q^*)\mid t^i].

The weighted potential is $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$ , and $\Psi(\lambda)=\min_{q\in\mathcal Q(\lambda)}\Phi(q)$ is its equilibrium value. In route-flow form, $\widehat\Phi(f)$ is the same expression in terms of $f$ ; route flows satisfy linear constraints (14a)–(14c) (a separability condition across populations, total demand $D$ , nonnegativity) and one information impact constraint per population, $\widehat J^i(f)\le\lambda^iD$ , where $\widehat J^i(f)=D-\sum_r\min_{t^i}f_r(t^i,\widehat t^{-i})$ measures how much of the demand reacts to population $i$ 's signal. Let $\mathcal F^\dagger$ be the set of minimizers of $\widehat\Phi$ subject to (14a)–(14c) only, and

\Lambda^\dagger=\{\lambda\in\Delta:\ \exists f^\dagger\in\mathcal F^\dagger,\ \widehat J^i(f^\dagger)\le\lambda^iD\ \ \forall i\}.

In the two-stage game, travelers first choose a TIS, inducing $\lambda$ , and then play $\Gamma(\lambda)$ . A size vector is a vector of equilibrium adoption rates if no traveler gains by switching TIS:

\lambda^i>0\ \Longrightarrow\ C^{i*}(\lambda)=\min_{j\in\mathcal I}C^{j*}(\lambda)\qquad\forall i\in\mathcal I.\tag{31}

Formalization targets

Goal: Theorem 4

For every $\lambda\in\Delta$ and every BWE of $\Gamma(\lambda)$ ,

(31)\ \text{holds}\iff\lambda\in\Lambda^\dagger .

With the existence of a BWE for every $\lambda\in\Delta$ , this is the paper's statement that the set of equilibrium adoption rates is $\Lambda^\dagger$ .

Milestones

Theorem 1. $q$ is a BWE of $\Gamma(\lambda)$ iff $q$ minimizes $\Phi$ over $\mathcal Q(\lambda)$ ; the equilibrium edge load $w^*(\lambda)$ is unique.
Proposition 2. A route flow in the flow polytope $\mathcal F(\lambda)$ ((14a)–(14c) plus all information impact constraints) is an equilibrium flow iff it minimizes $\widehat\Phi$ over $\mathcal F(\lambda)$ .
Lemma 5. $\Psi$ is convex on $\Delta$ , and with $z^{ij}=e_i-e_j$ and $V^{ij*}=C^{j*}-C^{i*}$ ,

\lim_{\epsilon\to0^+}\frac{\Psi(\lambda+\epsilon z^{ij})-\Psi(\lambda)}{\epsilon}=-D\,V^{ij*}(\lambda).

Proposition 5. $\Lambda^\dagger$ is convex, $\Lambda^\dagger=\operatorname{argmin}_{\lambda\in\Delta}\Psi(\lambda)$ , and the equilibrium edge load equals the size-independent load $w^\dagger$ of $\mathcal F^\dagger$ iff $\lambda\in\Lambda^\dagger$ .

A separate item states the existence of a BWE for every $\lambda\in\Delta$ .

Significance

The result. Theorem 4 reduces a question about a two-stage game with a continuum of travelers and private signals to the minimization of one convex function over a simplex. It shows that the stable market shares form a convex set, generally not a single point, so each system's equilibrium adoption rate ranges over an interval; and that this set is determined by the joint information environment of all systems, not by each system's signal alone. On $\Lambda^\dagger$ the equilibrium edge load does not depend on the shares at all, which identifies when changes in market shares leave congestion unchanged.

Formalizing it. The proofs of Theorem 1, Proposition 2 and Proposition 5 are in the paper's online e-companion, and Lemma 5 relies on sensitivity results for parametric convex programs cited from the literature. No part of this development has, to our knowledge, been machine-checked. A complete formalization would produce a verified potential-game characterization of Bayesian Wardrop equilibria with heterogeneous information and a verified directional-derivative formula for the optimal value of a parametric convex program; nothing comparable is currently on the platform (the existing Wardrop development covers complete information only).

Difficulty

The direction " $\lambda\in\Lambda^\dagger$ implies (31)" is not a pointwise statement about costs: it follows from $\Lambda^\dagger$ being the argmin of $\Psi$ together with the formula linking directional derivatives of $\Psi$ to cost differences. Both are hard. The derivative formula (26) is a statement about the optimal value of a convex program whose feasible set moves with $\lambda$ ; its standard proofs pass through uniqueness of Lagrange multipliers, which fails exactly at the degenerate size vectors ( $\lambda^i=0$ ) that Theorem 4 must cover, since an unused TIS is a legitimate outcome. The identity $\Lambda^\dagger=\operatorname{argmin}\Psi$ needs the route-flow reformulation (Proposition 2), in which the size vector enters only through the information impact constraints, and the uniqueness of the minimizing edge load. The natural first idea, comparing population costs directly at a given equilibrium, gives no handle on which size vectors make them equal.

Formalization scope

The Lean development lives in the namespace BayesRouting.Adoption. Populations, types, states, edges and routes are finite types; type spaces and the route set are nonempty; routes are edge sets. The game is a structure whose fields include the paper's standing assumptions: the prior is a probability distribution, $D>0$ , and each cost is positive on nonnegative loads, strictly increasing and differentiable (on all of $\mathbb R$ , which loses no generality). One assumption is added: every type profile has positive probability. Without it the equilibrium edge load need not be unique and the beliefs can be undefined; it excludes the paper's Example 2(i) (perfectly correlated signals).

Conventions: size vectors range over the probability simplex; $\Psi$ is the infimum of $\Phi$ over $\mathcal Q(\lambda)$ and is only compared at points of the simplex (outside it the feasible set can be empty and the value is a default); $C^{i*}$ is the last form of the paper's (7), well defined when $\lambda^i=0$ ; $\widehat J^i$ is the maximum over reference profiles, which equals the paper's value on flows satisfying (14a); equilibrium statements are made for every BWE rather than for "the" equilibrium; $\mathcal F^\dagger$ and similar sets are argmin sets. Lemma 5 is stated for the directions $z^{ij}$ with $\lambda^j>0$ (otherwise $\lambda+\epsilon z^{ij}$ leaves the simplex); $\lambda^i=0$ is allowed.

A trivializing formalization is ruled out: the existence of a BWE is its own item, so "for every BWE" is not vacuous, and $\Lambda^\dagger$ is defined by (30) from the flow problem (28), not as the argmin of $\Psi$ , so the goal is not a restatement of Proposition 5.

Infrastructure a complete development needs: KKT conditions for convex programs with linear constraints, convexity of integrals of increasing functions, compactness arguments for existence of minimizers, and one-sided directional derivatives of optimal-value functions. The last two are reusable well beyond this mission. Proofs of any item, and of auxiliary lemmas such as Proposition 1 of the paper (feasible route flows form the polytope $\mathcal F(\lambda)$ ), are welcome.

Selected references

M. Wu, S. Amin, A. E. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999 (preprint: https://arxiv.org/abs/1808.10590)
W. H. Sandholm, Potential games with continuous player sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
A. V. Fiacco, J. Kyparisis, Convexity and concavity properties of the optimal value function in parametric nonlinear programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986. https://doi.org/10.1007/BF00938592

9 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Probability·Captain: mikedeng1

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program II: Stability of the Deterministic Equivalent Convex ProgramResearch Paper

Motivation

A two-stage stochastic linear program with fixed recourse chooses a first-stage decision $x$ before a random vector $\xi$ is observed, and then pays for a cheapest corrective action $y$ once $\xi$ is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.

Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of $x$ (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.

Setting

The data are a random element $\xi=(c,q,p,T)$ with $c\in\mathbb R^n$ , $q\in\mathbb R^{\bar n}$ , $p\in\mathbb R^{\bar m}$ and $T$ an $\bar m\times n$ matrix, distributed according to a probability measure $\mu$ . The recourse matrix $W$ ( $\bar m\times\bar n$ ), the first-stage matrix $A$ ( $m\times n$ ) and $b\in\mathbb R^m$ are fixed. The recourse function is

Q(x,\xi)=\min\{q(\xi)y \mid Wy=p(\xi)-T(\xi)x,\ y\ge0\},

equal to $+\infty$ if the second-stage program is infeasible and $-\infty$ if it is unbounded.

The weak covariance condition (Definition 2.2) requires $c_j$ , $q_jp_i$ and $q_jt_{ik}$ to be integrable for all indices; it does not require $q$ , $p$ or $T$ themselves to be integrable. The paper also assumes throughout that $W$ has full row rank (p. 312).

Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and $(+\infty)+(-\infty)=+\infty$ . The expected recourse is $\mathcal Q(x)=E_\xi\{Q(x,\xi)\}$ and the objective is

Z(x)=\bar c\,x+\mathcal Q(x),\qquad \bar c=E_\xi\{c(\xi)\}.

The induced constraints are $K_2=\bigcap_{\zeta\in\tilde\Xi_{p,T}}\{x : p-Tx\in\operatorname{pos}W\}$ , where $\operatorname{pos}W=\{Wy:y\ge0\}$ and $\tilde\Xi_{p,T}$ is the support of the distribution of $(p,T)$ . The fixed constraints are $K_1=\{x: Ax=b,\ x\ge0\}$ , and $K=K_1\cap K_2$ . The deterministic equivalent program (8.2) is to minimize $Z$ over $K$ .

A convex program of the form $\min\{f(x) : Ax=b,\ x\ge0,\ x\in D\}$ with finite value $v$ is stable (Definition 8.1(iv)) if there is $\pi\in\mathbb R^m$ with $v\le f(x)+\pi(b-Ax)$ for all $x\in D$ , $x\ge0$ . Equivalently, the dual obtained by perturbing $b$ is solvable and has no duality gap.

Formalization targets

Goal: Theorem 8.11 (p. 337)

If the weak covariance condition holds, $W$ has full row rank, $K_2$ is a polyhedron and the program is finite, $v=\inf_K Z\in\mathbb R$ , then

\exists\,\pi\in\mathbb R^m:\quad v\le Z(x)+\pi\,(b-Ax)\quad\text{for all }x\in K_2,\ x\ge0 .

Milestones

Corollary 7.3 (p. 328). The value $t\mapsto\min\{cx\mid Ax=t,\ x\ge0\}$ is a finite maximum of affine functions on $\operatorname{pos}A$ , or $-\infty$ on all of $\operatorname{pos}A$ .
Proposition 7.5 (p. 329). $Q(x,\xi)$ is convex polyhedral in $x$ on $K_2$ for each $\xi$ in the support, concave polyhedral in $q$ , and convex polyhedral in $(p,T)$ .
Theorem 7.6 (p. 329). $Z$ is convex on $K$ , and it is either finite on $K$ or identically $-\infty$ on $K$ .
Theorem 7.7 (pp. 329–330). If $Z>-\infty$ on $K$ , then $|Z(x)-Z(x^0)|\le\bar B\|x-x^0\|$ on $K$ (Euclidean norm).
Lemma 8.9 (p. 337). A finite program $\min\{f(x): Ax=b,\ x\ge0\}$ whose objective is convex and Lipschitz on a polyhedral domain is stable.

Significance

Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function $\phi(u)=\inf\{Z(x) : Ax=b-u,\ x\in K_2\cap\mathbb R^n_+\}$ at $u=0$ , and hence a bounded rate of change of the optimal value under perturbations of $b$ . The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically $-\infty$ on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.

The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on $K_2$ for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.

Difficulty

The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of $Q(\cdot,\xi)$ . It fails unless that constant is integrable, and the weak covariance condition, not integrability of $\xi$ , is what has to deliver this, uniformly over the finitely many second-stage bases.

For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of $Z$ has curved boundary, the perturbation function can have infinite slope at $0$ ; the polyhedral hypothesis on $K_2$ is what excludes this.

Formalization scope

Types. Vectors are Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper ( $c$ , $q$ , $\pi$ ) enter through dotProduct. The law $\mu$ is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). $Q$ is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.
The integral. $\mathcal Q$ is written as lintegral of the positive part minus lintegral of the negative part, with $+\infty$ whenever the positive part is $+\infty$ . This is the paper's $(+\infty)+(-\infty)=+\infty$ ; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be $0$ for non-integrable integrands and make every expected-cost statement trivial, and it is not used. $\bar c$ is a Bochner integral, legitimate because Definition 2.2 makes each $c_j$ integrable.
Readings of informal words.
- "Has first moments" is Integrable.
- "Convex polyhedron" means finitely many weak linear inequalities; $\emptyset$ and $\mathbb R^n$ are included.
- "Finite convex (concave) polyhedral function on $S$ " means equal on $S$ to the maximum (minimum) of finitely many affine functions. The $x$ and $(p,T)$ parts of Proposition 7.5 are stated as a dichotomy with the identically $-\infty$ case; the $q$ part is stated, as Corollary 7.4 gives it, as finite concave polyhedral on $\operatorname{pos}(W^T,-W^T,I)$ when the recourse problem is feasible.
- "Convex" for the extended-real $Z$ (Theorem 7.6) is ConvexOn of toReal on the finite branch.
- "Bounded on $K$ " (Theorem 7.7) is read as $Z>-\infty$ on $K$ , the proof's own reading. Finiteness on $K$ is part of the conclusion.
- "Convex and Lipschitz on a polyhedron" (Lemma 8.9) means the objective's domain is the polyhedron.
- "The program is finite" means the infimum over $K$ is a real number.
- "Stable" is the Kuhn–Tucker form above: a multiplier compared against the primal value, not merely a solvable dual. The latter would allow a duality gap.
Standing assumptions. Full row rank of $W$ appears in Theorems 7.7 and 8.11, where the proof uses square nonsingular submatrices of $W$ . It is omitted from Theorem 7.6 and Corollary 7.3 (Theorem 7.2's rank assumption), where it is not needed; this makes those statements stronger.
Corrections to the page. Theorem 8.11 is printed with " $K$ is polyhedral", $K=K_1\cap K_2$ , and read literally it is false. Take $T(\xi)$ uniform on the unit circle, $p\equiv1$ , $W=(1)$ , $q\equiv0$ , $c\equiv(-1,0)$ and $K_1=\{x_2=1,\ x\ge0\}$ . Then $K_2$ is the unit disk and $K=\{(0,1)\}$ is polyhedral with finite value $0$ , but no multiplier exists. The goal therefore assumes " $K_2$ is polyhedral", as the sentence before Lemma 8.9 and the proof require. In the dual (8.3) the page writes $c$ for $\bar c$ .
Ruled out. A statement of stability as "the dual supremum is attained" without equality to the primal value is not the goal, and neither is a hypothesis making $K$ empty or $Z$ identically $-\infty$ : the finiteness hypothesis excludes both.
Infrastructure. The needed pieces are Minkowski–Weyl for polyhedra (PointedCone.FG/DualFG in Mathlib), LP duality with $\pm\infty$ values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.

Selected references

R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
D. W. Walkup and R. J.-B. Wets, Stochastic programs with recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
R. M. Van Slyke and R. J.-B. Wets, A duality theory for abstract mathematical programs with applications to optimal control theory, J. Math. Anal. Appl. 22(3):679–706, 1968 (cited by Wets for Definition 8.1 and the dual (8.3)).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 3. https://doi.org/10.1007/978-1-4614-0237-4

10 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program I: The Induced Feasibility Region Is a Closed Convex Polyhedron When T Is FixedResearch Paper

Motivation

A two-stage stochastic program with recourse is a linear program in which a decision $x$ is taken before a random vector $\xi$ is observed, and a corrective (recourse) decision $y$ is taken afterwards at a cost. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning, energy dispatch and inventory models are routinely written this way. Before any algorithm can be applied, the model has to be reduced to a deterministic equivalent program in $x$ alone, and the first question is which $x$ are admissible at all: the random second-stage constraints induce constraints on $x$ that are not written down anywhere in the data.

Roger J.-B. Wets's survey (SIAM Review 16(3), 1974) settled this question for fixed recourse (the recourse matrix $W$ is not random) under a weak moment condition on the data. Its §4 shows that the natural definitions of the induced feasibility region agree, that the region is always closed and convex, and that it is a polyhedron, described by finitely many deterministic linear inequalities, whenever the technology matrix $T$ is fixed. The last fact is what makes decomposition methods such as the L-shaped method of Van Slyke and Wets (1969) terminate with finitely many feasibility cuts.

Timeline: Dantzig (1955) and Beale (1955) introduce linear programs under uncertainty, under assumptions that make every $x$ feasible (relatively complete recourse). Wets (1966) and Kall (1966) begin studying the feasibility region without that assumption; Wets (1966c) introduces the polar matrix used for the polyhedrality result. Walkup and Wets (1967) treat random $W$ . The 1974 survey collects these results in the form formalized here.

Setting

The data are a fixed real $\bar m \times \bar n$ matrix $W$ and a random vector $\xi = (c, q, p, T)$ with $c \in \mathbb{R}^n$ , $q \in \mathbb{R}^{\bar n}$ , $p \in \mathbb{R}^{\bar m}$ and $T$ an $\bar m \times n$ matrix. The law of $\xi$ is a probability measure $\mu$ on the product space, and its support $\tilde\Xi$ is the smallest closed set of measure one. The recourse function is

Q(x,\xi) = \min\{\, q(\xi)y \mid Wy = p(\xi) - T(\xi)x,\ y \ge 0 \,\},

equal to $+\infty$ when the program is infeasible and $-\infty$ when it is unbounded below. The expected recourse $\mathcal Q(x) = E_\xi\{Q(x,\xi)\}$ uses the paper's integral: the sum of the positive part $\int Q^+ d\mu \in [0,+\infty]$ and the negative part $-\int Q^- d\mu \in [-\infty,0]$ , with $(+\infty) + (-\infty) = +\infty$ .

The weak covariance condition (Definition 2.2) asks that $c_j$ , $q_j p_i$ and $q_j t_{ik}$ be integrable for all $i, j, k$ . Write $\operatorname{pos} W = \{Wy \mid y \ge 0\}$ . The candidate feasibility sets for the induced constraints are

$K_2^\mu$ : the $x$ for which, with probability one, some $y \ge 0$ solves $Wy = p(\xi) - T(\xi)x$ ;
$K_2^p$ : the $x$ for which such a $y$ exists for every $\xi \in \tilde\Xi$ ;
$K_2^s = \{x \mid \mathcal Q(x) < +\infty\}$ ;
$K_2 = \bigcap_{\zeta \in \tilde\Xi_{p,T}} K_2(\zeta)$ , where $\tilde\Xi_{p,T}$ is the support of the law of $(p,T)$ and $K_2(\zeta) = \{x \mid p - Tx \in \operatorname{pos} W\}$ for $\zeta = (p,T)$ .

A convex polyhedron is a set $\{x \mid Gx \ge \alpha\}$ given by finitely many linear inequalities; $\emptyset$ and $\mathbb{R}^n$ are polyhedra.

Formalization targets

Goal: Theorem 4.10

If $T$ is fixed and $\xi$ satisfies the weak covariance condition, then

K_2 = \{x \in \mathbb{R}^n \mid Gx \ge \alpha\} \quad \text{for some finite system } G, \alpha,

so $K_2$ is a closed convex polyhedron. The number of inequalities is not fixed in advance, and $K_2$ may be empty.

Milestones

Theorem 4.1. Under weak covariance, $K_2^\mu = K_2^p = K_2^s$ .
Corollary 4.5. Under weak covariance, $K_2 = K_2^p = K_2^\mu = K_2^s$ .
Theorem 4.6. For every set $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$ , $K_2 = \bigcap_{\zeta \in \Sigma} K_2(\zeta)$ .
Theorem 4.7. $K_2$ is closed and convex; if the closed positive hull $\operatorname{pos}(\tilde\Xi_{p,T})$ is a convex polyhedral cone, $K_2$ is a convex polyhedron.

Significance

Theorem 4.1 and Corollary 4.5 show that three different notions of second-stage feasibility (almost sure, on the support, finite expected cost) coincide, and that feasibility depends only on the distribution of $(p, T)$ . This justifies computing the feasibility region from the support alone, which is what feasibility-cut algorithms do. Theorem 4.7 guarantees that the deterministic equivalent program is a convex program over a closed convex set, with no moment condition. Theorem 4.10 shows that with a fixed technology matrix the induced constraints are finitely many linear inequalities, even when $p(\xi)$ has an unbounded continuous distribution, so the deterministic equivalent program has a polyhedral feasible region.

The results are classical and proved in the paper. None of them is formalized on Prove2Me for a general distribution. The platform has the finite-scenario analogue of Theorem 4.7's first part, StochasticProg.Recourse.thm5a_K2_closed_convex (Birge and Louveaux, Ch. 3, Thm 5(a)), for finitely many scenarios; it is related work, not a special case in the Lean sense, because its model differs. The mission produces a machine-checked account of the measure-theoretic part (supports, pushforwards, an extended-valued integral with a nonstandard convention) and of the polyhedral part (Minkowski–Weyl for cones).

Difficulty

Two steps resist the obvious approach. First, $K_2^p \subseteq K_2^s$ needs an integrable upper bound for the positive part of $Q(x,\cdot)$ on the whole support. $Q$ is only piecewise linear in $\xi$ , can equal $-\infty$ , and $q$ , $p$ , $T$ are not assumed integrable separately, so no single dominating function is at hand; only the products controlled by the weak covariance condition are integrable. Second, Theorem 4.10 intersects infinitely many polyhedra $K_2(\zeta)$ , and an infinite intersection of polyhedra is in general only closed and convex (Theorem 4.7). Showing that finitely many inequalities suffice without any assumption on the shape of the support of $p$ is the content of the goal, and the resulting system may be inconsistent, in which case $K_2 = \emptyset$ .

Formalization scope

Vectors are Fin k → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; the paper's row vectors and suppressed transposes become Matrix.mulVec. The data space is $\mathbb{R}^n \times \mathbb{R}^{\bar n} \times \mathbb{R}^{\bar m} \times \mathbb{R}^{\bar m \times n}$ with its Borel structure, and $\mu$ is a probability measure on the whole space (the paper's sample space $\Xi$ only carries $\mu$ ). Readings fixed by the formalization:

"has first moments" (Def. 2.2) is Integrable with respect to $\mu$ .
The integral is the paper's: two lower Lebesgue integrals, returning $+\infty$ whenever the positive part diverges. Mathlib's EReal subtraction ( $\top - \top = \bot$ ) and the Bochner integral of toReal (zero for non-integrable functions) would both make $K_2^s$ wrong and are not used.
"support" is Mathlib's Measure.support; $\tilde\Xi_{p,T}$ is the support of the pushforward under the (continuous, hence measurable) projection onto $(p,T)$ .
" $T$ is fixed" means $T(\xi) = T_0$ with probability one, a weaker hypothesis than pointwise constancy.
"convex polyhedron" is the solution set of finitely many weak linear inequalities, the number of them existentially quantified; "convex polyhedral cone" is the conic hull of finitely many vectors; "closed positive hull" is the closure of the conic hull.
Full row rank of $W$ is the paper's standing assumption (p. 312) and is carried as a hypothesis of Theorem 4.1, Corollary 4.5 and Theorem 4.10; it is inessential for them.
Theorem 4.6 is stated as "for every $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$ ". The literal statement fails: a closed half-plane has no extreme points, so the "inverse of convex closure" would give $\Sigma = \emptyset$ and an intersection equal to $\mathbb{R}^n$ .
The set on p. 314 (iii) is printed $K_2^p$ .

A trivializing formalization is ruled out: a polyhedron indexed by an arbitrary type or by the support would make Theorem 4.10 a restatement of the first part of Theorem 4.7, and a Bochner-integral $\mathcal Q$ would make $K_2^s = \mathbb{R}^n$ . Neither is used.

A complete development needs Minkowski–Weyl for finitely generated cones (available in Mathlib as PointedCone.FG / DualFG), closedness of finitely generated cones, supports of pushforward measures, and simplicial covers of $\operatorname{pos} W$ (Carathéodory). The support and integral lemmas are reusable for every result about recourse functions with general distributions; contributions of such lemmas as separate theorems are welcome.

Selected references

R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
R. M. Van Slyke and R. J.-B. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Ch. 3. https://doi.org/10.1007/978-1-4614-0237-4

8 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research·Captain: mikedeng1

A New Projection Method for Variational Inequality Problems: The Hyperplane Projection Method Converges to a Solution Under Continuity and Generalized MonotonicityResearch Paper

Motivation

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. The format covers the first-order optimality conditions of constrained optimization, nonlinear complementarity problems, traffic and economic equilibria (Wardrop, Walrasian, Nash–Cournot), and systems of nonlinear equations; see Harker and Pang's survey (Math. Programming 48, 1990) and Facchinei and Pang's monograph (Springer, 2003).

When the map has no special structure (not strongly monotone, not Lipschitz with known constant, not affine) and the feasible set is a general closed convex set, the practical algorithms are projection methods. The oldest is Korpelevich's extragradient method (1976). Without a known Lipschitz constant, extragradient-type methods need a linesearch in which every trial point costs one projection onto the feasible set, and projection onto a general convex set is itself an optimization problem.

Solodov and Svaiter (SIAM J. Control Optim. 37 (1999) 765–776) proposed a method that spends exactly two projections per iteration, whatever the linesearch does, and proved global convergence under only continuity of the map and a generalized monotonicity condition weaker than pseudomonotonicity. The method, often called the hyperplane projection method, is a standard reference point for later projection and extragradient-type algorithms.

Timeline:

1976: Korpelevich, extragradient method, Lipschitz monotone maps.
1987–1994: Khobotov (1987), Iusem (1994) and others: extragradient variants with Armijo-type stepsize rules, which need one projection per trial step.
1997: Iusem and Svaiter, a separating-hyperplane variant of extragradient for monotone maps (reference [9] of the paper).
1999: Solodov and Svaiter, Algorithm 2.1: two projections per iteration, convergence under condition (1.2) below.

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $C \subseteq \mathbb{R}^n$ be closed and convex and $F : \mathbb{R}^n \to \mathbb{R}^n$ continuous. The problem $\mathrm{VI}(F, C)$ is to find $x^*$ with

x^* \in C, \qquad \langle F(x^*), x - x^*\rangle \ge 0 \quad \text{for all } x \in C. \tag{1.1}

Its solution set is $S$ . The projection onto a nonempty closed convex set $K$ is $P_K[x] := \arg\min_{y \in K}\|y - x\|$ . The projected residual is $r(x) := x - P_C[x - F(x)]$ ; its zeros are exactly the points of $S$ .

Condition (1.2) requires, for every $x^* \in S$ ,

\langle F(x), x - x^*\rangle \ge 0 \qquad \text{for all } x \in C. \tag{1.2}

It holds when $F$ is monotone or pseudomonotone, and in cases where $F$ is neither.

Algorithm 2.1. Fix $\gamma, \sigma \in (0,1)$ and $x^0 \in C$ . Given $x^i$ : if $r(x^i) = 0$ , stop. Otherwise let $k_i$ be the smallest nonnegative integer $k$ with

\langle F(x^i - \gamma^k r(x^i)), r(x^i)\rangle \ge \sigma\|r(x^i)\|^2, \tag{2.1}

set $\eta_i = \gamma^{k_i}$ , $z^i = x^i - \eta_i r(x^i)$ , $H_i = \{x \mid \langle F(z^i), x - z^i\rangle \le 0\}$ , and

x^{i+1} = P_{C \cap H_i}[x^i].

The hyperplane $\partial H_i$ separates $x^i$ from $S$ .

Formalization targets

Goal: Theorem 2.1

If $C$ is closed and convex, $F$ is continuous, $S \ne \emptyset$ and (1.2) holds, then every sequence generated by Algorithm 2.1 converges to a single point of $S$ :

\exists\, \hat x \in S:\quad x^i \to \hat x \quad (i \to \infty).

The theorem fixes no rate and no constant; it asserts convergence of the whole sequence, not only of a subsequence.

Milestones (in attack order)

Lemma 2.1 (p. 768): for nonempty closed convex $B$ , $\langle x - P_B[x], z - P_B[x]\rangle \le 0$ for $z \in B$ , and $\|P_B[x]-P_B[y]\|^2 \le \|x-y\|^2 - \|P_B[x]-x+y-P_B[y]\|^2$ .
Residual characterization (p. 767): $x \in S \iff r(x) = 0$ .
(2.5) (p. 769): $\langle F(x), r(x)\rangle \ge \|r(x)\|^2$ for $x \in C$ .
Linesearch well-definedness (p. 769): for $x \in C$ with $r(x) \ne 0$ , some $k$ satisfies (2.1).
Lemma 2.2 (p. 768): $x^{i+1} = P_{C\cap H_i}[\bar x^i]$ with $\bar x^i = P_{H_i}[x^i]$ .
(2.6) (pp. 769–770): $\|x^{i+1}-x^*\|^2 \le \|x^i-x^*\|^2 - \|x^{i+1}-\bar x^i\|^2 - \big(\eta_i\sigma/\|F(z^i)\|\big)^2\|r(x^i)\|^4$ for every $x^* \in S$ .
(2.8) (p. 770): $\eta_i\|r(x^i)\| \to 0$ .

Significance

Theorem 2.1 gives global convergence of a projection method for variational inequalities with no Lipschitz constant, no monotonicity and no knowledge of the problem beyond continuity and (1.2), at a fixed cost of two projections per iteration. Condition (1.2) covers pseudomonotone maps, which arise as gradients of pseudoconvex functions and in equilibrium models where monotonicity fails. The separating-hyperplane-and-project template of the proof is reused throughout the later literature on projection, proximal and hybrid methods for monotone inclusions.

The result has been proved since 1999. To the best of available knowledge no machine-checked proof of it, or of any convergence theorem for a projection method for variational inequalities, exists in Lean or Mathlib. This mission produces the statement and the supporting layer: a Euclidean projection onto closed convex sets with its standard inequalities, variational inequality solution sets, the projected residual, and a formal model of an Armijo-type linesearch algorithm with termination.

Difficulty

The Fejér-type inequality (2.6) quickly gives bounded iterates and $\eta_i\|r(x^i)\| \to 0$ . The obvious next step, concluding $r(x^i) \to 0$ , fails: nothing prevents the stepsizes $\eta_i$ from tending to zero, and in that regime the product going to zero says nothing about the residual. This regime is where the minimality of $k_i$ and the continuity of $F$ enter, and it is the step a naive formalization (for instance one that drops minimality, or fixes the stepsize) cannot reach. A second subtlety is that (1.2) is needed at an accumulation point that is only known to lie in $S$ at the end of the argument, which is why the condition must hold for every $x^* \in S$ . Finally, subsequential convergence must be upgraded to convergence of the whole sequence to one solution; convergence of a subsequence, or of the distance to $S$ , is strictly weaker.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) (not Fin n → ℝ, whose norm is the sup norm). The accumulation-point step needs finite dimension; no Hilbert-space generalization is intended.
Projection encoding. projOnto K x is a nearest point of $K$ to $x$ when one exists, chosen by Classical.choose, and the junk value $x$ otherwise. On nonempty closed convex sets it is exactly $P_K[x]$ ; the paper only projects onto such sets ( $C$ , $H_i$ , $C \cap H_i$ ), so the junk value is never reached under the hypotheses.
Stopping-rule encoding. A run is a sequence x : ℕ → ℝⁿ with Armijo indices k : ℕ → ℕ (predicate IsAlg21Run). If $r(x^i) = 0$ the method has stopped and the run stalls, $x^{i+1} = x^i$ ; otherwise $k_i$ is the least index satisfying (2.1) and $x^{i+1} = P_{C \cap H_i}[x^i]$ . A stalled point is a solution, so finitely terminating runs are included in the goal.
Parameters $\gamma, \sigma$ are real with $0 < \gamma < 1$ , $0 < \sigma < 1$ , universally quantified; $n$ , $C$ , $F$ and $x^0 \in C$ are arbitrary.
(2.6) is stated for one generic step ( $x \in C$ , $r(x)\ne 0$ , $k$ satisfying (2.1)) rather than along a run; it is the same inequality with $x^i, k_i$ abstracted.
Trivializing formalizations are ruled out: condition (1.2) is quantified over every solution and every $x \in C$ (not replaced by monotonicity or an existential), $k_i$ is the least index satisfying (2.1), the update projects $x^i$ onto $C \cap H_i$ (not onto $C$ alone), the stopped case is pinned down by the stall encoding, and the conclusion is convergence of the whole sequence to one solution, not $r(x^i) \to 0$ or $\operatorname{dist}(x^i, S) \to 0$ .
Needed infrastructure: existence, uniqueness and variational characterization of the projection (Mathlib has exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero), firm nonexpansiveness, the explicit projection onto a halfspace, and a bounded-sequence subsequence argument in $\mathbb{R}^n$ . The projection lemmas are reusable for any projection-type method; contributions proving them as standalone lemmas are welcome.

Selected references

M. V. Solodov and B. F. Svaiter, A New Projection Method for Variational Inequality Problems, SIAM J. Control Optim. 37(3), 765–776, 1999. https://doi.org/10.1137/S0363012997317475
G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Matecon 12, 747–756, 1976.
A. N. Iusem and B. F. Svaiter, A variant of Korpelevich's method for variational inequalities with a new search strategy, Optimization 42, 309–321, 1997. https://doi.org/10.1080/02331939708844365
P. T. Harker and J.-S. Pang, Finite-dimensional variational inequality and nonlinear complementarity problems: a survey of theory, algorithms and applications, Math. Programming 48, 161–220, 1990. https://doi.org/10.1007/BF01582255
F. Facchinei and J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543

16 thms2 active usersReviewed

Completed

Linear algebra Numerical Analysis Operations Research·Captain: mikedeng1

Conjugate Gradient Methods with Inexact Searches: The Self-Scaled Direction Is a Multiple of Beale's Restart DirectionResearch Paper

Motivation

Conjugate gradient methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using only gradients and a handful of stored vectors. This makes them the standard choice when $n$ is too large for Newton or quasi-Newton methods, which store an $n\times n$ matrix. On a strictly convex quadratic with exact line searches the classical method of Hestenes and Stiefel terminates in at most $n$ steps. On general functions, and with the inexact line searches used in practice, its behaviour is much less clear.

D. F. Shanno's 1978 paper in Mathematics of Operations Research (doi:10.1287/moor.3.3.244) links conjugate gradient methods to quasi-Newton methods. It writes the search direction as $-\hat H g$ , where $\hat H$ is a positive definite approximation of the inverse Hessian that is never stored. The resulting "memoryless" BFGS directions give descent without exact line searches. The paper's new algorithm uses two BFGS updates: one from the last restart and one from the current step. Its first update is scaled by the Oren–Spedicato factor $\gamma_t$ . Shanno and Phua's CONMIN code implements the algorithm, and the memoryless BFGS direction is the one-pair case of the later limited-memory BFGS methods.

1952: Hestenes and Stiefel, linear conjugate gradients.
1964: Fletcher and Reeves, nonlinear conjugate gradients.
1969: Polak and Ribière, a second nonlinear variant.
1972: Beale, a restart procedure that keeps the computed direction $d_t$ .
1977: Powell's restart criterion (Powell 1977).
1978: Shanno's reformulation as memoryless and two-update quasi-Newton methods (this paper).

Setting

Vectors are columns in $\mathbb R^n$ . A prime denotes transpose: $u'v$ is the inner product and $uv'$ the outer product. An iterative method produces points $x_k$ , steps $p_k = x_{k+1}-x_k = \alpha_k d_k$ along search directions $d_k$ , gradients $g_k = \nabla f(x_k)$ , and gradient changes $y_k = g_{k+1}-g_k$ . A line search is exact when $p_k'g_{k+1} = 0$ .

The BFGS update of a matrix $H$ with the pair $(p,y)$ is

H^+ = H - \frac{p\,y'H + H y\,p'}{p'y} + \left(1+\frac{y'Hy}{p'y}\right)\frac{pp'}{p'y}.

A restart cycle begins at iteration $t$ . At a later iteration $k>t$ , Shanno's self-scaled restart matrix is

\hat H_k = \gamma_t\left(I - \frac{p_ty_t'+y_tp_t'}{p_t'y_t} + \frac{y_t'y_t}{p_t'y_t}\frac{p_tp_t'}{p_t'y_t}\right) + \frac{p_tp_t'}{p_t'y_t}, \qquad \gamma_t = \frac{p_t'y_t}{y_t'y_t}.

The matrix $\hat H_{k+1}$ is its BFGS update with $(p_k,y_k)$ , and the self-scaled two-update direction is $d_{k+1} = -\hat H_{k+1}g_{k+1}$ . The unscaled variant uses the BFGS update of $I$ in place of the first matrix.

Beale's direction is

d_{k+1} = -g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t.

The quadratic case has gradient $g(x) = Ax + c$ with $A$ symmetric positive definite.

Formalization targets

Goal: reduction of the self-scaled method to Beale's method

Let $A$ be symmetric positive definite, $g_i = Ax_i + c$ and $t<k$ . Assume that for $t\le i\le k$ we have $x_{i+1} = x_i + p_i$ , $p_i = \alpha_i d_i$ and $p_i'g_{i+1}=0$ , that $p_t'Ap_i = 0$ for $t<i\le k$ , and that $p_t, p_k \ne 0$ . Then

-\hat H_{k+1}g_{k+1} = \gamma_t\left(-g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t\right).

This is the paper's claim that "for $f(x)$ quadratic with exact searches each of the above methods reduces exactly to Beale's method defined by (28)", with the conclusion (44). The scale is exactly $\gamma_t$ .

Companion statements

The unscaled two-update direction equals Beale's direction exactly.
Both two-update directions are descent directions, $g_{k+1}'d_{k+1} < 0$ , whenever $p_t'y_t > 0$ and $p_k'y_k > 0$ . No exact search is needed.

Milestones on the path

(34): the expansion of $-\hat H_{k+1}g_{k+1}$ .
(40): its form under an exact search.
(41): gradients along a run on a quadratic.
$p_t'g_{k+1} = 0$ .
(38), corrected by a factor 2: the action of the self-scaled restart matrix.
(42): its form when $p_t'g_{k+1} = 0$ .
(43): the direction after substitution.

Significance

The result. The reduction says that the new algorithm reproduces Beale's restarted conjugate gradient directions on a quadratic with exact line searches. So it keeps the finite-termination and rate-of-convergence properties behind Beale's restart. Away from that setting it behaves as a quasi-Newton method, whose directions are descent directions under any line search with $p'y>0$ . The two regimes are what justify relaxing the line search, which the paper's computations exploit. The scale $\gamma_t$ changes only the length of the step, not its direction.

Formalizing it. The claim is proved in the paper by a short computation, and no machine-checked version is known. This mission produces:

a checked statement of the claim with every hypothesis explicit, including the conjugacy the proof takes as known;
a corrected version of display (38), which is misprinted;
reusable definitions of the additive BFGS update and of Beale's direction.

Difficulty

The obvious attempt is to expand both BFGS updates symbolically and compare with Beale's formula. This fails without two facts that are not algebraic identities. The first is that the restart step stays orthogonal to every later gradient, $p_t'g_{k+1}=0$ . It needs the affine gradient of a quadratic, the exact search at the restart step, and conjugacy of $p_t$ with all later steps. The second is $y_k'p_t = 0$ , which again comes from conjugacy. Beale's formula also has to be matched in its $d$ -form: the coefficient $\frac{y'g}{d'y}d$ equals $\frac{y'g}{p'y}p$ only when the step length is nonzero. The descent statements need a different argument: the BFGS update of a positive definite matrix with $p'y>0$ must be shown to remain positive definite, and this has to be done twice.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The inner product $u'v$ is u ⬝ᵥ v, the outer product $uv'$ is vecMulVec u v, and $Hv$ is H *ᵥ v. The quadratic enters only through its gradient A *ᵥ x + c with A.PosDef. The paper's (4) is the case $c = -A\hat x$ . Iterates, steps, directions and gradients are sequences indexed by ℕ. Division is Lean's total division. Every statement that divides therefore carries hypotheses making its denominators nonzero: $p_t \ne 0$ and $p_k\ne0$ in the quadratic statements, and $p_t'y_t\ne 0$ or $p'y>0$ in the generic ones.

The conjugacy $p_t'Ap_i=0$ for $t<i\le k$ is a hypothesis, exactly as the paper's proof uses it. It is not derived from a full run of Beale's algorithm. The range $k\le t+n-1$ of Beale's formula is not assumed.

Several formalizations would make the claim easier than the paper's, and none of them is used:

defining the direction by the expanded formula (34), or the restart matrix by (38);
adding orthogonality or conjugacy hypotheses beyond those listed;
concluding only that the two directions are parallel;
dropping the restart term of Beale's direction;
allowing a zero denominator.

The generic milestones — (34), (40), (38), (42), (43) and the descent statements — are statements about arbitrary vectors and matrices and are reusable for any BFGS-based method. Proofs of any milestone, and alternative derivations of the goal, are welcome.

Selected references

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
E. M. L. Beale, A derivation of conjugate gradients, in F. A. Lootsma (ed.), Numerical Methods for Nonlinear Optimization, Academic Press, 1972, 39–43.
M. J. D. Powell, Restart procedures for the conjugate gradient method, Mathematical Programming 12 (1977) 241–254. https://doi.org/10.1007/BF01593790
M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
S. S. Oren and E. Spedicato, Optimal conditioning of self-scaling variable metric algorithms, Mathematical Programming 10 (1976) 70–90. https://doi.org/10.1007/BF01580654

18 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Information Sharing in a Supply Chain with a Common Retailer 1: Under Production Diseconomy the Retailer Earns More from Sequential Information Contracting and the Manufacturers from ConcurrentResearch Paper

Motivation

Retailers hold point-of-sale data that their suppliers cannot observe, and large retailers sell access to it through data-sharing programs (Costco's CRX, Walmart's Retail Link and similar programs). When one retailer carries the substitutable products of two competing manufacturers, sharing its demand information is a strategic decision: a manufacturer who knows the demand signal sets his wholesale price in response to it, which changes the retailer's margin and the rival manufacturer's order uncertainty. Whether the retailer should sell the information, to how many manufacturers, and by which protocol, is the question of Shang, Ha and Tong (Management Science 62(1):245–263, 2016).

The paper belongs to the information-sharing literature of Li (2002), Li and Zhang (2008) and Ha, Tong and Zhang (2011), which studies competing supply chains or a single chain. The common-retailer structure differs: the retailer can price-discriminate between the manufacturers through the order in which she offers the information.

Setting

Two manufacturers $i \in \{1, 2\}$ sell substitutable products through one retailer. The demand for product $i$ is

q_i = a + \theta - (1+\phi)p_i + \phi p_j,

where $p_i$ is the retail price, $\phi > 0$ measures competition, and $\theta$ is a random shock with mean $0$ and variance $\sigma^2 > 0$ . The retailer observes a demand signal $Y$ that is unbiased, $E[Y \mid \theta] = \theta$ , and has linear expectation: $E[\theta \mid Y] = \beta Y$ for a weight $\beta$ (in the paper $\beta = t\sigma^2/(1+t\sigma^2)$ , with $t$ the signal accuracy). The retailing cost is zero, and manufacturer $i$ produces $q$ units at cost $bq + c_d q^2$ with $b, c_d > 0$ : a production diseconomy.

The game has four stages.

The retailer and the manufacturers contract on information sharing, which fixes each manufacturer's status $X_i \in \{I, U\}$ (informed or uninformed).
The retailer observes $Y$ and discloses it truthfully to the informed manufacturers.
The manufacturers set wholesale prices $w_i$ simultaneously, an informed one as a function of $Y$ . The retailer then sets retail prices.
Demand realizes and payoffs are received.

The pricing stage is a Bayesian game. Its equilibrium ex ante profits are $\pi_M(n)$ , $\pi_M^I(1)$ , $\pi_M^U(1)$ for the manufacturers and $\pi_R(n)$ for the retailer, where $n$ is the number of informed manufacturers. They define a payoff table for the contracting stage.

Two contracting protocols are compared.

Concurrent contracting: the retailer offers both manufacturers the same payment $T$ , and they accept or reject simultaneously; a Pareto-optimal pure equilibrium is the outcome, and the retailer chooses $T$ .
Sequential contracting: the retailer offers one manufacturer $T_f$ , he accepts or rejects, then the retailer offers the other $T_s$ , and he decides having observed the first decision. The retailer cannot commit to $T_s = T_f$ , and the solution is subgame perfect equilibrium.

Formalization targets

Goal: Proposition 4(d)

For every $\phi > 0$ , $c_d > 0$ and every signal model, the pricing stage has an equilibrium; for every pricing equilibrium, both contracting games have equilibria; and for every concurrent outcome and every sequential subgame-perfect equilibrium (either first mover),

\Pi_R^{C} \le \Pi_R^{S}, \qquad \Pi_M^{S} \le \Pi_M^{C},

with both inequalities strict when $c_d > (\sqrt2 - 1)/(1+\phi)$ . Here $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The paper's word "higher" is read as $\ge$ because for small $c_d$ neither protocol sells information and all profits coincide.

Milestones

§4.1, Eq. (1): the retailer's best response $\hat p_i = \frac12(a + \beta Y + w_i)$ and the resulting demand.
Lemma 1: the pricing equilibrium exists, is unique, and is linear in $Y$ .
§4.2: the closed forms of the seven ex ante profits.
Lemma 3: $\pi_M(2) > \pi_M^I(1) > \pi_M(0) > \pi_M^U(1)$ , $\pi_R(0) > \pi_R(1) > \pi_R(2)$ , $\pi_R(1) - \pi_R(2) > \pi_R(0) - \pi_R(1)$ .
Proposition 1(b): without contracting, no information is shared.
Propositions 2 and 3: thresholds $c_d^C$ and $c_d^{S1}, c_d^{S2}$ , depending only on $\phi$ , at which the number of informed manufacturers changes under each protocol.
Proposition 4(a): $c_d^{S1} < c_d^C < c_d^{S2}$ .

Significance

The result. Proposition 4(d) says that the order of the offers transfers surplus: selling information one manufacturer at a time lets the retailer exploit the manufacturers' fear of being the only uninformed firm, which raises her profit and lowers theirs. Propositions 2 and 3 show that concurrent contracting shares with both manufacturers or with neither, while sequential contracting can end with only one informed manufacturer. Together they give a complete map of the equilibrium sharing decisions in $(c_d, \phi)$ (Figure 1 of the paper).

Formalizing it. The results are proved in the paper, partly by "it can be shown" and "straightforward" steps: Lemma 3's proof is omitted, and so is the convexity of the function whose root is $c_d^{S2}$ . No part of the paper has a machine-checked proof. A complete formalization would check every such step and make the equilibrium notions precise, in particular the Pareto selection and the tie-breaking at the thresholds, where the retailer is exactly indifferent.

Difficulty

Most of the work is in the contracting stage, not the algebra. The pricing stage must be solved over all square-integrable strategies measurable in the signal. Uniqueness is then almost sure and rests on the linear-expectation identities $E[\theta Y] = \sigma^2$ and $E[Y^2] = \sigma^2/\beta$ . The concurrent game has multiple equilibria for intermediate payments, and the retailer's optimum lies at a payment where two equilibria coexist. The sequential game is a three-stage game with a continuum of offers: at each threshold the retailer is indifferent, and an SPE exists only if acceptance at indifference is chosen correctly. The threshold $c_d^{S2}$ has no closed form; it is the root of a convex rational function of $c_d$ .

Formalization scope

The Lean development lives in the namespace InfoSharing.Diseconomy. Conventions:

The probability space carries $\theta$ and $Y$ in $L^2$ , with the two conditional-expectation identities holding almost everywhere. $\beta$ is a parameter fixed by $E[\theta \mid Y] = \beta Y$ ; Ericson's formula for $\beta$ is not formalized.
Wholesale strategies are measurable, square-integrable functions of the signal value, and constants for an uninformed manufacturer. A pricing equilibrium is ex ante optimality over such strategies, which is equivalent to the paper's conditional optimization. The retailer's rule must be a best response at every wholesale-price pair.
The payoff table is produced by an arbitrary pricing-equilibrium family, not by the §4.2 closed forms. A formalization that takes the closed forms as the definition of the profits would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out.
Payments are nonnegative, only pure strategies are used in the contracting games, and the concurrent outcome selects, among Pareto-optimal equilibria, the one best for the retailer.
Threshold statements use two clauses: the printed value is attained on the closed region, and it is the only value on the region's interior. The thresholds depend only on $\phi$ .
Demands may be negative (θ is unbounded), as in the paper's formulas.

A complete development needs:

the conditional-expectation algebra behind Lemma 1 and §4.2;
rational-function inequalities for Lemma 3;
a case analysis of the two contracting games.

The model layer is shared with the companion mission on production economy.

Selected references

G. Shang, A. Y. Ha, S. Tong, Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
W. A. Ericson, A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969.
L. Li, Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
L. Li, H. Zhang, Confidentiality and information sharing in supply chain coordination, Management Science 54(8):1467–1481, 2008. https://doi.org/10.1287/mnsc.1070.0851
A. Y. Ha, S. Tong, H. Zhang, Sharing imperfect demand information in competing supply chains with production diseconomies, Management Science 57(3):566–581, 2011. https://doi.org/10.1287/mnsc.1100.1295
X. Vives, Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999.

17 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Algorithmic Mechanism Design VIII: A Truthful Approximation Scheme for Bounded Scheduling with VerificationResearch Paper

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested agents: the designer can pay the agents, and must choose payments so that each agent's own interest leads it to reveal what the algorithm needs. Nisan and Ronen introduced the framework with task scheduling on unrelated machines as the running example (Nisan–Ronen 2001). In the basic model, where payments depend only on what the agents declare, they showed that no truthful mechanism approximates the optimal make-span within a factor below 2, and that the natural mechanism only reaches a factor $n$ .

Their Section 5 changes the information available: in a mechanism with verification the payments may also depend on the times in which the tasks were actually performed. With this extra information, an exact optimizer becomes a strongly truthful mechanism (Theorem 5.1, the Compensation-and-Bonus mechanism). Exact scheduling on unrelated machines is NP-hard, so the question is whether an approximation algorithm can take the optimizer's place. Theorem 5.6 of the paper shows that plugging a non-optimal algorithm into Compensation-and-Bonus destroys truthfulness in general. Theorem 5.9, the subject of this mission, shows that for the bounded problem a specific approximation scheme, the rounding algorithm of Horowitz and Sahni (1976), can be combined with a modified payment rule to give a truthful mechanism whose outcome is within a factor $1+\varepsilon$ of optimal.

Setting

There are $n$ agents and $k$ tasks. Agent $i$ needs time $t^i_j$ for task $j$ ; the vector $t = (t^i_j)$ is the type vector, and agent $i$ alone knows its row $t^i$ . In the bounded scheduling problem (Definition 33) there are fixed numbers $0 < a < b$ with $a \le t^i_j \le b$ for all $i, j$ , and every declaration lies in the same range. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$ .

A strategy of agent $i$ has two parts: a declaration $d^i \in [a,b]^k$ , and an execution, which for each decision $x$ of the mechanism specifies the actual time $\tilde t_j \ge t^i_j$ in which agent $i$ performs each task $j \in x^i$ . The mechanism chooses $x = x(d)$ from the declarations alone and afterwards observes the actual times $\tilde t$ . The objective is the make-span with actual times,

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

Agent $i$ receives a payment $p^i$ and has utility $p^i - \sum_{j \in x^i} \tilde t_j$ .

The corrected time vector of agent $i$ keeps agent $i$ 's actual times on its own tasks and the other agents' declarations elsewhere: $\mathrm{corr}^i(x,d,\tilde t)_j = \tilde t_j$ for $j \in x^i$ and $d^l_j$ for $j \in x^l$ , $l \ne i$ . For a step $\delta > 0$ , $\hat r = \delta\lceil r/\delta\rceil$ rounds $r$ up to a multiple of $\delta$ , and $\hat g(x,\tau) = g(x,\hat\tau)$ .

The rounding mechanism (Definition 34) allocates with an algorithm that exactly solves the problem with rounded declarations $\hat d$ , and pays

p^i = \sum_{j\in x^i}\tilde t_j \;-\; \hat g\big(x, \mathrm{corr}^i(x, d, \tilde t)\big).

The first term, the compensation, uses exact actual times; the second, the bonus, uses rounded quantities.

A strategy is dominant if it is a best response to every declarations and executions of the others. The mechanism is truthful if every agent has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.9 without running time

For every $\varepsilon > 0$ , every $0 < \delta \le \varepsilon a$ and every allocation algorithm solving the rounded problem exactly, the rounding mechanism is truthful, and at every profile of dominant strategies from the class named in the proof (declarations with the true rounded values, executions whose rounded times equal the rounded true times),

g\big(x(d),\tilde t\big) \le (1+\varepsilon)\, g(y,t) \quad \text{for every allocation } y .

Milestones

The solution of the rounded problem is a $(1+\varepsilon)$ -approximation: $g(x,\hat t) \le g(y,\hat t)\ \forall y$ implies $g(x,t) \le (1+\varepsilon) g(y,t)\ \forall y$ .
After rounding, $\hat g$ is the make-span, $\hat g(x,\mathrm{corr}^*(x,d)) = g(x,\hat d)$ , and each agent's utility equals its rounded bonus.
Every strategy with the true rounded values is dominant.
When all agents follow such strategies, the outcome is a $(1+\varepsilon)$ -approximation.
Truth-telling with minimal execution is dominant; hence the mechanism is truthful.

Significance

The result shows that verification does more than make exact optimization truthful: it lets a polynomial-time approximation scheme be implemented in dominant strategies, provided the bonus is computed on the same rounded instance the algorithm optimizes. This contrasts with Theorem 5.6, where an arbitrary approximation algorithm inside Compensation-and-Bonus is not truthful, and with the factor-2 lower bound of the basic model. The principle it illustrates is that the payments must reward exactly the objective the algorithm optimizes.

The paper gives only a proof sketch. Formalizing it makes the argument's hypotheses explicit: which rounding step suffices, what the allocation algorithm must satisfy, and over which strategy profiles the approximation guarantee holds. No machine-checked version of this theorem or of the Compensation-and-Bonus argument is known to exist.

Difficulty

The sketch reduces the theorem to "arguments similar to those in 5.1", but the rounded setting departs from Theorem 5.1 in two ways. Rounding is many-to-one, so an agent's declaration and execution are pinned down only up to their rounded values, and the algorithm's optimality holds only for the rounded instance. Consequently the claim that the strategies with the true rounded values are the only dominant ones does not survive arbitrary tie-breaking: an agent that is always favoured on ties can overstate its rounded time by one step without ever losing, and two such lies at one profile can push the make-span above the $(1+\varepsilon)$ bound. The approximation guarantee therefore has to be stated for the strategy class the proof identifies, not derived from dominance alone. The remaining steps require exact bookkeeping of rounding across sums and of the corrected time vectors, which a proof sketch leaves implicit.

Formalization scope

Agents are Fin n with [NeZero n], tasks Fin k; allocations are functions Fin k → Fin n; the make-span is a Finset.sup' over agents. Types and declarations satisfy a ≤ t i j ≤ b with 0 < a < b; actual times are only bounded below by the true times.
roundUp δ r = δ * ⌈r / δ⌉. The statement holds for every $\delta \in (0,\varepsilon a]$ , which covers the intended choice $\delta = \varepsilon a$ ; the paper leaves $\delta$ as "a function of $a$ and $\varepsilon$ ".
The Horowitz–Sahni dynamic program is not formalized. The allocation algorithm is a parameter with the hypothesis that it solves the rounded problem exactly; ties are arbitrary, and the goal holds for every such algorithm. Running time ("polynomial time") is out of scope, and with it the role of the upper bound $b$ , which is kept as part of the problem.
An execution is a function of the decision (Definition 18). Dominance quantifies over all declarations in $[a,b]$ and all executions of the others.
The payment uses the allocation $x(d)$ in the bonus. Definition 34 prints $x(\hat t)$ ; since the rounding algorithm rounds the declarations itself, $x(d)$ is the allocation actually computed. The hat on $\mathrm{corr}$ is absorbed by $\hat g$ .
The goal's approximation part is restricted to dominant profiles of the class named in the proof, because the unrestricted form (Definition 3, every dominant profile) is false for some tie-breaking rules; an explicit two-agent, one-task instance is recorded in the goal's Formalization Note.
A formalization that measures the approximation with declared rather than actual times, lets the allocation read the true types, or states the approximation only at the truthful profile while claiming the general form, does not formalize this theorem.

Useful infrastructure: lemmas on Int.ceil rounding of finite sums and on Finset.sup' monotonicity, and a reusable model of mechanisms with verification. Proofs of the milestones in any order are welcome.

Selected references

N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
E. Horowitz, S. Sahni, Exact and Approximate Algorithms for Scheduling Nonidentical Processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Algorithmic Mechanism Design VII: Compensation-and-Bonus Based on a Non-Optimal Approximation Algorithm Is Not TruthfulResearch Paper

Motivation

Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: the algorithm must compute a good solution and, through payments, make it in each agent's interest to report its input honestly. Nisan and Ronen introduced the field with the problem of scheduling tasks on unrelated machines, where each machine is an agent that privately knows how long it needs for every task (Nisan–Ronen 2001).

The classical tool for truthfulness, the Vickrey–Groves–Clarke (VGC) family of mechanisms, requires the allocation to be exactly optimal. Exact optimization is often computationally out of reach: minimizing the make-span on unrelated machines is NP-hard, and even approximating it within a factor below 3/2 is NP-hard (Lenstra–Shmoys–Tardos 1990). A mechanism designer would therefore like to plug an approximation algorithm into a truthful mechanism and keep truthfulness. This mission formalizes a result showing that the simplest way of doing so fails in the model with verification, where the mechanism may pay after the tasks are performed and observes the actual execution times.

Timeline.

1999/2001: Nisan and Ronen define mechanisms with verification and the Compensation-and-Bonus mechanism, prove it strongly truthful when its allocation algorithm is optimal (their Theorem 5.1), and prove that replacing the optimal algorithm by a non-optimal approximation algorithm destroys truthfulness (Theorem 5.6, the goal here). They remark that a similar argument applies to VGC mechanisms.
2002: Lehmann, O'Callaghan and Shoham show the analogous failure for VGC payments with approximate allocation in combinatorial auctions (JACM 2002).
2007: Nisan and Ronen study which approximation algorithms can be made truthful within the VGC framework (JAIR 2007).

Setting

There are $n \ge 1$ agents and $k$ tasks. The type of agent $i$ is a vector $t^i = (t^i_1,\dots,t^i_k)$ of positive reals, $t^i_j$ being the minimum time agent $i$ needs for task $j$ ; a type vector is $t = (t^1,\dots,t^n)$ . An allocation $x = (x^1,\dots,x^n)$ gives each task to one agent. The make-span is

g(x,t) = \max_i \sum_{j\in x^i} t^i_j,

and $x$ is optimal for $t$ if $g(x,t)\le g(y,t)$ for every allocation $y$ .

In the model with verification, an agent's strategy has two parts: a declaration $d^i$ (any positive vector) and an execution plan that, for every allocation the mechanism may choose, fixes the actual time $\tilde t_j \ge t^i_j$ in which the agent performs each task $j$ it receives. An allocation algorithm $x(\cdot)$ maps the declarations to an allocation $x(d)$ ; the tasks are then executed, producing actual times $\tilde t$ .

The Compensation-and-Bonus mechanism based on $x(\cdot)$ pays agent $i$

p^i(d,\tilde t) = \sum_{j\in x^i(d)} \tilde t_j \;-\; g\bigl(x(d), \operatorname{corr}^i(x(d),d,\tilde t)\bigr),

a compensation for the time actually spent plus a bonus equal to minus the make-span computed from agent $i$ 's actual times on its own tasks and the other agents' declared times on theirs (the corrected time vector $\operatorname{corr}^i$ ). The agent's utility is its payment minus the time it spends. A strategy is dominant if it is at least as good as every alternative whatever the other agents declare and execute; the mechanism is truthful if every agent of every type has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.6

Let $x(\cdot)$ be an allocation algorithm such that, for some real $c$ ,

g\bigl(x(t),t\bigr) \le c\, g(y,t)\quad\text{for every positive } t \text{ and every allocation } y,

and such that $g(y,t) < g(x(t),t)$ for some positive $t$ and some allocation $y$ . Then the Compensation-and-Bonus mechanism based on $x(\cdot)$ is not truthful.

The ratio $c$ is arbitrary and existentially quantified: the theorem holds for every finite approximation ratio, so it is stated without a constant.

Milestones

Claim 5.7. If the mechanism based on $x(\cdot)$ is truthful, $o$ is optimal for $t$ and $M$ is at least every entry of $t$ , then replacing one agent's type by $t^i_j$ on $o^i$ and $M$ elsewhere gives a type vector $t'$ with $g(x(t'),t') \ge g(x(t),t)$ .
Corollary 5.8. Under the same assumptions, the type vector $s$ that makes this replacement for every agent satisfies $g(x(s),s) \ge g(x(t),t)$ .
Final step. $g(o,s) = g(o,t)$ , $o$ is optimal for $s$ , and every allocation $y\ne o$ has $g(y,s)\ge M$ .

Significance

The result. Theorem 5.1 of the same paper shows that with an optimal algorithm the Compensation-and-Bonus mechanism is a strongly truthful implementation of make-span minimization. Theorem 5.6 shows that this guarantee is tied to exact optimization: it does not survive replacing the optimizer by any non-optimal approximation algorithm, whatever its ratio. It explains why the paper then turns to a restricted problem (bounded scheduling) and a mechanism designed around a specific rounding algorithm, and it is an early instance of the general tension between approximation and incentive compatibility.

Formalizing it. The result is proved in the paper; to the best of the platform's catalog it has not been formalized. The mission produces a machine-checked model of mechanisms with verification (declarations together with execution plans that may depend on the decision), the Compensation-and-Bonus payment rule for an arbitrary allocation algorithm, and Definition 19 truthfulness, together with a checked proof of the impossibility.

Difficulty

The argument is short on paper; the difficulty lies in the model. The paper's " $\infty$ " is not a number, and a faithful statement must replace it by a finite value that is large enough to conflict with the approximation ratio yet keeps every type positive and entrywise above the true types; both requirements refer to data fixed earlier in the argument. The incentive step compares utilities in a mechanism where an agent's strategy is a declaration and an execution plan that may depend on the decision, and where the bonus mixes the agent's actual times with the other agents' declarations, so a naive reading in which only declarations matter (the direct-revelation model of §2) does not capture the claim. Finally, Corollary 5.8 concerns a type vector modified at every agent, while Claim 5.7 modifies one agent at a time, so the claim must be applicable at type vectors that are no longer the original one.

Formalization scope

Agents are Fin n with [NeZero n], tasks Fin k, allocations are functions Fin k → Fin n, types and declarations are positive real vectors. Make-spans are Finset.sup' over the nonempty set of agents. With no agents no allocation algorithm meets the hypotheses, so requiring $n\ge 1$ loses nothing.
An execution plan is a function of the allocation; feasibility is $\tilde t_j \ge t^i_j$ on the agent's own tasks. In the dominance quantifier the other agents' declarations are positive and their execution plans arbitrary; the agent's alternative declarations are positive and its alternative plans feasible for its true type.
The allocation algorithm is an arbitrary function of the declarations; "approximation algorithm" is the hypothesis $\exists c$ above, "non-optimal" the hypothesis of one positive witness. The optimal allocation $\mathrm{opt}(t)$ in the milestones is any optimal allocation $o$ , supplied as a parameter.
The paper's $\infty$ is a real parameter $M$ with $M \ge t^l_j$ for all $l,j$ ; extended reals are not used.
Claim 5.7 is stated for an arbitrary agent $i$ , not only for agent 1, so that Corollary 5.8 can iterate it.
Running time is not modelled; "algorithm" means function.
Dropping the approximation hypothesis makes the statement false: an allocation rule that ignores the declarations is non-optimal, yet its Compensation-and-Bonus mechanism is truthful. Stating only "not strongly truthful", or proving the theorem for a fixed instance, would be a weaker claim.

Welcome contributions: proofs of the milestones and the goal, and reusable lemmas about the corrected time vector and the monotonicity of the make-span in the time vector.

Selected references

N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
D. Lehmann, L. I. O'Callaghan, Y. Shoham, Truth revelation in approximately efficient combinatorial auctions, Journal of the ACM 49 (2002) 577–602. https://doi.org/10.1145/585265.585266
N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29 (2007) 19–47. https://doi.org/10.1613/jair.2046
E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Algorithmic Mechanism Design III: No Additive Truthful Mechanism Achieves a c-Approximation for Task Scheduling for Any c < nResearch Paper

Motivation

Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: an algorithm must not only compute a good solution but also pay the agents so that reporting their data truthfully is in their own interest. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001) with task scheduling on unrelated machines as the model problem. Each machine is owned by an agent who alone knows how long it takes for each task; the designer wants a schedule of small make-span.

The paper gives a truthful mechanism, MinWork, whose make-span is within a factor $n$ of optimal, and a lower bound of $2$ for every truthful mechanism. It conjectures that no truthful mechanism beats $n$ (Conjecture 4.9) and proves the conjecture for two natural classes. This mission is about one of them, additive mechanisms (Theorem 4.10, p. 180).

Timeline of the gap between $2$ and $n$ :

1999/2001: Nisan and Ronen prove the lower bound $2$ for all truthful mechanisms and $n$ for additive and for local mechanisms.
2007: Christodoulou, Koutsoupias and Vidali raise the general lower bound to $1+\sqrt 2$ for $n\ge 3$ (SODA 2007; Algorithmica 2009).
2008: Christodoulou, Koutsoupias and Vidali characterize the truthful mechanisms for two machines (ESA 2008; arXiv 0807.3427); in parallel, Dobzinski and Sundararajan (EC 2008) characterize them and show that for two machines no truthful mechanism beats $2$ .
2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no truthful mechanism beats $n$ (STOC 2023; arXiv 2301.11905).

Setting

There are $n$ agents $i=1,\dots,n$ and $k$ tasks $j=1,\dots,k$ . The type of agent $i$ is a vector $t^i=(t^i_1,\dots,t^i_k)$ of positive reals, $t^i_j$ being the time agent $i$ needs for task $j$ ; a type vector $t=(t^1,\dots,t^n)$ collects all types, and $t^{-i}$ denotes the types of the agents other than $i$ . An allocation $x=(x^1,\dots,x^n)$ is a partition of the tasks, $x^i$ being the set given to agent $i$ . For a set $X$ of tasks write $t^i(X)=\sum_{j\in X}t^i_j$ . The make-span is

g(x,t)=\max_i t^i(x^i).

A direct mechanism $m=(x,p)$ maps every declared type vector $t$ to an allocation $x(t)$ and to payments $p^i(t)$ handed to the agents. An agent with true type $t^i$ gets utility $p^i(t)-t^i(x^i(t))$ . The mechanism is truthful if, whatever the others declare, no agent gains by declaring a type other than its true one. It is a $c$ -approximation if $g(x(t),t)\le c\,g(y,t)$ for every positive type vector $t$ and every allocation $y$ .

The price offered for a set $X$ to agent $i$ (Definition 12) is the payment $p^i(t'^i,t^{-i})$ at any declaration $t'^i$ for which the mechanism gives agent $i$ exactly $X$ , and $0$ if there is no such declaration. For truthful mechanisms this is well defined (Proposition 4.4, Independence). The mechanism is additive (Definition 13) if

p^i(X,t^{-i})=\sum_{j\in X}p^i(\{j\},t^{-i})

for every agent $i$ , type vector $t$ and set $X$ of tasks. MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is additive.

Formalization targets

Goal: Theorem 4.10

For $n\ge 1$ agents and $k\ge n^2$ tasks, for every truthful additive mechanism $(x,p)$ and every real $c<n$ ,

\exists\,t,\ \exists\,y:\qquad g\bigl(x(t),t\bigr)>c\cdot g(y,t).

The goal leaves the mechanism, its tie-breaking and $c$ completely general. It says that the ratio $n$ of MinWork is optimal among additive mechanisms.

Milestones

Proposition 4.4 (Independence): the payment depends on agent $i$ 's declaration only through its allocation.
Proposition 4.5 (Maximization): $x^i(t)$ maximizes $p^i(X,t^{-i})-t^i(X)$ over the sets $X$ agent $i$ can obtain against $t^{-i}$ .
Pigeonhole: with $k\ge n^2$ tasks some agent receives at least $n$ tasks.
Claim 4.11: at the all-ones type vector $t$ , lowering agent $i$ 's times to $1-\epsilon$ on $x^i(t)$ and $\epsilon$ elsewhere keeps all of $x^i(t)$ with agent $i$ , provided the empty set is attainable for agent $i$ .
The ratio step: at that perturbed type vector, an allocation giving agent $i$ a fixed set of $n$ tasks has make-span at least $(1-\epsilon)n$ , while some allocation has make-span at most $1+k\epsilon$ .

Significance

Theorem 4.10 shows that the gap between MinWork's ratio $n$ and the general lower bound $2$ cannot be closed by any mechanism that prices tasks separately, and so any better mechanism would have to couple the prices of different tasks. It was the first class-restricted confirmation of Conjecture 4.9, which was eventually proved for all truthful mechanisms (Christodoulou–Koutsoupias–Kovács 2023). The additive case is the cleanest entry point: its proof needs only the two basic properties of truthful mechanisms, Independence and Maximization, which every later lower bound also uses.

All results here are proved on paper, and none has a machine-checked proof on Prove2Me as of this mission's drafting. The mission produces a formal model of scheduling mechanisms and prices that other lower bounds can reuse, formal statements of Independence and Maximization, and a formal proof of Theorem 4.10. Along the way the formalization corrects two points of the printed argument (see Formalization scope).

Difficulty

The work is to extract prices from an arbitrary truthful mechanism. Prices are defined through the attainable sets of Definition 12. A natural first idea replaces the mechanism by per-task prices $q^i_j(t^{-i})$ that the agent maximizes against. That gives a different class, because Definition 13 constrains the price of every set of tasks, including sets the mechanism never allocates, whose price is $0$ .

Claim 4.11 is the critical step, and its printed argument does not go through for an arbitrary truthful additive mechanism. It needs the empty set to be attainable with price $0$ . For a mechanism with a bounded ratio this holds, because a very slow agent must receive nothing, but this has to be derived from the approximation hypothesis. From that, one has to show that every task of $x^i(t)$ carries a single-task price of at least $1$ . The final step also needs care. The paper's "w.l.o.g. $|x^1|=n$ " is a further reduction, and the paper's bound $g\ge|x^1|$ has to be replaced by $(1-\epsilon)|x^1|$ .

Formalization scope

Representation. Agents are Fin n, tasks Fin k, type vectors Fin n → Fin k → ℝ, and an allocation is a map Fin k → Fin n sending each task to its agent. taskSet x i is $x^i$ , and the make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]). A mechanism is a pair alloc, pay of arbitrary functions; nothing about its tie-breaking is fixed.
Standing assumptions. Types are positive. Truthfulness, additivity and approximation quantify over positive type vectors only. Utility is quasi-linear, with payments handed to the agent.
Prices. price follows Definition 12 literally: the payment at a Classical.choose witness declaration when the set is attainable, and $0$ otherwise. Additivity (IsAdditive) is required for every set of tasks, attainable or not, as Definition 13 states. It is a condition on prices, not on the payment function.
Explicit threshold. The goal assumes $k\ge n^2$ , the value the paper's proof starts from; the printed theorem does not mention $k$ . It is stated for every $n\ge1$ ; at $n=1$ it holds because all allocations coincide.
Printed slips, corrected. (1) Proposition 4.5 is stated over attainable sets: over all sets, with the price $0$ of unattainable sets, it fails for truthful mechanisms that never give the agent nothing and charge it. (2) Claim 4.11 carries the added hypothesis that $\emptyset$ is attainable for agent $i$ . Without it the claim is false: a mechanism that always gives agent $i$ its $|x|$ cheapest tasks and pays nothing is truthful and additive. The claim is stated for an arbitrary agent $i$ instead of "agent 1 after relabelling". (3) The ratio step states $g\ge(1-\epsilon)n$ where the paper prints $g\ge|x^1|\ge n$ , and states the paper's w.l.o.g. $|x^1|=n$ as a hypothesis of the step, not of the goal.
Out of scope. Running time and the revelation principle are not modelled; the goal is stated for truthful direct mechanisms, as §4.3 fixes.
Ruled out. A trivializing encoding would define additivity through the payment function instead of the prices of Definition 12, fix $n$ , prove the ratio for one $c<n$ only, or drop truthfulness. The last makes the claim false: an optimal allocation rule with zero payments is additive and a $1$ -approximation. The goal here quantifies over every $n$ , every $c<n$ and every truthful additive mechanism.
Non-vacuity. Every hypothesis of the goal except the ratio is satisfiable (a constant allocation with zero payments is truthful and additive), and the bound is tight by MinWork.
Contributions welcome. Proofs of the milestones, a proof that a bounded-ratio mechanism makes $\emptyset$ attainable for every agent, and reuse of the model for the local-mechanism bound (Theorem 4.12).

Selected references

N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, SODA 2007; Algorithmica 55, 2009. https://doi.org/10.1007/s00453-008-9165-3
G. Christodoulou, E. Koutsoupias, A. Vidali, A characterization of 2-player mechanisms for scheduling, ESA 2008. https://arxiv.org/abs/0807.3427
S. Dobzinski, M. Sundararajan, On characterizations of truthful mechanisms for combinatorial auctions and scheduling, EC 2008, pp. 38–47.
G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023. https://doi.org/10.1145/3564246.3585176 (arXiv:2301.11905)

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

A New Branch-and-Cut Algorithm for the Capacitated Vehicle Routing Problem: Safe Shrinking of Customer SetsResearch Paper

Motivation

The capacitated vehicle routing problem (CVRP) asks for minimum-cost routes, starting and ending at a depot, that serve every customer exactly once without any vehicle carrying more than its capacity. It is one of the central problems of operations research and logistics, and exact algorithms for it have been built on branch-and-cut for three decades: a linear programming relaxation is strengthened at every node of a search tree by adding valid inequalities that the current LP solution violates.

The most important of these inequalities are the capacity inequalities. Deciding whether an LP solution violates one of them is strongly NP-hard, so practical codes rely on heuristics, and most heuristics first shrink the support graph: groups of customers are contracted into single supervertices so that the search runs on a smaller graph. Shrinking is only useful if it is safe, meaning it cannot hide a violated inequality. Before the work of Lysgaard, Letchford and Eglese, the standard safe rule allowed shrinking a single edge whose LP value is at least one (Augerat et al. 1998; Ralphs et al. 2003). Lysgaard, Letchford & Eglese (2004), whose separation routines were released as the widely used CVRPSEP package, generalized the rule to customer sets of any size in their Proposition 1, the only numbered result of the paper.

Setting

Let $G = (V, E)$ be the complete undirected graph on $V = \{0, 1, \dots, n\}$ . Vertex $0$ is the depot and $V_c = \{1, \dots, n\}$ are the customers. Vehicles have capacity $Q > 0$ and each customer $i$ has an integer demand $q_i$ with $0 < q_i \le Q$ . An LP point is a vector $x = (x_e)_{e \in E}$ ; $x_{ij}$ and $x_{ji}$ are the same variable, and LP solutions satisfy $x \ge 0$ .

For a vertex set $S$ , $\delta(S)$ is the set of edges with exactly one end-vertex in $S$ (edges to the depot included), and $x(\delta(S)) = \sum_{e \in \delta(S)} x_e$ is its cut value. For a customer set $S \subseteq V_c$ :

$q(S) = \sum_{i \in S} q_i$ is its total demand;
$r(S)$ , the bin-packing number, is the minimum number of bins of capacity $Q$ into which the items of sizes $q_i$ , $i \in S$ , can be packed;
$k(S) = \lceil q(S)/Q \rceil \le r(S)$ is the rounded capacity bound.

The capacity inequalities and the rounded capacity inequalities (RCIs) are

x(\delta(S)) \ge 2r(S) \quad\text{and}\quad x(\delta(S)) \ge 2k(S), \qquad S \subseteq V_c,\ |S| \ge 2 .

The violation of such an inequality at $x$ is $2r(S) - x(\delta(S))$ (resp. $2k(S) - x(\delta(S))$ ); it is violated when this is positive.

Shrinking a customer set $S$ contracts it to one supervertex. The supervertices of the shrunk graph are then $S$ and the single customers outside $S$ , so a union of supervertices is a customer set $T'$ with $S \subseteq T'$ or $S \cap T' = \emptyset$ . Shrinking $S$ is safe if for every customer set $T$ with $|T| \ge 2$ whose inequality is violated, there is such a union $T'$ with $|T'| \ge 2$ and at least the same violation.

Formalization targets

Goal: Proposition 1

For every $x \ge 0$ and every customer set $S$ with

x(\delta(S)) \le 2 \qquad\text{and}\qquad x(\delta(R)) \ge 2 \ \text{ for every nonempty proper subset } R \subsetneq S,

shrinking $S$ is safe for the capacity inequalities $x(\delta(T)) \ge 2r(T)$ .

Milestones (proof of Proposition 1, p. 426)

Monotonicity of the bin-packing number: $2r(S \cup T) - 2r(T) \ge 0$ .
Submodularity of the cut function, in the paper's arrangement: $x(\delta(T)) - x(\delta(S \cup T)) \ge x(\delta(S \cap T)) - x(\delta(S))$ for $x \ge 0$ .
The crossing-set inequality: if $T$ crosses $S$ ( $T \cap S$ , $T \setminus S$ , $S \setminus T$ all nonempty), then $2r(T) - x(\delta(T)) \le 2r(S \cup T) - x(\delta(S \cup T))$ .

Further statements on the same page

The same shrinking condition is safe for the rounded capacity inequalities $x(\delta(T)) \ge 2k(T)$ , which are the inequalities the algorithm separates.
The paper's first separation heuristic checks the RCI for each connected component $S_i$ of the support graph on the customers, for each complement $V_c \setminus S_i$ , and for the union of the components with no support edge to the depot. At an integer point satisfying the degree equations $x(\delta(\{i\})) = 2$ and the bounds $x_{ij} \in \{0,1\}$ , $x_{0j} \in \{0,1,2\}$ , this heuristic finds a violated RCI whenever one exists. This claim is stated in the paper without proof and is not needed for the goal.

Significance

Proposition 1 justifies contracting whole groups of customers before running separation heuristics, which shrinks the graph those heuristics work on while preserving every violated capacity inequality up to its violation. The rule is part of the separation routines of CVRPSEP and of later branch-and-cut and branch-cut-and-price codes for vehicle routing that reuse them.

The result is proved in the paper; to the best of the platform's records, none of it is formalized. The mission produces a reusable formal layer for the two-index CVRP formulation: cut values on the complete graph with a depot, the bin-packing number, the rounded capacity bound, and the notion of safe shrinking. Submodularity of the cut function (target 2) is a classical fact that the paper cites rather than proves; the platform already has a related statement for symmetric weight matrices on Boolean regions (EmergentGeometry.cutWeight_submodular), in a different representation. Target 5 records a claim of the paper that it asserts without proof.

Difficulty

When the violated set $T$ contains $S$ or misses it, $T$ itself is a union of supervertices and there is nothing to show. The difficulty is a set $T$ that crosses $S$ : no union of supervertices is obviously as violated as $T$ , because enlarging $T$ can raise its cut value — $x(\delta(S \cup T))$ can be smaller or larger than $x(\delta(T))$ depending on the edges leaving $S \setminus T$ — and the hypotheses on $S$ say nothing about $T$ directly. Both hypotheses on $S$ and the sign condition $x \ge 0$ matter here; for signed $x$ the statement fails. A violated $T$ strictly inside $S$ is not a crossing set in the paper's sense and has to be handled as well.

On the formal side, the bin-packing number is an optimum of a combinatorial problem; its properties must be derived from a definition by assignments to bins, and it is well defined only because every demand fits in one vehicle. Target 5 needs a structural understanding of integer points satisfying the degree equations, which the paper does not supply.

Formalization scope

Vertices are Fin (n+1), the depot is 0, and a customer set is a Finset (Fin (n+1)) not containing 0. The edge vector is a function x : Sym2 (Fin (n+1)) → ℝ on unordered pairs, and the cut value is ∑ i ∈ S, ∑ j ∈ Sᶜ, x s(i, j), which includes the edges to the depot. The capacity $Q$ is real (the paper does not say it is an integer) and demands are natural numbers with $0 < q_i \le Q$ for customers. The bin-packing number is the least number of bins over assignments of the customers of $S$ to bins of total demand at most $Q$ ; under $q_i \le Q$ this minimum exists. Of the LP point only $x \ge 0$ is assumed in Proposition 1 and targets 1–4, which is at least as strong as the paper's setting. The hypothesis " $x(\delta(R)) \ge 2$ for all $R \subset S$ " ranges over nonempty proper subsets.

A formalization that lets $R = \emptyset$ in that hypothesis is vacuous, because $x(\delta(\emptyset)) = 0$ ; one that drops the condition " $S \subseteq T'$ or $S \cap T' = \emptyset$ " from safe shrinking is trivial (take $T' = T$ ); and one that defines $r$ as $k$ , as an arbitrary monotone function, or with a junk value $0$ , or that omits the depot edges from the cut, states a different result. None of these is the mission's statement.

Needed infrastructure: finite sums over cuts of Sym2-indexed vectors, a working API for the bin-packing number, and, for target 5, connected components of the support graph (SimpleGraph.Reachable). The cut-function lemmas and the bin-packing number are reusable for any later formalization of CVRP polyhedra (framed capacity, comb and multistar inequalities). Contributions of general lemmas about cut functions on complete graphs are welcome as separate theorems.

Selected references

J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming Ser. A 100 (2004) 423–445. https://doi.org/10.1007/s10107-003-0481-8
G. L. Nemhauser, L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
P. Augerat, J. M. Belenguer, E. Benavent, A. Corberán, D. Naddef, Separating capacity constraints in the CVRP using tabu search, European Journal of Operational Research 106 (1998) 546–557. https://doi.org/10.1016/S0377-2217(97)00290-7
T. K. Ralphs, L. Kopman, W. R. Pulleyblank, L. E. Trotter, On the capacitated vehicle routing problem, Mathematical Programming 94 (2003) 343–359. https://doi.org/10.1007/s10107-002-0323-0

13 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

Selected Topics in Column Generation II: A Strictly Redundant Column Is Never Optimal for the Ratio Pricing ProblemResearch Paper

Motivation

Column generation solves linear programs with far more columns than can be written down: a restricted master problem holds a few columns, its dual multipliers are passed to a pricing problem, and the pricing problem returns a column to add. It is the standard engine behind branch-and-price for vehicle routing, crew scheduling and cutting stock, where the master problem is very often a set-partitioning problem (Lübbecke and Desrosiers 2005; Desrosiers and Lübbecke 2005).

Which column the pricing problem returns matters. The classical Dantzig rule picks the column of most negative reduced cost, but in set-partitioning masters with identical subproblems this rule tends to produce columns that are "weak" in the dual: their dual constraint is implied by the constraints of smaller columns. Sol (1994, PhD thesis, Eindhoven) called such columns redundant and studied pricing rules that avoid them. In their survey, Lübbecke and Desrosiers state the key fact as Proposition 2 (Operations Research 53(6), p. 1016): under ratio pricing, a strictly redundant column is never the optimal choice.

Setting

Let the rows of a set-partitioning master problem be $\{1,\dots,m\}$ . A column is a subset $s$ of the rows, with incidence vector $\mathbf a_s \in \{0,1\}^m$ ( $(\mathbf a_s)_i = 1$ iff $i \in s$ ). Let $\mathcal A$ be a finite collection of nonempty columns with costs $c_s$ . The master problem is

\min \sum_{s \in \mathcal A} c_s \lambda_s \quad\text{s.t.}\quad \sum_{s \in \mathcal A} \mathbf a_s \lambda_s = \mathbf 1,\ \lambda \ge 0,

with $\lambda$ integer in the integer program. Its dual has one free multiplier $u_i$ per row and one constraint $\mathbf u^{\mathsf T}\mathbf a_s \le c_s$ per column.

A column $s$ is redundant, eq. (30), p. 1015, if

\mathbf a_s = \sum_{r \subset s} \mathbf a_r \lambda_r \qquad\text{and}\qquad c_s \ge \sum_{r \subset s} c_r \lambda_r ,

with $\lambda_r \ge 0$ and $r$ ranging over the columns of $\mathcal A$ that are proper subsets of $s$ ; then its dual constraint is implied by those of its subcolumns. It is strictly redundant if the cost inequality is strict. The pair $(\mathcal A, \mathbf c)$ has the subcolumn property if $c_r < c_s$ for all $r, s \in \mathcal A$ with $r \subsetneq s$ . Given dual multipliers $\bar{\mathbf u} \in \mathbb R^m$ , the ratio pricing problem (31) is

\min\left\{ \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a} \;\middle|\; \mathbf a \in \mathcal A \right\},

the reduced cost per covered row. In Lean these objects are incidence, IsRedundant, IsStrictlyRedundant, SubcolumnProperty and pricingRatio in the namespace Lubbecke2005.SubcolumnPricing.

Formalization targets

Goal: Proposition 2 (p. 1016)

Let $(\mathcal A, \mathbf c)$ satisfy the subcolumn property, $\emptyset \notin \mathcal A$ , and let $\bar{\mathbf u} \in \mathbb R^m$ be arbitrary. If $s \in \mathcal A$ is strictly redundant, then

\neg\Bigl(\forall \mathbf a \in \mathcal A:\ \frac{c_s - \bar{\mathbf u}^{\mathsf T}\mathbf a_s}{\mathbf 1^{\mathsf T}\mathbf a_s} \le \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a}\Bigr),

that is, $\mathbf a_s$ is not an optimal solution of (31). The paper states the proposition and refers to Sol (1994) for the concept; it gives no proof.

Milestone: the cost shift (§5.1, p. 1016)

If only $c_r \le c_s$ holds for $r \subsetneq s$ in $\mathcal A$ , the shifted costs $c'_s = c_s + |s|$ satisfy the subcolumn property, and on every $\lambda$ with $\sum_s \mathbf a_s \lambda_s = \mathbf 1$ ,

\sum_{s} c'_s \lambda_s = \sum_s c_s \lambda_s + m .

This is the paper's remark that the shift "adds to $z^\star$ a constant term equal to the number of rows and does not change the problem".

Significance

Proposition 2 is the paper's argument for alternative pricing rules (§5.2): it shows that dividing the reduced cost by the number of covered rows filters out a whole class of columns that contribute nothing to the dual polyhedron, whatever the current dual multipliers are. Steepest-edge pricing, Devex and the lambda pricing rule are motivated along the same lines. The cost-shift remark extends the proposition to cost structures that are only weakly monotone under inclusion, which covers the frequent case of costs that do not decrease when rows are added to a column.

The result is published and elementary once stated precisely, but the paper leaves the definition of redundancy informal (no sign on $\lambda$ , no index set of the sum), and those choices decide whether the proposition is true. A formal statement pins them down. To our knowledge neither the proposition nor the vocabulary of redundant columns and ratio pricing has a machine-checked formalization; the definitions here are reusable for other statements about pricing rules in set-partitioning column generation.

Difficulty

The mathematical difficulty is modest; the difficulty is in the reading. With multipliers $\lambda_r$ of arbitrary sign in (30), the proposition is false: on rows $\{1,2,3\}$ take $s = \{1,2,3\}$ , $r_1 = \{1,2\}$ , $r_2 = \{2,3\}$ , $r_3 = \{2\}$ with costs $2.2$ , $2$ , $2$ , $1.9$ and $\bar{\mathbf u} = 0$ ; then $\mathbf a_s = \mathbf a_{r_1} + \mathbf a_{r_2} - \mathbf a_{r_3}$ , $2.2 > 2.1$ , the subcolumn property holds, and $s$ has the unique smallest ratio. The empty column is a second trap: its denominator $\mathbf 1^{\mathsf T}\mathbf a$ is zero. The formal statement has to exclude both, and has to keep the minimum in (31) over $\mathcal A$ only.

Formalization scope

Conventions committed to in Lean:

Rows are Fin m (indexed from $0$ ); a column is a Finset (Fin m), and its incidence vector is the real 0/1 vector incidence s : Fin m → ℝ. The collection $\mathcal A$ is a Finset (Finset (Fin m)); costs are a function Finset (Fin m) → ℝ, of which only the values on $\mathcal A$ matter.
Reading of (30): the multipliers are nonnegative ( $\lambda_r \ge 0$ ), the Farkas form of "the corresponding constraint is redundant for the dual problem". The paper leaves the sign implicit; with signed multipliers the proposition fails (example above).
Reading of $r \subset s$ : proper inclusion, over columns $r \in \mathcal A$ only. With $r \subseteq s$ every column would be redundant via $\lambda_s = 1$ .
Strictly redundant: (30) with strict cost inequality; the equality part is unchanged.
Reading of (31)'s denominator: $\emptyset \notin \mathcal A$ is a hypothesis of the goal ("a set-partitioning column covers at least one row"); it is named here as an addition to the literal text. The denominator is 1 ⬝ᵥ incidence a, which equals $|a|$ .
Dual multipliers: $\bar{\mathbf u} \in \mathbb R^m$ is arbitrary; no sign, no optimality for the restricted master.
"Cannot be an optimal solution" is stated literally as the negation of "the ratio of $\mathbf a_s$ is at most the ratio of every column of $\mathcal A$ "; this is equivalent to the existence of a column with strictly smaller ratio. No infimum over real sets is used.
The subcolumn property is kept as a hypothesis because the paper states it, although the conclusion may hold without it.
Cost shift: stated for real multipliers; the optimal value $z^\star$ is not formalized, and "does not change the problem" is rendered as the pointwise identity on the feasible set.

A trivializing formalization — a redundancy witness not tied to the proper subcolumns of $s$ in $\mathcal A$ , signed multipliers, or an empty column with ratio $0$ — is ruled out by the definitions above.

Needed infrastructure is only finite sums of vectors in $\mathbb R^m$ and the identity $\mathbf 1^{\mathsf T}\mathbf a_s = |s|$ . Contributions welcome: proofs of the goal and the milestone, and further statements from §5 (for example the redundancy characterisation of Sol 1994) built on the same definitions.

Selected references

M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
M. Sol, Column Generation Techniques for Pickup and Delivery Problems, PhD thesis, Eindhoven University of Technology, 1994 (cited in the paper as Sol 1994).
J. Desrosiers and M. E. Lübbecke, A Primer in Column Generation, in Column Generation, Springer, 2005. https://doi.org/10.1007/0-387-25486-2_1
F. Vanderbeck, Decomposition and Column Generation for Integer Programs, PhD thesis, Université catholique de Louvain, 1994.

3 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization I: Cluster Points of the Proximal ADMM Are Stationary and Improve on a Non-Stationary StartResearch Paper

Motivation

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

\min_x\ h(x) + P(\mathcal M x),

where $h$ is smooth (a least-squares loss, for instance), $P$ is a nonsmooth regularizer or constraint, and $\mathcal M$ is a linear map such as a finite-difference operator. When $P$ is nonconvex — the cardinality function $\|\cdot\|_0$ , the $\ell_{1/2}$ quasi-norm, the indicator of a nonconvex set — the problem is NP-hard in general, and the realistic goal is a stationary point. The alternating direction method of multipliers (ADMM) is widely used on such problems because each iteration splits into a proximal step on $P$ and a smooth step on $h$ , but for nonconvex $P$ it was long used without a convergence theory.

Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave one of the first general analyses. Their Theorem 1 shows that, under explicit conditions on the penalty parameter and a proximal term, every cluster point of a proximal ADMM sequence is stationary, and that a suitable start is strictly improved on. Earlier, Ames and Hong (arXiv:1401.5492) proved convergence of the plain ADMM for one specific nonconvex quadratic problem with an $\ell_1$ and norm-ball term; Li–Pong's argument follows their idea of bounding the dual changes by the primal changes, together with a descent analysis of the augmented Lagrangian from Wen, Peng, Liu, Bai and Sun (Optimization Online 2013/01/3730).

Setting

Let $h : \mathbb{R}^n \to \mathbb{R}$ be twice continuously differentiable with bounded Hessian $\nabla^2 h$ , let $P : \mathbb{R}^m \to (-\infty, +\infty]$ be proper (finite somewhere, never $-\infty$ ) and closed (lower semicontinuous), and let $\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ be linear with adjoint $\mathcal M^*$ .

A vector $v$ is a regular subgradient of $f$ at $x$ (with $f(x)$ finite) if $\liminf_{z \to x} \frac{f(z) - f(x) - \langle v, z-x\rangle}{\|z - x\|} \ge 0$ . The limiting subdifferential $\partial f(x)$ collects all limits $v = \lim v^t$ of regular subgradients $v^t$ at points $x^t \to x$ with $f(x^t) \to f(x)$ . A point $x$ is stationary if

0 \in \nabla h(x) + \mathcal M^* \partial P(\mathcal M x).

For $\beta > 0$ the augmented Lagrangian is $L_\beta(x,y,z) = h(x) + P(y) - \langle z, \mathcal M x - y\rangle + \frac\beta2\|\mathcal M x - y\|^2$ , and for a convex $C^2$ function $\phi$ the Bregman distance is $D_\phi(x_1,x_2) = \phi(x_1) - \phi(x_2) - \langle\nabla\phi(x_2), x_1 - x_2\rangle$ . The proximal ADMM generates, from arbitrary $x^0, z^0$ ,

y^{t+1} \in \operatorname{Arg\,min}_y L_\beta(x^t, y, z^t),\quad x^{t+1} \in \operatorname{Arg\,min}_x \{L_\beta(x, y^{t+1}, z^t) + D_\phi(x, x^t)\},\quad z^{t+1} = z^t - \beta(\mathcal M x^{t+1} - y^{t+1}).

Assumption 1 requires $\mathcal M\mathcal M^* \succeq \sigma\mathcal I$ for some $\sigma > 0$ (so $\mathcal M$ is surjective), Loewner bounds $\mathcal Q_1 \succeq \nabla^2 h \succeq \mathcal Q_2$ , $\mathcal T_1^2 \succeq [\nabla^2\phi]^2 \succeq \mathcal T_2^2$ with $\mathcal T_1 \succeq \mathcal T_2 \succeq 0$ , $\mathcal Q_3 \succeq [\nabla^2 h + \nabla^2 \phi]^2$ , a strong-convexity margin $\mathcal Q_2 + \beta\mathcal M^*\mathcal M + \mathcal T_2 \succeq \delta\mathcal I$ , and some $\gamma \in (0,1)$ with $\delta\mathcal I + \mathcal T_2 \succ \frac{2}{\sigma\beta}\big(\frac1\gamma \mathcal Q_3 + \frac1{1-\gamma}\mathcal T_1^2\big)$ . Here $\|x\|^2_{\mathcal T} := \langle x, \mathcal T x\rangle$ .

Formalization targets

Goal: Theorem 1 (p. 7)

Under the standing assumptions and Assumption 1, for every proximal ADMM sequence:

(Global subsequential convergence) at every cluster point $(x^*, y^*, z^*)$ ,

\lim_{t\to\infty}\|y^{t+1}-y^t\|^2 + \|x^{t+1}-x^t\|^2 + \|z^{t+1}-z^t\|^2 = 0,\qquad \nabla h(x^*) = \mathcal M^* z^*,\ \ -z^* \in \partial P(y^*),\ \ y^* = \mathcal M x^*,

and $x^*$ is stationary; 2. (Strict improvement) if $x^0$ is not stationary, $h(x^0) + P(\mathcal M x^0) < \infty$ and $\mathcal M^* z^0 = \nabla h(x^0)$ , then every cluster point satisfies

h(x^*) + P(\mathcal M x^*) < h(x^0) + P(\mathcal M x^0).

The theorem does not assert that a cluster point exists; that is the subject of Theorem 2 of the same paper.

Milestones

In attack order: the robustness (3) of $\partial$ ; the optimality relations (11) of each iterate; the passage from (9) and (10) to (12) and stationarity; the dual-step bound (14); the one-step estimate (20) and its summed form (21) for $L_\beta$ ; the vanishing of the primal steps (16); the convergence (10) of $P(y^{t_i+1})$ ; and, for part (ii), $x^1 \ne x^0$ , the first-step estimate (27) and the strict decrease after (28).

Significance

Theorem 1 turns the proximal ADMM into a method with a guarantee for a nonconvex $P$ : any limit it produces is a stationary point, and with the initialization of part (ii) — for example, a stationary point of a convex relaxation — it cannot return to a stationary point worse than its start. The conditions are checkable: Remark 1 of the paper shows that the choice $\phi(x) = \frac L2\|x\|^2 - h(x)$ turns the $x$ -update into a convex quadratic program, and that the last condition of Assumption 1 can be enforced by taking $\beta$ large when $\phi$ , $\mathcal T_1$ , $\mathcal T_2$ do not depend on $\beta$ . The estimate (20) is reused by the paper's boundedness result (Theorem 2), and its whole-sequence convergence result for semi-algebraic data (Theorem 3) starts from Theorem 1.

The result is proved in the paper; Mathlib contains neither the limiting subdifferential nor any convergence theorem for ADMM, so none of it is formalized yet. A formalization would give a verified library of the limiting subdifferential of extended-real-valued functions, its robustness and its Fermat rule with a smooth sum, and the first formally verified convergence theorem for ADMM with a nonconvex term.

Difficulty

The obvious argument — "the augmented Lagrangian decreases, so it converges" — fails: $L_\beta$ need not decrease, because the multiplier step increases it by $\frac1\beta\|z^{t+1}-z^t\|^2$ . The proof has to bound this increase by primal steps, which uses surjectivity of $\mathcal M$ and the squared Hessian bounds, and it produces a two-step recursion (involving $x^{t-1}$ ) rather than a monotone sequence. Nor is $L_\beta$ known to be bounded below; the proof uses the cluster point and lower semicontinuity to get a lower bound along a subsequence. Passing to the limit in the inclusion for $\partial P$ requires $P(y^{t_i+1}) \to P(y^*)$ , which lower semicontinuity alone does not give. For part (ii), the start $y^0$ is not an iterate at all, so the first step needs its own estimate.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $\mathcal M$ is a continuous linear map and $\mathcal M^*$ is ContinuousLinearMap.adjoint. $P$ and $L_\beta$ take values in EReal; inequalities involving $L_\beta$ are written additively ( $a \le b + r$ with real $r$ ), never through EReal.toReal. The Hessian is the derivative of the gradient. $\succeq$ is Mathlib's Loewner order on self-maps, which includes symmetry of the difference; $\succ$ adds positive definiteness. $\|x\|^2_{\mathcal T} = \langle x, \mathcal T x\rangle$ for every $\mathcal T$ , possibly indefinite. The witnesses of Assumption 1 are explicit parameters, universally quantified. A proximal ADMM sequence is any triple of sequences satisfying the three updates (global minimizers, not necessarily unique); $x^0, z^0$ are free and $y^0$ is unconstrained. A cluster point is the limit along a strictly increasing subsequence. Stationarity is the inclusion (4) itself.

The limiting subdifferential keeps all three requirements of its definition — $x^t \to x$ , $f(x^t) \to f(x)$ and $v^t \to v$ — and the domain condition $f(x) < \infty$ ; dropping $f$ -attentive convergence or replacing $\partial$ by the convex subdifferential would make stationarity a different, and for nonconvex $P$ wrong, notion. Part (ii) is a strict inequality for every cluster point, and its hypotheses are exactly non-stationarity of $x^0$ , finiteness of the objective at $x^0$ and $\mathcal M^* z^0 = \nabla h(x^0)$ . The paper's assumption that proximal maps of $P$ exist is not a hypothesis, since no statement asserts that the iteration can be run.

Needed infrastructure: Fermat's rule and the smooth sum rule for regular subgradients, a diagonal argument for (3), Taylor bounds for $C^2$ functions with Loewner-bounded Hessians (the paper's (5) and (6)), strong convexity from a Hessian lower bound, and the monotonicity of the positive square root in the Loewner order. These are reusable well beyond this mission; contributions of any of them as separate lemmas are welcome.

Selected references

G. Li, T. K. Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, SIAM J. Optim. 25(4), 2015. arXiv:1407.0753v6, https://arxiv.org/abs/1407.0753 (cited version), DOI https://doi.org/10.1137/140998135
B. P. W. Ames, M. Hong, Alternating direction method of multipliers for sparse zero-variance discriminant analysis and principal component analysis, preprint, 2014. https://arxiv.org/abs/1401.5492
Z. Wen, X. Peng, X. Liu, X. Bai, X. Sun, Asset allocation under the Basel accord risk measures, preprint, 2013. http://www.optimization-online.org/DB_HTML/2013/01/3730.html
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

17 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research·Captain: mikedeng1

Accelerated Proximal Point Method for Maximally Monotone Operators: The Fixed-Point Residual Rate of the Accelerated MethodResearch Paper

Motivation

Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.

For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from $O(1/i)$ to $O(1/i^2)$ . For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual $\|x_{i}-y_{i-1}\|$ , the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate $O(1/i)$ for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most $R^2/i^2$ .

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ . A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns a subset $Mx\subseteq\mathcal H$ to every point $x$ . It is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in Mx$ and $v\in My$ , and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of $M$ . The class of maximally monotone operators is $\mathcal M(\mathcal H)$ , and $X_*(M)=\{x:0\in Mx\}$ is the set of zeros.

For a step size $\lambda>0$ , the resolvent $J_{\lambda M}=(I+\lambda M)^{-1}$ maps $y$ to the unique $x$ with $y\in x+\lambda Mx$ . It is single-valued for monotone $M$ and defined on all of $\mathcal H$ for maximally monotone $M$ .

The general proximal point method with step coefficients $h=\{h_{i,k}\}$ starts at $y_0$ and iterates

x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=y_i+\sum_{k=0}^{i}h_{i+1,k+1}(x_{k+1}-y_k).

Kim's proposed accelerated proximal point method starts at $x_0=y_0=y_{-1}$ and iterates

x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=x_{i+1}+\frac{i}{i+2}(x_{i+1}-x_i)-\frac{i}{i+2}(x_i-y_{i-1}).

The coefficients (25) are $h_{i,k}=-\frac{2k}{i(i+1)}$ for $k<i$ and $h_{i,i}=\frac{2i}{i+1}$ .

The PEP of Section 3 bounds the worst case of $\|x_N-y_{N-1}\|^2/R^2$ over all $M\in\mathcal M(\mathcal H)$ and all starts with $\|y_0-x_*\|\le R$ . A semidefinite relaxation leads to the dual problem (D): minimize $c$ over nonnegative $a_2,\dots,a_N,b_N,c$ such that $\sum_{i=2}^Na_iA_{i-1,i}(h)+b_NB_N(h)+cC-u_Nu_N^\top\succeq0$ . The matrices are explicit symmetric $(N+1)\times(N+1)$ matrices built from $h$ and the canonical basis $u_1,\dots,u_{N+1}$ . Its optimal value is $\mathcal B_D(h)$ .

Formalization targets

Goal: Theorem 4.1

For every $M\in\mathcal M(\mathcal H)$ , every $\lambda>0$ , every run of the proposed method, and every $x_*\in X_*(M)$ with $\|x_0-x_*\|\le R$ for a constant $R>0$ ,

\|x_i-y_{i-1}\|^2\le\frac{R^2}{i^2}\qquad\text{for every }i\ge1.

The constant is the paper's, and nothing is left unfixed.

Milestones

Lemma 4.1. For every $N\ge1$ , $h$ from (25) with $a_i=\frac{2(i-1)i}{N^2}$ , $b_N=\frac2N$ , $c=\frac1{N^2}$ is feasible for (D) and for (HD) $=\min_h\mathcal B_D(h)$ .
Section 3, (D). For any $h$ and any feasible point of (D), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le c$ for every run of the general method with $\|y_0-x_*\|\le R$ .
Eq. (28). With $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$ for every $N\ge1$ .
Proposition 4.1. The general method with (25) and the proposed method generate identical sequences from the same initial point.

Significance

Theorem 4.1 gives the first $O(1/i^2)$ rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).

The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.

Difficulty

The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an $(N+1)\times(N+1)$ matrix whose entries are double sums over $h$ , uniformly in $N$ . The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in $\mathcal H$ . The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for $\dim\mathcal H\ge N+1$ (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at $i=0,1$ .

Formalization scope

$\mathcal H$ is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.

The resolvent step is relational: $x_{i+1}=J_{\lambda M}(y_i)$ is encoded as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$ . For monotone $M$ and $\lambda>0$ this determines $x_{i+1}$ uniquely, and for maximally monotone $M$ such an $x_{i+1}$ exists for every $y_i$ (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's $y_{-1}=y_0$ is y (0 - 1) = y 0 under natural-number subtraction. The general method has no $x_0$ , so its initial-distance condition is on $y_0$ , as in (17). The step size $\lambda$ is written lam.

PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i $=u_i$ . $\mathcal B_D(h)$ is the infimum of the feasible values of $c$ computed in EReal, so an infeasible $h$ gets the value $+\infty$ as in the paper; Eq. (28) compares it with the real bounds cast to EReal.

A formalization in which the iterate predicate cannot be satisfied, the residual is $\|x_i-x_{i-1}\|$ , the correction term is dropped or has the wrong sign, the initial point is decoupled ( $x_0\ne y_0$ ), or $M$ is only monotone on finitely many points, would state a different theorem, and none is used here.

Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in $\mathcal H$ (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.

Selected references

D. Kim, Accelerated proximal point method for maximally monotone operators, Math. Program. 190 (2021) 57–87; arXiv:1905.05149v4. https://arxiv.org/abs/1905.05149
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
O. Güler, New proximal point algorithms for convex minimization, SIAM J. Optim. 2 (1992) 649–664. https://doi.org/10.1137/0802032
Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Math. Program. 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
G. Gu, J. Yang, Tight sublinear convergence rate of the proximal point algorithm for maximal monotone inclusion problems, SIAM J. Optim. 30 (2020) 1905–1921. https://doi.org/10.1137/19M1299049
F. Lieder, On the convergence rate of the Halpern-iteration, Optim. Lett. 15 (2021) 405–418. https://doi.org/10.1007/s11590-020-01617-9
J. Park, E. K. Ryu, Exact optimal accelerated complexity for fixed-point iterations, ICML 2022; arXiv:2201.11413. https://arxiv.org/abs/2201.11413
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

10 thms2 active usersReviewed

Combinatorics Linear Optimization Operations Research·Captain: mikedeng1

An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem I: ALGORITHM 1, Linear Grouping with LP Rounding, Is an Asymptotic Approximation SchemeResearch Paper

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$ . It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.

1961–1963: Gilmore and Gomory introduce the configuration linear program for cutting stock and solve it by column generation (Gilmore–Gomory 1961).
1974: Johnson, Demers, Ullman, Garey and Graham analyse First Fit and related heuristics, with asymptotic ratio $17/10$ and $11/9$ (Johnson et al. 1974).
1981: Fernandez de la Vega and Lueker give the first asymptotic approximation scheme, packing within $(1+\varepsilon)\,OPT(I) + 1$ bins in time linear in $n$ for fixed $\varepsilon$ , using elimination of small pieces and linear grouping (Fernandez de la Vega–Lueker 1981).
1982: Karmarkar and Karp replace the enumeration of configurations by an approximate solution of the configuration LP and a rounding step, obtaining an additive term polynomial in $1/\varepsilon$ (this mission), and, with geometric grouping, $OPT(I) + O(\log^2 OPT(I))$ (Karmarkar–Karp 1982).
2013–2017: Rothvoß and then Hoberg–Rothvoß improve the additive term to $O(\log OPT \cdot \log\log OPT)$ and $O(\log OPT)$ (Hoberg–Rothvoß 2017).

Setting

An instance $I$ is a finite multiset of piece sizes, each in the open interval $(0,1)$ . Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, and $SIZE(I)$ for the sum of all sizes. A packing of $I$ is a finite multiset of bins, each a multiset of sizes, whose union is exactly $I$ and in which every bin has total size at most $1$ . Its cost is the number of bins, and $OPT(I)$ is the minimum cost.

A configuration of $I$ is a nonempty multiset of sizes occurring in $I$ with total at most $1$ . With $b_t$ the number of pieces of size $t$ and $a_{tc}$ the number of occurrences of $t$ in configuration $c$ , the fractional bin-packing problem is the linear program

\min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x\ge 0,\qquad \sum_c a_{tc}x_c \ge b_t\ \ \text{for every size } t,

whose optimal value is $LIN(I)$ . A basic feasible solution is an extreme point of its feasible region.

For instances $I,J$ , write $I\le J$ if there is a one-to-one map $f$ from the pieces of $I$ into the pieces of $J$ with $x\le f(x)$ . Linear grouping with parameter $k$ sorts $I$ non-increasingly, cuts it into groups $G_1,\dots,G_q$ of $k$ consecutive pieces (the last possibly shorter), rounds every piece of $G_i$ up to the largest size of $G_i$ to get $G_i'$ , and outputs $J = \bigcup_{i\ge 2} G_i'$ and $J' = G_1$ .

ALGORITHM 1 takes $I$ and $\varepsilon>0$ : (1) discard the pieces of size $\le \max(1/n(I), \varepsilon/2)$ , leaving $J$ ; (2) apply linear grouping to $J$ with $k = \lceil n(J)\varepsilon^2\rceil$ , giving $K$ and $K'$ ; (3) put each piece of $K'$ in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution $x$ of the LP of $K$ with $\mathbf 1\cdot x\le LIN(K)+1$ ; (5) round $x$ to a packing of $K$ with at most $\mathbf 1\cdot x + (m(K)+1)/2$ bins; (6) shrink the pieces back to obtain a packing of $J$ ; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. $A(I)$ is the cost of the resulting packing.

Formalization targets

Goal: Theorem 3, as its proof establishes it

A(I) \le (1+2\varepsilon)\,OPT(I) + \frac{1}{2\varepsilon^2} + 3 \qquad\text{for every } \varepsilon>0,\ \text{every instance } I,\ \text{every run of ALGORITHM 1.}

The additive term depends on $\varepsilon$ only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor $1+\varepsilon$ , which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with $\varepsilon/2$ gives the paper's main result (4), $A(I)\le(1+\varepsilon)OPT(I)+O(\varepsilon^{-2})$ , stated as a separate corollary with the explicit term $2/\varepsilon^2+3$ .

Milestones

Lemma 1: $OPT(I)\le 2\,SIZE(I)+1$ .
Lemma 2: $SIZE(I)\le LIN(I)\le OPT(I)\le LIN(I)+\frac{m(I)+1}{2}$ .
Corollary 1: every basic feasible solution $x$ can be rounded to a packing of cost $\le \mathbf 1\cdot x + \frac{m(I)+1}{2}$ .
Lemma 3: inserting pieces of size $\le g/2$ last, with new bins only when necessary, costs at most $\max(A, (1+g)\,OPT(I)+1)$ .
Monotonicity: $I\le J$ implies $OPT$ , $LIN$ and $SIZE$ do not decrease.
Lemma 4: linear grouping loses at most $k$ in $OPT$ , $LIN$ and $SIZE$ .
Proof steps (ii)–(iii) (corrected): $k\le 2\varepsilon\,OPT(I)+1$ .
Proof step (iv): $m(K)\le 1/\varepsilon^2$ .
Proof step (vii): $\mathbf 1\cdot x\le OPT(I)+1$ .
Proof step (viii) (corrected): the packing of Step 6 has at most $(1+2\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+\frac52$ bins.

Significance

The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within $(m+1)/2$ of the integer optimum, and grouping reduces $m$ at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.

The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order $I\le J$ , any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.

Difficulty

The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of $\{x\ge0,\ Ax\ge b\}$ has at most as many nonzero coordinates as there are rows of $A$ ; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of $LIN$ under $I\le J$ ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.

Formalization scope

Sizes are real numbers in the open interval $(0,1)$ ; the paper says "a rational number between 0 and 1". Real sizes generalize rational ones; the open interval is what the paper's arguments use.
Instances are Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most $1$ , empty bins allowed and counted. $OPT$ is a natural-number infimum over a set that is always nonempty.
LP solutions are Multiset ℝ →₀ ℝ supported on configurations. $LIN$ is a real infimum over a set that is nonempty (singleton configurations) and bounded below by $0$ . "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.
The Fractional Bin-Packing subroutine is modelled by its contract only (§5, p. 315): any basic feasible solution of cost at most $LIN(K)+1$ . The ellipsoid method of §6 is not modelled.
ALGORITHM 1 is a relation Alg1Run ε I P: $P$ is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.
The paper's $O(\cdot)$ in result (4) is replaced by the explicit $2/\varepsilon^2+3$ .
Corrected statements. The printed Theorem 3 bound $(1+\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+3$ fails: for $\varepsilon=1/10$ and $19\,000$ pieces of size $0.051$ , some run uses $1180$ bins while the bound is $1153$ . The failing step is (ii), $SIZE(J)\ge\varepsilon\,n(J)$ , since Step 1 discards only pieces $\le\varepsilon/2$ . Steps (ii)–(iii) and (viii) are stated with $2\varepsilon$ ; step (iv) is stated as $m(K)\le 1/\varepsilon^2$ because its first link $m(K)\le n(K)/k$ fails when the last group is short.
Running time (Theorem 3's first half, Corollary 1's time bound, the function $T$ ) is out of scope.
Trivializations are ruled out: "some packing has at most the bound" is not the goal; the goal constrains every output of the algorithm, and the packing property of that output is part of its conclusion.

Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.

Selected references

N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd FOCS (SFCS 1982), IEEE, pp. 312–320. https://doi.org/10.1109/sfcs.1982.61
W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1+ε in linear time, Combinatorica 1 (1981) 349–355. https://doi.org/10.1007/BF02579456
P. C. Gilmore, R. E. Gomory, A Linear Programming Approach to the Cutting-Stock Problem, Operations Research 9 (1961) 849–859. https://doi.org/10.1287/opre.9.6.849
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 (1974) 299–325. https://doi.org/10.1137/0203025
R. Hoberg, T. Rothvoß, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. SODA 2017, 2616–2625. https://doi.org/10.1137/1.9781611974782.172

16 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Optimal Two- and Three-Stage Production Schedules with Setup Times Included 1: Johnson's Rule Minimizes the Total Elapsed Time on Two MachinesResearch Paper

Motivation

A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written $F2\,\|\,C_{\max}$ . The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.

Timeline:

1954. Johnson proves the two-machine rule and a three-machine special case (the latter is the second mission of this series).
1976. Garey, Johnson and Sethi prove that the three-machine flow shop is NP-hard in the strong sense, so the two-machine case marks the boundary of tractability.

Setting

There are $n$ items $i = 1, \dots, n$ . Item $i$ needs $A_i > 0$ units of time on machine 1 and then $B_i > 0$ units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times $s^1_i$ and $s^2_i$ . It is feasible when all start times are nonnegative, the intervals $[s^1_i, s^1_i + A_i]$ of distinct items do not overlap on machine 1, the intervals $[s^2_i, s^2_i + B_i]$ do not overlap on machine 2, and $s^1_i + A_i \le s^2_i$ for every item. The total elapsed time $T(s) = \max_i (s^2_i + B_i)$ is the time at which the last item leaves machine 2.

An order is a permutation $\sigma$ , where $\sigma(k)$ is the item in position $k$ . The as-soon-as-possible schedule $a_\sigma$ of an order processes the items in the order $\sigma$ on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.

Relation (II). Item $i$ is definitely preferred to item $j$ when

\min(A_i, B_j) < \min(A_j, B_i),

and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.

For an order $\sigma$ the paper uses the quantities

K_u = \sum_{l \le u} A_{\sigma(l)} - \sum_{l < u} B_{\sigma(l)}, \qquad F(\sigma) = \max_u K_u .

Formalization targets

Goal: Theorem 1 (p. 63)

For positive $A, B$ :

\exists\, \sigma \text{ consistent with (II)}, \qquad\text{and}\qquad \forall\, \sigma \text{ consistent with (II)},\ \forall\, s \text{ feasible}:\quad a_\sigma \text{ is feasible and } T(a_\sigma) \le T(s).

The comparison is against every feasible schedule, including those whose two machines follow different orders.

Milestones

Lemma 1 (p. 61). Every feasible schedule can be replaced, at no greater total elapsed time, by a feasible schedule that follows one common order on both machines.
As soon as possible (p. 62). For a fixed common order, $a_\sigma$ is feasible and minimizes $T$ among the feasible schedules that follow $\sigma$ .
Closed form (p. 62). $T(a_\sigma) = \sum_i B_i + F(\sigma)$ , i.e. the total idle time of machine 2 is $\max_u K_u$ .
Adjacent interchange (p. 63). Interchanging the items in positions $j, j+1$ leaves every other $K_u$ unchanged. Moreover, $\max(K_j, K_{j+1}) < \max(K'_j, K'_{j+1})$ holds if and only if (II) holds for the pair.
Interchanges do not increase $F$ (p. 63). If the pair in positions $j, j+1$ satisfies (II) non-strictly, then $F(\sigma) \le F(\sigma')$ .
Lemma 2 (p. 64). Relation (II) is transitive, except when the middle item is indifferent to both others.
Worked example (p. 65). For $A = (4,4,30,6,2)$ and $B = (5,1,4,30,3)$ , the order $(5,1,4,3,2)$ takes 47 units with 4 units of idle time. The reversed order takes 78 units, and every order takes between 47 and 78 units.

Significance

The theorem reduces an optimization over a continuum of start-time vectors, and over $n!$ orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in $O(n \log n)$ time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for $m$ machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form $T(a_\sigma) = \sum_i B_i + \max_u K_u$ reappears across flow-shop theory as a longest-path formula.

The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.

Difficulty

The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items $(A, B) = (5,2), (1,1), (2,5)$ , in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.

Formalization scope

Items are Fin n (0-based) and times are real numbers. Positivity $A_i > 0$ , $B_i > 0$ is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions $j, j+1$ is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is $0$ when $n = 0$ . $K_u$ is indexed by 0-based positions (Lean's $K_u$ is the paper's $K_{u+1}$ ), and $F$ requires $n \ge 1$ .

Conventions made explicit or corrected:

"Consistent with all the definite preferences" is imposed on all pairs of positions $k < l$ as the non-strict inequality $\min(A_{\sigma(k)}, B_{\sigma(l)}) \le \min(A_{\sigma(l)}, B_{\sigma(k)})$ . The goal also asserts that such an order exists, so its main clause is not vacuous.
The display of $K'_u$ on p. 63 prints the upper limit $u$ on the $B'$ -sum. The definition of $K_u$ on p. 62 and the reduction of (I) to (II) require $u-1$ , and the formalization uses $u-1$ .
Lemma 2 keeps the page's exception (item 2 indifferent to both items); without it the statement is false.

Measuring the objective by $F(\sigma)$ , or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.

Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.

Selected references

S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. doi:10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. doi:10.1287/moor.1.2.117
R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5:287–326, 1979. doi:10.1016/S0167-5060(08)70356-X
H. G. Campbell, R. A. Dudek, M. L. Smith, A heuristic algorithm for the n job, m machine sequencing problem, Management Science 16(10):B630–B637, 1970. doi:10.1287/mnsc.16.10.B630

16 thms2 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Single Machine Scheduling with Release Dates III: The Random Per-Job α-Schedule with a Truncated Exponential DensityResearch Paper

Motivation

Scheduling jobs with release dates on one machine to minimize the total weighted completion time, written $1|r_j|\sum w_jC_j$ , is strongly NP-hard even with unit weights (Lenstra, Rinnooy Kan & Brucker, 1977). It is a basic model of scheduling theory and a standard testbed for approximation algorithms built on linear programming relaxations. Several LP relaxations give lower bounds for it (Dyer & Wolsey, 1990; Queyranne, 1993), and the question how far these bounds can be from the optimum is also a question about the quality of branch-and-bound methods that use them.

Timeline, as surveyed in Table 1 of Goemans, Queyranne, Schulz, Skutella & Wang (2002):

Phillips, Stein & Wein (Math. Programming, 1998) introduce converting a preemptive schedule into a nonpreemptive one by list scheduling, and the notion of $\alpha$ -points; for the weighted problem their bound is $16+\epsilon$ .
Hall, Shmoys & Wein (SODA 1996) obtain 4; Schulz (IPCO 1996) and Hall, Schulz, Shmoys & Wein (Math. Oper. Res., 1997) obtain 3; Chakrabarti et al. obtain $2.8854+\epsilon$ , and a combination of methods gives $2.4427+\epsilon$ .
Goemans (SODA 1997) orders jobs by $\alpha$ -points of the LP schedule: $\alpha=1/\sqrt2$ gives $1+\sqrt2\approx2.4143$ , a uniformly random $\alpha$ gives 2.
Chekuri, Motwani, Natarajan & Stein (SIAM J. Comput., 2001) use random $\alpha$ -points of an arbitrary preemptive schedule and obtain $e/(e-1)$ for unit weights, relative to the preemptive optimum rather than an LP value.
Goemans, Queyranne, Schulz, Skutella & Wang (2002) prove $1.7451$ for the best common $\alpha$ and $1.6853$ for job-dependent random $\alpha_j$ , both relative to the LP value $Z_R$ . Afrati et al. (FOCS 1999) later give a polynomial-time approximation scheme, which does not bound the LP relaxations.

This mission formalizes the $1.6853$ result, the paper's main theorem.

Setting

There are $n$ jobs $N=\{0,\dots,n-1\}$ . Job $j$ has an integral processing time $p_j>0$ , an integral release date $r_j\ge0$ and a weight $w_j>0$ . The jobs are indexed so that $w_0/p_0\ge w_1/p_1\ge\dots\ge w_{n-1}/p_{n-1}$ .

The LP schedule is the preemptive schedule that at every moment processes the available (released, unfinished) job of smallest index. Since the data are integral, it is determined slot by slot: in $[\tau,\tau+1)$ it runs the smallest-index job $j$ with $r_j\le\tau$ and work left, or idles. Let $A^{LP}_j\subseteq\mathbb R$ be the set of times at which it processes $j$ . The mean busy time of $j$ is

M^{LP}_j=\frac1{p_j}\int_{A^{LP}_j}t\,dt .

The mean busy time relaxation (R) has a variable $M_j$ per job:

Z_R=\min\Bigl\{\sum_j w_j\bigl(M_j+\tfrac12p_j\bigr)\ :\ \sum_{j\in S}p_jM_j\ge p(S)\bigl(r_{\min}(S)+\tfrac12p(S)\bigr)\ \text{for all nonempty }S\subseteq N\Bigr\},

with $p(S)=\sum_{j\in S}p_j$ and $r_{\min}(S)=\min_{j\in S}r_j$ . $Z_R$ is a lower bound on the optimum of $1|r_j|\sum w_jC_j$ .

For $0<\alpha\le1$ the $\alpha$ -point $t_j(\alpha)$ is the first time at which $j$ has been processed for $\alpha p_j$ units in the LP schedule; $t_j(0^+)$ is the start time of $j$ . For a vector $\boldsymbol\alpha\in(0,1]^n$ , the $(\alpha_j)$ -schedule processes the jobs nonpreemptively, as early as possible, in nondecreasing order of $t_j(\alpha_j)$ ; $C^{\boldsymbol\alpha}_j$ is the completion time of $j$ in it.

Let $\gamma\approx0.4835$ be the solution in $(0,1)$ of $\gamma+\ln(2-\gamma)=e^{-\gamma}\bigl((2-\gamma)e^{\gamma}-1\bigr)$ , and set

\delta=\gamma+\ln(2-\gamma)\approx0.8999,\qquad c=1+\frac{e^{-\gamma}}{\delta},\qquad g(\alpha)=\begin{cases}(c-1)e^\alpha&0<\alpha\le\delta,\\0&\text{otherwise.}\end{cases}

Formalization targets

Goal: Theorem 3.9 (p. 185)

$c<1.6853$ , and if $\alpha_1,\dots,\alpha_n$ each have density $g$ and are pairwise independent, then $\sum_j w_jC^{\boldsymbol\alpha}_j$ is integrable and

\mathbb E\Bigl[\sum_j w_jC^{\boldsymbol\alpha}_j\Bigr]\le c\cdot Z_R .

The bound is against the constant $c$ defined by the formula; the decimal $1.6853$ appears only in the separate inequality $c<1.6853$ .

Milestones

Theorem 2.5 (p. 173): $M^{LP}$ is an optimal solution of (R), so $Z_R=\sum_jw_j(M^{LP}_j+\tfrac12p_j)$ .
Eq. (3.1) (p. 176): $M^{LP}_j=\int_0^1t_j(\alpha)\,d\alpha$ .
Corollary 3.2 (p. 179): $C^{\boldsymbol\alpha}_j\le t_j(\alpha_j)+\sum_{k:\alpha_k\le\eta_k(\alpha_j)}(1+\alpha_k-\eta_k(\alpha_j))p_k$ , where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$ .
Eq. (3.10) (p. 182): $M^{LP}_j=t_j(0^+)+\sum_{k\in N_2}(1-\mu_k)p_k+\tfrac12p_j$ , where $N_2$ is the set of jobs processed between the start and completion of $j$ and $\mu_k$ is the fraction of $j$ processed before $k$ starts.
Eq. (3.11) (p. 183): the bound of Corollary 3.2 split over $N_1=N\setminus(N_2\cup\{j\})$ and $N_2$ .
Lemma 3.11 (p. 185): $g$ is a probability density on $(0,1]$ , and (i) $\int_0^\eta g(\alpha)(1+\alpha-\eta)\,d\alpha\le(c-1)\eta$ , (ii) $(1+E_g[\alpha])\int_\mu^1g(\alpha)\,d\alpha\le c(1-\mu)$ for $\eta,\mu\in[0,1]$ .

Significance

Theorem 3.9 gives a randomized algorithm for $1|r_j|\sum w_jC_j$ whose expected cost is at most $1.6853$ times the optimum, and a variant of it runs on-line (Theorem 3.14). Since $Z_R$ is a lower bound, it also shows that the relaxation (R), and the preemptive time-indexed relaxation (D), which has the same value, is within a factor $1.6853$ of the optimum (Corollary 3.10). The paper's Section 3.6 shows the gap of these relaxations can approach $e/(e-1)\approx1.5819$ , so the bound is not far from what this relaxation can give.

The result is proved on paper; no machine-checked proof exists, and no part of this theory (LP schedule, $\alpha$ -points, list scheduling from a preemptive schedule) is on the platform. The mission produces, besides the goal, a reusable formal account of $\alpha$ -point scheduling: the LP schedule as a concrete object, the identity between mean busy times and average $\alpha$ -points, and the deterministic completion-time bound of Corollary 3.2, which underlies many later $\alpha$ -point analyses.

Difficulty

The obvious argument, bounding $C^{\boldsymbol\alpha}_j$ by Corollary 3.2 and integrating each $\alpha_k$ independently against $g$ , does not work directly: the set of jobs $k$ with $\alpha_k\le\eta_k(\alpha_j)$ depends on $\alpha_j$ , and the two effects of the random $\alpha_k$ pull in opposite directions (a small $\alpha_k$ shrinks the terms $1+\alpha_k-\eta_k$ , a large one removes terms from the sum). The analysis needs the structure of the LP schedule around job $j$ (equations (3.9)–(3.11)) to separate the jobs whose $\eta_k$ is constant in $\alpha_j$ from those for which it jumps from $0$ to $1$ , and then a density tuned to both at once. The claim is made under pairwise independence only, so no product structure of the random vector is available. On the formal side, the LP schedule, $\alpha$ -points and list scheduling are defined from scratch, and the measure-theoretic content (integrability of a piecewise-constant function of $\boldsymbol\alpha$ , conditioning under pairwise independence) is real work.

Formalization scope

Jobs are Fin n (0-based), $p$ and $r$ are natural numbers and $w$ is real. The ordering by $w_j/p_j$ is a hypothesis of every statement about the LP schedule, which is defined by the smallest-index rule; under that hypothesis the two coincide. The LP schedule is defined slot by slot, which is exact for integral data. Processing is represented by sets of times, not indicator functions. $t_j(\alpha)$ is an infimum over times, $t_j(0^+)=\inf A^{LP}_j$ , and the $(\alpha_j)$ -schedule is the closed form $C^{\boldsymbol\alpha}_j=\max_{k\preceq j}\bigl(r_k+\sum_{k\preceq i\preceq j}p_i\bigr)$ of list scheduling in lexicographic (α-point, index) order. $Z_R$ is the real infimum of the objective over the feasible set of (R), which is nonempty and bounded below for $w\ge0$ . The random vector is any probability measure on $\mathbb R^n$ whose coordinate laws all equal the law with density $g$ and whose coordinates are pairwise independent; the product measure is one example, but the theorem is for all of them. $\gamma$ is any solution in $(0,1)$ of its equation.

A trivializing formalization is ruled out: the expectation is asserted together with integrability (a non-integrable integrand would have Bochner integral $0$ ), $g$ is supported on $(0,\delta]$ so every $\alpha_j$ lies in $(0,1]$ almost surely, and the bound is against $Z_R$ defined from (R), not against an expression that already contains Theorem 2.5.

Running times ( $O(n\log n)$ , $O(n^2)$ ), derandomization, the counting results (Proposition 3.8, Lemma 3.12) and the on-line variant are not formalized. Lemma 3.1 on the auxiliary $(\alpha_j)$ -Conversion schedule is not a milestone; Corollary 3.2 is stated directly for the $(\alpha_j)$ -schedule.

Contributions welcome: proofs of the milestones in any order; general lemmas on list scheduling and $\alpha$ -points of preemptive schedules, which are reusable beyond this mission; and the measure-theoretic step from pairwise independence to the conditional bound on $\mathbb E[C^{\boldsymbol\alpha}_j\mid\alpha_j]$ .

Selected references

M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single machine scheduling with release dates, SIAM J. Discrete Math. 15(2):165–192, 2002. https://doi.org/10.1137/S089548019936223X
C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998.
L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Math. Oper. Res. 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM–SIAM SODA, 591–598, 1997.
C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31:146–166, 2001. https://doi.org/10.1137/S0097539797327180
M. E. Dyer, L. A. Wolsey, Formulating the single machine sequencing problem with release dates as a mixed integer program, Discrete Appl. Math. 26:255–270, 1990.
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Ann. Discrete Math. 1:343–362, 1977.

13 thms2 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Single Machine Scheduling with Release Dates II: The Random α-Schedule with a Truncated Exponential DensityResearch Paper

Motivation

Minimizing the total weighted completion time $\sum_j w_j C_j$ of jobs with release dates on a single machine, written $1\,|\,r_j\,|\,\sum w_j C_j$ in scheduling notation, is strongly NP-hard. It is one of the basic models of machine scheduling, and it has served as a test case for a general technique in approximation algorithms: solve a linear programming relaxation, read off a preemptive schedule, and convert it into a nonpreemptive one using $\alpha$ -points, the times at which a given fraction of each job has been processed. Phillips, Stein and Wein (doi:10.1007/BF01585872) introduced ordering jobs by points of a preemptive schedule; Goemans (SODA 1997, reference [11] of the paper below) and Chekuri, Motwani, Natarajan and Stein (doi:10.1137/S0097539797327180) showed that choosing $\alpha$ at random improves the guarantee.

Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X) combine two LP relaxations, shown to have equal value, with carefully chosen random $\alpha$ . This mission formalizes their Theorem 3.5: when a single $\alpha$ is drawn from a truncated exponential density, the resulting schedule costs in expectation at most $c < 1.7451$ times the LP lower bound.

Timeline:

1998: Phillips, Stein and Wein give the first constant-factor approximation (ratio $2$ ) for the unit-weight problem $1\,|\,r_j\,|\,\sum C_j$ by converting a preemptive schedule.
1997: Goemans (SODA) introduces randomly chosen $\alpha$ -points for the weighted problem, the conference precursor of the paper formalized here.
2001: Chekuri, Motwani, Natarajan and Stein give a randomized $e/(e-1) \approx 1.58$ -approximation for the unit-weight problem.
2002: Goemans, Queyranne, Schulz, Skutella and Wang give $1.7451$ for a single random $\alpha$ (Theorem 3.5) and $1.6853$ for job-dependent random $\alpha_j$ (Theorem 3.9), both against the same LP bound.
1999: Afrati et al. (doi:10.1109/SFFCS.1999.814574) give a polynomial-time approximation scheme for the problem. It is not LP-based, so the LP-relative factors of Theorems 3.5 and 3.9 remain of interest as bounds on the relaxations' integrality gaps.

Setting

There are $n$ jobs $N = \{1, \dots, n\}$ . Job $j$ has an integral processing time $p_j > 0$ , an integral release date $r_j \ge 0$ and a weight $w_j > 0$ . The jobs are indexed so that $w_1/p_1 \ge w_2/p_2 \ge \cdots \ge w_n/p_n$ .

A preemptive schedule gives each job a set $A_j \subseteq [r_j, \infty)$ of processing times of measure $p_j$ , the sets pairwise disjoint. The mean busy time of $j$ is $M_j = \frac{1}{p_j}\int_{A_j} t\,dt$ .

The LP schedule is the preemptive schedule that always processes the available job of smallest index, which under the indexing above is the available job of largest ratio $w_j/p_j$ . Its mean busy times are $M^{LP}_j$ .

The mean busy time relaxation (R) minimizes $\sum_j w_j (M_j + \tfrac12 p_j)$ subject to $\sum_{j \in S} p_j M_j \ge p(S)\big(r_{\min}(S) + \tfrac12 p(S)\big)$ for every nonempty $S \subseteq N$ , where $p(S) = \sum_{j\in S} p_j$ and $r_{\min}(S) = \min_{j\in S} r_j$ . Its optimal value is $Z_R$ , a lower bound on the optimum of $1\,|\,r_j\,|\,\sum w_j C_j$ .

For $0 < \alpha \le 1$ , the $\alpha$ -point $t_j(\alpha)$ is the first time at which $j$ has received $\alpha p_j$ units of processing in the LP schedule, and $t_j(0^+)$ is its start time. The $\alpha$ -schedule processes the jobs nonpreemptively, each as early as possible, in nondecreasing order of $t_j(\alpha)$ ; $C^\alpha_j$ is the completion time of $j$ in it. More generally, the $(\alpha_j)$ -schedule orders the jobs by $t_j(\alpha_j)$ for a vector $\boldsymbol\alpha = (\alpha_j)$ .

Let $0 < \gamma < 1$ solve $1 - \frac{\gamma^2}{1+\gamma} = \gamma + \ln(1+\gamma)$ ( $\gamma \approx 0.4675$ ), and set

c = \frac{1+\gamma}{1+\gamma-e^{-\gamma}}, \qquad \delta = 1 - \frac{\gamma^2}{1+\gamma}, \qquad f(\alpha) = \begin{cases}(c-1)e^{\alpha} & 0 < \alpha \le \delta,\\ 0 & \text{otherwise.}\end{cases}

Formalization targets

Goal: Theorem 3.5

If $\alpha$ is drawn with density $f$ , then $c < 1.7451$ , the expectation below is finite, and

\mathbb E_f\Big[\sum_{j} w_j C^\alpha_j\Big] \le c \cdot Z_R .

Milestones

Theorem 2.5: $M^{LP}$ is an optimal solution to (R), so $Z_R = \sum_j w_j (M^{LP}_j + \tfrac12 p_j)$ .
Eq. (3.1): $M^{LP}_j = \int_0^1 t_j(\alpha)\,d\alpha$ .
Corollary 3.2: $C^{\boldsymbol\alpha}_j \le t_j(\alpha_j) + \sum_{k:\,\alpha_k\le\eta_k(\alpha_j)} (1+\alpha_k-\eta_k(\alpha_j))\,p_k$ , where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$ in the LP schedule.
Eq. (3.10): $M^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_j$ , where $N_2$ is the set of jobs processed between the start and the completion of $j$ and $\mu_k$ the fraction of $j$ done before $k$ starts.
Eq. (3.11): the bound of Corollary 3.2 rewritten in terms of $N_1$ , $N_2$ and $\mu_k$ .
Lemma 3.6: $f$ is a density on $[0,1]$ with $\int_0^\eta f(\alpha)(1+\alpha-\eta)\,d\alpha \le (c-1)\eta$ and $\int_\mu^1 f(\alpha)(1+\alpha)\,d\alpha \le c(1-\mu)$ for $\eta, \mu \in [0,1]$ .

Significance

Theorem 3.5 is a randomized $1.7451$ -approximation for $1\,|\,r_j\,|\,\sum w_j C_j$ , and simultaneously a bound on the integrality gap of (R): every instance has $\mathrm{OPT} \le 1.7451\, Z_R$ . The paper also derandomizes it: there are at most $n$ distinct $\alpha$ -schedules (its Proposition 3.8), and the best of them can be found in $O(n^2)$ time. The paper remarks that the truncated exponential density is optimal for its analysis and that the factor is tight for it.

On the formal side, the mission produces a reusable model of single-machine preemptive schedules, the LP schedule, $\alpha$ -points and list scheduling, and the first machine-checked instance of the $\alpha$ -point rounding technique that recurs across scheduling approximation. The result itself is proved in the paper; no machine-checked proof of it or of the LP-schedule identities (3.1), (3.10) is known to exist.

Difficulty

The obvious approach, bounding each $C^\alpha_j$ separately by a multiple of $t_j(\alpha)$ , gives only the factor $\max\{1 + 1/\alpha, 1 + 2\alpha\}$ for fixed $\alpha$ (Theorem 3.3 of the paper), which is at least $1+\sqrt2$ . The improvement needs the precise structure of the LP schedule around each job: which jobs interrupt $j$ ( $N_2$ ) and which do not ( $N_1$ ), and how the fraction $\eta_k(\alpha)$ of each other job depends on $\alpha$ . Turning this structure into exact identities for piecewise-constant, piecewise-linear functions of $\alpha$ defined through a recursively built schedule is the bulk of the formal work. The analytic part (Lemma 3.6) is elementary but depends on the specific equation that defines $\gamma$ .

Formalization scope

Jobs are Fin n (0-based) with $p, r : \texttt{Fin } n \to \mathbb N$ and real weights. The sortedness $w_j/p_j \ge w_k/p_k$ for $j \le k$ , positivity $p_j > 0$ and $w_j > 0$ are hypotheses of every theorem about the LP schedule. Because the data are integral, the LP schedule is defined slot by slot on unit intervals $[\tau, \tau+1)$ ; a job's processing set is a finite union of such intervals. $\alpha$ -points are infima over reals, and every statement restricts $\alpha$ to $(0,1]$ . The $(\alpha_j)$ -schedule's completion times are given by the closed form of list scheduling, $C_j = \max_{k \preceq j}(r_k + \sum_{k \preceq i \preceq j} p_i)$ , with ties of $\alpha$ -points broken by index (they do not occur for $\alpha \in (0,1]$ ). $Z_R$ is the infimum of the objective of (R) over its feasible set. The random $\alpha$ has law $f(\alpha)\,d\alpha$ on $\mathbb R$ , and the expectation is a Lebesgue integral.

The goal asserts integrability of $\alpha \mapsto \sum_j w_j C^\alpha_j$ together with the bound, so the inequality cannot hold through the convention that a non-integrable function has integral $0$ . The bound is against $Z_R$ defined from (R), not against $\sum_j w_j (M^{LP}_j + \tfrac12 p_j)$ , which would build Theorem 2.5 into the goal; and the density's support $(0,\delta]$ is written out, so no mass is placed outside $(0,1]$ . The running-time claims are not formalized, and the uniqueness of $\gamma$ is not asserted: the statements hold for every solution in $(0,1)$ .

Useful infrastructure: finite unions of intervals and their measures, monotone piecewise-linear functions and their integrals, and list-scheduling identities. Contributions to any milestone, and general lemmas about the LP schedule (it is a preemptive schedule, has no idle time inside a job's span, processes interrupting jobs completely), are welcome.

Selected references

M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2):165–192, 2002. doi:10.1137/S089548019936223X
C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998. doi:10.1007/BF01585872
M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 591–598, 1997 (no DOI; reference [11] of Goemans et al. 2002).
C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1):146–166, 2001. doi:10.1137/S0097539797327180
F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th IEEE FOCS, 32–43, 1999. doi:10.1109/SFFCS.1999.814574

13 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

Revenue Management Under the Markov Chain Choice Model IV: Dimension Reduction Recovers a Choice-Based Solution with at Most n+1 Nested Offer SetsResearch Paper

Motivation

In network revenue management a firm sells $n$ products that consume $m$ capacitated resources over $T$ periods, and in each period it chooses which offer set of products to make available. When customers choose among the offered products according to a choice model, the standard planning tool is the choice-based linear program, which assigns a frequency $u_S\ge 0$ to every offer set $S\subseteq N$ (Liu and van Ryzin 2008). It has $2^n$ variables. Its optimal solution is what the firm actually implements: a randomization over offer sets.

For the Markov chain choice model of Blanchet, Gallego and Goyal (2016), Feldman and Topaloglu (2017) show that the choice-based program is equivalent to a reduced linear program with only $2n$ variables. The reduced program can be solved directly, but its solution is a pair of vectors $(\hat x,\hat z)$ , not a randomization over offer sets. This mission formalizes the paper's Section 7, which converts the reduced solution back into a randomization over offer sets: the Dimension Reduction algorithm, and Theorem 9, which says that the algorithm produces at most $n+1$ offer sets and that these sets are nested.

Setting

Products are indexed by $N=\{1,\dots,n\}$ . A customer arrives wanting product $j$ with probability $\lambda_j$ . If the product she visits is offered, she buys it. Otherwise she moves to product $i$ with probability $\rho_{j,i}$ , and leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$ . Throughout, $\lambda_j>0$ , $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j,i$ .

For an offer set $S\subseteq N$ , the (Balance) equations

P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S

have a unique solution. $P_{j,S}$ is the probability that product $j$ is purchased, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. Write $P_S=(P_{j,S})_j$ and $R_S=(R_{j,S})_j$ .

The set $\mathcal H$ consists of all pairs $(x,z)\in\mathbb R^n\times\mathbb R^n$ with $x,z\ge0$ and $x_j+z_j=\lambda_j+\sum_{i}\rho_{i,j}z_i$ for all $j$ . The (Reduced) linear program maximizes $\sum_j T r_j x_j$ over $(x,z)\in\mathcal H$ subject to the capacity rows $\sum_j T a_{q,j}x_j\le c_q$ for each resource $q$ .

The Dimension Reduction algorithm starts from the optimal solution $(\hat x,\hat z)$ of (Reduced) and sets $(x^1,z^1)=(\hat x,\hat z)$ . At iteration $k$ it forms $S^k=\{j: x^k_j>0\}$ . It stops with $\alpha^k=1$ if $S^k=\emptyset$ . Otherwise it sets $\alpha^k=\min\{x^k_j/P_{j,S^k}: j\in S^k\}$ , stops if $\alpha^k=1$ , and if not updates

x^{k+1}_j=\frac{x^k_j-\alpha^kP_{j,S^k}}{1-\alpha^k},\qquad z^{k+1}_j=\frac{z^k_j-\alpha^kR_{j,S^k}}{1-\alpha^k}.

The weights are $\gamma^k=(1-\alpha^1)\cdots(1-\alpha^{k-1})\alpha^k$ .

Formalization targets

Goal: Theorem 9

Let $(\hat x,\hat z)$ be optimal for (Reduced). The algorithm stops at some first iteration $K$ with $1\le K\le n+1$ . At that $K$ ,

\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},\qquad \sum_{k=1}^K\gamma^k=1,\qquad S^1\supseteq S^2\supseteq\cdots\supseteq S^K .

Milestones

In the order the proof uses them:

(Balance) has a unique, nonnegative solution for every $S$ (p. 1325).
$P_{j,S}>0$ for $j\in S$ (p. 1325).
For $(\hat x,\hat z)\in\mathcal H$ : $\hat z_j\ge R_{j,S_{\hat x}}$ . This is Lemma 11 of the online appendix, as quoted on p. 1332.
For $(\hat x,\hat z)\in\mathcal H$ with nonempty support: $\alpha_{\hat x}\le1$ (p. 1332).
The two stopping configurations are (Balance) solutions: $S_{\hat x}=\emptyset$ gives $(P_\emptyset,R_\emptyset)$ , and $\alpha_{\hat x}=1$ gives $(P_{S_{\hat x}},R_{S_{\hat x}})$ (p. 1332).
Lemma 8: one step of the algorithm maps $\mathcal H$ into $\mathcal H$ and removes a minimizing index from the support (p. 1333).
The iterates stay in $\mathcal H$ , and $S^{k+1}\subseteq S^k\setminus\{j^k\}$ (pp. 1333–1334).

Significance

Theorem 9 makes the reduced program usable. Together with the equivalence of (Reduced) and the choice-based program, it produces an optimal choice-based solution that offers at most $n+1$ sets. By a basic-solution count the choice-based program has an optimal solution with at most $m+1$ nonzero offer sets. Theorem 9 bounds the number by the number of products instead, and adds a structural property: the offered sets form a chain. Each set is contained in the previous one, so the implemented policy offers a single nested sequence of assortments. The algorithm needs at most $n+1$ solutions of linear systems of size $n$ . It never enumerates offer sets.

The result is proved in the paper. As far as a search of the platform and of Mathlib shows, it has not been formalized. Mathlib's Carathéodory theorem (Analysis/Convex/Caratheodory) bounds the number of points in a convex combination. It does not construct this decomposition, and it does not give nestedness. Formalizing Theorem 9 therefore requires the paper's argument: a verified, terminating peeling procedure on the polyhedron $\mathcal H$ whose output is a convex combination of (Balance) solutions indexed by a chain of sets.

Difficulty

The algorithm divides twice. Step 2 divides by $P_{j,S^k}$ , which must be positive on $S^k$ . Step 3 divides by $1-\alpha^k$ , which must be nonzero whenever the algorithm continues. Both rest on nontrivial facts: the positivity of purchase probabilities, and the bound $\alpha\le1$ on $\mathcal H$ . That bound in turn requires the comparison $\hat z\ge R_{S_{\hat x}}$ . The paper proves this comparison only in its online appendix; it is a monotonicity property of the inverse of $I-\rho^\top$ restricted to the unoffered products. The update of Step 3 can make coordinates of $z$ negative unless this comparison holds, so the naive observation that " $(x^k,z^k)$ is a combination of points of $\mathcal H$ " does not by itself keep the iterates in $\mathcal H$ .

Termination is not a consequence of $\alpha^k<1$ alone. It needs the strict decrease of the support, which comes from choosing a minimizing index. The weights $\gamma^k$ are defined by products of the $(1-\alpha^l)$ . Their sum telescopes to $1$ only because the last step has $\alpha^K=1$ .

Formalization scope

Everything lives in the namespace MarkovChainChoice.DimReduction. Products are Fin n and offer sets are Finset (Fin n). The model is a structure carrying $\lambda_j>0$ , $\sum_i\rho_{j,i}<1$ and, as a disclosed implicit hypothesis, $\rho_{j,i}\ge0$ . The pair $(P_S,R_S)$ is chosen by Classical.epsilon among the solutions of (Balance); milestone 1 is what identifies it with the paper's unique solution. Revenues, capacities and consumptions carry no sign conditions. "Optimal for (Reduced)" means feasible and at least as good as every feasible point.

The iterates are indexed from $k=1$ as in the paper. The value at index $0$ is an unused copy of the input. "The algorithm stops at iteration $K$ " is the first $K\ge1$ with $S^K=\emptyset$ or $\alpha^K=1$ . Iterates after the first stop involve a division by zero, which Lean evaluates to $0$ , and no statement refers to them. The termination bound $K\le n+1$ is a conclusion of the goal, not a hypothesis. The goal is about the algorithm's actual iterates, not about an arbitrary sequence that satisfies the invariants. The paper's $\subset$ and $\supset$ denote non-strict inclusion and are rendered as $\subseteq$ and $\supseteq$ .

Two milestones are stated more generally than the page. The paper states the iteration invariants for the (Reduced) optimum; the Lean requires only $(\hat x,\hat z)\in\mathcal H$ , which every feasible (Reduced) solution satisfies. Lemma 8's $\arg\min$ may be a set; the statement holds for every minimizer. The page contains printed slips: on p. 1332, $\hat v_j$ has numerator $\hat x_j-\alpha R_{j,S}$ , and the paper writes $R_{\hat x}$ for $R_{S_{\hat x}}$ . The Lean uses the correct forms, as in Lemma 8 and Step 3. None of these slips appears in a milestone quotation.

A complete development needs a small theory of M-matrices, in the form of nonnegativity of $(I-Q)^{-1}$ for substochastic $Q$ , together with finite induction on supports. The comparison lemma (milestone 3) and the (Balance) existence and uniqueness result (milestone 1) are reusable across the other missions on this paper. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169

14 thms2 active usersReviewed

Completed

Convex Optimization Graph Theory Operations Research·Captain: mikedeng1

The Traveling-Salesman Problem and Minimum Spanning Trees, Part II: Convergence of the Constant-Step Ascent to the 1-Tree BoundResearch Paper

Motivation

The traveling-salesman problem (TSP) asks for a cheapest cycle through all vertices of a weighted complete graph. Exact algorithms for it are branch-and-bound searches, and their size depends almost entirely on the quality of the lower bounds used to prune the search. In 1970 Held and Karp introduced the 1-tree bound: a Lagrangian relaxation of the degree-2 constraints of a tour, whose value can be evaluated by one minimum-spanning-tree computation (Held & Karp, Part I, 1970). Part II (Held & Karp, 1971) replaces the ascent procedure of Part I by an iterative method related to the relaxation method for linear inequalities of Agmon and of Motzkin and Schoenberg (1954), and with it solved to proven optimality every instance presented to it, up to 64 cities. The iteration is the prototype of what is now called the subgradient method with Polyak-type step sizes, and the 1-tree bound remains a standard lower bound in exact TSP codes.

Timeline:

1954 — Agmon; Motzkin and Schoenberg: the relaxation method for systems of linear inequalities, and convergence of Féjer-monotone sequences relative to full-dimensional sets.
1970 — Held and Karp (Part I): the 1-tree bound $\max_\pi w(\pi)$ and a column-generation / ascent method for it.
1971 — Held and Karp (Part II): the iteration $\pi^{m+1} = \pi^m + t_m v_{k(\pi^m)}$ , its relaxation-method analysis (Lemmas 1–3) and the constant-step guarantee (Theorem 1).
1974 — Held, Wolfe and Crowder validate the method as general subgradient optimization.

Setting

Let $n \ge 3$ and let $(c_{ij})$ be a symmetric real $n\times n$ matrix of weights on the edges of the complete graph $K_n$ with vertex set $\{1,\dots,n\}$ ; weights may be negative and need not satisfy the triangle inequality. A subgraph has weight equal to the sum of its edge weights. A tour is a cycle through every vertex exactly once; $C^*$ is the weight of a minimum tour.

A 1-tree is a tree on the vertex set $\{2,\dots,n\}$ together with two distinct edges at vertex $1$ . Index the 1-trees by $k$ ; let $c_k$ be the weight of the $k$ -th 1-tree, $d_{ik}$ the degree of vertex $i$ in it, and $v_k \in \mathbb R^n$ the degree-excess vector with components $d_{ik}-2$ . For $\pi \in \mathbb R^n$ define

w(\pi) = \min_k\,[c_k + \pi\cdot v_k].

A tour is a 1-tree with $v_k = 0$ , so $C^* \ge w(\pi)$ for every $\pi$ (Eq. (2)); the best bound is $\max_\pi w(\pi)$ . For a point $\pi$ , $k(\pi)$ denotes a minimum-weight 1-tree at $\pi$ , a 1-tree attaining the minimum defining $w(\pi)$ . The ascent iteration (3) is

\pi^{m+1} = \pi^m + t_m\,v_{k(\pi^m)}.

For a target value $\bar w$ , $P_{\bar w}$ is the polyhedron of solutions of $\bar w \le c_k + \pi\cdot v_k$ for all $k$ (system (5)). All norms $\|\cdot\|$ are Euclidean.

Formalization targets

Goal: Theorem 1

With constant step $t_m = \bar t > 0$ , any starting point and any choice of minimum-weight 1-trees,

\sup_m w(\pi^m) \;\ge\; \max_\pi w(\pi) - \tfrac12\,\bar t\,\limsup_{m\to\infty}\|v_{k(\pi^m)}\|^2 .

Milestones

Eq. (2): $C^* \ge w(\pi)$ for every $\pi$ .
Lemma 1: if $w(\bar\pi) \ge w(\pi)$ then $(\bar\pi-\pi)\cdot v_{k(\pi)} \ge w(\bar\pi) - w(\pi) \ge 0$ .
Lemma 2: if $0 < t < 2(w(\bar\pi)-w(\pi))/\|v_{k(\pi)}\|^2$ then $\|\bar\pi - (\pi + t v_{k(\pi)})\| < \|\bar\pi-\pi\|$ .
Féjer-monotone convergence (Motzkin–Schoenberg, quoted in the proof of Lemma 3): a sequence whose distance to every point of a set with nonempty interior is nonincreasing converges.
Lemma 3, Case 1: for $\bar w < \max_\pi w$ and the relaxation iteration

\pi^{m+1} = \pi^m + \lambda_m\,\frac{\bar w - w(\pi^m)}{\|v_{k(\pi^m)}\|^2}\,v_{k(\pi^m)} \qquad (6)

with $0<\varepsilon<\lambda_m\le 2$ , the iterates enter $P_{\bar w}$ or converge to a boundary point of $P_{\bar w}$ . 6. Lemma 3, Case 2: with $\lambda_m = 2$ the iterates enter $P_{\bar w}$ . 7. §3 bound: the restricted minimum $w_{X,Y}(\pi)$ over 1-trees containing the edges $X$ and avoiding the edges $Y$ is a lower bound on every tour of the derived problem.

Milestones 1–5 are the steps of the paper's proof of Theorem 1; 6 and 7 are further results of the paper on the same objects.

Significance

Theorem 1 is the paper's justification of the step rule actually used in its computations: a fixed step $\bar t$ loses at most $\tfrac12\bar t$ times the asymptotic squared deviation of the generated 1-trees from being tours. Since $\|v_k\|^2$ is an even integer that vanishes exactly on tours, and the paper observes it is typically small in practice, the bound explains why the constant-step ascent reaches bounds sharp enough for branch-and-bound. Lemmas 1–3 are the first analysis of a subgradient-type method for a nonsmooth concave function, cast as the relaxation method for the (exponentially large) system (5).

All results are proved in the paper (except the Féjer-monotone convergence and Case 2 of Lemma 3, which it cites from Motzkin and Schoenberg). None is formalized: the platform has the 1-tree lower bound only under a metric assumption on the weights (SupplyChainTheory.held_karp_bound, SupplyChainTheory.one_tree_lower_bound), and the subtour-LP bound MetricTSP.held_karp_le_opt, a different object. This mission produces the bound for arbitrary real weights, the supergradient property of $v_{k(\pi)}$ , and a machine-checked convergence analysis of the relaxation iteration.

Difficulty

Lemmas 1 and 2 and Eq. (2) are short once the finite minimum defining $w$ is handled. The difficulty is in Lemma 3 and Theorem 1. The iteration is not monotone in $w$ , so no descent argument applies; progress is measured by the Euclidean distance to the target polyhedron $P_{\bar w}$ , and turning distance decrease into convergence requires the Féjer-monotonicity theorem, which in turn needs $P_{\bar w}$ to have nonempty interior (from $\bar w < \max_\pi w$ ). In Theorem 1 the step is constant rather than of the relaxation form (6), and the target polyhedron is not given in advance: the relevant relaxation parameters are admissible only eventually and must be kept away from zero, which requires controlling degenerate directions $v_{k(\pi^m)} = 0$ and the behaviour of $w$ along an iteration that is not known a priori to stay bounded. A direct argument that $w(\pi^m)$ increases fails, since single steps can decrease $w$ .

Formalization scope

Vertices are Fin n, the paper's vertex 1 is 0 : Fin n, and graphs are SimpleGraph (Fin n). Weights are c : Sym2 (Fin n) → ℝ, arbitrary reals. A 1-tree is a graph whose restriction to the vertices other than 0 is a tree and in which 0 has degree 2; a tour is a connected graph with all degrees 2. w(π) is the minimum of weight c G + ∑ i, π i * (deg G i − 2) over 1-trees, written as an sInf over a finite set that is nonempty for n ≥ 3; every theorem assumes 3 ≤ n. Euclidean norms and inner products are written as coordinate sums of squares and products, never Mathlib's sup norm on Fin n → ℝ. The minimum-weight 1-tree $k(\pi^m)$ is a hypothesis at every step, and ties may be broken arbitrarily. The goal is stated as "for every $\pi^*$ and $\delta>0$ some iterate has $w(\pi^m) > w(\pi^*) - \tfrac12\bar t L - \delta$ ", which is equivalent to the printed inequality; $L$ is the limsup of a sequence with finitely many values, a genuine real.

The statements exclude trivializing readings: the 1-tree predicate rejects graphs without exactly two edges at vertex 1; w is never a minimum over an empty set under the standing hypothesis 3 ≤ n; no ⨆ of a possibly unbounded family is used; the step size $\bar t$ and the parameter $\varepsilon$ are strictly positive.

A complete development needs finite minima of affine functions (concavity, attainment), 1-tree and tour combinatorics on simple graphs, and Féjer-monotone sequences in $\mathbb R^n$ ; the last two are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3, are welcome.

Selected references

M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18 (1970) 1138–1162. https://doi.org/10.1287/opre.18.6.1138
T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 382–392. https://doi.org/10.4153/CJM-1954-037-2
M. Held, P. Wolfe and H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223

10 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research·Captain: Shuze Chen

Discrete Convex Analysis XXXV: Gross Substitutes and Equilibrium PricesTextbook

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

41 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Strategic Inventory and Supplier Encroachment: For Any Positive Holding Cost the Buyer Withholds Strategic Inventory When the Direct Selling Cost Is Just Below 5/6, at Total Holding Cost Below 11/72Research Paper

Motivation

Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below $\alpha/4$ . The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.

Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the $\alpha/4$ cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.

Setting

There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is $p = \alpha - q$ , where $q$ is the total quantity sold in that period and $\alpha > 0$ is the demand intercept. The buyer pays a per-unit holding cost $h \ge 0$ on inventory carried into period 2. The supplier pays a per-unit direct selling cost $s \ge 0$ . All other costs and the salvage value are zero. The moves are:

The supplier quotes a wholesale price $w_1 \ge 0$ .
The buyer orders $Q_1$ and sells $q_1$ , with $0 \le q_1 \le Q_1$ . It carries the inventory $I = Q_1 - q_1$ into period 2.
The supplier quotes $w_2 \ge 0$ .
The buyer orders $Q_2 \ge 0$ and sells $q_2$ , with $0 \le q_2 \le I + Q_2$ .
Having observed everything, the supplier sells $q_s \ge 0$ directly. The period-2 price is $\alpha - q_2 - q_s$ .

The total profits are

\Pi_b = (\alpha - q_1)q_1 - w_1 Q_1 - hI + (\alpha - q_2 - q_s)q_2 - w_2 Q_2, \qquad \Pi_s = w_1 Q_1 + w_2 Q_2 + (\alpha - q_2 - q_s - s)q_s .

A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is $I$ on that path. Following the paper (§4), the goal theorem sets $\alpha = 1$ .

Formalization targets

Goal: Proposition 4.2

With $\alpha = 1$ ,

\forall h > 0\ \ \exists \epsilon > 0\ \ \forall s \in \big(\tfrac56 - \epsilon, \tfrac56\big):\quad \text{an SPE exists, and every SPE has } I > 0 \text{ and } hI < \tfrac{11}{72}.

Here $\epsilon$ may depend on $h$ , and the bound $11/72$ applies at the same $(h, s)$ .

Milestones, in attack order

Stage-3 best response (§3.1.1): in every SPE, the supplier sells $q_s = (\alpha - q_2 - s)^+/2$ at every history.
Eq. (1) (§3.1.1): with no inventory, the buyer's period-2 quantity is the four-branch function $q_b(w)$ of the period-2 wholesale price $w$ .
Proposition 4.1, existence half: an SPE exists for every $h \ge 0$ and $s \ge 0$ .
Region 8 (Tables A.1 and A.4): for $h < h_{11}$ with $s_3 \le s < 5\alpha/6$ , or for $h < \alpha/4$ with $5\alpha/6 \le s < \alpha$ , every SPE has $I = 5(\alpha - 4h)/34$ and the path of Table A.4.
Region 7, second part (Tables A.1 and A.3): for $h_{11} < h < h_{10}$ and $s_3 \le s < 5\alpha/6$ , every SPE has $I = I^* = (2\alpha - 3s + x)/2$ and the path of Table A.3.
Region 10, second part (Tables A.1 and A.4): for $h > h_7$ and $2\alpha/3 < s < 5\alpha/6$ , every SPE has $I = 0$ .

The thresholds $x$ , $s_3$ , $h_7$ , $h_{10}$ , $h_{11}$ are explicit algebraic functions of $s$ , given in Appendix A.

Significance

Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once $h \ge \alpha/4$ . With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as $h$ grows. Milestone 6 shows the flip side: for a fixed $s < 5\alpha/6$ , a large enough $h$ removes the inventory. This is why the window $\epsilon$ must depend on $h$ .

The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near $s = 5\alpha/6$ . It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.

Difficulty

The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response $(\cdot)^+$ switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of $I$ has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of $h_7$ , $h_{10}$ and $h_{11}$ as $s \uparrow 5/6$ , where the denominator $3s - 2 - x$ of $h_7$ tends to $0$ .

Formalization scope

Representation. Strategies are functions of the full history, not Markov rules in $I$ . IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with $q_1 \le Q_1$ and $q_2 \le I + Q_2$ .
Normalization. The goal instantiates $\alpha = 1$ as the paper does from §4 on. The milestones keep a general $\alpha > 0$ .
Uniqueness is not stated. Proposition 4.1's uniqueness claim is false for strategy profiles: after the off-path price $w_2 = 0$ , every order $Q_2 \ge q_2 - I$ is optimal. The goal and the region milestones therefore quantify over every SPE and carry existence as a separate conjunct.
Corrected hypotheses.
- The printed $s_3 = (\sqrt{(37 - 3\sqrt{65})/34} + 4/6)\alpha \approx 1.28\alpha$ is replaced by $(\sqrt{37 - 3\sqrt{65}}/34 + 4/6)\alpha \approx 0.772\alpha$ , which matches the paper's "≈0.77".
- Eq. (1) excludes the corner $w = 0$ , $s < \alpha/3$ , where its second branch is wrong.
- Region 8 drops its boundary $h = h_{11}$ and Region 7 drops $h = h_{10}$ , because the equilibrium path switches there and need not be unique.
Ruled-out trivialization. The inventory in the goal is the inventory on the path of an SPE of the game above. It is not the closed form $5(1 - 4h)/34$ or $I^*$ from the tables, and the regional characterization is not a hypothesis. Otherwise the goal would reduce to algebra about the thresholds.
Infrastructure and contributions. The definitions Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
- lemmas on maximizing concave piecewise-quadratic functions on half-lines;
- a reusable backward-induction lemma for finite-stage games with real action sets;
- interval-arithmetic facts about $x$ , $h_7$ , $h_{10}$ and $h_{11}$ near $s = 5/6$ ;
- proofs of the paper's other regions.

Selected references

T. Guan, H. Gurnani, X. Geng, Y. Luo, Strategic Inventory and Supplier Encroachment, Manufacturing & Service Operations Management 21(3):536–555, 2019. https://doi.org/10.1287/msom.2018.0705
K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10):1792–1804, 2008. https://doi.org/10.1287/mnsc.1080.0894
A. Arya, B. Mittendorf, D. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5):651–659, 2007. https://doi.org/10.1287/mksc.1070.0280

10 thms2 active usersReviewed

Missions

Global Convergence of Splitting Methods for Nonconvex Composite Optimization III: For Semi-Algebraic Problems the ADMM Sequence Converges and Has Finite LengthResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 13)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Global Convergence of Splitting Methods for Nonconvex Composite Optimization II: The Proximal ADMM Sequence Is Bounded Under CoercivityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Two- and Three-Stage Production Schedules with Setup Times Included 2: Johnson's Rule for Three MachinesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 67)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robustness and Generalization IV: Robustness of the Lasso on a Compact Sample SpaceResearch Paper

Motivation

Setting

Formalization targets

Goal: Example 6 (p. 404)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Value of Information in Bayesian Routing Games II: Equilibrium Adoption Rates of Information Systems Are the Minimizers of the Equilibrium PotentialResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program II: Stability of the Deterministic Equivalent Convex ProgramResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.11 (p. 337)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program I: The Induced Feasibility Region Is a Closed Convex Polyhedron When T Is FixedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.10

Milestones

Significance

Difficulty

Formalization scope

Selected references

A New Projection Method for Variational Inequality Problems: The Hyperplane Projection Method Converges to a Solution Under Continuity and Generalized MonotonicityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1

Milestones (in attack order)

Significance

Difficulty