Optimization

Motivation

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

Setting

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

Formalization targets

Goal: Theorem 23.2

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

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

Milestones

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

Significance

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

Goal: Theorem 22.4

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

Milestones

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Setting

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

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

Formalization targets

Goal: Theorem 6.4

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Chapter 5 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), presents the achievable region methodology of Tsoucas, Bertsimas and Niño-Mora, Glazebrook and Garbe, and Dacre, Glazebrook and Niño-Mora: instead of arguing about policies, one argues about the set of performance vectors they can produce. For a multi-armed bandit the natural performance of a policy is the vector of discounted numbers of times each state is continued; the expected return is linear in it; and the set of achievable performances turns out to be a polytope cut out by conservation laws, one inequality per subset of states, with equality exactly for the priority policies that put that subset last. Optimizing a linear objective over a polytope is a linear program, its dual is solved by an adaptive greedy algorithm, and the primal solution is the performance of a priority policy whose priorities are the algorithm's outputs, the Gittins indices. This gives yet another proof of the index theorem (Section 5.3) and, more importantly, a definition, generalized conservation laws (Section 5.4), of the class of systems for which the same argument works: branching bandits, multi-class queues, job scheduling with discounted rewards, systems with imposed priority classes. The chapter's main result, Theorem 5.5, is the statement that every such system is solved by an index policy.

Setting

There are $N$ job types $E = \{1, \dots, N\}$. A policy $\pi$ has a performance $x^\pi \in \mathbb{R}^N_+$, a vector of expectations; a permutation $\sigma$ of $E$ defines the permutation policy giving $\sigma_N$ highest and $\sigma_1$ lowest priority, and $S_k = \{\sigma_1, \dots, \sigma_k\}$ is the set of the $k$ lowest-priority types. The system satisfies GCL(1) if there are a base function $b : 2^E \to \mathbb{R}_+$ and a matrix $A = (A_i^S)$, positive on $S$ and zero off it, such that for every policy

$$\sum_{i \in S} A_i^S x_i^\pi \ge b(S) \quad (S \subseteq E), \qquad \sum_{i \in E} A_i^E x_i^\pi = b(E),$$

with equality in the first for every permutation policy whose $|S|$ lowest-priority types are $S$. GCL(2) reverses the inequality. The adaptive greedy algorithm $AG(A, r)$ picks $i_N$ maximizing $r_i/A_i^E$, sets $\bar y_E$ to the maximum, removes $i_N$, and repeats with the adjusted rewards $r_i - \sum_{j \ge k} A_i^{S_j}\bar y_{S_j}$ divided by $A_i^{S_{k-1}}$; its outputs are the order $i_1, \dots, i_N$, the dual variables $\bar y_{S_k}$ and the indices $\nu_{i_k} = \sum_{j \ge k} \bar y_{S_j}$.

For the SFABP of Section 5.3, $n$ identical bandit processes on $E$ with kernel $P$ and discount factor $a$ in the model of the Bandit Algorithms series, $x_i^\pi = \mathbb{E}^\pi \sum_t a^t I_i(t)$ is the discounted number of continuations of a bandit in state $i$, $A_i^S = \mathbb{E}[1 + a + \cdots + a^{T_i^S - 1}]$ is the discounted return time to $S$ from $i \in S$, and $b(S)$ is the minimal cost $\sum_{i \in S} A_i^S x_i^\pi$, namely $(1-a)^{-1}\mathbb{E}[a^\tau]$ with $\tau$ the number of continuations needed to bring every bandit into $S$.

Formalization targets

Goal: Theorem 5.5

For a GCL(1) system whose achievable region is convex, and any reward vector $r$: the achievable region is the polytope

$$P(A, b) = \Big\{x \in \mathbb{R}_+^N : \sum_{i \in S} A_i^S x_i \ge b(S),\ S \subset E,\ \sum_{i \in E} A_i^E x_i = b(E)\Big\};$$

its extreme points are performances of permutation policies; $AG(A, r)$ has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes $\sum_i r_i x_i^\pi$ over all policies.

Milestones

Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside $S$); the identification on p. 123 of the adaptive greedy indices of a SFABP with the Gittins indices, together with their monotonicity along the order found; Theorem 5.10, the GCL(2) counterpart of the goal for cost minimization.

Significance

Theorem 5.5 is the index theorem in its most general form of this kind: it says nothing about Markov chains, only that performances are expectations, objectives are linear and conservation laws hold, and it delivers both the optimal policy and the algorithm that computes its priorities in polynomial time in the number of job types. It is the theorem behind the index results for branching bandits and Klimov's multi-class queue and behind the suboptimality bounds of Sections 5.5 and 5.7, all of which are calculations on the polytope. Lemma 5.1 and the p. 123 identification are what tie the abstract theorem to the Gittins index: they show that the multi-armed bandit is a GCL(1) system and that the priorities the algorithm produces are the same indices as Chapters 2 to 4 define through stopping times.

None of these is machine-checked. Formalizing Theorem 5.5 puts an LP-duality index theorem on the platform in a form any system can instantiate by verifying its conservation laws; formalizing Lemma 5.1 relates the Bandit Algorithms run law to the single-chain return times, which is the first conservation law on that model; and the p. 123 theorem gives an algorithmic characterization of the Gittins index on finite chains, distinct from the restart and largest-remaining-index characterizations of Chapter 2.

Difficulty

The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except $\bar y_E$ and satisfy the dual constraints with equality, which is a finite induction on the stages; the extreme-point clause needs that every vertex of a polyhedron is the unique maximizer of some linear functional, and the region clause that a compact convex set is the convex hull of its extreme points (Krein–Milman in finite dimension, or the polyhedral fact directly). None of this is in Mathlib in the required form. Lemma 5.1 is probabilistic: the lower bound requires the strong Markov property of the continued bandit under an arbitrary past-measurable policy, a pathwise accounting of the discounted periods paid for by each continuation from $S$, and the observation that at most $\tau$ slots can be spent on bandits that have never been in $S$; the equality for priority policies requires that these policies use exactly those slots first and then tile the future with return excursions, and the product form of $b(S)$ requires independence of the bandits' process-time trajectories under the run law, which is built decision time by decision time rather than as a product. The p. 123 theorem is the computation (5.13) to (5.14) combined with the optimal-stopping characterization of Chapter 2 for the stop sets $\{i_1, \dots, i_{k-2}\}$, which lie between $\{\nu < \nu(i_{k-1})\}$ and $\{\nu \le \nu(i_{k-1})\}$; ties make the induction delicate, and the statement is claimed for every tie-breaking.

Formalization scope

GCL(1) and GCL(2) systems are structures over an arbitrary policy type: performance, base function, matrix, permutation policies and the three laws are fields, so the theorems are statements about finite-dimensional data and the platform's proof needs no probability. The adaptive greedy algorithm is specified relationally, as the set of its possible outputs with arbitrary tie-breaking, and the conclusion holds for each of them; existence of an output is asserted separately. The optimality clause is stated as a comparison with every policy rather than as a real supremum. The hypothesis that the achievable region is convex is explicit: the book's argument from extreme points to the whole polytope uses randomization of policies, and without it the region of a system with only its permutation policies is finite. The SFABP items use $n$ identical bandits on Fin N in the Bandit Algorithms model, the coefficients $A_i^S$ through Mission I's stoppedTime at the return time, and $b(S)$ in the product form $(1-a)^{-1}\prod_{j : k_j \notin S}\mathbb{E}[a^{T^S_{k_j}}]$, which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is $0$ when all bandits start in $S$ where the minimal cost is $1/(1-a)$. Discount factors are in $(0, 1)$ throughout.

Trivializing readings are excluded: $A_i^S > 0$ for $i \in S$ is part of the structure and of Lemma 5.1's conclusion, the polytope equations are over all subsets, and the index clause quantifies over every greedy output. Welcome contributions: the nonpositivity and dual feasibility of the greedy variables, the vertex-exposure lemma for polyhedra, and the product decomposition of the run law of identical bandits.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 5. doi:10.1002/9780470980033
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2), 1996. doi:10.1287/moor.21.2.257
• P. Tsoucas, The region of achievable performance in a model of Klimov, IBM Research Report RC16543, 1991.
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3), 1980. doi:10.1287/opre.28.3.810
• K. D. Glazebrook, R. Garbe, Almost optimal policies for stochastic systems which almost satisfy conservation laws, Annals of Operations Research 92, 1999. doi:10.1023/A:1018992306696
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Safety stock in a chain

Chapter 10 of Axsäter's Inventory Control turns to reorder points and safety stocks in multi-echelon systems, where the installations cannot be treated separately: a large stock downstream lets an upstream site run lean, and a long upstream lead-time argues for stock at the top. The best-known exact technique for serial systems is the decomposition of Clark and Scarf (1960), which the book presents in the infinite-horizon form of Federgruen and Zipkin (1984). It is also where the echelon stock measure comes from. The section's argument is short and self-contained, and its conclusion is a complete description of the optimal policy for a two-level serial system: order-up-to levels at both installations, one of them a newsboy solution, the other the minimizer of a convex function in which upstream shortages appear as an induced cost. It is the capstone of Chapter 10.

Setting

Installation 1 faces normally distributed period demand with mean $\mu$ and standard deviation $\sigma$, independent across periods, so the demand over $n$ periods, $D(n)$, is normal with mean $n\mu$ and standard deviation $\sqrt n\,\sigma$. Installation 1 replenishes from installation 2 with lead-time $L_1$ periods; installation 2 replenishes from an outside supplier with infinite supply and lead-time $L_2$. Demand that cannot be met is backordered. Costs per unit and period are echelon holding costs $e_1, e_2 \ge 0$, so the installation holding costs are $h_1 = e_1 + e_2$ and $h_2 = e_2$, and a shortage cost $b_1$ at installation 1; there are no ordering costs. Events in a period occur in the order: installation 2 orders, its delivery arrives, installation 1 orders, its delivery arrives, demand, cost evaluation.

Consider an arbitrary period $t$. After ordering, installation 2 has an echelon inventory position $y_2$, and by the standard argument its echelon stock in period $t + L_2$ is $y_2 - D(L_2)$. Installation 1 then orders, realizing an echelon position $y_1$ that cannot exceed what is available: $y_1 \le y_2 - D(L_2)$ (Eq. 10.1). Its inventory level after the demand in period $t + L_2 + L_1$ is $y_1 - D(L_1+1)$. The expected period costs are $C_2 = h_2\,\mathbb{E}(y_2 - D(L_2) - y_1)$ at installation 2 and $C_1 = h_1\,\mathbb{E}(y_1 - D(L_1+1))^{+} + b_1\,\mathbb{E}(y_1 - D(L_1+1))^{-}$ at installation 1, and the book reallocates the term $-h_2y_1$ to obtain

$$\tilde C_2(y_2) = h_2(y_2 - \mu_2'), \qquad \tilde C_1(y_1) = e_1y_1 - h_1\mu_1'' + (h_1 + b_1)\,\mathbb{E}\big(y_1 - D(L_1+1)\big)^{-},$$

with $\mu_2' = L_2\mu$ and $\mu_1'' = (L_1+1)\mu$. As a function of a free $\hat y_1$, $\tilde C_1$ is the newsboy-type function $\hat C_1$ of Eq. (10.6), minimized at the level $S_1 = \hat y_1^{*}$ given by the fractile equation (10.8). Passing everything available up to $S_1$ to installation 1, $y_1 = \min\{S_1, y_2 - D(L_2)\}$, gives the total cost $\hat C_2(y_2)$ of Eq. (10.9), whose minimizer $S_2 = y_2^{*}$ is the order-up-to level of installation 2.

Formalization targets

Goal — the decomposition

With $S_1$ from (10.8) and $S_2$ a minimizer of $\hat C_2$: for every $y_2$ and every allocation rule $a$ with $a(u) \le y_2 - u$ and finite expected cost,

$$\hat C_2(S_2) \;\le\; \mathbb{E}\big[\tilde C_2(y_2) + \tilde C_1(a(D(L_2)))\big],$$

and the order-up-to policy $(S_1, S_2)$ attains $\hat C_2(S_2)$.

Supporting targets

Eq. (10.3), the stage-1 period cost through the expected backorders; the reallocation (10.4)-(10.5), which leaves the total unchanged; the closed form (10.6) of $\hat C_1$ through the loss function $G$; the convexity of $\hat C_1$, its derivative (10.7), and the fractile characterization (10.8) of its minimizers; the pointwise rule that $\min\{S_1, y_2 - u\}$ is the cheapest feasible $y_1$; the identity (10.9); and the convexity of $\hat C_2$ (Problem 10.1) with the existence of its minimizer when $e_2 > 0$.

Significance

The result itself. The decomposition reduces a two-dimensional stochastic control problem to two one-dimensional convex problems solved in sequence, from downstream to upstream, and it identifies the optimal policy class. The downstream level $S_1$ is a newsboy solution with overage cost $e_1$, the value added, and underage cost $e_2 + b_1$, and it is independent of the upstream installation altogether; the upstream level $S_2$ sees the downstream installation only through the induced shortage cost, the last term of (10.9). The book notes the extensions the argument admits, to more echelons, to batch ordering at the top, and, via Rosling's equivalence, to assembly systems, and its Sect. 10.1.2 adapts it, now only approximately, to distribution systems under the balance assumption. Example 10.1 shows the typical outcome: the optimal average stock at the upstream installation is slightly negative.

Formalizing it. The section's mathematics is a chain of expectations under Gaussian laws and two convexity arguments. Formalizing it fixes what "optimal" means, a per-period comparison against every allocation rule, and separates the two convexity claims the book makes in one clause each. Nothing here is open; no statement has a machine-checked proof yet.

Difficulty

The pointwise allocation rule and the newsboy fractile are the same arguments as in the newsboy mission. The two places where work is needed are the identity (10.9), an expectation of a piecewise function split at $u = y_2 - S_1$, and the convexity of $\hat C_2$, which requires seeing that $x \mapsto \hat C_1(\min\{S_1, x\})$ is convex precisely because $S_1$ is a minimizer of the convex $\hat C_1$ (for any other cut-off the function is not convex), and that convexity is preserved by integrating against the law of $D(L_2)$, which needs the integrability of the linearly growing $\hat C_1$. Existence of $S_2$ then follows from the growth of $\hat C_2$ at both ends, which comes from the asymptotics of the loss function: $G(z) \to 0$ as $z \to \infty$ and $G(z) + z \to 0$ as $z \to -\infty$.

Formalization scope

$D(n)$ is csDemand mu sigma n, the Gaussian law newsboyDemand (n μ) (√n σ) from the newsboy mission, so the loss function $G$ and its closed form are reused as references. The costs are parametrized by $e_1, e_2, b_1$ with $h_1 = e_1 + e_2$ and $h_2 = e_2$ written out; $\tilde C_1$, $\tilde C_2$, the pre-reallocation period cost and $\hat C_2$ are Bochner integrals against these laws. Every statement assumes $\sigma > 0$; the goal and the convexity statements assume $e_1, e_2 \ge 0$ and $b_1 > 0$, the book's cost signs. $L_2 = 0$ is allowed and makes $D(L_2)$ a point mass, which is the setting of the book's Problem 10.2.

$S_1$ enters as any solution of the fractile equation (10.8) and $S_2$ as any minimizer of $\hat C_2$; the other items show that both exist when $e_1, e_2 > 0$. When $e_1 = 0$ the fractile is $1$, no $S_1$ exists, and the goal is vacuous, which is faithful: the book observes that then $S_1 \to \infty$ and installation 2 never carries stock. Symmetrically, when $e_2 = 0$ and $L_2 \ge 1$, $\hat C_2$ decreases towards its infimum without attaining it, so no $S_2$ exists and the goal is again vacuous: with free upstream holding the optimal $y_2$ is unbounded. Allocation rules are arbitrary functions of the realized $D(L_2)$ with an integrability hypothesis; without it Lean's integral of a non-integrable cost would be $0$ and could undercut $\hat C_2(S_2)$, which is negative in Example 10.1's stage-1 term.

What is not modelled is the infinite-horizon dynamic problem: the book's optimality claim is made period by period, and the passage to the stationary policy rests on the remark that the outside supplier has infinite supply, so the same $y_2$ can be chosen in every period. The definitions are reusable for the three-echelon extension and for the distribution system of Sect. 10.1.2; contributions formalizing Problem 10.2 ($L_2 = 0$) as a first step are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sect. 10.1.1. DOI 10.1007/978-3-319-15729-0
• Andrew J. Clark and Herbert Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4), 1960, pp. 475-490. DOI 10.1287/mnsc.6.4.475
• Awi Federgruen and Paul Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4), 1984, pp. 818-836. DOI 10.1287/opre.32.4.818
• Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4), 1989, pp. 565-579. DOI 10.1287/opre.37.4.565
• Geert-Jan van Houtum, Karl Inderfurth and Willem H. M. Zijm, Materials Coordination in Stochastic Multi-Echelon Systems, European Journal of Operational Research 95(1), 1996, pp. 1-23. DOI 10.1016/0377-2217(96)00080-8

Motivation

Every data-driven decision problem faces the same trap. A decision-maker estimates a risk functional $R(P,\ell) = \mathbb{E}_P[\ell(\xi)]$ from a nominal distribution $\hat P_N$ built from $N$ training samples, then optimizes a loss function $\ell$ against $\hat P_N$ instead of the unknown true distribution $P$. Because the optimizer adapts to the noise in $\hat P_N$, the in-sample risk of the optimizer systematically understates its true, out-of-sample risk — a phenomenon Smith and Winkler named the optimizer's curse (Smith & Winkler, Management Science, 2006). The remedy explored here is to hedge against a whole neighborhood of plausible distributions around $\hat P_N$, rather than trusting the point estimate. Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh's INFORMS TutORials chapter (2019) develops this neighborhood using the Wasserstein distance, and the present mission formalizes its foundational duality theory: the machinery every later result in the chapter (finite-sample guarantees, elliptical tractability, regularization) builds on.

Setting

Fix a norm $\|\cdot\|$ on a finite-dimensional real vector space $E$ (representing $\mathbb{R}^m$). For $p \in [1,\infty)$, the type-$p$ Wasserstein distance between two Borel probability measures $Q, Q'$ on $E$ is

$$W_p(Q,Q') = \left(\inf_{\pi \in \Pi(Q,Q')} \int_{E\times E} \|\xi-\xi'\|^p\, \pi(d\xi,d\xi')\right)^{1/p},$$

where $\Pi(Q,Q')$ is the set of couplings of $Q$ and $Q'$ — joint probability measures on $E \times E$ whose marginals are $Q$ and $Q'$. The optimal $\pi$ can be read as a transportation plan moving one pile of dirt ($Q$) into another ($Q'$) at minimum cost, which is why $W_p$ is also called the earth mover's distance; the underlying linear program was formalized by Kantorovich (1942) after Monge's 1781 original.

Given $N$ training samples $\hat\xi_1,\dots,\hat\xi_N$, the empirical distribution is $\hat P_N = \frac1N\sum_{i=1}^N \delta_{\hat\xi_i}$. Centered at $\hat P_N$, the Wasserstein ambiguity set of radius $\varepsilon \ge 0$ is

$$B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\},$$

where $\Xi \subseteq E$ is a closed set known to contain the support of the true distribution. The worst-case risk of a loss function $\ell$ is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} \mathbb{E}_Q[\ell(\xi)],$$

and minimizing it over a class of admissible loss functions $\mathcal{L}$ is a distributionally robust optimization problem. $\varepsilon$ measures the estimation error one insures against; a larger ambiguity set gives a more conservative (and more expensive) guarantee.

Formalization targets

Goal — Theorem 7, strong duality

$$R_{\varepsilon,p}(\hat P_N,\ell) = \inf_{\gamma \ge 0}\ \mathbb{E}_{\hat P_N}[\ell_\gamma(\xi)] + \gamma\varepsilon^p,\qquad \ell_\gamma(\xi) = \sup_{z\in\Xi} \ell(z) - \gamma\|z-\xi\|^p.$$

This is the Lagrangian dual of the worst-case risk evaluation problem, with $\gamma$ the multiplier of the Wasserstein constraint $W_p(Q,\hat P_N)\le\varepsilon$: it converts a supremum over an infinite-dimensional space of measures into a one-dimensional minimization of the Moreau-Yosida regularization $\ell_\gamma$. Every tractability result later in the chapter (finite convex reformulations, SDP relaxations) specializes this duality by choosing a loss class for which $\ell_\gamma$ is computable.

Supporting dual representations of $W_p$ — Theorems 1 and 2

$$W_p^p(Q,Q') = \sup\left\{\int \psi\,dQ' - \int \varphi\,dQ : \varphi,\psi \text{ bounded continuous},\ \psi(\xi)-\varphi(\xi') \le \|\xi-\xi'\|^p\right\}$$ $$W_1(Q,Q') = \sup_{\mathrm{Lip}(\varphi)\le 1} \int \varphi\,dQ - \int \varphi\,dQ'$$

These identify $W_p$ as a linear program's strong dual (Theorem 1) and, for $p=1$, specialize it to the Kantorovich-Rubinstein form (Theorem 2), which is what lets the worst-case-risk analysis reason about Lipschitz loss functions directly.

Upper and lower bounds — Theorems 5 and 6

$$R_{\varepsilon,p}(\hat P_N,\ell) \le R(\hat P_N,\ell) + \varepsilon\cdot\mathrm{Lip}(\ell)$$ $$R_{\varepsilon,p}(\hat P_N,\ell) \ge \sup\left\{\tfrac1N\textstyle\sum_i \ell(\hat\xi_i+\theta_i) : \hat\xi_i+\theta_i\in\Xi,\ \tfrac1N\textstyle\sum_i\|\theta_i\|^p\le\varepsilon^p\right\}$$

These are the tractable, easily-computed bracket that Theorems 7 and 10 later show is tight in important special cases.

Exact case — Theorem 10

$$\Xi = \mathbb{R}^m,\ \ell \text{ convex},\ p=1 \implies R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon\,\mathrm{Lip}(\ell)$$

Theorem 5's inequality becomes exact under convexity — the cleanest closing corollary of the duality theory, obtained from Theorem 7 by evaluating the Moreau-Yosida regularization of a convex function explicitly.

Significance

Theorem 7 is the hinge on which the entire computational program of Wasserstein distributionally robust optimization turns: every tractable reformulation in the source chapter (piecewise-concave losses via conic duality, quadratic losses via semidefinite programming, the shrinkage-estimator connection) is obtained by substituting a specific loss class into the right-hand side of Theorem 7 and showing the resulting Moreau-Yosida regularization is computable. Kuhn et al. themselves derive it as a corollary of Blanchet & Murthy (2019) and Gao & Kleywegt (2016) for the empirical case, generalized to Polish spaces by Blanchet & Murthy and Gao & Kleywegt independently — the paper cites [12] and [37] for the general statement. Formalizing it is what makes every later, more computational result in the chapter — the ones a solver is more likely to reach for next — rest on a mechanically verified foundation rather than a citation chain.

Status. The mathematical result is well established (multiple independent published proofs cited above); nothing here is open research. What this mission contributes is the first machine-checked formal statement of the duality theorem and its supporting dual representations (Theorems 1, 2, 5, 6, 10) on the Prove2Me platform — none of Wp's dual representation, the Wasserstein ambiguity set, or the worst-case risk functional exist there prior to this mission (see Formalization scope).

Difficulty

The obvious proof strategy — write down the Lagrangian of the semi-infinite program (6), swap the order of the outer supremum over $Q$ and the inner minimization over the multiplier $\gamma$, and invoke ordinary Lagrangian strong duality — fails because (6) is an infinite- dimensional linear program over measures, not a finite convex program: there is no compact feasible set or Slater point in a form that ordinary finite-dimensional duality applies to directly. The actual proof goes through the dual representation of the Wasserstein distance itself (Theorem 1, which is why it is a prerequisite milestone), reformulating the constraint $W_p(Q,\hat P_N)\le\varepsilon$ via its own dual variables and swapping the resulting sup-inf using minimax theorems for semi-infinite programs, not ordinary Lagrangian duality for finite programs.

Formalization scope

$E$ is a generic finite-dimensional real normed space (NormedAddCommGroup, NormedSpace ℝ, Borel-measurable), representing $\mathbb{R}^m$ with the paper's arbitrary fixed norm as a parameter rather than fixing the Euclidean norm. A coupling is formalized directly via MeasureTheory.Measure.map: π.map Prod.fst = Q ∧ π.map Prod.snd = Q'. Constrained infima/suprema (over couplings, over the ambiguity set, over Lipschitz test functions, over perturbation matrices) use Mathlib's guarded-binder idiom ⨅ x (_ : P x), f x, which correctly returns $\top$ (resp. $\bot$) outside the feasible set rather than a finite junk value.

Two deliberate, disclosed conventions keep the extremal-value definitions faithful without extended-real integration machinery, both recorded in MODERATION_NOTES.md:

1. worstCaseRisk and the dual representations (Theorems 1, 2) are valued in EReal, not ℝ, so an unbounded supremum is recorded as $+\infty$ rather than collapsed to Mathlib's real-valued junk value 0 on an unbounded family.
2. The goal theorem (7) and its Moreau-Yosida regularization restrict the loss function to bounded continuous $\ell$ (BoundedContinuousFunction E ℝ), narrower than the paper's general upper-semicontinuous, $\hat P_N$-integrable loss class $\mathcal{L}$ (Assumption 1). This keeps $\ell_\gamma(\xi) = \sup_{z\in\Xi}\ell(z)-\gamma\|z-\xi\|^p$ a finite real number for every nonempty $\Xi$, so the right-hand side's Bochner integral is well-posed; the milestones (Theorems 5, 6, 10) keep the more general real-valued (not necessarily bounded) loss class, since their statements do not require evaluating a pointwise supremum over $\Xi$.
3. Ξ is required closed in Theorems 5, 6 and 7, matching the paper's own standing assumption (p. 6: "we let $\Xi\subseteq\mathbb{R}^m$ be a closed set that is known to contain the support of $P$") for the whole worst-case-risk framework, which is used silently in the paper wherever a theorem takes $\Xi$ as an argument but was not carried into these theorems' own hypothesis lists in an earlier draft.
4. The goal theorem (7) additionally requires $\hat P_N$ itself supported on $\Xi$ ($\hat P_N(\Xi^c)=0$, the same "supported on $\Xi$" convention ambiguitySet uses for $Q\in\mathcal P(\Xi)$), which the paper's framework presupposes for the nominal distribution throughout §2. Combined with $\ell$ bounded, this makes $\ell_\gamma$ bounded on the full-measure set $\Xi$ (above by $\sup\ell$ unconditionally, below by $\ell(\xi)$ itself via $z=\xi$ for $\xi\in\Xi$), which is what makes the right-hand side's integral genuinely well-posed rather than liable to Mathlib's non-integrable junk value $0$.

There is no trivializing formalization risk from a vacuous hypothesis: Ξ.Nonempty and 0 < N are both required exactly where the paper's own indexing and support assumptions require them, and every extremal value uses the extended-real convention above rather than a convention that would make an inequality vacuously true.

No definition in this mission exists on the platform prior to this series (GET /theorems?q=Wasserstein, q=Kantorovich, q=optimal transport, q=coupling return only unrelated discrete/finite-type constructions); all seven definitions and six theorems are drafted fresh. WassersteinDRO.Duality.wassersteinDistance, .ambiguitySet and .worstCaseRisk are the substrate every later mission in this five-part series (Gelbrich tractability, finite-sample guarantees, regularization, shrinkage estimation) either imports directly or redefines locally per the series' reuse rule.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research, 130–166. https://doi.org/10.1287/educ.2019.0198
• Villani, C. (2009). Optimal Transport: Old and New. Springer. (Cited as [108] for Theorems 1 and 2.)
• Smith, J. E., & Winkler, R. L. (2006). The optimizer's curse: Skepticism and postdecision surprise in decision analysis. Management Science, 52(3), 311–322. https://doi.org/10.1287/mnsc.1050.0451
• Gao, R., & Kleywegt, A. J. (2016). Distributionally Robust Stochastic Optimization with Wasserstein Distance. arXiv:1604.02199.
• Blanchet, J., & Murthy, K. (2019). Quantifying Distributional Model Risk via Optimal Transport. Mathematics of Operations Research, 44(2), 565–600. https://doi.org/10.1287/moor.2018.0936

Motivation

A Markov decision process (MDP) chooses a decision in every period of a dynamic system whose state evolves stochastically in response to the decision, so as to maximize expected discounted return. Firms use this model for inventory, pricing, and advertising decisions that respond to a randomly evolving demand state; engineers use it for maintaining or replacing equipment that degrades stochastically. A recurring practical question is qualitative rather than numerical: does the optimal decision increase with the state — should a firm price higher after a period of strong sales, or replace a machine sooner the worse its observed condition — without having to solve the dynamic program numerically for every instance of the model? Topkis's Chapter 3, Section 3.9 (Topkis, Supermodularity and Complementarity, 2011, building on Topkis [1968]) answers this by isolating the lattice-theoretic structure — supermodularity of the return function and of the transition law — under which monotone optimal policies are guaranteed on structural grounds alone. A closely related but logically independent question was studied earlier by Lehmann [1955], who characterized when a family of distributions is stochastically increasing in a parameter; Topkis generalizes Lehmann's characterization to any property of the parameter dependence whose defining set of functions forms a closed convex cone, of which stochastic monotonicity, supermodularity, and convexity are three instances (Theorem 3.9.1, Corollary 3.9.1). Serfozo [1976] independently develops related conditions for partially observed Markov decision processes, and Amir [1996] and Amir, Mirman, and Perkins [1991] give analogous monotonicity results for other classes of dynamic programming models.

Setting

Fix a finite planning horizon of $k$ periods, $i = 1, \dots, k$. In period $i$ the state $t$ ranges over a set $T_i \subseteq \mathbb{R}^m$; given state $t$, the decision $x$ is restricted to a finite, nonempty set $X_{t,i} \subseteq \mathbb{R}^n$ (finiteness guarantees that an optimal decision always exists — no continuity or compactness argument is used). Write $S_i = \{(x,t) : t \in T_i,\, x \in X_{t,i}\}$ for the set of admissible (decision, state) pairs in period $i$. The (bounded) expected net return of choosing decision $x$ in state $t$, period $i$, is $r_i(x,t)$. A discount rate $\beta \in [0,1]$ gives $\gamma = 1/(1+\beta)$, the value in period $i$ of one unit of return in period $i+1$. Given decision $x$, state $t$, and period $i$, the state $w$ of period $i+1$ is drawn from a distribution $F(x,t,i,\cdot)$ on $\mathbb{R}^m$.

The optimal-value function $f_i(t)$ (present value of acting optimally from state $t$, period $i$, onward) and the decision-value function $g_i(x,t)$ (present value of choosing $x$ in state $t$, period $i$, then acting optimally thereafter) are defined by backward induction from period $k$:

$$g_k(x,t) = r_k(x,t), \qquad f_i(t) = \max_{x \in X_{t,i}} g_i(x,t), \qquad g_i(x,t) = r_i(x,t) + \gamma \int f_{i+1}(w)\, dF(x,t,i,w) \quad (i < k).$$

A subset $S$ of a Euclidean space is increasing if it is upward closed under the coordinatewise order. A family of distributions $\{F(a,\cdot) : a \in D\}$ indexed by a parameter $a$ is stochastically increasing on $D$ if the probability $\int_S dF(a,w)$ of every increasing set $S$ is a monotone (non-decreasing) function of $a$ on $D$; when $D$ is a sublattice, the family is stochastically supermodular on $D$ if that same probability is a supermodular function of $a$ on $D$. A real-valued function $\varphi$ on a lattice is supermodular on a set $D$ if $\varphi(a_1) + \varphi(a_2) \le \varphi(a_1 \vee a_2) + \varphi(a_1 \wedge a_2)$ for all $a_1, a_2 \in D$ — the mission series' shared notion, defined once in chunk 02-monotonicity and reused here as Supermodularity.Monotonicity.SupermodularOn.

Formalization targets

Goal — Theorem 3.9.2 (monotone optimal policies)

$$g_i(x,t) \text{ supermodular on } S_i, \qquad f_i(t) \text{ supermodular on } T_i, \qquad \arg\max_{x \in X_{t,i}} g_i(x,t) \text{ increasing in } t,$$

together with the existence of a greatest and a least optimal decision at every state, each increasing in the state, in every period $i$ — under the hypotheses that $S_i$ is a sublattice of $\mathbb{R}^{n+m}$, $X_{t,i}$ is expanding in $t$, $r_i$ is increasing in $t$ (on sections) and jointly supermodular in $(x,t)$, and $F(x,t,i,\cdot)$ is stochastically increasing in $t$ (on sections) and stochastically jointly supermodular in $(x,t)$, for every period $i$.

This is the weakest of the targets that is still worth stating on its own: it packages four related conclusions (parts (a)–(d) of Theorem 3.9.2) that share one hypothesis set, rather than isolating just the headline monotone-decision claim, because the book's own proof derives all four together and a solver attacking part (c) or (d) needs part (a) and (b) established first.

Supporting milestones

• Lemma 3.9.4: under the monotonicity half of the goal's hypotheses alone (no supermodularity), $f_i(t)$ is increasing in $t$ for every period $i$. This is the induction Theorem 3.9.2 reuses and strengthens.
• Corollary 3.9.1(b): on a sublattice $T$, a family of distributions is stochastically supermodular in $t$ iff $\int h(w)\,dF(t,w)$ is supermodular in $t$ for every increasing $h$. This is what lets the goal's hypothesis "$F(x,t,i,\cdot)$ stochastically supermodular in $(x,t)$" be converted into "$\int f_{i+1}(w)\,dF(x,t,i,w)$ supermodular in $(x,t)$", the step that feeds $g_i$'s supermodularity.
• Theorem 3.9.1: the general closed-convex-cone characterization of which Corollary 3.9.1(b) is the supermodularity instance (monotonicity and convexity are the other two instances, not formalized here since the goal's proof only needs the supermodularity case).

Significance

The result gives a purely structural sufficient condition — no smoothness, convexity of the decision set, or specific functional form — for monotone comparative statics in dynamic optimization: whenever the one-period return and the state transition are individually monotone and jointly supermodular in (decision, state), so is the whole multi-period value function, and so are the optimal decisions. Textbook applications include optimal advertising that decreases with prior-period sales, optimal pricing that increases with prior-period sales, and optimal maintenance of a deteriorating system, none of which need to be re-derived from scratch once the structural hypotheses are checked for the specific return and transition functions at hand.

Formalizing it contributes a genuinely new layer to the mission series and, per the paper's own triage (substrate.md), to the platform's application of Mathlib's probability-kernel infrastructure: a finite-horizon MDP with a Lebesgue–Stieltjes-style transition law and its associated stochastic-dominance vocabulary (stochastically increasing / stochastically supermodular families of distributions) did not previously exist on the platform or in this mission series, and both are reusable beyond this mission by any future formalization of dynamic programming under uncertainty. The proof itself is not open — Topkis [2011] (unchanged from the 1968/1998 original) gives a complete, elementary backward-induction argument — so what this mission produces is the formalization of a known, structurally distinctive proof technique, not a new mathematical result.

Difficulty

The naive argument — "supermodularity of $r_i$ plus supermodularity of the transition kernel obviously gives supermodularity of $g_i$" — breaks exactly at the integral: supermodularity of $(x,t) \mapsto F(x,t,i,\cdot)$ is a statement about the whole family of distributions, not about a single number, so "the transition is jointly supermodular" has to be unpacked into "the probability of every increasing set is jointly supermodular in $(x,t)$" before it says anything about $\int f_{i+1}(w)\,dF(x,t,i,w)$ for a specific function $f_{i+1}$. Corollary 3.9.1(b) is exactly the step that licenses this unpacking, and it is not free: it needs Theorem 3.9.1's closed-convex-cone argument (approximating $f_{i+1}$ from below by increasing step functions and invoking monotone convergence), not a pointwise argument on $r_i$ and $F$ separately. A second place the naive argument fails is at the constraint sets: because $X_{t,i}$ only grows with $t$ rather than being fixed, monotonicity of $f_i$ (Lemma 3.9.4) needs its own induction combining that growth with monotonicity of $g_i$ — supermodularity of $g_i$ alone does not hand you monotonicity of the arg max without it.

Formalization scope

States and decisions are represented as Fin m → ℝ and Fin n → ℝ (finite-dimensional Euclidean coordinate spaces with the coordinatewise/product order, matching the book's own restriction to $\mathbb{R}^m$ and $\mathbb{R}^n$ — no abstract lattice is used where the book itself specializes). Distributions are represented as MeasureTheory.Measure on the relevant coordinate space, with IsProbabilityMeasure supplied explicitly wherever a stochastic-dominance hypothesis is used (the probability of a set is read off as (μ S).toReal, which is only faithful to $\int_S dF$ when μ is a probability measure — an unconstrained arbitrary measure would let .toReal collapse an infinite value to $0$ and make the hypothesis trivially satisfiable, a formalization this mission rules out). Integrands h are required integrable against every measure in the family wherever an integral is asserted to lie in a set V, since the Bochner integral of a non-integrable function is definitionally 0 in Lean/Mathlib and would otherwise make Theorem 3.9.1 and Corollary 3.9.1(b) trivially true. Decision sets $X_{t,i}$ are finite (Finset, not merely a bounded or compact Set) and required nonempty exactly where the book assumes it: this finiteness, not any compactness or semicontinuity argument, is what guarantees an optimal decision exists, and dropping it would silently substitute Chapter 2's compactness-based existence machinery for the different argument this section actually uses. The optimal-value and decision-value functions $f_i, g_i$ are represented as any functions satisfying the two backward-recursion equations that define them, rather than being constructed by explicit backward recursion in Lean; since the equations determine $f_i, g_i$ uniquely from $r_i$ and $F$, this is a faithful reading of "define $f_i, g_i$ by (3.9.1) and (3.9.2)," not a weakening of the theorem. The goal's part (c) is stated using the mission series' InducedSetOrder (the Veinott/strong set order, chunk 01-lattices) and part (d) as the existence of two selection functions (greatest, least optimal decision), each monotone in the state — matching the book's "there is a greatest (least) optimal decision ... and this greatest (least) optimal decision is increasing in $t$." The infinite-horizon stationary extension that the book gives immediately after Theorem 3.9.2 (relying on an unproved citation to Blackwell [1965]) is out of scope for this mission.

Reusable infrastructure: the StochasticallyIncreasingOn/StochasticallySupermodularOn definitions are parametric in the ambient preorder/lattice and in the measure's target dimension, so a future mission on stochastic convexity (Corollary 3.9.1(c), not formalized here) or on Topkis's §3.10 stochastic inventory model (which explicitly depends on §3.9, per the book's own reading-order note) can reuse them without modification. Contributions extending this mission to the infinite-horizon case, or completing Corollary 3.9.1's monotonicity and convexity halves, are welcome.

Selected references

• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011 (unchanged from the 1998 original), Chapter 3, Section 3.9. DOI: 10.1515/9781400822539.
• D. M. Topkis, "Ordered Optimal Solutions," PhD dissertation / working paper, Stanford University, 1968 (the original source for this section's results).
• E. L. Lehmann, "Ordered Families of Distributions," Annals of Mathematical Statistics 26(3), 1955, pp. 399–419. https://doi.org/10.1214/aoms/1177728487
• R. Serfozo, "Monotone Optimal Policies for Markov Decision Processes," Mathematical Programming Study 6, 1976, pp. 202–215.
• R. Amir, "Sensitivity Analysis of Multisector Optimal Economic Dynamics," Journal of Mathematical Economics 25(1), 1996, pp. 123–141.
• R. Amir, L. J. Mirman, and W. R. Perkins, "One-Sector Nonclassical Optimal Growth: Optimality Conditions and Comparative Dynamics," International Economic Review 32(3), 1991, pp. 625–644.
• D. Blackwell, "Discounted Dynamic Programming," Annals of Mathematical Statistics 36(1), 1965, pp. 226–235. https://doi.org/10.1214/aoms/1177700285