Theoretical Computer Science

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 4.1

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.

Their headline answer is that both rules use at most about $\tfrac{17}{10}$ times the optimal number of bins, and that $\tfrac{17}{10}$ is asymptotically attained. The lists that force this ratio use items larger than $\tfrac12$. When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size $\alpha\le\tfrac12$.

Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a $\tfrac{17}{10}L^*+3$ bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most $\alpha$. The additive constants in the unrestricted $\tfrac{17}{10}$ bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that $FF(L)\le\lfloor\tfrac{17}{10}L^*\rfloor$.

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$. Its optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$. The level of a bin is the sum of the numbers in it. For a real $\alpha>0$, write $L\subseteq(0,\alpha]$ when every element of $L$ is at most $\alpha$.

First-Fit ($FF$) considers bins $B_1,B_2,\dots$, all initially empty, and places $a_1,a_2,\dots,a_n$ in that order: $a_i$ goes into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$. Best-Fit ($BF$) is the same except that, among the bins with $\beta\le 1-a_i$, it chooses one of largest level $\beta$ (least index among ties). $FF(L)$ and $BF(L)$ denote the numbers of nonempty bins at the end.

The restricted worst-case ratios are

$$R^\alpha_{FF}(k)=\max\Big\{\frac{FF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\},\qquad R^\alpha_{BF}(k)=\max\Big\{\frac{BF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\}.$$

Throughout, $0<\alpha\le\tfrac12$ and $m=\lfloor\alpha^{-1}\rfloor$, an integer with $m\ge 2$ and $\tfrac1{m+1}<\alpha\le\tfrac1m$.

Formalization targets

Goal: the asymptotic ratio (Corollary of Theorem 2.3, p. 308)

$$\lim_{k\to\infty}R^\alpha_{FF}(k)=\lim_{k\to\infty}R^\alpha_{BF}(k)=1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.$$

The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.

Theorem 2.3(i): the lower bound (p. 307)

For each $k\ge1$ there is a list $L\subseteq(0,\alpha]$ with $L^*=k$ and $FF(L)\ge\frac{m+1}{m}L^*-\frac1m$; likewise for $BF$.

Two steps of the First-Fit upper bound (p. 308)

If no element of $L$ exceeds $\frac1m$, then in the First-Fit packing every bin except possibly the last contains at least $m$ elements, and all but at most two bins have level at least $\frac{m}{m+1}$.

Theorem 2.3(ii): the upper bounds (p. 307)

For every list $L\subseteq(0,\alpha]$,

$$FF(L)\le\frac{m+1}{m}L^*+2,\qquad BF(L)\le\frac{m+1}{m}L^*+2.$$

Significance

The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is $\tfrac32$ when items are at most $\tfrac12$, $\tfrac43$ when at most $\tfrac13$, and tends to $1$ as the maximum item size tends to $0$. Combined with the $\tfrac{17}{10}$ bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than $\tfrac12$. Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.

The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.

Difficulty

For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.

The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.

The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of $m$, and computing $L^*$ exactly for that list, which needs a matching lower bound on the optimum.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$); $L\subseteq(0,\alpha]$ is the additional hypothesis ∀ a ∈ L, a ≤ α. $L^*$ is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least $j$" over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and $FF(L)$, $BF(L)$ are the lengths of the final bin lists. $m$ is Nat.floor α⁻¹, cast before any division.

The ratios $R^\alpha_{FF}(k)$, $R^\alpha_{BF}(k)$ are suprema taken in ℝ≥0∞: an unbounded family would give $+\infty$, never a default value, and at $k=0$ the only admissible list is empty and the value is $0$. The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned $0$ on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant $2$ and the lower bound the subtractive $\frac1m$ exactly as printed.

The two proof steps are stated under the proof's own hypothesis "no element exceeding $1/m$", which is weaker than $L\subseteq(0,\alpha]$.

A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound $L^*\ge\sum_i a_i$, and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about $L^*$ are reusable in the companion missions on the $\tfrac{17}{10}$, $\tfrac{11}{9}$ and $\tfrac{71}{60}$ bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• J. D. Ullman, The Performance of a Memory Allocation Algorithm, Technical Report 100, Princeton University, 1971.
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-Case Analysis of Memory Allocation Algorithms, Proc. 4th ACM Symposium on Theory of Computing, 143–150, 1972. https://doi.org/10.1145/800152.804907
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, Massachusetts Institute of Technology, 1973. http://hdl.handle.net/1721.1/57819
• G. Dósa, J. Sgall, First Fit Bin Packing: A Tight Analysis, Proc. 30th STACS, LIPIcs 20:538–549, 2013. https://doi.org/10.4230/LIPIcs.STACS.2013.538

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It is one of the first problems studied through the worst-case analysis of approximation algorithms, and it models storage allocation, paging and file placement on tracks, as well as cutting-stock problems in operations research. Deciding the optimum exactly is NP-hard, so the practical question is how badly simple rules can do. The two simplest on-line rules, First-Fit and Best-Fit, are still the baseline against which every later bin-packing heuristic is measured.

Timeline:

• 1972. Garey, Graham and Ullman announce that First-Fit uses at most about $1.7$ times the optimal number of bins (Proc. 4th ACM STOC, 1972); Johnson's thesis (MIT, 1973) develops the analysis.
• 1974. Johnson, Demers, Ullman, Garey and Graham prove $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list, and give lists with $FF(L)=BF(L)>1.7L^*-8$ for every optimum $L^*=k$, so the asymptotic worst-case ratio of both rules is exactly $\tfrac{17}{10}$ (SIAM J. Comput. 3(4)). This paper is the source of the mission.
• 1976–2014. The additive constant is lowered: Garey, Graham, Johnson and Yao (1976) show $FF(L)\le\lceil 1.7L^*\rceil$, and Dósa and Sgall prove the tight bound $FF(L)\le\lfloor 1.7L^*\rfloor$ (STACS 2013) and the same bound for Best-Fit (ICALP 2014).

Setting

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

Both rules place $a_1,\dots,a_n$ in this order into bins $B_1,B_2,\dots$, each initially at level $0$, and never move an element once placed.

1. First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$.
2. Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, taking the least index among ties.

$FF(L)$ and $BF(L)$ are the numbers of nonempty bins at the end. The worst-case ratio at optimum $k$ is

$$R_{FF}(k)=\sup\Bigl\{\frac{FF(L)}{L^*}:L^*=k\Bigr\},\qquad R_{BF}(k)=\sup\Bigl\{\frac{BF(L)}{L^*}:L^*=k\Bigr\}.$$

The analysis also uses a weighting function $W:[0,1]\to[0,1]$, piecewise linear with $W(\alpha)=\tfrac65\alpha$ on $[0,\tfrac16]$, $\tfrac95\alpha-\tfrac1{10}$ on $(\tfrac16,\tfrac13]$, $\tfrac65\alpha+\tfrac1{10}$ on $(\tfrac13,\tfrac12]$ and $1$ on $(\tfrac12,1]$, and the coarseness of a bin of a completed packing: the largest $1-\operatorname{level}(B')$ over the bins $B'$ of smaller index, and $0$ for the first bin.

Formalization targets

Goal: the asymptotic ratio (Corollary of Section 2, p. 306)

$$\lim_{k\to\infty}R_{FF}(k)=1.7\qquad\text{and}\qquad\lim_{k\to\infty}R_{BF}(k)=1.7.$$

The goal fixes only the asymptotic ratio and leaves the additive constants free, so it is the statement that survives the later improvements of the constants.

Milestones, in the order the proof uses them

• Claim 2.2.1 (p. 304): a bin with total size at most $1$ has $\sum_i W(b_i)\le\tfrac{17}{10}$.
• Claim 2.2.2 (p. 305): in an FF or BF packing, every element placed into a bin before the bin was more than half full exceeds the bin's coarseness.
• Claim 2.2.3 (p. 305): a bin of coarseness $\alpha<\tfrac12$ whose level exceeds $1-\alpha$ has weight at least $1$.
• Claim 2.2.4 (p. 306): a bin of coarseness $\alpha<\tfrac12$ with weight $1-\beta$, $\beta>0$, either holds a single element at most $\tfrac12$ or has level at most $1-\alpha-\tfrac59\beta$.
• Theorem 2.2 (p. 304): $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list.
• Theorem 2.1 (p. 301): for every $k\ge1$ there is a list with $L^*=k$ and $FF(L)=BF(L)>1.7L^*-8$.

A companion item, not a milestone, records the explicit list of Fig. 3 (p. 307) with $L^*=10$ and $FF(L)=BF(L)=17$.

Significance

The result fixes the worst-case behaviour of the two simplest bin-packing heuristics: neither ever uses more than about $70\%$ more bins than an optimal packing, and both can be forced to. The weighting-function technique introduced for this bound became the standard method for analysing bin-packing heuristics, including First-Fit Decreasing, Harmonic-type algorithms and on-line lower bounds, and the constant $\tfrac{17}{10}$ is the reference point for later on-line algorithms.

The theorem is proved, and its constants have since been sharpened. No machine-checked proof of any of these results is known. This mission produces a Lean model of on-line bin packing (the optimum, the First-Fit and Best-Fit runs with their placement history, and the worst-case ratio) that the other missions of this paper and later bin-packing formalizations can reuse. It also produces formal proofs of the weighting-function bounds, of the $1.7L^*+2$ upper bound and of the lower-bound construction.

Difficulty

The first idea, charging each bin its level, gives only $FF(L)\le 2L^*+1$: at most one bin is at most half full. The ratio $\tfrac{17}{10}$ comes from bins that are more than half full but far from full, and a bound on the total size of the elements cannot see them. No property of the final packing alone suffices: the bins that are far from full can only be controlled through the order in which the rule opened and filled them, so the argument depends on the dynamics of the run. On the lower-bound side, the natural periodic list (sizes near $\tfrac16,\tfrac13,\tfrac12$, p. 301) gives only the ratio $\tfrac53$; reaching $\tfrac{17}{10}$ needs a list on which both rules waste space in every medium bin, for every $k$, while $L^*$ is still known exactly.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$), and every statement assumes it. $L^*$ is optBins L, the least b : ℕ for which some assignment Fin L.length → Fin b has every bin sum at most $1$. A run is a fold over the list that keeps only the nonempty bins, in index order, each with its contents in placement order. A new bin is opened at the end exactly when no nonempty bin fits, which is the paper's "least $j$" over infinitely many initially empty bins, since elements are positive. The fit test is the non-strict $\beta+a_i\le1$, and Best-Fit breaks ties by least index. The placement history (the bin chosen for each element and that bin's level just before) is read off the run on the prefix of the list. Indices are $0$-based. Coarseness is computed in the completed packing. $W$ is a function ℝ → ℝ and is only ever applied to elements of $(0,1]$. $R_{FF}(k)$ and $R_{BF}(k)$ are suprema in the extended nonnegative reals $[0,\infty]$, and the limit is taken there.

A real-valued supremum would be $0$ on an empty or unbounded family, and the limit statement would then say nothing about the algorithms. The extended-real supremum rules this trivialization out. Every claim is stated for the concrete First-Fit run and the concrete Best-Fit run, not for an abstract rule with the properties used in the proof.

Claim 2.2.4 is printed with alternative (i) "$m=1$ and $b_1<\tfrac12$", which is false: First-Fit on $(0.6,0.5)$ gives a counterexample. The mission states it with $b_1\le\tfrac12$, which is what the paper's proof establishes and what the main proof uses. The milestone text keeps the printed version.

The model definitions are reusable for any on-line bin-packing rule, since the run is parameterized by the choice rule. Contributions welcome: proofs of the milestones, general lemmas about the runs (levels stay at most $1$, at most one bin is at most half full, the history determines the final packing), and the computation of $L^*$ for the explicit lists of Theorem 2.1 and Fig. 3.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-case analysis of memory allocation algorithms, Proc. 4th ACM STOC, 1972.
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, MIT, 1973.
• M. R. Garey, R. L. Graham, D. S. Johnson, A. C. Yao, Resource constrained scheduling as generalized bin packing, J. Combinatorial Theory Ser. A 21, 1976.
• G. Dósa, J. Sgall, First Fit bin packing: A tight analysis, STACS 2013, LIPIcs 20:538–549. https://doi.org/10.4230/LIPIcs.STACS.2013.538
• G. Dósa, J. Sgall, Optimal analysis of Best Fit bin packing, ICALP 2014, LNCS 8572.

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Corollary 2.7

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

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

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

Milestones

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

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

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

Companion statements, not milestones:

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

The uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation algorithms.

Local search is the simplest of these and the one most used in practice: start from any set of open facilities and repeatedly add, drop or exchange one facility while this lowers the cost. The question is how bad a solution can be when no such move helps. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) answered it for UFL with an exact constant.

Timeline. Korupolu, Plaxton and Rajaraman (SODA 1998, J. Algorithms 2000) analysed local search with add, drop and swap moves and proved a locality gap of at most 5; their analysis contains the service cost bound restated here as Lemma 4.1. Charikar and Guha (FOCS 1999) proved a locality gap of 3 for a different local search, in which one facility is added and any number are dropped. Arya et al. (STOC 2001; journal version 2004) proved that the add/drop/swap neighbourhood itself has locality gap at most 3, and gave an instance showing that 3 cannot be improved (§4.3).

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities, and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality. The cost of serving client $j$ by facility $i$ is $c_{ji} = d(j,i)$; the distance $c_{ii'}$ between two facilities is also available. Each facility $i \in F$ has an opening cost $f_i \ge 0$.

A solution is a nonempty set $S \subseteq F$ of open facilities. Every client is served by its nearest open facility, so

$$\mathrm{cost}_f(S) = \sum_{i \in S} f_i, \qquad \mathrm{cost}_s(S) = \sum_{j \in C} \min_{i \in S} c_{ji}, \qquad \mathrm{cost}(S) = \mathrm{cost}_f(S) + \mathrm{cost}_s(S).$$

The neighbourhood of $S$ is the set of solutions reachable by adding one facility, dropping one facility, or swapping one open facility for another:

$$\mathcal B(S) = \{S + \{s'\}\} \cup \{S - \{s\} \mid s \in S\} \cup \{S - \{s\} + \{s'\} \mid s \in S\}.$$

$S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The locality gap is the supremum, over all instances, of the ratio between the cost of a worst local optimum and the cost of a global optimum.

The proofs use the following notation, which appears in the milestones but not in the goal. Fix a second solution $O$ and nearest-facility assignments $\sigma_S : C \to S$, $\sigma_O : C \to O$; write $S_j = c_{j\sigma_S(j)}$, $O_j = c_{j\sigma_O(j)}$, $N_S(s) = \sigma_S^{-1}(s)$, $N_O(o) = \sigma_O^{-1}(o)$ and $N^o_s = N_O(o) \cap N_S(s)$. A facility $s \in S$ captures $o \in O$ if $|N^o_s| > \tfrac12 |N_O(o)|$; $s$ is good if it captures no facility of $O$ and bad otherwise. The proof of the facility cost bound uses a permutation $\pi$ of the clients that maps each $N_O(o)$ onto itself, moves every client of a non-capturing block $N^o_s$ out of that block (Property 3.1), and fixes every client of a capturing block that it would map into the same block.

Formalization targets

Goal: Theorem 4.3

$$\mathrm{cost}(S) \le 3 \cdot \mathrm{cost}(O) \quad \text{for every locally optimum } S \text{ and every solution } O.$$

This is the locality gap bound of Theorem 4.3 (p. 557) in its strongest printed form: $O$ is any solution, not only an optimal one.

Milestones

1. Lemma 4.1 (service cost), p. 554: $\mathrm{cost}_s(S) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$.
2. The refined mapping $\pi$ of the proof of Lemma 4.2, p. 555: such a permutation exists for any two assignments.
3. Inequality (5), p. 555: the drop move for a good facility $s$,

$$-f_s + \sum_{j \in N_S(s),\ \pi(j) \neq j} (O_j + O_{\pi(j)} + S_{\pi(j)} - S_j) + 2 \sum_{j \in N_S(s),\ \pi(j) = j} O_j \ge 0.$$

4. Inequality (6), pp. 555–556: the swap of a bad facility $s$ with the facility $o$ it captures that is nearest to it.
5. Inequality (8), p. 556: for a bad facility $s$ capturing the set $P \subseteq O$, the analogue of (5) with $\sum_{o' \in P} f_{o'} - f_s$ in place of $-f_s$.
6. Lemma 4.2 (facility cost), p. 555: $\mathrm{cost}_f(S) \le \mathrm{cost}_f(O) + 2 \cdot \mathrm{cost}_s(O)$.

A companion item, not a milestone, states the bound in the proof of Theorem 4.4 with $\alpha = \sqrt2$: a local optimum of the instance with facility costs $\sqrt2 f_i$ costs at most $(1+\sqrt2)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 4.3 shows that the simplest local search for metric UFL is within a factor 3 of optimal at every local optimum, with no LP and no rounding, and the tight example of §4.3 shows the analysis cannot be improved for this neighbourhood. Because Lemmas 4.1 and 4.2 hold against every solution $O$, scaling the facility costs before running local search trades the two bounds against each other and gives the $1 + \sqrt2 + \epsilon$ guarantee of Theorem 4.4. The same capture-and-reassign technique is used for k-median (§3) and capacitated facility location (§5).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any locality gap bound for facility location is known to this mission. A formal development would check the reassignment arguments, which are stated case by case in the paper, and would produce reusable Lean infrastructure for metric facility location instances, nearest-facility costs and neighbourhood-based local optimality.

Difficulty

The service cost bound is routine; the facility cost bound is where the work lies. The natural first idea, closing a facility $s \in S$ and sending each of its clients to the facility of $S$ nearest to that client's optimal facility, fails when $s$ serves most of the clients of some $o \in O$: the nearest facility of $S$ to $o$ may be $s$ itself, so the client has nowhere to go. The proof separates good facilities, which can be dropped, from bad ones, which must be swapped with a captured facility, and pays for the clients that cannot be moved through the distance between $s$ and its nearest captured facility. The combinatorial core is the construction of a permutation within each $N_O(o)$ that avoids every non-capturing block and has fixed points only where they are unavoidable.

Formalization scope

Clients and facilities are finite types Cl and Fa. The distance is a real-valued function on Cl ⊕ Fa that is nonnegative, symmetric and satisfies the triangle inequality; $d(x,x) = 0$ is not assumed, since the paper neither states nor uses it. Opening costs are a function f : Fa → ℝ with 0 ≤ f i, and demands are unit, as in the paper.

Solutions are nonempty Finsets. The service cost is $\sum_j \min_{i \in S} c_{ji}$ (Finset.inf') and is defined only for nonempty sets, so no junk value for $\emptyset$ enters. Accordingly the drop move is considered only when a facility remains open; with at least one client, $\emptyset$ cannot serve anyone and is not a solution. Local optimality is required for all moves of $\mathcal B(S)$: every added facility, every dropped facility and every swap, not only the moves used in the proof. The goal is stated as the multiplied-out inequality $\mathrm{cost}(S) \le 3\,\mathrm{cost}(O)$ for every nonempty $O$, never as a ratio, since $\mathrm{cost}(O)$ may be $0$.

In the milestones, the nearest-facility assignments $\sigma_S$, $\sigma_O$ are arbitrary among the nearest ones (ties broken arbitrarily), and the family of bijections $\pi : N_O(o) \to N_O(o)$ is a single permutation of the clients with $\sigma_O \circ \pi = \sigma_O$. Inequality (5) assumes at least one client, which the paper assumes implicitly: with no clients and $S = \{s\}$ it would read $-f_s \ge 0$. The goal and Lemma 4.2 need no such assumption.

A statement that assumes local optimality only for the moves the proof uses, that fixes $O$ to be a global optimum defined by hypotheses, or that allows the empty set a zero service cost would be a different theorem; none of these is used.

Needed infrastructure: sums over nearest-facility assignments and their fibers $N_O(o)$, the permutation $\pi$, and bookkeeping of the three kinds of moves. The instance, cost and local optimality definitions are reusable for other local search analyses of metric location problems. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• M. Charikar, S. Guha, Improved Combinatorial Algorithms for the Facility Location and k-Median Problems, FOCS 1999, 378–388. https://doi.org/10.1109/SFFCS.1999.814609

Motivation

Every generalization bound in Chapters 2-11 depends only on the complexity of a fixed hypothesis set $H$ — Rademacher complexity, VC-dimension, growth function — and holds regardless of which algorithm within $H$ actually returns the hypothesis. This is both a strength (broad applicability) and a limitation: it throws away everything specific to how an algorithm searches $H$, and can be uninformative when $H$ itself is large or unbounded (e.g. a regularized objective that implicitly restricts the search without shrinking $H$ as a set). Chapter 14 introduces a fundamentally different route to a generalization bound — a property of the algorithm rather than the hypothesis class — first used by Devroye, Rogers and Wagner for $k$-nearest-neighbor rules and given its modern general form by Bousquet and Elisseeff (2002), whose treatment this chapter follows and (for non-differentiable convex losses) extends.

Setting

A labeled example is $z=(x,y)\in X\times Y$; for a loss function $L:Y'\times Y\to\mathbb R_+$ (where $Y'$ may differ from $Y$, e.g. $Y=\{-1,+1\}$ but $Y'=\mathbb R$ for a real-valued hypothesis), the loss of a hypothesis $h$ at $z$ is $L_z(h)=L(h(x),y)$. Given a learning algorithm $A$ that maps a sample $S$ of size $m$ to a hypothesis $h_S\in H$, the empirical error and generalization error are $\hat R_S(h)=\frac1m\sum_iL_{z_i}(h)$ and $R(h)=\mathbb E_{z\sim D}[L_z(h)]$. Uniform $\beta$-stability (Definition 14.1) says: for any two samples $S$, $S'$ differing by a single point, the algorithm's returned hypotheses satisfy $|L_z(h_S)-L_z(h_{S'})|\le\beta$ for every $z$ — replacing one training point can change the algorithm's loss on any point by at most $\beta$. For the regularized algorithms studied in §14.3, a kernel-based regularization algorithm minimizes $F_S(h)=\hat R_S(h)+ \lambda\|h\|_K^2$ over the RKHS $H$ of a positive-definite kernel $K$, and a loss $L$ is $\sigma$-admissible (Definition 14.3) if $|L(h'(x),y)-L(h(x),y)|\le\sigma|h'(x)-h(x)|$ for all hypotheses $h,h'$ — a Lipschitz-like smoothness condition satisfied by the standard regression and classification losses.

Formalization targets

Proposition 14.4 (milestone). For a PDS kernel $K$ with $K(x,x)\le r^2$ and a convex, $\sigma$-admissible loss $L$, the kernel-based regularization algorithm is $\beta$-stable with

$$\beta \le \frac{\sigma^2r^2}{m\lambda}.$$

Corollary 14.5 (milestone). For SVR (the $\epsilon$-insensitive loss $L_\epsilon$, bounded by $M$), with probability at least $1-\delta$:

$$R(h_S) \le \hat R_S(h_S) + \frac{r^2}{m\lambda} + \Big(\frac{2r^2}\lambda+M\Big)\sqrt{\frac{\log(1/\delta)}{2m}}.$$

Theorem 14.2 — the mission's goal. For a loss bounded by $M$ and a $\beta$-stable algorithm $A$, with probability at least $1-\delta$ over a sample $S$ of size $m$:

$$R(h_S) \le \hat R_S(h_S) + \beta + (2m\beta+M)\sqrt{\frac{\log(1/\delta)}{2m}}.$$

Significance

Theorem 14.2 is the book's demonstration that algorithm-dependent analysis is not merely a special-case curiosity: it is broad enough to cover an entire family (every kernel-based regularization algorithm — KRR, SVR, SVMs, and beyond) uniformly, via a single stability coefficient computation (Proposition 14.4) that is then specialized per algorithm just by plugging in that loss's admissibility constant $\sigma$. Corollary 14.5's SVR bound is the concrete payoff: a fully explicit, dimension-free generalization guarantee for a widely used regression algorithm, with every constant ($r$, $\lambda$, $m$) traceable to the algorithm's own hyperparameters, no VC-dimension or Rademacher-complexity computation required. Unlike Chapters 3-11, whose bounds are oblivious to how $H$ is searched, algorithmic stability is the first tool in the book that can, in principle, certify generalization for a hypothesis class too large or poorly understood for a complexity-based bound to be informative, provided the algorithm itself is stable. No prior art on the Prove2Me platform is faithful: GET /theorems?q=algorithmic+stability, q=uniform+stability return no hits; q=McDiarmid returns only bounded_diff_martingale_two_sided (Boucheron-Lugosi-Massart's own two-sided bounded-differences martingale inequality), which is McDiarmid's inequality's own proof engine (the background result Theorem 14.2's proof applies), not any result of this chapter — a different mathematical object entirely, not reused. All eleven items are drafted fresh.

Not formalized here: Corollary 14.6 (KRR bound), Lemma 14.7 (boundedness of kernel-regularization hypotheses) and Corollary 14.8 (SVM bound). Corollary 14.6 is structurally identical to Corollary 14.5 (a different loss function's admissibility constant plugged into the same Proposition 14.4 + Theorem 14.2 chain) and adds no new formalization content beyond Corollary 14.5, already drafted; Lemma 14.7 and Corollary 14.8 are omitted together, since 14.8's own statement needs 14.7's bound on $|h_S(x)|$ to compute its explicit $M$ (unlike Corollary 14.5, which is given $M$ as a hypothesis) — a genuine additional formalization layer (the reproducing-kernel norm bound $|h_S(x)|\le r\sqrt{B/\lambda}$) disproportionate to a single further corollary within this mission's budget.

Difficulty

The chapter's central technical step is recognizing that $\beta$-stability plus the loss bound $M$ together give exactly the bounded-difference property McDiarmid's inequality needs, applied to $\Phi(S)=R(h_S)-\hat R_S(h_S)$ as a function of the sample: replacing one point of $S$ changes $R(h_S)$ by at most $\beta$ (stability applied to the population loss, an expectation over $z$) and changes $\hat R_S(h_S)$ by at most $\beta+M/m$ (stability on the $m-1$ shared points, plus the full loss bound $M/m$ on the one point that actually changed) — two different, asymmetric arguments that must be combined correctly to get $|\Phi(S)-\Phi(S')|\le 2\beta+M/m$, not merely "stability implies boundedness" asserted directly. Proposition 14.4's own proof (not formalized here beyond its statement) needs a generalized Bregman divergence to handle a possibly non-differentiable convex loss — an extension of Bousquet-Elisseeff's original argument the book credits to itself as novel — via the reproducing-kernel property and Cauchy-Schwarz to convert a divergence bound into a bound on $\|h-h'\|_K$, then back into a pointwise loss bound.

Formalization scope

IsRKHSOf/IsMinimizer are restated locally in Stability, byte-identical to chunk 06-kernels's own copies (a draft item cannot import another chunk's draft module); H is an abstract real inner-product space with an evaluation map ev : H → X → ℝ standing for "elements of H are functions on X", the same device chunk 06's own RKHS formalization uses, since Mathlib's abstract Hilbert spaces are not themselves spaces of functions. UniformlyStable fixes the sample size m as part of the algorithm's type (A : (Fin m → X × Y) → (X → Y')), matching the book's own standing convention of a fixed sample size m throughout the chapter. Proposition 14.4 is stated pairwise — for any two samples differing by one point and any minimizers of their respective regularized objectives, the pointwise loss bound holds — rather than fixing a global choice-function algorithm A, since the book's own proof picks an arbitrary minimizer of each objective without asserting uniqueness; Corollary 14.5 does fix a choice function A (one minimizer per sample), since Theorem 14.2's own statement needs a single algorithm evaluated across the whole product-measure sample space. No numerical constant in any of the three theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 14.2 only for the strict per-hypothesis loss bound (∀ h ∈ H, ∀ z, L_z(h) ≤ M) rather than the book's own weaker, algorithm-specific condition (hbound, ∀ S, ∀ z, L_z(A S) ≤ M) — the weaker hypothesis is kept, exactly matching the book's explicit statement that "a weaker condition suffices."

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 14.
• O. Bousquet, A. Elisseeff, "Stability and generalization," Journal of Machine Learning Research 2, 2002, 499-526.
• M. Kearns, D. Ron, "Algorithmic stability and sanity-check bounds for leave-one-out cross-validation," Neural Computation 11(6), 1999, 1427-1453.

Motivation

Maximum entropy (Maxent) models are a widely used family of density-estimation algorithms: given a sample and a set of features, they select the distribution that matches the empirical feature averages while being otherwise as "agnostic" (close to a prior, usually uniform) as possible — a principle that, notably, never requires specifying a parametric family of distributions to search over. This mission formalizes the theorem that explains why this works in practice: Maxent's primal optimization (over distributions, subject to feature-matching constraints) is exactly dual to an unconstrained maximum-likelihood problem over a specific, rich parametric family — the Gibbs distributions — even though the Maxent principle never mentions that family at all.

Setting

For a sample $S=(x_1,\dots,x_m)$ drawn i.i.d. from $D$ over a finite set $X$, and a feature map $\Phi:X\to\mathbb R^N$ with $\|\Phi\|_\infty\le r$, the Maxent principle seeks $p\in\Delta$ (the simplex of distributions over $X$) minimizing the relative entropy $D(p\|p_0)$ to a prior $p_0$, subject to $\|E_{x\sim p}[\Phi(x)]-E_{x\sim\hat D}[\Phi(x)]\|_\infty\le\lambda$ (problem 12.7). Introducing the indicator function $I_K$ ($0$ on $K$, $+\infty$ elsewhere) turns this into the unconstrained primal objective $F(p)=\tilde D(p\|p_0)+I_C(E_p[\Phi])$ (Eq. 12.8), with $C$ the feature-constraint set. A Gibbs distribution with parameter $w\in\mathbb R^N$ is $p_w(x)=p_0(x)e^{w\cdot\Phi(x)}/Z(w)$, $Z(w)$ the partition function (Eq. 12.9); its associated dual objective is $G(w)=\frac1m\sum_i\log\frac{p_w(x_i)}{p_0(x_i)}-\lambda\|w\|_1$ (Eq. 12.10) — note $-\frac1m\sum_i\log p_w(x_i)$ is exactly the empirical log-loss $L_S(w)$, so maximizing $G$ is minimizing an L1-regularized log-loss over the Gibbs family.

Formalization targets

Theorem 12.2 — the mission's goal (Maxent duality). $\sup_{w\in\mathbb R^N}G(w)=\min_pF(p)$. Furthermore, letting $p^*=\arg\min_pF(p)$ and $d^*=\sup_wG(w)$: for any $\epsilon>0$ and any $w$ with $|G(w)-d^*|<\epsilon$, $D(p^*\|p_w)\le\epsilon$.

Theorem 12.3 (Maxent L1-regularization generalization bound, milestone). Fix $\delta>0$. Let $\hat w$ solve the L1-regularized dual (12.12) with $\lambda=2R_m(H)+r\sqrt{\log(2/\delta)/(2m)}$. Then, with probability at least $1-\delta$,

$$L_D(\hat w) \le \inf_wL_D(w) + 2\|\hat w\|_1\Big[2R_m(H)+r\sqrt{\log(2/\delta)/(2m)}\Big].$$

Significance

Theorem 12.2 is one of the most striking dualities in the book: the Maxent principle, phrased purely in terms of closeness to a prior distribution, turns out to always produce a solution in the Gibbs family — not because that family was ever specified, but because relative entropy is the specific measure of closeness whose Fenchel conjugate is the log-partition function. This explains a whole zoo of models (log-linear models, exponential families, Gaussian and bimodal Gibbs distributions from quadratic features) as instances of a single duality theorem, and gives a computationally friendlier route to the (constrained, infinite-if-$X$-is-large) primal problem via the (unconstrained, $N$-dimensional) dual. The theorem's proof is a genuine application of conditional (Fenchel) strong duality, not an unconditional fact — this is, per the chapter's own brief, the sharpest trivialization risk in the entire mission series, since "strong duality always holds for convex problems" is false in general, and a formalization skipping the book's own qualification condition ($\lambda>0$, placing $u_0$ in the interior of the constraint set) would prove a different, potentially-false statement. No prior art on the platform is faithful: GET /theorems?q=maximum+entropy returns no hits, and Mathlib's generic Fenchel-conjugate machinery (Analysis/Convex/Conjugate) does not package the book's own specific qualification conditions as a single reusable theorem matching Theorem B.39 — reusing it inside a proof (not the audited statement) remains available to whoever proves this theorem later.

Not formalized here: Theorem 12.4 (a Bregman-divergence generalization of Theorem 12.2) and Theorem 12.5 (its L2-regularized concrete special case). BRIEF.md itself flags Theorem 12.4 as possibly too heavy and offers Theorem 12.5 as an easier alternative; this mission omits both, since even Theorem 12.5 requires a second, structurally parallel dual-objective-and-minimizer formalization (for L2 rather than L1 regularization) — disproportionate to this mission's budget once Theorem 12.2's own qualification-condition bookkeeping (the heaviest single item in this mission series) is accounted for. §12.1 (density estimation without features: ML/MAP), §12.7 (coordinate descent), and §12.8-12.9 (Bregman-divergence extensions, L2-regularization in general) are likewise out of scope, per BRIEF.md's own page-range restriction.

Difficulty

Theorem 12.2's proof is the book's own explicit application of the Fenchel duality theorem (Theorem B.39, Appendix B) to the specific triple $f(p)=\tilde D(p\|p_0)$, $g(u)=I_C(u)$, $Ap=\sum_xp(x)\Phi(x)$ — every qualification condition (A a bounded linear map, u_0\in A(\mathrm{dom}f)\cap\mathrm{cont}(g), needing \lambda>0 to place u_0 in int(C)) must be checked for this triple, not assumed generically; the conjugate computations themselves (f^*(q)=\log\sum_xp_0(x)e^{q(x)}$ via Lemma B.37, g^(w)=E_{\hat D}[w\cdot\Phi]+\lambda|w|_1 via the dual-norm identity) are specific algebraic derivations, not immediate from abstract duality alone. The second clause's proof needs a further, non-obvious algebraic identity (G(w)-D(p^|p_0)+D(p^|p_w)expanding, via Hölder's inequality applied to the primal feasibility ofp^, to something \le0) that is not a restatement of the first clause but a separate argument built on top of it. Theorem 12.3's proof structurally mirrors chunk 04's SRM bound (bounding L_D(\hat w)-L_S(\hat w)via Hölder's inequality and the Rademacher-complexity feature-concentration bound of Eq. 12.5, then using\hat w`'s optimality twice), but is applied to the log-loss of a Gibbs distribution rather than a generic bounded loss.

Formalization scope

MaxEntPrimalObjective uses EReal (the extended reals) so that the book's own +\infty values (from I_K, \tilde D) are represented exactly, matching the chapter's own explicit use of an extended-real-valued indicator function rather than a soft penalty — a trivializing formalization this mission avoids is silently replacing +\infty with a large real sentinel, which would misstate a convex-analysis object whose entire role in the proof is its infinite value outside the feasible/simplex set. hlam : 0 < lam is a genuine load-bearing hypothesis in the goal theorem, matching the book's own use of \lambda>0 to invoke Theorem B.39's qualification condition — not a free convexity assumption; this is the mission's central faithfulness guard against the chapter's own named trivialization risk. EmpiricalRademacherComplexity/ RademacherComplexity are restated locally, byte-identical to chunks 05-svm/07-boosting's own copies (a draft item cannot import another chunk's draft module). p^* in the goal theorem and \hat w in Theorem 12.3 are both quantified via explicit hypotheses (IsLeast, a minimizer inequality) rather than assumed to exist unconditionally, matching the book's own "let p^*=..."/"let \hat w be a solution of..." phrasing without asserting existence or uniqueness beyond what the book itself asserts. No numerical constant in either theorem is altered from the book's own displayed form.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 12, §12.1-12.6.
• E. T. Jaynes, "Information theory and statistical mechanics," Physical Review 106(4), 1957, 620-630.
• S. Della Pietra, V. Della Pietra, J. Lafferty, "Inducing features of random fields," IEEE Transactions on Pattern Analysis and Machine Intelligence 19(4), 1997, 380-393.