Operations Research

Motivation

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through $n$ points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' $3/2$ algorithm, the double-tree $2$-approximation) are compared.

The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.

Setting

A traveling salesman graph on $n$ nodes is a complete graph with a distance $d(a,b)\in\mathbb R$ that is symmetric, $d(a,b)=d(b,a)$, nonnegative, $d(a,b)\ge 0$, and satisfies the triangle inequality $d(a,c)\le d(a,b)+d(b,c)$. A tour lists the nodes in a visiting order $\tau(0),\dots,\tau(n-1)$ and returns to $\tau(0)$; its length is the sum of the $n$ distances along it. OPTIMAL is the least length of a tour.

The nearest neighbor algorithm starts at an arbitrary node $\tau(0)$; having reached $\tau(k)$, it moves to a node $\tau(k+1)$ that minimizes $d(\tau(k),\cdot)$ over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to $\tau(0)$. The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.

The instances of the proof are built from a recursive family of weighted graphs. With $l_i=\frac16(4\cdot 2^i-(-1)^i+3)$ (so $l_1,l_2,l_3,l_4=2,3,6,11$), the graph $F_1$ is a triangle with unit weights, and $F_{i+1}$ consists of two copies of $F_i$ joined through one new node by two edges of length $1$ and two edges of length $l_i$. Each $F_i$ has $2^{i+1}-1$ nodes and a path $P_i$ from its start node to its middle node through every node, of length $L_i$ with $L_1=2$, $L_{i+1}=2L_i+2l_i$. The graph $G_i$ adds two closing edges to $F_i$, and $\bar G_i$ is the complete graph on the same nodes whose distance is the shortest-path distance of $G_i$.

Formalization targets

Goal: Theorem 2 (p. 566)

For each $m>3$ there is a traveling salesman graph with $n=2^m-1$ nodes and a nearest-neighbor tour on it such that

$$\frac{\mathrm{NEARNEIBER}}{\mathrm{OPTIMAL}}>\frac13\lg(n+1)+\frac49 .$$

The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.

Milestones, in the order the proof uses them

1. (2.12): the difference equation $L_{i+1}=2L_i+2l_i$, $L_1=2$, has the solution $L_i=\frac19(6\,i\,2^i+8\cdot2^i+(-1)^i-9)$.
2. $\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
3. (2.13)–(2.17): the shortest-path distances in $F_{i+1}$ between the seven named nodes $A,\dots,G$ of Fig. 1, e.g. $\overline{AG}=l_{i+2}-2$.
4. Property a): every edge of $G_i$ is a shortest path between its endpoints.
5. Property b): the nearest neighbor algorithm started at the start node of $\bar G_i$ can follow $P_i$ and return along the edge of length $l_i-1$.
6. The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$.
7. The exact ratio: the tour along $P_i$ has length $L_i+l_i-1$, so its ratio is $(L_i+l_i-1)/n$.
8. The inequality: $(L_i+l_i-1)/n>\frac13\lg(n+1)+\frac49$ for $i\ge3$.

The instance for $m$ is $\bar G_{m-1}$.

Significance

Theorem 1 of the same paper shows $\mathrm{NEARNEIBER}/\mathrm{OPTIMAL}\le\frac12\lceil\lg n\rceil+\frac12$ for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ($\frac13$ against $\frac12$) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor $2$ of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with $n$.

The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.

Difficulty

The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of $F_i$ are not shortened by embedding it into $F_{i+1}$. Property b) then needs that at each step of $P_i$ the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows $P_i$. Checking small cases by computer does not give either property for all $i$.

Formalization scope

Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries $d(a,a)=0$, a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.

Ratios are multiplied out: the goal is $(\frac13\log_2(n+1)+\frac49)\cdot\mathrm{OPTIMAL}<\mathrm{NEARNEIBER}$ together with $\mathrm{OPTIMAL}>0$, the paper's standing assumption (1.1). $\lg(n+1)$ is Real.logb 2 of $n+1$, as printed. Because of the strict inequality and the conjunct $\mathrm{OPTIMAL}>0$, the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.

In the construction the nodes of $F_i$, $G_i$, $\bar G_i$ are numbered $0,\dots,2^{i+1}-2$ from left to right (start node $0$, middle node $2^i-1$, right node $2^{i+1}-2$); in $F_{i+1}$ the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and $l_i$ is defined in $\mathbb R$ exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be $0$ for two nodes with no connecting walk, a case that does not arise because every $G_i$ and $F_i$ is connected. $L_i$ is defined by its difference equation; its identification with the length of the tour along $P_i$ is milestone 7. All construction statements assume $i\ge1$.

A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• M. Bellmore, G. L. Nemhauser, The Traveling Salesman Problem: A Survey, Operations Research 16(3):538–558, 1968. https://doi.org/10.1287/opre.16.3.538
• J. W. Gavett, Three Heuristic Rules for Sequencing Jobs to a Single Production Facility, Management Science 11(8):B166–B176, 1965. https://doi.org/10.1287/mnsc.11.8.B166
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, Graduate School of Industrial Administration, Carnegie Mellon University, 1976.

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

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a decision $x_t$ from a fixed set $D\subseteq\mathbb R^n$ and observes only the noisy cost of that one decision, whose expectation is a fixed but unknown linear function $\mu^\top x_t$. The model covers online routing, ad and product selection with feature vectors, and any sequential decision problem whose decision set is too large to enumerate but whose expected cost is linear in a known representation. The multi-armed bandit is the special case where $D$ is the set of standard basis vectors.

Dani, Hayes and Kakade (COLT 2008) analysed the algorithm ConfidenceBall₂, a generalization of Auer's LinRel (JMLR 2002), and proved that its regret is $O^*(n\sqrt T)$ with high probability for an arbitrary compact decision set, and that this is optimal up to logarithmic factors. Their confidence-ellipsoid construction became the template for later linear bandit algorithms (OFUL, LinUCB), and the ellipsoid-plus-potential analysis is the standard argument of the field (Lattimore and Szepesvári, Bandit Algorithms, Chapters 19–20).

Timeline: Auer (2002) introduced LinRel for finite decision sets; Dani, Hayes and Kakade (2008) extended it to arbitrary compact sets with the $O^*(n\sqrt T)$ bound and a matching $\Omega(n\sqrt T)$ lower bound; Rusmevichientong and Tsitsiklis (Math. Oper. Res. 2010) studied linearly parameterized bandits with dimension-dependent regret bounds; Abbasi-Yadkori, Pál and Szepesvári (NeurIPS 2011) sharpened the confidence ellipsoids with self-normalized martingale bounds.

Setting

Fix $n\ge1$ and a compact decision set $D\subseteq\mathbb R^n$ whose standard basis $e_1,\dots,e_n$ is a barycentric spanner: each $e_i\in D$ and every $x\in D$ lies in the cube $[-1,1]^n$. The paper's Section 5 adopts these coordinates without loss of generality. An unknown vector $\mu\in\mathbb R^n$ satisfies $|\mu^\top x|\le1$ for $x\in D$, and $x^*\in D$ minimises $\mu^\top x$.

On round $t=1,2,\dots$ the learner plays $x_t\in D$, measurable with respect to the information $\mathcal F_t$ before round $t$, and observes a loss $\ell_t\in[-1,1]$ with $\mathbb E[\ell_t\mid\mathcal F_t]=\mu^\top x_t$. The regret after $T$ rounds is

$$R_T=\sum_{t=1}^T\big(\mu^\top x_t-\mu^\top x^*\big).$$

ConfidenceBall₂$(D,\delta)$ maintains the design matrix $A_t=I+\sum_{\tau<t}x_\tau x_\tau^\top$, the least-squares estimate $\hat\mu_t=A_t^{-1}\sum_{\tau<t}\ell_\tau x_\tau$, the radius

$$\beta_t=\max\Big(128\,n\ln t\ln(t^2/\delta),\ \big(\tfrac83\ln(t^2/\delta)\big)^2\Big),$$

and the confidence ellipsoid $B^2_t=\{\nu:(\nu-\hat\mu_t)^\top A_t(\nu-\hat\mu_t)\le\beta_t\}$. It plays the optimistic decision $x_t\in\operatorname{argmin}_{x\in D}\min_{\nu\in B^2_t}\nu^\top x$. The analysis uses the width $w_t=\sqrt{x_t^\top A_t^{-1}x_t}$, the error $Z_t=(\hat\mu_t-\mu)^\top A_t(\hat\mu_t-\mu)$, and the noise $\eta_t=\ell_t-\mu^\top x_t$.

Formalization targets

Goal: Theorem 2, ConfidenceBall₂ bullet (corrected)

For $0<\delta<1$ with $n\le\beta_1$ and noise $|\eta_t|\le1$,

$$\Pr\Big(\forall T\ge1,\ R_T\le\sqrt{8nT\beta_T\ln(T+1)}\Big)\ge1-\delta.$$

A single event covers every horizon, so the bound is anytime.

Milestones

• Lemma 8. If $\mu\in B^2_t$ then $r_t\le2\min(\sqrt{\beta_t}w_t,1)$.
• Lemma 10. $\det A_{t+1}=\prod_{\tau=1}^t(1+w_\tau^2)$.
• Lemma 9 (corrected). $\sum_{\tau=1}^t\min(w_\tau^2,1)\le2n\ln(t+1)$.
• Theorem 6 (corrected). If $\mu\in B^2_t$ for all $t\le T$, then $\sum_{t\le T}r_t^2\le8n\beta_T\ln(T+1)$.
• Theorem 4 (Freedman). $\Pr(\sum X_i\ge a,\ V\le v)\le\exp(-a^2/(2v+2ab/3))$ for martingale differences bounded above by $b$.
• Lemma 12. $Z_t\le n+2\sum_{\tau<t}\eta_\tau\frac{x_\tau^\top(\hat\mu_\tau-\mu)}{1+w_\tau^2}+\sum_{\tau<t}\eta_\tau^2\frac{w_\tau^2}{1+w_\tau^2}$.
• Lemma 14. $\Pr(\forall t,\ \sum_{\tau<t}M_\tau\le\beta_t/2)\ge1-\delta$.
• Theorem 5 (Confidence). $\Pr(\forall t,\ \mu\in B^2_t)\ge1-\delta$.

Significance

The result gives a regret bound for linear bandits over an arbitrary compact decision set that depends on the dimension $n$ rather than on $|D|$, holds uniformly over horizons, and requires no gap between the best and second-best decision. With the paper's lower bound it shows that the price of bandit feedback, compared with full information, is a factor $\Theta^*(\sqrt n)$. The two components, a confidence theorem for a least-squares ellipsoid under martingale noise and a deterministic potential argument on $\log\det A_t$, are reused in the analysis of most optimistic linear and generalized-linear bandit algorithms.

The theorem has a published proof but, to our knowledge, no machine-checked one. The platform already has the elliptical potential lemma (BanditAlgorithm.elliptical_potential_lemma, Lattimore–Szepesvári Lemma 19.4), the matrix determinant lemma and the Woodbury identity, which cover the linear-algebra layer; the LinUCB regret theorem there (BanditAlgorithm.linear_bandit_linucb_regret_bound) is pathwise given confidence, for a different algorithm, so the probabilistic half is new. Formalization also settles the printed constants, three of which need correction (below).

Difficulty

The deterministic half is linear algebra. The difficulty is the confidence theorem. Hoeffding–Azuma applied to $\sum_\tau M_\tau$ would need a deterministic step bound, and the natural one gives only a $T^{3/4}$ regret. The step sizes of $M_t$ are bounded in terms of the random widths $w_t$, so the argument must control the conditional variances pathwise and apply Freedman's inequality, whose event $\{V\le v\}$ is random. The escape indicator $E_t$, which switches the martingale off after the first failure of confidence, is what makes the variance bound hold on every path, and the induction that turns Lemma 14 into Theorem 5 must be carried out on a single event for all $t$ simultaneously. Freedman's inequality itself is not in Mathlib.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, rounds are indexed $t=1,2,\dots$ in ℕ. The spanner is the standard basis, as in Section 5 of the paper (the algorithm is equivariant under the linear change of coordinates). The probability model is a probability space with a general filtration $(\mathcal F_t)$; $x_t$ is $\mathcal F_t$-measurable and $\ell_t$ is $\mathcal F_{t+1}$-measurable. The argmin is encoded as a joint minimiser over $D\times B^2_t$, which admits every tie-break and is required on every outcome; measurability of $x_t$ is a hypothesis, not derived from the selection. The optimum $x^*$ is a hypothesis ($x^*\in D$, minimising), not an sInf.

Corrections of the printed statements, each labelled in the item's Formalization Note:

1. $\ln(T+1)$ for $\ln T$ in Lemma 9, Theorem 6 and Theorem 2. The printed bounds are false at $T=1$ (with $n=1$, $D=[-1,1]$, $\mu>0$, the tie-break $x_1=1$ gives $R_1=2\mu>0$ against a bound of $0$); the proof of Lemma 9 gives $2\ln\det A_{t+1}\le2n\ln(t+1)$.
2. $n\le\beta_1=(\tfrac83\ln(1/\delta))^2$ is added to Theorems 5 and 2: the proof of Theorem 5 claims $Z_1\le n<\beta_1$, which fails for $\delta$ near $1$. Theorem 6 takes the proof's "$1<\beta_1$" as the hypothesis $\beta_1\ge1$.
3. $|\ell_t-\mu^\top x_t|\le1$ is added to Lemma 14, Theorems 5 and 2: Section 5.2 uses $|\eta_t|\le1$, while the model gives only $|\eta_t|\le2$. It holds when costs lie in $[0,1]$.
4. Theorem 5's "$\delta>0$" is stated with $0<\delta<1$; Lemma 10's index typo ($w_t$ for $w_\tau$) and Theorem 4's $\sum_{i=1}^n$ (for $T$) are corrected.

A regret bound for an arbitrary decision sequence under the assumption $\mu\in B^2_t$ for all $t$ is Theorem 6, not the goal; the goal carries the ConfidenceBall₂ selection rule, the conditional-mean and measurability hypotheses, and $\delta$ as the algorithm's own parameter. The hypotheses are jointly satisfiable, for example by a finite $D$ with a fixed tie-break and i.i.d. costs in $[0,1]$.

Needed infrastructure: Freedman's inequality for a filtration (reusable across all of bandit theory), the potential lemma (available), and measurability of the algorithm's statistics. Contributions of alternative proofs of Theorem 5, for example via self-normalized bounds, are welcome.

Selected references

• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, JMLR 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• D. A. Freedman, On Tail Probabilities for Martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
• B. Awerbuch, R. Kleinberg, Adaptive Routing with End-to-End Feedback, STOC 2004. https://doi.org/10.1145/1007352.1007367
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://arxiv.org/abs/1102.2670
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

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

A decision-maker has $n$ projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the $n$ state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number $\nu(B, x)$, computable for each bandit process $B$ from its own data and its own current state $x$, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.

The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.

Setting

A bandit process $B$ (§2.3–2.4) is a Markov reward process on a countable state space $E$: transition probabilities $P(y \mid x)$, a bounded reward $r(x)$ received each time the continuation control is applied in state $x$, and a discount factor $a \in (0, 1)$; the freeze control leaves the state unchanged and yields nothing. The law of the process started at $x$ is $\mathbb{P}_x$ and $x(t)$ is its state at process time $t = 0, 1, 2, \dots$. A stopping time $\tau$ is a past-measurable rule for switching from continuation to freezing, taking values in $\{1, 2, \dots\} \cup \{\infty\}$. For such $\tau$, $R_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t r(x(t))]$ is the expected discounted reward and $W_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t]$ the expected discounted time; their ratio $\nu_\tau(B, x)$ (2.7) is the equivalent constant reward rate of that portion of $B$. The Gittins index is

$$\nu(B, x) = \sup_{\tau > 0} \frac{R_\tau(B, x)}{W_\tau(B, x)} \tag{2.6}$$

and, equivalently, the fair charge (2.5): the greatest rent $\lambda$ per period for which continuing $B$ for one or more periods, paying $\lambda$ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is $n$ such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted $\mathbb{N}\cup\{\infty\}$-valued maps on trajectories, and gittinsIndex P r a x is (2.6).

Formalization targets

Goal: Lemma 2.2, the optimal stopping set

The supremum in (2.6) is attained. For the initial state $\xi$, the attaining stopping rule may be taken to be "stop at the first time $t \ge 1$ at which the state lies in $\Sigma_0$" for any set $\Sigma_0$ with

$$\{x : \nu(B, x) < \nu(B, \xi)\} \subseteq \Sigma_0 \subseteq \{x : \nu(B, x) \le \nu(B, \xi)\},$$

and every such rule has $\nu_\tau(B, \xi) = \nu(B, \xi)$.

Milestones

Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at $\tau = \infty$.

Significance

Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.

Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.

Difficulty

The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge $\lambda = \nu(B, \xi)$, whose value function satisfies $\varphi(x) = \max\{0, r(x) - \lambda + a\mathbb{E}[\varphi(x(1)) \mid x(0) = x]\}$, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities $\lambda > \nu(B, x)$ and $\lambda \ge \nu(B, x)$. That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is $\max(0, \nu/(1-a))$, not $\nu/(1-a)$, because restarting forever is free.

Formalization scope

The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; $a \in (0, 1)$. The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes $\tau \ge 1$ everywhere, so $W_\tau \ge 1$ and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time $1$ of a set, with $\infty$ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over $\{\lambda : \text{profit}(\lambda) \ge 0\}$, a nonempty set bounded above. The restart iteration is stated as a limit, with the value $\max(0, \nu(B, \xi)/(1-a))$: for a nonnegative index this is the book's $\nu/(1-a)$, and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under $\mathbb{P}_x$, written as events of measure one.

Two trivializing readings are excluded: the index is never taken over all $\mathbb{N}\cup\{\infty\}$-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
• M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range $\mathcal{Z}$, and let it degrade at a controlled rate outside, proportionally to the distance from $\mathcal{Z}$. That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.

Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most $\alpha \,\mathrm{dist}(\zeta, \mathcal{Z})$" has no direct meaning. What replaces it is the observation that a scalar inequality $a^Ty - b \le 0$ is the inclusion $a^Ty - b \in \mathbf{Q} \equiv \mathcal{R}_-$, and that the violation is the distance from the left hand side to $\mathbf{Q}$. In that form the notion lifts verbatim, and the whole chapter follows.

Setting

Definition 11.1.2. Consider an uncertain convex constraint

$$\Bigl[P^0 + \sum_{\ell=1}^L \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_{\ell=1}^L \zeta_\ell p^\ell\Bigr] \ \in\ \mathbf{Q}, \tag{11.1.4}$$

with $\mathbf{Q} \subseteq \mathcal{R}^k$ nonempty, closed and convex. Let the perturbation space split as $\mathcal{R}^L = \mathcal{R}^{L_1}\times\cdots\times\mathcal{R}^{L_S}$, each factor carrying a normal range $\mathcal{Z}^s$, a closed convex cone $\mathcal{L}^s$ and a norm $\|\cdot\|_s$, and let $\|\cdot\|_{\mathbf{Q}}$ be a norm on $\mathcal{R}^k$. A candidate $y$ is robust feasible with global sensitivities $\alpha_s$ if

$$\mathrm{dist}\bigl(P(y,\zeta), \mathbf{Q}\bigr) \ \le\ \sum_{s=1}^S \alpha_s\, \mathrm{dist}(\zeta^s, \mathcal{Z}^s|\mathcal{L}^s) \qquad \forall\, \zeta \in \mathcal{Z} + \mathcal{L}, \tag{11.1.6}$$

where $\mathrm{dist}(u,\mathbf{Q}) = \min_{v\in\mathbf{Q}}\|u - v\|_{\mathbf{Q}}$ and $\mathrm{dist}(\zeta^s,\mathcal{Z}^s|\mathcal{L}^s) = \min\{\|\zeta^s - v\|_s : v \in \mathcal{Z}^s,\ \zeta^s - v \in \mathcal{L}^s\}$.

The object that makes the analysis work is the recessive cone of $\mathbf{Q}$ (Definition 11.3.1): for any $\bar x \in \mathbf{Q}$,

$$\mathrm{Rec}(\mathbf{Q}) = \{h : \bar x + th \in \mathbf{Q}\ \ \forall t \ge 0\},$$

which does not depend on $\bar x$ and is a nonempty closed convex cone.

Formalization targets

Goal — Proposition 11.3.3, the decomposition of the conic GRC

A candidate $y$ is feasible for the GRC (11.1.6) if and only if it satisfies the system

$$\text{(a)}\quad \Bigl[P^0 + \sum_\ell \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_\ell \zeta_\ell p^\ell\Bigr] \in \mathbf{Q} \qquad \forall \zeta \in \mathcal{Z} = \mathcal{Z}^1\times \cdots\times\mathcal{Z}^S,$$ $$\text{(b}_s)\quad \mathrm{dist}\Bigl(\sum_{\ell} [P^\ell y - p^\ell](E_s\zeta^s)_\ell,\ \mathrm{Rec}(\mathbf{Q})\Bigr) \ \le\ \alpha_s \qquad \forall \zeta^s \in \mathcal{L}^s \text{ with } \|\zeta^s\|_s \le 1, \quad s = 1,\ldots,S .$$

Line (a) is the ordinary robust counterpart over the normal range. Each line (b$_s$) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to $\mathbf{Q}$ itself.

Supporting targets

$$\text{(Def 11.3.1)}\quad \mathrm{Rec}(\mathbf{Q}) \text{ is independent of the base point and is a nonempty closed convex cone},$$ $$\text{(Ex 11.3.2)}\quad \mathbf{Q} \text{ bounded} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \{0\}; \quad \mathbf{Q} \text{ a cone} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \mathbf{Q}; \quad \mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\},$$ $$\text{(Prop 11.4.1)}\quad \Psi_\Xi(\mathcal{M}) = \Psi_{\Xi_*}(\mathcal{M}^*), \qquad \Psi(\mathcal{M}) = \max\{\mathrm{dist}_{\|\cdot\|_F}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\} .$$

Significance

The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.

The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b$_s$) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function

$$\Psi(\mathcal{M}) = \max\bigl\{\mathrm{dist}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\bigr\}$$

of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that $\Psi$ of a map with respect to a setup equals $\Psi$ of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on $\Psi$ be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.

The recessive cone results are the vocabulary. The one that earns its place is $\mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\}$: the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.

Difficulty

The goal is an equivalence and the two directions are asymmetric.

Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix $\bar\zeta \in \mathcal{Z}$ and $\zeta^s$ in the unit ball of $\mathcal{L}^s$, and run $\zeta_i = \bar\zeta + i\,\zeta^s$ out along the cone. The GRC bounds the distance to $\mathbf{Q}$ by $\alpha_s i$, so there are $q_i \in \mathbf{Q}$ with $\|P(y,\bar\zeta) + i\Phi(y)E_s\zeta^s - q_i\|_{\mathbf{Q}} \le \alpha_s i$; the rescaled points $q_i/i$ stay bounded, and a limit point of them lies in $\mathrm{Rec}(\mathbf{Q})$ by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not $\mathbf{Q}$ — is what appears in lines (b$_s$).

Backward is a decomposition-and-assemble: split each $\zeta^s = \bar\zeta^s + \delta^s$ with $\bar\zeta^s \in \mathcal{Z}^s$, $\delta^s \in \mathcal{L}^s$ realizing the distance, get a point of $\mathbf{Q}$ from line (a) and a recession direction from each line (b$_s$), and add them — using that $\mathbf{Q} + \mathrm{Rec}(\mathbf{Q}) \subseteq \mathbf{Q}$.

Proposition 11.4.1 is a chain of polarity identities: the polar of $X + K$ is $X^o \cap (-K_*)$ for compact convex $X$ containing the origin, the polar of a norm ball of radius $\alpha$ is the dual-norm ball of radius $1/\alpha$, and bipolarity. Each step is standard and the composition is not.

Formalization scope

Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function $\Psi$.

Conventions committed to:

• Norms are functions carrying an explicit predicate, not typeclass instances. Chapter 11 quantifies over arbitrary norms $\|\cdot\|_{\mathbf{Q}}$ and $\|\cdot\|_s$ on fixed coordinate spaces, and a statement must be able to range over them; a typeclass instance would fix one norm per type. IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and nonnegativity follows from them.
• The dual norm is a predicate, not a construction. $\|f\|^* = \sup\{f^Te : \|e\| \le 1\}$ is asserted as a least upper bound of the set of values, so no supremum is taken on faith.
• Distances are infima, not minima. The source writes $\min$, which is correct because the sets are closed; writing $\inf$ avoids carrying an attainment proof into every statement, and agrees with the minimum whenever the source's own hypotheses hold.
• The recessive cone is indexed by a base point. Definition 11.3.1 defines it at an arbitrary $\bar x \in \mathbf{Q}$ and then asserts independence of the choice; that assertion is one of the published items, so the definition cannot presuppose it.
• The perturbation is carried as a family of blocks, $\zeta = (\zeta^1,\ldots,\zeta^S)$ with $\zeta^s \in \mathcal{R}^{L_s}$, rather than as a single vector in $\mathcal{R}^L$ together with the embeddings $E_s$. This is the same data and removes the index bookkeeping of $E_s$ from every statement.
• $\Psi$ is a predicate on a real number, as for the dual norm and for the same reason.
• §11.2 and §11.5 are out of scope: the definition of a tight safe approximation of a GRC and the worked analysis of nonexpansive dynamical systems. The first is a definition the chapter uses only to phrase §11.4's programme, the second an application.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. Chapter 11, §§11.1, 11.3-11.4, pp. 281-294; Chapter 3 for the linear case. https://doi.org/10.1515/9781400831050
• A. Ben-Tal, S. Boyd and A. Nemirovski, Extending scope of robust optimization: comprehensive robust counterparts of uncertain problems, Mathematical Programming 107 (2006), 63-89. https://doi.org/10.1007/s10107-005-0679-z
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.

The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link $j$ is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.

Setting

The links are $\mathcal{J} = \{1,\dots,J\}$, link $j$ carrying $C_j$ circuits. A route $r$ belongs to a set $\mathcal{R}$ of $R$ routes, and the link-route incidence matrix $A$ records how much of each link a route needs: a call on route $r$ requires $A_{jr}$ circuits from link $j$ and is lost if any link has fewer than $A_{jr}$ free. (The classical case is $A$ a $0$–$1$ matrix and $A_{jr}=1$ exactly when $j\in r$; from section 3.3 the book allows any non-negative integers.)

Calls requesting route $r$ arrive as a Poisson process of rate $\nu_r$, independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing $n_r$ for the number of calls in progress on route $r$, the process $n=(n_r)$ is Markov on

$$S(C)=\{n\in\mathbb{Z}_+^{R} : An\le C\},$$

and is called a loss network with fixed routing.

Write $E(\nu,C)$ for Erlang's formula, $E(\nu,C)=\dfrac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}$, published in mission I of this series. The Erlang fixed point equations are

$$E_j \;=\; E\!\left((1-E_j)^{-1}\sum_r A_{jr}\,\nu_r\prod_i (1-E_i)^{A_{ir}},\; C_j\right), \qquad j=1,\dots,J. \tag{3.7}$$

The factor $(1-E_j)^{-1}$ removes link $j$'s own thinning from the product, so in the $0$–$1$ case the argument is $\sum_{r\ni j}\nu_r\prod_{i\in r\setminus\{j\}}(1-E_i)$, the reduced load offered to link $j$.

Formalization targets

Goal — Theorem 3.20, existence and uniqueness of the Erlang fixed point

$$\exists!\,(E_1,\dots,E_J)\in[0,1]^J \text{ satisfying } (3.7).$$

The goal fixes no formula for $E$ and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube $[0,1]^J$; uniqueness is the substance.

Supporting levels

The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution $\pi(n)=G(C)\prod_r \nu_r^{n_r}/n_r!$ on $S(C)$; and the acceptance probability $1-L_r=G(C)/G(C-Ae_r)$. Then the optimization side: that $E(\nu,C)$ and the utilization $\nu(1-E(\nu,C))$ are strictly increasing in $\nu$, which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on $B$, equation (3.6).

Significance

The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by $\int_0^{y_j}U(z,C_j)\,dz$. That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector $B$ coming from the maximum-probability problem.

Formalizing it. Nothing here is open. What the mission produces is the loss network model in Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked statement of the object the reduced-load approximation computes. It is also where this series' earlier missions pay off: the uncapacitated network is literally the open migration process of mission II with $\lambda\equiv 0$, $\mu\equiv 1$, $\varphi_j(n)=n$, and the exact distribution (3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I published.

Difficulty

Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization $\nu\bigl(1-E(\nu,C)\bigr)$ is strictly increasing in $\nu$, which is itself a milestone here.

A second, formal difficulty: the equations involve $(1-E_j)^{-1}$, so a solution with $E_j=1$ would be meaningless. It is worth checking before starting that no such solution exists for $C_j\ge 1$, rather than assuming it.

Formalization scope

Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only $0$–$1$), capacities are natural numbers, and arrival rates are positive reals. The feasible set $S(C)$ is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.

Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route $r$ is $n_r$ and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; $G(C)$ is the reciprocal of the sum in the book's notation. Capacities are assumed at least $1$ in the goal: a link with no circuits blocks everything, $E(\nu,0)=1$ identically, and the factor $(1-E_j)^{-1}$ would then be undefined rather than merely large.

The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.

Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the $0$–$1$ equations (3.1) of section 3.2; the utilization function $U(y,C)$ and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 3 (pp. 49–82); Lemma 3.4, equation (3.3), Theorems 3.10 and 3.20, equations (3.1), (3.5)–(3.9). DOI 10.1017/cbo9781139565363
• F. P. Kelly, Loss networks, Annals of Applied Probability 1 (1991), 319–378. DOI 10.1214/aoap/1177005872
• F. P. Kelly, Blocking probabilities in large circuit-switched networks, Advances in Applied Probability 18 (1986), 473–505. DOI 10.2307/1427303
• R. B. Cooper and S. Katz, Analysis of alternate routing networks with account taken of the nonrandomness of overflow traffic, Bell Telephone Laboratories memorandum, 1964.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1 on truncation.