All missions

Motivation

Missions I and II of this series showed that finite hypothesis classes are learnable, with and without the realizability assumption, by empirical risk minimization. Chapter 5 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) asks the converse question: is prior knowledge, in the form of a restricted hypothesis class, really necessary? Could there be a universal learner, an algorithm that, given enough examples from any distribution, outputs a predictor of low risk? The No-Free-Lunch theorem (Theorem 5.1) answers no: for binary classification with the 0–1 loss over a domain $X$, for every learning algorithm and every training-set size $m$ smaller than $|X|/2$ there is a distribution on which the learner fails with probability at least $1/7$, even though that distribution is perfectly predictable by some function $f$, so that another learner (ERM over $\{f\}$) succeeds. The consequence for the framework is Corollary 5.2: over an infinite domain, the class of all functions is not PAC learnable. This is the first lower bound of the book and the reason the rest of it is about the complexity of hypothesis classes rather than about universal algorithms.

Setting

The framework is the UnderstandingML_Framework module of Mission I, cited as a reference. Binary classification over a domain $X$ uses examples in $X \times \{0,1\}$, hypotheses $h : X \to \{0,1\}$ and the 0–1 loss, so the risk of $h$ under a distribution $D$ over $X \times \{0,1\}$ is $L_D(h) = D(\{(x,y) : h(x) \ne y\})$, computed as the integral of the 0–1 loss. A learner is a function from samples of each size to hypotheses, and a sample of size $m$ has the law $D^m$. PAC learnability of a class $H$ (Definition 3.1) requires a sample-complexity function $m_H$ and a learner $A$ such that for every $\epsilon, \delta \in (0,1)$, every distribution $D$ over $X$ and every measurable labeling function $f$ realizable by $H$, samples of size $m \ge m_H(\epsilon,\delta)$ yield $L_{(D,f)}(A(S)) \le \epsilon$ with probability at least $1-\delta$.

Two conventions specific to this mission. The domain $X$ is assumed to have measurable singletons (the book's Remark 3.1 assumes away measurability issues); this makes the finitely supported distributions of the proof honest probability measures and makes every $L_D(h)$ under them a genuine integral. And "$m$ smaller than $|X|/2$" is written $2m < |X|$ in the extended natural numbers, so that an infinite domain satisfies it for every $m$.

Formalization targets

Goal: Theorem 5.1 (No-Free-Lunch)

Let $A$ be any learning algorithm for binary classification with respect to the 0–1 loss over a domain $X$ with measurable singletons, and let $m$ be a training-set size with $2m < |X|$. Then there exists a probability distribution $D$ over $X \times \{0,1\}$ such that

1. there is a measurable $f : X \to \{0,1\}$ with $L_D(f) = 0$;
2. there is a measurable set $E$ of samples of size $m$ with $D^m(E) \ge 1/7$ on which $L_D(A(S)) \ge 1/8$.

Milestones

Lemma B.1 (Appendix B). If $Z$ takes values in $[0,1]$ and $E[Z] = \mu$, then for every $a \in (0,1)$, $P[Z > 1-a] \ge (\mu - (1-a))/a$, and consequently $P[Z > a] \ge (\mu - a)/(1-a) \ge \mu - a$.

Equation (5.2). Under the hypotheses of Theorem 5.1 there are $D$ and a measurable $f$ with $L_D(f) = 0$ and $\mathbb{E}_{S \sim D^m}[L_D(A(S))] \ge 1/4$.

Corollary 5.2. For an infinite domain $X$ with measurable singletons, the class of all functions $X \to \{0,1\}$ is not PAC learnable.

Two further items: Exercise 5.1, the passage from an expectation of at least $1/4$ to a probability of at least $1/7$ of exceeding $1/8$ for a $[0,1]$-valued variable; and Exercise 5.3, the $k$-fold version of Equation (5.2), with bound $1/2 - 1/(2k)$ when $km \le |X|$, $k \ge 2$ and $X$ is nonempty.

Significance

The No-Free-Lunch theorem is the book's first impossibility result and the conceptual pivot of Part I: it shows that learnability is a property of the pair (hypothesis class, learner) and not of the learner alone, and it motivates the bias–complexity tradeoff of §5.2 and the VC-dimension of Chapter 6, whose lower bound (Theorem 6.7, the "only if" direction of the fundamental theorem) is proved by the same symmetrization argument. Corollary 5.2 is the statement that the class of all functions has infinite sample complexity, the negative half of the characterization of learnable classes.

Nothing here is machine-checked. The proof is combinatorial and elementary but has real content for a formalization: a finite subset $C$ of the domain, the $2^{2m}$ labelings of $C$, the uniform distribution on $C$ labeled by each of them, an exchange of a maximum, an average and a minimum over labelings and sample sequences, and a pairing argument on labelings that differ at exactly one unseen point. Lemma B.1 is a reverse Markov inequality for bounded variables that later chapters also use.

Difficulty

Lemma B.1 is Markov's inequality applied to $1 - Z$ and is the entry point; Exercise 5.1 is its instance with $a = 1/8$ and $\mu \ge 1/4$, giving $(1/4 - 1/8)/(7/8) = 1/7$, together with the inclusion of $\{\theta > 1/8\}$ in $\{\theta \ge 1/8\}$. Theorem 5.1 follows from Equation (5.2) and Exercise 5.1 once one knows that $S \mapsto L_D(A(S))$ is, under the finitely supported $D^m$, almost everywhere equal to a measurable function with values in $[0,1]$; the set $E$ is the intersection of the event with the finite support of $D^m$, which is measurable because singletons are. Equation (5.2) is the heart of the mission. One picks $C \subseteq X$ of size $2m$ (available because $2m < |X|$), lets $D_i$ be uniform on $C$ labeled by the $i$-th function $f_i : C \to \{0,1\}$ extended by $0$ off $C$, and computes $\mathbb{E}_{S \sim D_i^m}[L_{D_i}(A(S))]$ as an average over the $(2m)^m$ sequences of instances, which requires identifying $D_i^m$ as a finitely supported measure on sequences, that is, the product of finitely supported measures. The inequalities (5.4)–(5.6) exchange max, average and min and restrict to the unseen points, and the pairing argument shows that for each unseen point the average over $i$ of the indicator that $A$ errs on it is exactly $1/2$. Exercise 5.3 is the same argument with $|C| = km$, where at least $(k-1)m$ points are unseen. Corollary 5.2 takes $\epsilon < 1/8$, $\delta < 1/7$, $m = m_H(\epsilon,\delta)$ and a set $C$ of size $2m$ in the infinite domain, and derives the contradiction from Theorem 5.1 via the identification of $L_D$ for $D$ uniform on $C$ labeled by $f$ with the true error $L_{(D_X, f)}$ of Definition 3.1, where $D_X$ is uniform on $C$; the case $m = 0$ is handled separately with a single point.

Formalization scope

The items are stated in the joint-distribution form of the book's Chapter 5, with $D$ over $X \times \{0,1\}$ and $L_D$ the risk under the 0–1 loss, rather than in the $(D, f)$ form of Definition 3.1; Corollary 5.2 is the bridge and is stated with the framework's PACLearnable. Witness labeling functions are required to be measurable, because a non-measurable $f$ would make $L_D(f) = 0$ true by Lean's convention for non-integrable functions rather than by content. Clause (2) of Theorem 5.1 is stated in the inner form (a measurable set of probability at least $1/7$ inside the event) rather than as a lower bound on the outer measure of the event, which for a non-measurable event would be the weaker statement. The size condition uses ENat.card, so infinite domains satisfy it. Learners are deterministic functions of the sample; the book's argument goes through for randomized learners by averaging, but the framework does not model them.

Trivializing readings are excluded: the distribution must be a probability measure, the failing set must be measurable with an honest lower bound, and the witness $f$ must be measurable. Welcome contributions: the finitely supported product law on sequences, the averaging identity (5.3), and the pairing argument on labelings of $C$.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 5 and Appendix B. doi:10.1017/CBO9781107298019
• D. H. Wolpert, W. G. Macready, No free lunch theorems for optimization, IEEE Transactions on Evolutionary Computation 1(1), 1997. doi:10.1109/4235.585893
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3), 1989. doi:10.1016/0890-5401(89)90002-3
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.

Motivation

Mission I of this series set up the statistical learning framework of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) and proved, in the book's Chapters 2 and 3, that finite classes are PAC learnable under the realizability assumption. Chapter 4 removes that assumption. Its idea is the one that organizes the rest of the theory: if the empirical risks $L_S(h)$ of all hypotheses in $H$ are simultaneously close to their true risks $L_D(h)$, then minimizing $L_S$ over $H$ is nearly as good as minimizing $L_D$ over $H$, whatever the distribution $D$ is. A sample with that property is called $\epsilon$-representative (Definition 4.1), and a class for which representative samples are guaranteed at some sample size is said to have the uniform convergence property (Definition 4.3). Lemma 4.2 turns representativeness into a guarantee for ERM, Corollary 4.4 turns uniform convergence into agnostic PAC learnability, Hoeffding's inequality (Lemma 4.5) gives uniform convergence for a single hypothesis, and a union bound gives it for a finite class: Corollary 4.6, the capstone, says every finite class with a loss in $[0,1]$ is agnostic PAC learnable by ERM with sample complexity $\lceil 2\log(2|H|/\delta)/\epsilon^2 \rceil$.

Setting

The framework is the UnderstandingML_Framework module of Mission I, cited here as a reference. A domain $Z$ is a measurable space, hypotheses form a type with a class $H$, and a loss $\ell : H \times Z \to \mathbb{R}$ is given. The risk is $L_D(h) = \mathbb{E}_{z \sim D}\,\ell(h,z)$, the empirical risk on $S = (z_1,\dots,z_m)$ is $L_S(h) = \frac1m \sum_i \ell(h, z_i)$, and a sample of size $m$ has the product law $D^m$. A hypothesis is an ERM hypothesis for $S$ if it lies in $H$ and minimizes $L_S$ over $H$; a learner is a function from samples of each size to hypotheses, and an ERM learner returns an ERM hypothesis on every sample.

$S$ is $\epsilon$-representative with respect to $H$, $\ell$ and $D$ if $|L_S(h) - L_D(h)| \le \epsilon$ for every $h \in H$. $H$ has the uniform convergence property with the function $m^{UC}_H$ if for every $\epsilon, \delta \in (0,1)$ and every distribution $D$ over $Z$, a sample of $m \ge m^{UC}_H(\epsilon, \delta)$ i.i.d. examples is $\epsilon$-representative with probability at least $1 - \delta$. $H$ is agnostic PAC learnable with the function $m_H$ and the learner $A$ if $A$ returns hypotheses in $H$ and, for every $\epsilon, \delta \in (0,1)$, every $D$ and every $m \ge m_H(\epsilon,\delta)$, $L_D(A(S)) \le \min_{h' \in H} L_D(h') + \epsilon$ with probability at least $1 - \delta$ over $S \sim D^m$. As in Mission I, "with probability at least $1-\delta$" is an upper bound $\delta$ on the outer measure of the failure event, "$\min_{h' \in H} L_D(h') + \epsilon < L_D(h)$" is written as "$\exists h' \in H$, $L_D(h') + \epsilon < L_D(h)$", and sample-complexity functions are carried explicitly rather than as minimal functions.

Formalization targets

Goal: Corollary 4.6

Let $H$ be a finite hypothesis class, $Z$ a domain and $\ell : H \times Z \to [0,1]$ a loss function whose sections $\ell(h,\cdot)$ are measurable. Then

1. $H$ has the uniform convergence property with the function $m^{UC}_H(\epsilon,\delta) = \lceil \log(2|H|/\delta)/(2\epsilon^2) \rceil$;
2. every ERM learner for $H$ is an agnostic PAC learner with the function $m_H(\epsilon,\delta) = \lceil 2\log(2|H|/\delta)/\epsilon^2 \rceil$, which is $m^{UC}_H(\epsilon/2,\delta)$;
3. if $H$ is nonempty, $H$ is agnostic PAC learnable.

Milestones

Lemma 4.2. If $S$ is $\epsilon/2$-representative and $h_S$ is an ERM hypothesis for $S$, then $L_D(h_S) \le L_D(h) + \epsilon$ for every $h \in H$.

Corollary 4.4. If $H$ has the uniform convergence property with $m^{UC}_H$, then every ERM learner for $H$ is an agnostic PAC learner with the function $(\epsilon,\delta) \mapsto m^{UC}_H(\epsilon/2, \delta)$, and $H$ is agnostic PAC learnable as soon as an ERM learner exists.

Lemma 4.5 (Hoeffding's inequality). For a probability measure $D$, a measurable $\theta$ with $a \le \theta \le b$ almost surely and mean $\mu = \int \theta\,dD$, and $\epsilon > 0$,

$$D^m\Big[\Big|\tfrac1m \textstyle\sum_{i=1}^m \theta(\omega_i) - \mu\Big| > \epsilon\Big] \le 2\exp\!\big(-2m\epsilon^2/(b-a)^2\big).$$

Significance

Chapter 4 is where the book's account of learnability becomes distribution-free in the agnostic sense: nothing is assumed about $D$ beyond being a probability distribution, and the guarantee is relative to the best hypothesis in the class. Lemma 4.2 and Corollary 4.4 are the reduction that every later generalization bound in the book (VC dimension, Rademacher complexity, covering numbers, compression) plugs into: prove uniform convergence, get ERM learnability. Corollary 4.6 is the first instance, and its $\log|H|/\epsilon^2$ dependence, against the $\log|H|/\epsilon$ of the realizable case, is the standard illustration of the price of agnosticism. Hoeffding's inequality is stated in the form the book uses everywhere afterward, for the product law of one distribution, with an almost-sure range bound and the mean written as an integral.

Nothing here is machine-checked. Mathlib has no Hoeffding inequality for sums of i.i.d. bounded variables on a product measure in this form, so Lemma 4.5 is a genuine contribution; its proof in the book's Appendix B goes through Hoeffding's lemma on the moment generating function of a bounded centered variable and the Chernoff bounding method, both of which will be needed by the concentration results of later missions.

Difficulty

Lemma 4.2 is three inequalities on real numbers and is the intended entry point. Corollary 4.4 is Lemma 4.2 applied on the complement of the failure event of uniform convergence at $\epsilon/2$: the failure set of the learner is contained in the failure set of representativeness, and outer measure is monotone. Hoeffding's inequality is the substantial item: one needs the moment generating function bound $\mathbb{E}\,e^{\lambda(\theta-\mu)} \le e^{\lambda^2(b-a)^2/8}$ (Lemma B.7 of the book, by convexity of the exponential on $[a,b]$), independence of the coordinates under Measure.pi to factor the expectation of the product, Markov's inequality, and the optimization over $\lambda$; the two tails are treated separately and added. The degenerate cases are genuine: for $m = 0$ the bound is $2$ and the claim holds trivially, and for $a = b$ Lean's convention $x/0 = 0$ makes the bound $2$ again. Corollary 4.6 combines Hoeffding for each $h \in H$ with a union bound over the finite class and an arithmetic step showing that $m \ge \log(2|H|/\delta)/(2\epsilon^2)$ gives $2|H|e^{-2m\epsilon^2} \le \delta$; the empty class makes the uniform convergence clause vacuous. The second and third clauses of the goal then follow from Corollary 4.4, the third by exhibiting an ERM learner, which exists for a nonempty finite class by choosing a minimizer of $L_S$.

Formalization scope

The four items live in the general loss framework, not the binary-classification special case, because the chapter is stated for an arbitrary loss; Mission I's IsRepresentative and HasUniformConvergenceWith already carry the chapter's definitions, so no new definition module is introduced. Losses in Corollary 4.6 are real-valued with the range condition $\ell(h,z) \in [0,1]$ for every $z$ and measurability of $\ell(h,\cdot)$ for $h \in H$, which is what the book's "$\ell : H \times Z \to [0,1]$" and Remark 3.1 give. The book's "$m_H(\epsilon,\delta) \le \cdots$" is stated as "the guarantee holds with the function $\lceil \cdots \rceil$", the same convention as Mission I. In Corollary 4.4 the ERM clause is universal over ERM learners, matching "the ERM paradigm is a successful agnostic PAC learner" for every choice of minimizer; the existence of an ERM learner is a separate hypothesis for the learnability clause because a class with no minimizers on some sample has no ERM rule. Hoeffding's inequality is on i.i.d. coordinates of Measure.pi; the book's "$E[\theta_i] = \mu$" is the definition of $\mu$ rather than an assumption.

Trivializing readings are excluded: the failure events are bounded in outer measure, so measurability of the events is not a loophole; representativeness is required for every $h \in H$; the sample-complexity functions are the book's, with ceilings. Welcome contributions: Hoeffding's lemma on bounded centered variables, the factorization of the moment generating function under Measure.pi, and a reusable union bound over a finite class.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 4 and Appendix B. doi:10.1017/CBO9781107298019
• 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
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013, Chapter 2. doi:10.1093/acprof:oso/9780199535255.001.0001

Motivation

Chapters 2 and 3 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (Cambridge University Press, 2014, doi:10.1017/CBO9781107298019), set up the framework in which the whole book asks what learning is. A learner sees a sample drawn independently from an unknown distribution over examples, chooses a hypothesis from a class fixed in advance, and is judged by its risk, the expected loss on a fresh example. The natural rule is Empirical Risk Minimization: pick a hypothesis that does best on the sample. Chapter 2 shows that ERM over an unrestricted class overfits, that restricting the class is what makes learning possible, and that a finite class never overfits once the sample is larger than $\log(|H|/\delta)/\epsilon$ (Corollary 2.3). Chapter 3 turns this into a definition, Probably Approximately Correct learnability with its sample-complexity function $m_H(\epsilon, \delta)$, restates the finite-class result as Corollary 3.2, and then generalizes in two directions that the rest of the book lives in: the agnostic model, in which no hypothesis need be perfect and the learner competes with the best hypothesis in the class, and general loss functions, which cover regression, multiclass prediction and unsupervised tasks. Chapter 4 adds the notion of an ε-representative sample and of uniform convergence, the tool by which the finite-class result extends to the agnostic case; its definitions are included here since they complete the framework.

Setting

A domain $Z$ of examples, a class $H$ of hypotheses and a loss $\ell : H \times Z \to \mathbb{R}$. The risk of $h$ under a distribution $D$ is $L_D(h) = \mathbb{E}_{z \sim D}\,\ell(h, z)$ and its empirical risk on $S = (z_1, \dots, z_m)$ is $L_S(h) = \frac1m\sum_i \ell(h, z_i)$; a sample is drawn i.i.d., $S \sim D^m$; an ERM hypothesis minimizes $L_S$ over $H$; a learning algorithm maps samples of each size to hypotheses. In binary classification the examples are $(x, f(x))$ with $x \sim D$ over $X$ and $f$ a labeling function, and the true error is $L_{(D,f)}(h) = D(\{x : h(x) \ne f(x)\})$; the realizability assumption says some $h^\star \in H$ has $L_{(D,f)}(h^\star) = 0$. $H$ is PAC learnable if some sample-complexity function $m_H$ and algorithm guarantee, for all $\epsilon, \delta \in (0,1)$, all $D$ and all realizable $f$, true error at most $\epsilon$ with probability at least $1 - \delta$ from $m \ge m_H(\epsilon, \delta)$ examples; agnostic PAC learnability with respect to a loss asks instead for $L_D(h) \le \min_{h' \in H} L_D(h') + \epsilon$ for every distribution over $Z$.

Formalization targets

Goal: Corollary 3.2

Every finite hypothesis class is PAC learnable with sample complexity

$$m_H(\epsilon, \delta) \le \Big\lceil \frac{\log(|H|/\delta)}{\epsilon} \Big\rceil,$$

by the ERM rule: for a nonempty finite class of measurable hypotheses there is an ERM learner satisfying the PAC guarantee with that sample-complexity function.

Milestone

Corollary 2.3: under realizability, with $m \ge \log(|H|/\delta)/\epsilon$ examples, every ERM hypothesis has true error at most $\epsilon$ with probability at least $1 - \delta$.

Significance

Corollaries 2.3 and 3.2 are the first learning theorem of the book and the template for all later sample-complexity bounds: a bad hypothesis is consistent with an i.i.d. sample with probability at most $(1 - \epsilon)^m \le e^{-\epsilon m}$, and a union bound over the class turns this into a guarantee that holds uniformly over all distributions and all realizable labelings. Everything that follows, uniform convergence for finite classes, the fundamental theorem for classes of finite VC dimension, structural risk minimization, replaces the count $|H|$ by a finer measure of the class's complexity but keeps the argument. None of this is machine-checked. The mission fixes on the platform the objects that the rest of the series uses without change: risks, empirical risks, the product law of a sample, the ERM relation, and the four learnability notions of Definitions 3.1, 3.4, 4.1 and 4.3.

Difficulty

The milestone needs that, for a fixed measurable hypothesis whose true error exceeds $\epsilon$, the product law gives the event "zero empirical risk" probability at most $(1-\epsilon)^m$; this is the product structure of Measure.pi on the event that each labeled example lies in the measurable set where the hypothesis agrees with $f$, followed by $1 - \epsilon \le e^{-\epsilon}$, the union bound over the finite class and the observation that under realizability every ERM hypothesis has zero empirical risk, so a bad ERM hypothesis is a consistent bad hypothesis. The goal packages this as a learner: existence of an ERM hypothesis for every sample (a finite nonempty class has a minimizer), and the arithmetic of the ceiling.

Formalization scope

The framework is the book's, with the risk as a Bochner integral, the sample law as a product measure, ERM as a relation and learners as deterministic functions of the sample; failure probabilities are stated as upper bounds on the outer measure of the failure set, the strong form of "with probability at least $1 - \delta$"; the comparison with $\min_{h' \in H} L_D(h')$ is written without an infimum. Sample-complexity functions are carried explicitly: the book's $m_H$ as the minimal such function is not defined, and "$m_H \le f$" is stated as "the learner satisfies the guarantee with the function $f$". Hypotheses and labeling functions are assumed measurable (Remark 3.1). The union bound (Lemma 2.2) is Mathlib's measure_union_le and is not an item. Hypotheses: $\epsilon > 0$, $\delta \in (0,1)$, $H$ finite (and nonempty for the learner to exist).

Trivializing readings are excluded: the milestone's failure event ranges over every ERM hypothesis, and the goal quantifies over all distributions, all realizable labelings and all $\epsilon, \delta$. Welcome contributions: the product-law bound for a fixed hypothesis and the union bound over a finset, which every later mission of the series reuses.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 2–4. doi:10.1017/CBO9781107298019
• L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
• V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. doi:10.1007/978-1-4757-2440-0
• D. Haussler, Decision theoretic generalizations of the PAC model for neural net and other learning applications, Information and Computation 100(1), 1992. doi:10.1016/0890-5401(92)90010-D

Motivation

Chapter 2 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), gives a formal justification of Occam's Razor inside the PAC model. An Occam algorithm is judged not by the predictive power of its hypothesis but by how succinctly the hypothesis explains the sample before it: it must be consistent with the data and short, in the sense that its representation has fewer bits than the data it reproduces. The chapter's theorems say that, when the examples are drawn independently from a fixed distribution, such compression automatically yields prediction: a consistent hypothesis drawn from a small class is, with high probability, accurate on unseen examples. This turns the design of PAC learning algorithms into a combinatorial task, finding a short consistent hypothesis, and the chapter demonstrates the method three times: it shaves a logarithmic factor off the conjunction bound of Chapter 1, it learns conjunctions with few relevant variables through the greedy set-cover heuristic, and it learns Rivest's decision lists, a class strictly more expressive than $k$-CNF and $k$-DNF, by a greedy algorithm whose correctness is a one-line consequence of consistency.

Setting

The framework is that of Mission I: a measurable instance space, concepts as boolean functions, a target distribution $D$, the product law of a sample of $m$ labeled examples, the error $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \neq c(x)]$, and consistency of a hypothesis with a sample. Hypotheses may be represented by binary strings through a representation map, with size the bit length; an $(\alpha, \beta)$-Occam algorithm outputs a consistent hypothesis of size at most $(n \cdot \mathrm{size}(c))^\alpha m^\beta$ with $0 \le \beta < 1$. The set cover problem asks for a minimum subcollection of a collection $\mathcal{S}$ of subsets of a finite universe $U$ that covers $U$; the greedy heuristic repeatedly picks the set covering the most uncovered elements. A $k$-decision list is a sequence of conditions, each a conjunction of at most $k$ literals, with a bit attached to each and a default bit; it evaluates to the bit of the first satisfied condition. The greedy decision-list algorithm repeatedly finds a useful condition, one satisfied by some remaining examples all of which carry the same label, appends it with that label and removes those examples.

Formalization targets

Goal: Theorem 2.2 (Occam's Razor, cardinality version)

For a finite hypothesis class $H$, a target $c$, a distribution $D$ and $0 < \epsilon \le 1$, the probability that a sample of $m$ examples is consistent with some $h \in H$ of error greater than $\epsilon$ is at most $|H|(1 - \epsilon)^m$; hence

$$m \ge \frac{1}{\epsilon}\Big(\ln|H| + \ln\frac{1}{\delta}\Big)$$

makes this probability at most $\delta$, and any algorithm that outputs a consistent hypothesis from $H$ has error greater than $\epsilon$ with probability at most $|H|(1-\epsilon)^m$.

Milestones

Theorem 2.1 (an $(\alpha, \beta)$-Occam algorithm is a PAC algorithm, with explicit sample-size conditions in place of the constant $a$); the greedy set-cover bound of §2.3 ($|U_i| \le (1 - 1/\mathrm{opt})^i|U|$ and $\mathrm{opt}\ln|U|$ sets cover); the improved conjunction bound of §2.2; Theorem 2.3 ($k$-decision lists are PAC learnable by the greedy algorithm, which never fails and whose outputs are consistent).

Significance

Theorem 2.2 is the single most used tool of the subject: every finite-class sample bound, including the ones for conjunctions, decision lists, $k$-CNF and the discretized geometric classes, is an instance of it, and the Vapnik–Chervonenkis theory of Chapter 3 is its extension to infinite classes with the growth function in place of $|H|$. Theorem 2.1 is the philosophical statement, that succinct explanation implies prediction, and its converse (Exercise 2.3, and more strongly the boosting theorem of Chapter 4) makes Occam learning equivalent to PAC learning. The greedy set-cover bound is Chvátal's classical approximation guarantee, used in the book for learning with few relevant variables and again in later chapters. Theorem 2.3 is Rivest's result, and its proof exhibits the pattern "consistency by construction plus a counting bound" in its purest form. None of these is machine-checked. Their formalization gives the platform the union-bound-over-a-finite-class argument once and for all, in a form that the later missions of this series reuse verbatim.

Difficulty

Theorem 2.2 requires that, for a fixed measurable hypothesis with error greater than $\epsilon$, the product law gives the event "consistent with all $m$ examples" probability at most $(1 - \epsilon)^m$, which is the product structure of Measure.pi applied to the event that each coordinate lies in the set where $h$ agrees with $c$; the union bound over $H$ and the elementary inequality $(1 - \epsilon)^m \le e^{-\epsilon m}$ finish. Theorem 2.1 adds only the count of binary strings of length at most $K$ and arithmetic with real exponents. The set-cover bound is a discrete induction: an optimal cover of $U$ restricted to the uncovered elements has at most $\mathrm{opt}$ sets, so one of them, hence the greedy choice, covers a $1/\mathrm{opt}$ fraction; the covering clause needs the strict inequality $1 - 1/\mathrm{opt} < e^{-1/\mathrm{opt}}$. Theorem 2.3 needs that a run of the greedy algorithm never repeats a condition (its satisfied examples are removed), so outputs lie in an explicit finite class, that the first condition of the target list satisfied by a remaining example is useful, and that a complete run is consistent; the bound is then Theorem 2.2.

Formalization scope

Everything is in the sample-complexity sense on the Mission I framework; running time is not modelled and "efficient" is dropped from every statement, which is recorded in the natural-language statements. Theorem 2.2's constant $b$ is $1$ with natural logarithms; Theorem 2.1's constant $a$ is replaced by three explicit sufficient conditions. Hypotheses in the finite class are required to be measurable. The greedy heuristic and the greedy decision-list algorithm are relations (any tie-breaking), and the theorems quantify over every run; the decision-list theorem is stated for every $k$ with the $k$-conjunctions as conditions, so that its hypothesis is a $k$-decision list rather than the expansion the book sketches for $k > 1$. The conjunction count is $3^n + 1$, including the empty concept that the elimination algorithm outputs on a sample without positive examples. The few-relevant-variables algorithm of §2.3 is not stated (its bound has an unspecified constant and $m$ on both sides). Hypotheses: $0 < \epsilon \le 1$, $0 < \delta$ (and $\delta < 1$ where $\ln(1/\delta)$ must be nonnegative).

Trivializing readings are excluded: the bad-consistent event is over all of $H$, the decision-list failure event ranges over every possible output, and the set-cover bound holds for every greedy run. Welcome contributions: the product-law bound for a fixed hypothesis, the union bound over a finset, the string-counting lemma, and the no-repetition lemma for greedy runs.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 2. doi:10.7551/mitpress/3897.001.0001
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Occam's razor, Information Processing Letters 24(6), 1987. doi:10.1016/0020-0190(87)90114-1
• V. Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4(3), 1979. doi:10.1287/moor.4.3.233
• R. L. Rivest, Learning decision lists, Machine Learning 2(3), 1987. doi:10.1007/BF00058680
• D. Haussler, Quantifying inductive bias: AI learning algorithms and Valiant's learning framework, Artificial Intelligence 36(2), 1988. doi:10.1016/0004-3702(88)90002-1

Motivation

Chapter 1 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), introduces Valiant's Probably Approximately Correct model, the framework for the whole book. A learner sees labeled examples of an unknown target concept drawn from an unknown but fixed distribution, and must output a hypothesis that, with probability at least $1 - \delta$ over the sample, misclassifies a fresh example with probability at most $\epsilon$; the model is distribution-free, and the hypothesis is judged on the same distribution it was trained on. The chapter's three positive results are the templates for everything that follows. The rectangle game (Theorem 1.1) shows that an infinite class can be learned from a finite sample by exploiting the geometry of the error region. Conjunctions (Theorem 1.2) are learned by the elimination algorithm, whose analysis, a union bound over "bad" literals, is the prototype of every sample-size bound in the book. And 3-CNF formulae (Theorem 1.4) are learned by a change of variables that reduces them to conjunctions, which, set against the intractability of learning 3-term DNF as 3-term DNF (Theorem 1.3), is the reason the final definition of the model lets the hypothesis class differ from the concept class.

Setting

The instance space is a measurable space $X$, a concept is a function $c : X \to \{0, 1\}$, and the target distribution $D$ is a probability measure on $X$. The error of a hypothesis $h$ is $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \ne c(x)]$. A sample of $m$ examples is $S = ((x_1, c(x_1)), \dots, (x_m, c(x_m)))$ with the $x_i$ independent draws from $D$; a learning algorithm is a function from samples to hypotheses; it has the $(\epsilon, \delta)$ guarantee on a class $C$ if for every $c \in C$ and every $D$ the probability that its hypothesis has error greater than $\epsilon$ is at most $\delta$; $C$ is PAC learnable using $H$ if for all $\epsilon, \delta \in (0, 1/2)$ some sample size and algorithm with hypotheses in $H$ achieve the guarantee. For $X = \{0,1\}^n$ a literal is a variable or its negation and a conjunction is a finite set of literals; the elimination algorithm starts from all $2n$ literals and deletes every literal contradicted by a positive example. For $X = \mathbb{R}^2$ the concepts are the closed axis-aligned rectangles and the tightest-fit algorithm returns the smallest rectangle containing the positive examples. A 3-CNF formula is a conjunction of clauses of at most three literals; the expansion $a \mapsto a'$ records for each triple $(u, v, w)$ of literals the value $u \vee v \vee w$.

Formalization targets

Goal: Theorem 1.2

Conjunctions of boolean literals are PAC learnable by the elimination algorithm: for every target conjunction, every distribution on $\{0,1\}^n$ and $\epsilon, \delta > 0$, the elimination hypothesis is consistent with every sample labeled by the target, and with

$$m \ge \frac{2n}{\epsilon}\Big(\ln 2n + \ln\frac{1}{\delta}\Big)$$

examples its error exceeds $\epsilon$ with probability at most $\delta$; hence conjunctions are PAC learnable using conjunctions.

Milestones

Theorem 1.1 (rectangles by the tightest fit, $m \ge (4/\epsilon)\ln(4/\delta)$) and Theorem 1.4 (3-CNF formulae by elimination over the $(2n)^3$ expanded variables, the hypothesis being itself a 3-CNF formula).

Significance

Theorem 1.2 is Valiant's original result and the first instance of the two ideas that organize the subject: a hypothesis that is more specific than the target never errs on negative examples, and the error of the hypothesis decomposes as a sum over a polynomial number of "bad" events, each of which is avoided with probability exponentially close to one. Theorem 1.1 is the first learning result for an infinite concept class and the seed of the Vapnik–Chervonenkis theory of Chapter 3. Theorem 1.4 is the first reduction between learning problems and, together with Theorem 1.3, the demonstration that the choice of hypothesis representation can separate tractable from intractable. None of these theorems is machine-checked. Formalizing them fixes, for the rest of the series, the framework in which the error of a hypothesis, the law of a sample and the learnability of a class are stated, so that the Occam, VC-dimension, boosting and noise results of later chapters can be stated on the same objects.

Difficulty

The elimination analysis needs that the hypothesis contains every literal of the target, that its error is at most the sum over its literals $z$ of $p(z) = \Pr[c(a) = 1 \wedge z = 0 \text{ in } a]$, and that a literal with $p(z) \ge \epsilon/2n$ survives $m$ independent examples with probability at most $(1 - \epsilon/2n)^m$; the probabilistic content is the independence of the coordinates of the sample law, which is a product measure, and the inequality $1 - x \le e^{-x}$. The rectangle analysis is the four-strip argument, which for an arbitrary distribution, possibly with atoms, requires choosing the strip $\{y \ge t^*\}$ with $t^*$ the supremum of the heights at which the strip has weight at least $\epsilon/4$ and using the left-continuity of the weight in the height. The 3-CNF result transports the conjunction bound along the injective expansion: the pushforward of the sample law is the sample law of the expanded distribution, and the error of the composed hypothesis equals the error over the expanded variables. The deduction of PACLearnable from the explicit bounds is a choice of sample size.

Formalization scope

The model is stated in the sample-complexity sense: algorithms are functions of the sample, and the guarantee bounds the outer measure of the failure set under the product law of the sample, which is the strong form of "with probability at least $1 - \delta$" and requires no measurability of the failure set. Running time, and hence "efficiently", is not modelled, and the hardness Theorem 1.3 is not stated; each theorem carries instead the explicit algorithm and the explicit sample bound of the book's analysis. Concepts on general instance spaces are required to be measurable in the guarantee. The cube is $\{0,1\}^n$ as functions Fin n → Bool; the expanded variables are indexed by the triples of literals, so $N = (2n)^3$ is a Fintype.card. Rectangles are closed, possibly empty; the tightest fit of a sample without positive examples is the empty concept. Hypotheses: $\epsilon > 0$, $0 < \delta < 1$; the sample bounds are as printed, with natural logarithms.

Trivializing readings are excluded: the failure bound is uniform over all distributions and all targets in the class, consistency is asserted for every sample labeled by the target, and the learnability clause quantifies over all $\epsilon, \delta$. Welcome contributions: the product-law bound $\Pr[\text{a fixed event of probability} \ge p \text{ is missed by all } m \text{ examples}] \le (1 - p)^m$, the union bound over literals, and the pushforward identity for the expanded sample.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 1. doi:10.7551/mitpress/3897.001.0001
• L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• L. Pitt, L. G. Valiant, Computational limitations on learning from examples, Journal of the ACM 35(4), 1988. doi:10.1145/48014.63140

When is the auctioneer's revenue acceptable?

The Vickrey-Clarke-Groves auction is the textbook mechanism for selling several objects at once: bidders report valuations for bundles, the auctioneer computes the welfare-maximizing allocation, and each winner pays the externality it imposes on the others. Truthful bidding is a dominant strategy and the outcome is efficient. Yet Ausubel and Milgrom (2006) catalogued its practical defects: revenue can be zero when the objects are valuable, revenue can fall when bidders or bids are added, losing bidders can profit by colluding, and a bidder can profit from false identities. Chapter 15 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reproduces those examples and then gives the cooperative-game answer to when they cannot occur: the VCG payoff vector should lie in the core, the set of outcomes no coalition of auctioneer and bidders can improve upon, and it does so for every set of participants exactly when the coalitional value function is bidder-submodular. This mission formalizes that characterization, Theorem 15.3, together with the lemma and theorem leading to it.

Setting

Players are the auctioneer $0$ and bidders $1, \dots, n$. A coalitional value function $V$ assigns to each coalition $T$ the value it can create by trading among themselves: $0$ if the auctioneer, who owns the objects, is not in $T$, and otherwise the optimal value of the auctioneer's allocation problem among the bidders of $T$, each bidder receiving at most one bundle and bundles disjoint (capValue). Two properties of $V$ are all the theory uses: coalitions without the auctioneer are worthless, and adding players never lowers the value (IsCoalitionalValue).

A payoff vector $\pi$ gives each player a payoff. It lies in the core of the game on a coalition $S \ni 0$ (InCore V S π) if the payoffs of $S$ sum to $V(S)$ and no sub-coalition $T \subseteq S$ is paid less than $V(T)$. The VCG payoff vector $\bar\pi(S)$ (vcgPayoff) pays each bidder $k$ its marginal contribution $V(S) - V(S \setminus k)$, which is its valuation minus its VCG payment, and the auctioneer the remainder. A core vector is bidder dominant (BidderDominant) if every bidder weakly prefers it to every other core vector. $V$ is bidder-submodular (BidderSubmodular) if each bidder's marginal contribution weakly decreases as the coalition grows.

Formalization targets

Goal: Theorem 15.3

For a coalitional value function $V$, the following are equivalent: (i) $V$ is bidder-submodular; (ii) for every coalition $S \ni 0$ the core equals $\Pi_S = \{\pi : \sum_{k \in S}\pi_k = V(S),\ 0 \le \pi_k \le \bar\pi_k(S)\ \forall k \in S \setminus 0\}$; (iii) for every coalition $S \ni 0$, $\bar\pi(S)$ lies in the core of $S$. This is vcg_core_characterization.

Supporting targets

That the combinatorial auction's $V$ is a coalitional value function; Lemma 15.1, the core is nonempty and each bidder's VCG payoff is the largest it receives at any core point; Theorem 15.2, the VCG vector is the bidder-dominant core point when it is in the core, and otherwise no bidder-dominant point exists and the auctioneer's VCG payoff is below every core payoff.

The English auction of Sect. 15.2, presented as a primal-dual interpretation of a linear program, and the combinatorial allocation problem of Sect. 15.3 carry no numbered results and are not targets.

Significance

Theorem 15.3 is the criterion an auction designer can check before running a VCG auction: when the bidders' valuations make $V$ bidder-submodular (for instance when objects are substitutes), the VCG outcome is a competitive outcome, its revenue meets the core benchmark, and none of the defects of Sect. 15.4.2 can arise; when they do not, Theorem 15.2 says the auctioneer's revenue is strictly below every competitive outcome. The result underlies the ascending package auctions proposed as VCG alternatives and the procurement auctions used in supply chains, such as the combinatorial reverse auctions of the chapter's case study.

None of these results has a machine-checked proof. The book proves all three. The formal treatment of the core and of marginal-contribution vectors is reusable for the cooperative-game models of cost allocation in supply chains.

Difficulty

The theorems are combinatorial statements about a function on finite sets, and the difficulty is entirely in the bookkeeping of coalitions. Lemma 15.1 needs the explicit core vector of its proof to be verified against every sub-coalition, which splits into cases on whether the sub-coalition contains the auctioneer and the distinguished bidder. The implication (i) $\Rightarrow$ (ii) telescopes marginal contributions along a chain of coalitions between a sub-coalition and $S$, and the chain has to be built and its sum computed. The implication (iii) $\Rightarrow$ (i) is the delicate one: a failure of submodularity is a pair of nested coalitions, and the proof needs to extract from it a single-element step at which a bidder's marginal contribution increases, then show the two-bidder sub-coalition blocks the VCG vector. The obvious idea, that submodularity can be checked only on single-element extensions, is correct but must itself be proved.

Formalization scope

Coalitions are finite sets of Fin (n+1) and payoff vectors are functions on all players; the core and $\Pi_S$ constrain only the players of $S$, so vectors differing outside $S$ are interchangeable. The core's budget equation sums over all players of the coalition, including the auctioneer, which is what the book's proofs use although its displayed definition sums over the bidders. The theorems take $V$ as any function with the two properties, and the auction's $V$ is shown to have them; the VCG vector is defined by the formulas (15.23) and (15.24) rather than through the payment rule, whose equivalence is the book's derivation. Bidder-submodularity is stated for $S \subseteq S'$ rather than proper inclusion, which changes nothing.

The definition module is shared by all five items. The single-item English auction as a primal-dual algorithm and the condition on individual preferences (substitutes) that implies bidder-submodularity are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 15. https://doi.org/10.1002/9781119584445
• L. M. Ausubel and P. Milgrom, The lovely but lonely Vickrey auction, in Combinatorial Auctions, MIT Press, 2006. https://doi.org/10.7551/mitpress/9780262033428.003.0002
• S. de Vries and R. V. Vohra, Combinatorial auctions: a survey, INFORMS Journal on Computing 15(3), 2003. https://doi.org/10.1287/ijoc.15.3.284.16077
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x

When competing firms settle on prices and allocations

Revenue management is practised by firms that compete: airlines matching fares while allocating seats, retailers ordering stock and then pricing to clear it, hotels protecting rooms for late high-paying guests. Chapter 8 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) surveys the economics behind these situations: monopoly pricing and mechanism design, the Coase problem, advance-purchase discounts, and oligopoly in quantities (Cournot), in prices (Bertrand, Bertrand–Edgeworth with capacities), in newsvendor capacities and in RM allocations. Most of its numbered results are quoted from the literature; what the book itself establishes is a family of equilibrium arguments built on Talluri's equilibrium graph: when each firm's best response moves monotonically with the rival's action, following best-response arcs must end in an equilibrium pair. This mission formalizes those arguments, with Proposition 8.3, existence of an equilibrium in offer sets under the multinomial-logit choice model, as the goal.

Setting

A two-firm game on finite chains of strategies has payoffs $u_1, u_2$, best responses and pure Nash equilibria (IsBestResponse1, IsNashEquilibrium); its equilibrium graph has no crossing arcs (NoCrossing1) when best-response arcs $(k_2, k_1)$, $(l_2, l_1)$ with $k_2 < l_2$ always have $k_1 \le l_1$. The chapter's games are: the RM duopoly of Sect. 8.4.1.3, two firms with capacity $C$ and fares $p_L < p_H$ whose high-fare demand spills over to the rival beyond its protection level (spilloverDemand), each firm answering with Littlewood's protection level (littlewoodResponse); the duopoly newsvendor of Example 8.16 with effective demands $R_1 = D_1 + (D_2 - x_2)^+$ (effectiveDemand); linear Cournot (cournotPayoff); Bertrand–Edgeworth price competition with capacity $C$ per firm, linear demand and efficient rationing (beSales, bePayoff, IsBEEquilibrium); the advance-purchase model of Sect. 8.3.6 (peakLoadRevenue, advancePurchaseRevenue); and the one-period offer-set game of Sect. 8.4.3.2, where a firm offering its first $k$ products earns $g(C_k)/(W_1(k) + W_2(l) + w_0)$ with $g(C_k) = \sum_{j \le k} w_j(p_j - \Delta) - w_0\delta$ (OfferFirm, offerPayoff1, CaseI, CaseII).

Formalization targets

Goal: Proposition 8.3

If both firms are in Case I ($g(G^*) \ge 0$) or both in Case II ($g < 0$ on every complete set), the offer-set game has a pure-strategy equilibrium in complete sets: mnl_offer_set_equilibrium.

Supporting targets

The equilibrium-graph lemma, monotone best responses for both firms give an equilibrium (Sect. 8.4.1.3); Proposition 8.1, Littlewood responses in the RM duopoly are monotone in the rival's protection level, and the resulting equilibrium of the RM duopoly game; Example 8.16, duopoly newsvendor capacities total at least the monopoly capacity; Example 8.15, the symmetric Cournot equilibrium and its price; Theorem 8.5 (i)-(ii), the pure-strategy Bertrand–Edgeworth equilibria; and the advance-purchase comparison of Sect. 8.3.6, $w_2 < \hat w$ and $V_{APD}(\hat w) \ge V_{peak}(w_2)$.

Not targets: Theorems 8.1-8.2 (the Coase problem, subgame-perfect equilibria of an infinite-horizon game, proofs in von der Fehr and Kühn), Theorem 8.3 (Harris–Raviv priority pricing, stated with a garbled price formula), Theorem 8.4 (existence via quasiconcavity, cited), Theorem 8.5 (iii), 8.6 and 8.7-8.8 (mixed-strategy and supergame equilibria of Kreps and Scheinkman and Benoit and Krishna), Proposition 8.2 and Proposition 8.4 (the dynamic offer-set game under condition (8.32), proved in Talluri's paper), and the Kreps–Scheinkman derivation of Sect. 8.4.1.6, which rests on Theorem 8.6.

Significance

The equilibrium graph is the chapter's own contribution: a bipartite picture of best responses on chains in which monotonicity, the absence of crossing arcs, forces an equilibrium. It is the finite, combinatorial form of the monotone comparative-statics route to Nash equilibrium (Tarski's fixed point on a chain), and it is what makes RM allocation games tractable: the two-class duopoly with Littlewood responses always has an equilibrium, and the offer-set duopoly does whenever the two firms face the same sign of $g$, while Example 8.18 shows a best-response cycle when they do not. The Bertrand–Edgeworth, Cournot and newsvendor results are the benchmarks the book uses to interpret RM competition: capacity constraints soften Bertrand's zero-profit outcome, competing in allocations tends to raise total capacity above the monopoly level, and advance-purchase discounts dominate peak-load pricing as a self-selection mechanism. None of these has a machine-checked proof.

Difficulty

The lemma and the goal are fixed-point arguments on finite chains: the largest best response is a monotone map of the rival's index, the composition of two monotone (or two antitone) maps on a finite chain has a fixed point, and for the offer-set game the monotonicity itself must be extracted from the ratio structure $g(C_k)/(W(k) + a)$ as in the appendix's inequalities (8.A.3)-(8.A.5), separately in the two cases. Proposition 8.1 is a monotonicity of tail probabilities under the pointwise order of effective demands. Example 8.16 is a short probabilistic argument that needs the identity $\{D > x_1 + x_2\} = \{R_1 > x_1\} \cap \{R_2 > x_2\}$ and the strict monotonicity of the tail. Theorem 8.5 requires computing efficient-rationing sales for every unilateral deviation from a symmetric profile, through the recursive definition of residual demand, and a quadratic inequality for upward deviations in part (ii). The advance-purchase item reduces to the identity $V_{APD}(w) - V_{peak}(w) = (1 - \alpha)w$ and the strict decrease of the first-order-condition function.

Formalization scope

Products, protection levels and complete sets are natural numbers; the offer-set game's strategies are the complete sets $C_1, \dots, C_n$ of the book, and its payoff is (8.31) up to the positive factor $\lambda$ and the terms independent of both offer sets. Prices decreasing in the product index are a hypothesis, as the nested-by-revenue order of Sect. 8.4.3.2. The RM duopoly is modeled through Littlewood's response, as the book's appendix argues, rather than through expected revenues. Efficient rationing is defined recursively over the firms priced strictly below a given firm, with equal sharing among firms at the same price. Example 8.16 is stated with the equilibrium conditions (8.23) and the strictly increasing distribution of aggregate demand as hypotheses. The advance-purchase item takes the first-order conditions (8.13) and (8.15) and the book's uniqueness assumption as hypotheses, the latter as $(v - w) - F(w)/f(w)$ strictly decreasing in $w$ (the page prints "increasing", but its footnote identifies it with the monotone marginal-revenue assumption, which is decreasing in the waiting cost). Theorem 8.5 is stated for its pure-strategy parts (i) and (ii) only.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 8. https://doi.org/10.1007/b139000
• D. M. Kreps and J. A. Scheinkman, Quantity precommitment and Bertrand competition yield Cournot outcomes, Bell Journal of Economics 14(2), 1983. https://doi.org/10.2307/3003636
• S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.54
• S. Netessine and R. A. Shumsky, Revenue management games: horizontal and vertical competition, Management Science 51(5), 2005. https://doi.org/10.1287/mnsc.1040.0356
• I. L. Gale and T. J. Holmes, Advance-purchase discounts and monopoly allocation of capacity, American Economic Review 83(1), 1993. https://www.jstor.org/stable/2117500
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Many vehicles, one depot

The vehicle routing problem asks for the cheapest set of delivery routes from a depot to a set of customers when each vehicle can carry only so much. It generalizes the traveling salesman problem, which is the case of a single vehicle of unlimited capacity, and it is the operational problem behind every distribution fleet. Exact methods reach a few hundred customers; the questions that shape fleet design are structural: how does the optimal routing cost compare with the cost of a single grand tour, and how does it grow with the number of customers? Haimovich and Rinnooy Kan (1985) answered both for unit demands by bounding the optimal cost above and below in terms of the optimal TSP tour and the average distance to the depot. Chapter 11 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents that result with its full proof as Theorem 11.6, and it is the goal of this mission.

Setting

Nodes are the depot $0$ and customers $1, \dots, n$, with distances $c_{ij}$ that are symmetric, nonnegative and satisfy the triangle inequality (VRPMetric). Every customer has demand $1$ and every vehicle capacity $C$, so a route is a sequence of at most $C$ distinct customers, served by one vehicle that leaves the depot, visits them in order and returns; its length is routeCost c L. A solution is a family of routes visiting every customer exactly once (IsVRPSolution), with total length solutionCost; the number of routes is free. The optimal VRP value $z^*$ (vrpOpt c C) is the least total length, the optimal TSP value $z_T$ (tspOpt c) is the least length of a single route through all customers, and $\bar c$ (avgDepotDist) is the average distance from the depot to a customer.

Formalization targets

Goal: Theorem 11.6

For every metric instance with $n \ge 1$ customers and capacity $C \ge 1$,

$$\max\Big\{2\frac{n}{C}\bar c,\ z_T\Big\} \;\le\; z^* \;\le\; 2\Big\lceil\frac{n}{C}\Big\rceil\bar c + \Big(1 - \frac{1}{C}\Big)z_T.$$

This is vrp_tsp_bounds.

Supporting targets

The three steps of the book's proof: the radial bound $2\frac{n}{C}\bar c \le z^*$, obtained route by route from the triangle inequality and the capacity; the routing bound $z_T \le z^*$; and the iterated optimal tour partition bound (11.59), that for any tour $\Gamma$ through all customers some partition of its customer sequence into $\lceil n/C\rceil$ consecutive routes costs at most $2\lceil n/C\rceil\bar c + (1 - \lceil n/C\rceil/n)\,z(\Gamma)$.

The chapter's other numbered results are not targets: Proposition 11.1 (state-space relaxation of the routing dynamic program) and Theorem 11.2 (the capacitated comb inequality, proof omitted, which needs the bin-packing function $v(S)$), and Theorems 11.3, 11.5, 11.7 and Lemma 11.4 (almost-sure asymptotics of random instances and the location-based heuristic), whose proofs the book cites.

Significance

Theorem 11.6 is the quantitative link between routing and the two things a planner can estimate without solving anything: the TSP length, which grows like $\sqrt{n}$ for random customers, and the average depot distance. It says that the VRP cost is the TSP cost plus a radial term $2\bar c$ per vehicle, and that this decomposition is exact up to a factor bounded by the capacity. The radial term explains Theorem 11.7, that the optimal cost grows linearly in $n$ for fixed capacity, and the tour partition heuristic in the proof is a practical route-first-cluster-second method with a provable guarantee. The bounds are the basis of the continuous approximation formulas used in strategic distribution design.

None of these results has a machine-checked proof. The book proves Theorem 11.6 in full. The formal treatment of routes as lists and of the averaging argument over rotations of a tour is reusable for the capacitated heuristics of Sect. 11.3.

Difficulty

The upper bound is an averaging argument that is easy to state and fiddly to formalize: for each of the $n$ rotations of the tour's customer sequence, the sequence is cut into blocks of $C$, and one must count, across all rotations, how often each customer is the first or last of a block and how often each tour edge is cut. The counts, $\ell = \lceil n/C\rceil$ each, hold only after the rotations are indexed carefully, and the passage from the average to the best rotation needs the sum of the $n$ solution costs computed exactly.

The lower bound has two parts with different flavors. The radial part needs, for each route, that the closed route from the depot is at least twice the largest depot distance among its customers, which is the triangle inequality applied along the route, followed by an averaging step that uses the capacity. The routing part is a shortcutting argument: the routes of a solution concatenate into a closed walk that revisits the depot, and removing the repeated depot visits must not increase the length. The obvious idea, that a VRP solution is itself a tour, is false, and the shortcut has to be constructed.

Formalization scope

Routes are lists of customers, solutions are lists of routes, and the feasibility predicate requires nonempty routes of length at most $C$ avoiding the depot, with the concatenation of all routes a duplicate-free list containing every customer. Costs use the closed walk through the depot followed by the route. The optimal values are infima of finite nonempty sets of reals, nonempty because singleton routes are feasible when $C \ge 1$. The ceiling $\lceil n/C\rceil$ is Mathlib's Nat.ceil of the real quotient. The number of vehicles is unrestricted, as the section assumes; the fixed-fleet version of the problem is not modeled.

The TSP value $z_T$ is defined as the least route cost over all orderings of the customers, so no separate tour model is needed and the mission does not depend on the TSP mission of this series.

The definition module is shared by all five items. Problem 11.18 (tightness of both bounds) and Theorem 11.7 for deterministic instance families are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 11. https://doi.org/10.1002/9781119584445
• M. Haimovich and A. H. G. Rinnooy Kan, Bounds and heuristics for capacitated routing problems, Mathematics of Operations Research 10(4), 1985. https://doi.org/10.1287/moor.10.4.527
• P. Toth and D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014. https://doi.org/10.1137/1.9781611973594

The problem every routing model contains

A salesman must visit $n$ cities and return home by the shortest route. The traveling salesman problem is the prototype of combinatorial optimization: easy to state, NP-hard (Karp 1972), and solved to optimality on instances with tens of thousands of nodes by branch-and-cut. In a supply chain it is the core of every vehicle routing model and of the location-routing models of the chapters that follow. Chapter 10 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) covers the symmetric metric TSP, in which distances satisfy the triangle inequality: the cutting planes of branch-and-cut (comb inequalities), the construction heuristics with their worst-case guarantees, culminating in Christofides' (1976) 3/2-approximation, and the lower bounds of Little et al. and of Held and Karp (1970). This mission formalizes those results, with Christofides' theorem as its goal.

Setting

Nodes are $N = \{1, \dots, n\}$ with distances $c_{ij}$ that are symmetric, nonnegative, zero on the diagonal and satisfy the triangle inequality $c_{ij} \le c_{ik} + c_{kj}$ (IsMetric). A tour is a visiting order $\tau$ of all the nodes, of length $z(\tau) = \sum_k c(\tau_k, \tau_{k+1})$ with indices mod $n$ (tourLength); $z^*$ is the least tour length (optTourLength). A tour has an edge set (tourEdges), and for a node set $S$ the counts of tour edges inside $S$ and leaving $S$ (edgesWithin, edgesLeaving) are the sums $\sum_{i,j \in S} x_{ij}$ and $\sum_{i \in S, j \notin S} x_{ij}$ of the integer programming formulation. A comb is a handle $H$ with an odd number $s \ge 3$ of pairwise disjoint teeth, each meeting both $H$ and its complement (IsComb); when every tooth has exactly two nodes the comb is a 2-matching configuration.

The nearest neighbor heuristic always moves to a nearest unvisited node (IsNearestNeighborTour); the nearest insertion heuristic grows a partial tour by inserting the unvisited node nearest to it at the cheapest position (IsNearestInsertionRun, with cycleLength and distToTour). The minimum spanning tree heuristic doubles an MST (IsMST, graphWeight), takes an Eulerian tour of the doubled tree and shortcuts it, visiting the nodes in order of first appearance (IsShortcut). Christofides' heuristic instead adds to the MST a minimum-weight perfect matching on its odd-degree nodes (oddNodes, IsMinMatchingOn) before taking the Eulerian tour. A 1-tree rooted at $r$ is a spanning tree on the other nodes plus two edges at $r$ (Is1Tree); the revised distances $c'_{ij} = c_{ij} + \lambda_i + \lambda_j$ (revisedCost) define the Held-Karp bound.

Formalization targets

Goal: Theorem 10.13

For every metric instance, every minimum spanning tree $T^*$, every minimum-weight perfect matching $M$ on the odd-degree nodes of $T^*$, every Eulerian tour of $T^* + M$ and its shortcut $\tau$,

$$z(\tau) \;\le\; \tfrac{3}{2}\, z^*.$$

This is christofides_bound.

Supporting targets

Theorem 10.1, the reduced-matrix bound $\sum_i \rho_i + \sum_j \kappa_j \le z^*$; Theorem 10.2, Proposition 10.3 and Theorem 10.4, the 2-matching and comb inequalities valid for every tour; Theorem 10.6, $z_{NN} \le \frac{1}{2}(\lceil\log_2 n\rceil + 1) z^*$; Theorem 10.7, $z_{NI} \le 2z^*$; Lemma 10.9, $z(T^*) \le z^*$; Theorem 10.10, Euler's theorem; Theorem 10.11, $z_{MST} \le 2z^*$; Lemma 10.12, the handshaking lemma; Lemma 10.15, the 1-tree bound; Lemma 10.16, the revised distance identities; Theorem 10.17, the Held-Karp bound. Theorem 10.5 (no constant-factor approximation unless P = NP), Theorem 10.8 and the second part of Theorem 10.6 (tightness instances), Lemma 10.14 (Euclidean tours do not cross), Lemma 10.18 (the integrality gap) and Theorem 10.19 (the Beardwood-Halton-Hammersley asymptotics) are not targets.

Significance

Christofides' bound was the best approximation guarantee for the metric TSP for over forty years, until the $3/2 - 10^{-36}$ of Karlin, Klein and Oveis Gharan (2021), and it is the reference point against which every heuristic in the chapter is measured: nearest neighbor has no constant bound, nearest insertion and the MST heuristic achieve $2$, Christofides $3/2$. The comb inequalities are the cuts that make branch-and-cut work, and the Held-Karp bound is the lower bound that tells a practitioner how far a heuristic tour is from optimal. Theorem 10.1 is the historical bounding rule of the first branch-and-bound algorithm.

None of these results has a machine-checked proof. The book proves Theorems 10.2, 10.11, 10.13 and 10.17 and Proposition 10.3 and Lemma 10.9, cites Theorems 10.6, 10.7 and 10.10, and leaves Theorem 10.4 and Lemmas 10.12 and 10.16 as exercises. The formal infrastructure for tours, shortcutting and Eulerian walks is reusable for the vehicle routing chapter.

Difficulty

Christofides' argument has three steps and each has a formal obstacle. The MST bound is a spanning-path argument that needs the removal of an edge from a tour to yield a tree, in Mathlib's terms a connected acyclic subgraph of the complete graph. The matching bound is the subtle one: the optimal tour shortcut to the odd-degree nodes, of length at most $z^*$ by the triangle inequality, is an even cycle whose alternate edges form two perfect matchings on those nodes, the cheaper of which costs at most $z^*/2$; formalizing the decomposition of a cycle on an even node set into two matchings, and the shortcut's length bound, is the bulk of the work. The final step, that shortcutting an Eulerian walk does not lengthen it, is an induction along the walk using the triangle inequality on the skipped stretches, and it needs the first-occurrence order to be handled explicitly.

The obvious approach to the heuristic bounds, comparing the heuristic tour directly with the optimal tour, fails; every proof goes through a spanning tree. For nearest insertion the tree is Prim's, grown in the same order as the insertions, and the bound charges each insertion cost to a tree edge; for nearest neighbor the argument of Rosenkrantz et al. bounds the sum of the $k$ largest steps by $2z^*$ for each $k$ and sums a geometric series, which is where the logarithm comes from.

The comb inequalities are counting arguments on degrees, but the general comb of Theorem 10.4 needs the case analysis of how a tour enters and leaves each tooth. Euler's theorem in the sufficiency direction is Hierholzer's construction, which is not in Mathlib.

Formalization scope

Tours are permutations of Fin n, so a tour is an ordering rather than an edge set, and every tie-breaking of a heuristic is covered by a predicate on its output rather than by an algorithm. Graphs are Mathlib SimpleGraphs on Fin n; the multigraphs of the two tree heuristics are represented by closed walks with prescribed edge multisets, and shortcutting is the first-occurrence order along the walk's node sequence. All degree and edge-set computations use classical decidability. Theorems on tours assume $n \ge 3$ where a tour must have distinct edges, $n \ge 1$ otherwise.

Theorem 10.1 is stated for the reduction of the full off-diagonal matrix, because the book's upper-triangular version is false: a random metric instance violates it, since the last row and first column of a triangular matrix are empty and the two edges at a node need not be one row and one column entry. The full-matrix version is the statement of Little et al. It is stated for $n \ge 2$, because a one-node "tour" is a self-loop that no off-diagonal entry constrains.

Theorem 10.4 is stated with the comb inequality's right-hand side corrected to $|H| + \sum_k(|T_k| - 1) - \tfrac{1}{2}(s+1)$, the standard form. The book prints $+\tfrac{1}{2}(s-1)$, which contradicts its own 2-matching special case (10.15) and is weaker by $s$. The corrected statement implies the printed one.

The $1$-tree root is an explicit node $r$, the book's node $1$. The nearest insertion run is a sequence of lists indexed by iteration, and the theorem compares the $n$-th list's closed length with $z^*$; a run always exists, so the hypothesis is satisfiable.

The definition module is shared by all fifteen items. Theorem 10.8 and Problem 10.12 (tightness of the bounds of $2$), the second part of Theorem 10.6, and Lemma 10.18 on the integrality gap are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 10. https://doi.org/10.1002/9781119584445
• N. Christofides, Worst-case analysis of a new heuristic for the travelling salesman problem, Report 388, GSIA, Carnegie Mellon University, 1976; reprinted in Operations Research Forum 3, 2022. https://doi.org/10.1007/s43069-021-00101-z
• D. J. Rosenkrantz, R. E. Stearns and P. M. Lewis II, An analysis of several heuristics for the traveling salesman problem, SIAM Journal on Computing 6(3), 1977. https://doi.org/10.1137/0206041
• M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18(6), 1970. https://doi.org/10.1287/opre.18.6.1138
• J. D. C. Little, K. G. Murty, D. W. Sweeney and C. Karel, An algorithm for the traveling salesman problem, Operations Research 11(6), 1963. https://doi.org/10.1287/opre.11.6.972
• M. Grötschel and M. W. Padberg, On the symmetric travelling salesman problem I and II, Mathematical Programming 16, 1979. https://doi.org/10.1007/BF01582116

Prices that respond to inventory

A retailer marking down a seasonal line, an airline raising fares as seats sell, a manufacturer pricing while restocking: each sets prices over time against a finite and changing inventory. Chapter 5 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) collects the structural theory of that problem. Without replenishment, the Bernoulli-arrival model of Gallego and van Ryzin (1994) gives a marginal value of capacity that falls with inventory and with time, hence prices that jump up at each sale and drift down between sales, and the deterministic fluid model bounds it from above. With replenishment, the model of Federgruen and Heching (1999) has a jointly concave and supermodular continuation value, from which the base-stock, posted-price policy follows: below a base-stock level order up to it and post a fixed price, above it order nothing and discount, more the higher the inventory. This mission formalizes those results with Proposition 5.3 as the goal.

Setting

Bernoulli demand (Sect. 5.2.2.2). One customer arrives per period with a random willingness to pay; the firm's decision is the demand rate $d \in [0, 1]$, the probability of a sale at the inverse-demand price $p(t, d)$, with revenue rate $r(t, d) = d\,p(t, d)$ (revenueRate). The value function (5.12) is $V_t(x) = \max_{d}\{r(t, d) - d\,\Delta V_{t+1}(x)\} + V_{t+1}(x)$, $V_{T+1} = 0$, $V_t(0) = 0$ (bernoulliValue), and $\Delta V_t(x) = V_t(x) - V_t(x-1)$ (bernoulliDelta). The deterministic model (5.1) maximizes $\sum_t r(t, d(t))$ over rates with $\sum_t d(t) \le C$ (deterministicValue).

Pricing with replenishment (Sect. 5.3.2). Inventory may be negative (backorders). In period $t$ with inventory $x$ the firm orders up to $y \ge x$ at unit cost $c_t$, chooses a rate $d \in [0, \bar d]$, sells the random demand $D(t, d, \xi_t) = a_t(\xi_t)\,d + b_t(\xi_t)$ (additive, multiplicative or mixed noise), and pays the convex cost $h_t$ on ending inventory. The value function (5.20) is $V_t(x) = \sup_{y \ge x,\, d}\{r(t, d) - c_t(y - x) + G_{t+1}(y, d)\}$ with the continuation value $G_{t+1}(y, d) = \mathbb E[V_{t+1}(y - D(t, d, \xi_t)) - h_t(y - D(t, d, \xi_t))]$ (ReplPricing.value, contValue). Assumption 7.2, marginal revenue decreasing, is the concavity of $r(t, \cdot)$.

Formalization targets

Goal: Proposition 5.3

For every period, $G_{t+1}$ is jointly concave on $\mathbb R \times [0, \bar d]$, $V_t$ is concave on $\mathbb R$, and $G_{t+1}$ has increasing differences in $(y, d)$, the supermodularity that the book states through its partial derivatives: replenishment_concave_supermodular.

Supporting targets

Proposition 5.2, the marginal value of capacity in the Bernoulli model decreases in $t$ and in $x$; the upper bound of Sect. 5.2.2.3, the optimal deterministic revenue dominates the optimal expected stochastic revenue; and the base-stock, posted-price structure of Sect. 5.3.2.1, derived from Proposition 5.3: below the unconstrained optimum $y^0$ order up to it and use $d^0$, above it order nothing and use a rate at least $d^0$ that is nondecreasing in the inventory.

Proposition 5.1 and Lemma 5-5.A.1 (the continuous-demand model without replenishment) are not targets; see the formalization scope. The deterministic sections (efficient prices, discrete price sets), the asymptotic optimality of the deterministic heuristic, the infinite-horizon stationary problem and the multiproduct and finite-population models carry no numbered results.

Significance

Proposition 5.3 is the structural core of joint pricing and inventory control: joint concavity makes the period problem a concave program, and supermodularity is what turns its solution into a policy, the base-stock, posted-price rule that Federgruen and Heching showed optimal and that later work on pricing with inventory builds on. Proposition 5.2 is the reason optimal dynamic prices in the stochastic single-item model rise at every sale and fall while inventory sits, the behaviour of Figure 5.5, and the deterministic upper bound is what justifies the fluid model as a benchmark and a heuristic, the pattern quantified in Table 5.6. None of these has a machine-checked proof; the replenishment result in particular needs the interplay of concavity, expectation and partial maximization on all of $\mathbb R$.

Difficulty

Proposition 5.2 is an induction whose step compares suprema over the rate interval, with the boundary condition $V_t(0) = 0$ breaking the recursion at $x = 1$ and requiring $r(t, 0) = 0$. The deterministic bound is an induction on periods that uses the concavity of the deterministic value in the inventory (a concave program's value) to absorb the two branches of the Bernoulli recursion. The goal needs: integrability and continuity of $V_{t+1}(y - D) - h_t(y - D)$ under bounded noise; that the expectation of a concave function of an affine map is jointly concave, and its increasing differences from those of the concave integrand; that a partial supremum of a jointly concave function over the convex feasible set $\{y \ge x\}$ is concave in $x$; and the boundedness of the objective so that every supremum is a real number. The base-stock item is the segment argument that moves an unconstrained maximizer onto the boundary $y = x$ and a monotone comparative-statics argument on the supermodular objective, with maxima attained by continuity on the compact rate interval.

Formalization scope

Periods are natural numbers with value t the value with $T + 1 - t$ periods to go, the maxima are suprema, and the book's ranges are hypotheses. The demand is affine in the rate, which is the additive and multiplicative models the book names; with a merely convex demand (Assumption 5.1) the joint concavity of Proposition 5.3 fails when $V_{t+1} - h_t$ is not monotone, and the noise has bounded support, strengthening Assumption 7.6. The partial-derivative statements (iii)-(iv) are in difference form. Proposition 5.1 is not formalized: its model (5.11) evaluates $V_{t+1}(x - D)$ at negative inventories the model does not define while truncating revenue at $x$, and its Lemma 5-5.A.1 (joint concavity of $r^+$) is false as stated, its Hessian argument mistaking an indefinite matrix for a negative definite one; a counterexample is in the mission's check. The deterministic model restricts rates to $[0, 1]$, the rates the Bernoulli model can realize.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 5. https://doi.org/10.1007/b139000
• G. Gallego and G. J. van Ryzin, Optimal dynamic pricing of inventories with stochastic demand over finite horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
• A. Federgruen and A. Heching, Combined pricing and inventory control under uncertainty, Operations Research 47(3), 1999. https://doi.org/10.1287/opre.47.3.454
• W. Elmaghraby and P. Keskinocak, Dynamic pricing in the presence of inventory considerations, Management Science 49(10), 2003. https://doi.org/10.1287/mnsc.49.10.1287.17315
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

When the supplier is the risk

Every model in the earlier chapters of this series treats demand as the uncertain quantity and supply as given. Chapter 9 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reverses the roles: demand is deterministic and the supplier fails. A disruption is a binary event, modeled as a two-state Markov process between up and down periods, during which nothing can be ordered. The chapter's thesis, from Snyder and Shen (2006), is that supply uncertainty is a mirror image of demand uncertainty: the optimal base-stock level has the same critical-fractile form as the newsvendor solution but with the fractile taken over the disruption-length distribution (Tomlin 2006), and consolidation, which pools demand risk, now does nothing to expected cost and multiplies its variance, the risk-diversification effect of Schmitt, Sun, Snyder and Shen (2015). The chapter closes with the reliable fixed-charge location problem of Snyder and Daskin (2005). This mission formalizes the chapter's theorems on disruptions, with the risk-diversification theorem as its goal.

Setting

A supplier that is up is disrupted next period with probability $\alpha$; one that is down recovers with probability $\beta$. The disruption chain records $0$ when the supplier is up and $n \ge 1$ in the $n$-th consecutive period of a disruption; its stationary distribution is $\pi_0 = \beta/(\alpha+\beta)$ and $\pi_n = \frac{\alpha\beta}{\alpha+\beta}(1-\beta)^{n-1}$ (disruptionPmf), with distribution function $F(n) = \sum_{i \le n}\pi_i$ (disruptionCdf).

A single location faces demand $d$ per period, pays $h$ per unit held and $p$ per unit backordered per period, and follows a base-stock policy: it orders up to $S$ in every up period and nothing in down periods. In the $n$-th period of a disruption it has $S - (n+1)d$ units on hand or backordered, so its cost is $\hat g(S, n) = h[S-(n+1)d]^+ + p[(n+1)d - S]^+$ (periodCost), and the expected cost per period is $g(S) = \sum_n \pi_n \hat g(S, n)$ (meanCost), with variance $V(S)$ over the disruption state (varCost). The critical fractile $\gamma = p/(p+h)$ and $F^{-1}(\gamma)$, the smallest $n$ with $F(n) \ge \gamma$, determine the optimal level.

In the reliable fixed-charge location problem (RFLP), sites fail independently with probability $q$ and each customer is assigned to a chain of facilities: its level-$r$ facility serves it when the $r$ closer facilities are disrupted, until it is assigned to an emergency facility $u$ that never fails and charges the penalty $\theta_i$. The objective (9.61) is fixed cost plus expected transportation cost, with coefficients $\psi_{ijr} = h_i c_{ij} q^r (1-q)$ (rflpPsi, rflpCost) under the constraints (9.62)-(9.67) (RFLPFeasible).

Formalization targets

Goal: Theorem 9.9

For $N$ identical locations and the centralized location formed by merging them (demand $Nd$):

$$S^*_C = NS^*, \qquad g^*_C = g^*_D = Ng^*, \qquad V^*_C = N V^*_D = N^2 V^*,$$

that is, an optimal single-location level $S$ scales to the optimal centralized level $NS$, the centralized expected cost at $NS$ is $N$ times the single-location cost, and its variance is $N^2$ times the single-location variance. This is risk_diversification.

Supporting targets

Lemma 9.2, the stationary distribution and distribution function of the disruption chain; Lemma 9.4, that the optimal base-stock level is a multiple of $d$; Theorem 9.5, $S^* = d + dF^{-1}(p/(p+h))$, as the least minimizer of $g$; and Theorem 9.10, that in every optimal RFLP solution consecutive backup assignments are ordered by cost. Theorem 9.3, the optimality of base-stock policies, is cited by the book to Song and Zipkin without a model of the policy space and is not a target; Proposition 9.1 and the multisupplier results of Sect. 9.4 are left for a later mission, as discussed below.

Significance

Theorem 9.5 is the supply-side newsvendor formula: it says exactly how much inventory buys protection against disruptions of a given length, and it underlies the disruption models used in practice for raw-material buffers. Theorem 9.9 is the chapter's central insight and the reason supply and demand uncertainty call for opposite strategies: pooling reduces expected cost under demand uncertainty but only redistributes risk under supply uncertainty, concentrating it. Its three identities are what a risk-averse planner needs to compare the two designs by a mean-variance criterion. Theorem 9.10 is what lets the RFLP be formulated without ordering constraints and solved by Lagrangian relaxation like the UFLP.

None of these results has a machine-checked proof. The book proves Theorem 9.5 and the identities behind Theorem 9.9, sketches Lemma 9.4, and leaves Lemma 9.2 and Theorem 9.10 as exercises. The formal treatment of the piecewise-linear cost $g$ and its finite differences is reusable for the yield-uncertainty and multi-supplier models of the same chapter.

Difficulty

The cost $g$ is an infinite series whose terms grow linearly in $n$ against a geometric weight, so every statement about it begins with summability, and the finite-difference identity $\Delta g(S) = d[(h+p)F(S/d - 1) - p]$ requires exchanging a difference with a sum. Theorem 9.5 then needs the convexity and piecewise linearity of $g$ to pass from a sign condition on slopes at multiples of $d$ to a global minimum over all real $S$, and the identification of the least minimizer needs the slopes to be strictly negative below $S^*$. The obvious idea, treating the problem as a discrete newsvendor over multiples of $d$, is only half of the argument: it does not by itself exclude non-multiple minimizers, which is what Lemma 9.4 asserts.

Lemma 9.2 is elementary but the stationary equations involve a series over all down states, and the proof must establish summability before manipulating it. Theorem 9.9's scaling identities are termwise, but the optimality transfer in part 1 requires the scaling to preserve minimizers, which follows from the cost identity holding for every $S$.

Theorem 9.10 is an exchange argument on a binary program with layered constraints. The delicate case is the emergency facility: swapping it into a lower level is infeasible, and the correct move is to promote it and drop the later assignment, which changes the constraints for every higher level; the argument must show feasibility of the modified solution level by level.

Formalization scope

The disruption distribution is given by Lemma 9.2's formula rather than defined as the stationary distribution, and Lemma 9.2 shows it satisfies the stationary equations; the theorems assume $0 < \alpha \le 1$ and $0 < \beta \le 1$, under which every series is a geometric series times a polynomial and is summable. The quantity $F^{-1}(\gamma)$ enters Theorem 9.5 as a natural number $k$ characterized by $F(k) \ge \gamma$ and $F(n) < \gamma$ for $n < k$, which exists since $F(n) \to 1 > \gamma$; the conclusion asserts both optimality and leastness of $d + dk$ among all real levels.

Theorem 9.9 is stated as the scaling of the single-location functions; the decentralized totals $Ng^*$ and $NV^*$ are the mean and variance of a sum of $N$ independent copies, which the book asserts rather than derives, and are not modeled separately. In the RFLP, levels are indexed by Fin m, the emergency facility is a designated index $u$ whose data satisfy the book's conventions through the hypotheses, and demands are positive with $0 < q < 1$, both needed: with $q = 0$ or $h_i = 0$ backup assignments are free and any order is optimal.

The EOQ with disruptions (Proposition 9.1) is a renewal-reward derivation without a formal model of the renewal process in the book, and the multisupplier newsvendor of Sect. 9.4 (Lemma 9.6, Theorems 9.7 and 9.8) rests on differentiability conditions the book defers to Dada et al. and on a lemma it leaves as an exercise; both are natural extensions on the same definitions rather than targets here.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 9. https://doi.org/10.1002/9781119584445
• B. Tomlin, On the value of mitigation and contingency strategies for managing supply chain disruption risks, Management Science 52(5), 2006. https://doi.org/10.1287/mnsc.1060.0515
• A. J. Schmitt, S. A. Sun, L. V. Snyder and Z.-J. M. Shen, Centralization versus decentralization: risk pooling, risk diversification, and supply chain disruptions, Omega 52, 2015. https://doi.org/10.1016/j.omega.2014.10.010
• L. V. Snyder and M. S. Daskin, Reliability models for facility location: the expected failure cost case, Transportation Science 39(3), 2005. https://doi.org/10.1287/trsc.1040.0107
• L. V. Snyder and Z.-J. M. Shen, Supply and demand uncertainty in multi-echelon supply chains, working paper, 2006. https://doi.org/10.1287/msom.1080.0224