Operations Research

Combinatorics Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Santa Claus Schedules Jobs on Unrelated Machines: The Configuration LP Has Integrality Gap at Most 33/17Research Paper

Motivation

Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below $3/2$ unless P = NP; closing the gap between $3/2$ and $2$ has been open since.

The restricted assignment problem is the special case in which every job $j$ has a single size $p_j$ and may only run on a given set $\Gamma(j)$ of machines. The $3/2$ hardness already holds here, and the best known algorithms were still $2$ -approximations. Every linear program previously used for the problem has integrality gap $2$ , so a better LP lower bound was the natural target.

Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most $33/17 \approx 1.9412$ . Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than $2$ .

1990: Lenstra, Shmoys, Tardos, 2-approximation for unrelated machines, and $3/2$ hardness already for restricted assignment.
2006: Bansal and Sviridenko introduce the configuration LP for the max–min variant (the Santa Claus problem).
2008: Feige shows the configuration LP has constant integrality gap for restricted Santa Claus, and Asadpour, Feige and Saberi (2008) give a local search proof of a factor-4 gap.
2011: Svensson adapts that local search to makespan and proves the gap $33/17$ for restricted assignment (arXiv:1011.1168).

Setting

An instance consists of finite sets $J$ (jobs) and $M$ (machines), sizes $p_j \ge 0$ , and for each job a set $\Gamma(j) \subseteq M$ . A schedule is a map $\sigma : J \to M$ with $\sigma(j) \in \Gamma(j)$ . The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ , and the makespan is the largest load. $\mathrm{OPT}$ is the least makespan of a schedule.

For a target makespan $T$ , a configuration for machine $i$ is a set $C \subseteq J$ of jobs that may all run on $i$ ( $i \in \Gamma(j)$ for $j \in C$ ) with $p(C) = \sum_{j \in C} p_j \le T$ . Write $\mathcal C(i,T)$ for the set of configurations. The configuration LP asks for $x_{i,C} \ge 0$ with

\text{[C-LP]}\qquad \sum_{C \in \mathcal C(i,T)} x_{i,C} \le 1 \quad (i \in M), \qquad \sum_{i \in M}\ \sum_{C \in \mathcal C(i,T),\ C \ni j} x_{i,C} \ge 1 \quad (j \in J).

Its dual has variables $y_i, z_j \ge 0$ and constraints $y_i \ge \sum_{j \in C} z_j$ for all $i$ and $C \in \mathcal C(i,T)$ . $\mathrm{OPT}_{LP}$ is the least $T$ at which [C-LP] is feasible, and $\mathrm{OPT}_{LP} \le \mathrm{OPT}$ .

In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.

Formalization targets

Goal: Theorem 4.1

For every instance with $p \ge 0$ and every $T \ge 0$ ,

\text{[C-LP] feasible at } T \ \Longrightarrow\ \exists\, \sigma : J \to M,\ \ \sigma(j) \in \Gamma(j)\ \forall j,\quad \sum_{j : \sigma(j) = i} p_j \le \tfrac{33}{17}\, T \ \ \forall i .

Equivalently $\mathrm{OPT} \le \tfrac{33}{17}\,\mathrm{OPT}_{LP}$ . The statement is scale-free and does not define $\mathrm{OPT}_{LP}$ .

Milestones

The milestones follow the paper's proof, which normalizes $\mathrm{OPT}_{LP} = 1$ and sets $R = 16/17$ :

a dual solution with $\sum_i y_i < \sum_j z_j$ makes [C-LP] infeasible;
the local search, Algorithm 2 (ExtendSchedule), keeps its partial schedule valid (load at most $1 + R$ , at most one big job per machine);
when the algorithm has no potential move, an explicit pair $(y^*, z^*)$ is dual feasible (Claim 4.7) and has $\sum y^* < \sum z^*$ (Claim 4.8);
hence, if [C-LP] is feasible, a potential move always exists (Lemma 4.6);
the algorithm has no infinite run (Lemma 4.9);
[C-LP] feasible at $T = 1$ gives a schedule of makespan at most $1 + 16/17$ .

Three facts from Section 2 complete the list: normalization by scaling, $\mathrm{OPT}_{LP} \le \mathrm{OPT}$ , and monotonicity of feasibility in $T$ .

Significance

The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor- $2$ algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within $33/17 + \epsilon$ . The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to $11/6$ (Jansen and Rohwedder, 2017) along the same lines.

The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:

a reusable definition of the configuration LP and its dual certificate;
a precise, nondeterministic model of a local search whose termination rests on a lexicographic potential;
a check of a proof that has many cases. The formalization already exposed two edge cases:
- Claim 4.8 fails when $j_{\mathrm{new}}$ has size $0$ and no admissible machine;
- the termination proof needs positive job sizes. With a job of size $0$ , the algorithm can move it back and forth between two tied machines forever.

The milestones are stated with the corresponding hypotheses.

Difficulty

The obvious approach, rounding a fractional configuration solution, loses a factor $2$ . If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.

The milestones along the paper's route are hard for two reasons. First, the dual pair $(y^*, z^*)$ rounds job sizes down by class (big to $11/17$ , medium to $9/17$ ). Proving $\sum y^* < \sum z^*$ requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.

Formalization scope

Jobs and machines are finite types with decidable equality, sizes are real numbers with $p_j \ge 0$ , and admissible machines are a Finset per job. Schedules are total maps $J \to M$ with $\sigma(j) \in \Gamma(j)$ stated explicitly. Partial schedules are maps $J \to$ Option M. Constants are exact rationals in $\mathbb R$ . Values of moves live in Lex (ℝ × ℝ).

Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.

Three statements would trivialize the goal, and the formalization rules them out:

a schedule allowed to use machines outside $\Gamma(j)$ ;
a target $T < 0$ ;
an LP missing either constraint row.

Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.

Useful contributions include:

the weak-duality certificate;
the scaling and monotonicity facts;
the invariants of reachable states (each job lies in at most one blocker, blockers on a machine are never reassigned while present);
the two claims and the termination argument.

The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.

Selected references

O. Svensson, Santa Claus Schedules Jobs on Unrelated Machines, arXiv:1011.1168v2, 2011; SIAM J. Comput. 41(5), 2012. https://arxiv.org/abs/1011.1168
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Math. Programming 46, 1990. https://doi.org/10.1007/BF01585745
N. Bansal, M. Sviridenko, The Santa Claus problem, STOC 2006. https://doi.org/10.1145/1132516.1132522
A. Asadpour, U. Feige, A. Saberi, Santa Claus meets hypergraph matchings, APPROX 2008; ACM Trans. Algorithms 8(3), 2012. https://doi.org/10.1145/2229163.2229168
K. Jansen, L. Rohwedder, On the configuration-LP of the restricted assignment problem, SODA 2017. https://arxiv.org/abs/1611.01934

13 thms2 active usersReviewed

Completed

Discrete Geometry Linear Optimization Optimization·Captain: mikedeng1

Maximal Lattice-Free Convex Sets in Linear Subspaces II: Minimal Valid Inequalities Come from Maximal Lattice-Free Convex SetsResearch Paper

Cutting planes from lattice-free convex sets

Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping $q$ rows for basic integer variables $x_1,\dots,x_q$ , dropping the nonnegativity of $x$ (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of $s\ge0$ with $f+\sum_j r^js_j\in\mathbb Z^q$ . Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.

Setting

Fix $q\ge0$ , a point $f\in\mathbb R^q$ and a linear subspace $W\subseteq\mathbb R^q$ , and assume that the affine space $f+W$ contains an integral point. Products such as $ry$ are standard inner products.

$\mathcal W$ is the space of real functions $s=(s_r)_{r\in W}$ with finite support. The semi-infinite relaxation is

R_f(W)=\Big\{s\in\mathcal W \ \Big|\ f+\sum_{r\in W}rs_r\in\mathbb Z^q,\ s_r\ge0\ (r\in W)\Big\}.

A linear inequality is a pair $(\psi,\alpha)$ with $\psi:W\to\mathbb R$ an arbitrary function and $\alpha\in\mathbb R$ , read as $\Psi(s)=\sum_{r\in W}\psi(r)s_r\ge\alpha$ . It is valid if every $s\in R_f(W)$ satisfies it.
$V$ is the affine hull of $(f+W)\cap\mathbb Z^q$ , and $\mathcal V=\{s\in\mathcal W\mid f+\sum_r rs_r\in V\}$ . A linear inequality is trivial if every $s\in\mathcal V$ with $s\ge0$ satisfies it. When $W$ is irrational (not spanned by the integral points it contains, up to translation), $V$ is a proper affine subspace of $f+W$ .
$\sum\psi(r)s_r\ge\alpha$ dominates $\sum\psi'(r)s_r\ge\alpha$ if $\psi\le\psi'$ pointwise. A valid inequality is minimal if no valid inequality with the same $\alpha$ and a different $\psi'\le\psi$ exists.
Choose $C\in\mathbb R^{\ell\times q}$ and $d\in\mathbb R^\ell$ with $V=\{x\in f+W\mid Cx=d\}$ . Two valid inequalities are equivalent if $\psi(r)=\rho\psi'(r)+\lambda^TCr$ for all $r\in W$ and $\alpha=\rho\alpha'+\lambda^T(d-Cf)$ , for some $\rho>0$ , $\lambda\in\mathbb R^\ell$ .
A maximal lattice-free convex set in $f+W$ is a convex $B\subseteq f+W$ with no integral point in its interior relative to $f+W$ , inclusionwise maximal with these properties.
For $K\subseteq W$ closed, convex, with $0$ in its interior relative to $W$ : the polar $K^*=\{y\in W\mid ry\le1\ \forall r\in K\}$ , $\hat K=\{y\in K^*\mid\exists x\in K,\ xy=1\}$ , and $\rho_K(r)=\sup_{y\in\hat K}ry$ . For such a $B$ with $f$ in its interior, $\psi_B=\rho_{B-f}$ ; for a polyhedral $B=\{x\in f+W\mid a_i(x-f)\le1\}$ with tight rows this is $\psi_B(r)=\max_ia_ir$ .

A function $\sigma:W\to\mathbb R$ is sublinear if $\sigma(\lambda r)=\lambda\sigma(r)$ for $\lambda\ge0$ and $\sigma(r+r')\le\sigma(r)+\sigma(r')$ .

Formalization targets

Goal: Theorem 3 (p. 6)

Every nontrivial valid linear inequality for $R_f(W)$ is dominated by a nontrivial minimal valid linear inequality for $R_f(W)$ .
Every nontrivial minimal valid linear inequality for $R_f(W)$ is equivalent to one of the form

\sum_{r\in W}\psi_B(r)s_r\ \ge\ 1

with $\psi_B\ge0$ on $W$ and $B$ a maximal lattice-free convex set in $f+W$ with $f$ in its interior.

The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on $f$ or $W$ .

Milestones

In the order in which the proof on pp. 15–21 uses them:

Lemma 23 (a sublinear valid inequality below any valid one)
Lemma 26 (invariance under equivalence)
Claims 1 and 2 in the proof of Theorem 3
Theorem 28 (Basu–Cornuéjols–Zambelli: $\rho_K$ is the smallest sublinear function with $1$ -sublevel set $K$ )
Remark 30 and Claim 4 (the inequality $\sum\rho_K(r)s_r\ge1$ )
Remark 29 ( $\rho_K=\max_ia_ir$ for tight rows)
Claim 6 (a shift by $\lambda^TC$ making $\psi$ nonnegative)
Claim 7 ( $\psi_B$ below a nonnegative sublinear $\psi''$ )
Lemma 31 (maximal lattice-free sets give minimal inequalities)

Significance

Theorem 3 says that the minimal valid inequalities of $R_f(W)$ are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull $\mathcal V$ . It also says that for irrational $W$ , where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of $\operatorname{conv}(R_f(W))$ in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.

The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.

Difficulty

For rational data every valid inequality can be written with right-hand side $1$ and nonnegative coefficients, and $\psi$ is then the gauge of $B_\psi$ . For irrational $W$ this fails. Since $R_f(W)\subseteq\mathcal V$ , adding $\lambda^TCr$ to $\psi$ changes nothing on $R_f(W)$ , so coefficients can be negative, and $B_\psi=\{x\in f+W\mid\psi(x-f)\le\alpha\}$ may have a full-dimensional recession cone. A maximal lattice-free set containing $B_\psi$ then yields a $\psi_B$ that need not lie below $\psi$ (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within $V$ . This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that $\psi$ is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.

Formalization scope

Ambient space. $\mathbb R^q$ is EuclideanSpace ℝ (Fin q), $W$ is a Submodule, and $\mathcal W$ is W →₀ ℝ. The printed phrase "the set $\{r\mid s_r>0\}$ has finite cardinality" is read as ordinary finite support.
Standing hypothesis. Every statement assumes that $f+W$ contains an integral point. Without it $R_f(W)=\emptyset$ and every inequality is valid, so this hypothesis rules out the trivializing formalization. The equivalence predicate carries the hypothesis $V=\{x\in f+W\mid Cx=d\}$ together with validity of both inequalities. With $C,d$ unconstrained, equivalence would be rescaling only, and part 2 of the goal would be false for irrational $W$ .
Interiors. All interiors are relative: to $f+W$ for $B$ and $B_\psi$ , to $W$ for $K$ .
$\psi_B$ . It is defined as $\rho_{B-f}$ , independent of any description of $B$ .

The paper is imprecise in three places, and the formalization departs from the page in each:

Remark 29 is false without tight rows: for $K=(-\infty,1]\subseteq\mathbb R$ written with $a_1=1$ , $a_2=1/2$ , $\rho_K(r)=r\ne\max(r,r/2)$ for $r<0$ . It is stated with the tightness the paper arranges before using it.
The identity $\operatorname{int}(B_\psi)=\{x\mid\psi(x-f)<\alpha\}$ on p. 17 fails at $\alpha=0$ , for example for $\psi\equiv0$ . Claims 1 and 2 use the strict sublevel set, and Claim 2 is false for the topological interior.
Claims 5 and 7 invoke Corollary 20 in $f+W$ , although it is proved only for a lattice of a linear space. Corollary 20 and Claim 5 are therefore not milestones.

Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.

Selected references

A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543v1
A. Basu, G. Cornuéjols, G. Zambelli, Convex sets and minimal sublinear functions, J. Convex Anal. 18(2), 2011 (reference [9]).
V. Borozan, G. Cornuéjols, Minimal valid inequalities for integer constraints, Math. Oper. Res. 34(3), 2009. https://doi.org/10.1287/moor.1090.0400
K. Andersen, Q. Louveaux, R. Weismantel, L. Wolsey, Inequalities from two rows of a simplex tableau, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_1
E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2, 1969. https://doi.org/10.1016/0024-3795(69)90017-2

16 thms2 active usersReviewed

Discrete Geometry Linear Optimization Number Theory+1·Captain: mikedeng1

Maximal Lattice-Free Convex Sets in Linear Subspaces I: Characterization of Maximal Lattice-Free Convex Sets in a SubspaceResearch Paper

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$ . The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$ ) needs.

Timeline.

Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$ ).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$ . For $X\subseteq\mathbb R^n$ , $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$ -subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$ , the line $x_2=2x_1$ is a $\Lambda$ -subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$ .

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$ -free convex set of $W$ if $S\subseteq W$ , $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$ . It is maximal if no other $\Lambda$ -free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ( $W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$ . The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$ .

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$ , a set $S$ is a maximal $\Lambda$ -free convex set of $W$ if and only if

\text{(i) } S \text{ is a full-dimensional polyhedron in } W,\ S\cap V \text{ is maximal } \Lambda\text{-free in } V,\ F\mapsto F\cap V \text{ is a bijection of facets};

\text{(ii) } S=v+L \text{ is a hyperplane of } W \text{ with } L\cap V \text{ a hyperplane of } V \text{ that is not a } \Lambda\text{-subspace};

\text{(iii) } S \text{ is a half-space of } W \text{ containing } V \text{ on its boundary.}

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$ , $S$ is a maximal $\Lambda$ -free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$ -subspace and $\dim S=\dim P+\dim L=\dim V$ , with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$ -subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ( $S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$ -free), Lemma 17 (projection along a $\Lambda$ -subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$ .

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$ ) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$ -subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$ .

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$ , the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$ -subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$ , and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$ , and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$ . For $W=V=\{0\}$ the only maximal set is $\emptyset$ , which satisfies none of the listed cases, so the printed statements are false there.
Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$ ) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$ , discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054

18 thms2 active usersReviewed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks VII: Global Stability, Rings, and the Rybko–Stolyar BoundaryTextbook

Motivation

Mission VI showed that two structural families of queueing networks — feedforward routing, and any network under HLSPS control — are stable throughout their entire subcritical region: no extra condition beyond the standard load condition is ever needed. Until the early 1990s it was widely conjectured that this held for every queueing network. Rybko and Stolyar's 1992 example disproved it: a specific, entirely reasonable two-station network, still subcritical, whose buffer contents grow without bound under a particular non-idling policy. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the third part of Chapter 8 to mapping the boundary this discovery opened up: which network structures still enjoy subcriticality-implies-stability (unidirectional rings), and, for a network that does not, exactly what extra condition restores it (the two-station, five-class re-entrant line, the book's own worked instance of the Rybko–Stolyar phenomenon).

Setting

A queueing network is globally stable (Definition 8.22) if it is Markov-chain stable under every simply structured, non-idling control policy — the strongest policy-independent notion of stability a network can have. At the fluid-model level (Definition 8.23, restricting to single-server stations, $b \equiv 1$ ), this becomes: every solution of the fluid equations (8.20)-(8.23) plus the non-idling condition (8.42) is driven to the origin, uniformly in its starting size. A unidirectional ring network routes each customer type through a fixed cyclic sequence of stations; a two-station, five-class re-entrant line (Figure 8.3) routes its single input stream through five classes in a fixed order, alternating between two stations.

Formalization targets

Goal: Theorem 8.25 — the Rybko–Stolyar-style boundary for a re-entrant line

The two-station, five-class re-entrant network's fluid model is globally stable if and only if

\lambda_1(m_1+m_3+m_5) < 1, \qquad \lambda_1(m_2+m_4) < 1, \qquad \lambda_1(m_2+m_5) < 1.

The first two conditions together are the standard load condition; the third is a genuinely new "virtual station condition," the direct analogue of the Rybko–Stolyar network's own extra requirement. This is the weakest possible target for the phenomenon it captures: a two-sided iff, so it cannot be strengthened by dropping either the necessity or the sufficiency direction, and it isolates the exact extra condition rather than a merely sufficient one.

Supporting milestones

Lemma 8.20 (restated from mission VI, since this chunk's page range overlaps mission VI's at page 164) is a general departure-rate extinction criterion. Theorem 8.21 proves stability of an "assembly with complementary side business" network via a first two-dimensional piecewise-linear Lyapunov function. Theorem 8.24 shows unidirectional ring networks are globally stable throughout their entire subcritical region — no extra condition needed, in sharp contrast to the goal theorem's network. Lemma 8.26 gives four algebraic sufficient conditions for the workload derivative inequalities the goal theorem's Lyapunov argument needs; Lemma 8.27 shows these conditions are simultaneously satisfiable exactly when (8.47)-(8.49) hold — the geometric core of the sufficiency direction.

Significance

The result itself. Theorem 8.25 is the book's own fully worked instance of the field's most cited stability-boundary phenomenon: it pins down, for a specific and analyzable network, exactly how much more than subcriticality is required, and shows the extra requirement (8.49) is not an artifact of the proof technique but a genuine necessary condition, via an explicit unstable sample path under the "extreme" priority policy that violates it. Theorem 8.24, by contrast, demonstrates that the ring topology is not automatically pathological in this way, delineating the boundary from the other side.

Formalizing it. Searches for "re-entrant line," "Rybko-Stolyar," and "virtual station" (q=re-entrant%20line, q=Rybko-Stolyar, q=virtual%20station) return no results specific to this material; this mission is a from-scratch formalization of global stability at both the Markov-chain and fluid-model tiers, unidirectional ring networks, the two-station five-class re-entrant line, and the assembly-with-side-business network.

Difficulty

Theorem 8.25's necessity direction needs an entirely different proof technique from its sufficiency direction: rather than a Lyapunov argument, it requires exhibiting an explicit unstable fluid model solution under a specific "extreme" static-buffer-priority policy — a sample-path construction, echoing the divergent-cycle construction mission III's own chapter (Section 6.2) gives for the original Rybko–Stolyar network, that the book itself says is "omitted" as analogous. A formalization that stated only the sufficiency direction (dropping the "only if") would misrepresent the theorem entirely, since sufficiency alone is not what makes this result the field's canonical boundary-of-stability statement. A second difficulty is genuinely geometric: Lemma 8.27's proof intersects a parallelogram of admissible $(x_2,x_4)$ pairs with a wedge region, then separately solves an analogous system for $(x_1,x_3,x_5)$ — reducing a five-dimensional existence claim to two two-dimensional geometric arguments, each depending on (8.47)-(8.49) in a way that is not visible from the inequalities' surface form alone.

Formalization scope

Missions IV/VI's queueing-network model data, fluid-equation specialization, and workload operator are restated locally (drafts in this series do not import one another), as is mission VI's non-idling fluid model (renamed to track Definition 8.23's own name, FluidModelGloballyStable, even though defeq in shape). Definition 8.22 (network-level global stability) is stated abstractly over an uninterpreted policy type and two predicates, since the concrete "simply structured non-idling policy" and "positive recurrence under a policy" notions belong to mission I's apparatus, not a dependency of this chunk. The unidirectional ring network is characterized as a structural property of an ordinary flat-indexed queueing network (a partial successor function encoding the deterministic route) rather than by re-introducing the book's own two-index type/stage bookkeeping — a faithful re-encoding, since every ring network in the book's sense is representable this way. The re-entrant line's routing (station 1 serves classes 1,3,5; station 2 serves classes 2,4) was recovered from the explicit computations in Lemma 8.26's own proof, not read off Figure 8.3 directly, though the two are cross-checked as consistent. The assembly-with-side-business network, which needs a genuinely multi-input activity outside Chapter 2's "unitary network" vocabulary, is packaged directly via its already-derived fluid equations (8.36)-(8.39) rather than a general SPN activity structure. Theorem 8.25 is stated as a bare ↔, exposing neither the sufficiency direction's Lyapunov witnesses nor the necessity direction's instability construction — a formalization that dropped either direction of the iff, or that conflated the unidirectional ring's cyclic structure with an unrestricted deterministic routing graph, would each be an unfaithful weakening. IsGloballyStable, FluidModelGloballyStable, IsUnidirectionalRing, and the re-entrant line's Lyapunov ingredients (reentrantG1/reentrantG2/ reentrantH1/reentrantH2) are the primary reusable contributions; contributions completing the six by sorry proofs — Theorem 8.25's necessity direction in particular, which needs machinery this mission does not otherwise build — are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
J. G. Dai and J. H. Vande Vate, "The stability of two-station multitype fluid networks," Operations Research 48 (2000), 721–744.

13 thms2 active usersReviewed

Completed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks VI: Feedforward and Generalized Jackson Network StabilityTextbook

Motivation

Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.

Setting

A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator $W(z) := AM(I-P')^{-1}z$ (Eq. 8.24) gives, for any buffer-contents vector $z$ , the total service effort each pool would need to drain $z$ to emptiness with no further arrivals; the load vector of the standard load condition is $\rho = W(\lambda)$ (Eq. 8.25), and the total arrival rate vector $\alpha$ (including internally routed traffic) is the unique solution of the traffic equations $\alpha = \lambda + P'\alpha$ . A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions $\gamma_i := \alpha_i m_i/\rho_{p(i)}$ (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.

Formalization targets

Goal: Theorem 8.18 — HLSPS control is stable under the standard load condition

For any queueing network under HLSPS control with proportion vector $\gamma$ , if

\rho < b \qquad (\text{the standard load condition, Eq. 5.1}),

the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.

Supporting milestones

Lemma 8.15 isolates the workload derivative identity $\dot W_k(Z(t)) = \rho_k - b_k$ at a busy station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma 8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct structural engine behind the goal theorem: a uniform excess departure rate over the total arrival rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.

Significance

The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.

Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network, q=workload) return no relevant results (per triage.json); this mission is a from-scratch formalization of feedforward networks, the workload operator, HLSPS control, and their stability theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.

Difficulty

Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights $\delta_k$ , chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function $H(z) = \max_k \delta_k W_k(z)$ is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.

Formalization scope

Mission IV's queueing-network model data and fluid-equation specialization are restated locally (drafts in this series do not import one another). The workload operator's matrix inverse $(I-P')^{-1}$ is supplied as external data with its defining two-sided-inverse property, rather than derived from substochasticity/transience hypotheses on $P$ (Chapter 2 material, out of series scope) — the same convention mission III used for its process-family apparatus. The non-idling and HLSPS fluid models are each packaged as their own predicate plus a Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the non-idling stability object (not a separately restated "FCFS fluid model") since the book's own remark identifies the two exactly for generalized Jackson networks. A formalization that stated Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's actual proof architecture (see Difficulty); this mission keeps them as independent milestones/ goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range but absent from the planning brief's disposition table, is added as a milestone rather than silently dropped, since it is the structural step the goal theorem's own proof cites by name. QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model predicates are the primary reusable contributions; contributions completing the five by sorry proofs are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.

10 thms2 active usersReviewed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks IV: Fluid Equations for Non-Idling, Priority and FCFS ControlTextbook

Motivation

Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.

The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.

Setting

A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class $i$ is served by a unique pool $p(i)$ , and on completion a class- $i$ job becomes class $j$ with probability $P_{ij}$ (the routing matrix). $I(k)$ denotes the set of classes served by pool $k$ . The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity ( $\hat D = \hat F$ ) and the output matrix is $\Gamma_{ij} = P_{ji}$ .

Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation $\sigma$ , always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy $\beta = h(\hat z)$ , where $\hat z$ is the updated job-count vector and $h$ is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.

Formalization targets

Goal: Theorem 7.5 — the FCFS fluid equation

For a queueing network under FCFS control, every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ satisfies (6.1)-(6.6) and

\hat D_i\big(t + \hat W_k(t)\big) = \hat G_i(t), \qquad t \ge 0,\ i \in I(k),\ k \in K,

where $\hat G_i(t) = \lambda_i t + \sum_j P_{ji}\hat D_j(t)$ is the fluid arrival rate into class $i$ and $\hat W_k(t) = \sum_{i \in I(k)} m_i \hat Z_i(t)$ is pool $k$ 's fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).

Supporting milestones

Theorem 7.2 (non-idling): $\sum_{i\in I(k)} \hat Z_i(t) > 0$ forces pool $k$ 's aggregate service rate to run at full capacity $b_k$ . Theorem 7.3 (non-preemptive SBP): the same conclusion with $I(k)$ sharpened to the priority set $H(j)$ (Eq. 7.5), for every buffer $j$ . Theorem 7.8 (general relaxed control): under Assumption 7.6, $\hat Z_i(t) > 0$ forces $\hat T_i$ 's derivative to equal $h_i(\hat Z(t))$ exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable $h$ .

Significance

The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.

Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy all return zero hits, consistent with triage.json's record that none of this book's Chapters 6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing networks, their three named control-policy families, and the four policy-specific fluid equations Chapter 7 derives for them.

Difficulty

The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with $I(k)$ replaced by $H(j)$ — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at $t + \hat W_k(t)$ match arrivals at $t$ ), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on $\hat T$ or $\hat D$ alone, without introducing the auxiliary workload process $\hat W$ , could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — " $\hat Z_i(t) = 0$ implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.

Formalization scope

Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally in this chapter's own namespace rather than imported, since drafts in this series do not import one another; the restatement is trimmed to the four raw processes $(D^x,F^x,T^x,Z^x)$ this chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized, applied to different index sets ( $I(k)$ vs. $H(j)$ ) — the pathwise full-utilization identity (7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of the service-starting mechanism is out of scope for this chapter, exactly as it was for mission III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12) (rewritten via the material-balance equation to avoid needing the raw arrival process) and the fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the "delayed random walk" $V$ of Eq. (6.47). A formalization that dropped the workload shift $\hat W_k(t)$ from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication (which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions completing the four by sorry proofs — each of which needs the u.o.c.-convergence and dominated-convergence arguments mission III's own proofs still lack — are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.
M. Bramson, "Instability of FIFO queueing networks," Annals of Applied Probability 4 (1994), 414–431.
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Optimization·Captain: mikedeng1

Existence of an Equilibrium for a Competitive Economy I: Equilibrium Exists When Every Consumer Can Trade Every GoodResearch Paper

Motivation

Walras (1874) described an economy as a system of simultaneous equations, one per market, and argued that a set of prices clearing all markets exists because the number of equations equals the number of unknowns. Counting equations proves nothing, and the question of whether competitive equilibrium exists at all remained open for eighty years. Wald (1935–36) proved existence in special production models under restrictive assumptions on demand. In 1954 Kenneth Arrow and Gérard Debreu gave the first existence proof for a general model with production, many consumers, convex technologies and preferences given by utility indicators (Econometrica 22 (1954) 265–290); McKenzie published an independent proof for a trade model in the same year (Econometrica 22 (1954) 147–161). The resulting Arrow–Debreu model is the reference model of general equilibrium theory and the starting point of market-equilibrium problems in operations research and algorithmic game theory.

The paper proves two existence theorems. This mission is the first, Theorem I, whose key assumption is that every consumer initially holds a positive amount of every commodity. A second mission treats Theorem II, which replaces that assumption by a weaker condition on labour supply.

Setting

There are $l \ge 1$ commodities; a commodity vector is an element of $\mathbb R^l$ , compared componentwise ( $x \geqq y$ means $x_h \ge y_h$ for all $h$ ; $x > y$ means $x_h > y_h$ for all $h$ ). The inner product is $p\cdot x = \sum_h p_h x_h$ .

Producers $j = 1, \dots, n$ each have a production set $Y_j \subseteq \mathbb R^l$ (outputs positive, inputs negative). The aggregate production set is $Y = \sum_j Y_j$ .
Consumers $i = 1, \dots, m$ each have a consumption set $X_i \subseteq \mathbb R^l$ , a utility indicator $u_i$ on $X_i$ , initial holdings $\zeta_i \in \mathbb R^l$ , and a share $\alpha_{ij}$ of the profit of producer $j$ .

Assumptions I–IV are: (I.a) each $Y_j$ is closed, convex and contains $0$ ; (I.b) $Y \cap \Omega = \{0\}$ with $\Omega = \{x \geqq 0\}$ ; (I.c) $Y \cap (-Y) = \{0\}$ ; (II) each $X_i$ is closed, convex and bounded from below; (III.a) $u_i$ is continuous on $X_i$ ; (III.b) no $x_i \in X_i$ is a satiation point; (III.c) if $u_i(x_i) > u_i(x_i')$ and $0 < t < 1$ then $u_i[t x_i + (1-t) x_i'] > u_i(x_i')$ ; (IV.a) some $x_i \in X_i$ satisfies $x_i < \zeta_i$ ; (IV.b) $\alpha_{ij} \ge 0$ and $\sum_i \alpha_{ij} = 1$ .

A competitive equilibrium is a tuple $(x_1^*, \dots, x_m^*, y_1^*, \dots, y_n^*, p^*)$ such that

each $y_j^*$ maximizes $p^*\cdot y_j$ over $Y_j$ ;
each $x_i^*$ maximizes $u_i$ over $\{x_i \in X_i : p^*\cdot x_i \leqq p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*\}$ ;
$p^* \in P = \{p \geqq 0 : \sum_h p_h = 1\}$ ;
$z^* = \sum_i x_i^* - \sum_j y_j^* - \sum_i \zeta_i$ satisfies $z^* \leqq 0$ and $p^*\cdot z^* = 0$ .

An abstract economy (§2) is a game in which each player's feasible set $A_\iota(\bar a_\iota)$ depends on the other players' actions $\bar a_\iota$ ; an equilibrium point is a profile at which every player maximizes its pay-off over its feasible set. The proof builds an abstract economy $E$ with the consumers, the producers and a fictitious market participant who chooses $p \in P$ and receives $p\cdot z$ , and a truncated version $\tilde E$ in which all choices are restricted to a large cube $C$ .

Formalization targets

Goal: Theorem I

\text{Assumptions I–IV} \implies \exists\, (x^*, y^*, p^*) \text{ satisfying Conditions 1–4.}

The statement fixes no constants; its only added hypothesis is $l \ge 1$ .

Milestones

In the order of the paper's argument:

§1.3.1: under II, III.a and III.c, each $u_i$ is quasi-concave on $X_i$ .
§1.4.2 (1): Condition 2 together with II, III.b and III.c gives $p^*\cdot x_i^* = p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*$ .
Lemma 2.5: an abstract economy with compact convex action sets, continuous pay-offs that are quasi-concave in the player's own action, and continuous constraint correspondences with closed graphs and nonempty convex values has an equilibrium point.
§3.1.2 (2): at an equilibrium point of $E$ , Condition 2 holds.
§3.2: every equilibrium point of $E$ is a competitive equilibrium.
§3.3.1 (7) and §3.3.2 (2): the attainable sets $\hat Y_j$ and $\hat X_i$ (choices compatible with $z \leqq 0$ ) are bounded.
Remark §3.3.5: if $p\cdot\zeta_i > \min_{\tilde X_i} p\cdot x_i$ , the truncated budget correspondence $\tilde A_i$ is continuous at that point.
§3.4.0: for a cube $C$ containing every $\hat X_i$ and $\hat Y_j$ in its interior, $\tilde E$ has an equilibrium point.
§3.4.1: every equilibrium point of $\tilde E$ is an equilibrium point of $E$ .

Significance

Theorem I shows that the competitive model is consistent: under convexity, continuity, non-satiation and survival assumptions, prices exist at which profit maximization, utility maximization and market clearing hold simultaneously. The welfare theorems, comparative statics, and algorithms that compute equilibria (Scarf's method, market-equilibrium algorithms) presuppose it. Lemma 2.5, Debreu's social-equilibrium theorem (PNAS 38 (1952) 886–893), is also used on its own for generalized Nash equilibrium problems with coupled constraints.

The theorem is proved and textbook material (Debreu, Theory of Value, 1959). To the best of the catalog search, no proof assistant library contains Theorem I, Lemma 2.5, or a Kakutani-type fixed-point theorem for correspondences; on this platform the only related results are Brouwer's fixed-point theorem (AGT.brouwer_fixed_point, proved) and Nash's theorem for finite games (AGT.nash_existence), a special case of Lemma 2.5 with constant constraint sets. The mission produces a machine-checked proof of the paper's argument and, along the way, reusable statements about abstract economies and their equilibria.

Difficulty

The central difficulty is Lemma 2.5. The paper does not prove it but cites Debreu (1952), whose proof uses the Eilenberg–Montgomery fixed-point theorem for correspondences with contractible values. Brouwer's theorem alone does not suffice: the best-response correspondence of an abstract economy is set-valued, and its closed graph must be established from the continuity of the feasible-set correspondences, which is a maximum-theorem argument that Mathlib does not contain. A Kakutani-type fixed-point theorem, or an approximation argument reducing to Brouwer, is needed.

A second difficulty is non-compactness. The economy $E$ has unbounded action sets, so the Lemma does not apply to it directly. The boundedness of the attainable sets (§3.3.1) is an asymptotic argument using the irreversibility and no-free-production assumptions I.b and I.c, and the passage from $\tilde E$ back to $E$ (§3.4.1) needs the attainable choices to lie in the interior of the cube, so that local optimality implies global optimality through III.c. A fixed-point argument on an excess-demand function does not apply directly: demand need not be single-valued or even defined at every price.

Formalization scope

Commodity space is Fin l → ℝ with its componentwise order; the paper's strict vector inequality is written coordinatewise (∀ h, x h < ζ i h), not with the order-theoretic strict inequality on functions. Consumers are Fin m, producers Fin n, and the players of $E$ are Fin m ⊕ Fin n ⊕ Unit. Utilities are total functions, and every assumption on them quantifies over $X_i$ only. "Maximizes" is always written as membership plus an inequality against every feasible alternative, never through a supremum. Continuity of a constraint correspondence is the paper's sequential definition (§2.4), a lower-hemicontinuity condition, required at every point of the other players' action space; convergence is asked only in the other players' coordinates.

Two hypotheses are made explicit because the formal statements would otherwise be false: Theorem I and §3.4.0 assume $l \ge 1$ (for $l = 0$ the price simplex is empty), and Lemma 2.5 assumes every action set nonempty (otherwise, with two or more players and all action sets empty, every hypothesis holds vacuously). The Remark of §3.3.5 carries, as a hypothesis, the nonemptiness of $\tilde A_i$ established in §3.3.4. A formalization that makes Theorem I trivial, for instance by taking $P$ to contain $0$ , by reading IV.a with the order-theoretic strict inequality, or by allowing an empty commodity space, is ruled out by these definitions.

A complete development needs: Kakutani's fixed-point theorem (or a Brouwer-based substitute) for compact convex subsets of $\mathbb R^l$ ; Berge's maximum theorem for the best-response correspondence; the asymptotic-cone argument for §3.3.1; and elementary convex analysis for the budget sets. The abstract-economy definitions and Lemma 2.5 are reusable beyond this mission, including by the Theorem II mission. Contributions of any of these components are welcome, as are alternative proofs of Lemma 2.5.

Selected references

K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3) (1954) 265–290. https://doi.org/10.2307/1907353
G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10) (1952) 886–893. https://doi.org/10.1073/pnas.38.10.886
L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2) (1954) 147–161. https://doi.org/10.2307/1907539
J. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1) (1950) 48–49. https://doi.org/10.1073/pnas.36.1.48
S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Mathematical Journal 8(3) (1941) 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
G. Debreu, Theory of Value: An Axiomatic Analysis of Economic Equilibrium, Wiley, 1959 (Cowles Foundation Monograph 17).

16 thms2 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Dual Stochastic Dominance and Related Mean-Risk Models 1: Second-Degree Stochastic Dominance Is Dominance of Absolute Lorenz CurvesResearch Paper

Motivation

Comparing uncertain outcomes is the basic problem of decision making under risk. Second-degree stochastic dominance (SSD) is the comparison that every risk-averse decision maker who prefers larger outcomes agrees with: $X$ dominates $Y$ in this sense exactly when $\mathbb E\,U(X)\ge\mathbb E\,U(Y)$ for every nondecreasing concave utility $U$ for which the expectations are finite. The relation grew out of majorization theory for finite distributions (Hardy, Littlewood and Pólya) and was extended to general distributions by Rothschild and Stiglitz and by Hadar and Russell around 1970; it is the standard consistency requirement for portfolio models and for risk measures in operations research and finance.

SSD is defined through the distribution function, which is awkward in optimization: portfolio returns are linear in the decision variables, but their distribution functions are not. Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) showed that SSD has an equivalent dual description through the integrated quantile function, the absolute Lorenz curve, and that the two descriptions are related by Fenchel conjugation. That dual description underlies the later theory of SSD-constrained optimization (Dentcheva and Ruszczyński, SIAM J. Optim. 14 (2003)) and the use of conditional value-at-risk as an SSD-consistent risk measure.

Setting

Fix a probability space $(\Omega,\mathcal B,\mathbb P)$ and real random variables $X,Y:\Omega\to\mathbb R$ with $\mathbb E|X|<\infty$ , $\mathbb E|Y|<\infty$ .

The distribution function is $F_X(\eta)=\mathbb P\{X\le\eta\}$ (Lean: distFun P X).
The second performance function is the area below it, $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi$ (secondPerformance P X, eq. (2.1)).
SSD: $X\succeq_{SSD}Y$ iff $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for every $\eta\in\mathbb R$ (SSD P X Y, eq. (2.2)). The dominating variable has the smaller curve.
The first quantile function is the left-continuous inverse $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$ , $0<p\le1$ (leftQuantile P X). A number $q$ is a $p$ -quantile if $\mathbb P\{X<q\}\le p\le\mathbb P\{X\le q\}$ (IsPQuantile P X p q).
The second quantile function (absolute Lorenz curve) $F_X^{(-2)}:\mathbb R\to\overline{\mathbb R}$ is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ for $0\le p\le1$ and $+\infty$ otherwise (secondQuantile P X, eq. (3.2)).
The convex conjugate of $F:\mathbb R\to\overline{\mathbb R}$ is $F^*(p)=\sup_\xi\{p\xi-F(\xi)\}$ (conj F), and $\partial f(\eta)$ is the subdifferential of a real function $f$ at $\eta$ (subdiff f η).

Formalization targets

Goal: Theorem 3.2

X\succeq_{SSD}Y\iff F_X^{(-2)}(p)\ge F_Y^{(-2)}(p)\quad\text{for all }0\le p\le1.

Both directions are required, and the range of $p$ includes both endpoints (at $p=1$ the right-hand side contains $\mathbb EX\ge\mathbb EY$ ).

Milestones, in the order the argument uses them

(2.4): $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}(\eta-\xi)\,P_X(d\xi)=\mathbb E\max(\eta-X,0)$ .
§2, p. 62: $F_X^{(2)}$ is continuous, convex, nonnegative and nondecreasing.
§3, p. 64: for $p\in(0,1)$ the $p$ -quantiles form a closed interval with left end $F_X^{(-1)}(p)$ .
(3.3): $\partial F_X^{(2)}(\eta)=[\mathbb P\{X<\eta\},\mathbb P\{X\le\eta\}]$ for every $\eta$ .
Theorem 3.1(i): $F_X^{(-2)}=[F_X^{(2)}]^*$ on all of $\mathbb R$ .
Theorem 3.1(ii): $F_X^{(2)}=[F_X^{(-2)}]^*$ on all of $\mathbb R$ .

A companion item, Corollary 3.3, states the four equivalent characterizations of a $p$ -quantile (quantile condition, attainment in either conjugate, and the Fenchel–Young equality $F_X^{(-2)}(p)+F_X^{(2)}(\eta)=p\eta$ ).

Significance

Theorem 3.2 converts a condition on distribution functions into a condition on integrated quantiles. Its consequences in the paper include the SSD consistency of the mean–risk models built on tail means (conditional value-at-risk), on the Gini mean difference and on the mean absolute deviation from a quantile, and the linear-programming representations of those models for finitely many scenarios; the companion mission Dual Stochastic Dominance and Related Mean-Risk Models 2 builds on the same objects. Theorem 3.1 is the precise statement that $F_X^{(2)}$ and $F_X^{(-2)}$ form a conjugate pair; Corollary 3.3 identifies the subgradients of each with the quantiles of $X$ .

All results here are proved in the paper, and the quantile characterization of the increasing concave order also appears in the stochastic-orders literature. None of them is formalized: Mathlib at the pinned revision has ProbabilityTheory.cdf but no convex conjugate on the extended reals, no subdifferential of a real function, no quantile function and no stochastic dominance. The mission produces a machine-checked account of the quantile side of SSD, with the conjugacy stated exactly, including the value $+\infty$ off $[0,1]$ .

Difficulty

The naive route to Theorem 3.2 compares $F_X^{(2)}$ and $F_Y^{(2)}$ through the quantile functions directly, but the first quantiles $F^{(-1)}$ need not be ordered when $X\succeq_{SSD}Y$ (the paper notes this on p. 65), so no pointwise argument on quantiles works. The equivalence rests on Theorem 3.1, and there the hard part is computing the conjugate of $F_X^{(2)}$ for a general distribution: atoms of $X$ make $F_X^{(2)}$ nondifferentiable and flat pieces of $F_X$ make the maximizer non-unique, so the subdifferential (3.3) and the interval of $p$ -quantiles must be handled as sets, and the endpoints $p=0,1$ (where the supremum need not be attained) and $p\notin[0,1]$ (where it is $+\infty$ ) must be treated separately. Part (ii) is a biconjugation statement for a closed convex function, whose general form is not in Mathlib.

Formalization scope

One probability space (Ω, P) with [IsProbabilityMeasure P] carries both $X$ and $Y$ ; nothing depends on anything but the laws, and no independence is assumed.
$F_X(\eta)$ is P.real {ω | X ω ≤ η}; $F_X^{(2)}$ is a Bochner integral over Set.Iic η; $F_X^{(-2)}$ is an interval integral over $(0,p]$ , placed in EReal, with ⊤ off $[0,1]$ .
The conjugate is ⨆ ξ, ((p * ξ : ℝ) : EReal) - F ξ in the complete lattice EReal, so terms where $F=+\infty$ contribute $-\infty$ , exactly the paper's convention.
Standing assumption. Every item using $F^{(2)}$ or $F^{(-2)}$ assumes Integrable X P (and Integrable Y P in the goal). This is the paper's own hypothesis $\mathbb E|X|<\infty$ (p. 65, and the hypothesis of Theorem 3.1), not a repair. The $p$ -quantile milestone assumes only AEMeasurable X P.
Quantile at $p=1$ . $F_X^{(-1)}$ is a real sInf. It is the true infimum for $0<p<1$ ; at $p=1$ the paper's value can be $+\infty$ while sInf ∅ = 0. This one point does not affect (3.2), and no item states anything about $F_X^{(-1)}(1)$ .
Omitted. The conditional-expectation form $\mathbb P\{X\le\eta\}\,\mathbb E\{\eta-X\mid X\le\eta\}$ in (2.4) is not stated, since it is undefined when $\mathbb P\{X\le\eta\}=0$ .
Trivializing encodings are ruled out. $F^{(2)}$ is defined by (2.1), not as $\mathbb E\max(\eta-X,0)$ , and $F^{(-2)}$ by (3.2), not as a conjugate; either shortcut would make a milestone or Theorem 3.1 true by definition.
Infrastructure and reuse. Welcome contributions: the extended-real conjugate and Fenchel–Young inequality on $\mathbb R$ , biconjugation of closed convex functions of one variable, subdifferentials of integrals of monotone functions, and the basic theory of left quantiles (the quantile transform $F_X^{(-1)}(U)\sim X$ ). These are reusable beyond this mission, in particular by mission 2 of this series and by any formalization of conditional value-at-risk. The platform's VectorSpaceOpt.fenchel_biconjugate_on and ConvexOptimization.fenchelConjugate concern real-valued conjugates on other spaces and are related but not reused.

Selected references

W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 12.2 and 23.5 are used in the paper's proofs). https://doi.org/10.1515/9781400873173
M. Rothschild, J. E. Stiglitz, Increasing risk: I. A definition, J. Econom. Theory 2 (1970) 225–243. https://doi.org/10.1016/0022-0531(70)90038-4
J. Hadar, W. R. Russell, Rules for ordering uncertain prospects, Amer. Econom. Rev. 59 (1969) 25–34. https://www.jstor.org/stable/1811090
D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14(2) (2003) 548–566. https://doi.org/10.1137/S1052623402420528
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

10 thms2 active usersReviewed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks I: The Equivalence of SPN StabilityTextbook

Motivation

A stochastic processing network (SPN) is the general model behind manufacturing lines, call centers, computer systems, communication networks and hospital wards: a collection of buffers holding waiting work, a collection of activities (servers) that consume items from buffers and produce items into others, and stochastic primitives — arrival processes and service requirements — that drive the whole system forward in continuous time. Before any control policy can be designed, evaluated, or proved to work, the modeler needs a single, unambiguous, checkable notion of what it means for such a system to be stable: to settle into statistical equilibrium rather than pile up work without bound.

The difficulty is that "stability" has several natural, superficially different candidate definitions — positive recurrence of the underlying Markov chain, existence of a unique stationary distribution, convergence in distribution of queue lengths — each convenient for a different purpose (positive recurrence for verifying via drift criteria, a stationary distribution for computing long-run averages, distributional convergence for interpreting simulation output). J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' own pre-publication draft, 2020-4-2, http://spnbook.org) opens its technical development by proving these candidates coincide, so that the rest of the book — and, in practice, most stability results for queueing networks published since Rybko and Stolyar's and Dai's foundational work in the 1990s — can speak of "SPN stability" as one well-posed property.

Setting

An SPN has $I$ buffers, indexed $1, \dots, I$ , and $J$ activities (service types), indexed $1, \dots, J$ . External work arrives into buffer $i$ according to a counting process $E_i(t)$ ; activity $j$ , whenever engaged, requires a service time and produces an output vector into the buffers on completion. The baseline stochastic assumptions (Assumption 2.1) specify these primitives precisely: the $I$ external arrival processes are independent Poisson processes with rates $\lambda_1, \dots, \lambda_I \ge 0$ (no arrivals into a buffer with rate $0$ ); for each activity $j$ , the matched pairs of processing variables — service time and output vector, $(v_j(\ell), \varphi_j(\ell))_{\ell \ge 1}$ — form an i.i.d. sequence with finite means $m_j = \mathbb{E}[v_j(1)] > 0$ and $\Gamma_j = \mathbb{E}[\varphi_j(1)] \ge 0$ ; each such pair has a joint phase-type distribution (realized as the absorption time and terminal mark of a finite-state continuous-time Markov chain, per Appendix D.9); and the initial processing variables, the arrival process, and the $J$ processing-variable sequences are, collectively, mutually independent.

Under a fixed control policy, the SPN generates two continuous-time processes: the service-count process $N(t) \in \mathbb{Z}_+^J$ and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$ . Assumption 3.1 (Markov representation) requires these to be embeddable in a richer, irreducible Markov chain $X = \{X(t), t \ge 0\}$ on a countable state space $\mathcal{X}$ : a function $f : \mathcal{X} \to \mathbb{Z}_+^J \times \mathbb{Z}_+^I$ with $(N(t), Z(t)) = f(X(t))$ on every sample path, whose level sets $B(z) = \{x : f(x) = (n,z)\ \text{for some } n\}$ are finite for every buffer-content vector $z$ , and which has at least one empty state $x^\ast$ with $f(x^\ast) = (0,0)$ .

Formalization targets

Goal: Proposition 3.5 — equivalent definitions of stability

X \text{ positive recurrent} \iff X \text{ has a unique stationary distribution } \pi \iff Z(t) \text{ converges in distribution to a non-defective limit},

and, when these hold, for every bounded $h : \mathcal{X} \to \mathbb{R}$ and every initial distribution of $X(0)$ ,

\Pr\left\{ \lim_{t \to \infty} \frac{1}{t} \int_0^t h(X(s))\, ds = \bar h \right\} = 1, \qquad \bar h := \sum_{x \in \mathcal{X}} \pi(x)\, h(x).

Definition 3.6 then names an SPN stable exactly when these equivalent conditions hold — the weakest possible target, since it commits to no particular one of the three characterizations, only to their joint truth or falsity.

Supporting milestones

Two strong laws of large numbers for the primitive stochastic elements (Propositions 2.2 and 2.3) — the arrival counts $E_i(t)/t \to \lambda_i$ and the processing-variable sample means $\frac{1}{n}\sum_{\ell \le n} v_j(\ell) \to m_j$ , $\frac{1}{n}\sum_{\ell \le n} \varphi_j(\ell) \to \Gamma_j$ — and two structural results about the ambient chain: Lemma 3.7, a drift-type sufficient condition for positive recurrence that foreshadows the fluid-model methodology of later chapters, and Proposition 3.9, a sufficient condition (reachability of the empty state) for the irreducibility that Assumption 3.1 itself demands.

Significance

The result itself. Proposition 3.5 is what turns "is this queueing network stable?" into a single question rather than three potentially different ones, and it licenses every later chapter of the book (and a large fraction of the queueing-theory literature going back to the 1990s fluid-limit program of Rybko–Stolyar, Dai, and others) to prove stability via whichever characterization is most convenient — typically positive recurrence via a Lyapunov drift argument — while concluding all three, including the practically important long-run-average SLLN. Every one of the thirteen other missions in this series builds directly on Definition 3.6: their goal theorems all conclude "the SPN is stable," meaning exactly the three-way equivalence established here.

Formalizing it. No result in this mission or its milestones has a prior formal counterpart on Prove2Me: a search for "positive recurrent," "stationary distribution Markov chain," and "irreducible Markov chain" surfaced only MarkovMixing's PositiveRecurrent predicate, defined for a countable-state discrete-time chain — a different object from Assumption 3.1's continuous-time ambient chain, reused here only conceptually (as the pattern for a mean-return-time definition), not as a Lean dependency. This mission is a from-scratch formalization of the model (baseline stochastic assumptions, Markov representation) and of positive recurrence, stationary-distribution uniqueness, and distributional convergence for it.

Difficulty

The obvious first attempt — define $X$ as an arbitrary countable-state Markov chain and directly import a Mathlib theorem relating its recurrence, its stationary distribution, and long-run convergence — fails because Mathlib currently has no general countable-state continuous-time Markov chain theory of the kind Appendix D of the book develops (its own finite-state CTMC stationary-distribution result is unproven substrate, not applicable to a countably infinite state space). The formalization instead works at the level of the chain's embedded discrete-time jump chain, which is where Lean's PMF-based machinery is available, and states the three equivalent conditions and the SLLN conclusion directly as hypotheses to be discharged, rather than inheriting them from a pre-existing continuous-time framework. A second difficulty is Assumption 2.1(d)'s independence clause, which is a genuine three-way mutual independence of $\sigma$ -algebras (initial processing variables, arrival process, and the collection of all $J$ processing-variable sequences), not the pairwise independence a careless reading might substitute — a weaker hypothesis here would silently make later derivations in the series unsound.

Formalization scope

The ambient chain's state space Xstate is an arbitrary countable type ([Countable Xstate], not Fintype) — no result may assume finiteness anywhere. The chain itself is represented by its one-step jump kernel jump : Xstate → PMF Xstate (stepIter gives $n$ -step iteration, Irreducible requires every state to reach every other in finitely many jump-chain steps); positive recurrence is mean return time under jump, defined via the standard first-return-time renewal decomposition. IsStable is defined as positive recurrence of the jump chain — one of the three equivalent conditions — with the goal theorem itself certifying the equivalence, so the choice carries no loss of faithfulness. Buffer contents and service counts are Fin I → ℕ and Fin J → ℕ-valued, matching the book's $\mathbb{Z}_+^I$ , $\mathbb{Z}_+^J$ . A formalization that took IsStable to mean, say, only distributional convergence of $Z$ (dropping the chain-level characterizations) would be a strictly weaker, trivializing shortcut — ruled out here by proving all three equivalent and stating the SLLN as part of the same goal theorem. The definitions in this mission (BaselineAssumptions, MarkovRepresentation, IsStable) are the shared substrate every other mission of the series is built on, and are the primary reusable contribution; contributions completing the by sorry proofs, particularly of the goal theorem (which the book proves via appeal to general CTMC theory in its Appendix D, not reproduced here), are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.

11 thms2 active usersReviewed

Completed

Optimization·Captain: mikedeng1

An Interactive Weighted Tchebycheff Procedure for Multiple Objective Programming I: In the Finite Case the Augmented Weighted Tchebycheff Program Characterizes the Nondominated SetResearch Paper

Motivation

A decision problem with several conflicting objectives, such as cost, risk and service level, has no single optimum. What it has is a set of nondominated outcomes: those that cannot be improved in one objective without being worsened in another. Interactive methods of multiple objective programming search this set with a decision-maker, and at each step they need a computational device that returns nondominated outcomes and can return any of them.

The classical device, maximizing a weighted sum of the objectives, fails the second requirement. On a nonconvex or discrete outcome set it only reaches the supported nondominated points, those on the boundary of the convex hull, and misses the rest (see, e.g., Boyd and Vandenberghe, Convex Optimization, §4.7.4, where the weighted-sum approach is shown to be sufficient but not necessary for Pareto optimality). Steuer and Choo (Math. Programming 26 (1983) 326–344) replaced the weighted sum by a weighted Tchebycheff distance to an ideal point, augmented by a small linear term. Their procedure became one of the standard interactive methods of the field, and the augmented Tchebycheff scalarization is now a standard tool in multiobjective integer programming and in the generation of nondominated sets.

Timeline, as recorded in the paper's own references. Dinkelbach and Dürr (1972) showed, in the linear case, that among the minimizers of a weighted Tchebycheff program there is always a nondominated one (the paper's Theorem 3.1 extends this to the discrete case). Bowman (Lecture Notes in Economics and Mathematical Systems, as cited by the paper) related the Tchebycheff norm to the efficient frontier of multiple-criteria problems. Choo and Atkins (Computers and Operations Research 7, 1980) and Choo's dissertation (1980) developed interactive weighted Tchebycheff algorithms. Steuer and Choo (1983) added the augmentation term $\rho\,e^{\mathsf T}(z^*-z)$ , gave an explicit choice of the weights and of $\rho$ in the discrete case, and proved that the resulting program characterizes the nondominated set exactly (Theorem 3.7).

Setting

There are $k \ge 1$ objectives to be maximized. The set of attainable criterion vectors is a finite set $Z \subset \mathbb R^k$ (in the paper, $Z$ is the image of a discrete feasible set $S$ under the objectives $f_1,\dots,f_k$ ). A vector $z$ dominates $\bar z$ if $z_i \ge \bar z_i$ for all $i$ and $z_i > \bar z_i$ for at least one $i$ . The nondominated set $N \subseteq Z$ consists of the $\bar z \in Z$ that no $z \in Z$ dominates.

An ideal criterion vector $z^* \in \mathbb R^k$ has coordinates $z^*_i = \max_{z\in Z} z_i + \varepsilon_i$ with $\varepsilon_i \ge 0$ , where $\varepsilon_i$ must be strictly positive if (i) more than one nondominated vector maximizes objective $i$ , or (ii) the only nondominated vector maximizing objective $i$ also maximizes another objective.

Weights range over the simplex $\bar\Lambda = \{\lambda \in \mathbb R^k \mid \lambda_i \ge 0,\ \sum_i \lambda_i = 1\}$ . For a scalar $\rho$ the augmented weighted Tchebycheff program is

\min\ \alpha + \rho\, e^{\mathsf T}(z^* - z) \quad\text{s.t.}\quad \alpha \ge \lambda_i (z^*_i - z_i),\ 1 \le i \le k,\quad z \in Z,

where $e$ is the vector of ones; at a fixed $z$ its value is $\max_i \lambda_i(z^*_i - z_i) + \rho\,e^{\mathsf T}(z^*-z)$ .

For $z^p \in Z$ the paper defines weights $\lambda^p$ by (b): $\lambda^p_i \propto 1/(z^*_i - z^p_i)$ , normalized to sum to one, when $z^p_i \ne z^*_i$ for all $i$ ; otherwise $\lambda^p$ puts weight $1$ on the coordinates where $z^p_i = z^*_i$ and $0$ elsewhere. With $\alpha_{pq} = \max_i \lambda^p_i (z^*_i - z^q_i)$ it sets

\rho = \tfrac12 \min_{z^i \in N,\ z^j \in Z}\Big\{\frac{\alpha_{ij} - \alpha_{ii}}{e^{\mathsf T}(z^j - z^i)} \;\Big|\; e^{\mathsf T}(z^j - z^i) > 0\Big\}. \tag{3.8}

Formalization targets

Goal: Theorem 3.7

For every $z^p \in Z$ ,

z^p \in N \iff \exists \lambda \in \bar\Lambda\ \ \forall z \in Z:\ \max_i \lambda_i(z^*_i - z^p_i) + \rho\, e^{\mathsf T}(z^*-z^p) \le \max_i \lambda_i(z^*_i - z_i) + \rho\, e^{\mathsf T}(z^*-z),

with $\rho$ from (3.8). One coefficient $\rho$ , computed from $Z$ and $z^*$ alone, works for the whole nondominated set.

Milestones, in the order of the paper

Theorem 3.1. For any $\lambda \in \bar\Lambda$ , some minimizer of the (unaugmented) weighted Tchebycheff program over $Z$ is nondominated.
Lemma 3.2 (corrected). For $z^p \in N$ and $z^q \in Z$ with $z^q \ne z^p$ and $z^q \not\le z^p$ , $z^q$ lies outside the level set $\Phi(\alpha_{pp})$ .
Lemma 3.3 (corrected). Under the same hypotheses, $\alpha_{pp} < \alpha_{pq}$ .
$\rho_p > 0$ , the first step of the proof of Theorem 3.4, for the single-vector coefficient $\rho_p$ of (3.6).
Theorem 3.4. Each $z^p \in N$ is the unique minimizer of the augmented program with weights $\lambda^p$ and coefficient $\rho_p$ .
Corollary 3.9. The same with the common $\rho$ of (3.8), and $\lambda^p \in \bar\Lambda$ .

Printed Lemmas 3.2 and 3.3 are false. For $Z = \{(5,3), (5,1), (1,10)\}$ and $z^* = (5,10)$ , which is ideal with $\varepsilon = 0$ , the nondominated vector $z^p = (5,3)$ has $\lambda^p = (1,0)$ and $\alpha_{pp} = 0$ , while the dominated vector $z^q = (5,1)$ lies in $\Phi(0) = \{z \mid z_1 \ge 5\}$ and has $\alpha_{pq} = 0$ . The proof's second case assumes that only $z^p$ reaches $z^*_j$ in coordinate $j$ , but the $\varepsilon$ -rule constrains nondominated vectors only. The mission states both lemmas with the added hypothesis $z^q \not\le z^p$ , under which they hold; the milestone texts are the printed ones. Theorems 3.4, 3.7 and Corollary 3.9 are unaffected, since for $z^q \le z^p$ , $z^q \ne z^p$ the augmentation term separates $z^q$ from $z^p$ on its own. Hypothesis (a) of the paper also contains the misprint " $z^q \ne z^q$ " for $z^q \ne z^p$ .

Significance

Theorem 3.7 says that the augmented weighted Tchebycheff program, with a computable $\rho$ , is an exact scalarization of the discrete multiple objective program. It returns only nondominated vectors (unlike the plain Tchebycheff program, whose optima can be weakly dominated) and it can return every nondominated vector, including unsupported ones (unlike weighted sums). Corollary 3.9 adds that each nondominated vector is the unique optimum for a suitable weight, so it is found even by a solver that stops at the first optimum. These facts underlie the interactive Tchebycheff procedure of the paper's §5 and a large body of later work on generating nondominated sets of multiobjective integer programs.

The results are proved in the paper; to our knowledge none has been machine-checked. The mission produces a checked version with the two lemmas of the paper's proof chain corrected, a precise treatment of the ideal-vector rule, and an explicit $\rho$ . Alternative proofs, for instance one for the goal that avoids the explicit $\rho$ of (3.8), are welcome.

Difficulty

The ⇐ direction is short. The work is in ⇒: the explicit weights $\lambda^p$ must be shown to lie in $\bar\Lambda$ and to make $z^p$ strictly better than every competitor that is not below it. Both depend on the $\varepsilon$ -rule for $z^*$ , whose role is subtle: it forbids two coordinates of a nondominated vector from reaching $z^*$ , and forbids two nondominated vectors from sharing a coordinate equal to $z^*_j$ , but it says nothing about dominated vectors. The paper's own argument overlooks exactly those dominated vectors, so a proof that follows the printed Lemma 3.2 literally will fail; the gap is closed only by combining the corrected lemma with the augmentation term. Choosing a single $\rho$ for all of $N$ also requires that every quotient in (3.8) be strictly positive.

Formalization scope

Criterion vectors are Fin k → ℝ (objective indices $0,\dots,k-1$ ), $Z$ is a Finset, and $k \ge 1$ is imposed as [NeZero k]. The decision set $S$ , the objectives $f_i$ and the program variable $\alpha$ are eliminated: the programs are stated over $Z$ , and $\alpha$ is replaced by its minimal value $\max_i \lambda_i(z^*_i - z_i)$ . The programs use $z^*_i - z_i$ without absolute values, as printed; on $Z$ this equals the metric's $|z^*_i - z_i|$ when $z^*$ is ideal. " $z$ minimizes the program" means that $z$ minimizes the value over $Z$ , and "uniquely minimizes" means that every other element of $Z$ has a strictly larger value. $\bar\Lambda$ is Mathlib's stdSimplex ℝ (Fin k).

The ideal vector is encoded with its full $\varepsilon$ -rule, not as " $z^* > z$ for all $z \in Z$ "; the latter would exclude the paper's case where $z^p$ touches $z^*$ in one coordinate. The minima in (3.6) and (3.8) can range over empty sets (e.g. $Z = N = \{z^p\}$ ); the paper assigns them no value, and the formalization sets $\rho_p$ , $\rho$ to $1$ then. A value of $0$ would make the goal's ⇒ direction false, so no formalization may rely on Lean's default for an empty minimum. Theorem 3.1 is stated for an arbitrary reference vector $z^*$ , since it needs no ideal-vector hypothesis. The paper's "Let $N$ be finite" in Theorem 3.7 is taken as " $Z$ finite", which is what (3.8) and the proof require.

A trivializing formalization would take $\rho = 0$ or leave $\lambda$ unconstrained; both are excluded, since $\rho$ is the specific value (3.8) and $\lambda$ ranges over $\bar\Lambda$ .

The definitions (dominance, $N$ , ideal vector, Tchebycheff values, $\Phi$ , the weights and coefficients of §3) are reusable for the continuous and polyhedral cases of the paper's §4 and for other scalarization results. Contributions of proofs of any milestone are welcome.

Selected references

R. E. Steuer and E.-U. Choo, An Interactive Weighted Tchebycheff Procedure for Multiple Objective Programming, Mathematical Programming 26 (1983) 326–344. https://doi.org/10.1007/BF02591870
W. Dinkelbach and W. Dürr, Effizienzaussagen bei Ersatzprogrammen zum Vektormaximumproblem, in: R. Henn, H. P. Künzi and H. Schubert (eds.), Operations Research Verfahren XII, Anton Hain, Meisenheim, 1972, 117–123 (reference [4] of the paper; no online version known).
V. J. Bowman, On the Relationship of the Tchebycheff Norm and the Efficient Frontier of Multiple-Criteria Objectives, Lecture Notes in Economics and Mathematical Systems, Springer (reference [1] of the paper).
E.-U. Choo and D. R. Atkins, An Interactive Algorithm for Multicriteria Programming, Computers and Operations Research 7 (1980) 81–87 (reference [3] of the paper).
S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, §4.7.4. https://web.stanford.edu/~boyd/cvxbook/

11 thms2 active usersReviewed

Completed

Linear Optimization Machine Learning Optimal Transport+2·Captain: mikedeng1

Distributionally Robust Logistic Regression II: Worst- and Best-Case Misclassification Risks over a Wasserstein Ball Are Linear ProgramsResearch Paper

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$ , and let labels take the values $y\in\{-1,+1\}$ . The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$ . A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$ ; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$ .

Metric (Definition 2). For a weight $\kappa>0$ ,

d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .

Changing a label costs $\kappa$ ; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$ , $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$ . The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$ .

Data. Training samples $(\hat x_i,\hat y_i)$ , $i=1,\dots,N$ , define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$ .

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$ .

Worst- and best-case risks.

\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$ , a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$ , $s,r,t\in\mathbb R^N$ , program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$ ,

1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$ , $\varepsilon\ge0$ , $N\ge1$ , all samples and every weight vector $\hat\beta$ , both programs attain their minima $v$ and $w$ , and

\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .

The identities hold for each fixed $\hat\beta$ , so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$ , then for any sample-dependent $\hat\beta$

\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,

\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$ . Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$ . The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$ .

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$ ; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$ , $\text{false}\mapsto-1$ ; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$ , and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$ .

The following choices differ from a literal reading of the page:

The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ . This fails on the hyperplane $\langle\beta,x\rangle=0$ , where $f_\beta(x)=-1$ is correct for $y=-1$ . The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$ , as a hypothesis, and "with probability $1-\eta$ " is read as "with probability at least $1-\eta$ ". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$ , restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

8 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Optimal Transport+1·Captain: mikedeng1

Distributionally Robust Logistic Regression I: The Worst-Case Expected Logloss over a Wasserstein Ball Is a Tractable Convex ProgramResearch Paper

Motivation

Logistic regression is among the most widely used classification methods in statistics and machine learning. Its maximum-likelihood estimator minimizes the average logloss on the training data and is known to overfit when data are scarce; practitioners respond with ad hoc regularization, typically a norm penalty on the weight vector. Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015, arXiv:1509.09259) replace the empirical average by a worst case over all distributions within a Wasserstein ball around the empirical distribution. The resulting model has a finite convex reformulation, contains classical and norm-regularized logistic regression as special cases, and comes with out-of-sample guarantees. It is one of the early instances of Wasserstein distributionally robust optimization in learning, building on the duality theory of Mohajerin Esfahani and Kuhn (Math. Program. 2018, arXiv:1505.05116); the regularization interpretation was later extended to general losses by Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (JMLR 2019, arXiv:1710.10016).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$ , and let $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$ be the dual norm of a weight vector $\beta$ . Labels are $y\in\{-1,+1\}$ , and the feature-label space is $\Xi = V\times\{-1,+1\}$ . The logloss of $\beta$ at $(x,y)$ is

l_\beta(x,y) = \log\big(1+\exp(-y\langle\beta,x\rangle)\big).

For a label weight $\kappa>0$ , the metric of Definition 2 on $\Xi$ is

d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 ,

so that changing a label costs $\kappa$ . The Wasserstein distance $W(\mathbb Q,\mathbb P)$ between probability distributions on $\Xi$ (Definition 1) is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$ , and $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$ . Given training samples $(\hat x_i,\hat y_i)_{i=1}^N$ , the empirical distribution is $\hat{\mathbb P}_N = \frac1N\sum_i\delta_{(\hat x_i,\hat y_i)}$ , and the distributionally robust logistic regression problem (6) is

\hat J = \inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)} \mathbb E^{\mathbb Q}\big[l_\beta(x,y)\big].

Program (7) has variables $\beta$ , $\lambda\in\mathbb R$ , $s\in\mathbb R^N$ , objective $\lambda\varepsilon + \frac1N\sum_i s_i$ , and constraints $l_\beta(\hat x_i,\hat y_i)\le s_i$ , $l_\beta(\hat x_i,-\hat y_i)-\lambda\kappa\le s_i$ for all $i$ , and $\|\beta\|_*\le\lambda$ .

Formalization targets

Goal: Theorem 1 (tractable reformulation)

For every $\varepsilon\ge0$ , $\kappa>0$ , $N\ge1$ and every norm on the feature space,

\inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta] \;=\; \inf\Big\{\lambda\varepsilon+\tfrac1N\textstyle\sum_i s_i : (\beta,\lambda,s)\text{ feasible for (7)}\Big\},

and for $\varepsilon>0$ the infimum of (7) is attained.

Milestones

§3.1 — the feasible set of (7) is convex.
§2 — for $\varepsilon=0$ the worst-case expected logloss is the empirical average logloss, so (6) reduces to classical logistic regression (2).
Theorem 1 for fixed $\beta$ — $\sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta]$ equals the attained minimum of (7) over $(\lambda,s)$ with $\beta$ fixed.
Remark 2, eq. (9) — at an optimal solution $(\hat\beta,\hat\lambda,\hat s)$ ,

\hat J = \hat\lambda\varepsilon + \mathbb E^{\hat{\mathbb P}_N}[l_{\hat\beta}] + \tfrac1N\textstyle\sum_i\max\{0,\hat y_i\langle\hat\beta,\hat x_i\rangle-\hat\lambda\kappa\}.

Remark 1 — as $\kappa\to\infty$ the optimal value of (7) converges to $\inf_\beta \varepsilon\|\beta\|_* + \frac1N\sum_i l_\beta(\hat x_i,\hat y_i)$ .
Theorem 2, implication — if $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$ , then $\mathbb P^N\{\mathbb E^{\mathbb P}[l_{\hat\beta}]\le\hat J\}\ge1-\eta$ .

Significance

Theorem 1 turns a minimax problem over an infinite-dimensional family of distributions into a finite convex program whose size grows linearly in $N$ ; with the $\ell_1$ , $\ell_2$ or $\ell_\infty$ norm it is a standard exponential-cone or conic program. Remark 1 explains norm-regularized logistic regression as a distributionally robust model: the regularizer is the dual norm of the transport cost on features, and the regularization weight is the radius of the ambiguity set. Remark 2 exposes an additional term that accounts for label noise and vanishes as label changes become prohibitively expensive. Theorem 2 makes the optimal value $\hat J$ a certificate on the out-of-sample logloss whenever the ball contains the true distribution.

The paper's proofs are in a technical appendix and have not been machine-checked. Mathlib contains no Wasserstein distributionally robust duality. This mission produces a formal statement of the reformulation with an arbitrary norm and a label-dependent cost, together with formal versions of the paper's printed consequences of it (Remarks 1 and 2, the $\varepsilon=0$ reduction, and the implication in Theorem 2).

Difficulty

The worst-case expectation ranges over every Borel probability distribution within transport distance $\varepsilon$ of the empirical distribution, including distributions with unbounded support and distributions that move mass across labels. Exhibiting good distributions in the ball shows only that the robust value is at least the value of (7); the reverse inequality must control every distribution in the ball at once, and nothing in the definition of the ball bounds its elements' supports. The obvious simplification, restricting attention to distributions supported on finitely many points, again yields only a one-sided bound unless the supremum is shown to be approached by such distributions. The label term of the metric couples the two label classes, so results for a pure norm cost on the features do not apply directly, and the dual norm enters through an arbitrary norm rather than the Euclidean one.

Formalization scope

The feature space is an abstract finite-dimensional real normed space V standing for $(\mathbb R^n,\|\cdot\|)$ with an arbitrary norm; weights are continuous linear functionals V →L[ℝ] ℝ, and $\|\beta\|_*$ is their operator norm, which is exactly the dual norm. Labels are Bool, embedded as $\pm1$ ; the label $-y$ is Boolean negation. The metric of Definition 2 is written literally.
The Wasserstein distance is of type 1, valued in $[0,\infty]$ , with couplings ranging over all probability measures on $\Xi\times\Xi$ with the two prescribed marginals. The ball consists of probability measures.
Expectations of the positive logloss are lower Lebesgue integrals in $[0,\infty]$ , and the supremum over the ball is taken there; the optimal value of (7) is the infimum of its (nonnegative) objective over the feasible set, also in $[0,\infty]$ . A Bochner integral, which vanishes on non-integrable functions, would make the worst case trivially finite and is not used.
The standing hypotheses are $\kappa>0$ , $\varepsilon\ge0$ , $N\ge1$ .
Correction. The paper prints "min" in (7) for all $\varepsilon\ge0$ . At $\varepsilon=0$ the minimum can fail to be attained ( $V=\mathbb R$ , $N=1$ , $\hat x_1=1$ , $\hat y_1=+1$ : the value is $0$ but every feasible point has positive objective). The goal states the value identity for $\varepsilon\ge0$ and attainment for $\varepsilon>0$ .
Remark 1 is formalized as convergence of optimal values as $\kappa\to\infty$ ; a metric with $\kappa=\infty$ is not formalized. Only convexity, not tractability, of (7) is stated. The first claim of Theorem 2 (the radius (8) and the light-tail assumption) is not formalized; the confidence of the ball event is a hypothesis of milestone 6.
A formalization in which the ball is taken only over distributions supported on the training samples, or in which the label term of the metric is dropped, trivializes the second constraint group of (7) and is ruled out: the ball here contains every Borel probability distribution on $\Xi$ within the prescribed distance.
Infrastructure needed and reusable beyond this mission: type-1 optimal transport on product spaces with a label component, couplings and their marginals, and elementary properties of the logloss as a function of $\beta$ . Contributions of such supporting lemmas as independent theorems are welcome.

Selected references

S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://arxiv.org/abs/1509.09259
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://arxiv.org/abs/1505.05116
N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://arxiv.org/abs/1312.2128
S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Regularization via Mass Transportation, Journal of Machine Learning Research 20 (2019). https://arxiv.org/abs/1710.10016

9 thms2 active usersReviewed

Completed

Combinatorics Convex Optimization Graph Theory·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization IV: Clique, Odd Hole, Odd Wheel and Odd Antihole Constraints Hold after One Round of N₊Research Paper

Motivation

The stable set problem (find a largest, or maximum-weight, set of pairwise non-adjacent nodes in a graph) is NP-hard, and its linear programming relaxations have been studied since the 1970s as a test bed for polyhedral combinatorics. Lovász and Schrijver (SIAM J. Optim. 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation to a cone of $(n+1)\times(n+1)$ matrices, impose conditions every 0–1 solution satisfies, and project back. Its semidefinite version, the operator $N_+$ , is one of the first systematic uses of positive semidefinite constraints in combinatorial optimization, and it is the ancestor of the Sherali–Adams, Lasserre and sum-of-squares hierarchies used today in approximation algorithms and proof complexity.

For the stable set problem the paper measures the strength of the operators by an index: how many rounds are needed before a given valid inequality is implied. This mission formalizes the paper's result that one round of $N_+$ already implies four of the classical families of facets of the stable set polytope.

Timeline:

1975: Chvátal shows that the rank constraint of a connected α-critical graph defines a facet of its stable set polytope (Chvátal 1975); clique, odd hole and odd antihole constraints are special rank constraints.
1981–88: Grötschel, Lovász and Schrijver show that the weighted stable set problem is solvable in polynomial time for perfect and $h$ -perfect graphs, through the theta body $\mathrm{TH}(G)$ (Grötschel, Lovász, Schrijver 1988).
1991: Lovász and Schrijver define the operators $N$ and $N_+$ and prove Corollary 2.15: clique, odd hole, odd wheel and odd antihole constraints have $N_+$ -index 1.

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$ . The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$ . Let $Q$ be the cone spanned by the 0–1 vectors with $x_0 = 1$ . For a convex cone $K \subseteq Q$ , the matrix cone $M_+(K)$ consists of the symmetric positive semidefinite matrices $Y = (y_{ij})$ with $y_{ii} = y_{0i}$ for $1 \le i \le n$ and $u^{\mathsf T}Yv \ge 0$ for all $u \in K^*$ , $v \in Q^*$ . The operator is

N_+(K) = \{Ye_0 : Y \in M_+(K)\},

and $N_+^0(K) = K$ , $N_+^t(K) = N_+(N_+^{t-1}(K))$ .

Let $G = (V, E)$ be a finite graph with no isolated nodes (the paper's standing assumption for Section 2). $\mathrm{STAB}(G)$ is the convex hull of incidence vectors $\chi^A$ of stable sets $A$ . $\mathrm{FRAC}(G)$ is the polytope given by $x_i \ge 0$ and $x_i + x_j \le 1$ for $ij \in E$ . $\mathrm{FR}(G) \subseteq \mathbb R^{V\cup\{0\}}$ is the cone $x_i \ge 0$ , $x_i + x_j \le x_0$ . The relaxations are

N_+^r(G) = \{x \in \mathbb R^V : (1, x) \in N_+^r(\mathrm{FR}(G))\},

so $N_+^0(G) = \mathrm{FRAC}(G) \supseteq N_+^1(G) \supseteq \dots \supseteq \mathrm{STAB}(G)$ . The $N_+$ -index of an inequality $a^{\mathsf T}x \le b$ valid for $\mathrm{STAB}(G)$ is the least $r$ with $a^{\mathsf T}x \le b$ valid for $N_+^r(G)$ .

The four constraint families are:

clique: $\sum_{i\in B} x_i \le 1$ for a clique $B$ ;
odd hole: $\sum_{i\in C} x_i \le \frac12(|C|-1)$ for $C$ inducing a chordless odd cycle;
odd wheel: $\sum_{i\in U\setminus\{u_0\}} x_i + \frac{|U|-2}{2}x_{u_0} \le \frac{|U|-2}{2}$ for $U$ inducing an odd wheel with center $u_0$ (an odd hole plus a node adjacent to all of it);
odd antihole: $\sum_{i\in D} x_i \le 2$ for $D$ inducing a chordless odd cycle in the complement of $G$ .

The contraction of a node $v$ turns $a^{\mathsf T}x \le b$ into the inequality with the coefficients of $v$ and its neighbours removed and right-hand side $b - a_v$ .

Formalization targets

Goal: Corollary 2.15

For every graph $G$ without isolated nodes, each clique constraint (clique of size at least 3), odd hole constraint, odd wheel constraint and odd antihole constraint has $N_+$ -index exactly 1:

a^{\mathsf T}x \le b \text{ holds on } N_+^1(G) \quad\text{and fails somewhere on } \mathrm{FRAC}(G).

Milestones

Lemma 1.5: for a closed convex cone $K \subseteq Q$ and $a$ with $a_i \le 0$ ( $i \ge 1$ ), $a_0 \ge 0$ , if $a^{\mathsf T}x \ge 0$ holds on $K \cap G_i$ (where $G_i = \{x_i = x_0\}$ ) for every $i$ with $a_i < 0$ , then it holds on $N_+(K)$ .
Lemma 2.14: if $a^{\mathsf T}x \le b$ is valid for $\mathrm{STAB}(G)$ , and the contraction of every node with positive coefficient is valid for $N_+^r(G)$ , then $a^{\mathsf T}x \le b$ is valid for $N_+^{r+1}(G)$ .
Bipartite support (Section 2.c): an inequality valid for $\mathrm{STAB}(G)$ whose nonzero-coefficient nodes induce a bipartite graph is valid for $\mathrm{FRAC}(G)$ .
Contraction property (Section 2.d): contracting a node with positive coefficient in any of the four constraints leaves positive-coefficient nodes that induce a bipartite subgraph.

Further result

Corollary 2.19 (first sentence): the $N_+$ -index of a $\mathrm{STAB}(G)$ -valid inequality $a^{\mathsf T}x \le b$ is at most the independence number of the subgraph induced by the nodes with positive coefficient.

Significance

Corollary 2.15 shows that a single round of $N_+$ , a relaxation over which one can optimize in polynomial time for each fixed number of rounds (the paper's Theorem 2.1), captures all clique, odd hole, odd wheel and odd antihole inequalities at once. Consequently $N_+(G) = \mathrm{STAB}(G)$ for every $h$ -perfect graph, in particular for perfect and $t$ -perfect graphs. The result is a standard reference point when comparing lift-and-project hierarchies, and the lemmas behind it (Lemma 1.5 and Lemma 2.14) are the paper's general tools for bounding $N_+$ -ranks.

The theorem was proved in 1991. To our knowledge it has not been machine-checked: this mission would produce the first formal development of the Lovász–Schrijver $N_+$ operator, its iterates, and the stable set relaxations $\mathrm{STAB}$ , $\mathrm{FRAC}$ , $\mathrm{FR}$ in Lean.

Difficulty

The lower bound (each constraint fails on $\mathrm{FRAC}(G)$ ) is a direct computation; the upper bound is where the work lies. The obvious approach, deriving each constraint from the linear conditions on the lifted matrix $Y$ alone, cannot succeed: those conditions define the linear operator $N$ , and the goal is specifically about what positive semidefiniteness adds. The general lemmas are stated for arbitrary cones and require a working theory of polar cones and closedness in $\mathbb R^{n+1}$ , including closedness of the iterates $N_+^r(\mathrm{FR}(G))$ , which the paper uses without comment. The graph-theoretic steps require facts about the stable set and fractional stable set polytopes of bipartite graphs and a careful case analysis of chordless odd cycles in a graph and in its complement, none of which is in Mathlib.

Formalization scope

Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι, with none the special coordinate $x_0$ . For graphs, ι := V.
$M$ is defined by condition (iii) with polar cones, not by its reformulations. Only $M_+$ , $N_+$ and their iterates are defined; the linear operator $N$ is not used.
Lemma 1.5 carries the hypothesis that $K$ is closed. The paper takes it tacitly (all its cones are polyhedral); without it the lemma fails, since $N_+(K)$ depends only on the closure of $K$ .
$\mathrm{FR}(G)$ is defined by its constraints, which agree with the paper's "cone spanned by the vectors $(1,x)$ , $x \in \mathrm{FRAC}(G)$ " because $G$ has no isolated nodes. Every graph statement carries the no-isolated-nodes hypothesis.
Contraction is written on the same graph $G$ as a zeroed coefficient vector, rather than on the subgraph $G - \Gamma(v) - v$ .
Odd holes include triangles; odd antiholes have at least 5 nodes (a 3-node "antihole" is a stable set, for which the constraint is false); odd wheels are an odd hole plus a center adjacent to all its nodes.
Clique constraints in the goal are restricted to cliques with at least 3 nodes: cliques of size 1 or 2 give inequalities already valid on $\mathrm{FRAC}(G)$ , of index 0.
" $N_+$ -index at most $r$ " is stated as validity on $N_+^r(G)$ ; the index itself is stated with IsLeast, never with an infimum that would default to 0 on an empty set.

A formalization asserting only validity on $N_+^1(G)$ , or only for one fixed graph, would be weaker than the paper's statement and is ruled out: the goal states the exact index for all graphs without isolated nodes and all four families.

Not formalized: the linear operator $N$ and its results, the polynomial-time separation results (Theorem 2.1, Corollaries 2.20–2.21), the theta-body results (Lemma 2.17, Corollary 2.18), graph indices (Corollary 2.16), and the second sentence of Corollary 2.19.

Reusable infrastructure includes the polar cone, the matrix cone $M_+$ and the $N_+$ operator (usable for any 0–1 program), the polytopes $\mathrm{STAB}$ and $\mathrm{FRAC}$ , and odd holes, antiholes and wheels as finite-set predicates. Contributions proving closedness of the iterates, the integrality of $\mathrm{FRAC}$ for bipartite graphs, or the $M$ -cone reformulations (iii′)–(iii″) are welcome.

Selected references

L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2), 1991, 166–190. https://doi.org/10.1137/0801013
M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988 (2nd ed. 1993). https://doi.org/10.1007/978-3-642-78240-4
V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory B 18, 1975, 138–154. https://doi.org/10.1016/0095-8956(75)90041-6

8 thms2 active usersReviewed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization III: The Defect of a Stable Set Inequality Bounds Its N-IndexResearch Paper

Motivation

Many 0–1 optimization problems can be written as linear programs over the convex hull of the 0–1 points of a polytope, but that hull usually has no manageable description by inequalities. Lift-and-project methods approximate it by a sequence of convex sets. Each set comes from a linear or semidefinite system in more variables, followed by a projection. Lovász and Schrijver introduced the operator $N$ in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim. 1(2), 1991). For any polytope $K$ in the unit cube, $n$ rounds of $N$ reach the 0–1 hull (their Theorem 1.4), and each round keeps linear optimization tractable.

The stable set problem is the paper's main test case, and the question is quantitative: how many rounds does a given valid inequality need? Section 2.c answers it with a single number read off a linear program. Later work on the rank of lift-and-project hierarchies uses this measure: Balas, Ceria and Cornuéjols's lift-and-project cuts (1993), the Sherali–Adams and Lasserre comparisons of Laurent (2003), and the rank lower bounds for stable set relaxations in the decades since.

Setting

Let $G = (V, E)$ be a finite graph with no isolated nodes, which is the paper's standing assumption for Section 2. For $A \subseteq V$ let $\chi^A \in \mathbb R^V$ be its incidence vector.

The stable set polytope is $\mathrm{STAB}(G) = \operatorname{conv}\{\chi^A : A \text{ stable}\}$ .
The fractional stable set polytope $\mathrm{FRAC}(G)$ is the solution set of $x_i \ge 0$ ( $i \in V$ ) and $x_i + x_j \le 1$ ( $ij \in E$ ).

Homogenize with a new coordinate $x_0$ . Let $Q \subseteq \mathbb R^{V \cup\{0\}}$ be the cone spanned by the 0–1 vectors with $x_0 = 1$ , and let $\mathrm{FR}(G)$ be the cone given by $x_i \ge 0$ and $x_i + x_j \le x_0$ . For a convex cone $K$ with polar cone $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$ , the matrix cone $M(K)$ is the set of symmetric matrices $Y$ that satisfy two conditions:

$y_{ii} = y_{0i}$ for every $i$ ;
$u^{\mathsf T} Y v \ge 0$ for all $u \in K^*$ and $v \in Q^*$ .

The operator is $N(K) = \{Y e_0 : Y \in M(K)\}$ . Its iterates are $N^0(K) = K$ and $N^t(K) = N(N^{t-1}(K))$ . On the graph side, $N^t(G) = \{x : \binom1x \in N^t(\mathrm{FR}(G))\}$ , so $N^0(G) = \mathrm{FRAC}(G)$ and $\mathrm{STAB}(G) \subseteq N^t(G)$ for every $t$ .

Let $a^{\mathsf T}x \le b$ be valid for $\mathrm{STAB}(G)$ , with $a \in \mathbb Z_+^V$ and $b \in \mathbb Z_+$ . Two numbers are attached to it:

its N-index $k$ is the least $t$ such that $a^{\mathsf T}x \le b$ is valid for $N^t(G)$ ;
its defect is $r = 2\max\{a^{\mathsf T}x - b : x \in \mathrm{FRAC}(G)\}$ , which is an integer.

For a node $v$ with neighbourhood $\Gamma(v)$ , the deletion of $v$ zeroes $a_v$ . The contraction of $v$ zeroes $a$ on $\{v\}\cup\Gamma(v)$ and lowers the right-hand side to $b - a_v$ .

Formalization targets

Goal: Theorem 2.13

For every such inequality with defect $r \ge 0$ and N-index $k$ ,

\frac{r}{b} \;\le\; k \;\le\; r,

formalized as $r \le k\,b$ and $k \le r$ . The goal holds for every graph without isolated nodes and every valid inequality with nonnegative integer coefficients and nonnegative defect.

Milestones

Lemma 2.11. Let $a \ge 0$ and $\max_{\mathrm{STAB}} a^{\mathsf T}x < \max_{\mathrm{FRAC}} a^{\mathsf T}x$ . Then the edges $ij$ with $y_i + y_j = 1$ at every FRAC-maximizer $y$ form a nonbipartite graph.
Lemma 2.12. Under the same hypothesis, some node $i$ has $y_i = \tfrac12$ at every FRAC-maximizer $y$ .
The defect-decrease claim (proof of Theorem 2.13). For such a node $i$ , the deletion and the contraction of $i$ both have defect smaller than $r$ .
Lemma 2.2. If the deletion and the contraction of some node are valid for $K$ , where $K \subseteq \mathrm{FR}(G)$ is a closed convex cone, then $a^{\mathsf T}x \le b$ is valid for $N(K)$ .
Lemma 2.7. $\frac{1}{k+2}\mathbb 1 \in N^k(G)$ for every $k \ge 0$ .

Further result

Corollary 2.8. Let $G$ have $n$ nodes, stability number $\alpha$ and graph N-index $k$ . Then

\frac n\alpha - 2 \le k \le n - \alpha - 1.

Significance

Theorem 2.13 turns the N-index, which is defined through an infinite family of matrix-cone projections, into a quantity computable by one linear program over $\mathrm{FRAC}(G)$ . Some consequences:

Odd hole constraints have defect 1 and hence N-index 1.
An odd antihole on $2k+1$ nodes has index exactly $k$ ; the paper notes that the lower bound is tight for odd antihole constraints.
Inequalities of large defect relative to their right-hand side need many rounds. With Lemma 2.7 this yields Corollary 2.8 and the unboundedness of the N-index of line graphs, the stable set side of Yannakakis's matching-polytope question.

The result is proved in the paper; the mission's work is to formalize it. Nothing on Prove2Me or in Mathlib covers stable set polytopes, the Lovász–Schrijver operator or its index, and no machine-checked version of Theorem 2.13 is known. A formal proof would give the first verified rank bound for a lift-and-project hierarchy. It would also build a reusable library for $\mathrm{STAB}$ , $\mathrm{FRAC}$ , half-integrality of $\mathrm{FRAC}$ vertices, and the $N$ operator.

Difficulty

The upper bound is an induction on the defect, and it needs several facts about $\mathrm{FRAC}(G)$ :

its vertices are half-integral;
the defect is therefore an integer;
a node $\tfrac12$ at every optimum exists, which is a statement about the whole optimal face and not about one optimal vertex.

The last is the heart of Lemmas 2.11 and 2.12. The induction also climbs through $N^t(\mathrm{FR}(G))$ for every $t$ , so Lemma 2.2 must hold for an arbitrary closed convex cone inside $\mathrm{FR}(G)$ , not only for polytopes given by inequalities.

The lower bound is where the obvious argument fails. The printed proof tests $a^{\mathsf T}x \le b$ at $\frac1{k+2}\mathbb 1$ and obtains $k \ge a^{\mathsf T}\mathbb 1/b - 2$ . That equals $r/b$ only when $r = a^{\mathsf T}\mathbb 1 - 2b$ , which Lemma 2.10 gives for facets alone. For a general valid inequality $r$ can exceed $a^{\mathsf T}\mathbb 1 - 2b$ , so the uniform vector does not suffice. The theorem is stated, as printed, for every valid inequality, and a complete proof must supply the missing step.

Formalization scope

Coordinates of $\mathbb R^{V\cup\{0\}}$ are indexed by Option V, with none as $x_0$ . Graphs are finite SimpleGraphs with the hypothesis that every node has a neighbour.
$\mathrm{FR}(G)$ is defined by its two constraint families. This equals the cone over $\mathrm{FRAC}(G)$ because there are no isolated nodes.
$M$ is defined by condition (iii) itself.
The defect and the N-index are never suprema or infima. They are values $r$ , $k$ with IsGreatest and IsLeast hypotheses, so no default value such as $\sup\emptyset = 0$ can make a statement vacuous.
Coefficients are natural numbers cast to $\mathbb R$ . Lemmas 2.11–2.12 take real $a \ge 0$ , as printed.
Deletion and contraction are zero-extended coefficient vectors on the same graph $G$ , with defects taken over $\mathrm{FRAC}(G)$ . Subgraphs with isolated nodes never arise.
The goal adds the hypothesis $r \ge 0$ . Without it the upper bound is false: for $x_1 \le 2$ on one edge, $r = -2$ but $k = 0$ . The paper's proof presumes it.
The lower bound is stated as $r \le kb$ , which avoids Lean's $r/0 = 0$ convention.
Lemma 2.2 is stated for a closed convex cone $K \subseteq \mathrm{FR}(G)$ . The paper tacitly takes $K$ closed, and the Section 1 lemma it rests on is false for non-closed cones. Its hypothesis " $K$ contains $\mathrm{STAB}(G)$ " is dropped, which makes the lemma stronger.
Corollary 2.8 uses the least $k$ with $N^k(G) = \mathrm{STAB}(G)$ . This is equivalent to the paper's "largest N-index of a facet" and avoids a facet notion.
The goal is the two-sided bound for all graphs and inequalities. A version for one fixed graph, a version with a facet hypothesis, or "valid for $N^r(G)$ " alone would each be a different, weaker theorem.
Not formalized: Lemma 2.10 (facets), Corollaries 2.6 and 2.9 (graph index via facets), and the polynomial-time results.

The work needs half-integrality of $\mathrm{FRAC}(G)$ , Lemma 1.3 of the paper ( $N(K) \subseteq (K\cap H_i) + (K \cap G_i)$ ) and monotonicity of $N$ . Each of these is reusable and welcome as a separate contribution.

Selected references

L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
E. Balas, S. Ceria, G. Cornuéjols, A lift-and-project cutting plane algorithm for mixed 0–1 programs, Mathematical Programming 58 (1993) 295–324. https://doi.org/10.1007/BF01581273
M. Laurent, A comparison of the Sherali–Adams, Lovász–Schrijver, and Lasserre relaxations for 0–1 programming, Mathematics of Operations Research 28(3) (2003) 470–496. https://doi.org/10.1287/moor.28.3.470.16391
M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43 (1991) 441–466. https://doi.org/10.1016/0022-0000(91)90024-Y

10 thms2 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems IV: Greedy Set Cover C1 Has Worst-Case Ratio H(k) on SC(k)Research Paper

Motivation

Set covering asks for the fewest members of a family of sets whose union is everything the family covers. It models crew scheduling, facility siting, test-suite reduction, logic minimization and fault testing; Johnson names the last two as its practical applications. Karp showed in 1972 that the decision version is NP-complete (Karp 1972), so in practice one runs a heuristic and asks how far from optimal it can be.

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (JCSS 9, 256–278) is one of the founding papers of the worst-case analysis of approximation algorithms. For set covering it analyses the obvious greedy rule, repeatedly take a set that covers the most still-uncovered points, and proves that on families whose sets have at most $k$ elements its output is never more than the harmonic number $H(k) = \sum_{j=1}^k 1/j$ times the optimum, and that this factor is attained.

Timeline.

1974: Johnson proves the $H(k)$ bound for unweighted set cover with sets of size at most $k$ , together with a matching family of examples (this mission).
1975: Lovász proves the same bound for the fractional relaxation, giving an integrality-gap statement (Lovász 1975).
1979: Chvátal extends the bound to weighted set cover, with the greedy rule choosing the set of least cost per newly covered point (Chvátal 1979).
1998: Feige shows that no polynomial-time algorithm achieves $(1-\varepsilon)\ln n$ unless NP has slightly superpolynomial deterministic algorithms (Feige 1998), so the greedy guarantee is essentially the best possible.

Setting

An input $F$ of SET COVERING I is a finite family $\{S_1, \dots, S_p\}$ of finite sets. The set to be covered is $T = \bigcup_{S \in F} S$ . A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S \in F'} S = T$ , and its measure is $|F'|$ . The optimum $F^*$ is the minimum measure of a subcover; $F$ itself is a subcover, so the minimum exists. The subproblem SC(k) restricts the inputs to families no set of which has more than $k$ elements.

Algorithm C1 keeps a family SUB of chosen sets, the set UNCOV of uncovered points, and an array SET $[i]$ holding the still-uncovered part of $S_i$ . It starts with SUB $= \emptyset$ , UNCOV $= T$ , SET $[i] = S_i$ . While UNCOV is nonempty it chooses an index $j$ with $|\mathrm{SET}[j]|$ maximal, adds $S_j$ to SUB, and removes SET $[j]$ from UNCOV and from every SET $[i]$ . When UNCOV is empty it returns SUB. When several indices tie at Step 3 any of them may be chosen, so one input can have several choosable outputs. Following Section 2 of the paper, the algorithm's value $C1(F)$ is the worst choosable output, here the largest, and the ratio is $r(C1, F) = C1(F)/F^*$ .

For the proof the paper introduces configurations $K = \langle N_K, \mathrm{UNCOV}_K, \langle \mathrm{SET}_K[1], \dots, \mathrm{SET}_K[N_K]\rangle\rangle$ with $\bigcup_i \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$ , runs from a configuration (sequences of admissible choices ending when UNCOV is empty), $\mathrm{Numbers}(R)$ , the set of indices chosen in a run $R$ , and calls a set $M$ selectable from $K$ if $M = \mathrm{Numbers}(R)$ for some run $R$ from $K$ . Write $n(K, i) = |\mathrm{SET}_K[i]|$ .

Formalization targets

Goal: Theorem 4

For every $k \ge 1$ :

\text{for every input } F \in SC(k) \text{ and every choosable } F_1:\quad |F_1| \le H(k)\cdot F^*,

\text{and some } F \in SC(k) \text{ with } F^* > 0 \text{ has a choosable } F_1 \text{ with } |F_1| = H(k)\cdot F^*.

The paper states this as $R[C1, SC(k)](n) \le \sum_{j=1}^k (1/j)$ for all $n > 0$ , with equality for all sufficiently large $n$ . The two-part form above is the size-free equivalent.

Milestones

Lemma 1. For a subcover $F_1$ with index set $M1 = \{i : S_i \in F_1\}$ and $K$ the configuration after Step 1: $F_1$ is choosable by C1 if and only if $M1$ is selectable from $K$ .
Lemma 2. For any configuration $K$ , any $M1$ selectable from $K$ and any $M0$ with $\bigcup_{i \in M0} \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$ :

|M1| \le \sum_{i \in M0} \sum_{j=1}^{n(K,i)} \frac{1}{j}.

Fig. 1. For every $k \ge 1$ there is an explicit input of $SC(k)$ on $k \cdot k!$ points with $F^* = k!$ and a choosable output of $k!\,H(k)$ sets.

Significance

The result. Theorem 4 is the first proof that greedy set cover has a worst-case guarantee depending only on the largest set size, and it pins the guarantee down exactly: the constant $H(k)$ cannot be lowered for any $k$ . Since $H(k) \le 1 + \ln k$ , it also gives the well-known $1 + \ln n$ bound for general inputs. The $H(k)$ bound and its later refinements are the standard reference point for analyses of greedy covering, dual fitting and submodular covering.

Formalizing it. The theorem has been proved since 1974. As far as a search of the platform shows, no machine-checked proof of it exists: the platform holds a Kearns–Vazirani-style statement ComputationalLearning.greedy_set_cover (the $\mathrm{opt}\cdot\ln|U|$ form for a greedy sequence, still open) and a dual-fitting certificate lemma for weighted set cover, neither of which covers the $SC(k)$ bound, the tie-breaking semantics or the tightness construction. A complete development provides both halves of Theorem 4, the configuration and run machinery of Lemmas 1–2, and the explicit Fig. 1 family.

Difficulty

The obvious argument charges each chosen set to the points it newly covers and compares the charges with an optimal cover. A statement about the initial input alone, with the original sizes of the optimal sets, does not survive a single greedy step: after a step the optimal sets are only partly uncovered and the remaining run faces a different instance. This is why Lemma 2 is stated for an arbitrary configuration, in terms of the current sizes $n(K, i)$ , and for an arbitrary covering subfamily $M0$ . Because Step 3 breaks ties arbitrarily, the statement must hold for every admissible run, and a formalization that fixes one tie-breaking rule proves a weaker upper bound and cannot express the tightness example, which relies on adversarial ties at every stage.

For the tightness half, the difficulty is bookkeeping: showing that the $k!/j$ blocks of each segment are admissible choices at each stage and that no cover uses fewer than $k!$ sets.

Formalization scope

An input is an indexed family S : ι → Finset α over a finite index type ι and a ground type with decidable equality. The indices play the role of $1, \dots, N$ ; two indices may carry the same set, which only widens the input class. The family, subcovers and $F^*$ are taken over the set of sets family S, as on the page. $F^*$ is a Finset.inf' over the nonempty finite set of subcovers; if $T = \emptyset$ then $F^* = 0$ .
C1 is a nondeterministic step relation: a step is allowed for every index maximizing $|\mathrm{SET}[j]|$ . An output is choosable if a finite chain of steps from the initial state reaches a halting state with that SUB. No tie-breaking rule is fixed.
The paper's $R[A, P](n)$ is a maximum over inputs of size at most $n$ in an unspecified notation; it is replaced by the size-free two-part statement above, which is equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$ .
Ratios are stated multiplicatively in $\mathbb{Q}$ ( $|F_1| \le H(k)\cdot F^*$ ), never as a quotient, so an input with $F^* = 0$ does not make the bound vacuous, and the attainment part requires $F^* > 0$ . $H(k)$ is Mathlib's harmonic k.
Configurations carry the covering condition as a field; runs are an inductive predicate on the list of chosen indices; Selectable K M means $M$ is the set of indices of some run.
Lemma 1 assumes the family's sets are pairwise distinct (the paper's family is a set of sets); without that the index set $\{i : S_i \in F_1\}$ may contain a duplicate index C1 never chose.
Trivializing formalizations are ruled out: a deterministic tie-break, a ratio written as a division, the original set sizes in place of $n(K, i)$ in Lemma 2, or an attaining input with $F^* = 0$ would each change the theorem.

Contributions welcome: proofs of Lemma 2 (the core induction), of Lemma 1, of the Fig. 1 run, and of Theorem 4 from these; the configuration/run layer and the Fig. 1 family are reusable for other greedy covering analyses.

Selected references

David S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
Richard M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
László Lovász, On the ratio of optimal integral and fractional covers, Discrete Mathematics 13 (1975), 383–390. https://doi.org/10.1016/0012-365X(75)90058-8
Vašek Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233
Uriel Feige, A threshold of ln n for approximating set cover, Journal of the ACM 45 (1998), 634–652. https://doi.org/10.1145/285055.285059

8 thms2 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems II: The Greedy Literal Algorithm B1 Has Worst-Case Ratio (k+1)/k on MS(k)Research Paper

Motivation

Maximum satisfiability asks for a truth assignment satisfying as many clauses of a propositional formula as possible. The paper notes that the restriction $MS(k)$ , in which every clause has at least $k$ literals, is polynomial complete for every $k \ge 1$ , so exact optimization is out of reach in general and one asks instead how close a fast algorithm is guaranteed to come. David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 256–278) set up a framework for exactly this question — optimization problems, nondeterministic approximation algorithms, and the worst-case ratio between the optimum and the algorithm's output — and applied it to subset-sum, maximum satisfiability, set covering, graph coloring and maximum clique. It is one of the founding papers of the theory of approximation algorithms.

Section 4 of the paper treats maximum satisfiability with two algorithms. This mission covers the first, a greedy literal-selection rule called B1, and its exact worst-case ratio (Theorem 2). A companion mission covers the weighted algorithm B2 (Theorem 3).

Timeline, for orientation:

1971–1972: Cook and Karp establish NP-completeness of satisfiability and of many combinatorial problems.
1974: Johnson proves that B1 has worst-case ratio exactly $(k+1)/k$ on $MS(k)$ and that the weighted algorithm B2 achieves $2^k/(2^k-1)$ (Theorems 2 and 3).
1990s: semidefinite and LP-based algorithms (Goemans–Williamson, SIAM J. Discrete Math. 1994) improve the constants for general MAX-SAT.

Setting

Let $L = \bigcup_{i>0}\{x_i, \bar x_i\}$ be the set of literals; the complement of $x_i$ is $\bar x_i$ and conversely. A clause is a finite set $C \subseteq L$ . A truth assignment is a set $T \subseteq L$ containing no complementary pair $\{x_i, \bar x_i\}$ ; it may leave variables unassigned. $T$ satisfies $C$ if $C \cap T \ne \emptyset$ .

An input is a finite set $S$ of clauses. Its feasible solutions are the subsets $S' \subseteq S$ satisfied by a single truth assignment, measured by $|S'|$ , and the optimum is

S^* = \max\{|S'| : S' \subseteq S,\ \text{some truth assignment satisfies every } C \in S'\}.

The subproblem $MS(k)$ admits only inputs whose clauses each contain at least $k$ distinct literals.

Algorithm B1 keeps four variables: SUB (clauses already satisfied), LEFT (clauses not yet satisfied), TRUE (literals made true) and LIT (literals still available). It starts with SUB $=$ TRUE $= \emptyset$ , LEFT $= S$ , LIT $= L$ . While some literal of LIT occurs in a clause of LEFT, it picks a literal $y \in$ LIT contained in the most clauses of LEFT, moves those clauses $YT$ from LEFT to SUB, adds $y$ to TRUE, and removes $y$ and $\bar y$ from LIT. When no literal of LIT occurs in LEFT it returns SUB.

The choice of $y$ is not determined when several literals tie. Following the paper's framework, every output reachable by some sequence of admissible choices is choosable, and the performance of B1 on $S$ is the smallest $|X|$ over choosable outputs $X$ . The worst-case ratio on inputs of size at most $n$ is

R[B1, MS(k)](n) = \max\{S^*/B1(S) : S \in MS(k),\ |S| \le n\}.

Formalization targets

Goal: Theorem 2 (p. 262)

For all $k \ge 1$ ,

R[B1, MS(k)](n) \le \frac{k+1}{k}\quad\text{for all } n > 0,

with equality for all sufficiently large $n$ . In the size-free form used here: every choosable output $X$ on every $S \in MS(k)$ satisfies $k\,S^* \le (k+1)\,|X|$ , and for every $k \ge 1$ some $S \in MS(k)$ has a choosable $X$ with $|X| > 0$ and $k\,S^* = (k+1)\,|X|$ .

Milestones (from the proof of Theorem 2, pp. 262–263)

In each iteration, the number of clauses saved (added to SUB) is at least the number of clauses remaining in LEFT that are wounded (lose a literal from LIT without being satisfied).
When B1 halts, every clause left in LEFT is dead: each of its literals has had its complement made true.
When B1 halts on an input of $MS(k)$ , $|\mathrm{SUB}| \ge k\,|\mathrm{LEFT}|$ , and SUB and LEFT partition $S$ .
On the four-clause input $\{\{x_1,x_2,x_3\},\{\bar x_1,x_4,x_5\},\{\bar x_2,x_6,x_7\},\{\bar x_3,x_8,x_9\}\}$ of $MS(3)$ , $S^* = 4$ while B1 may return three clauses.

Significance

The bound is stronger than a ratio: milestone 3 shows that B1 always satisfies at least $\tfrac{k}{k+1}|S|$ clauses, whatever the optimum. The tightness half shows that this simple greedy rule cannot be analysed any better, which is what motivated the weighted algorithm B2 of the same section, with ratio $2^k/(2^k-1)$ . The pair of theorems is an early instance of a now standard pattern: a potential-style counting argument for an upper bound, and an adversarial tie-breaking instance for the matching lower bound.

The result is proved in the paper; it has not, to our knowledge, been machine-checked. This mission produces a formal model of Johnson's framework for a maximization problem with a nondeterministic algorithm, a formal proof of the upper bound through the "saved versus wounded" accounting, and explicit tightness instances for every $k \ge 1$ . The paper spells out only $k = 3$ and states that "similar examples can be constructed for any other $k > 0$ "; the formal goal requires them for all $k$ .

Difficulty

The upper bound needs an invariant over entire runs, not over a single step: a clause wounded in one iteration may be saved in a later one, so wounds and saves must be tallied globally, and the count of wounds received by a clause that ends in LEFT must be matched with its number of literals. That matching relies on the facts that B1 never makes both a literal and its complement true and that a clause containing a true literal has already left LEFT. Clauses containing both $x_i$ and $\bar x_i$ are allowed and have to be handled.

The lower bound cannot be obtained from a fixed tie-breaking rule: the attaining run chooses negative literals whose count merely ties the maximum. For general $k$ the instance has to be built so that every literal occurs in few enough clauses that the adversarial choice is admissible at every step; at $k = 1$ the paper's pattern degenerates and needs adjusting.

Formalization scope

A literal is a pair (variable index in $\mathbb N$ , sign); a clause is a Finset of literals; an input is a Finset of clauses, so duplicate clauses are not allowed, as on the page. Tautological clauses are allowed.
A truth assignment is a Set of literals without a complementary pair (partial, as in the paper). $S^*$ is the maximum of $|S'|$ over the finite nonempty family of satisfiable subsets, taken with Finset.sup'.
B1 is a nondeterministic run relation: a state holds SUB, LEFT, TRUE and the set of decided variables (LIT is its complement, since $L$ is infinite); one step chooses any literal of LIT, of either sign, with maximum count; "choosable" is reachability of a halting state with the given SUB. No tie-break is fixed. A formalization that picks a variable and then its better sign, or that resolves ties deterministically, is a different algorithm and would make the tightness half false.
The ratio $R[B1, MS(k)](n)$ , whose problem size is left unspecified in the paper, is replaced by its size-free equivalent, and ratios are written multiplicatively in $\mathbb N$ : $k\,S^* \le (k+1)|X|$ . The tightness half requires $|X| > 0$ , so the empty input cannot witness it.
The running time $O(n \log n)$ is not stated.

Welcome contributions: proofs of the milestones, the invariants of reachable B1 states (SUB and LEFT partition $S$ ; TRUE is consistent and exactly covers the decided variables; no clause of LEFT meets TRUE), and the family of tightness instances for general $k$ . The run-relation encoding of choosable outputs is reusable for the other algorithms of the paper.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
M. X. Goemans and D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM Journal on Discrete Mathematics 7 (1994), 656–666. https://doi.org/10.1137/S0895480192243516

8 thms2 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems I: The Subset-Sum Algorithms A_k Have Worst-Case Ratio (k+1)/kResearch Paper

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.

Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity $b$ so as to fill it as much as possible. For this problem the paper gives a family of algorithms $A_k$ , one for each $k \ge 1$ , whose guaranteed ratio $(k+1)/k$ tends to $1$ . It is one of the first examples of what is now called a polynomial-time approximation scheme: for every $\epsilon > 0$ there is a polynomial-time algorithm within a factor $1 + \epsilon$ of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.

This mission formalizes Theorem 1 of the paper, the performance guarantee of $A_k$ together with its tightness.

Setting

An input $\langle T, s, b\rangle$ of SUBSET-SUM is a finite set $T$ , a positive rational size $s(x)$ for every $x \in T$ , and a positive rational bound $b$ . An approximate solution is a subset $T' \subseteq T$ with $m(T') \le b$ , where the measure is $m(T') = \sum_{x \in T'} s(x)$ . The problem is a maximization problem with optimal measure

\langle T, s, b\rangle^* = \max\{\, m(T') : T' \subseteq T,\ m(T') \le b \,\}.

Fix $k \ge 1$ and call $x$ big if $s(x) > b/(k+1)$ and small otherwise. Algorithm $A_k$ keeps a set $\mathrm{SUB}$ , its measure $\mathrm{SUM}$ , and the remaining elements $\mathrm{LEFT}$ :

$\mathrm{SUB}$ is a subset of the big elements whose measure is as large as possible without exceeding $b$ ; $\mathrm{SUM} = m(\mathrm{SUB})$ and $\mathrm{LEFT} = T \setminus \mathrm{SUB}$ .
If $s(x) + \mathrm{SUM} > b$ for every $x \in \mathrm{LEFT}$ , return $\mathrm{SUB}$ .
Otherwise pick $y \in \mathrm{LEFT}$ with $s(y) + \mathrm{SUM}$ as large as possible without exceeding $b$ , move it from $\mathrm{LEFT}$ to $\mathrm{SUB}$ , add $s(y)$ to $\mathrm{SUM}$ , and return to step 2.

Steps 1 and 3 may have ties. Following the paper, a set $T_1$ is choosable by $A_k$ if some resolution of all ties produces it, and the performance $A_k(u)$ on input $u$ is the smallest measure of a choosable output. The ratio is $r(A_k, u) = u^*/A_k(u) \ge 1$ , and $R[A_k](n)$ is its maximum over inputs of size at most $n$ .

Formalization targets

Goal: Theorem 1 (p. 260)

For $k \ge 1$ and $n > 0$ ,

R[A_k](n) \le \frac{k+1}{k}, \qquad \lim_{n \to \infty} R[A_k](n) = \frac{k+1}{k}.

Formally, for every $k \ge 1$ : every choosable output $T_1$ of every input satisfies $k\,\langle T,s,b\rangle^* \le (k+1)\,m(T_1)$ ; and for every $\delta > 0$ some input has a choosable output $T_1$ with $m(T_1) > 0$ and $\langle T,s,b\rangle^* > \big(\tfrac{k+1}{k} - \delta\big)\,m(T_1)$ .

Milestones

For $T_1$ choosable and $T_0$ any approximate solution, $m(T_1^{\mathrm{BIG}}) \ge m(T_0^{\mathrm{BIG}})$ (p. 260).
If a small $x \in T$ is not in a choosable $T_1$ , then $s(x) + m(T_1) > b$ , hence $m(T_1) > kb/(k+1) \ge \tfrac{k}{k+1}\langle T,s,b\rangle^*$ (p. 261).
The stronger dichotomy: $m(T_1) = \langle T,s,b\rangle^*$ or $m(T_1) \ge \tfrac{k}{k+1}\,b$ (p. 260).
The lower-bound input $T = \{a_1,\dots,a_{k+2}\}$ , $s(a_1) = 1+\varepsilon$ , $s(a_i) = 1$ otherwise, $b = k+1$ : its optimum is $k+1$ , some output is choosable, and every choosable output has measure $k + \varepsilon$ (p. 261).

Significance

Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above $1$ , in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms $A_k$ are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of $A_k$ itself cannot be sharpened.

The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly $(k+1)/k$ . The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.

Difficulty

The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing $A_k$ as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as $\mathrm{SUM}$ always equalling $m(\mathrm{SUB})$ or which elements can enter $\mathrm{SUB}$ after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general $k$ : exactly $k-1$ unit elements are added after $a_1$ , and this must be shown for every choosable run, not only for one.

Formalization scope

Numbers. Sizes and the bound are rationals (ℚ), as in the paper; sizes are required to be positive on $T$ and $b > 0$ . The index $k$ is a natural number with $1 \le k$ as a hypothesis; $b/(k+1)$ is rational division, and "big" is the strict inequality $s(x) > b/(k+1)$ .
Optimum. opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains $\emptyset$ ; it is $0$ when no element fits.
Run relation. Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning $T_1$ . Every "closest to, without exceeding" is an existential choice among all maximizers.
Size-free restatement. The paper's input size $|u|$ ("in some standard notation") is never fixed, so the goal quantifies over all inputs instead of over sizes. The upper bound for all choosable outputs is equivalent to $R[A_k](n) \le (k+1)/k$ for all $n$ ; since $R[A_k]$ is nondecreasing, the limit claim is equivalent to the supremum of the ratio over all inputs being $(k+1)/k$ , which is the second part.
Multiplicative ratios. No ratio is written as a division, so an output of measure $0$ cannot satisfy a bound vacuously; the lower-bound part requires $m(T_1) > 0$ . The value $(k+1)/k$ is not claimed to be attained: the paper's family has ratio $(k+1)/(k+\varepsilon)$ .
Lower-bound input. A def on Fin (k + 2) exactly as on the page, with $0 < \varepsilon < 1$ (the page leaves the range implicit; $\varepsilon < 1$ keeps $a_1$ the only big element that fits when $k = 1$ ).
Ruled out. A formalization with a deterministic tie-break, with a bound of the form $\mathrm{opt}/m \le c$ in a field where $x/0 = 0$ , or with tightness for a single fixed $k$ would be trivial or weaker; none of these is the target.

Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ( $O(n^k)$ for step 1) and Sahni's knapsack extension are not part of the mission.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
S. Sahni, Approximate algorithms for the 0/1 knapsack problem, Journal of the ACM 22 (1975) 115–124. https://doi.org/10.1145/321864.321873
O. H. Ibarra, C. E. Kim, Fast approximation algorithms for the knapsack and sum of subset problems, Journal of the ACM 22 (1975) 463–468. https://doi.org/10.1145/321906.321909
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9

8 thms2 active usersReviewed

Markov Chain Stochastic Systems·Captain: mikedeng1

Jobshop-Like Queueing Systems: The Equilibrium Distribution with State-Dependent Arrival and Service RatesResearch Paper

Motivation

A jobshop is a factory in which each job visits a sequence of machine groups, the sequence differing from job to job. J. R. Jackson's 1963 paper Jobshop-Like Queueing Systems (Management Science 10(1), 131–142) models such a shop as a network of queues and computes its long-run distribution of queue lengths in closed form. It generalizes his 1957 paper Networks of Waiting Lines (Operations Research 5(4)), which treated Poisson arrivals and multi-server centers, to arrival rates that depend on the total number of customers present and service rates that depend arbitrarily on the local queue length. The resulting product-form equilibrium is the starting point of queueing-network theory, which is used in performance analysis of manufacturing systems, computer systems and communication networks.

Timeline:

1957: Jackson, Networks of Waiting Lines, constant external Poisson arrivals and multi-channel exponential servers; product-form equilibrium.
1963: Jackson, this paper: state-dependent total arrival rate $\lambda(S(\bar k))$ , queue-length-dependent service rates $\mu(n, k)$ , routings with self-loops and empty routings; Theorem (4.5).
1967: Gordon and Newell, Closed Queuing Systems with Exponential Servers, the closed-network analogue.
1979: Kelly, Reversibility and Stochastic Networks, the general theory of migration processes and partial balance.

Setting

There are $N \ge 1$ service centers, Center $1, \dots, N$ . A state vector $\bar k = (k_1, \dots, k_N)$ has non-negative integer components, $k_n$ being the number of customers at Center $n$ , and $S(\bar k) = k_1 + \dots + k_N$ . The system $(N, L, M, R)$ is given by:

arrival rates $\lambda(K)$ , $K = 0, 1, 2, \dots$ : in state $\bar k$ a customer arrives at rate $\lambda(S(\bar k))$ ;
service rates $\mu(n, k)$ : a service at Center $n$ completes at rate $\mu(n, k_n)$ ;
routing probabilities $r(m, n)$ , $m \in [0, N]$ , $n \in [1, N+1]$ : an arriving customer's first center is $n$ with probability $r(0, n)$ , its routing is empty with probability $r(0, N+1)$ ; after service at Center $m$ it moves to Center $n$ with probability $r(m, n)$ (possibly $n = m$ ) or leaves with probability $r(m, N+1)$ .

The paper's standing Assumptions (2.1)–(2.4): (2.1) either all $\lambda(K) > 0$ , or $\lambda(K) > 0$ exactly for $K \le K_0$ ; (2.2) $\mu(n, 0) = 0$ and $\mu(n, k) > 0$ for $k \ge 1$ ; (2.3) each row $\{r(m, n)\}_{n \in [1, N+1]}$ is a probability distribution; (2.4) the traffic equations

e(n) = r(0, n) + \sum_{m=1}^N e(m)\, r(m, n), \qquad n \in [1, N], \tag{2.5}

have a unique solution, and it is non-negative.

The process is defined by its transition probabilities over a short interval (p. 134), from which the paper derives the balance equations (3.1) for $P(\bar k, t)$ . An equilibrium state probability distribution is a probability distribution $p$ on state vectors such that $P(\bar k, t) \equiv p(\bar k)$ solves (3.1). With

W(K) = \prod_{i=0}^{K-1}\lambda(i), \quad w(\bar k) = \prod_{n=1}^N\prod_{i=1}^{k_n}\frac{e(n)}{\mu(n, i)}, \quad T(K) = \sum_{S(\bar k) = K} w(\bar k),

the constant $\pi$ is $\{\sum_{K \ge 0} W(K) T(K)\}^{-1}$ when the series converges and $0$ otherwise.

Formalization targets

Goal: Theorem (4.5)

If $\pi > 0$ , then

p(\bar k) = \pi\, w(\bar k)\, W(S(\bar k)) \tag{4.6}

is an equilibrium state probability distribution; and if the arrival rates are bounded, it is the only one. The goal fixes no constants; the condition $\pi > 0$ is the paper's.

Milestones

The series in (4.4) converges to a positive number or diverges to $+\infty$ (§4, p. 136).
If $\pi > 0$ , (4.6) is a probability distribution (first claim of the proof sentence, p. 136).
(4.6) satisfies equations (3.1) at every state (second claim, p. 136).
Under bounded arrival rates, an equilibrium distribution is unique (§4, p. 135).

Companion

Theorem (6.3) in its case $K^* = 0$ , $k_n^* = +\infty$ : with constant arrival rate $\lambda(K) \equiv \lambda(0)$ and $p_n(0) > 0$ for every $n$ , the equilibrium is $p(\bar k) = \prod_n p_n(k_n)$ , $p_n$ being the normalized $w_n(k) = \prod_{i=1}^k \lambda(0)e(n)/\mu(n, i)$ .

Significance

Theorem (4.5) states that the queue lengths of a whole network have an explicit stationary law, determined by the routing only through the visit ratios $e(n)$ , and that conditionally on the total $S(\bar k) = K$ it does not depend on the arrival process. With constant arrival rate it factorizes into independent one-center laws (Theorem (6.3)), each that of a single queue fed at rate $\lambda(0)e(n)$ ; this is the form in which Jackson networks enter textbooks. State-dependent arrivals cover systems with balking or finite capacity: taking $\lambda(K) = 0$ for $K > K_0$ caps the population.

The result is classical and proved; it has no machine-checked proof on this platform. The platform has Kelly–Yudovina's open migration process (KellyStochasticNetworks.open_migration_equilibrium): constant external arrivals, no self-loops, a full-balance conclusion without uniqueness. It is the companion (6.3) in substance but not the general theorem: arrival rates depending on the total population are not in it. This mission contributes the state-dependent model, a stationary form of Jackson's own equations (3.1), and a uniqueness statement.

Difficulty

The balance equations are an infinite system in $\mathbb{Z}_{\ge 0}^N$ . Substituting (4.6) gives terms with shifted states, guarded by non-negativity of components, a double sum over ordered pairs of distinct centers, self-loops appearing only in the outflow factor $1 - r(n, n)$ , and centers with $e(n) = 0$ , where $w$ vanishes. Checking each state term by term against the traffic equations requires the diagonal of (2.5), excluded in (3.1), to be handled exactly. Summing (4.6) to one requires regrouping a series over $\mathbb{Z}_{\ge 0}^N$ by the finite fibres of $S$ .

Uniqueness is the hard part. The paper gives no proof: footnote 5 refers to a limit theorem for Markov processes and to the communication structure of non-transient states. A solution of the algebraic balance equations need not be the stationary law of the process when the process can explode, and the model allows explosion with $\pi > 0$ (e.g. $N = 1$ , $\lambda(K) = 4^K$ , $\mu(1,k) = 2\cdot 4^{k-1}$ ). Uniqueness therefore depends on non-explosion as well as on the communication structure of the states, and neither is addressed on the page.

Formalization scope

Centers are Fin N with $N > 0$ ; states are Fin N → ℕ; rates are real. The routing is one function r : Option (Fin N) → Option (Fin N) → ℝ, where none is the index $0$ in the first argument and $N + 1$ in the second. A structure JobshopSystem N bundles $\lambda, \mu, r, e$ with Assumptions (2.1)–(2.4) as fields; $e$ is a parameter satisfying (2.5), uniqueness and non-negativity, not a formula. Balance sys q k is the stationary equation (3.1) at k for an arbitrary q, and IsEquilibrium sys q is $q \ge 0$ , HasSum q 1, and Balance at every state. $\pi$ is defined with an explicit if Summable … then … else 0.

Explicit choices, each stated in the item where it applies:

Correction of (3.1). The paper prints the arrival outflow as $\lambda(S(\bar k))$ :

$\dfrac{dP(\bar k, t)}{dt} = -[\lambda(S(\bar k)) + \sum_n \mu(n, k_n)(1 - r(n, n))]P(\bar k, t) + \dots$

Its transition probabilities (p. 134) give $\lambda(S(\bar k))\sum_{n=1}^N r(0, n)$ , since an arrival with an empty routing leaves the state unchanged. The two agree only when $r(0, N+1) = 0$ , and with the printed coefficient Theorem (4.5) is false ( $N = 1$ , $r(0,1) = r(0,2) = 1/2$ , $r(1,2) = 1$ , constant rates, at $\bar k = 0$ ). The formalization uses the coefficient the transition probabilities give. It does not assume $r(0, N+1) = 0$ : the paper allows empty routings.
Uniqueness under bounded arrival rates. Uniqueness (milestone 4 and the goal's second conjunct) assumes $\exists \Lambda,\ \forall K,\ \lambda(K) \le \Lambda$ . The paper asserts uniqueness without proof, citing a limit theorem for regular processes; bounded arrival rates make the process regular and hold for every example in the paper. Existence and the formula carry no added hypothesis.
Companion (6.3). System $(N, L, M, R)^*$ of §5 is not formalized in the paper and not here; only its case $K^* = 0$ , $k_n^* = +\infty$ is stated.

A trivializing formalization is ruled out: Balance and IsEquilibrium are stated for an arbitrary function on states and never mention $w$ , $W$ or $\pi$ , and equilibrium is neither defined as (4.6) nor as detailed or partial balance.

Useful infrastructure: summation over Fin N → ℕ grouped by total (Finset.Nat.antidiagonalTuple), and a non-explosion and uniqueness theory for countable-state continuous-time chains, which is reusable beyond this mission. Not included: the limit $\lim_{t\to\infty} P(\bar k, t) = p(\bar k)$ , which needs a construction of the process; the equivalence of (2.4) with finiteness of routings; Theorem (5.5) and (5.7)–(5.9).

Selected references

J. R. Jackson, Jobshop-Like Queueing Systems, Management Science 10(1), 131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4), 518–521, 1957. https://doi.org/10.1287/opre.5.4.518
W. J. Gordon and G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2), 254–265, 1967. https://doi.org/10.1287/opre.15.2.254
F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/book/whole.pdf
A. T. Bharucha-Reid, Elements of the Theory of Markov Processes and Their Applications, McGraw-Hill, 1960 (Theorem 2.9, p. 102, cited in footnote 5).

6 thms2 active usersReviewed

Completed

Optimization Theoretical Computer Science·Captain: mikedeng1

An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs I: Moore's Algorithm Yields a Schedule with the Minimum Number of Late JobsResearch Paper

Motivation

A single machine must process a set of jobs, each with a processing time and a due-date, and a job that finishes after its due-date is late. Counting late jobs is the natural objective when a late order is simply lost, whatever its lateness. In the three-field notation of scheduling theory this is the problem $1\,\|\,\sum U_j$ , and it is one of the few single-machine problems with a due-date objective that a simple greedy rule solves exactly.

J. Michael Moore gave that rule in 1968 (Management Science 15(1):102–109). The only exact method previously available was the Held–Karp dynamic program, which is exponential in the number of jobs. Moore's algorithm is two sorts plus at most $n(n+1)/2$ additions and comparisons. The rule, and the variant from the paper's Author's Supplement (credited to T. J. Hodgson and today called the Moore–Hodgson algorithm), is in every scheduling textbook, for example Brucker, Scheduling Algorithms, Ch. 4, and is the base case of later work on weighted and release-date variants.

Timeline:

1955: J. R. Jackson shows that a job set can be scheduled with no late job if and only if the earliest-due-date order has none (Management Science Research Project report 43, UCLA).
1968: Moore publishes the algorithm and its proof of optimality, with Hodgson's variant stated without proof.
1970s onward: the weighted version $1\,\|\,\sum w_jU_j$ is shown NP-hard (Karp 1972, via knapsack), and $1\,|\,r_j\,|\,\sum U_j$ likewise (Lenstra, Rinnooy Kan and Brucker 1977), so Moore's greedy rule does not extend to them.

Setting

A finite set $J$ of jobs is given. Job $j$ has a processing time $t_j \ge 0$ and a due-date $D_j$ , and the paper assumes $t_j \le D_j$ for every job (a job that cannot finish on time even if started at time $0$ is removed beforehand). The machine starts at time $0$ and processes the jobs one after another, without idle time or preemption.

A schedule $S$ of $J$ is an ordering $(J_{i_1},\dots,J_{i_n})$ of all jobs of $J$ . The job in position $k$ completes at $C_{i_k} = t_{i_1} + \dots + t_{i_k}$ . The late set is $L = \{J_i : C_i > D_i\}$ and the early set is $E = \{J_i : C_i \le D_i\}$ . A schedule is optimal if no schedule of $J$ has fewer late jobs. $A$ and $R$ denote the early and late jobs of $S$ , each kept in their order in $S$ .

Moore's algorithm works on a current sequence and a list of rejected jobs.

Step 1: order the jobs by non-decreasing processing time (the shortest processing time rule).
Step 2: find the first late job $J_{i_q}$ of the current sequence. If there is none, stop.
Step 3: re-order $J_{i_1},\dots,J_{i_q}$ by non-decreasing due-date. If all of them are then early, keep the re-ordered sequence. Otherwise reject $J_{i_q}$ and remove it. Return to Step 2.

The output is the final current sequence sorted by due-dates, followed by the rejected jobs in any order.

In Lean, a schedule is IsSchedule J l, the late set is lateSet t D l, optimality is IsOptimal t D J l, $A$ and $R$ are earlyPart/latePart, and one pass of Steps 2–3 is the relation MooreStep t D, all in the namespace MooreLateJobs.NumLate.

Formalization targets

Goal: Moore's algorithm is optimal (The Algorithm, Step 2, p. 103)

Let $l_0$ be a shortest-processing-time schedule of $J$ , and let a run of MooreStep from $(l_0,[\,])$ reach a state $(\mathrm{cur},\mathrm{rej})$ in which $\mathrm{cur}$ has no late job. Then for every due-date ordering $A_D$ of $\mathrm{cur}$ and every ordering $P$ of $\mathrm{rej}$ ,

(A_D,\,P)\ \text{is an optimal schedule for } J.

All tie-breaks in both sorts are covered.

Milestones

In attack order:

Lemma 1 (p. 105): every optimal schedule has the same number of late jobs as $(A,R)$ and as every $(A,P)$ .
Jackson's lemma (p. 105).
Lemma 2 (p. 105): re-ordering $A$ by due-dates keeps an optimal $(A,R)$ schedule optimal.
Lemma 3 (p. 105): a job that is late in some optimal schedule can be removed and appended.
The repeated-elimination claim (p. 106): after removing jobs late in successive optimal schedules until the rest is feasible, $(A_D,P)$ is optimal.
Cases 2) and 3) of the Selection Algorithm (p. 107): in either case the job $J_q$ is late in some optimal schedule.
Progress and termination of the algorithm (p. 108).

A companion item states the p. 104 remark that the final current sequence need not be re-sorted: $(\mathrm{cur},P)$ is already optimal.

Significance

The theorem shows that the minimum number of late jobs on one machine can be found in $O(n\log n)$ time, by a rule that also produces an optimal schedule of a very particular shape: due-date ordered early jobs first, then the late jobs in any order. Lemma 3's decomposition, that jobs late in some optimal schedule may be discarded one at a time, is the template reused for many related greedy results in scheduling.

The result is classical and fully proved on paper. To our knowledge no machine-checked proof of Moore's algorithm, of the Moore–Hodgson variant, or of Jackson's rule exists in Mathlib. This mission produces a checked proof of the algorithm as stated in the paper, with every tie-break allowed, together with reusable single-machine objects (schedules as lists, completion times, late sets) and Jackson's earliest-due-date feasibility lemma.

Difficulty

Neither ordering rule works alone. Sorting by due-dates alone gives a schedule with no late job whenever one exists, but it can make many jobs late once any must be. Keeping the shortest jobs first does not respect the due-dates at all. The step that fails in a direct greedy argument is the claim that the specific job $J_{i_q}$ , the one just found late, belongs to the late set of some optimal schedule. That job is not in general the longest job of the prefix, and the paper has to treat separately the two cases in which it is rejected. On top of this, the algorithm re-sorts prefixes on the fly, so the claim has to be tied to the invariants of the run: the prefix is early and due-date sorted, and the jobs after it are at least as long as $J_{i_q}$ .

Formalization scope

Jobs and times. Jobs form a type ι with decidable equality; $J$ is a Finset ι; $t, D : ι \to \mathbb{R}$ .
Standing hypotheses. Every statement that involves schedules assumes $t_j \ge 0$ and $t_j \le D_j$ on $J$ . The first is added: processing times are durations, and Jackson's lemma fails for negative times. The second is the paper's assumption on p. 102.
Schedules and completion times. A schedule is a duplicate-free list with exactly the jobs of $J$ . Positions are 0-based, and the job in position $k$ completes at the sum of the first $k+1$ processing times. Lateness is strict ( $C_j > D_j$ ).
Optimality compares against every schedule of the same job set.
Ties. Orderings "by due-dates" and "by processing times" are List.Pairwise with ≤. Ties are arbitrary, and every statement quantifies over all such orderings.
The algorithm. Steps 2–3 are the relation MooreStep. The re-ordered prefix is any due-date sorted permutation of the first $q+1$ jobs, and case 2) rejects the first late job $J_{i_q}$ itself, not the longest job of the prefix (that is Hodgson's variant). A run is Relation.ReflTransGen.

The goal must concern runs of this step relation from a shortest-processing-time schedule of $J$ . Replacing the run by an arbitrary set of rejected jobs satisfying invariants would state a different theorem. The goal is not vacuous: the progress and termination milestones show that a terminal state is always reached.

Contributions are welcome at every level. Useful ones include general lemmas on completion times under permutation and filtering of lists, a proof of Jackson's lemma, proofs of the Selection Algorithm cases, and a proof of Hodgson's variant.

Selected references

J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
M. Held and R. M. Karp, A Dynamic Programming Approach to Sequencing Problems, J. SIAM 10(1):196–210, 1962. https://doi.org/10.1137/0110015
R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

15 thms2 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

Scheduling with Deadlines and Loss Functions: On One Processor, Decreasing Penalty-to-Length Order Is Optimal When No Task Finishes Before Its DeadlineResearch Paper

Motivation

A processor, a machine shop or a single server must work through a set of jobs one at a time, and each job is costly when it is late. Deciding the order is the single-machine sequencing problem, the simplest and most studied model of scheduling theory. Robert McNaughton's 1959 article Scheduling with Deadlines and Loss Functions (Management Science 6(1):1–12) treats it for a computer that must run several tasks, each with a deadline and a loss that grows linearly with the lateness. Its §2 gives the first sufficient condition under which a simple ratio rule is optimal in the presence of deadlines, and shows that interrupting and resuming tasks ("splitting", now called preemption) never helps on one processor.

Timeline.

1956: W. E. Smith, Various optimizers for single-stage production (Naval Research Logistics Quarterly 3), proves that sequencing jobs by non-increasing weight-to-processing-time ratio minimizes the total weighted completion time over non-preemptive sequences.
1959: McNaughton, §2 of the present paper, proves independently that the same ratio order is optimal against all schedules, split or not and with idle time (Theorem 2.3), and extends it to deadlines when no task finishes early in that order (Theorem 2.4). §3 of the same paper gives the "wrap-around" rule for preemptive makespan on identical processors, and §4 the non-preemptive optimality for weighted completion time on several processors.
1977: J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker show that minimizing total weighted tardiness on one machine, the general problem of §2, is strongly NP-hard (Annals of Discrete Mathematics 1); this is why §2 gives a sufficient condition and not an algorithm.

Setting

There are $m$ tasks $(1),\dots,(m)$ for a single processor, and the present is time $0$ . Task $(i)$ takes $a_i > 0$ units of processing time, has a deadline $d_i$ and a penalty rate $p_i \ge 0$ . If $(i)$ is finished at time $C_i \le d_i$ there is no loss; otherwise the loss on $(i)$ is $p_i x$ , where $x = C_i - d_i$ is the time from the deadline to the completion. Thus the loss on a task completed at time $t$ is

\ell_i(t) = p_i \max(0,\ t - d_i).

The ratio of task $(i)$ is $r_i = p_i / a_i$ .

A task may be split: part of it may run between times 4 and 6 and the remainder between times 8 and 11, and similarly in any finite number of parts. A schedule $S$ is therefore a finite list of pieces, each a task together with a start and a stop time. It is feasible when every piece lies in $[0,\infty)$ with start $\le$ stop, no two pieces overlap in time, and the pieces of each task $(i)$ have total length exactly $a_i$ . The completion time $C_i(S)$ is the latest stop time of a piece of $(i)$ , and the total loss is

c(S) = \sum_{i=1}^{m} \ell_i\bigl(C_i(S)\bigr).

For an order $\sigma$ of the tasks ( $\sigma(k)$ in position $k$ ), the sequenced schedule $S_\sigma$ runs the tasks without splits and without unused time: $\sigma(k)$ occupies $\bigl[\sum_{l<k} a_{\sigma(l)},\ \sum_{l\le k} a_{\sigma(l)}\bigr]$ . The order is in decreasing $r_i$ when $k \le l$ implies $r_{\sigma(l)} \le r_{\sigma(k)}$ . Finally $c^*(S)$ denotes the total loss of $S$ computed as if $d_1 = \dots = d_m = 0$ .

Formalization targets

Goal: Theorem 2.4 (p. 5)

If $\sigma$ is in decreasing $r_i$ and no task finishes before its deadline in $S_\sigma$ , i.e. $d_i \le C_i(S_\sigma)$ for every $i$ , then $S_\sigma$ is feasible and

c(S_\sigma) \le c(S') \qquad \text{for every feasible schedule } S'.

The competitors $S'$ may split tasks and leave the processor idle. The condition is sufficient but not necessary.

Milestones, in attack order

Theorem 2.1 (p. 4): if both $(i)$ and $(j)$ run in the $a_i + a_j$ consecutive units of time after a time $t$ past both deadlines and $r_i > r_j$ , their joint loss is strictly smaller when $(i)$ goes first:

\ell_i(t+a_i) + \ell_j(t+a_i+a_j) < \ell_j(t+a_j) + \ell_i(t+a_j+a_i).

The reduction in the proof of Theorem 2.2 (pp. 4–5): a feasible schedule with more than $m$ pieces can be replaced by a feasible one with fewer pieces and no greater loss.
Theorem 2.2 (p. 4): some optimal schedule, optimal among all feasible schedules, splits no task.
Theorem 2.3 (p. 5): if $d_1 = \dots = d_m = 0$ , the sequenced schedule in decreasing $r_i$ minimizes the total loss over all feasible schedules.
The display of the proof of Theorem 2.4 (p. 6): if no task finishes early in $S = S_\sigma$ , then for every feasible $S'$ ,

c(S') - c(S) \ge c^*(S') - c^*(S).

Significance

The result. Theorem 2.3 is the ratio rule for total weighted completion time, in its strongest single-machine form: it holds against preemptive schedules and schedules with idle time, not only against permutations. Theorem 2.4 carries the rule over to deadlines and linear tardiness penalties under a checkable condition on one schedule. Since weighted tardiness is strongly NP-hard in general, a condition of this kind is what one can hope for, and the paper's two-step heuristic for general deadlines (p. 6) is built on it. Theorem 2.2, as the paper remarks (p. 6), "does not depend on the linear loss function": it makes non-preemptive scheduling without loss of generality for single-machine objectives of this kind.

Formalizing it. All results of §2 are proved in the paper and are textbook material; none has a machine-checked proof on the platform. The platform's Scheduling Algorithms V mission formalizes the multi-processor results of §§3–4 (via Brucker's textbook), and nothing there states a single-processor ratio rule with deadlines. This mission supplies a single-processor schedule model with splitting, the interchange lemma, the non-preemption theorem and the ratio rule, each over all feasible schedules.

Difficulty

The interchange argument of Theorem 2.1 compares only two schedules that differ in the order of two adjacent tasks. Turning it into optimality against every feasible schedule requires two further steps, and each fails if done naively. First, a competitor may split tasks and leave gaps; the interchange argument does not apply to such schedules, so a separate argument must remove splits without raising any completion time. Second, with deadlines the loss $\max(0, t - d_i)$ is not linear in the completion time, so the ratio order is in general not optimal; the obvious attempt to repeat the interchange argument fails as soon as a task can finish before its deadline, since moving such a task later costs nothing. This is why Theorem 2.4 needs its hypothesis that no task finishes early, and why the paper leaves the general case to a heuristic.

Formalization scope

Tasks and positions are the zero-based indices of Fin m; times, lengths, deadlines and penalties are real numbers. A schedule is a List of pieces (task, start, stop), mirroring the public definition SchedulingAlgorithms_ParallelMachines with one processor. Feasibility requires $0 \le$ start $\le$ stop, pairwise disjoint pieces, and exact total length $a_i$ per task; zero-length pieces and unsorted lists are allowed. The completion time is the maximum stop time of the task's pieces ( $0$ for a task with no pieces, which feasibility excludes). "No split" means exactly one piece per task, so two abutting pieces count as a split. "Decreasing $r_i$ " is non-increasing, with ties in any order. "Minimal" and "optimal" are stated as $\le$ against every feasible schedule, never as an infimum.

Standing assumptions, stated in every item: $a_i > 0$ (tasks take time, and $r_i = p_i/a_i$ needs $a_i \ne 0$ ), and $p_i \ge 0$ for Theorems 2.2–2.4 and the proof steps (penalties are non-negative; with a negative penalty and idle time allowed the loss is unbounded below). Theorem 2.1 carries no sign condition. No condition is placed on the deadlines.

A formalization that restricts the competitors of Theorems 2.2–2.4 to unsplit schedules, or to sequenced schedules of other orders, states a weaker theorem and is ruled out: every statement quantifies over all feasible schedules.

A complete development needs: sums over sublists of pieces, rearrangements of pieces of a schedule and their effect on completion times, and optimality over permutations of a finite set of tasks. The schedule model and the non-preemption argument are reusable for any single-machine regular objective. Contributions of intermediate lemmas on these points are welcome.

Selected references

R. McNaughton, Scheduling with Deadlines and Loss Functions, Management Science 6(1):1–12, 1959. https://doi.org/10.1287/mnsc.6.1.1
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3(1–2):59–66, 1956. https://doi.org/10.1002/nav.3800030106
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

7 thms2 active usersReviewed

Numerical Analysis Optimization·Captain: mikedeng1

Pattern Search Algorithms for Bound Constrained Minimization: Generalized Pattern Search Drives the Projected Stationarity Measure to ZeroResearch Paper

Motivation

Pattern search methods minimize a function $f:\mathbb R^n\to\mathbb R$ by comparing values of $f$ at points of a structured set of trial points, without evaluating or approximating derivatives. Coordinate search and the method of Hooke and Jeeves (Hooke–Jeeves 1961) are the classical members of the family. Such methods remain in use when derivatives are unavailable, unreliable or expensive, for instance when $f$ is the output of a simulation, and practical problems of this kind usually carry simple bounds on the variables.

Torczon (SIAM J. Optim. 1997) gave a global convergence theory for pattern search on unconstrained problems: under compactness of the level set and continuous differentiability of $f$ , $\liminf_k\|\nabla f(x_k)\|=0$ , and under stronger hypotheses $\lim_k\|\nabla f(x_k)\|=0$ . Lewis and Torczon extended this theory to bound constrained problems (ICASE Report 96-20, 1996; SIAM J. Optim. 1999). The extension is not automatic: the paper exhibits a pattern search method for unconstrained problems (Box's evolutionary operation with factorial designs) that fails on bound constrained ones, and identifies the structural condition on the pattern that restores convergence.

Timeline.

1961: Hooke and Jeeves introduce "direct search" pattern methods.
1987–1988: Calamai and Moré (Math. Program. 1987) and Conn, Gould and Toint (SIAM J. Numer. Anal. 1988) develop the projected-gradient stationarity theory for bound and linear constraints, for methods that use derivatives.
1997: Torczon proves global convergence of generalized pattern search for unconstrained problems.
1996/1999: Lewis and Torczon prove the bound constrained theory formalized here.

Setting

The problem is

\min f(x)\quad\text{subject to}\quad \ell\le x\le u,

with $\ell,u$ vectors of extended reals and $\ell_j<u_j$ for every $j$ ; $\ell_j=-\infty$ or $u_j=+\infty$ is allowed. The feasible region is $\Omega=\{x:\ell\le x\le u\}$ , $P$ is the coordinatewise projection onto $\Omega$ , $g=\nabla f$ , and $L_\Omega(y)=\{x\in\Omega:f(x)\le f(y)\}$ is the feasible level set. A stationary point is an $x\in\Omega$ with $\langle g(x),z-x\rangle\ge0$ for all $z\in\Omega$ . The stationarity measure is

q(x)=P\bigl(x-g(x)\bigr)-x,

which vanishes exactly at stationary points.

A generalized pattern search method is fixed by a nonsingular basis matrix $B\in\mathbb R^{n\times n}$ , a finite set $\mathcal M$ of nonsingular integer matrices, a rational $\tau>1$ , an integer $w_0<0$ and nonnegative integers $w_1,\dots,w_L$ . At iteration $k$ the generating matrix is $C_k=[M_k\ \ {-M_k}\ \ L_k]=[\Gamma_k\ \ L_k]$ with $M_k\in\mathcal M$ , $L_k$ an integer matrix containing a zero column, and $BM_k$ diagonal. A trial step is $\Delta_kBc$ for a column $c$ of $C_k$ . The step $s_k$ is a trial step with $x_k+s_k\in\Omega$ , and it must decrease $f$ whenever some feasible trial step from the core $\Delta_kB\Gamma_k$ does. The iterate moves, $x_{k+1}=x_k+s_k$ , exactly when $f(x_k+s_k)<f(x_k)$ . The step length $\Delta_k$ is multiplied by $\theta=\tau^{w_0}<1$ after an unsuccessful iteration and by some $\tau^{w_i}\ge1$ after a successful one. The Strong Hypotheses additionally require $f(x_k+s_k)$ to be no larger than the best feasible core trial value whenever that value is below $f(x_k)$ .

Formalization targets

Goal: Theorem 3.3

If $L_\Omega(x_0)$ is compact, $f$ is continuously differentiable, the columns of the $C_k$ are uniformly bounded, $\Delta_k\to0$ , and the Strong Hypotheses hold, then

\lim_{k\to\infty}\|q(x_k)\|=0 .

Milestones

Lemma 2.1, Theorem 2.2, Lemma 2.3: the unconstrained results the paper recalls from Torczon (1997): nonzero steps have length at least $\zeta_*\Delta_k$ ; the iterates lie on the translated lattice $x_0+\beta^{r_{LB}}\alpha^{-r_{UB}}\Delta_0B\,\mathbb Z^n$ (with $\tau=\beta/\alpha$ ); bounded columns give $\Delta_k\ge\psi_*\|s_k^i\|$ .
Proposition 3.1 (6), (8): $\|q(x)\|\le\|g(x)\|$ , and $x$ is stationary iff $q(x)=0$ .
All iterates lie in $L_\Omega(x_0)$ (§4, p. 10).
Propositions 4.1–4.3: a descent estimate along short steep directions; a feasible core step with $g_k^Ts\le-n^{-1/2}\|q_k\|\|s\|$ whenever $q_k\ne0$ and the step length is small; a uniform $\delta$ (and, under the Strong Hypotheses, a $\sigma$ ) with $f(x_{k+1})\le f(x_k)-\sigma\|q(x_k)\|\|s_k\|$ when $\Delta_k<\delta$ and $\|q(x_k)\|>\eta$ .
Corollary 4.4 and Theorem 4.5: $\liminf\|q(x_k)\|\ne0$ keeps $\Delta_k$ bounded away from zero, whereas compactness alone forces $\liminf\Delta_k=0$ .
Theorem 3.2: $\liminf_k\|q(x_k)\|=0$ .

Significance

Theorem 3.2 shows that a method which never computes a gradient still has a subsequence approaching first-order stationarity for the bound constrained problem, even though it cannot enforce a sufficient decrease condition measured by the projected gradient. Theorem 3.3 upgrades this to the whole sequence, so every limit point of the iterates is a KKT point. These results justify the bound constrained variants of coordinate search and Hooke–Jeeves discussed in §5 of the paper, and they are the template for the later theory of pattern search under linear constraints and generating set search.

The results are proved in the paper, and three of the milestones are proved in Torczon (1997). None of them has a machine-checked proof. Formalizing them produces a Lean model of generalized pattern search (patterns, exploratory moves, step-length updates) that later missions on direct search, mesh adaptive direct search or linearly constrained pattern search can reuse, and checks the details the paper handles briefly: the lattice argument, the feasibility of the chosen coordinate step, and uniform constants.

Difficulty

The obvious argument copies the unconstrained proof with $\nabla f$ replaced by $q$ . The step that fails is the existence of a good trial step: in the unconstrained case some pattern direction makes an acute angle with $-\nabla f(x_k)$ , but near the boundary of $\Omega$ that direction may leave the feasible region, and a feasible direction may not be a descent direction. For a general pattern no uniform choice exists, and the paper's counterexample in §5.2 shows convergence can fail. The diagonality of $BM_k$ is what makes the pattern contain coordinate directions, one of which is both feasible and a descent direction of quality $n^{-1/2}\|q_k\|$ (Proposition 4.2). The second difficulty is Theorem 4.5, which uses no derivatives: it rests on the rationality of $\tau$ and the integrality of the $C_k$ , which confine the iterates to a lattice that meets the compact set $L_\Omega(x_0)$ in finitely many points.

Formalization scope

Points are EuclideanSpace ℝ (Fin n) with the Euclidean norm; the bounds are Fin n → EReal with the hypothesis $\ell_j<u_j$ for all $j$ , so infinite bounds are allowed as in the paper. Paper coordinates $1,\dots,n$ are Lean's Fin n. The gradient is Mathlib's gradient f. A run of the method is a structure of sequences $(x_k,\Delta_k,s_k,M_k,L_k)$ together with a predicate IsGPSRun that encodes §2.1–§2.4 clause by clause; the parameter $m\ge1$ is the number of columns of $L_k$ (the paper's $p-2n$ ). $\tau$ is rational and the $C_k$ are integer matrices, as the lattice argument requires. " $\min\{f(x_k+y):\dots\}<f(x_k)$ " over the finite set of feasible core trial points is encoded as "some feasible core trial step strictly decreases $f$ ". $\liminf$ statements are encoded with ∃ᶠ, not Filter.liminf. The modulus of continuity $\omega$ is not formed as a real supremum; Proposition 4.1 takes an explicit radius $\delta>\|d\|$ .

Standing assumptions and every departure from the page:

Smoothness. The page assumes $f$ continuously differentiable on $L_\Omega(x_0)$ . The mission assumes $f$ is $C^1$ on an open set $U\supseteq\Omega$ . The proofs evaluate $\nabla f$ along segments to trial points that lie in $\Omega$ but generally outside $L_\Omega(x_0)$ , and $L_\Omega(x_0)$ may have empty interior, so the page's hypothesis does not define what the proofs use.
Strong Hypothesis 3. The page prints $f(x_k+s_k)<\min\{\cdots\}$ . No core step can satisfy the strict form, which would exclude coordinate search, which the paper says satisfies it. The mission uses $\le$ , the form of Torczon (1997) and the one the proof of Proposition 4.3 uses. The theorem with $\le$ implies the one with $<$ .
The nonemptiness of $\{w_1,\dots,w_L\}$ is made explicit.
Proposition 3.1 (7) is omitted: its $P(g(x))$ is a projected gradient the paper does not define.
Proposition 4.2 quantifies over every step length below $\nu_k$ , because $\nu_k$ does not depend on $\Delta_k$ .

The run predicate is not vacuous: an explicit run of coordinate search on $f(x)=x$ over $[0,\infty)$ satisfies IsGPSRun, the Strong Hypotheses, bounded columns, $\Delta_k\to0$ and compactness of $L_\Omega(x_0)$ . That check is proved in Lean without sorry, so the goal cannot be closed by exhibiting an unsatisfiable hypothesis.

A complete development needs the mean value theorem along segments, uniform continuity of $\nabla f$ near the compact set $L_\Omega(x_0)$ , finiteness of a discrete lattice inside a compact set, and elementary facts about the coordinatewise projection. The projection and lattice lemmas are reusable beyond this mission. Proofs of any milestone, alternative proofs, and a general statement of Proposition 3.1 for closed convex $\Omega$ are welcome.

Selected references

R. M. Lewis and V. Torczon, Pattern Search Algorithms for Bound Constrained Minimization, ICASE Report No. 96-20 (NASA CR-198306), 1996; SIAM J. Optim. 9(4):1082–1099, 1999. https://doi.org/10.1137/S1052623496300507
V. Torczon, On the Convergence of Pattern Search Algorithms, SIAM J. Optim. 7(1):1–25, 1997. https://doi.org/10.1137/S1052623493250780
P. H. Calamai and J. J. Moré, Projected Gradient Methods for Linearly Constrained Problems, Math. Program. 39:93–116, 1987. https://doi.org/10.1007/BF02592073
A. R. Conn, N. I. M. Gould and P. L. Toint, Global Convergence of a Class of Trust Region Algorithms for Optimization with Simple Bounds, SIAM J. Numer. Anal. 25(2):433–460, 1988. https://doi.org/10.1137/0725029
R. Hooke and T. A. Jeeves, "Direct Search" Solution of Numerical and Statistical Problems, J. ACM 8(2):212–229, 1961. https://doi.org/10.1145/321062.321069

16 thms2 active usersReviewed

Completed

Control Theory Convex Optimization Optimization·Captain: mikedeng1

Robust Solutions to Uncertain Semidefinite Programs II: An SDP Inner Approximation of the Robust Feasible Set under Structured PerturbationsResearch Paper

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$ . In engineering applications the coefficient matrices are rarely known exactly: they come from measurements, from a model of a physical plant, or from a finite-precision implementation. El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for solutions that remain feasible for every admissible value of the uncertain data, and showed how to compute such robust solutions by semidefinite programming. The paper appeared alongside Ben-Tal and Nemirovski's robust convex programming (Math. Oper. Res. 23(4), 1998) and is one of the two founding treatments of robust SDP.

When the uncertainty has structure (a block-diagonal perturbation, repeated scalar parameters, a symmetric matrix), the exact robust problem is NP-hard (El Ghaoui and Lebret, SIAM J. Matrix Anal. Appl. 18, 1997). This is the same obstacle that robust control meets in computing the structured singular value, and the remedy the paper uses, scaling matrices that commute with the perturbation structure, goes back to that literature (Doyle, IEE Proc. D 129, 1982; Fan, Tits and Doyle, IEEE Trans. Automat. Control 36, 1991). This mission formalizes the resulting tractable conservative approximation, Theorem 3.2 of the paper, together with the lemma it rests on and an application to integer feasibility problems.

Setting

Fix natural numbers $m, n, p, q$ . The decision variable is $x \in \mathbb{R}^m$ . The nominal data are affine maps

F(x) = F_0 + \sum_{i=1}^m x_i F_i \in \mathbb{R}^{n\times n}, \qquad R(x) = R_0 + \sum_{i=1}^m x_i R_i \in \mathbb{R}^{q\times n},

with every $F_i$ symmetric, and fixed matrices $L \in \mathbb{R}^{n\times p}$ , $D \in \mathbb{R}^{q\times p}$ . A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$ , and the perturbed constraint matrix is the linear-fractional representation (LFR)

\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,

which is defined when $\det(I - D\Delta) \neq 0$ . The perturbation ranges over a linear subspace $\mathcal{D} \subseteq \mathbb{R}^{p\times q}$ , which encodes the structure, and is bounded by a level $\rho > 0$ in the spectral norm $\|\Delta\|$ (the largest singular value). The robust feasible set is

\mathcal{X}_\rho = \{x : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \det(I - D\Delta) \neq 0 \text{ and } \mathbf{F}(x,\Delta) \succeq 0\},

and the robust SDP (RSDP) is to minimize $c^Tx$ over $\mathcal{X}_\rho$ .

The scaling set of $\mathcal{D}$ is the linear subspace

\mathcal{B} = \{(S,T,G) \in \mathbb{R}^{p\times p}\times\mathbb{R}^{q\times q}\times\mathbb{R}^{p\times q} : S\Delta = \Delta T,\ G\Delta^T = -\Delta G^T \text{ for every } \Delta \in \mathcal{D}\}.

Formalization targets

Goal: Theorem 3.2 (p. 37), as an inclusion of feasible sets

For every $x$ : if some $(S,T,G) \in \mathcal{B}$ has $S \succ 0$ , $T \succ 0$ and

\begin{bmatrix} F(x) - LSL^T & R(x)^T - LSD^T + LG \\ R(x) - DSL^T + G^TL^T & \rho^{-2}T - DSD^T + DG + G^TD^T\end{bmatrix} \succ 0,

then $x \in \mathcal{X}_\rho$ , and in fact $\mathbf{F}(x,\Delta) \succ 0$ for every $\Delta \in \mathcal{D}$ with $\|\Delta\| \le \rho$ . A companion item states the consequence for optimal values: the SDP value is an upper bound on the RSDP value, with both infima taken in the extended reals.

Milestones

Lemma 3.2 (p. 37): the same implication for constant $F$ , $R$ and $\rho = 1$ , with the matrix (13).
The full-perturbation case (p. 37): for $\mathcal{D} = \mathbb{R}^{p\times q}$ and $p, q \ge 1$ , $\mathcal{B}$ consists exactly of the triples $(\tau I_p, \tau I_q, 0)$ , with $\tau \ge 0$ when $S \succeq 0$ .
Theorem 5.6 (p. 48): if $F_i = 2L_iR_i$ with $r_i = \operatorname{rank} F_i$ , and $x_{\mathrm{feas}}$ satisfies, for some $\lambda \ge 0$ and block-diagonal $S = S^T$ , $G = -G^T$ ,

\begin{bmatrix} F(x_{\mathrm{feas}}) - \lambda I - LSL^T & \tfrac12R^T + LG \\ \tfrac12R - GL^T & S\end{bmatrix} \succ 0,

then every integer vector closest to $x_{\mathrm{feas}}$ in the maximum norm satisfies $F(z) \succeq 0$ .

Significance

The result. Theorem 3.2 replaces an NP-hard semi-infinite constraint, one matrix inequality for each admissible perturbation, by a single linear matrix inequality in the enlarged variable $(x, S, T, G)$ . Every point it certifies is robustly feasible, so its optimal value is a certified upper bound on the robust optimum and its optimizer is a usable robust solution. In the full case the scalings collapse to one multiplier $\tau$ (milestone 2), which connects the bound to the exact reformulation of Section 3.1 of the paper. Theorem 5.6 shows the same machinery at work on a combinatorial problem: robustness against perturbations of size $1/2$ in each coordinate of $x$ turns an SDP-feasible point into an integer solution by rounding.

Formalizing it. The results are proved in the paper (Lemma 3.2 with the proof deferred to [16]); none of them has a machine-checked proof that this mission is aware of, and the platform has no linear-fractional or structured-perturbation results. The formalization also settles the exact form of the certificate: as printed, the matrix (13) and the LMI of Theorem 3.2 contain products that are dimensionally undefined, and this mission states the condition the proof actually yields (see the scope section).

Difficulty

The inequality to be proved is a statement about infinitely many perturbations, and $\mathbf{F}(x,\Delta)$ depends on $\Delta$ through a matrix inverse. The natural first step, eliminating $\Delta$ by an exact S-procedure as in the full case, is not available: with a structured $\mathcal{D}$ the set of pairs of vectors linked by some $\Delta \in \mathcal{D}$ is not described by one quadratic inequality, and losslessness fails. The scalings in $\mathcal{B}$ give several valid quadratic inequalities instead, and one must show that their combination controls every $\Delta$ in the norm ball, including the well-posedness claim $\det(I - D\Delta) \neq 0$ , which is part of the conclusion rather than an assumption. The commutation condition $S\Delta = \Delta T$ must be turned into an inequality for $\|\Delta\| \le 1$ , which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between $\rho = 1/2$ and the stated matrix must be matched to the general lemma.

Formalization scope

Matrices are Matrix (Fin a) (Fin b) ℝ; $\succ 0$ and $\succeq 0$ are Matrix.PosDef and Matrix.PosSemidef (both include symmetry); block matrices are Matrix.fromBlocks on Fin n ⊕ Fin q. The norm of a perturbation is the $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), i.e. the largest singular value; the maximum norm in Theorem 5.6 is Mathlib's sup norm on Fin m → ℝ. $\mathcal{D}$ is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is $0$ at a singular matrix, so every statement pairs the LFR with $\det(I - D\Delta) \neq 0$ . The standing assumption $\rho > 0$ of Section 3 is a hypothesis.

Readings and corrections of the printed statements:

(13) as printed is dimensionally inconsistent; we state the condition the proof yields, which coincides with the printed one when $G$ is square and skew-symmetric and $\mathcal{D}$ consists of symmetric matrices. Concretely, (11) prints $G \in \mathbb{R}^{q\times p}$ with $G\Delta = -\Delta^TG^T$ and (13) prints the blocks $R - DSL - GL^T$ and $T - GD^T + DG - DSD^T$ ; the mission uses $G \in \mathbb{R}^{p\times q}$ with $G\Delta^T = -\Delta G^T$ and the blocks $R - DSL^T + G^TL^T$ and $T - DSD^T + DG + G^TD^T$ . The same correction applies to the LMI of Theorem 3.2 (with $\rho^{-2}T$ ). Theorem 5.6 is stated as printed.
"An upper bound on the RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the inclusion of the SDP's feasible projection in $\mathcal{X}_\rho$ , for every $x$ ; the goal states it with the strict conclusion $\mathbf{F}(x,\Delta) \succ 0$ as well. The value form is a separate item.
In the full-perturbation remark, "for some $\tau \ge 0$ " is stated under $S \succeq 0$ , and "We then recover the exact results of section 3.1" is not formalized.
In Theorem 5.6, $\mathcal{S}$ 's index range " $i = 1,\dots,n$ " is read as $i = 1,\dots,m$ ; the hypothesis $r_i = \operatorname{rank}F_i$ is kept.

Trivializing formalizations are ruled out: $(0,0,0) \in \mathcal{B}$ always, so the hypotheses $S \succ 0$ and $T \succ 0$ are kept outside $\mathcal{B}$ ; $\mathcal{D}$ is a subspace, not an arbitrary set; and the norm is the spectral norm, not Mathlib's default entrywise norm.

A complete development needs the square root of a positive definite matrix and its commutation with $S$ and $T$ , the spectral-norm characterization $\Delta\Delta^T \preceq \|\Delta\|^2 I$ , Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating $(I - D\Delta)^{-1}$ to an auxiliary vector. These are reusable well beyond this mission; contributions of any of them, and of the value and rounding corollaries, are welcome.

Selected references

L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18:1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
M. K. H. Fan, A. L. Tits, J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36:25–38, 1991. https://doi.org/10.1109/9.62265
J. C. Doyle, Analysis of feedback systems with structured uncertainties, IEE Proc. D 129(6):242–250, 1982. https://doi.org/10.1049/ip-d.1982.0053
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777

5 thms2 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

Integrating Replenishment Decisions with Advance Demand Information II: With Zero Set-up Cost the Myopic Base-Stock Policy Is Optimal When Myopic Levels Are NondecreasingResearch Paper

Motivation

Many firms learn about demand before it has to be served: customers place orders days or weeks ahead of the date they want delivery. Gallego and Özer (Management Science 47(10), 2001) model this advance demand information in a periodic-review inventory system and ask how the optimal replenishment policy should use it. Classical inventory theory (Arrow, Harris and Marschak 1951; Scarf 1959; Veinott 1965, 1966; Iglehart 1963) assumes that nothing about future demand is known when an order is placed. With advance orders the state of the system is no longer a single number, and it is not a priori clear whether the familiar policy structures survive.

This mission covers the paper's zero set-up cost case (Section 5). The companion mission Integrating Replenishment Decisions with Advance Demand Information I covers the positive set-up cost case and its $(s, S)$ policies.

Setting

Time is divided into periods $t = 1, \dots, T$ . The supply lead time is an integer $L \ge 0$ , and the information horizon is $N$ . In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$ , where $D_{t,s} \ge 0$ is demand placed in period $t$ for delivery in period $s$ . Throughout, $N > L + 1$ ; write $M = N - L - 1 \ge 1$ .

At the start of period $t$ the decision maker knows two things. The first is the modified inventory position $x_t$ : on-hand stock plus outstanding orders minus backorders, net of the demand already observed for the protection period $t, \dots, t+L$ . The second is the vector

o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M

of demands already observed for periods beyond the protection period. The decision maker raises the position to $y \ge x_t$ at zero fixed cost, the demand vector $D_t$ is realised, and the state moves to

x_{t+1} = y - \sum_{k=0}^{L+1} D_{t,t+k} - o_{t,t+L+1}, \qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ (s = t+L+2, \dots, t+N),

with $o_{t,t+N} = 0$ .

Costs enter through a single-period cost $G_t : \mathbb{R} \to \mathbb{R}$ (holding, backorder and linear ordering cost, charged against the demand over the protection period) and one-period discount factors $\alpha_{t+1} > 0$ . The optimal cost-to-go $J_t$ and the cost $V_t$ of ordering up to $y$ satisfy

J_t(x, o) = \min_{y \ge x} V_t(y, o), \qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb{E}\,J_{t+1}(x_{t+1}, o_{t+1}), \qquad J_{T+1} \equiv 0,

where the expectation is over $D_t$ . The base-stock level in period $t$ is the smallest minimizer

y_t(o) = \min\{y : V_t(y, o) = \min_x V_t(x, o)\},

and the myopic level is the smallest minimizer of the single-period cost,

y^m_t = \min\{y : G_t(y) = \min_x G_t(x)\}.

A function $f(x, \theta)$ has decreasing differences if $f(x_1, \theta) - f(x_2, \theta) \le f(x_1, \theta') - f(x_2, \theta')$ whenever $x_1 \ge x_2$ and $\theta \ge \theta'$ componentwise.

Formalization targets

Goal: Theorem 5 (p. 1352)

If $t \mapsto y^m_t$ is nondecreasing on $\{1, \dots, T\}$ , then for every period $t$ and every observed-demand vector $o \ge 0$ ,

y_t(o) = y^m_t .

The optimal order-up-to level then ignores all advance information beyond the protection period. A second item states the paper's stationary special case: if $G_t = G$ for all $t$ , the smallest minimizer $y^m$ of $G$ is the optimal base-stock level in every period.

Milestones: Theorem 4 (p. 1351)

For every period $t$ and every fixed $o_t$ :

$V_t(\cdot, o_t)$ is convex and $V_t(x, o_t) \to \infty$ as $|x| \to \infty$ ;
$y_t(o_t)$ exists and $J_t(x, o_t) = V_t(\max(y_t(o_t), x), o_t)$ : a state-dependent base-stock policy is optimal;
$J_t(\cdot, o_t)$ is nondecreasing and convex;
$V_t(x, o)$ has decreasing differences in $(x, o)$ ;
$J_t(x, o)$ has decreasing differences in $(x, o)$ ;
$y_t(o)$ is nondecreasing in $o$ .

Parts 1–3 are what the goal's proof uses. Parts 4–6 are the paper's second zero set-up result, monotonicity of the base-stock level in observed demand.

Significance

The theorem identifies when advance demand information beyond the protection period can be ignored. When the myopic levels do not decrease over time, which includes stationary costs and ramping-up demand, the $(1 + M)$ -dimensional dynamic program collapses to a sequence of one-dimensional newsvendor-type problems. That is both a computational simplification and a managerial statement: information about demand after the protection period does not change the order. Theorem 4, Part 5 gives the complementary monotone comparative statics. When the myopic condition fails, more observed demand never lowers the order-up-to level.

The results are proved in the paper, with the proofs in Appendix B. No machine-checked version exists. This mission produces a formal account of the finite-horizon recursion with a multi-dimensional information state, and checks the base-stock and myopic-optimality arguments against it.

Difficulty

The obvious induction carries convexity of $J_{t+1}$ backward, but here the future cost is evaluated at a random next state $(x_{t+1}, o_{t+1})$ whose first coordinate depends on the current observed demand $o_{t,t+L+1}$ . Showing that the base-stock level does not depend on $o_t$ therefore needs more than convexity. It needs to know where $J_{t+1}(\cdot, o_{t+1})$ is flat, uniformly in the random $o_{t+1}$ , and that the next position cannot exceed the current order-up-to level. The latter holds only on the reachable states, where observed demands are nonnegative. For a sufficiently negative $o_{t,t+L+1}$ the next period starts above its myopic level whatever is ordered now, and the conclusion fails. On the analytic side, every infimum and expectation in the recursion must be shown to be finite and attained before the order-theoretic argument can start.

Formalization scope

The model is parametrised by $L$ and $M \ge 1$ , with $N = L + M + 1$ . The demand vector is a function on $\{0, \dots, N\}$ and $o$ a function on $\{0, \dots, M-1\}$ , ordered componentwise. $J_t$ is defined by backward recursion with $J_t \equiv 0$ for $t > T$ . The minimum over $y \ge x$ is a real infimum and the expectation a Bochner integral against the law $\mu_t$ of $D_t$ . Attainment and finiteness are consequences proved in the theorems, not assumptions. Base-stock and myopic levels are characterised as smallest minimizers (IsLeast), never through sInf.

The single-period cost $G_t$ is a primitive rather than being assembled from $c_t$ , $g_t$ and the lead-time demand; the paper's $G_t$ has the assumed properties, so the theorems cover the paper's model. Hypotheses the paper uses without stating, all placed on primitives and labelled in the statements:

nonnegative demands, $D_{t,s} \ge 0$ almost surely;
coercivity of $G_t$ (the paper states it for $\tilde G_t$ only);
$\alpha_{t+1} > 0$ ;
finiteness of the expectation in (9), guaranteed by linear growth of $G_t$ and finite first moments of $D_t$ . This covers piecewise-linear holding and backorder costs with any finite-mean demand (including the paper's Poisson example), but excludes superlinear costs;
in the goal, $o \ge 0$ , the set of reachable states.

The goal cannot be trivialised: the hypotheses are satisfied by concrete instances (for example $G_t(y) = |y|$ with any finite-mean nonnegative demand), and the conclusion identifies the base-stock level exactly rather than asserting that some minimizer exists.

Out of scope: the reduction of the control problem to the functional equation (Appendix A, Özer 2000), the infinite-horizon Theorem 6, and Lemma 5, whose proof argues on the integers and whose real-valued form with a unit forward difference is unverified. Contributions of general lemmas are welcome: convexity and attainment for $\inf_{y \ge x}$ of a convex coercive function, and preservation of convexity and decreasing differences under expectation. All of them are reusable in other inventory models.

Selected references

G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
A. F. Veinott, Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

9 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Validation of Subgradient Optimization I: The Core Problem Built from the Subgradient Iterates Solves the Dual Linear ProgramResearch Paper

Motivation

Subgradient optimization maximizes a concave function that is not differentiable by stepping along an arbitrary subgradient with a prescribed sequence of step sizes. It became a standard tool of integer programming after Held and Karp used it to compute the Lagrangian 1-tree bound for the traveling-salesman problem (Held & Karp 1971). Held, Wolfe and Crowder then tested it on the assignment problem, a traveling-salesman relaxation and a multicommodity flow problem (Held, Wolfe & Crowder 1974).

The method has one practical defect that the paper names at the start of its Section 6: it contains no test of optimality. The value $w(\pi^j)$ approaches the maximum, but at no finite step does the method say that the maximum has been reached, or what the maximum is. Section 6 of the paper supplies such a test for the case where $w$ is a minimum of finitely many affine functions. The finitely many subgradients produced by the iterates define a small linear program, the core problem, and from some iteration on this linear program already solves the full dual linear program. Its optimal value is therefore the exact maximum of $w$ , obtained from quantities the method computes anyway. This is how the authors certified the optimal values reported in their experiments.

Timeline:

1967–1969: Poljak proves that the subgradient iterates satisfy $w(\pi^j)\to\max w$ when the step sizes tend to zero and have divergent sum (Poljak 1967; Poljak 1969).
1971: Held and Karp apply the method to the 1-tree bound (Held & Karp 1971).
1974: Held, Wolfe and Crowder prove that the core problem $P(J,J^*)$ solves the dual linear program (Theorem 6.3) and give a sufficient condition for bounded iterates (Theorem 6.1).
1996–1999: primal recovery from subgradient iterates is developed further, by convex combinations of the subgradients with weights derived from the step sizes (Sherali & Choi 1996; Larsson, Patriksson & Strömberg 1999).

Setting

Fix $n\ge0$ and write $E^n=\mathbb R^n$ with the Euclidean inner product $\pi\cdot v$ . The data are $K\ge1$ scalars $c_k$ and vectors $v_k\in E^n$ , and

w(\pi)=\min\{c_k+\pi\cdot v_k : k=1,\dots,K\}.\qquad(2.2)

The function $w$ is assumed bounded above, the paper's standing assumption. An index $k$ attains the minimum at $\pi$ if $c_k+\pi\cdot v_k=w(\pi)$ .

A run of the subgradient algorithm consists of a starting point $\pi^0\in E^n$ , step sizes $t_j>0$ and indices $k(j)$ such that $k(j)$ attains the minimum at $\pi^j$ , and

\pi^{j+1}=\pi^j+t_j\,v_{k(j)}\qquad(j=0,1,\dots).\qquad(2.6)

No rule for choosing among several minimizing indices is imposed. Write $v^j=v_{k(j)}$ and $c^j=c_{k(j)}$ . The step-size conditions are

t_j\to0,\qquad \sum_{j=0}^\infty t_j=\infty.\qquad(2.7)

The dual linear program of $\max w$ is

\min\Big\{\sum_k c_ky_k : y_k\ge0,\ \sum_ky_k=1,\ \sum_ky_kv_k=0\Big\}.\qquad(6.1)

For integers $J<J^*$ the core problem $P(J,J^*)$ has one variable $y_j$ for each iteration $j\in[J,J^*]$ :

\min\Big\{\sum_{j=J}^{J^*}c^jy_j : y_j\ge0,\ \sum_{j=J}^{J^*}y_j=1,\ \sum_{j=J}^{J^*}y_jv^j=0\Big\}.

An index chosen at several iterations contributes several identical columns. A point $y$ of $P(J,J^*)$ is sent to the point $\bar y_k=\sum\{y_j : J\le j\le J^*,\ k(j)=k\}$ of (6.1). This aggregation preserves feasibility and objective value.

Formalization targets

Goal: Theorem 6.3 (p. 82)

Assume $w$ is bounded above, $(t_j,\pi^j,k(j))$ is a run satisfying (2.7), and $\{\pi^j\}$ is bounded. Then

\forall J\ \exists J^*>J:\quad P(J,J^*)\text{ has a solution, and every solution of }P(J,J^*)\text{ aggregates to a solution of (6.1)}.

The goal states existence of $J^*$ , which is what the paper claims. The paper's argument in fact gives the conclusion for every sufficiently large $J^*$ . That stronger form is not the goal. Feasibility of $P(J,J^*)$ (Lemma 6.2) or the inequality $\mathrm{Value}[P(J,J^*)]\ge\mathrm{Value}[(6.1)]$ , which holds for every feasible $P(J,J^*)$ , is not a formalization of the goal. The content is optimality in (6.1).

Milestones

Eq. (2.10): if $\pi^*$ maximizes $w$ and $k$ attains the minimum at $\pi$ , then $w^*-w(\pi)\le v_k\cdot(\pi^*-\pi)$ .
§6, p. 80 (display): under (2.6), (2.7) and $w$ bounded above, $\lim_j w(\pi^j)=\max w=w(\pi^*)$ for some $\pi^*$ . The iterates are not assumed bounded.
Theorem 6.1: if every $\pi\ne0$ has some $\pi\cdot v_k<0$ , every run satisfying (2.7) is bounded.
Eq. (6.1): (6.1) has a solution, and its optimal value equals $\max w$ .
Lemma 6.2: for any $J$ there is $J^*>J$ with $P(J,J^*)$ feasible, for bounded runs.

Significance

Theorem 6.3 turns an asymptotic method into one that returns an exact answer. Solving $P(J,J^*)$ for growing $J^*$ produces a linear program of bounded size whose optimum is eventually the optimum of (6.1), and hence $\max w$ . In the Lagrangian applications, where (6.1) is the linear relaxation of a combinatorial problem, this yields both the bound and a primal solution of the relaxation. The theorem is the ancestor of the primal-recovery results listed in the timeline.

The mission produces a machine-checked version of the paper's Section 6, together with the input the paper takes on citation: Poljak's convergence theorem for divergent-series step sizes, specialized to piecewise-linear concave functions. Neither Poljak's theorem nor Theorem 6.3 is in Mathlib. The pieces are reusable: the convergence theorem applies to every Lagrangian dual solved by subgradient steps, and the duality between $\max w$ and (6.1) is linear-programming duality for a minimum of affine functions.

Difficulty

The inequality $\operatorname{Value}P(J,J^*)\ge\operatorname{Value}(6.1)$ is immediate, since aggregation maps feasible points to feasible points with the same objective. All of the content lies in the reverse inequality. That inequality ties a finite linear program to the limit of an infinite sequence, and it must hold for an arbitrary choice among tied minimizing indices. The iterates themselves need not converge, and under (2.7) the values $w(\pi^j)$ are not monotone. So an argument that inspects a single iterate, or assumes that the method settles on one face of $w$ , fails. The convergence statement of milestone 2 is not proved in the paper and is the heaviest single step. Feasibility of $P(J,J^*)$ also needs its own argument, and it fails without the boundedness hypothesis.

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), the index set is a finite nonempty type ι, and $w$ is the finite minimum Finset.univ.inf'. A run is the predicate IsSubgradientRun c v t π k: positive steps, a minimizing index at every step, and update (2.6). It is not a function of $\pi^0$ , so every tie-breaking rule is covered. (2.7) is StepSizeCond t: t → 0, and the partial sums tend to $+\infty$ . Iterates are indexed from $j=0$ . Boundedness is Bornology.IsBounded (Set.range π). The variables of $P(J,J^*)$ are a function on $\mathbb N$ of which only the values at $J\le j\le J^*$ enter. Optimality of $y$ in either linear program means feasibility plus an objective no larger than that of every feasible point. Suprema are never taken over unbounded sets: every maximum of $w$ is stated as attained at an explicit $\pi^*$ .

A statement that only asserts feasibility of $P(J,J^*)$ , or only $\operatorname{Value}P\ge\operatorname{Value}(6.1)$ , is not the theorem. The goal requires that the solutions of $P(J,J^*)$ be optimal for (6.1).

Theorem 6.1 is printed for the step rule (2.8), but its proof uses $w(\pi^j)\to w^*$ , the consequence of (2.7). The mission states it for (2.7), and its milestone title says so.

A complete development needs:

linear-programming duality for (6.1), including attainment;
the convergence theorem for divergent-series step sizes;
existence of a maximizer of a bounded-above minimum of finitely many affine functions;
basic facts on convex hulls of finitely many vectors in $E^n$ .

The first three are reusable well beyond this mission. Contributions of any of them, as standalone theorems, are welcome.

Selected references

M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
M. Held, 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
B. T. Poljak, A general method of solving extremum problems, Soviet Mathematics Doklady 8 (1967) 593–597.
B. T. Poljak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9 (1969) 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
H. D. Sherali, G. Choi, Recovery of primal solutions when using subgradient optimization methods to solve Lagrangian duals of linear programs, Operations Research Letters 19 (1996) 105–113. https://doi.org/10.1016/0167-6377(96)00019-3
T. Larsson, M. Patriksson, A.-B. Strömberg, Ergodic, primal convergence in dual subgradient schemes for convex programming, Mathematical Programming 86 (1999) 283–312. https://doi.org/10.1007/s101070050090

7 thms2 active usersReviewed

Control Theory Convex Optimization Linear algebra+2·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data IV: A Semidefinite Upper Bound on the Linear-Fractional Worst-Case Residual, Exact for Full PerturbationsResearch Paper

Motivation

Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data $A$ , $b$ are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose $x$ to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of $[A\ b]$ and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix $\Delta$ through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).

In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings $S$ and $G$ below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).

Setting

Vectors carry the Euclidean norm $\|v\|$ . For a matrix $X$ , $\|X\|$ is its largest singular value (operator norm between Euclidean spaces). Let $\mathcal D$ be a linear subspace of $\mathbb R^{N\times N}$ (the perturbation structure), and fix $A \in \mathbb R^{n\times m}$ , $b \in \mathbb R^n$ , $L \in \mathbb R^{n\times N}$ , $R_A \in \mathbb R^{N\times m}$ , $R_b \in \mathbb R^N$ , $D \in \mathbb R^{N\times N}$ . For $\Delta \in \mathcal D$ with $\det(I - D\Delta) \ne 0$ the perturbed data are

A(\Delta) = A + L\Delta(I - D\Delta)^{-1}R_A, \qquad b(\Delta) = b + L\Delta(I - D\Delta)^{-1}R_b .

With the normalization $\rho = 1$ (the paper's, with no loss of generality), the worst-case residual of $x \in \mathbb R^m$ is

r_{\mathcal D}(A,b,x) = \max_{\Delta \in \mathcal D,\ \|\Delta\| \le 1} \|A(\Delta)x - b(\Delta)\|

if $\det(I - D\Delta) \ne 0$ for every such $\Delta$ , and $+\infty$ otherwise (35). The commutant scalings are $\mathcal S = \{S = S^T : S\Delta = \Delta S\ \forall \Delta \in \mathcal D\}$ and $\mathcal G = \{G = -G^T : G\Delta = \Delta G\ \forall \Delta \in \mathcal D\}$ (37). The SDP constraint is

\mathcal F(\lambda,S,G,x) = \begin{bmatrix} \Theta & \begin{matrix} Ax - b \\ R_Ax - R_b\end{matrix} \\ \begin{matrix}(Ax-b)^T & (R_Ax - R_b)^T\end{matrix} & \lambda\end{bmatrix} \succ 0, \quad \Theta = \begin{bmatrix} \lambda I - LSL^T & -LSD^T + LG \\ -DSL^T + G^TL^T & S + DG - GD^T - DSD^T\end{bmatrix}. \qquad (38),(39)

Formalization targets

Goal: Theorem 5.2 (corrected)

For all $x$ and $\lambda$ :

\text{(a)}\quad S \in \mathcal S,\ G \in \mathcal G,\ S \succ 0,\ G\Delta \text{ skew } \forall \Delta \in \mathcal D,\ \mathcal F(\lambda,S,G,x) \succ 0 \ \Longrightarrow\ \lambda > r_{\mathcal D}(A,b,x);

\text{(b)}\quad \mathcal D = \mathbb R^{N\times N},\ \lambda > r_{\mathcal D}(A,b,x) \ \Longrightarrow\ \exists s > 0:\ \mathcal F(\lambda, sI, 0, x) \succ 0 .

Part (a) says the value of the SDP $\inf\{\lambda : (\lambda, S, G) \text{ feasible}\}$ (40) is an upper bound on $r_{\mathcal D}$ . Part (b) says this upper bound is exact for full perturbations, including the case $r_{\mathcal D} = \infty$ , where (40) is infeasible.

Milestones

Lemma 2.2, both directions: the full-block S-procedure. $\det(I - T_4\Delta) \ne 0$ and $T(\Delta) \succeq 0$ for all $\|\Delta\| \le 1$ if and only if $\|T_4\| < 1$ and a one-scalar LMI (10) holds (the "only if" under $T_2 \ne 0$ or $T_3 = 0$ ).
Lemma 2.3: sufficiency of the scaled LMI for a structured $\mathcal D$ , and its strict necessity for $\mathcal D = \mathbb R^{N\times N}$ .
§5.4, p. 1047: $\lambda > r_{\mathcal D}(A,b,x)$ if and only if a linear-fractional matrix function of $\Delta$ is positive definite on the structured unit ball.
§5.4, (38)–(39): the certificate (a) in the paper's own words.

Significance

The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate $(S, G)$ . Since $x$ enters (38) linearly, the same constraint can also be optimized over $x$ (Theorem 5.3, not part of this mission). For $\mathcal D = \mathbb R^{N\times N}$ the bound is exact, which covers the model $[A(\Delta)\ b(\Delta)] = [A\ b] + L\Delta[R_A\ R_b]$ and, as a special case, the unstructured problem of §3.

The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.

Difficulty

Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse $(I - D\Delta)^{-1}$ . The certificate is one LMI in which $\Delta$ does not appear, while the conclusion is about a rational function of $\Delta$ over a whole structured ball. The certificate also has to guarantee that $I - D\Delta$ is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating $\mathcal F$ at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only $\succeq$ , and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case $T_2 = 0$ is not covered by the S-lemma's regularity condition and has to be handled separately.

Formalization scope

Dimensions are Fin n, Fin m, Fin N; $\mathcal D$ is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with $\mathcal D = \mathbb R^{N\times N}$ as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. $\|\Delta\|$ is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.
$\lambda > r_{\mathcal D}(A,b,x)$ is the predicate ResidualBelow: every $\Delta \in \mathcal D$ with $\|\Delta\| \le 1$ has $\det(I - D\Delta) \ne 0$ and residual $< \lambda$ . It is false for every $\lambda$ when $r_{\mathcal D} = \infty$ . No real-valued supremum is used, so the $\infty$ branch of (35) cannot turn into a default $0$ . Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.
$\rho = 1$ throughout, as in the paper; general $\rho$ follows by scaling $\Delta$ .
Corrections of the printed statements. (i) (40) must require $S \succ 0$ . Without it, $N = n = m = 1$ , $D = 2$ , $L = 1$ , $A = b = R_A = R_b = 0$ , $x = 0$ , $S = -1$ , $G = 0$ satisfy (38) for every $\lambda > 1/3$ , while $r_{\mathcal D} = \infty$ . (ii) $G$ must make $G\Delta$ skew-symmetric for every $\Delta \in \mathcal D$ , which is the identity $p^TGq = 0$ used in the proof of Lemma 2.3. For $\mathcal D = \operatorname{span}\{I, J\}$ , $J = \begin{bmatrix}0&1\\-1&0\end{bmatrix}$ , the printed bound certifies $\lambda = 3/2$ for an instance with worst-case residual $2$ . The added condition holds automatically when every element of $\mathcal D$ is symmetric (e.g. the diagonal structures (36)) and when $G = 0$ (e.g. $\mathcal D = \mathbb R^{N\times N}$ ). (iii) Lemma 2.2's "only if" is stated under $T_2 \ne 0$ or $T_3 = 0$ . (iv) Lemma 2.3's necessity is stated in strict form, and its sufficiency concludes $T(\Delta) \succ 0$ .
Not stated: "If $\Theta > 0$ at the optimum, the upper bound is also exact". The infimum over the strict LMI (38) is not attained, and the paper does not say which limit is meant. Theorem 5.3, Lemma 2.4 and Lemma 5.1 are also not stated.
Trivializing encodings ruled out: the goal is not a statement about the value of an infimum (which a junk value could satisfy), and the added hypotheses are satisfiable (for instance $S = sI$ , $G = 0$ for full $\mathcal D$ , which part (b) produces).
Infrastructure needed: the Schur complement for block matrices (in Mathlib), a lossless S-lemma for two homogeneous quadratic forms in strict and non-strict form (the platform has ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with $\mathcal D$ , and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.

Selected references

L. El Ghaoui and H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
M. K. H. Fan, A. L. Tits and J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36(1):25–38, 1991. https://doi.org/10.1109/9.62265
I. Pólik and T. Terlaky, A survey of the S-lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

8 thms2 active usersReviewed