Motivation

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a $d$-regular graph is governed by the Alon–Boppana bound $2\sqrt{d-1}$, and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ($d = p+1$ with $p$ prime) and special numbers of vertices (orders of $PSL(2,\mathbb F_q)$ or $SL(2,\mathbb F_q)$). Applications often need a graph of a prescribed size $n$.

N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly $n$ vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on $m$ vertices can be enlarged to $n = m + r$ vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.

Setting

Let $V$ be a finite set of $m \ge 1$ vertices. A $(n,d,\lambda)$-graph is a $d$-regular graph on $n$ vertices whose adjacency matrix $A$ satisfies $|\mu| \le \lambda$ for every nontrivial eigenvalue $\mu$, that is, every eigenvalue other than the top eigenvalue $d$ of the constant vector $\mathbf 1$. For a symmetric $A$ with $A\mathbf 1 = d\,\mathbf 1$, the nontrivial eigenvalues are those with an eigenvector $f \ne 0$ satisfying $\sum_v f(v) = 0$. Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry $1$ of $A$.

Fix an integer $p \ge 0$ and let $H$ be an $(m, p+1, 2\sqrt p)$-graph on $V$, a $(p+1)$-regular Ramanujan graph. Let $R = \{u_1, \dots, u_r\}$ be $r$ new vertices and let $W_1, \dots, W_r \subseteq V$ be pairwise disjoint sets of $p+2$ vertices each. Put $W = \bigcup_i W_i$ and $L = V \setminus W$. The graph $G$ on $U = V \cup R$ is obtained from $H$ by joining each $u_i$ to every vertex of $W_i$ and adding one loop at each vertex of $L$. Its adjacency matrix is

$$A_G = A_H + A_R + A_L,$$

where $A_H$ is the adjacency matrix of $H$ (zero on $R$), $A_R$ that of the stars joining $u_i$ to $W_i$, and $A_L$ the diagonal matrix of the loops. Every vertex of $G$ has degree $p+2$.

Formalization targets

Goal: Theorem 1.2, spectral core

$$A_G \text{ is an } \Big(m+r,\; p+2,\; \sqrt{2(p+1)} + \sqrt p + \frac{(p+1)\,r}{m}\Big)\text{ matrix.}$$

The paper states $\lambda \le \sqrt{2(d-1)} + \sqrt{d-1} + o(1)$ for $d = p+2$; its proof gives $\sqrt{2(p+1)} + \sqrt p + o(1)$, which is stronger, and the error term it produces is $(p+1)r/m$. The goal is parametrised by $H$, $r$ and the sets $W_i$, so it does not depend on how $m$ and $r$ are chosen.

Milestones

1. The variational characterization of the nontrivial eigenvalues: for a symmetric matrix with constant row sums and $\lambda \ge 0$, $|\mu| \le \lambda$ for every nontrivial eigenvalue if and only if $|f^tAf| \le \lambda\|f\|^2$ whenever $\sum f = 0$.
2. The Cauchy–Schwarz display: $\sum_U f = 0$ implies $|\sum_V f|^2 = |\sum_R f|^2 \le |R| \sum_R f^2$.
3. Inequality (3): $|f^tA_Hf| \le b^2(p+1) + c^2\, 2\sqrt p$ with $b^2 = (\sum_V f)^2/m$ and $c^2 = \sum_V f^2 - b^2$.
4. Display (4): $f^tA_Lf = \sum_{v\in L} f^2(v)$.
5. Inequality (5): $|f^tA_Rf| \le \frac{p+2}{x}\sum_R f^2 + x\sum_W f^2$ for every $x > 0$.
6. Inequality (6): for $\sum_U f = 0$ and $x > 0$,

$$|f^tA_Gf| \le (2\sqrt p+1)\sum_L f^2 + (2\sqrt p+x)\sum_W f^2 + \frac{p+2}{x}\sum_R f^2 + (p+1)\frac rm \sum_R f^2.$$

Significance

With $H$ the Lubotzky–Phillips–Sarnak graph on $m = |SL(2,\mathbb F_q)|$ vertices for the largest suitable prime $q$ with $m \le n$, and $r = n - m$, the distribution of primes in arithmetic progressions gives $r = o(m)$, and the goal yields an explicit $(n, p+2, \lambda)$-graph with $\lambda \le (1+\sqrt2)\sqrt{d-1} + o(1)$ for every sufficiently large $n$. This is within a factor of about $1.21$ of the Ramanujan bound $2\sqrt{d-1}$, for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.

The result is proved in the paper. No formalization of it, of the $(n,d,\lambda)$ notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.

Difficulty

The vertices of $W$ and $L$ lie in the old graph $H$, whose spectrum is controlled, but the new vertices of $R$ are not; and a vector orthogonal to $\mathbf 1$ on $U$ need not be orthogonal to the constant vector on $V$. Bounding $f^tA_Gf$ by applying the Ramanujan bound for $H$ to $f$ restricted to $V$ therefore fails: the restriction has a component along the trivial eigenvector of $H$, whose eigenvalue $p+1$ is large. The argument must show that this component is small, of order $r/m$, and must balance the star edges between $R$ and $W$ against the loops on $L$ so that every vertex class gets the same coefficient. The naive bound $|f^tA_Rf| \le \|A_R\|\,\|f\|^2 = \sqrt{p+2}\,\|f\|^2$ added to $2\sqrt p$ for $H$ and $1$ for $L$ gives a constant larger than $\sqrt{2(p+1)}+\sqrt p$; the stated constant needs the weighted estimate.

On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace $\mathbf 1^\perp$, while Mathlib states the spectral theorem for the whole space.

Formalization scope

• Vertices of $G$ are the disjoint union $V \oplus \mathrm{Fin}\, r$. $G$ is represented by its real adjacency matrix, since it has loops; $H$ is a Mathlib SimpleGraph with adjMatrix.
• The $(n,d,\lambda)$ predicate is stated for matrices: $|V| = n$, symmetry, $A\mathbf 1 = d\,\mathbf 1$, and $|\mu| \le \lambda$ for every eigenpair $(\mu, f)$ with $f \ne 0$ and $\sum f = 0$. For simple graphs, $d$-regularity is added.
• The paper's $o(1)$ terms are replaced by the explicit quantities its proof produces: $(p+1)r/m$ in the goal, and $(p+1)\frac rm\sum_R f^2$ in (6). Inequality (3) is stated with the corrected relation $b^2 + c^2 = \sum_V f^2$; the paper's "$b^2 + c^2 = 1$" holds only for unit restrictions.
• The bound uses $\sqrt p = \sqrt{d-2}$, as in the proof and the abstract, which implies the printed $\sqrt{d-1}$.
• $p$ is any natural number. The hypothesis "$p$ prime, $p \equiv 1 \pmod 4$" serves only to obtain $H$ from LPS, and $H$ is a hypothesis here. The sets $W_i$ are arbitrary pairwise disjoint sets of size $p+2$, not the paper's consecutive blocks of a numbering of $SL(2,\mathbb F_q)$.
• Out of scope: the existence of the prime $q$ and the estimate $n - m = o(m)$; the numbering of $SL(2,\mathbb F_q)$; the "strongly explicit" and polynomial-time claims; the LPS construction (Theorem 2.1, cited); the variant that replaces loops by a matching for even $n$.
• The goal cannot be satisfied trivially: dropping the condition $\sum f = 0$ makes it false, since $p+2$ is always an eigenvalue, and for $p \ge 2$ and small $r/m$ the bound is below $p + 2$ (for $p = 5$ it is about $5.70 + 6r/m$). At $p = 1$ the bound $3 + 2r/m$ is at least the degree $3$, so that case holds trivially; it is the paper's statement there as well.
• Contributions welcome: proofs of each milestone, especially the variational characterization, which is reusable for mission 3 of this series and for any regular-graph spectral argument.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Motivation

Large-scale nonsmooth convex problems, such as minimising a Lipschitz convex function over a probability simplex with millions of coordinates, are routinely solved by first-order methods that use one subgradient per iteration. The classical projected subgradient method reaches accuracy $\varepsilon$ after $O(L^2 R^2/\varepsilon^2)$ iterations, where $L$ and $R$ are measured in the Euclidean norm; on the simplex this hides a factor of order $n$ in the dimension. Nemirovski and Yudin's mirror descent algorithm (MDA) replaces the Euclidean geometry by one adapted to the feasible set and, on the simplex, reduces the dimension dependence to $\ln n$.

Beck and Teboulle (Oper. Res. Lett. 31 (2003) 167–175, doi:10.1016/S0167-6377(02)00231-6) showed that mirror descent is a projected subgradient method in which the squared Euclidean distance is replaced by a Bregman-type distance $B_\psi$. This viewpoint gives a short convergence proof, and with the entropy as $\psi$ it yields a fully explicit method on the simplex, the entropic mirror descent algorithm (EMDA), the same multiplicative update that underlies exponentiated-gradient and Hedge-type algorithms in online learning.

Timeline. Nemirovski and Yudin (1983) introduce mirror descent with a $O(\sqrt{\ln n}/\sqrt k)$ rate on the simplex. Ben-Tal, Margalit and Nemirovski (SIAM J. Optim. 12 (2001)) analyse MDA with the $\ell_p$ potential $\tfrac12\|x\|_p^2$, $p = 1 + 1/\ln n$, whose conjugate requires a one-dimensional root-finding at each step. Beck and Teboulle (2003) derive MDA as a nonlinear projected subgradient method (SANP), prove its efficiency estimate for an arbitrary norm, and show that the entropy gives the same $\sqrt{2\ln n}\,L_f/\sqrt k$ rate with a closed-form update.

Setting

Let $E$ be $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and $\|z\|_* = \max\{\langle x, z\rangle : \|x\| \le 1\}$ the dual norm. The problem is $\min\{f(x) : x \in X\}$ under Assumption A: $X$ is closed and convex; $f$ is convex on $X$ and Lipschitz there, $|f(x) - f(y)| \le L_f\|x - y\|$; $f$ has a minimiser $x^* \in X$; and a subgradient $f'(x)$ can be computed at every $x \in X$.

Let $\psi : X \to \mathbb R$ be strongly convex with parameter $\sigma > 0$ and differentiable. The distance-like function (3.10) is

$$B_\psi(x, y) = \psi(x) - \psi(y) - \langle x - y, \nabla\psi(y)\rangle .$$

The subgradient algorithm with nonlinear projections (SANP, (3.11)) starts from $x^1$ and sets, with step sizes $t_k > 0$,

$$x^{k+1} = \operatorname*{argmin}_{x \in X}\Big\{\langle x, f'(x^k)\rangle + \tfrac{1}{t_k} B_\psi(x, x^k)\Big\}.$$

With $\psi = \tfrac12\|\cdot\|_2^2$ this is the projected subgradient method.

On the unit simplex $\Delta = \{x \in \mathbb R^n : x \ge 0,\ \sum_j x_j = 1\}$ take the entropy $\psi_e(x) = \sum_j x_j \ln x_j$ (5.27), with $0\ln0 = 0$. SANP becomes the entropic descent algorithm (EDA):

$$x^{k+1}_j = \frac{x^k_j\,e^{-t_k f'_j(x^k)}}{\sum_{i=1}^n x^k_i\,e^{-t_k f'_i(x^k)}} .$$

Formalization targets

Goal: Theorem 5.1 (p. 174)

If $f$ is convex and $L_f$-Lipschitz on $\Delta$ for $\|\cdot\|_1$, with subgradients satisfying $\|f'(x)\|_\infty \le L_f$, and the EDA is started at $x^1 = n^{-1}e$ with step $t = \sqrt{2\ln n}/(L_f\sqrt k)$ for a horizon $k \ge 1$, then

$$\min_{1 \le s \le k} f(x^s) - \min_{x \in \Delta} f(x) \le \frac{\sqrt{2\ln n}\;L_f}{\sqrt k}.$$

The general estimate: Theorems 4.1 and 4.2 (pp. 171–172)

For any norm, any $\sigma$-strongly convex $\psi$ and any SANP run,

$$\min_{1 \le s \le k} f(x^s) - \min_X f \le \frac{B_\psi(x^*, x^1) + (2\sigma)^{-1}\sum_{s=1}^k t_s^2\|f'(x^s)\|_*^2}{\sum_{s=1}^k t_s},$$

and with the optimal constant step this gives $L_f\sqrt{2B_\psi(x^*, x^1)/\sigma}/\sqrt k$.

The milestones follow the paper's proof: the three-point identity (Lemma 4.1), the optimality condition (4.16), the lower bound $B_\psi \ge \tfrac\sigma2\|\cdot\|^2$, the one-step inequality (4.21), Theorem 4.1(a), Proposition 4.1 (optimal step), Theorem 4.2 and its version with an upper bound on $B_\psi(x^*, x^1)$; then for the simplex, the 1-strong convexity of $\psi_e$ for $\|\cdot\|_1$ (Proposition 5.1(a), Remark 5.1), the bound $B_{\psi_e}(x^*, n^{-1}e) \le \ln n$ (Proposition 5.1(c)), and the identification of the EDA with SANP.

Significance

The result shows that for nonsmooth convex minimisation over the simplex an explicit first-order method attains accuracy $\varepsilon$ in $O(L_f^2\ln n/\varepsilon^2)$ iterations, with $L_f$ measured in the $\ell_\infty$ dual norm. The general estimate of Theorem 4.2 applies to any norm and any strongly convex potential, and is the template for later analyses of mirror descent, its stochastic and online variants, and mirror-prox methods.

Formalizing the paper produces a norm-agnostic, machine-checked proof of the mirror descent efficiency estimate, in which subgradients are dual-space objects and the dual norm is explicit, and a verified link between the entropy, the $\ell_1$ geometry and the multiplicative-weights update. To our knowledge none of these statements is formalized; existing formal developments of online mirror descent work in Euclidean space with Legendre potentials and bound regret for linear losses, which is a different statement.

Difficulty

The algebra of Theorem 4.1 is short, but it rests on facts that are not available off the shelf. The first-order optimality condition (4.16) must be derived for a minimiser over a convex set without assuming the set has interior (the simplex has none in $\mathbb R^n$). The bound $B_\psi(u, y) \ge \tfrac\sigma2\|u - y\|^2$ must be obtained from the chord definition of strong convexity for an arbitrary norm. On the simplex, strong convexity of the entropy with respect to $\|\cdot\|_1$ is a form of Pinsker's inequality, and it must hold on the closed simplex, where the entropy is not differentiable at the boundary. Finally, the EDA must be shown to be the exact minimiser of the SANP subproblem over $\Delta$, which is a Gibbs variational principle. A tempting shortcut, working throughout in Euclidean space, fails: it changes the dual norm of the subgradients from $\ell_\infty$ to $\ell_2$ and the strong convexity constant of the entropy, and loses the $\ln n$ rate.

Formalization scope

Sections 3–4 live in a general real normed space; a subgradient is a continuous linear functional, $\langle u, f'(x)\rangle$ is its value at $u$, and $\|\cdot\|_*$ is the operator norm. $\nabla\psi$ is the Fréchet derivative. Iterates are indexed from $1$. A SANP run is a predicate on sequences: each step size is positive, each iterate lies in $X$, $\psi$ is differentiable there, and the next iterate minimises the SANP objective. This encodes the paper's standing assumption that SANP is well defined, and replaces "$X$ has nonempty interior" and "$x^1 \in \operatorname{int} X$". Section 5 works on $\mathbb R^n$ as functions $\{1, \dots, n\} \to \mathbb R$ with explicit $\ell_1$ and $\ell_\infty$ sums; $\operatorname{int}\Delta$ is the relative interior, and the entropy formula is evaluated on $\Delta$ only. "$\min_{1\le s\le k} f(x^s) - \min_X f \le R$" is stated as the existence of $s \in \{1, \dots, k\}$ with $f(x^s) - f(x^*) \le R$.

Added hypotheses, each disclosed in the item: a bound $\|f'(x)\|_* \le L_f$ on the oracle (used by the proofs of Theorems 4.1(b), 4.2 and 5.1, not implied by the Lipschitz condition for subgradients relative to $X$); $D^{-1}b > 0$ in Proposition 4.1, without which the proposition as printed is false; $L_f > 0$ in the step sizes. The step sizes of (4.23) and of the EDA are constant over a fixed horizon $k$, which is what the proof chooses; Theorem 5.1 is stated with $L_f$, since the free index in the printed bound (5.28) cannot be bound, and $L_f$ is what the proof yields.

Trivializing formalizations are ruled out: $B_\psi$ is never evaluated where fderiv is a junk value (the run requires differentiability at every iterate), the SANP step is never chosen by Classical.epsilon, the bound of Theorem 5.1 is not stated with a maximum of $\|f'(x^s)\|_\infty$ over the run, and the step is not an anytime schedule $t_s \propto 1/\sqrt s$.

A complete development needs first-order optimality conditions over convex sets, strong convexity and Bregman distances in normed spaces, Pinsker-type inequalities for finite distributions, and the Gibbs variational principle. These are reusable beyond this mission; proofs of any milestone, and general lemmas that serve several of them, are welcome.

Selected references

• A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Oper. Res. Lett. 31 (2003) 167–175. https://doi.org/10.1016/S0167-6377(02)00231-6
• A. Ben-Tal, T. Margalit, A. Nemirovski, The ordered subsets mirror descent optimization method with applications to tomography, SIAM J. Optim. 12 (2001) 79–108. https://doi.org/10.1137/S1052623499354564
• A. Nemirovsky, D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• G. Chen, M. Teboulle, Convergence analysis of a proximal-like minimization algorithm using Bregman functions, SIAM J. Optim. 3 (1993) 538–543. https://doi.org/10.1137/0803026

Motivation

The newsvendor problem is the basic model of inventory under uncertain demand. A decision maker orders $q$ units before demand $D$ is observed, and pays a unit backordering cost $b$ for each unit of unmet demand and a unit holding cost $h$ for each unit left over. When the demand distribution is known, the optimal order is a quantile of it. In practice the distribution is unknown and the decision maker holds historical data, often including features: observable covariates such as the day of the week, the weather or a recent sales trend, recorded alongside each past demand.

Rudin and Vahn (MIT Sloan Working Paper 5036-13, version of February 6, 2014, from MIT DSpace; published as Ban and Rudin, Operations Research 67(1), 2019, doi:10.1287/opre.2018.1757) propose to learn the order quantity directly as a linear function of the features, by minimizing the empirical newsvendor cost over the training data, with or without a regularization penalty. Their question is the one any data-driven decision rule must answer: how much worse can the learned rule do on new data than it did on the data it was fitted to? When the number of features $p$ is comparable to the sample size $n$ ("big data"), a bound that grows with $p$ says nothing, and the paper's Theorem 2 gives one for the regularized rule that does not depend on $p$.

This mission formalizes that bound, Theorem 2 of the working paper, together with the results its proof is assembled from. All page and result numbers refer to the 2014 working paper, not to the published article.

Setting

Cost. For an order $q$ and a demand $d$, the newsvendor cost is

$$C(q;d)=b\,(d-q)^+ + h\,(q-d)^+ ,\qquad b,h>0 .$$

Write $b\vee h=\max(b,h)$.

Data. A data point is a pair $z=(x,d)$ of a feature vector $x\in\mathbb R^p$ and a demand $d\in\mathbb R$. Features lie in a domain $\mathcal X$ inside the ball $\|x\|_2^2\le X_{\max}^2$, and demands lie in $\mathcal D=[0,\bar D]$. A sample $S_n=\{(x_i,d_i)\}_{i=1}^n$ consists of $n$ independent draws from an unknown probability distribution $\mu$ concentrated on $\mathcal X\times\mathcal D$.

Rules and risks. A vector $q\in\mathbb R^p$ defines the linear decision rule $q(x)=q^\top x$. Its true risk and empirical risk are

$$R_{true}(q)=\mathbb E_{(x,d)\sim\mu}\bigl[C(q^\top x;d)\bigr],\qquad \hat R(q;S_n)=\frac1n\sum_{i=1}^n C(q^\top x_i;d_i).$$

The regularized algorithm (NV-reg). For a parameter $\lambda>0$, the rule $\hat q=\hat q(S_n)$ minimizes

$$\hat R(q;S_n)+\lambda\|q\|_2^2\qquad\text{over } q\in\mathbb R^p .$$

The objective is strictly convex, so the minimizer is unique. Following Appendix B of the paper, the rules the algorithm outputs on samples from $\mathcal X\times\mathcal D$ are assumed to map $\mathcal X$ into $\mathcal D$ (the paper's $\mathcal Q\subset\mathcal D^{\mathcal X}$): the learned order quantity is never negative and never exceeds the demand cap.

Uniform stability. An algorithm is uniformly stable with parameter $\alpha_n$ if removing one observation from any sample changes the loss of its output at any test point by at most $\alpha_n$ (Bousquet and Elisseeff's Definition 6, the paper's Definition 1).

Formalization targets

Goal: Theorem 2 (p. 9)

For every $\delta\in(0,1)$ and $n\ge1$, with probability at least $1-\delta$ over $S_n$,

$$|R_{true}(\hat q)-\hat R(\hat q;S_n)|\le\frac{(b\vee h)^2X_{\max}^2}{n\lambda}+\Bigl(\frac{2(b\vee h)^2X_{\max}^2}{\lambda}+(b\vee h)\bar D\Bigr)\sqrt{\frac{\ln(2/\delta)}{2n}} .$$

The dimension $p$ appears nowhere in the bound.

Milestones, in the order of the proof (p. 32)

1. Lemma 5 (p. 28). For $q,d\in[0,\bar D]$, $|C(q;d)|\le(b\vee h)\bar D$, and the bound is attained.
2. Display (31) (p. 31). $C$ is convex in its first argument and $(b\vee h)$-Lipschitz in it, i.e. $(b\vee h)$-admissible in the sense of Definition 2.
3. Theorem 5 (p. 31), Bousquet and Elisseeff's Theorem 22: regularization in a reproducing kernel Hilbert space with a $\sigma$-admissible loss and kernel bound $\kappa^2$ has uniform stability $\sigma^2\kappa^2/(2\lambda n)$. This is an existing platform statement, referenced rather than restated.
4. Theorem 4 (p. 30). (NV-reg) is uniformly stable with parameter $\alpha_n^r=(b\vee h)^2X_{\max}^2/(2n\lambda)$.
5. Theorem 6 (p. 31). Any algorithm with uniform stability $\alpha_n$ and loss in $[0,M]$ satisfies, with probability at least $1-\delta$,

$$|R_{true}(A,S_n)-\hat R(A,S_n)|\le2\alpha_n+(4n\alpha_n+M)\sqrt{\frac{\ln(2/\delta)}{2n}} .$$

Significance

The result. Theorem 2 bounds the generalization gap of the regularized feature-based newsvendor rule at rate $O(1/\sqrt n)$ with constants that depend on the costs, the demand cap, the feature radius and $\lambda$, but not on the number of features. It gives a theoretical basis for regularizing when $p/n$ is not small, and it indicates how to scale $\lambda$ with the feature radius. The companion bound for the unregularized rule (Theorem 1) grows linearly in $p$.

Formalizing it. The theorem is proved in the paper, but its proof is short and relies on cited results: Theorem 5 and Theorem 6 are stated with references to Bousquet and Elisseeff and no proof of their own, and the paper's Theorem 6 is a two-sided variant of Bousquet and Elisseeff's Theorem 12 that is only sketched. None of these results has a machine-checked proof. A formalization produces a checked two-sided stability-to-generalization theorem for general algorithms (reusable for any stable learner), a checked stability bound for a regularized piecewise-linear loss, and the newsvendor bound itself, with the constants the proof actually supports.

Difficulty

The bound is not a uniform-convergence argument: the class of linear rules on $\mathbb R^p$ has complexity growing with $p$, so any bound that holds simultaneously for all rules in the class depends on $p$. The bound must exploit the specific rule produced by the algorithm. The two analytic steps that carry this are the stability of the regularized minimizer, which needs a strong-convexity comparison between the full and the leave-one-out objective, and a concentration inequality of bounded-differences type for a function of the whole sample whose differences are controlled only through stability.

The leave-one-out comparison is a known pitfall. If the leave-one-out problem is run literally on $n-1$ points it carries the weight $1/(n-1)$, and the comparison argument then gives twice the constant of Theorem 4. The stated constant holds for the leave-one-out objective that keeps the weight $1/n$, which is the form of Theorem 5.

Formalization scope

Representation. Features are EuclideanSpace ℝ (Fin p), rules are vectors acting by the inner product, and data points live in EuclideanSpace ℝ (Fin p) × ℝ. The cost is the published newsboy loss with overage cost $h$ and underage cost $b$; the empirical and true risks are the published empirical and generalization errors, and the (NV-reg) objective and its $1/n$-weighted leave-one-out version are the published regularized objectives of Bousquet and Elisseeff. The regularizer is $\lambda\|q\|_2^2$ (the display prints both $\lambda\|q\|_2^2$ and $\lambda\|q\|_2$; the text calls the problem a quadratic program). "With probability at least $1-\delta$" is stated as: the event on which the gap exceeds the bound has measure at most $\delta$ under the product measure $\mu^n$.

Standing assumptions and pinned hypotheses.

1. $b,h,\lambda>0$, $X_{\max},\bar D\ge0$, $n\ge1$, $\delta\in(0,1)$.
2. $\mu$ is a probability measure giving full mass to $\mathcal X\times[0,\bar D]$, with $\|x\|_2^2\le X_{\max}^2$ on $\mathcal X$ (§3, p. 9; the page writes the ball as $\|x\|_2^2\le X_{\max}$, while Theorem 2's "$X_{\max}^2$ as the largest possible value of $\|x\|_2^2$" and Theorem 5's note fix the reading).
3. The algorithm is any map $S_n\mapsto\hat q(S_n)$ whose value minimizes the (NV-reg) objective, measurable in $S_n$ (Appendix B: "all functions are measurable").
4. The range assumption of Appendix B: for samples from $\mathcal X\times\mathcal D$, $\hat q^\top x\in[0,\bar D]$ for $x\in\mathcal X$.
5. The last constant is $(b\vee h)\bar D$, the loss bound $M$ from Lemma 5 that the proof feeds into Theorem 6; display (6) prints $\bar D$ there.
6. The convention that all sets are countable, and the intercept convention $x^1=1$, are not imposed.

Trivializing formalization ruled out. The range assumption is quantified only over feature vectors in $\mathcal X$ and over samples drawn from $\mathcal X\times\mathcal D$; stated over the whole ball $\|x\|_2\le X_{\max}$, it would force $\hat q=0$ (both $\hat q^\top x$ and $\hat q^\top(-x)$ would lie in $[0,\bar D]$) and the goal would be nearly empty.

What is needed and reusable. McDiarmid's two-sided bounded-differences inequality under product measures; integrability of bounded measurable losses; existence and properties of minimizers of strongly convex objectives on $\mathbb R^p$; the comparison argument behind Theorem 5. Theorem 6 is stated for an arbitrary data space and hypothesis space and is reusable for any uniformly stable algorithm. Contributions to the Theorem 5 reference and to McDiarmid's inequality benefit other missions as well.

Selected references

• C. Rudin and G.-Y. Vahn, The Big Data Newsvendor: Practical Insights from Machine Learning, MIT Sloan School Working Paper 5036-13, version of February 6, 2014 (MIT DSpace). The version formalized here.
• G.-Y. Ban and C. Rudin, The Big Data Newsvendor: Practical Insights from Machine Learning, Operations Research 67(1):90–108, 2019. https://doi.org/10.1287/opre.2018.1757
• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2:499–526, 2002. https://jmlr.org/papers/v2/bousquet02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, London Math. Soc. Lecture Note Series 141, 148–188, 1989. https://doi.org/10.1017/CBO9781107359949.008

Prove that $k$-SAT is NP-complete for every fixed $k\ge3$, with at most $k$ literal occurrences per clause.

Construct the reductions and certificate verifier using the existing WordRAM definitions. We reuse proved polynomial backend and Cook–Levin SAT completeness.

References:

• Richard M. Karp. Reducibility Among Combinatorial Problems. Complexity of Computer Computations, 85–103, 1972. Main Theorem, problem 11; reduction, p. 98.
• Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
• Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

Motivation

Many systems consist of units that form themselves into clusters: individuals at a gathering forming conversational groups, monomers forming polymers, particles coagulating and fragmenting. Chapter 8 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) treats such clustering processes as Markov processes whose state counts the clusters of each type, and shows that when the process is reversible its equilibrium distribution has an explicit product form. The chapter opens with a model of social grouping (§8.1), develops a general basic model (§8.2) and later applies it to polymerization (§8.4).

The basic model sits in the same family as the migration processes and queueing networks of the earlier chapters: the method is to guess reversibility, solve the detailed balance equations, and normalize. Its specific feature is that the transitions are unions and break-ups of clusters, with rates quadratic in the cluster counts, rather than movements of single individuals.

Setting

There is a countable collection of cluster types $r$. A state is a vector $m = (m_r)$ of non-negative integers, $m_r$ being the number of $r$-clusters present, with only finitely many $m_r$ non-zero. For cluster types $r, s, u$ let $e_r$ be the $r$-th unit vector and

$$R^{rs}_u m = m - e_r - e_s + e_u, \qquad R^u_{rs} m = m + e_r + e_s - e_u,$$

the union of an $r$-cluster with an $s$-cluster into a $u$-cluster, and the break-up of a $u$-cluster into an $r$-cluster and an $s$-cluster. Given non-negative parameters $\lambda_{rsu} = \lambda_{sru}$ and $\mu_{rsu} = \mu_{sru}$, the clustering process has transition rates

$$q(m, R^{rs}_u m) = \lambda_{rsu} m_r m_s \ (r \ne s), \qquad q(m, R^{rr}_u m) = \lambda_{rru} m_r(m_r - 1), \qquad q(m, R^u_{rs} m) = \mu_{rsu} m_u. \qquad (8.3)$$

A closed clustering process lives on a finite irreducible state space $\mathcal S$. The open clustering process additionally lets one-clusters enter at rate $\nu$ and leave at rate $\mu m_1$,

$$q(m, m + e_1) = \nu, \qquad q(m, m - e_1) = \mu m_1, \qquad (8.7)$$

and its state space is the countable set of all $m$ with $\sum_r m_r$ finite, every state being reachable from every other.

An equilibrium distribution is a collection of positive numbers $\pi(m)$ summing to one that satisfies the equilibrium equations $\pi(m)\sum_{m'} q(m, m') = \sum_{m'} \pi(m') q(m', m)$; the process is reversible in equilibrium exactly when $\pi$ satisfies the detailed balance conditions $\pi(m) q(m, m') = \pi(m') q(m', m)$.

Formalization targets

Goal: Theorem 8.2 (p. 164)

If there are positive numbers $c_r$ with

$$\nu = c_1 \mu, \qquad \lambda_{rsu} c_r c_s = c_u \mu_{rsu}, \qquad (8.8) \qquad \sum_r c_r < \infty, \qquad (8.9)$$

then the open clustering process has equilibrium distribution

$$\pi(m) = \prod_{r} e^{-c_r} \frac{c_r^{m_r}}{m_r!}, \qquad (8.10)$$

it is reversible, and the counts $m_1, m_2, \dots$ are independent, $m_r$ being Poisson with mean $c_r$.

Milestones

• Eq. (8.6): under (8.4), $c_r c_s \lambda_{rsu} = c_u \mu_{rsu}$, the weights $\prod_r c_r^{m_r}/m_r!$ satisfy the detailed balance conditions for the rates (8.3) on the whole state space.
• Theorem 8.1 (p. 163): under (8.4) the closed clustering process is reversible with equilibrium distribution $\pi(m) = B\prod_r c_r^{m_r}/m_r!$ on $\mathcal S$.
• Eq. (8.2) (p. 161): the social grouping model with $M$ individuals has equilibrium $\pi(m) = B \prod_{i} \frac{1}{m_i!}\bigl(\frac{\beta}{\alpha\, i!}\bigr)^{m_i}$ on $\{m : \sum_i i m_i = M\}$.
• Eq. (8.9) (p. 164): the product-form weights are summable over the finitely supported states if and only if $\sum_r c_r < \infty$, and then (8.10) sums to one.

Significance

Theorem 8.2 gives the equilibrium of a whole class of coagulation–fragmentation dynamics in closed form: the cluster counts are independent Poisson variables, and the equation system (8.8) is the only thing to solve. Quantities such as the expected number of clusters of each type, or the proportion of units in clusters of a given size, are then read off directly. Theorem 8.1 gives the corresponding result for a closed system, where the normalizing constant couples the types; opening the system removes that coupling. The results are the base of the polymerization models of §8.4 and of the later literature on reversible coagulation–fragmentation processes.

The results are proved in the book, with short proofs that state the detailed balance computation is "readily verified". To our knowledge they have no machine-checked proof. The work this mission asks for is the formal verification of that computation for the aggregated rate function, including unions in which two clusters of the same type meet, and the normalization of an infinite product over a countable set of types, which the book takes for granted.

Difficulty

The book calls the detailed balance computation readily verified; the bookkeeping is where a formal check can fail. Two different unions, or a break-up and the entry of a one-cluster, can lead from the same state to the same state when a cluster type is reproduced by the transition, so the rate between two states is a sum over transitions, and the identity has to be checked for the sums, not for single transitions. The same-type case $r = s$ carries the falling factorial $m_r(m_r - 1)$ rather than $m_r^2$.

The normalization is the second difficulty. The state space of the open process is countably infinite, the product (8.10) runs over infinitely many types, and the interchange $\sum_m \prod_r = \prod_r \sum_{n}$ that makes it sum to one requires (8.9). Without (8.9) the weights are not summable; this is the content of the book's remark that (8.9) is necessary.

Formalization scope

Cluster types are an arbitrary countable type R carrying a linear order, used only to count each unordered pair of types once. States are finitely supported vectors R →₀ ℕ. The rate $q(m, m')$ is the sum of the rates (8.3) of all unions and break-ups taking $m$ to $m'$, plus, for the open process, the rates (8.7); a transition is present only when the clusters it consumes exist, and $q(m, m) = 0$ holds because every transition changes the number of clusters. The one-cluster type is a distinguished element one. The closed state space is a finite non-empty set closed under positive-rate transitions and irreducible. The open process carries the book's assumptions that every state is reachable from every other and that the total rate out of each state is finite.

The statements are at the level of rates: reversibility is detailed balance for a positive, normalized $\pi$, the equivalence with reversibility of the stationary process being Kelly's Theorem 1.3. That $\pi$ is the law of a stationary Markov process with these rates is not formalized. Independence and the Poisson laws are stated as the joint law of every finite set of counts. A formalization in which $c_r$ may vanish, in which detailed balance is imposed only for a degenerate choice of rates, or in which (8.10) is not normalized does not meet the goal: the $c_r$ are positive, the rates are arbitrary non-negative symmetric parameters, and both detailed balance and total mass one are required.

The development uses the published definitions KellyStochasticNetworks_Balance (detailed balance and the equilibrium equations) and the proved implication from detailed balance to the equilibrium equations. Lemmas on summing products over finitely supported vectors, and on infinite products of exponentials, are reusable beyond this mission. Lemma 8.3, a partial converse to Theorem 8.1, is not part of this mission; a faithful statement of it, with the units structure of the clusters, is a welcome addition.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979, Chapter 8. Reissued by Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511564246 (author's copy: http://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html)
• P. Whittle, Systems in Stochastic Equilibrium, Wiley, 1986 (reversible models of association and polymerization). ISBN 978-0-471-90887-0.
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014 (detailed balance and the equilibrium equations used here). https://doi.org/10.1017/CBO9781139565363

Motivation

A migration process is a continuous-time Markov model of a population spread over $J$ sites, called colonies, in which individuals move one at a time: between colonies, out of the system, or into it from outside. The model was introduced by Whittle (1967) and Kingman (1969) and is the framework of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979). It covers closed and open networks of queues (Jackson networks), linear population models and the movement of particles between cells. Its central fact is that the equilibrium distribution is a product form: the joint law of the colony sizes factorizes into one term per colony, and for open processes the colony sizes are independent in equilibrium.

In the migration processes of Chapter 2 the rate at which an individual leaves colony $j$ depends on the number $n_j$ there, but not on the number already present in the colony it joins. Chapter 6 (§6.1) lifts this restriction. The rate of a move into colony $k$ is multiplied by a function $\psi_k(n_k)$ of the receiving colony's occupancy, which can model blocking (a crowded colony slows arrivals) or attraction (as in the models of social grouping of §6.2). The price is that product form survives only under a reversibility condition on the routing parameters. This mission formalizes the two theorems of §6.1 on top of the already-formalized results of Chapter 2.

Timeline. Whittle (1967) and Kingman (1969) introduced migration processes and their product-form equilibria; Kelly (1976) treated networks of queues with general routes; Kelly (1979, Ch. 2) states the closed and open product forms (Theorems 2.3, 2.4) and the time reversal of an open process (Theorem 2.5); Kelly (1979, §6.1) states the reversible versions with receiving-colony dependence (Theorems 6.1, 6.2).

Setting

There are $J$ colonies. The state is $n = (n_1,\dots,n_J) \in \mathbb{N}^J$, with $n_j$ the number of individuals in colony $j$. Three operators change the state by one individual: $T_{jk}n$ moves one individual from colony $j$ to colony $k$, $T_{j\cdot}n$ removes one from colony $j$, and $T_{\cdot k}n$ adds one to colony $k$.

The model is given by non-negative constants $\lambda_{jk}$ (with $\lambda_{jj} = 0$), $\mu_j$, $\nu_k$, and functions $\varphi_j,\psi_j : \mathbb{N}\to\mathbb{R}$ with $\varphi_j(0) = 0$, $\varphi_j(n) > 0$ for $n > 0$, and $\psi_j(n) > 0$ for all $n \ge 0$. A closed reversible migration process with $N$ individuals has state space $\mathcal{S} = \{n : \sum_j n_j = N\}$ and transition rates

$$q(n, T_{jk}n) = \lambda_{jk}\,\varphi_j(n_j)\,\psi_k(n_k). \qquad (6.2)$$

An open reversible migration process has state space $\mathbb{N}^J$ and, in addition to (6.2), the rates

$$q(n, T_{j\cdot}n) = \mu_j\,\varphi_j(n_j) \quad (6.5), \qquad q(n, T_{\cdot k}n) = \nu_k\,\psi_k(n_k) \quad (6.6).$$

The parameters are required to make the process irreducible: in the closed case an individual can pass between any two colonies along pairs with $\lambda_{ab} > 0$; in the open case it can reach every colony from outside and leave from every colony. Setting $\psi_j \equiv 1$ recovers the migration processes of Chapter 2.

Given positive constants $\alpha_1,\dots,\alpha_J$, the candidate equilibrium is

$$\pi(n) = B\prod_{j=1}^{J}\Bigl\{\alpha_j^{n_j}\prod_{r=1}^{n_j}\frac{\psi_j(r-1)}{\varphi_j(r)}\Bigr\}, \qquad (6.3)$$

with $B$ chosen so that $\pi$ sums to one over the state space.

Formalization targets

Goal: Theorem 6.2 (open process)

If positive $\alpha_j$ satisfy

$$\alpha_j\lambda_{jk} = \alpha_k\lambda_{kj} \quad (6.4), \qquad \alpha_j\mu_j = \nu_j \quad (6.7),$$

and every colony series $g_j = \sum_{m\ge 0}\alpha_j^m\prod_{r=1}^m \psi_j(r-1)/\varphi_j(r)$ converges, then (6.3) with $B = \prod_j g_j^{-1}$ is in detailed balance with the rates (6.2), (6.5), (6.6), satisfies the equilibrium equations, is positive and sums to one, and under it $n_1,\dots,n_J$ are independent with marginals $\pi_j(m) = g_j^{-1}\alpha_j^m\prod_{r=1}^m\psi_j(r-1)/\varphi_j(r)$.

Milestones

• Theorem 2.3: the closed migration process ($\psi\equiv 1$) has equilibrium of the form (2.3).
• Theorem 2.4: the open migration process has independent colonies with marginals $b_j\alpha_j^{n_j}/\prod_{r=1}^{n_j}\varphi_j(r)$.
• Theorem 2.5: the reversal of a stationary open migration process is an open migration process.
• Theorem 6.1: the closed process with rates (6.2) is reversible under (6.4), with equilibrium (6.3) on $\mathcal{S}$.

Theorems 2.3–2.5 are already proved on the platform and enter as references.

Significance

The result. Theorem 6.2 shows that product form and independence of colony sizes are not tied to routing that ignores the destination's occupancy. Any positive $\psi_k$ is allowed, provided the routing is reversible in the sense of (6.4) and (6.7). This is what makes the social-grouping models of §6.2 and the clustering models of Chapter 8 tractable, and it identifies (6.4) as the structural condition: Exercise 6.1.1 shows that without it the process cannot be reversible. Through Theorem 1.3 of the book, detailed balance also gives that the stationary process looks the same run backwards in time.

Formalization. The Chapter 2 results (Theorems 2.3–2.5) are formalized and proved on the platform, at the level of transition rates, in the KellyStochasticNetworks series. Theorems 6.1 and 6.2 are not formalized anywhere to our knowledge. The new work is the detailed-balance verification with the receiving-colony factor, the normalization over the finite set $\mathcal{S}$ in the closed case, and the summation over the countable space $\mathbb{N}^J$ with the marginal computation that expresses independence in the open case.

Difficulty

The equilibrium equations of a migration process with blocking have no simple solution in general (p. 135); a direct attack on the full balance equations does not close. Detailed balance is a local condition, but the formal statement has to be careful with transitions that do not exist: a move out of an empty colony, a departure that would make a count negative, and the coincidences between operators at the boundary ($T_{jk}n = T_{\cdot k}n$ when $n_j = 0$). In the open case the bookkeeping is in infinite sums: positivity and normalization need convergence of each colony series, and independence needs the marginal of $\pi$ on one colony to be computed as a sum over the remaining $J-1$ coordinates.

Formalization scope

Colonies are Fin J; states are Fin J → ℕ; rates are real-valued functions of two states, assembled as sums of indicator terms over the possible transitions, reusing the operators Tjk, Tout, Tin and the predicates DetailedBalance, FullBalance of the published definitions KellyStochasticNetworks_Migration and KellyStochasticNetworks_Balance. Transitions out of an empty colony carry the factor $\varphi_j(0) = 0$ and so vanish. The hypotheses $\lambda_{jj} = 0$, non-negativity of the rates, positivity of $\varphi_j(n)$ ($n>0$), $\psi_j(n)$ ($n\ge0$) and $\alpha_j$, and the book's irreducibility requirements are binders of each theorem.

The statements are at the level of transition rates: "reversible" is read as detailed balance of the equilibrium distribution, and "equilibrium distribution" as positive, summing to one, and satisfying the equilibrium equations. The stochastic process itself is not constructed. In the closed case the distribution lives on $\mathbb{N}^J$ and vanishes off $\mathcal{S}$, which is equivalent because every transition preserves $\sum_j n_j$; $J \ge 1$ is assumed so that $\mathcal{S}$ is nonempty. In the open case stationarity is the convergence of each colony series, carried as HasSum hypotheses with sums $g_j$.

The normalizing constant is never free: $\pi \equiv 0$ satisfies detailed balance, so a statement that leaves $B$ unconstrained, or omits the factor $\psi_k(n_k)$ from (6.2), (6.6) and (6.3), is not this theorem. Contributions welcome: proofs of Theorem 6.1 and 6.2, reusable lemmas on detailed balance for indicator-sum rates, and on products of summable families over Fin J → ℕ.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979; reprinted Cambridge University Press, 2011. Chapters 2 and 6. http://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• J. F. C. Kingman, Markov population processes, Journal of Applied Probability 6 (1969), 1–18. https://doi.org/10.2307/3212273
• F. P. Kelly, Networks of queues, Advances in Applied Probability 8 (1976), 416–432. https://doi.org/10.2307/1426136
• P. Whittle, Nonlinear migration processes, Bulletin of the International Statistical Institute 42 (1967).
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 2. http://www.statslab.cam.ac.uk/~frank/STOCHNET/

Motivation

Linear programming asks for the best value of a linear objective under linear constraints. In the form studied by George B. Dantzig in 1951, all variables are nonnegative and the constraints are equalities. The simplex technique moves between small sets of columns, seeking a feasible vector first and then improving its objective. Its basic promise is operational: a run should end with a valid answer, whether that answer is a maximum, infeasibility, or an objective that can grow without bound. Dantzig's chapter sets out both phases and the tests that distinguish these outcomes.

The formulation matters to readers of optimization because it separates the algebraic claim about a linear program from a particular rule for selecting the next column. The chapter permits any entering column satisfying the stated improvement test. This mission captures the correctness claim for every sequence of admissible choices under the chapter's nondegeneracy assumption, with one additional general-position condition needed for the Phase I argument.

Setting

Fix integers $1\le m\le n$. Let $P_0\in\mathbb R^m$ be a right-hand side, $P_1,\ldots,P_n\in\mathbb R^m$ be columns, and $c_1,\ldots,c_n\in\mathbb R$ be objective coefficients. A feasible solution is a weight vector $\lambda\in\mathbb R^n$ with $\lambda_j\ge0$ and $\sum_j\lambda_jP_j=P_0$. Its objective value is $z(\lambda)=\sum_j\lambda_jc_j$. It is maximum feasible when $z(\mu)\le z(\lambda)$ for every feasible $\mu$. Unboundedness means that feasible objective values exceed every real threshold.

Dantzig assumes nondegeneracy: every indexed selection of $m$ points among $P_0,P_1,\ldots,P_n$ is linearly independent. A Phase II state uses exactly $m$ basic columns $B$, each with a positive weight, and represents $P_0$ with them. Every column has unique coordinates $P_j=\sum_{i\in B}x_{ij}P_i$, and $z_j=\sum_{i\in B}x_{ij}c_i$ is the corresponding objective value. A column with $c_j>z_j$ can improve the objective. When some $x_{ij}>0$, the step uses the smallest ratio $\lambda_i/x_{ij}$ over those positive coordinates and replaces a minimizing basic column.

A Phase I state begins from $m-1$ basic columns $S$ and a fixed reference point $G$. Positive weights $w_i$ and $\rho>0$ satisfy $G+\rho P_0=\sum_{i\in S}w_iP_i$. Write $P_j=y_{0j}P_0+\sum_{i\in S}y_{ij}P_i$. A column with $y_{0j}>0$ either gives a new Phase I basis through the positive-ratio test or supplies the nonnegative weights in equation (39), which start Phase II.

Formalization targets

The goal is the correctness of the complete two-phase transition system. There is no infinite admissible run. Every state with no outgoing transition has one of three outcomes:

$$\begin{array}{ll} \text{Phase I:}& y_{0j}\le0\ (\forall j),\quad \text{no feasible solution};\\ \text{Phase II:}& \exists j\ (c_j>z_j\ \land\ x_{ij}\le0\ (\forall i\in B)),\quad \forall M\in\mathbb R\ \exists\lambda\text{ feasible}: z(\lambda)>M;\\ \text{Phase II:}& c_j\le z_j\ (\forall j),\quad z(\mu)\le z(\lambda)\text{ for every feasible }\mu. \end{array}$$

The five milestones follow the chapter's own statements: Theorem 3's infeasibility certificate, Section 2's termination and hand-off, Theorem 1's improving family and two cases, Section 1's termination alternatives, and Theorem 2's optimality test. The goal includes the hand-off from the first phase to the second; the milestones make each outcome separately auditable.

Significance

The result gives a complete outcome guarantee for the chapter's procedure under its stated nondegeneracy regime. A terminal basis satisfying $c_j\le z_j$ is certified optimal against every feasible solution, not just against nearby bases. The other terminal tests certify properties of the original problem: nonexistence of feasible weights or arbitrarily large feasible objective values. This is the distinction needed to use the procedure as an algorithm for an LP rather than merely a local improvement rule.

The chapter's Theorems A and B assert existence of a basic feasible solution, and existence of a basic optimal one when the objective is bounded above. A proved platform theorem on basic optimal solutions covers these structural results after changing minimization cost $q$ to $-c$; it is included by reference. Existing simplex results in the platform's minimization convention do not state Dantzig's Phase I reference-point process or his $x_{ij}$ and $z_j$ tests. Formalizing this mission adds that two-phase interface and a machine-checkable statement of its outcomes.

Difficulty

An improving column alone does not say whether another basis exists. In Phase II, the signs of its basis coordinates determine whether the positive weights meet a finite ratio limit or instead continue along an unbounded feasible family. In Phase I, the analogous limit must preserve strictly positive weights on exactly $m-1$ columns. The printed argument says that a coefficient vanishes at the limit, but does not exclude two coefficients vanishing together. That gap matters because the next state in the paper's recurrence must again have strictly positive basic weights. The mission states a general-position condition on $G$ that rules out this simultaneous-vanishing case. It is an explicit addition to the printed assumptions and should be reviewed as such.

Formalization scope

Lean uses Fin n → (Fin m → ℝ) for the columns, Fin m → ℝ for $P_0$ and $G$, Fin n → ℝ for weights and costs, and finite sets for bases. Its zero-based Fin n labels correspond to the paper's $1,\ldots,n$. Each state carries its basis cardinality, independence, coordinate equations, and strictly positive basic weights. This keeps the coordinate functions defined on genuine bases and prevents a zero-weight intermediate state from counting as a valid pivot. The transition relation records every admissible entering column and minimizing leaving index; the pivot-selection heuristics (20) and (21) are outside the claim.

The phrases “upper bound of $z$ is infinite” and “process terminates” are read as, respectively, objective values above every real threshold on the original feasible set and absence of an infinite sequence of admissible steps. “A feasible solution has been obtained” is the explicit vector of equation (39), not an unnamed existence assertion. Maximum feasible means feasible plus comparison with every feasible vector, avoiding a real supremum's empty-set default. The dimensions $1\le m\le n$ make both kinds of basis possible and prevent a vacuous nondegeneracy condition. General position asks every family containing $G$, $P_0$, and $m-2$ distinct $P_j$ to be independent. The paper does not write this condition, so its inclusion is a substantive qualification of the target.

The printed indices in (30), (45), and a sentence following (18) do not match their defining ranges. The Lean statements use all $n$ columns for $j$ and the current $m-1$ Phase I columns for $i$. The indices in (17) and (45) also carry the entering conditions $c_j>z_j$ and $y_{0j}>0$, respectively. These corrections preserve the paper's described procedure and prevent a terminal test from becoming trivial through a basic column. Contributions may address the finite-state termination argument, the ratio-test lemmas, coordinate uniqueness, and the translation from terminal signs to the three global LP outcomes. The operation counts and geometric interpretation on the last pages are outside the formalization.

Selected references

• George B. Dantzig, “Maximization of a Linear Function of Variables Subject to Linear Inequalities,” in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, Chapter XXI, pp. 339–347. Book catalog search.
• Hartmann_Psi, “A bounded feasible standard-form LP attains its minimum at a basic feasible solution,” Prove2Me, proved platform theorem. Theorem record.
• Shuze Chen, “Finite termination of the simplex method under nondegeneracy,” Prove2Me, proved platform theorem in a minimization convention. Theorem record.

Why variance-regularized risk bounds

In statistical learning, one picks a function $f$ from a class $\mathcal F$ to make the population risk $\mathbb E[f]$ small, with access only to an i.i.d. sample $x_1,\dots,x_n$ from an unknown distribution $P$. Empirical risk minimization replaces $\mathbb E[f]$ by the empirical mean $\mathbb E_{\widehat P_n}[f]$, and its classical guarantees decay like $1/\sqrt n$ regardless of how concentrated $f$ is. Bernstein-type inequalities show that the deviation of $\mathbb E_{\widehat P_n}[f]$ from $\mathbb E[f]$ scales with the standard deviation of $f$, so a procedure that minimizes "empirical risk plus a standard-deviation penalty" can, in principle, achieve faster rates when the variance at the optimum is small (Maurer and Pontil, 2009). The penalized objective is non-convex even when every $f$ is convex in its parameters, which makes it hard to optimize.

J. C. Duchi and H. Namkoong (arXiv:1610.02581v3, 2017) replace the penalty by a distributionally robust objective: the worst-case risk over all reweightings of the sample within a $\chi^2$-divergence ball. This objective is convex whenever the losses are, and (Theorem 1 of the paper) it equals the empirical mean plus a standard-deviation penalty up to an error of order $1/n$. This mission formalizes the paper's guarantee for the minimizer of that robust objective in terms of localized Rademacher complexities (Section 3.2, Theorem 4), the sharpest of the paper's three generalization analyses. It is the third of four missions on the paper.

Setting

Let $P$ be a probability measure on a measurable space $\mathcal X$ and $x_1,\dots,x_n$, $n\ge1$, an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$. Let $M\ge1$ and let $\mathcal F$ be a collection of measurable functions $f:\mathcal X\to[0,M]$ (losses).

• The $\chi^2$ ball of radius $\rho\ge0$ is the set $\mathcal P_n$ of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$, $\sum_ip_i=1$ and $\frac12\sum_i(np_i-1)^2\le\rho$; equivalently, the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$.
• The robust risk of $f$ is $\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]=\sup_{p\in\mathcal P_n}\sum_ip_if(x_i)$, and a robust minimizer $\widehat f$ minimizes it over $\mathcal F$.
• The empirical Rademacher complexity is $\mathfrak R_n(\mathcal F)=\mathbb E_\varepsilon\big[\sup_{f\in\mathcal F}\frac1n\sum_i\varepsilon_if(x_i)\big]$ with i.i.d. uniform signs $\varepsilon_i\in\{-1,1\}$, and $\mathbb E[\mathfrak R_n(\mathcal F)]$ averages it over the sample.
• A function $\psi:\mathbb R_+\to\mathbb R_+$ is sub-root if it is nonnegative, nondecreasing, and $r\mapsto\psi(r)/\sqrt r$ is nonincreasing on $r>0$.
• The localization inequality (20) asks that, for all $r\ge0$,

$$\psi_n(r)\ \ge\ \mathbb E\big[\mathfrak R_n(\{cf : f\in\mathcal F,\ c\in[0,1],\ \mathbb E[c^2f^2]\le r\})\big],$$

with $\psi_n$ sub-root, and $r_n^\star>0$ is a point with $r_n^\star\ge\psi_n(r_n^\star)$.

Formalization targets

Goal: Theorem 4, inequality (23), as its proof establishes it

Let $0<t<n$ and let $\rho$ satisfy (21): $\frac\rho n\ge8\big(\frac{45M}n\big(t+\log\lceil\log\frac nt\rceil\big)+18r_n^\star\big)$. With probability at least $1-4e^{-t}$, every robust minimizer $\widehat f$ satisfies

$$\mathbb E[\widehat f]\ \le\ \Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\inf_{f\in\mathcal F}\Big(\mathbb E[f]+\sqrt{\tfrac{182\rho}{45n}\mathrm{Var}(f)}\Big)+\Big(14+6\sqrt{\tfrac{2\rho}n}\Big)\frac{M(3\rho+t)}n .$$

Milestones

In attack order: Bousquet's form of Talagrand's inequality (Lemma B.2); the elementary root bound (Lemma D.4); the contraction principle (Lemma D.5, a published theorem); the uniform Bernstein inequality with Rademacher complexity (Lemma D.1); its localized version in terms of $r_n^\star$ (Lemma D.2); localized second-moment bounds (Lemma D.3); the deterministic expansion (10) of Theorem 1,

$$\Big(\sqrt{\tfrac{2\rho}n s_n^2}-\tfrac{2M\rho}n\Big)_+\le\sup_{P}\mathbb E_P[Z]-\mathbb E_{\widehat P_n}[Z]\le\sqrt{\tfrac{2\rho}ns_n^2};$$

and the uniform bound (22): with probability at least $1-2e^{-t}$, for all $f\in\mathcal F$,

$$\mathbb E[f]\le\Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]+\Big(13+4\sqrt{\tfrac{2\rho}n}\Big)\frac{M\rho}n .$$

Significance

The bound (23) says that the robust minimizer competes with the best trade-off between risk and standard deviation in the class, and that the complexity of the class enters only through the fixed point $r_n^\star$ of a localized complexity bound. For bounded VC classes $r_n^\star$ is of order $\frac{d\log(n/d)}n$ (Bartlett, Bousquet and Mendelson, 2005, Corollary 3.7), so when the optimal function has small variance the excess risk is of order $\rho/n$, faster than the $1/\sqrt n$ of uniform covering arguments; and localized complexities apply to classes, such as balls of reproducing kernel Hilbert spaces, whose covering numbers are too large for the covering-number analysis of the paper's Theorem 3 (mission II of this series).

The paper's result is proved, not open. No part of it, and none of the localized-complexity machinery of Bartlett, Bousquet and Mendelson, is formalized in Lean or Mathlib to our knowledge. The mission produces a checked version of the theorem with every constant explicit and, along the way, the localization lemmas D.1–D.3, which are reusable for any localized-complexity analysis. Reading the proof also exposed three arithmetic slips in the printed statements; the mission states what the proof establishes (see Formalization scope).

Difficulty

The obvious route applies a uniform concentration inequality to $\mathcal F$ and then a Bernstein bound to each $f$. Talagrand's inequality applied to the whole class gives a deviation governed by the largest variance in the class and by the global complexity $\mathbb E[\mathfrak R_n(\mathcal F)]$, which yields only $1/\sqrt n$ rates. Obtaining a deviation that scales with each function's own second moment requires peeling the class into shells of comparable second moment and a fixed-point argument on the sub-root bound, with a union bound whose cost appears as $\log\lceil\log\frac nt\rceil$. The two directions of the localized inequalities (population to sample, and sample to population for second moments) must then be combined with the deterministic expansion (10) while keeping the constants explicit. A further subtlety is the self-normalized rescaling $f\mapsto\sqrt{r/(\mathbb E[f^2]\vee r)}\,f$, which differs from the variance normalization of Bartlett et al. and is what makes the bound compatible with the robust objective.

Formalization scope

Lean conventions. The sample is the coordinate map of the product measure $P^n$ on Fin n → X. Distributions on the sample are weight vectors in the $\chi^2$ ball; the robust risk is the real supremum over that ball (attained, since the ball is nonempty and compact for $n\ge1$, $\rho\ge0$). Population means and variances are ∫ x, f x ∂P and ProbabilityTheory.variance f P for measurable bounded $f$; empirical means and variances are normalized by $1/n$. The empirical Rademacher complexity is the published UnderstandingML_Rademacher definition evaluated on $\{(f(x_1),\dots,f(x_n))\}$. Its expectation is a Bochner integral, and every hypothesis that bounds it also asserts that the integrand is integrable: otherwise the integral is $0$, (20) would hold for free, and the theorem would be false. Probability bounds are stated for the failure event under $P^n$ (an outer measure when the event is not measurable). The goal speaks about every minimizer of the robust risk, so it is not vacuous when the set of minimizers is empty. The condition $r_n^\star>0$ is part of the page's "root" (and the proof divides by $\sqrt{r_n^\star}$); with $r_n^\star=0$ allowed, $\psi(r)=\sqrt r$ would remove the complexity term from (21). The condition $t<n$ makes $\log\lceil\log\frac nt\rceil$ defined.

Corrections of printed statements, each recorded in the item's docstring and Formalization Note (the milestone texts stay verbatim):

• (22) is stated with probability $1-2e^{-t}$; the paper prints $1-e^{-t}$, and its proof (p. 41) concludes $1-2e^{-t}$.
• (23) is stated with probability $1-4e^{-t}$ (printed $1-3e^{-t}$; the proof adds two fixed-$f$ events to the two of (22)) and with $\frac{182\rho}{45n}$ (printed $\frac{91\rho}{45n}$; the proof's step $\sqrt\rho+\sqrt t\le\sqrt{91\rho/45}$ multiplies $\sqrt{2\mathrm{Var}(f)/n}$).
• Lemma D.3 is stated with the additive term $72M^2(1+\eta)r_n^\star+(4(1+\eta)+\frac{14}3)\frac{M^2t}n$ and, in the reversed direction, the coefficient $1+\frac1{1+\eta}$, as its proof yields (printed: $\frac{Mt}n(4+\frac73M)$ and $1+\frac\eta{1+\eta}$), under Theorem 4's standing hypothesis $M\ge1$.
• Lemma D.5 is linked to the published contraction lemma UnderstandingML.contraction_lemma, which states it at a fixed sample for nonempty bounded classes and allows a different Lipschitz map per coordinate.

Contributions welcome: proofs of the milestones in any order; Lemma B.2 (Bousquet's inequality) is the deepest single ingredient and is reusable well beyond this mission, as are the peeling Lemma D.1 and the sub-root fixed-point Lemma D.2.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• M. Ledoux and M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4