Motivation

Chapter 26 bounded the rate of uniform convergence by the Rademacher complexity; Chapter 27 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), introduces a second, metric measure of the size of a set of vectors, its covering numbers $N(r, A)$, the smallest number of Euclidean balls of radius $r$ needed to cover $A$, and connects the two through Dudley's chaining. Covering numbers behave well under scaling and under coordinatewise Lipschitz maps (Lemmas 27.2–27.3), they are easily bounded for sets lying in a low-dimensional subspace (Example 27.1), and the chaining lemma turns a bound on $\log N(r, A)$ at all scales $r = c2^{-k}$ into a bound on $R(A)$ (Lemma 27.4), with the clean corollary $R(A) \le \frac{6c}{m}(\alpha + 2\beta)$ when $\sqrt{\log N(c2^{-k}, A)} \le \alpha + \beta k$ (Lemma 27.5). The chapter's example recovers $R(A) = O(c\sqrt{d\log d}/m)$ for sets in a $d$-dimensional subspace, the technique that the book says would sharpen the fundamental theorem's sample complexity from $d\log(d/\epsilon)/\epsilon^2$ to $d/\epsilon^2$.

Setting

For $A \subseteq \mathbb{R}^m$ with the Euclidean metric, $A'$ is an $r$-cover of $A$ if every $a \in A$ is within distance $r$ of some $a' \in A'$, and $N(r, A)$ is the cardinality of the smallest $r$-cover (Definition 27.1). The Rademacher complexity $R(A) = \frac1m\mathbb{E}_\sigma\sup_{a \in A}\langle\sigma, a\rangle$ is Mission XX's. Chaining is run at the scales $c2^{-k}$, $k = 1, \dots, M$, where $c$ is a radius of a ball containing $A$, the book's $c = \min_{\bar a}\max_{a \in A}\|a - \bar a\|$ being the smallest such radius.

Formalization targets

Goal: Lemma 27.4

For a nonempty $A \subseteq \mathbb{R}^m$, $m \ge 1$, contained in the ball of radius $c$ about some $\bar a$, and every integer $M > 0$,

$$R(A) \le \frac{c\,2^{-M}}{\sqrt m} + \frac{6c}{m}\sum_{k=1}^M 2^{-k}\sqrt{\log N(c\,2^{-k}, A)}.$$

Milestones

Example 27.1 (the grid $r$-cover of a set of norm at most $c$ in a $d$-dimensional subspace, of size $(2c\sqrt d/r + 1)^d$); Lemma 27.2 (scaling and translation); Lemma 27.3 (the contraction principle); Lemma 27.5 (the corollary of chaining). Further item: Example 27.2 ($R(A) = O(c\sqrt{d\log d}/m)$ for sets in a $d$-dimensional subspace).

Significance

Chaining is the standard way to get sharp uniform convergence rates: a single-scale union bound (Massart's lemma at one resolution) loses a logarithmic factor, and summing Massart bounds over a geometric sequence of scales, applied to the increments between successive nearest cover points, recovers it. Lemma 27.4 is the discrete Dudley integral, and Lemma 27.5 is the form in which it is used: any polynomial-in-$1/r$ covering number gives $R(A) = O(c\sqrt{\log N}/m)$-type bounds without the extra logarithm. On the platform these items complete the complexity toolbox begun in Mission XX and provide covering numbers as a reusable notion; the contraction and scaling lemmas mirror their Rademacher counterparts.

Difficulty

Lemmas 27.2 and 27.3 are immediate: the image of an $r$-cover under the affine map is an $rc$-cover, and under a coordinatewise $\rho$-Lipschitz map a $\rho r$-cover, since $\|\varphi(a) - \varphi(a')\|^2 = \sum_i(\varphi_i(a_i) - \varphi_i(a'_i))^2 \le \rho^2\|a - a'\|^2$; formally they are manipulations of the infimum in $\mathbb{N} \cup \{\infty\}$. Example 27.1 needs an orthonormal basis of the subspace (Gram–Schmidt, or Mathlib's orthonormal bases of finite-dimensional inner product subspaces of $\mathbb{R}^m$ with the Euclidean structure) and the rounding of coordinates to a grid. Lemma 27.4 is the real work: after centering, take minimal $c2^{-k}$-covers $B_k$, the near-maximizer $a^*$ of $\langle\sigma, a\rangle$ (which depends on $\sigma$), its nearest points $b^{(k)} \in B_k$, the telescoping $a^* = (a^* - b^{(M)}) + \sum_k(b^{(k)} - b^{(k-1)})$, the bound $\|b^{(k)} - b^{(k-1)}\| \le 3c2^{-k}$, and Massart's lemma (Mission XX) on the sets $\hat B_k$ of increments, of cardinality at most $N(c2^{-k}, A)^2$; a formal proof must handle the supremum not being attained (approximate maximizers) and the dependence of all choices on $\sigma$ inside the finite average. Lemma 27.5 lets $M \to \infty$ using $\sum_k 2^{-k} = 1$ and $\sum_k k2^{-k} = 2$. Example 27.2 combines Example 27.1 at the scales $c2^{-k}$ with Lemma 27.5, with the book's constant $\log(2\sqrt d)$. The book's derivation uses the count without $+1$, so a proof needs the volumetric covering bound $(1 + 2c/r)^d$ for $d \ge 2$ and a direct count for $d = 1$.

Formalization scope

Vectors are Fin m → ℝ with an explicit Euclidean norm, because Mathlib's norm on that type is the sup norm; covers are arbitrary finsets of $\mathbb{R}^m$ and $N(r, A)$ is an infimum in $\mathbb{N} \cup \{\infty\}$, so no junk value arises when no finite cover exists, and the chaining statements read $N$ through ENat.toNat for the bounded sets they concern, where it is finite. Subspaces are Mathlib Submodules with finrank = d. Two statements are given with the constants their proofs support, and the item texts say so. Example 27.1's grid has $2c/\epsilon + 1$ points per coordinate, so the cover has size $(2c\sqrt d/r + 1)^d$, not $(2c\sqrt d/r)^d$, which is less than $1$ for $r > 2c\sqrt d$ and cannot bound a covering number of a nonempty set; Example 27.2 correspondingly has $\log(4\sqrt d)$ in place of $\log(2\sqrt d)$. Lemma 27.4 is stated for any enclosing radius $c$ about any center, since the proof only uses that $\{\bar a\}$ is a $c$-cover of $A$; the book's minimal radius is the special case, and this is the form Example 27.2 needs (with $\bar a = 0$ and $c = \max\|a\|$). Lemma 27.5 keeps the book's $\alpha, \beta > 0$.

Not stated: nothing else is in the chapter beyond the bibliographic remarks.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 27. doi:10.1017/CBO9781107298019
• R. M. Dudley, Universal Donsker classes and metric entropy, Annals of Probability 15(4), 1987. doi:10.1214/aop/1176991978
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216
• M. Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014. doi:10.1007/978-3-642-54075-2
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. doi:10.1017/9781108231596

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

Chapter 5 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks what happens to PAC learning when the labels are unreliable. In the classification noise model of Angluin and Laird, each label returned by the oracle is flipped independently with a fixed probability $\eta < 1/2$. The algorithms of Chapter 1 collapse at once: the elimination algorithm deletes a correct literal on the strength of a single mislabeled example, and the tightest-fit rectangle may not exist. The chapter's remedy is to learn from statistics: an algorithm that forms its hypothesis only from estimates of probabilities of simple events is insensitive to occasional wrong labels. Kearns's statistical query model makes this precise, replacing the example oracle by an oracle that returns the probability of any predicate of a labeled example to within a tolerance, and the main theorem (5.3) shows that every class learnable from statistical queries is PAC learnable in the presence of classification noise. The proof rests on a single identity, Equation (5.2), that expresses the true value of a statistical query in terms of three quantities that can each be estimated from noisy examples, and on the observation that a hypothesis's disagreement with the noisy label is an affine function of its true error, which lets the best of several candidate hypotheses be recognized without clean data.

Setting

The framework is that of Mission I. The noisy example law is that of $(x, b)$ with $x \sim D$ and $b = c(x)$ flipped with probability $\eta$. A statistical query is a predicate $\chi$ of a labeled example with value $P_\chi = \Pr_{x \sim D}[\chi(x, c(x)) = 1]$. The inputs split into $X_1$, where the label matters to $\chi$, and $X_2$, where it does not; $p_1 = D(X_1)$ and $D_1$ is $D$ conditioned on $X_1$. For conjunctions over $\{0,1\}^n$, $p_0(z)$ is the probability that a literal $z$ is set to $0$ and $p_{01}(z)$ the probability that it is $0$ on a positive example; $z$ is significant if $p_0(z) \ge \epsilon/8n$ and harmful if $p_{01}(z) \ge \epsilon/8n$.

Formalization targets

Goal: Equation (5.2)

For $0 \le \eta < 1/2$ and every statistical query $\chi$,

$$P_\chi = p_1 \cdot \frac{\Pr_{EX^\eta_{CN}(c, D_1)}[\chi = 1] - \eta}{1 - 2\eta} + \Pr_{EX^\eta_{CN}(c, D)}[\chi = 1 \wedge x \in X_2],$$

the probabilities on the right being taken under the noisy oracle.

Milestones

The §5.2 analysis behind Theorem 5.2 (the conjunction of all significant, non-harmful literals has error at most $\epsilon/2$); the product estimate bound of p. 115 ($AB - 2\tau' \le \hat A\hat B \le AB + 3\tau'$); the identity of p. 117 ($\gamma_h = \eta + (1 - 2\eta)\,\mathrm{error}(h)$).

Significance

Equation (5.2) is the entire mechanism of noise-tolerant learning in the statistical query model: the noisy oracle cannot be de-noised example by example, but the probability of any predicate can be recovered exactly from noisy probabilities, because on the inputs where the label matters the noise acts as a known affine contraction and on the others it acts not at all. Together with the p. 117 identity, which turns hypothesis selection into a comparison of noisy disagreement rates, and the Chernoff bounds of Mission IV, it yields Theorem 5.3 and hence noise-tolerant algorithms for every class the book has learned so far (conjunctions, decision lists, $k$-CNF). The §5.2 analysis is the first statistical-query algorithm and shows the pattern: a hypothesis defined by thresholds on a few probabilities, with enough slack between the thresholds that estimates suffice. None of this is machine-checked. The formalization fixes the noisy example law on the platform's sample framework and proves the exact identities on which the noise-tolerant simulation depends.

Difficulty

Equation (5.2) is a computation with the pushforward of a product measure: one must express the noisy law on $X_1$ as a mixture of the clean law and its label-flipped image, solve the affine relation for the clean probability, and combine with the restriction to $X_2$, where the flipped and unflipped labels give the same value of $\chi$; the degenerate case $D(X_1) = 0$, in which the conditional measure is zero and the first term vanishes, must be handled separately. The p. 117 identity is the same computation without the split. The §5.2 analysis is two union bounds over the $2n$ literals after the observation that a literal of the target is never harmful and that a literal of the hypothesis is never insignificant. The product lemma is elementary arithmetic with a case split at $A < \tau'$.

Formalization scope

The noisy oracle is a measure on labeled examples obtained by mapping the product of $D$ and a Bernoulli($\eta$) coin; the conditional $D_1$ is Mathlib's conditional measure; queries are arbitrary measurable predicates of a labeled example, with no tolerance or query-count bookkeeping. Theorem 5.3 itself, the definitions of efficient learnability from statistical queries (Definition 14) and of efficient noisy PAC learnability (Definition 13), Theorem 5.1, Theorem 5.2 as a statement about an algorithm with oracle access, and Corollary 5.4 are not stated: they quantify over query algorithms and their running times, for which this series has no model; the mission carries their exact probabilistic content. The error-propagation analysis of §5.4.2–5.4.3 with tolerance $\tau/27$ and the guessing resolution $\Delta$ is not stated beyond the product lemma, since the factor $1/(1-2\eta)$ is not in $[0,1]$ and the book's constant does not account for it. Hypotheses: $0 \le \eta < 1/2$ for the decomposition, $0 \le \eta \le 1$ for the disagreement identity, $\epsilon > 0$ for the conjunction analysis, all reals in $[0,1]$ for the product lemma.

Trivializing readings are excluded: the decomposition is an exact identity for every measurable query, and the conjunction bound is for the exact thresholds $\epsilon/8n$ with the union bound's $\epsilon/2$. Welcome contributions: the mixture representation of the noisy law, the restriction of a pushforward to $X_2$, and the two union bounds.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 5. doi:10.7551/mitpress/3897.001.0001
• D. Angluin, P. Laird, Learning from noisy examples, Machine Learning 2(4), 1988. doi:10.1007/BF00116829
• M. Kearns, Efficient noise-tolerant learning from statistical queries, Journal of the ACM 45(6), 1998. doi:10.1145/293347.293351
• M. Kearns, M. Li, Learning in the presence of malicious errors, SIAM Journal on Computing 22(4), 1993. doi:10.1137/0222052

Motivation

Chapter 4 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks whether the PAC model's demand for arbitrarily small error and confidence is essential. A weak learning algorithm need only, with some fixed positive probability, output a hypothesis that beats random guessing by a fixed margin. Schapire's theorem, the chapter's main result, says that this apparently much weaker requirement is equivalent to the original one: any weak learner can be converted, by running it on carefully filtered distributions and combining its hypotheses by majority votes, into a strong learner. The construction is boosting, which became one of the most influential ideas in machine learning. The chapter proves the equivalence in two steps. Boosting the confidence is elementary: run the learner several times and validate. Boosting the accuracy is the substance: a modest procedure that combines three hypotheses, each with error at most $\beta$ on its own distribution, into a majority with error at most $g(\beta) = 3\beta^2 - 2\beta^3 < \beta$, applied recursively until the error is driven below the target. The Chernoff bounds of the Appendix, the book's workhorse for estimating probabilities from samples, are what makes the validation steps rigorous.

Setting

The framework is that of Mission I. A class $C$ is weakly learnable using $H$ if for some advantage $\gamma > 0$, confidence $\delta_0 > 0$ and sample size $m$, an algorithm outputs hypotheses in $H$ that, for every target in $C$ and every distribution, have error at most $1/2 - \gamma$ with probability at least $\delta_0$; the algorithm's prediction $L(S)(x)$ is a measurable function of the sample and the instance together, as it is for every algorithm. Given a hypothesis $h_1$, the filtered distribution $D_2$ gives weight $1/2$ to the instances on which $h_1$ errs and $1/2$ to those on which it is correct, preserving relative weights within each part, and $D_3$ is $D$ conditioned on $h_1 \ne h_2$; the modest procedure outputs $\mathrm{majority}(h_1, h_2, h_3)$. Ternary majority trees over $H$ are the closure of $H$ under the majority of three. For confidence boosting, $k$ independent samples yield $k$ hypotheses, and a fresh sample selects the one with the fewest mistakes. Bernoulli trials are $m$ independent coin flips with success probability $p$.

Formalization targets

Goal: Theorem 4.9

If $C$ is weakly PAC learnable using measurable hypotheses in $H$, then $C$ is PAC learnable using the class of ternary majority trees with leaves from $H$: for all $\epsilon, \delta \in (0, 1/2)$ some sample size and some algorithm outputting majority trees achieve error at most $\epsilon$ with probability at least $1 - \delta$, for every target in $C$ and every distribution.

Milestones

Theorem 9.2 (the additive and multiplicative Chernoff bounds); the two facts of §4.2 behind confidence boosting (independent runs all fail with probability at most $(1 - \delta_0)^k$; the fewest-mistakes selection loses at most $\gamma$ with probability at least $1 - 2k e^{-m\gamma^2/2}$); Lemma 4.1 (the modest procedure: error at most $g(\beta)$).

Significance

Theorem 4.9 is one of the landmark results of learning theory: it shows that the PAC model has no intermediate strength, that Occam learning, weak learning and strong learning coincide, and that the resources of a strong learner can be bounded polylogarithmically in $1/\epsilon$ in memory and hypothesis size. Its constructive proof is the first boosting algorithm, ancestor of AdaBoost and of gradient boosting. Lemma 4.1 is the analytic core, a clean inequality about three hypotheses and three distributions in which the filtered distribution is exactly calibrated so that $h_1$ has no advantage on it. The Chernoff bounds are the concentration inequalities invoked throughout the book, and their formalization on the product law of Bernoulli trials makes every later "estimate to within $\gamma$ with confidence $1 - \delta$" step reusable. None of these is machine-checked in this form; the boosting theorem in the sample-complexity sense is, to our knowledge, not formalized anywhere.

Difficulty

Lemma 4.1 is a computation with conditional measures: writing $\mathrm{error}_D$ of the majority as the weight of the instances on which $h_1$ and $h_2$ both err plus $\beta_3$ times the weight of their disagreement, mapping weights under $D_2$ back to $D$ by the factors $2(1 - \beta_1)$ and $2\beta_1$ (Equation (4.1)), and maximizing the resulting polynomial in $\beta_1, \beta_2, \beta_3, \gamma_1, \gamma_2$; the degenerate cases where a conditioning event is null must be handled separately. The Chernoff bounds require the exponential moment method on a finite product measure. The confidence-boosting facts are the product bound for independent blocks and Hoeffding plus a union bound. The goal is a genuine construction: from a large sample of $D$ one must simulate the recursive algorithm Strong-Learn, whose calls to the weak learner on filtered distributions are served by rejection sampling from the remaining examples, bound the depth of the recursion by the growth of $g^{-1}$ iterates (Lemma 4.2), bound the number of examples consumed at each node (Lemmas 4.3–4.7) and allocate the confidence over all the places the simulation can fail; then package the result as a deterministic function of a sample of fixed size. An alternative route is available: weak learnability with a fixed sample size forces a finite VC dimension (a class shattering a large set defeats any fixed-size learner on the uniform distribution over it), after which Theorem 3.3 gives a consistent strong learner; but its hypotheses lie in $C$, not in the majority trees over $H$, so it does not prove the stated conclusion.

Formalization scope

The weak-learning hypothesis is the book's with constants $\gamma, \delta_0$ in place of the inverse polynomials, which is what the definition says for a fixed class; hypotheses in $H$ are required to be measurable, and the weak learner jointly measurable in the sample and the instance, because Strong-Learn runs it on distributions filtered through its own earlier outputs and the analysis integrates over the earlier samples (for an arbitrary function the combined failure event need not be measurable, and outer-measure bounds on separate runs do not combine); the conclusion is the book's hypothesis class, the majority trees over $H$, built as an inductive predicate. Filtered distributions use Mathlib's conditional measure, so that a null conditioning event yields the zero measure; Lemma 4.1 is stated for $0 \le \beta \le 1/2$ and holds in those degenerate cases too. The confidence-boosting milestone states the two probabilistic facts rather than the composite algorithm, whose sample indexing across runs and validation is bookkeeping; the selection rule is any rule minimizing mistakes. Chernoff's bounds are stated with non-strict inequalities in the events, for $0 \le p \le 1$ and $0 < \gamma \le 1$. Running time, the recursion-depth and sample-size lemmas with unspecified constants (4.2–4.8), and Exercises 4.1–4.3 are not stated.

Trivializing readings are excluded: the weak-learning guarantee is uniform over all targets and distributions with an advantage strictly positive, the strong conclusion is for every $\epsilon, \delta$, and Lemma 4.1 requires all three error bounds on their respective distributions. Welcome contributions: Lemma 4.1 itself, the Hoeffding bound on the product law, and the rejection-sampling lemma that turns a sample of $D$ into a sample of a filtered distribution.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 4 and Chapter 9. doi:10.7551/mitpress/3897.001.0001
• R. E. Schapire, The strength of weak learnability, Machine Learning 5(2), 1990. doi:10.1007/BF00116037
• Y. Freund, Boosting a weak learning algorithm by majority, Information and Computation 121(2), 1995. doi:10.1006/inco.1995.1136
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 1963. doi:10.1080/01621459.1963.10500830
• H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations, Annals of Mathematical Statistics 23(4), 1952. doi:10.1214/aoms/1177729330

Pooling as a design principle

A firm that holds inventory in five warehouses needs more safety stock than one that holds the same inventory in one warehouse, because the demands of five regions do not all run high at once. Eppen (1979) made this precise for a multi-location newsvendor and gave it its name, the risk-pooling effect. Chapter 7 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) follows the same idea through three settings in which pooling happens without physical consolidation: two retailers who ship stock to each other after seeing demand (transshipments, after Tagaras 1989), and plants that can each make more than one product (process flexibility, after Jordan and Graves 1995). The chapter's capstone is the theorem of Simchi-Levi and Wei (2012) that, among designs in which every plant makes two products and every product is made at two plants, a single long chain through all of them is best. This mission formalizes the chapter's numbered results, with that theorem as its goal.

Setting

Risk pooling. $N$ distribution centers face normally distributed per-period demands $D_i \sim N(\mu_i, \sigma_i^2)$ with correlation coefficients $\rho_{ij}$, and each runs a base-stock policy with holding cost $h$ and backorder cost $p$ per unit per period, so its optimal expected cost is the optimal newsvendor cost optNvCost h p D, the infimum over base-stock levels $S$ of $\mathbb{E}[h(S - D)^+ + p(D - S)^+]$. Merging the centers gives one facing the total demand, normal with mean $\sum_i \mu_i$ and variance $\sigma_0^2 = \sum_i \sum_j \sigma_i \sigma_j \rho_{ij}$ (pooledVariance).

Transshipments. Two retailers $i, j$ with base-stock levels $S_i, S_j$ face independent demands. After demand is observed, under complete pooling the retailer with a surplus sends the retailer with a shortage $Y_{ji} = \min\{S_j - D_j,\ D_i - S_i\}$ units (transship), and nothing moves otherwise. The type-1 service level is the probability of no stockout, $\alpha^0_i = \Pr[D_i \le S_i]$ without and $\alpha_i = \Pr[D_i - S_i \le Y_{ji}]$ with transshipments; the type-2 service level is the fill rate, one minus expected unmet demand over expected demand, $\beta^0_i$ and $\beta_i$ likewise.

Process flexibility. A flexibility design on $n$ products and $n$ plants is a set $E$ of (product, plant) pairs, an edge $(i, j)$ meaning plant $j$ can make product $i$. Given a demand realization $d$ and a common plant capacity $C$, the performance $P(d, E)$ (perf) is the maximum sales obtainable by assigning production along the edges of $E$ without exceeding any capacity or demand, the linear program (7.22) to (7.26). A balanced system (BalancedSystem) has equal capacities and an exchangeable demand vector, one whose joint law is invariant under permutations of the products, and $[E] = \mathbb{E}[P(D, E)]$ is the expected performance (expPerf). The named designs are the dedicated design $D_n = \{(i, i)\}$, the long chain $C_n$ in which plant $j$ also makes product $j + 1$ (and plant $n$ makes product $1$), the open chain $L_k$ obtained from $C_k$ by deleting the edge $(1, k)$, and $L^n_k$, the open chain on the first $k$ pairs together with the dedicated edges of the rest. A 2-flexibility design (TwoFlex) is one in which every product has exactly two plants and every plant exactly two products; $C_n$ is one, and so is any union of disjoint shorter chains.

Formalization targets

Goal: Theorem 7.9

For a balanced system of size $n \ge 2$ with exchangeable demand,

$$C_n \in \arg\max_{A \in \mathcal{F}_2} [A],$$

that is, $C_n$ is a 2-flexibility design and $[A] \le [C_n]$ for every 2-flexibility design $A$. This is long_chain_optimal.

Supporting targets

The chapter's route to the goal: Lemma 7.5, supermodularity of sales in the flexible edges of the long chain for every realization, $P(d, E) + P(d, E \setminus \{\alpha, \beta\}) \ge P(d, E \setminus \{\alpha\}) + P(d, E \setminus \{\beta\})$ for $E \subseteq C_n$; Corollary 7.6, the same in expectation; Lemma 7.7, the increments $[L^n_{k+1}] - [L^n_k]$ are nondecreasing in $k$, ending with $[C_n] - [L^n_n]$; and Lemma 7.8, $[C_n] = n([L_n] - [L_{n-1}])$.

Risk pooling, Theorem 7.1: $g^*_C \le g^*_D$, the optimal cost of the merged center is at most the sum of the optimal costs of the separate ones, with the covariance inequality $\sqrt{\sum_i\sum_j \sigma_i\sigma_j\rho_{ij}} \le \sum_i \sigma_i$ as a separate lemma.

Transshipments, Theorems 7.2 to 7.4: $\alpha_i = \alpha^0_i + |\partial\mathbb{E}[Y_{ji}]/\partial S_i|$, $\beta_i = \beta^0_i + \mathbb{E}[Y_{ji}]/\mathbb{E}[D_i]$, and all four post-transshipment service levels are nondecreasing in $S_i$.

Significance

Theorem 7.9 is the analytical answer to a question that had been settled only by simulation: Jordan and Graves reported that one chain through all plants achieves nearly twice the sales benefit of three short chains with the same number of edges, and Simchi-Levi and Wei proved that no arrangement of the same edge budget does better. It is the justification for the chaining guideline used in automotive and semiconductor capacity planning, and Lemma 7.8, which expresses the long chain through open chains, is what makes the long chain's performance computable by a greedy pass. Theorem 7.1 is the quantitative basis for consolidation decisions and for postponement, since a generic product is pooled inventory. Theorems 7.2 to 7.4 quantify what transshipments buy in service, which is the argument for allowing them despite their cost.

None of these results has a machine-checked proof. The book proves Lemma 7.7, Lemma 7.8 and Theorem 7.9 in full given Lemma 7.5, which it cites to Simchi-Levi and Wei, and omits the proofs of Theorems 7.3 and 7.4 and the identity (7.30) behind Lemma 7.8. Formalizing Lemma 7.5 and (7.30) means formalizing the structure of maximum flows on a cycle, which is reusable for the later results of Simchi-Levi and Wei on the long chain's performance relative to full flexibility and for the multi-echelon flexibility models the chapter cites.

Difficulty

The obvious approach to Theorem 7.9 is to compare $C_n$ with an arbitrary 2-flexibility design directly. Nothing in the definitions supports that: the two designs share no structure beyond their degree sequences. The book's argument instead routes everything through the long chain's own edges. Lemma 7.5 gives supermodularity only for subsets of $C_n$, and the decomposition of an arbitrary 2-flexibility design into disjoint cycles, each a relabeled long chain on a subsystem, is what allows the comparison. A solver must therefore prove that a 2-regular bipartite graph is a disjoint union of even cycles, that exchangeability makes every relabeling of a cycle worth the same as $C_{n_j}$ on its subsystem, and that the performance of a disjoint union is the sum of the performances of its parts.

Lemma 7.5 itself is where the combinatorics lives. It says that on the cycle $C_n$ the maximum flow is supermodular in the flexible edges, and the proof in Simchi-Levi and Wei goes through the structure of augmenting paths on a cycle. The natural first idea, that supermodularity follows from some general property of maximum flows, is false: maximum flow is not supermodular in arbitrary edge sets, and the lemma is specific to subsets of a single cycle.

Lemma 7.7 is where exchangeability is used, and it is used in a way that is easy to state and tedious to formalize: removing the edge $(2, 1)$ from $L^n_{k+1}$ leaves a design that is $L^n_k$ only after the pair $1$ is moved to the end, so the argument needs the invariance of $[E]$ under relabeling the products and plants by a common permutation. The book notes that Lemma 7.7, unlike Lemma 7.5, is false realization by realization.

For the transshipment theorems, the book differentiates a density formula by Leibniz's rule. Under the weaker hypothesis stated here, laws without atoms and with finite means, the derivative of $\mathbb{E}[Y_{ji}]$ in $S_i$ has to be obtained by dominated convergence from the pointwise derivative of a piecewise-linear function whose kinks lie on null sets.

Formalization scope

perf is a supremum over a set of reals, nonempty because $y = 0$ is feasible when $d \ge 0$ and $C \ge 0$, and bounded by $\sum_i d_i$; the demand is nonnegative for every outcome and the capacity nonnegative in BalancedSystem, and Lemma 7.5 carries these as hypotheses. The supremum is attained, but the definition does not assert it. Expected performance is a Lebesgue integral; the demand is integrable by assumption and $P(d, E)$ is $1$-Lipschitz in $d$, so the integrand is integrable, and a solver must prove this measurability rather than assume it.

Exchangeability is the equality of the laws of $(D_{\sigma(i)})_i$ and $(D_i)_i$ for every permutation $\sigma$. Designs are finite sets of pairs of Fin n; the chains are defined with finRotate, so indices wrap modulo $n$ and the closing edge of $C_n$ is $(1, n)$ in the book's numbering, which is the edge its proofs and Figure 7.3(c) use. Lemma 7.8 involves open chains on subsystems of sizes $n$ and $n - 1$; these are designs on Fin k evaluated on the first $k$ coordinates of the demand (subDemand, subPerf).

Theorem 7.1 states the optimal costs as infima of the newsvendor cost over all base-stock levels, on Mathlib's gaussianReal; a nonpositive pooled variance gives a degenerate law, for which the inequality still holds, so the statement is not trivialized by that convention. The transshipment theorems take the two demand laws as probability measures on $\mathbb{R}$ with no atoms (Theorem 7.2) and finite, positive means; the quantity $Y_{ji}$ is defined for all outcomes and the service levels are probabilities and expectations under the product law.

The definition module is shared by all eleven items. Beyond the milestones, formalizing the identity (7.30) as its own lemma and the disjoint-union additivity of perf would be natural contributions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 7. https://doi.org/10.1002/9781119584445
• G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5), 1979. https://doi.org/10.1287/mnsc.25.5.498
• G. Tagaras, Effects of pooling on the optimization and service levels of two-location inventory systems, IIE Transactions 21(3), 1989. https://doi.org/10.1080/07408178908966208
• W. C. Jordan and S. C. Graves, Principles on the benefits of manufacturing process flexibility, Management Science 41(4), 1995. https://doi.org/10.1287/mnsc.41.4.577
• D. Simchi-Levi and Y. Wei, Understanding the performance of the long chain and sparse designs in process flexibility, Operations Research 60(5), 2012. https://doi.org/10.1287/opre.1120.1082

Algorithmic Game Theory V: Stable Matching and Trading without Money

Motivation

When money is off the table and the Gibbard–Satterthwaite theorem (Mission III of this series) blocks general strategyproof choice, restricted preference domains reopen the door. The two great examples both come from allocation: Shapley–Scarf's housing market (1974), where Gale's Top Trading Cycle algorithm finds the unique core allocation and Roth (1982) showed the mechanism is strategy-proof; and the Gale–Shapley marriage market (1962), where deferred acceptance produces a stable matching, the men-optimal one, which Dubins–Freedman (1981) and Roth (1982) showed cannot be manipulated by any man. This machinery runs the US medical residency match and school choice systems worldwide, and the 2012 Nobel memorial prize to Roth and Shapley cites exactly the results of this mission. Chapter 10 (Schummer–Vohra, "Mechanism Design without Money") of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007) is the source text; its single-peaked §10.2 is left to a possible later mission, since it needs its own preference-domain machinery.

Setting

Marriage market (§10.4): finite sets $M$ of men and $W$ of women, each agent holding a strict preference ordering over the opposite side (the preference-profile vocabulary of Mission III; $P\,i\,a\,b$ reads "$i$ strictly prefers $a$ to $b$"). Following the book's dummy-partner convention, $|M| = |W|$ and a matching is a bijection $\mu : M \simeq W$. A pair $(m, w)$ blocks $\mu$ if each prefers the other to their assigned partner; $\mu$ is stable if no pair blocks it. A stable $\mu$ is male-optimal if every man weakly prefers it to every stable alternative. A coalition dominates $\mu$ if it can rematch within itself with every member strictly better off; the core is the set of undominated matchings.

Housing market (§10.3): a finite set $N$ of agents, agent $i$ owning house $i$, each with a strict preference over all houses; an allocation is a permutation of $N$. A coalition blocks an allocation if it can redistribute the houses its members own so that all are weakly and someone strictly better off.

Formalization targets

Goal (capstone) — Theorem 10.13

Any mechanism selecting the male-optimal stable matching is strategy-proof for the men: no man can misreport his ordering and obtain a wife he truly prefers.

Theorem 10.10 — existence

Every marriage market has a stable matching.

Theorem 10.11 / Gale–Shapley 1962 — male-optimality

Some stable matching is weakly best for every man simultaneously. This man-by-man form is Gale–Shapley's optimal assignment (1962, Theorem 2); the book's Theorem 10.11 phrases male-optimality as the absence of a stable alternative making every man weakly and some man strictly better off, which is equivalent for finite strict markets — the equivalence being a (short) theorem, the attribution follows Gale–Shapley.

Theorem 10.12 — the core

A matching is stable iff it is in the core of the matching game.

Theorems 10.6 and 10.7 — housing

The core of the housing market is a single allocation, and the mechanism selecting it is strategy-proof.

Significance

These are the foundational theorems of market design — the branch of mechanism design with the strongest record of deployed systems — and none of them exists in Lean. The mission also settles a methodological point for the series: algorithm-defined objects (deferred acceptance, top trading cycles) enter through the properties that characterize their outputs — male-optimality, core membership — so the theorems are statements about all mechanisms with the given property, and any construction of the algorithm proves the existence milestones. The matching vocabulary (bijections as matchings, blocking, stability, domination) is reusable for the college-admissions and roommates variants beyond this mission.

Difficulty

Existence (10.10) is the real formalization work: whether by formalizing deferred acceptance and its termination or by another route (e.g. Adachi's fixed-point formulation, which the book sketches as Theorem 10.14 via Tarski), the solver must build the proposal machinery. Male-optimality (10.11) rides on the same construction with the "no man is ever rejected by an achievable wife" invariant. The core equivalence (10.12) is deliberately light — a transposition embeds a blocking pair as a two-agent coalition. Housing uniqueness (10.6) needs the cycle-peeling induction of TTC. The two strategyproofness results are the subtle ones: both known proof routes (Dubins–Freedman's combinatorial argument, or Roth's via the blocking lemma) require careful bookkeeping of which coalitions can improve under a misreport, and the mechanism is pinned only by its defining property, so proofs must use optimality/core facts rather than algorithm internals.

Formalization scope

Preferences are strict total orders as in Mission III (IsPrefProfile), oriented "first argument preferred". Matchings are Equivs; the book's $|M| = |W|$ convention enters the existence statements as the hypothesis Nonempty (M ≃ W) and nothing else about cardinalities is assumed. Domination and house-blocking quantify a rematching Equiv together with the improving coalition, coalitions being sets closed under the rematching — single-agent and pair coalitions are special cases, so no separate pair-blocking clause is needed in the core theorems. Mechanisms in the strategyproofness results are arbitrary functions constrained only by their defining property (male-optimal selection; core selection), quantified before the misreport — nothing may be chosen with hindsight. Both sides keep finiteness only where used: the core equivalence (10.12) holds for arbitrary types and carries no Fintype.

Selected references

• D. Gale, L. S. Shapley, College admissions and the stability of marriage, Amer. Math. Monthly 69 (1962), 9–15. DOI
• L. Shapley, H. Scarf, On cores and indivisibility, J. Math. Econ. 1 (1974), 23–37. DOI
• L. E. Dubins, D. A. Freedman, Machiavelli and the Gale–Shapley algorithm, Amer. Math. Monthly 88 (1981), 485–494. DOI
• A. E. Roth, The economics of matching: stability and incentives, Math. Oper. Res. 7 (1982), 617–628. DOI
• A. E. Roth, Incentive compatibility in a market with indivisible goods, Econ. Letters 9 (1982), 127–132. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 10. DOI

Certify the classical quadratic separation between sensitivity and block sensitivity: $\alpha\ge2$.

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$, write $x^B$ for the input obtained by flipping the coordinates in $B$. Its sensitivity is $s(f)=\max_x|\{i:f(x^{\{i\}})\ne f(x)\}|$. Its block sensitivity $bs(f)$ is the largest number of pairwise disjoint nonempty sets $B$ that satisfy $f(x^B)\ne f(x)$ at a common input $x$.

The goal is to prove that for every $\varepsilon>0$ and every integer $S\ge2$, there is a total Boolean function with

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{2-\varepsilon}.$$

The construction milestone is Rubinstein’s quadratic separation: for each integer $m\ge1$, there is a function on $(2m)^2$ bits with

$$s(f)=2m,\qquad bs(f)=2m^2.$$

These exact bounds imply the goal because $bs(f)=s(f)^2/2$ and sensitivity grows without bound. This is a known theorem; the task is to formalize it using the campaign’s shared definitions.

The main combinatorial work is controlling sensitivity at every input and proving the matching block-sensitivity bounds. Lean represents functions as (Fin n → Bool) → Bool; both measures are maxima over all inputs. The goal reuses SensitivityCampaign.AchievesExponent, so it has exactly the same meaning as the campaign’s stronger targets. No composition theorem is required for this family argument.

References: David Rubinstein, Sensitivity vs. block sensitivity of Boolean functions, Combinatorica 15 (1995), 297–299, DOI. The statement and construction are also recalled in Theorem 1 of Madars Virza, Sensitivity versus block sensitivity of Boolean functions (2010), arXiv:1008.0521.

Motivation

In many auctions a bidder's value for what she wins depends on information held by others. The value of an oil lease, a spectrum licence or a piece of art to one bidder depends on survey data, market forecasts or expert opinions that other bidders hold privately. The model of interdependent values (Milgrom and Weber, 1982) captures this: each agent $i$ holds a private signal $s_i$, and every agent's value is a publicly known function of the whole signal profile $\mathbf s=(s_1,\dots,s_n)$.

With interdependent values, maximizing welfare in ex-post equilibrium is impossible unless the valuations satisfy the single-crossing condition (Maskin, 1992; Dasgupta and Maskin, 2000), and even single crossing does not suffice beyond single-item auctions with single-dimensional signals. Without any condition, there are valuations for which no deterministic mechanism achieves a bounded approximation ratio and no randomized mechanism does better than a factor $n$ (Eden, Feldman, Fiat and Goldner, ACM EC 2018; Examples 1.2–1.3 of the source). Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384v2, 2019) introduce submodularity over signals (SOS): raising one signal increases a value by less when the other signals are higher. They show that SOS valuations admit constant-factor, or signal-space-dependent, approximations in settings where single crossing fails, including combinatorial auctions. This mission formalizes their Theorem 6.1, the case of combinatorial auctions with single-dimensional signals taking $k$ values.

Timeline. Milgrom–Weber (1982) introduce the interdependent values model. Maskin (1992) and Dasgupta–Maskin (2000) show that single crossing makes efficient auctions truthful. Jehiel–Moldovanu (2001) show that efficient implementation fails generically with multidimensional signals. Eden–Feldman–Fiat–Goldner (2018) give approximations under a relaxed, $c$-single-crossing condition, with ratios depending on $c$ and $n$. Eden–Feldman–Fiat–Goldner–Karlin (2019; Mathematics of Operations Research, 2024) introduce SOS and prove Theorems 4.1, 5.1, 6.1 and 6.5.

Setting

There are $n$ agents and $m$ items, and $k\ge1$ signal values. Each agent $i$ has a signal $s_i\in\{0,1,\dots,k-1\}$, and $\{0,\dots,k-1\}^n$ is the grid. Agent $i$'s value for a bundle $T\subseteq[m]$ at the profile $\mathbf s$ is $v_{iT}(\mathbf s)\ge0$; the empty bundle is worth $0$, and for nonempty $T$, $v_{iT}$ is weakly increasing in every signal and strictly increasing in $s_i$. We write $(\mathbf s_{-i},x_i)$ for the profile with agent $i$'s signal replaced by $x$, and $(\mathbf s_A,\mathbf 0_B)$ for the profile that keeps the signals of the agents in $A$ and sets those in $B$ to $0$.

A function $w$ of the profile is SOS if for every coordinate $j$, all $x,\delta\ge0$ with $x+\delta\le k-1$, and grid profiles with $\mathbf s'_{-j}\le\mathbf s_{-j}$ coordinatewise,

$$w(\mathbf s_{-j},x+\delta)-w(\mathbf s_{-j},x)\;\le\;w(\mathbf s'_{-j},x+\delta)-w(\mathbf s'_{-j},x).$$

The setting is SOS when every $v_{iT}$ is.

A feasible allocation gives disjoint bundles $T_1,\dots,T_n$; its welfare at $\mathbf s$ is $\sum_i v_{iT_i}(\mathbf s)$. A deterministic mechanism maps reported profiles to an allocation and payments. Agent $i$'s utility is her value, at the true profile, for the bundle she receives at the reported profile, minus her payment. The mechanism is ex-post IC if truthful reporting maximizes each agent's utility whenever the others report truthfully, and ex-post IR if that utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

The mechanism k-HL runs, with probability $p_{RT}=\frac{k-1}{k+3}$, Random Threshold: choose $\ell$ uniformly in $\{1,\dots,k-1\}$, call $N_{\ge\ell}=\{i:s_i\ge\ell\}$ the high agents, allocate to them a feasible allocation maximizing $\sum_{i\in N_{\ge\ell}}v_{iS_i}(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$, and charge agent $i$ receiving $\bar T_i$ the price $v_{i\bar T_i}(\mathbf s_{-i},s_i=\ell-1)$. Otherwise it runs Random Sampling: split the agents uniformly at random into $A$ and $B$, allocate to $B$ a feasible allocation maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$, and charge nothing. In the Lean development (namespace InterdepSOS.KHL) these are rtAlloc, rtPay, rsAlloc and khlWelfare.

Formalization targets

Goal: Theorem 6.1 (p. 20)

For SOS valuations with $k$ signal values, every Random Threshold component and every Random Sampling component is ex-post IC and IR, and for every grid profile $\mathbf s$ and every feasible allocation $T^*$,

$$\sum_i v_{iT^*_i}(\mathbf s)\;\le\;(k+3)\,\mathbb E\bigl[\text{welfare of k-HL at }\mathbf s\bigr],$$

where the expectation is over $\ell$, over $(A,B)$ and over the coin choosing between the two mechanisms, and welfare is measured with true values at the truthful profile.

Milestones

1. Displays (6)–(7): the welfare of any allocation is at most $\mathsf{OTHER}+\mathsf{SELF}$, where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$ and $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$.
2. Random Sampling is ex-post IC-IR for every partition.
3. Random Threshold is ex-post IC-IR for every threshold.
4. Lemma 6.2: $\mathsf{SELF}\le(k-1)\,\mathbb E[\text{welfare of Random Threshold}]$.
5. Lemma 6.3: $\mathsf{OTHER}\le4\,\mathbb E[\text{welfare of Random Sampling}]$.

Significance

Theorem 6.1 is the paper's answer for general combinatorial auctions with single-dimensional signals and arbitrary bundle valuations, a setting where single crossing gives nothing and where the random-sampling technique of the single-parameter case (Theorem 4.1) is not enough on its own: Random Sampling alone covers only the contribution of the other agents' signals. The ratio $k+3$ depends on the size of the signal space but not on the number of agents or items. The same decomposition, with Random Threshold replaced by a bucketing mechanism, yields the $(2\log_2k+4)$-approximation for strong-SOS valuations (Theorem 6.5), so milestones 1 and 5 are shared by both results.

The result is proved in the paper; no machine-checked version is known to exist. A formalization fixes the incentive argument precisely (which data the allocation may depend on, how ties are broken) and makes the uniform averages over thresholds and partitions explicit. The development reuses the Key Lemma 3.1 of the paper, which is posed in a sibling mission of this series.

Difficulty

Two points resist a direct argument. First, incentive compatibility of Random Threshold requires that a high agent who changes her report within $\{\ell,\dots,k-1\}$ leaves the allocation unchanged, and this is true only if the argmax rule sees the reports through the proxy data $(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ alone: an argmax rule that breaks ties using the full report profile can make a high agent's bundle, and hence her utility, depend on her report. The formalization must therefore state precisely what the allocation rule may depend on. Second, the welfare bound for Random Sampling rests on the Key Lemma 3.1 (zeroing a uniformly random half of the other signals keeps, in expectation, half of an SOS value), which here has to hold on the discrete grid $\{0,\dots,k-1\}^n$, with SOS assumed only there; the expectations over partitions and thresholds are finite averages whose bookkeeping (agents in $A$ receive nothing, agents outside $N_{\ge\ell}$ receive nothing) must match the mechanism exactly.

Formalization scope

Agents are Fin n, items Fin m, bundles Finset (Fin m), signals natural numbers with the grid condition InGrid k s. All hypotheses on valuations (nonnegativity, monotonicity, strict monotonicity in the own signal, SOS) are imposed on grid profiles only, with the shifted coordinate staying below $k$; a condition on all of $\mathbb N^n$ would be stronger than the paper's. The empty bundle is worth $0$ and the monotonicity clauses concern nonempty bundles. Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values; agents outside the eligible set receive $\emptyset$.

The argmax allocations are produced by arbitrary selectors, functions of the threshold (or of $B$) and of the proxy profile, required to return a feasible maximizer of the proxy welfare; the theorems quantify over all such selectors. Expectations are finite uniform averages, $\frac1{k-1}\sum_{\ell=1}^{k-1}$ and $2^{-n}\sum_{B\subseteq[n]}$, never an existential or universal quantifier over $\ell$ or $B$. The ratio is stated against every feasible allocation, with welfare at true values, never with proxy values and never through a supremum. IC and IR are stated for every component of the mixture, with the paper's explicit payments. Random Sampling zeroes the signals of all of $B$, the agent's own included (the page's "$v_{ij}(\mathbf s_A,\mathbf 0_B)$" is read as $v_{iT}(\mathbf s_A,\mathbf 0_B)$). For $k=1$, $p_{RT}=0$ and the threshold average is the empty sum.

Lemmas 6.2 and 6.3 and displays (6)–(7) are stated for every feasible allocation (every assignment, for (6)–(7)), which is stronger than the paper's statements for a welfare-maximizing $T^*$.

Needed infrastructure: the Key Lemma 3.1 on the discrete grid, finite averages over subsets, and a lemma that a maximizer over a subfamily of allocations dominates any restriction of a feasible allocation. Contributions of proofs of the milestones in any order are welcome; the IC-IR milestones are independent of the welfare milestones.

The source is the arXiv preprint arXiv:1903.08384v2; the Mathematics of Operations Research (2024) version is not the cited source, and its numbering may differ.

Selected references

• A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
• A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, ACM EC 2018 (cited as [Eden et al., 2018] in the source).
• E. Maskin, Auctions and Privatization, in H. Siebert (ed.), Privatization, 1992 (cited as [Maskin, 1992] in the source).
• P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
• P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737
• P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00248