Optimization

Motivation

The k-median problem asks where to open $k$ facilities so that the total distance from a set of clients to their nearest open facility is as small as possible. It is a basic model of facility location in operations research (placing depots, warehouses or servers) and of clustering with representative centres, and it is NP-hard, so the question of interest is how close a polynomial-time method can come to the optimum.

Local search is among the most widely used heuristics for it: start from any $k$ facilities and repeatedly exchange one open facility for a closed one while the cost decreases. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first constant-factor guarantee for this heuristic on metric instances: every local optimum of the single-swap local search costs at most five times any solution with $k$ facilities. This mission formalizes that result.

Timeline of the relevant bounds:

• Korupolu, Plaxton and Rajaraman (SODA 1998) analysed a local search for k-median that opens $k(1+\epsilon)$ facilities and costs at most $3 + 5/\epsilon$ times the optimum with $k$ facilities.
• Charikar, Guha, Tardos and Shmoys (STOC 1999) gave the first constant-factor approximation for metric k-median, by LP rounding ($6\tfrac23$).
• Jain and Vazirani (J. ACM 2001) and Charikar and Guha (FOCS 1999) improved the constant with primal–dual methods to 6 and 4.
• Arya et al. (STOC 2001; SIAM J. Comput. 2004) proved the locality gap 5 for single swaps and $3 + 2/p$ for swaps of $p$ facilities at a time, with matching examples.

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. Write $c_{ji} = d(j,i)$ for the cost of serving client $j$ by facility $i$.

For a nonempty set $S \subseteq F$ of open facilities every client is served by its nearest open facility, and the cost of $S$ is

$$\mathrm{cost}(S) = \sum_{j \in C} \min_{i \in S} c_{ji}.$$

The k-median problem asks for a set $S$ of at most $k$ facilities of minimum cost.

A swap $\langle s, s'\rangle$ closes a facility $s \in S$ and opens a facility $s' \notin S$, giving $S - s + s' = (S \setminus \{s\}) \cup \{s'\}$. The neighbourhood of $S$ is

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

and $S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The local search starts from an arbitrary set of $k$ facilities and applies improving swaps until none exists; swaps preserve the number of facilities, so it stops at a locally optimum set of exactly $k$ facilities. The locality gap is the supremum, over instances, of the ratio between the cost of a worst local optimum and the optimal cost.

The analysis uses the following notation. For a solution $A$, let $\sigma_A$ assign each client to a nearest facility of $A$, let $A_j = c_{j\sigma_A(j)}$ be the service cost of client $j$, and let $N_A(a)$ be the set of clients served by $a \in A$. For two solutions $S$ and $O$ put $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 bad if it captures some $o \in O$ and good otherwise.

Formalization targets

Goal: Theorem 3.2

For every metric instance, every $k$, every locally optimum set $S$ of exactly $k$ facilities and every nonempty set $O$ of at most $k$ facilities,

$$\mathrm{cost}(S) \le 5 \cdot \mathrm{cost}(O).$$

The comparison solution $O$ is arbitrary, not an optimum; the statement is the locality gap bound in the form the proof gives.

Milestones, in the order the proof uses them

1. A facility $o$ is captured by at most one facility of $S$ (remark after Definition 3.1).
2. Property 3.1: for each $o$ there is a bijection $\pi$ of $N_O(o)$ with $\pi(N^o_s) \cap N^o_s = \emptyset$ whenever $s$ does not capture $o$.
3. When $|S| = |O|$ there are $|O|$ swaps $\langle s, o\rangle$, one for each $o \in O$, such that no facility capturing two or more facilities of $O$ is used, every good facility is used at most twice, and a used $s$ captures no $o' \ne o$.
4. Inequality (2): for a locally optimum $S$ and such a swap $\langle s, o\rangle$,

$$\sum_{j \in N_O(o)} (O_j - S_j) + \sum_{\substack{j \in N_S(s)\\ j \notin N_O(o)}} \bigl(O_j + O_{\pi(j)} + S_{\pi(j)} - S_j\bigr) \ge 0.$$

Significance

Theorem 3.2 shows that the simplest exchange heuristic for k-median is a constant-factor approximation on every metric instance, and the paper states that the analysis is tight: its example of §3.5, given for swaps of two facilities, is said to generalize to swaps of $p \ge 1$ facilities, where the bound $3 + 2/p$ is 5 for $p = 1$. Combined with the standard device of accepting only swaps that improve the cost by a factor $1 - \epsilon/Q$, it yields a polynomial-time $5/(1-\epsilon)$-approximation (p. 548). The same capture-and-reassignment argument is reused for multi-swap k-median, for uncapacitated and capacitated facility location in the same paper, and in later work on k-means and on local search for clustering; its milestones (the capture graph and the mapping $\pi$) are the reusable part.

The result has been proved since 2001 and is textbook material (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, Chapter 9). No machine-checked proof of it is known; Mathlib has no k-median problem and no locality-gap result for any clustering objective. The work remaining is to formalize the known proof.

Difficulty

The obvious argument adds up the inequalities $\mathrm{cost}(S - s + o) \ge \mathrm{cost}(S)$ over a pairing of $S$ with $O$, rerouting the clients of the closed facility $s$ to the nearest remaining facility. This fails when a single facility of $S$ serves most clients of several facilities of $O$: closing it leaves those clients with no nearby open facility, and no bound in terms of $\mathrm{cost}(O)$ follows. The analysis must choose which swaps to consider so that such facilities are never closed, and must reroute the displaced clients of the facilities it does close to a facility other than the closed one while paying only a constant multiple of their own service costs. Both choices must work for arbitrary ties in the nearest-facility assignments and when $S$ and $O$ share facilities.

Formalization scope

Namespace LocalSearchFL.KMedian. Clients and facilities are types Cl, Fa with Fintype and DecidableEq; the distance is a real-valued function on Cl ⊕ Fa with fields for nonnegativity, symmetry and the triangle inequality, and $d(x,x) = 0$ is not assumed. Solutions are Finset Fa. The cost is defined only for nonempty sets, from a nonemptiness proof, so no value is assigned to the empty solution; the goal takes $S$ nonempty with S.card = k, which is the paper's $k \ge 1$. Local optimality quantifies over every swap $\langle s, s'\rangle$ with $s \in S$ and $s' \notin S$, exactly the neighbourhood $\mathcal B(S)$ of Theorem 3.2, and not only over the swaps with $s' \in O$ that the proof uses. The inequality is stated multiplied out, $\mathrm{cost}(S) \le 5 \cdot \mathrm{cost}(O)$, so it is meaningful when $\mathrm{cost}(O) = 0$.

The milestones quantify over nearest-facility assignments $\sigma_S$, $\sigma_O$ with arbitrary ties. Capture is stated in integers as $|N_O(o)| < 2|N^o_s|$. The bijection $\pi$ of $N_O(o)$ is a permutation of all clients fixing every client outside $N_O(o)$; in inequality (2) it is a single permutation preserving every $N_O(o)$. Milestones 1–3 are purely combinatorial and are stated for arbitrary assignments, which contains the paper's case.

A formalization in which local optimality ranges over the swaps $\langle s, o\rangle$, $o \in O$, only, or in which $|O| = |S|$ or $O$ optimal is assumed, or in which the cost of the empty set is $0$, is a different statement and is ruled out.

A complete development needs the finite-sum and Finset.inf' API of Mathlib, permutations (Equiv.Perm) and finite counting. The capture machinery and the mapping $\pi$ are reusable for the multi-swap and facility location missions of this series. Proofs of individual milestones are welcome independently 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. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A Constant-Factor Approximation Algorithm for the k-Median Problem, J. Comput. System Sci. 65(1):129–149, 2002. https://doi.org/10.1006/jcss.2002.1882
• K. Jain, V. V. Vazirani, Approximation Algorithms for Metric Facility Location and k-Median Problems Using the Primal-Dual Schema and Lagrangian Relaxation, J. ACM 48(2):274–296, 2001. https://doi.org/10.1145/375827.375845
• 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
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

Motivation

The bilinear program

$$\min_{(x,y)} \; c^T x + x^T A y + d^T y \quad \text{subject to} \quad x \in X,\ y \in Y,$$

with $X \subseteq \mathbb{R}^p$ and $Y \subseteq \mathbb{R}^q$ polyhedra, is one of the recurring nonconvex problems of mathematical programming. It arises from constrained bimatrix games (Mangasarian 1964), dynamic Markovian assignment, multicommodity network flow and certain dynamic production problems (Konno 1971, 1976). Its classical structural fact is that, because the constraints on $x$ and on $y$ are separate and the objective is linear in each block, an optimal solution can be found at an extreme point of $X \times Y$ (Falk 1973, doi:10.1007/BF01580119). Vertex-enumeration, extreme-point ranking and cutting-plane methods for the problem rest on that fact.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) consider the jointly constrained version, in which the feasible region is an arbitrary set $S$ of pairs $(x, y)$, so that constraints may couple $x$ and $y$. They observe that the extreme-point property is then lost, and replace it with a weaker structural fact that survives: a minimum is attained on the boundary of the feasible region. This mission formalizes that result, Theorem 1 of the paper, together with the two examples on p. 274 that delimit it.

Setting

Write points of $\mathbb{R}^p \times \mathbb{R}^q$ as $(x, y)$, and let $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ be a nonempty compact set. No convexity of $S$ is assumed. Let $\varphi : \mathbb{R}^p \times \mathbb{R}^q \to \mathbb{R}$ be continuous on $S$.

The function $\varphi$ is biconcave over $S$ (Lean: BiconcaveOn S φ) when both partial functions are concave wherever they live inside $S$: for every fixed $y$, the map $x \mapsto \varphi(x, y)$ is concave on every convex set $C$ with $C \times \{y\} \subseteq S$; and for every fixed $x$, the map $y \mapsto \varphi(x, y)$ is concave on every convex set $D$ with $\{x\} \times D \subseteq S$. Equivalently, $\varphi$ is concave along every segment of $S$ that is parallel to the $x$-block or to the $y$-block. A bilinear objective $f(x) + x^T y + g(y)$ with $f$ and $g$ concave is biconcave; joint concavity of $\varphi$ is not required.

The boundary $\partial S$ is the topological frontier of $S$ in $\mathbb{R}^p \times \mathbb{R}^q$: the closure of $S$ minus its interior. A solution of $\min\{\varphi(x,y) : (x,y) \in S\}$ is a point $z \in S$ with $\varphi(z) \le \varphi(w)$ for all $w \in S$ (Lean: IsMinOn φ S z). The Euclidean distance on the product (Lean: eucDist) is $d\big((x,y),(x',y')\big) = \sqrt{\|x-x'\|^2 + \|y-y'\|^2}$.

Formalization targets

Goal: Theorem 1 (p. 274)

If $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ ($p + q \ge 1$) is nonempty and compact, and $\varphi$ is continuous on $S$ and biconcave over $S$, then

$$\exists\, z^* \in \partial S \quad \text{with} \quad \varphi(z^*) = \min\{\varphi(x, y) : (x, y) \in S\}.$$

The conclusion is existence of a boundary minimizer. It does not assert that every minimizer lies on $\partial S$ (a constant $\varphi$ is a counterexample to that).

Milestones

1. Proof of Theorem 1, p. 274. If $(\bar x, \bar y) \in \operatorname{int} S$ and $(x^*, y^*) \in \partial S$ is a nearest boundary point in Euclidean distance $d^*$, then the closed Euclidean ball of radius $d^*$ about $(\bar x, \bar y)$ lies in $S$, and with $(s,t) = 2(\bar x, \bar y) - (x^*, y^*)$ the points $(s,t)$, $(x^*, t)$ and $(s, y^*)$ are feasible.
2. Proof of Theorem 1, p. 275, first display. For $\varphi$ biconcave over $S$ and segments $[x^*, s] \times \{\tfrac12 y^* + \tfrac12 t\}$, $\{x^*\} \times [y^*, t]$, $\{s\} \times [y^*, t]$ inside $S$,

$$\varphi\big(\tfrac12(x^*,y^*) + \tfrac12(s,t)\big) \ge \tfrac12\varphi(x^*, \tfrac12y^*+\tfrac12t) + \tfrac12\varphi(s, \tfrac12y^*+\tfrac12t) \ge \tfrac14\big[\varphi(x^*,y^*)+\varphi(x^*,t)+\varphi(s,y^*)+\varphi(s,t)\big].$$

3. Example, p. 274. The program $\min\{-x + xy - y : -6x + 8y \le 3,\ 3x - y \le 3,\ 0 \le x, y \le 5\}$ has the solution $(7/6, 1/2)$, which is not an extreme point of the feasible region, and no extreme point is a solution.
4. Example, p. 274. $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$, the first of which is not global.

Significance

Theorem 1 is the structural statement that separates jointly constrained bilinear and biconcave programs from their separably constrained special case. It says where a global search may restrict attention, namely to $\partial S$, and example 3 shows that this cannot be sharpened to extreme points once the constraints couple the blocks. Example 4 records that such problems have proper local minima, so a local method alone does not solve them; this motivates the branch-and-bound algorithm of the same paper, which is the subject of the companion mission.

The result is proved in the paper; this mission produces its machine-checked statement and proof. Mathlib contains the Bauer-type principle for jointly concave functions on compact convex sets, but no statement of this kind for biconcave functions on nonconvex sets, and no formalization of Theorem 1 is known. The two examples are small but exact computations, and they certify that the definitions admit the intended instances.

Difficulty

The first idea is to apply the concave-minimization principle: a concave function on a compact convex set attains its minimum at an extreme point. It does not apply. $S$ need not be convex, so it has no useful extreme-point structure, and $\varphi$ is concave only along segments parallel to one block, so it is not concave along the segment from an interior point to a boundary point in a general direction. Example 3 shows that the conclusion "extreme point" is actually false here.

What remains is local geometry around an interior minimizer: one must find points of $S$ around it at which biconcavity can be applied in both blocks, and control their membership in $S$ without convexity. The feasibility of the mixed points $(x^*, t)$ and $(s, y^*)$, which the paper uses without comment, is where the choice of the Euclidean distance matters, and it is recorded as a separate milestone.

Formalization scope

• Points are pairs in EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin q). The boundary is Mathlib's frontier in this product; it does not depend on the norm. Only milestone 1 refers to a distance, and it uses eucDist, the Euclidean distance written out, because Mathlib's default metric on a product is the maximum of the block distances.
• The theorem is the "more general context" of p. 274, independent of the paper's Problem 𝒫: the standing assumptions (a)–(c) of p. 274 (convex $f$, $g$; closed convex $S$; a box $\Omega$) do not enter.
• Hypotheses of the goal: IsCompact S, S.Nonempty, ContinuousOn φ S (continuity only on $S$), and BiconcaveOn S φ. One hypothesis is added: $0 < p + q$. For $p = q = 0$ the space is a point, whose only nonempty subset has empty frontier, so the conclusion fails; the paper works in positive dimension throughout.
• Biconcavity is read over $S$: concavity on every convex subset of each section of $S$. Assuming instead concavity of each partial function on the whole space would be a stronger hypothesis and a weaker theorem.
• Trivializing formalizations ruled out: the statement assumes neither joint concavity of $\varphi$ nor convexity of $S$ (either would reduce it to the Bauer principle), and it covers sets with nonempty interior; the case of empty interior, where $\partial S = S$, is included but is not the only case.
• Corrected misprint (milestone 3): the paper prints the solution of example 3 as $(7/16, 1/2)$. That point has objective value $-23/32$, while the feasible vertex $(1,0)$ has value $-1$. On the edge $3x - y = 3$ the objective equals $3x^2 - 7x + 3$, minimized at $x = 7/6$, value $-13/12$, the global minimum. The Lean states the corrected point $(7/6, 1/2)$; the milestone text is kept verbatim.
• In milestone 4, "local solution" is IsLocalMinOn relative to the box, and non-globality of $(-1, 3)$ records the paper's word "proper".
• Infrastructure needed: nearest boundary points of compact sets (Mathlib has IsCompact.exists_mem_frontier_infDist_compl_eq_dist, stated for the ambient metric), the fact that a closed ball about an interior point whose radius is the distance to the frontier lies in the set, and concavity on segments. A lemma that works for an arbitrary norm on the product would be reusable. Contributions of alternative proofs are welcome.

Selected references

• Faiz A. Al-Khayyal and James E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
• James E. Falk, A Linear Max-Min Problem, Mathematical Programming 5:169–188, 1973. https://doi.org/10.1007/BF01580119
• Hiroshi Konno, A Cutting Plane Algorithm for Solving Bilinear Programs, Mathematical Programming 11:14–27, 1976. https://doi.org/10.1007/BF01580367
• Olvi L. Mangasarian, Equilibrium Points of Bimatrix Games, Journal of the Society for Industrial and Applied Mathematics 12(4):778–780, 1964. https://doi.org/10.1137/0112064
• Heinz Bauer, Minimalstellen von Funktionen und Extremalpunkte, Archiv der Mathematik 9:389–393, 1958. https://doi.org/10.1007/BF01900582

Motivation

Dimensionality reduction maps data in $\mathbb{R}^d$ to $\mathbb{R}^n$, $n \ll d$, by a linear map $x \mapsto Wx$, for computational reasons, for generalization (Chapter 19's curse of dimensionality) and for interpretability. Chapter 23 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies three ways to choose $W$. Principal Component Analysis chooses the pair of compression and recovery matrices that minimizes the total squared reconstruction error, and the answer is the eigenvectors of $\sum_i x_ix_i^\top$ for the largest eigenvalues (Theorem 23.2). Random projections choose $W$ with independent Gaussian entries, and the Johnson–Lindenstrauss lemma says that the norms of any finite set of vectors are then preserved up to $1 \pm \epsilon$ with $n = O(\epsilon^{-2}\log|Q|)$ (Lemma 23.4). Compressed sensing exploits sparsity: a matrix with the restricted isometry property compresses every $s$-sparse vector losslessly (Theorem 23.6), the reconstruction can be done by $\ell_1$ minimization, a linear program, with an error bound that degrades gracefully for approximately sparse inputs (Theorem 23.8, due to Candès), and Gaussian random matrices with $n = O(s\log d)$ rows are RIP with high probability (Theorem 23.9).

Setting

Vectors are functions $\mathbb{R}^d$ with $\|v\|_2^2 = \sum_i v_i^2$, $\|v\|_1 = \sum_i|v_i|$ and $\|v\|_0 = |\{i : v_i \ne 0\}|$. The PCA problem (23.1) is $\operatorname{argmin}_{W \in \mathbb{R}^{n \times d}, U \in \mathbb{R}^{d \times n}}\sum_{i=1}^m\|x_i - UWx_i\|_2^2$, and $A = \sum_i x_ix_i^\top$. A random matrix has independent $N(0, v)$ entries, $v = 1$ in Lemma 23.3 and $v = 1/n$ afterwards. $W$ is $(\epsilon, s)$-RIP if $\big|\|Wx\|_2^2/\|x\|_2^2 - 1\big| \le \epsilon$ for every $x \ne 0$ with $\|x\|_0 \le s$ (Definition 23.5); $v_I$ is $v$ restricted to an index set $I$.

Formalization targets

Goal: Theorem 23.2

Let $x_1, \dots, x_m \in \mathbb{R}^d$, $A = \sum_i x_ix_i^\top$, and let $u_1, \dots, u_n$ be eigenvectors of $A$ for its $n$ largest eigenvalues, formalized as the first $n$ columns of a spectral decomposition $A = V\operatorname{diag}(D)V^\top$ with $V^\top V = I$ and $D$ nonincreasing. Then $U = [u_1 \cdots u_n]$ with $W = U^\top$ minimizes (23.1): for every $U', W'$,

$$\sum_i\|x_i - UU^\top x_i\|^2 \le \sum_i\|x_i - U'W'x_i\|^2.$$

Milestones

Lemma 23.1 (the reduction of (23.1) to orthonormal $U$ and $W = U^\top$); Lemma 23.4 (Johnson–Lindenstrauss); Theorem 23.6 (exact $\ell_0$ recovery under RIP); Theorem 23.8 (Candès' $\ell_1$ recovery bound); Theorem 23.9 (Gaussian matrices are RIP). Further items: Equation (23.3), Exercise 2, Remark 23.1 (the optimal value $\sum_{i>n}D_{i,i}$), the eigenvector transfer of §23.1.1, Lemma 23.3, Theorem 23.7, Lemma 23.10, Lemma 23.11 and Lemma 23.12.

Significance

Theorem 23.2 is the Eckart–Young–Mirsky theorem in the form the book states it: PCA is the optimal linear compression-and-recovery scheme in the least-squares sense, and its solution is spectral. The Johnson–Lindenstrauss lemma is the basic tool of randomized dimensionality reduction, with a bound independent of $d$, and the book's variant with explicit constants is what later chapters and the compressed-sensing proofs use. Theorems 23.6–23.9 together are the three "surprising results" of compressed sensing: information-theoretic recoverability from RIP, efficient recovery by convex relaxation, and the existence of RIP matrices by randomness; their proofs, Candès' cone argument and Baraniuk–Davenport–DeVore–Wakin's net-plus-union-bound, are among the cleanest in applied mathematics and are natural formalization targets. On the platform, the mission introduces Gaussian random matrices as product measures and the RIP predicate, usable by later work on sparse recovery.

Difficulty

Lemma 23.1 requires building an orthonormal basis of the range of $UW$, padded to $n$ vectors when the range has smaller dimension, and the identity $\|x - Vy\|^2 = \|x\|^2 + \|y\|^2 - 2y^\top V^\top x$; Equation (23.3) is a trace computation. Theorem 23.2 combines (23.3), the change of basis $B = V^\top U$ with $B^\top B = I$, the bound $\sum_i B_{j,i}^2 \le 1$ from extending $B$ to an orthogonal matrix, and Exercise 2, a rearrangement inequality; Remark 23.1 adds $\operatorname{trace}(A) = \sum_j D_{j,j}$. Lemma 23.3 is the concentration of a $\chi^2_n$ variable (Lemma B.12), which must itself be established from the Gaussian moment generating function; the Johnson–Lindenstrauss lemma is then a union bound. Theorem 23.6 is a two-line contradiction with RIP applied to $x - \tilde x$. Theorem 23.8 is the substantial one: the partition of $[d]$ into blocks of $s$ largest remaining entries, the bound $\|h_{T_j}\|_2 \le s^{-1/2}\|h_{T_{j-1}}\|_1$, the $\ell_1$-minimality inequality (23.8), Lemma 23.10, and the two claims combined through (23.5); a formal proof must handle the last, possibly shorter block, which the book's "assume $d/s$ is an integer" sidesteps. Lemma 23.11 is a volumetric net bound; Lemma 23.12 applies the Johnson–Lindenstrauss lemma to the image of an $\epsilon/4$-net of the unit sphere of $\mathbb{R}^s$ and closes the gap by the "smallest $a$" argument, and Theorem 23.9 is a union bound over index sets.

Formalization scope

Vectors are plain functions Fin d → ℝ with explicit norms, and matrices are Mathlib matrices, so the objectives are finite sums with no coercions between normed spaces. Random matrices are functions Fin n → Fin d → ℝ with the product of Gaussian laws gaussianReal 0 v, applied through Matrix.of; probability statements bound the outer measure of the failure event, and the failure events of Lemmas 23.4 and 23.12 are written with $\ge \epsilon$ so that the book's strict conclusions follow. "Eigenvectors corresponding to the $n$ largest eigenvalues" is formalized as the first $n$ columns of a spectral decomposition with nonincreasing diagonal, which is exactly the set of such systems and avoids Mathlib's eigenvalue ordering conventions. Minimizers ($\tilde x$, $x^\star$, $x_s$) are arbitrary elements of the argmin.

Five statements are given as their proofs support them, and the item texts say so. Lemma 23.3 and the Johnson–Lindenstrauss lemma are stated for $\epsilon \le 3/4$: the printed range $\epsilon \in (0, 3)$ (and $\epsilon \le 3$) is false, since the $\chi^2_n$ upper tail decays like $e^{-n(\epsilon - \ln(1+\epsilon))/2}$, slower than $e^{-\epsilon^2 n/6}$ for $\epsilon > 0.785$ (at $\epsilon = 2.9$ it fails for $n = 10$); the audit found this. Lemma 23.1 as printed, "every solution has orthonormal columns and $W = U^\top$", is false, since $(cU, W/c)$ has the same objective as $(U, W)$; the item states what the proof shows, that every $(U, W)$ is dominated by some $(V, V^\top)$ with $V^\top V = I$, which is all that (23.2) needs. Theorem 23.9 is stated with $n \ge 216\,s\log(72d/(\delta\epsilon))/\epsilon^2$: Lemma 23.12 with $\epsilon/3$ (so that $(1 \pm \epsilon/3)^2$ lies within $1 \pm \epsilon$) and $\delta/d^s$, followed by a union bound over the at most $d^s$ index sets, gives these constants, and the printed $100$ and $40$ are not reached by the argument. Theorem 23.8's proof assumes $d/s$ is an integer for simplicity; the statement is given without that assumption, since only the last block of the partition can be short and the block inequality still holds. Lemma 23.3 has $x \ne 0$, and the Johnson–Lindenstrauss lemma $n \ge 1$, since for $n = 0$ its $\epsilon$ is $0$ and the conclusion fails.

Not stated: §23.1.2 (implementation), Remarks 23.2–23.3, §23.4 (the comparison of PCA and compressed sensing), Exercises 1 and 3–6.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 23. doi:10.1017/CBO9781107298019
• W. B. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemporary Mathematics 26, 1984. doi:10.1090/conm/026/737400
• E. J. Candès, The restricted isometry property and its implications for compressed sensing, Comptes Rendus Mathématique 346(9–10), 2008. doi:10.1016/j.crma.2008.03.014
• R. Baraniuk, M. Davenport, R. DeVore, M. Wakin, A simple proof of the restricted isometry property for random matrices, Constructive Approximation 28, 2008. doi:10.1007/s00365-007-9003-x
• D. L. Donoho, Compressed sensing, IEEE Transactions on Information Theory 52(4), 2006. doi:10.1109/TIT.2006.871582
• E. J. Candès, T. Tao, Decoding by linear programming, IEEE Transactions on Information Theory 51(12), 2005. doi:10.1109/TIT.2005.858979

Motivation

Clustering is the most widely used tool of exploratory data analysis and, at the same time, the least well defined: similar points should share a cluster and dissimilar points should not, but similarity is not transitive while cluster membership is, and without labels there is no ground truth against which to evaluate a proposed grouping. Chapter 22 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), surveys the main paradigms, linkage-based algorithms, cost minimization with the k-means family, spectral relaxations of graph cuts, and the information bottleneck, and then returns to the question of what clustering is through Kleinberg's axioms. Its one theorem about that question is negative: no clustering function is simultaneously scale invariant, rich and consistent (Theorem 22.4). The mission formalizes this impossibility together with the chapter's positive facts: an iteration of the k-means algorithm never increases the k-means objective (Lemma 22.1), the RatioCut objective is the trace of a quadratic form of the graph Laplacian over cluster indicator vectors (Lemma 22.3), and the farthest-first traversal is a 2-approximation for the k-diam objective (Exercise 3).

Setting

A clustering of a finite set $X$ is a partition $C = (C_1, \dots, C_k)$. For $X \subseteq \mathbb{R}^n$ the k-means objective is $G(C) = \sum_i\sum_{x \in C_i}\|x - \mu(C_i)\|^2$ with $\mu(C_i)$ the centroid of $C_i$, equivalently $\min_{\mu_1, \dots, \mu_k}\sum_i\sum_{x \in C_i}\|x - \mu_i\|^2$ (22.1); the k-means algorithm alternately reassigns each point to a nearest centroid and recomputes the centroids. For a similarity matrix $W \in \mathbb{R}^{m \times m}$, the degree matrix is $D = \operatorname{diag}(\sum_j W_{i,j})$, the unnormalized graph Laplacian is $L = D - W$ (Definition 22.2), and $\operatorname{RatioCut}(C) = \sum_i \frac1{|C_i|}\sum_{r \in C_i, s \notin C_i}W_{r,s}$. Kleinberg's setting is a clustering function $F$ that takes a dissimilarity $d$ over $X$, symmetric, zero on the diagonal and positive off it, and returns a partition; the three axioms are Scale Invariance ($F(\alpha d) = F(d)$), Richness (every partition is some $F(d)$) and Consistency (shrinking within-cluster and expanding between-cluster dissimilarities leaves $F$ unchanged). The k-diam objective is $\max_j\operatorname{diam}(C_j)$, and the farthest-first traversal picks $\mu_1$ arbitrarily and $\mu_j$ maximizing $\min_{i<j}d(x, \mu_i)$, then clusters by nearest center.

Formalization targets

Goal: Theorem 22.4

For a finite domain $X$ with at least two points, there is no function $F$ from dissimilarities over $X$ to partitions of $X$ satisfying Scale Invariance, Richness and Consistency.

Milestones

Lemma 22.1 (a k-means iteration does not increase $G$); the Laplacian identity $v^\top L v = \frac12\sum_{r,s}W_{r,s}(v_r - v_s)^2$ from the proof of Lemma 22.3; Lemma 22.3 ($H^\top H = I$ and $\operatorname{RatioCut}(C) = \operatorname{trace}(H^\top L H)$ for $H_{i,j} = |C_j|^{-1/2}\mathbb{1}[i \in C_j]$); Exercise 3 (farthest-first traversal is a 2-approximation for k-diam). Further item: the centroid minimizes $\sum_{x \in C}\|x - \mu\|^2$, the content of (22.1)–(22.3).

Significance

Kleinberg's theorem is the chapter's conceptual center: it says there is no ideal clustering function, only trade-offs, and the choice of a method must encode prior knowledge about the task, the unsupervised analogue of the No-Free-Lunch theorem. Its proof is short but delicate about what a dissimilarity is, and formalizing it fixes the exact hypotheses. Lemma 22.1 is the only guarantee the book offers for Lloyd's algorithm, and it is the reason the algorithm terminates on finite data. Lemma 22.3 is the bridge from a combinatorial cut objective to the spectrum of the Laplacian, the starting point of spectral clustering and of the PCA-type argument used in Chapter 23. The farthest-first result of Exercise 3 is Gonzalez's classical 2-approximation for k-center-type objectives, stated here for the diameter objective, and it is tight in the sense that no better constant is possible unless P = NP.

Difficulty

Theorem 22.4 follows the book: Richness gives $d_1$ with all-singleton output and $d_2$ with a different output; positivity lets one scale $d_2$ above $d_1$ pointwise, and Scale Invariance and Consistency then force two different values for $F(\alpha d_2)$. Formally the work is in building the scaled dissimilarity and in comparing Setoids. Lemma 22.1 is two inequalities: the nearest-centroid reassignment does not increase $\sum_i\sum_{x \in C_i}\|x - \mu_i\|^2$ for the old centroids, because it minimizes it pointwise over assignments, and recomputing centroids does not increase it either, because the centroid minimizes the within-cluster sum of squares; the latter is the separate centroid item, a completing-the-square computation in an inner product space. The Laplacian identity is a finite double-sum manipulation that uses the symmetry of $W$; Lemma 22.3 applies it to the columns of $H$ and computes $H^\top H$ from the partition structure. Exercise 3 is the hint's argument: let $r$ be the distance from the next farthest-first point $\mu_{k+1}$ to the chosen centers; every point is within $r$ of its center, so every cluster of the algorithm has diameter at most $2r$, while the $k+1$ points $\mu_1, \dots, \mu_{k+1}$ are pairwise at distance at least $r$, so two of them share a cluster of any $k$-clustering, whose diameter is then at least $r$. When $|X| \le k$ the argument degenerates but the statement stays trivially true.

Formalization scope

Partitions are $\mathrm{Fin}\ k$-indexed families of finsets covering each point of the data exactly once, and nearest-center assignments and farthest-first centers are predicates rather than functions, so every tie-breaking rule is covered. The k-means items live in $\mathbb{R}^n$ as EuclideanSpace; the centroid of an empty cluster is $0$, which never enters any sum. The spectral items use Mathlib matrices over Fin m, Matrix.diagonal, Matrix.trace, the root-namespace dotProduct, and require $W$ symmetric, which the identity needs and which every similarity matrix satisfies; Lemma 22.3 requires nonempty clusters, without which $H$ has a zero column. Kleinberg's function is formalized on a fixed finite domain, as a map from Dissimilarity X to Setoid X, dissimilarities being positive on distinct points as in Kleinberg (2003): the book's model of p. 309 only asks for $d \ge 0$, but the scaling step of the proof of Theorem 22.4 requires positivity, and the theorem is stated for domains with at least two points, since the proof uses two partitions only. The k-diam theorem is stated without a maximum: every cluster of the algorithm has diameter at most twice the diameter of some cluster of the competitor, which is $G_{k\text{-diam}}(\hat C) \le 2G_{k\text{-diam}}(C^*)$ without conventions for empty index sets, and Metric.diam gives $0$ on sets of fewer than two points, the exercise's convention.

Not stated: the linkage-based algorithms and dendrograms of §22.1 (no theorem is stated about them), the k-medoids and k-median objectives, the spectral clustering algorithm itself, the information bottleneck of §22.4, Exercises 1, 2 and 4–6.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 22. doi:10.1017/CBO9781107298019
• J. Kleinberg, An impossibility theorem for clustering, NIPS 2002.
• S. P. Lloyd, Least squares quantization in PCM, IEEE Transactions on Information Theory 28(2), 1982. doi:10.1109/TIT.1982.1056489
• U. von Luxburg, A tutorial on spectral clustering, Statistics and Computing 17, 2007. doi:10.1007/s11222-007-9033-z
• T. F. Gonzalez, Clustering to minimize the maximum intercluster distance, Theoretical Computer Science 38, 1985. doi:10.1016/0304-3975(85)90224-5
• M. Ackerman, S. Ben-David, Measures of clustering quality: a working set of axioms for clustering, NIPS 2008.

Motivation

The bandit processes that motivated the index theorem are sampling processes: an arm is a population from which one draws i.i.d. observations whose distribution has an unknown parameter, and each draw both earns something and teaches something. Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), develops the theory of such processes in the Bayesian setting: the state of the process is the current posterior for the parameter, continuing it samples the next value from the predictive distribution and moves to the new posterior. When the observations are themselves the rewards one has a reward process, the classical Bayesian multi-armed bandit; when the aim is to find as quickly as possible an individual whose measurement reaches a target $T$ (a compound active enough to warrant further testing, in the drug-screening problem from which the index theorem came) one has a target process, which is a job that completes when the target is reached. Two questions organize the chapter. When can the index be written down without any optimization, and when do symmetries of the model reduce the index to a function of fewer variables? The first is answered by the notion of a favourable prior (Section 7.3): if no run of observations below the target can raise the current probability of success, then the index is that probability, exactly, by Proposition 2.7. The second is answered by the invariance theorems of Section 7.4: a location parameter with a conjugate prior gives $\nu(\bar x, n) = \bar x + \nu(0, n)$, a scale parameter gives $\nu(\bar x, n) = \bar x\,\nu(1, n)$, and for target processes the target can be absorbed into the state, $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$. These identities are what make the tables of Chapter 8 one-dimensional.

Setting

A sampling model consists of a likelihood $f(\cdot \mid \theta)$, a family of priors $\pi(\cdot \mid p)$ on the parameter indexed by the parameters $p$ of a conjugate family, and the Bayes update $p \mapsto p_x$ of those parameters after observing $x$; the family is conjugate if the posterior of $\pi(\cdot \mid p)$ given $X = x$ is $\pi(\cdot \mid p_x)$. The predictive distribution is $f(\cdot \mid p) = \int f(\cdot \mid \theta)\pi(d\theta \mid p)$. The reward process moves from $p$ to $p_x$ with $x \sim f(\cdot \mid p)$ and earns $r(p) = \int x f(x \mid p)dx$. The target process with target $T$ moves to the completion state $C$ if $x \ge T$ and to $p_x$ otherwise, earning the current probability of success $r(p) = f([T, \infty) \mid p)$, and $0$ in $C$. A state $p$ is favourable if $r(p_{x_1 \cdots x_m}) \le r(p)$ for every finite sequence of observations $x_i < T$. For the invariance theorems the parameters are $(\bar x, n)$ with the update $((n\bar x + x)/(n+1), n+1)$; $\mu$ is a location parameter of the likelihood if $f(\cdot \mid \mu + c)$ is $f(\cdot \mid \mu)$ shifted by $c$, and $\bar x$ is a location parameter of the prior family if $\pi(\cdot \mid \bar x + c, n)$ is $\pi(\cdot \mid \bar x, n)$ shifted by $c$; scale parameters are defined with $x \mapsto bx$, $b > 0$. The Gittins index is that of the Bandit Algorithms model on these chains.

Formalization targets

Goal: Theorem 7.9 (in the form of Corollary 7.10)

If $\mu$ is a location parameter of a reward process with a conjugate prior family in which $\bar x$ is a location parameter and the parameters update as the sample mean and count, then for every $n > 0$

$$r(\bar x + c, n) = r(\bar x, n) + c \quad\text{and}\quad \nu(\bar x, n) = \bar x + \nu(0, n),$$

under the standing assumptions that the observations have a mean and the discounted rewards of the chain are integrable.

Milestones

Proposition 7.4 (favourable state: $\nu = r$); Example 7.5 (Bernoulli target process, $\nu(\alpha, \beta) = \alpha/(\alpha + \beta)$); Example 7.6 (normal target process with known variance, $\nu(\bar x, n) = \Phi(\bar x (1 + n^{-1})^{-1/2})$ for $\bar x \ge 0$); Theorem 7.11 (scale parameter: $\nu(\bar x, n) = \bar x\,\nu(1, n)$); Theorem 7.17 (target process with a location parameter: $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$).

Significance

Theorem 7.9 and its companions are the reason the Gittins index of the normal reward process is tabulated as a function of $n$ alone and that of the exponential process as a function of $n$ and one ratio; every computational method of Chapter 8 starts by reducing the state space with them. Proposition 7.4 is the source of every closed-form index in the book: it identifies the states in which sampling for information is worthless, so that the index collapses to the immediate expected reward, and Examples 7.5 and 7.6 show that for the Bernoulli target process this is every state and for the normal target process every state with a nonnegative posterior mean. The formalization gives the platform its first Bayesian sampling-process model, in which the state is a posterior and conjugacy is stated through the posterior kernel of the likelihood, and its first index identities on unbounded-reward chains, which is where the integrability assumptions of the Bandit Algorithms model do real work.

None of this is machine-checked. The invariance theorems are stated in the proper-prior form of the corollaries, with the model's symmetry as hypotheses, so that they apply to any conjugate family with the stated structure rather than to a particular density.

Difficulty

The invariance theorems require showing that the chain of parameters from the shifted (scaled) state is the image of the chain from the original state under the shift (scaling) of trajectories, which is an equivariance of the Ionescu–Tulcea construction with respect to a measurable bijection commuting with the kernel; that stopping times are carried to stopping times; that the discounted reward of a stopping time shifts by $c$ times the discounted time; and that the supremum of a nonempty bounded set of reals shifts and scales accordingly. Boundedness of the set of ratios is where the integrability assumption enters. Proposition 7.4 is the chain-level statement that all rewards along every trajectory from a favourable state are at most $r(p)$, which needs an induction on the trajectory law of the target chain, followed by the argument of Proposition 2.7. Example 7.6 needs the monotonicity of $\bar x_m (1 + 1/(n+m))^{-1/2}$ in the observations below the target, a small inequality, plus the Gaussian probability of a half-line as the current probability of success; Example 7.5 needs only that $\alpha/(\alpha + \beta + m)$ decreases.

Formalization scope

The sampling model is a structure with Markov likelihood and prior kernels and a jointly measurable update; the predictive distribution is the kernel composition; conjugacy is an almost-everywhere identity between Mathlib's posterior of the likelihood with respect to the prior and the prior at the updated parameters, and is carried as a hypothesis of the invariance theorems and of Proposition 7.4 so that their subject is the Bayesian process. For the parameters $(\bar x, n)$ it is required on $n > 0$ only (IsConjugateOn): a proper prior has $n > 0$, and conjugacy at every $(\bar x, n) \in \mathbb{R}^2$ is impossible with a location parameter, since at $n = -1$ the update divides by zero and sends every observation to one state, which made the first draft's location theorems vacuous. The chains are built with Kernel.map of product kernels, so their measurability is structural, and the target process lives on P ⊕ Unit with the completion state absorbing. The book's improper priors are replaced by proper conjugate families with the location or scale structure of Corollaries 7.10 and 7.12, as those corollaries do; the discrete-time correction factor of Section 2.8 is not applied since it cancels in every identity stated. The two examples are built directly from a uniform or Gaussian seed with the transition probabilities the book computes (the beta and normal posterior computations of Exercise 7.1 are not formalized). Hypotheses: $a \in (0, 1)$; integrable observations and L&S Assumption 35.6 for the reward processes; $n > 0$ for the invariance theorems and $\bar x > 0$ for the scale theorem; $\alpha, \beta > 0$; $\bar x \ge 0$ and $n > 0$ for the normal example.

Trivializing readings are excluded: the indices are the genuine suprema of the Bandit Algorithms definition with integrable rewards, the update rule is the book's and not a free parameter, and the favourability condition ranges over all finite observation sequences. Welcome contributions: the equivariance of the trajectory measure under a state bijection commuting with the kernel, the transport of stopping times, and the reward bound along the target chain from a favourable state.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 7. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani, ed.), North-Holland, 1974.
• D. M. Jones, Search Procedures for Industrial Chemical Research, PhD thesis, University of Wales, 1975.
• H. Raiffa, R. Schlaifer, Applied Statistical Decision Theory, Harvard University Press, 1961.
• T. S. Ferguson, Mathematical Statistics: A Decision Theoretic Approach, Academic Press, 1967.
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 34–35. doi:10.1017/9781108571401

Motivation

Every proof of the index theorem in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), uses the fact that a bandit not being processed is frozen. Chapter 6 drops that: Whittle's restless bandits evolve under the passive action too, by a different law, and $m$ of $n$ must be active at every time. The problem is PSPACE-hard in general, so Whittle proposed a heuristic built from a Lagrangian relaxation: replace the hard constraint by a subsidy $W$ paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy $W(x)$ at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with $W$, the bandit is indexable and $W(x)$ is its Whittle index; the Whittle index policy activates the $m$ bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as $n$ grows under a fluid-stability condition (Weber and Weiss), and it has become the standard heuristic for sensor management, opportunistic channel access, maintenance and queueing control. The price is that indexability must be established model by model. Section 6.5 shows how easy this is when the single-bandit problem is solved by a monotone policy, on two bi-directional models: the spinning plates asset, which improves under investment and deteriorates when neglected, and the vigour bandit of Whittle's Ehrenfest project, which tires when worked and recovers when rested.

Setting

A restless bandit is a Markov decision process with two actions, active ($u = 1$) and passive ($u = 0$), each with its own transition kernel and reward. Under a deterministic stationary Markov policy $g$ with passive subsidy $W$ the reward in state $x$ is $r(x, g(x)) + W(1 - g(x))$, and the average reward from $x$ is the Cesàro limit of the expected rewards. The optimal average reward $g(W)$ is the supremum over such policies and initial states; a policy is optimal if it attains $g(W)$ from every initial state; $E_0(W)$ is the set of states in which some optimal policy is passive; the bandit is indexable if $E_0(W)$ is nondecreasing in $W$; and $W(x) = \inf\{W : x \in E_0(W)\}$.

The spinning plates asset lives on $\{1, \dots, k\}$: active moves $x \to x + 1$ at rate $\lambda(x)$, passive moves $x \to x - 1$ at rate $\mu(x)$, $\lambda(k) = \mu(1) = 0$, and $r(x)$ is earned under both actions, $r$ increasing. Uniformized so that rates are at most one, it is a discrete-time bandit whose kernels move with the rate's probability and otherwise stay. The monotone policy $(y)$ is passive exactly on $\{x \ge y\}$; under it the asset alternates between $y - 1$ and $y$, spending the fraction $\phi(y) = \lambda(y-1)/(\lambda(y-1) + \mu(y))$ of its time at $y$, so its average reward is $W\phi(y) + R(y)$ with $R(y) = r(y)\phi(y) + r(y-1)(1 - \phi(y))$, and $W^*(x) = (R(x+1) - R(x))/(\phi(x) - \phi(x+1))$. The vigour bandit is the mirror image: active moves down at rate $\nu(x)$ and earns $r(x)$, passive moves up at rate $\rho(x)$ and earns nothing, $\psi(y) = \nu(y)/(\nu(y) + \rho(y-1))$, and $W^{**}(x) = (r(x)(1 - \psi(x)) - r(x+1)(1 - \psi(x+1)))/(\psi(x+1) - \psi(x))$.

Formalization targets

Goal: Theorem 6.4

For the spinning plates asset: (i) if $\phi$ is strictly decreasing over the thresholds $1 \le y \le k + 1$, the asset is indexable; (ii) if additionally $W^*$ is strictly decreasing over the states, the Whittle index is

$$W(x) = W^*(x) = \frac{R(x+1) - R(x)}{\phi(x) - \phi(x+1)}, \qquad 1 \le x \le k.$$

Milestones

Eqs. (6.9)–(6.10): the monotone policy $(y)$ earns $W\phi(y) + R(y)$ from every initial state and $g(W) = \max_y [W\phi(y) + R(y)]$, because a monotone policy always achieves $g(W)$; Theorem 6.5, the same two statements for the vigour bandit with $\psi$ increasing and $W^{**}$ increasing.

Significance

Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value $g(W)$ is the upper envelope of finitely many lines $W\phi(y) + R(y)$ whose slopes decrease in the threshold, so the optimal threshold moves monotonically with the subsidy and the hinge points of the envelope are the indices. The same argument gives Theorem 6.5, the admission-control indices of Section 6.7, and the marginal productivity indices of Niño-Mora; it is the reason Whittle indices are computable in closed form for bi-directional models. Its formalization establishes, on the platform, the first restless-bandit model with a proved index, and the general notions of passive set, indexability and Whittle index that every later restless-bandit statement will use.

None of this is machine-checked. The average-reward optimality notion is stated without the DP equation (6.6), through optimality from every initial state, which is what the equation's solution encodes on a finite state space and avoids the relative value function altogether.

Difficulty

The proof in the book is two paragraphs, but it stands on the reduction to monotone policies, which is only sketched: every deterministic stationary policy, from every initial state, drives the asset into an absorbing endpoint or a two-state cycle $\{z - 1, z\}$ whose average reward is that of the monotone policy $(z)$, so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly $\{x \ge x(W)\}$ for the smallest maximizing threshold. Formalizing this needs the average reward of a finite Markov chain as a limit determined by the stationary distribution of the recurrent class reached, for the two-point kernels of the model, and a case analysis of policies as $\{0,1\}$-strings. The envelope argument then needs that the smallest maximizer of $\max_y [W\phi(y) + R(y)]$ is nonincreasing in $W$ when $\phi$ is strictly decreasing, and that with $W^*$ strictly decreasing the maximizer is $\le x$ exactly when $W \ge W^*(x)$. Theorem 6.5 is the same with the roles of up and down exchanged. Nothing in Mathlib computes Cesàro limits of finite Markov chains.

Formalization scope

Restless bandits are the two-action DecisionProcesses of the superprocess module; average reward is a real limsup of Cesàro means of Bochner integrals over the chain law of the Bandit Algorithms model under the stationary kernel; the optimal average reward is a supremum over the finite type of deterministic stationary Markov policies and the finite state space, bounded by the reward bound. Both models are on Fin k with the book's states shifted down by one, kernels driftKernel p f that move to f x with probability p x, and the boundary conventions of $\phi$ and $\psi$ (the book's "convenient positive values") replaced by their values $1, 0$ and $0, 1$ at the two extreme thresholds; the model assumptions $\lambda(k) = \mu(1) = 0$, $\nu(1) = \rho(k) = 0$, rates in $[0, 1]$, and $r$ increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict $\psi$ admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires $k \ge 1$ and positive interior rates, which Theorem 6.4's hypothesis (i) implies.

Trivializing readings are excluded: indexability is monotonicity of the passive set over all real subsidies, the passive set is defined through policies optimal from every initial state, and the index identity is for every state. Welcome contributions: the average reward of a two-state cycle, the reduction of an arbitrary $\{0,1\}$-policy to a monotone one, and the envelope lemma for lines with decreasing slopes.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 6. doi:10.1002/9780470980033
• P. Whittle, Restless bandits: activity allocation in a changing world, Journal of Applied Probability 25(A), 1988. doi:10.2307/3214163
• R. R. Weber, G. Weiss, On an index policy for restless bandits, Journal of Applied Probability 27(3), 1990. doi:10.2307/3214547
• K. D. Glazebrook, C. Kirkbride, D. Ruiz-Hernandez, Spinning plates and squad systems: policies for bi-directional restless bandits, Advances in Applied Probability 38(1), 2006. doi:10.1239/aap/1143936141
• J. Niño-Mora, Restless bandits, partial conservation laws and indexability, Advances in Applied Probability 33(1), 2001. doi:10.1017/S0001867800010661
• C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queueing network control, Mathematics of Operations Research 24(2), 1999. doi:10.1287/moor.24.2.293