The OR Formalization Drive

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$, which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

• 1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
• 1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$.
• 1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
• 1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
• Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$, where $1\le k\le\min(m,n)$, keeps $k$ rows and $k$ columns of $A$. The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$. So $\Delta(0)=0$, and $\Delta(A)\ge 1$ whenever $A\ne 0$. Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$.

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$. An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$. For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$. A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$, $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$.

If $ay\le\beta$ for all $y\in P$, with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$. The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$. Then $P_I\subseteq P^{(i)}$ for all $i$. The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$. The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$.

Formalization targets

Goal: Theorem 10 (p. 260)

$$\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.$$

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$.

Milestones, in attack order

1. Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$-distance $n\Delta(A)$, and every IP optimum has an LP optimum within the same distance.
2. Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$.
3. Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$. This result is off the goal's path.
4. Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$-distance $n\Delta(A)$.
5. Theorem 7 (p. 257). A single integral matrix $M$, with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
6. Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$.
7. Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$.

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$. They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$: polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$. That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$. Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$, and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

• Rationality. Everything is over $\mathbb{Q}$, following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$, and a polyhedron is a finite system of rational inequalities.
• $\Delta(A)$. Only nonempty submatrices count, so $\Delta(0)=0$.
• Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
• Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$, using all integral $a$ and rational $\beta$. The rank is valued in $\mathbb{N}\cup\{\infty\}$, with $\infty$ if no iterate equals $P_I$. A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$, as printed.
• Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$. For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
• Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$.

A complete development needs the following:

• cone generation with Cramer bounds and Carathéodory's theorem;
• LP duality and Farkas' lemma over $\mathbb{Q}$;
• the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
• Schrijver's face lemma and unimodular invariance;
• a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

• W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
• V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
• A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
• W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
• F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322

Motivation

Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of $m$ ads out of $d$, a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of $d$ arms) and is a standard model in online advertising, routing and ranking.

Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret $O(\sqrt{mdn})$ with no logarithmic factor. For $m=1$ this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).

Setting

Vectors live in $\mathbb R^d$. The arm set is a nonempty $\mathcal C\subseteq\{0,1\}^d$ with $\|v\|_1=m$ for every $v\in\mathcal C$, and $\mathcal K=\mathrm{Conv}(\mathcal C)$. An oblivious adversary fixes loss vectors $\ell_1,\dots,\ell_n\in[0,1]^d$. In round $t$ the learner plays a random arm $v_t\in\mathcal C$, pays $\ell_t^\top v_t$, and observes $(\ell_t(1)v_t(1),\dots,\ell_t(d)v_t(d))$. The pseudo-regret is

$$\bar R_n=\mathbb E\sum_{t=1}^n\ell_t^\top v_t-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t^\top x .$$

A Legendre function on $\bar D$, for a nonempty open convex $D$, is a continuous $F:\bar D\to\mathbb R$ that is strictly convex and $C^1$ on $D$ and whose gradient norm tends to $+\infty$ at $\bar D\setminus D$. Its Bregman divergence is $D_F(x,y)=F(x)-F(y)-(x-y)^\top\nabla F(y)$, and its Legendre–Fenchel transform is $F^*(u)=\sup_{x\in\bar D}(x^\top u-F(x))$.

Online Mirror Descent with learning rate $\eta>0$ and vectors $g_t$ starts at $x_1\in\arg\min_{\mathcal K}F$. It then sets $\nabla F(w_{t+1})=\nabla F(x_t)-\eta g_t$ and $x_{t+1}=\arg\min_{y\in\mathcal K}D_F(y,w_{t+1})$. OSMD uses a random estimate $g_t=\tilde\ell_t$ of the loss. In the semi-bandit case it plays $v_t$ with $\mathbb E[v_t\mid x_t]=x_t$ and uses

$$\tilde\ell_t(i)=\frac{\ell_t(i)\,v_t(i)}{x_t(i)}. \tag{5.5}$$

A $0$-potential is a convex, $C^1$, increasing $\psi:(-\infty,a)\to(0,\infty)$ with $\psi(-\infty)=0$, $\psi(a^-)=+\infty$ and $\int_0^1|\psi^{-1}|<\infty$. It defines the Legendre function $F_\psi(x)=\sum_i\int_0^{x_i}\psi^{-1}(s)\,ds$ on $[0,\infty)^d$. With $\psi=\exp$ this is the negative entropy.

Formalization targets

Goal: Theorem 5.7 (p. 80)

For every $0$-potential $\psi$ and non-negative unbiased estimates,

$$\bar R_n\le\frac{\sup_{\mathcal K}F_\psi-F_\psi(x_1)}{\eta}+\frac\eta2\sum_{t=1}^n\sum_{i=1}^d\mathbb E\left[\frac{\tilde\ell_t(i)^2}{(\psi^{-1})'(x_t(i))}\right].$$

For $\psi(x)=(-x)^{-q}$ with $q>1$, the estimate (5.5) and $\eta=\sqrt{\tfrac{2}{q-1}\,m^{1-2/q}/(n\,d^{1-2/q})}$,

$$\bar R_n\le q\sqrt{\tfrac{2}{q-1}\,mdn},\qquad\text{and }\ \bar R_n\le2\sqrt{2mdn}\ \text{ at }q=2.$$

Milestones

1. Lemma 5.1: $F^{**}=F$, $\nabla F^*=(\nabla F)^{-1}$ on $D^*$, and $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$.
2. Lemma 5.2: existence, uniqueness and the Pythagorean inequality of Bregman projections.
3. Theorem 5.3: $\sum_t\ell_t(x_t)-\sum_t\ell_t(x)\le\frac{F(x)-F(x_1)}\eta+\frac1\eta\sum_tD_{F^*}(\nabla F(x_t)-\eta\nabla\ell_t(x_t),\nabla F(x_t))$.
4. Theorem 5.5, linear losses, and its corrected general form.
5. Lemma 5.3: $F_\psi$ is Legendre and $D_{F_\psi^*}(u,v)\le\frac12\sum_i\psi'(v_i)(u_i-v_i)^2$ for $u\le v$.
6. Theorem 5.6: with the negative entropy, $\bar R_n\le\sqrt{2mdn\ln(d/m)}$.

Significance

Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the $\sqrt{\ln(d/m)}$ factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.

All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside $D$ and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant $q\sqrt{2mdn/(q-1)}$, with two of the printed statements corrected (below).

Difficulty

The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of $D$. Another is the differentiability of $F^*$ on the open dual space and the identity $\nabla F^*=(\nabla F)^{-1}$. A third is the closed form of $F_\psi^*$ for a potential defined through an improper integral of $\psi^{-1}$.

The probabilistic step is not a martingale argument. Only conditioning on the current iterate $x_t$ is available. The estimate (5.5) divides by $x_t(i)$, so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, $\sum_ix_1(i)^{1-1/q}\le m^{(q-1)/q}d^{1/q}$, and the matching bound $\sum_ix_t(i)^{1/q}\le m^{1/q}d^{1-1/q}$.

Formalization scope

Vectors are Fin d → ℝ. The arm set is a Set of $0/1$ vectors with coordinate sum $m$, and $\mathcal K$ is convexHull ℝ C. Rounds are $t=1,\dots,n$, sums run over Finset.Icc 1 n, and index $0$ is unused. A randomized run is a family of measurable processes $x_t, v_t, \tilde\ell_t, w_t$ on a probability space, with the deterministic OMD recursion holding on every sample path. $\mathbb E[\cdot\mid x_t]$ is the coordinatewise conditional expectation given $\sigma(x_t)$, which is exactly what the book's proofs use. Losses are oblivious, so $\bar R_n\le B$ is stated as "for every $x\in\mathcal K$, $\mathbb E\sum_t\ell_t^\top v_t-\sum_t\ell_t^\top x\le B$". $F^*$ is valued in EReal, and $D_{F^*}$ is evaluated only on the open dual space, where $F^*$ is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then $+\infty$ and trivial, while Lean's integral would be $0$.

Corrections and instantiations, each labelled in the item's Formalization Note:

• Theorem 5.7, corrected misprint. The book prints $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{d^{1-2/q}}}$. The proof (p. 81) gives the stated bound only for $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{n\,d^{1-2/q}}}$, which is stated. At $q=2$ this is $\eta=\sqrt{2/n}$.
• Theorem 5.5, corrected misprint. In the first bound the book prints $\mathbb E[\|x_t-\tilde x_t\|\,\|\tilde g_t\|_*]$. That statement fails for $\ell_t(x)=x^2$ on $[-1,1]$ with $F=x^2/2$ and $\tilde x_t=\pm1$. The version stated uses $\|\nabla\ell_t(\tilde x_t)\|_*$, as the proof's first inequality does. The linear-loss bound is stated as printed.
• Lemma 5.2. "For all $z\in K\cap D$" is read as "for the projection $z$", which lies in $K\cap D$.
• Hypotheses made explicit: $q>1$; non-negativity of the estimates in Theorem 5.6 (used in its proof); unbiasedness $\mathbb E[\tilde\ell_t\mid x_t]=\ell_t$ in the general parts of Theorems 5.6 and 5.7; $\mathcal K\cap(0,\infty)^d\ne\emptyset$ (OMD's requirement $K\cap D\ne\emptyset$); a subgradient selection as an explicit input.
• Theorem 5.6's particular bound uses the book's $\eta=\sqrt{\frac{2m}{nd}\ln\frac dm}$ as printed. There are no O(·) constants in the chapter's statements.

A trivializing formalization would let $\eta$, $x_t$ or the estimate be junk values: an OSMD step at $\eta=0$, a Lean division $x/0=0$, or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in $\mathcal K$.

Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the $\omega$-potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012; arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921
• J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in online combinatorial optimization, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0598

Motivation

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

Timeline of the asymptotic regime the paper builds on:

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

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 5.1

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6.2, tuned

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3.3.13

For every locally quasiconcave $f$,

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

In many sequential decision problems the learner sees side information before acting. A news site chooses an article for a visitor whose history and location it knows; an ad server chooses an advertisement for a query. Only the reward of the chosen action is observed. These are contextual bandit problems, and Chapter 4 of Bubeck and Cesa-Bianchi's monograph Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems (arXiv:1204.5721v2) surveys several of their formal versions. In a contextual problem the learner is compared with the best policy, a map from contexts to arms, rather than with the best single arm.

This mission covers three of the chapter's models. The first marks each round with a context from a finite set. In the second, $N$ experts give advice, as in prediction with expert advice. The third is the bandit multiclass problem: a linear classifier predicts one of $K$ labels and then learns only whether its prediction was right. The goal is the mistake bound of the Banditron (Kakade, Shalev-Shwartz and Tewari, ICML 2008). The bound shows that one bit of feedback per round suffices to compete with every linear classifier, at regret $O(n^{2/3})$.

Setting

There are $K \ge 2$ arms (or labels) $\{1,\dots,K\}$ and rounds $t = 1, \dots, n$.

Adversarial losses. At round $t$ an adversary assigns losses $\ell_{i,t} \in [0,1]$ to the arms and may adapt to the forecaster's past plays $I_1, \dots, I_{t-1}$. The forecaster draws $I_t$ at random from a distribution $p_t$ that depends on what it has observed, and it observes only $\ell_{I_t,t}$. Expectations $\mathbb E$ are over the forecaster's draws.

Side information. Each round carries a context $s_t$ from a finite set $\mathcal S$, and the sequence $s_1, s_2, \dots$ is fixed in advance. The pseudo-regret against context-to-arm maps is

$$\overline R^{\mathcal S}_n = \max_{g:\mathcal S\to\{1,\dots,K\}} \mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \ell_{g(s_t),t}\Big].$$

The S-Exp3 forecaster runs one instance of Exp3 (Section 3.1 of the book) on each context.

Expert advice. At each round each of $N$ experts $j$ proposes a distribution $\xi^j_t$ over arms, which may depend on the forecaster's past plays. The contextual pseudo-regret is

$$\overline R^{\mathrm{ctx}}_n = \max_{k=1,\dots,N}\mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \mathbb E_{i\sim\xi^k_t}\ell_{i,t}\Big].$$

Exp4 (Fig. 4.1) runs exponential weights over the experts with importance-weighted loss estimates.

Bandit multiclass. The examples $(x_t, y_t) \in \mathbb R^d \times \{1,\dots,K\}$ are fixed in advance, with $\|x_t\| = 1$ (Euclidean). A $K\times d$ matrix $U$ classifies $x$ by $\arg\max_i (Ux)_i$. Its multiclass hinge loss on round $t$ is $\ell_t(U) = [1 - (Ux_t)_{y_t} + \max_{i\neq y_t}(Ux_t)_i]_+$. Write $L_n(U) = \sum_{t\le n}\ell_t(U)$ for the cumulative hinge loss, $\bar L_n(U) = L_n(U)/n$ for its average, and $\|U\|$ for the Frobenius norm. The multiclass Perceptron predicts $\hat y_t = \arg\max_i (W_tx_t)_i$ and, after seeing $y_t$, adds $x_t$ to row $y_t$ and subtracts it from row $\hat y_t$. The Banditron (p. 58) predicts $Y_t$ from $p_{i,t} = (1-\gamma)\mathbb 1_{\hat y_t = i} + \gamma/K$. It observes only $\mathbb 1_{Y_t = y_t}$ and updates $W_{t+1} = W_t + \widetilde X_t$, where $(\widetilde X_t)_{i,j} = x_{t,j}\big(\mathbb 1_{Y_t=y_t}\mathbb 1_{Y_t=i}/p_{i,t} - \mathbb 1_{\hat y_t=i}\big)$. Its number of mistakes is $M_n = \sum_{t\le n}\mathbb 1_{Y_t\neq y_t}$.

Formalization targets

Goal: Theorem 4.7 (Banditron)

For $n \ge 8K$, $\gamma = (K/n)^{1/3}$, every example sequence as above and every $K\times d$ matrix $U$,

$$\mathbb E\,M_n \le L_n(U) + \Big(1 + \|U\|\sqrt{2\bar L_n(U)}\Big)K^{1/3}n^{2/3} + 2\|U\|^2K^{2/3}n^{1/3} + \sqrt2\,\|U\|K^{1/6}n^{1/3}.$$

Milestones

1. Multiclass Perceptron bound (Section 4.4, p. 57). For every $n \ge 1$ and $U$, $\sum_{t\le n}\mathbb 1_{\hat y_t\ne y_t} \le L_n(U) + 2\|U\|^2 + \|U\|\sqrt{2n\bar L_n(U)}$.
2. Theorem 4.1 (p. 44). S-Exp3 satisfies $\overline R^{\mathcal S}_n \le \sqrt{2n|\mathcal S|K\ln K}$.
3. Theorem 4.2 (p. 46), with corrected constants. Exp4 without mixing satisfies $\overline R^{\mathrm{ctx}}_n \le \sqrt{2nK\ln N}$ for $\eta_t = \sqrt{2\ln N/(nK)}$, and $\overline R^{\mathrm{ctx}}_n \le 2\sqrt{nK\ln N}$ for $\eta_t = \sqrt{\ln N/(tK)}$.
4. Theorem 4.3 (p. 50), with corrected learning rate. Let the plays be drawn from distributions $q_t$ with $q_{i,t}\ge\varepsilon > 0$, and let Exp3 run on the estimates $\ell_{i,t}\mathbb 1_{I_t=i}/q_{i,t}$ with $\eta = \sqrt{2\varepsilon\ln K/n}$. Then $\max_k \mathbb E\big[\sum_t \mathbb E_{i\sim p_t}\ell_{i,t} - \sum_t\ell_{k,t}\big] \le \sqrt{(2n/\varepsilon)\ln K}$.

Significance

Theorem 4.7 shows that, on any sequence of examples, the bandit version of online multiclass classification costs at most $O(K^{1/3}n^{2/3})$ mistakes beyond the hinge loss of the best linear classifier. The full-information Perceptron, by comparison, pays $O(\sqrt n)$. The bound has no stochastic assumption and has explicit constants. Theorems 4.1–4.3 are the basic regret guarantees for side information and expert advice. Theorem 4.3 in particular lets learning algorithms serve as experts inside Exp4, which is the construction behind Theorem 4.5.

The mission produces machine-checked statements, and eventually proofs, of these results with fully explicit constants and an explicit model of adaptive adversaries and adaptive advice. To the curators' knowledge none of the Banditron, the multiclass Perceptron bound, S-Exp3 or Theorem 4.3 is formalized anywhere. The platform's Bandit Algorithms series has a proved Exp4 bound, but only for advice and rewards fixed in advance. The book proves all four milestones and the goal; two printed statements (4.2 and 4.3) contain misprints that this mission corrects.

Difficulty

The Banditron bound concerns a randomized process whose weight matrix depends on all earlier random predictions. The Perceptron argument tracks $\langle U, W_{n+1}\rangle$ and $\|W_{n+1}\|^2$. It carries over only in conditional expectation, and the second moment of the importance-weighted update is of order $K/\gamma$ on rounds where $\hat y_t \neq y_t$ and of order $\gamma$ otherwise. Combining these into one inequality for $\sum_t\mathbb P(\hat y_t\neq y_t)$ and then for $\mathbb E M_n$ requires solving a quadratic inequality in the presence of expectations, and the constants must come out as printed. For the Exp3/Exp4 results, the obstacle is that losses and advice adapt to past plays. The standard potential argument has to be run conditionally on the history, and a version that fixes the losses in advance proves a weaker theorem.

Formalization scope

• Rounds and laws. Rounds are numbered from $0$ in Lean (Lean round $t$ is the book's round $t+1$). Every forecaster is a sampling rule from past plays to weights on Fin K. The law of the first $n$ plays is the product $\prod_t p_t(\omega_t\mid\omega_{<t})$ over sequences $\omega : \mathrm{Fin}\,n\to\mathrm{Fin}\,K$, and expectations are finite sums against it. The adversary and the experts are deterministic functions of past plays; an independent randomized adversary is a mixture of these. The examples of the Banditron are fixed.
• Argmax. $\hat y_t$ uses any argmax selector; all tie-breaking rules are covered.
• Norms. $\|x_t\| = 1$ is the Euclidean condition $\sum_j x_{t,j}^2 = 1$; $\|U\|$ is the Frobenius norm written out explicitly.
• Infima and maxima. Each "$\inf_U$" and "$\max_k$" of the book is stated as "for every $U$" or "for every $k$", which is equivalent.
• Explicit constants. Every bound is the one printed or, for the corrected items, the one the proof yields. No $O(\cdot)$ appears.
• Corrected misprints. Theorem 4.7 prints the examples in $\mathbb R^d\times\{-1,+1\}$; labels are in $\{1,\dots,K\}$. Theorem 4.2 prints $\sqrt{2nN\ln K}$ and $2\sqrt{nN\ln K}$; the proof gives $\sqrt{2nK\ln N}$ and $2\sqrt{nK\ln N}$. Theorem 4.3 prints $\eta = \sqrt{2\ln K/(nK)}$; (4.7) follows from the proof with $\eta = \sqrt{2\varepsilon\ln K/n}$.
• Parameter range. At $n = 8K$ the Banditron's $\gamma$ equals $1/2$, outside the box's open interval $(0,1/2)$. The proof uses only $\gamma\le 1/2$, so $n = 8K$ is included.
• Ruling out trivial forms. Theorem 4.1 is stated for the explicit S-Exp3 forecaster, not as an existence claim, so no forecaster tuned to the losses can witness it. The losses and the advice are allowed to adapt, so a proof for oblivious sequences does not suffice.
• Left out. Theorem 4.4 (Exp4 with mixing) is proved in the book only by reference. The argument that reference suggests yields $\tfrac32\gamma n + K\ln N/\gamma$, not the printed $\gamma n/2 + K\ln N/\gamma$. Theorem 4.5 is stated with $O(\cdot)$, Theorem 4.6 "for some constant $c$", and Eq. (4.8) is left to the reader.

Useful reusable infrastructure: the path-law expectation for history-dependent sampling, the exponential-weights potential argument under adaptive losses, and Perceptron-type inner-product arguments for matrices. Proofs of any milestone and of the goal are welcome.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721 ; https://doi.org/10.1561/2200000024
• S. M. Kakade, S. Shalev-Shwartz, A. Tewari, Efficient Bandit Algorithms for Online Multiclass Prediction, ICML 2008. https://doi.org/10.1145/1390156.1390212
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• O.-A. Maillard, R. Munos, Adaptive Bandits: Towards the Best History-Dependent Strategy, AISTATS 2011. https://proceedings.mlr.press/v15/maillard11a.html