Operations Research

Motivation

The ellipsoid method is the cutting-plane algorithm that settled the polynomial-time solvability of linear programming and, more generally, of convex optimization over any set that comes with an efficient separation oracle. It was introduced for convex minimization by Shor and by Yudin and Nemirovski in the 1970s, and Khachiyan used it in 1979 to give the first polynomial-time algorithm for linear programming. Grötschel, Lovász and Schrijver later turned it into the general equivalence between separation and optimization that underlies much of combinatorial optimization.

This mission is the second of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). Its goal is the convergence guarantee of the ellipsoid method, Theorem 2.4 (p. 250), together with the geometric lemma and the steps of the proof on which it rests.

Timeline:

• 1976–1977: Yudin–Nemirovski and Shor introduce the method for convex minimization.
• 1979: Khachiyan applies it to linear programming and obtains polynomial time.
• 1981: Grötschel, Lovász and Schrijver derive the equivalence of separation and optimization.

Setting

Write $\mathbb R^n$ for the space of real $n$-vectors, with the dot product $x^\top y$. An ellipsoid is a set

where $c\in\mathbb R^n$ is its center and $H$ is a symmetric positive definite matrix.

A convex body $\mathcal X\subset\mathbb R^n$ is a compact convex set with non-empty interior. The objective $f$ is continuous and convex on $\mathcal X$ with values in $[-B,B]$, and $r,R>0$ are such that $\mathcal X$ lies in the Euclidean ball $\mathcal E_0$ of center $c_0$ and radius $R$ and contains some Euclidean ball of radius $r$. A subgradient of $f$ at $x\in\mathcal X$ is a vector $g$ with $f(x)+g^\top(y-x)\le f(y)$ for all $y\in\mathcal X$.

The method starts from $\mathcal E_0$, $H_0=R^2\mathrm I_n$. At step $t\ge0$ it asks for a vector $w_t$:

• if $c_t\notin\mathcal X$, a separating vector, with $\mathcal X\subset\{x:(x-c_t)^\top w_t\le0\}$;
• otherwise a subgradient of $f$ at $c_t$.

It then replaces $\mathcal E_t$ by the ellipsoid $\mathcal E_{t+1}$ given by

After $t$ iterations the output $x_t$ is the best of the queried centers that lie in $\mathcal X$.

Formalization targets

Goal: Theorem 2.4

For $n\ge2$ and every $t\ge 2n^2\log(R/r)$, $t\ge1$, some queried center lies in $\mathcal X$, and every output satisfies

Milestones

1. The scalar inequality $(1+1/n)^2(1-1/n^2)^{n-1}\ge\exp(1/n)$ for $n\ge2$ (proof of Lemma 2.3, pp. 248–249).
2. Lemma 2.3 (p. 247): for $w\ne0$ the half-ellipsoid $\{x\in\mathcal E_0:w^\top(x-c_0)\le0\}$ lies in an ellipsoid $\mathcal E$ with

and for $n\ge2$ the explicit ellipsoid (2.5)–(2.6) works. 3. The remark before Theorem 2.4 (p. 250): a point of $\mathcal X$ can leave the current ellipsoid only at a step with $c_t\in\mathcal X$, and then its value exceeds $f(c_t)$. 4. Two steps reused from Theorem 2.1 (pp. 246–247): $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\mathrm{vol}(\mathcal X)$ for $\mathcal X_\varepsilon=(1-\varepsilon)x^*+\varepsilon\mathcal X$, and $f\le f(x^*)+2\varepsilon B$ on $\mathcal X_\varepsilon$.

Significance

Theorem 2.4 bounds the oracle complexity of the ellipsoid method: accuracy $\varepsilon$ needs $O(n^2\log(1/\varepsilon))$ oracle calls. Each step costs $O(n^2)$ arithmetic operations plus one oracle call. With the separation oracles of linear and semidefinite programs this gives polynomial overall complexity (p. 250). The rate depends on the instance only through $\log(R/r)$ and $B$, so the method needs no smoothness and no strong convexity. Lemma 2.3 is also the geometric step of the ellipsoid method for linear feasibility.

The result has a textbook proof. The work of this mission is to formalize it. The same update is published on the platform from Bertsimas and Tsitsiklis's Introduction to Linear Optimization (Theorem 8.1), with a proved volume factor of $\exp(-1/(2(n+1)))$. That factor is weaker than (2.4)'s $\exp(-1/(2n))$ and does not give Theorem 2.4's constant. The sharper factor and the optimization version of the method (subgradient cuts, the output rule and the value bound) are not formalized on the platform.

Difficulty

There are two difficulties: Lemma 2.3 with the sharp constant, and the bookkeeping that turns per-step volume decrease into a value bound.

For the lemma, the volume of the explicit ellipsoid is $\big(n/\sqrt{n^2-1}\big)^n\sqrt{(n-1)/(n+1)}$ times that of $\mathcal E_0$. Bounding it by $\exp(-1/(2n))$ rather than by the cruder $\exp(-1/(2(n+1)))$ needs the scalar inequality of milestone 1 for every $n\ge2$. The reduction from a general ellipsoid to the unit ball also needs determinants under an affine map.

For the theorem, the obvious argument compares $\mathrm{vol}(\mathcal X_\varepsilon)$ with $\mathrm{vol}(\mathcal E_t)$. This only works if no cut removes an optimal point and if every removed point of $\mathcal X$ is worse than a queried center. At the threshold $t=2n^2\log(R/r)$ the admissible $\varepsilon$ is exactly $1$, so a non-strict volume bound alone does not close the argument there.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ with Lebesgue measure, as in the reused Bertsimas–Tsitsiklis ellipsoid definitions (LinearOptimization.ellipsoid, ellipsoidUpdateCenter, ellipsoidUpdateMatrix, IsSubgradientOn).
• Euclidean balls are written with the dot product, because Mathlib's norm on Fin n → ℝ is the sup norm.
• The method is a run predicate, IsEllipsoidRun. Every theorem holds for every admissible oracle answer. The update is the published one with $a=-w_t$.
• If an oracle answer is $w_t=0$ (possible only at a minimizer $c_t\in\mathcal X$), the run stops. The page's update would divide by zero there.

Conventions and hypotheses added to the page:

1. $n\ge2$, because the update (2.6) is defined only for $n\ge2$.
2. A minimizer $x^*$ exists (the book's standing assumption, p. 242).
3. The output ranges over the queried centers $c_0,\dots,c_{t-1}$. The page writes $\{c_1,\dots,c_t\}$, but $c_t$ has not been cut yet and $c_0$ has.
4. $t\ge1$, because at $R=r$ and $t=0$ no center has been queried.

A run predicate whose separation branch does not require $\mathcal X\subset\{x:(x-c_t)^\top w_t\le0\}$, or that accepts $w_t=0$ with an update, would make the statements false or vacuous. Both are excluded.

Lemma 2.3's volume factor is $\exp(-1/(2n))$. The weaker published factor does not prove that milestone. The published theorem LinearOptimization.ellipsoid_update_halfspace_volume is included as a reference: it supplies the containment (2.3) and positive definiteness. Contributions are welcome on every milestone. A determinant formula for the volume of an ellipsoid would be reusable well beyond this mission.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
• N. Z. Shor, Cut-off method with space extension in convex programming problems, Cybernetics 13:94–96, 1977. doi:10.1007/BF01071394
• D. B. Yudin and A. S. Nemirovski, Informational complexity and efficient methods for the solution of convex extremal problems, Matekon 13(2):22–45, 1976.
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20:191–194, 1979.
• M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1:169–197, 1981. doi:10.1007/BF02579273
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 8.1).

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$, whose parameter $\tilde{\mathbf u}\in\mathbb R^d$ is random, by the requirement that the constraint hold for every $\mathbf u$ in a chosen uncertainty set $\mathcal U$:

The resulting problem is deterministic and, for many shapes of $\mathcal U$, tractable (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009). The modelling question it leaves open is how to choose $\mathcal U$. A set that is too large makes every solution conservative; a set that is too small gives no protection. The practitioner's real requirement is usually probabilistic: a robust feasible $\mathbf x$ should violate the uncertain constraint with probability at most $\epsilon$.

Bertsimas, Gupta and Kallus (Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167, 2018) build uncertainty sets directly from data so that this requirement holds with high confidence. Their whole construction rests on one characterization, Theorem 1 of the paper, of when a set carries such a guarantee. This mission formalizes that characterization and the two results (Theorems 2 and 3) that turn it into a data-driven recipe.

Earlier work used the "if" direction of the characterization for bi-affine constraints when designing sets for specific distributional assumptions (Ben-Tal et al., 2009; Chen, Sim and Sun, Oper. Res. 55, 2007). The extension to every constraint concave in $\mathbf u$ is due to Bertsimas, Gupta and Kallus.

Setting

Let $\mathbb P$ be a probability measure on $\mathbb R^d$, the law of $\tilde{\mathbf u}$, and fix a level $0<\epsilon<1$. Throughout, $f(\mathbf u,\mathbf x)$ is concave in $\mathbf u$ for every value of the decision variable $\mathbf x\in\mathbb R^k$.

The support function of a set $\mathcal U\subseteq\mathbb R^d$ is

The Value at Risk of the linear loss $\tilde{\mathbf u}^T\mathbf v$ at level $\epsilon$ is

A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P$ (property (P2) of the paper) if for every $k$, every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ for each $\mathbf x\in\mathbb R^k$, and every $\mathbf x^*\in\mathbb R^k$,

A function is bi-affine if it has the form $f(\mathbf u,\mathbf x)=\mathbf u^TF\mathbf x+\mathbf f_u^T\mathbf u+\mathbf f_x^T\mathbf x+f_0$.

In the data-driven setting, $\mathbb P^*$ is unknown and a sample $\mathcal S=(\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N)$ is drawn i.i.d. from it. The paper's schema fixes $0<\alpha<1$, takes the confidence region $\mathcal P(\mathcal S)$ of a hypothesis test at level $\alpha$, and builds a closed convex set $\mathcal U(\mathcal S)$ whose support function bounds $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)$ for every $\mathbb P\in\mathcal P(\mathcal S)$ and every $\mathbf v$.

Formalization targets

Goal: Theorem 1

(a) If $\mathcal U$ is nonempty, convex and compact and

then $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P$.

(b) If $\mathcal U$ is nonempty and $\delta^*(\mathbf v\mid\mathcal U)<\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)$ for some $\mathbf v$ at which $\delta^*(\mathbf v\mid\mathcal U)$ is finite, then some bi-affine $f$ violates (2).

Milestones toward the goal

The proof in the electronic companion (EC.1.1) is a short chain, and its steps are the milestones: the attainment property of VaR, $\mathbb P(\tilde{\mathbf u}^T\mathbf v>\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v))\le\epsilon$ (already proved on the platform); a strict separating hyperplane between $\mathcal U$ and the superlevel set $\{f(\cdot,\mathbf x^*)\ge t\}$; the bound $\mathbb P(f(\tilde{\mathbf u},\mathbf x^*)\ge t)\le\epsilon$ for $t>0$; its limit $\mathbb P(f(\tilde{\mathbf u},\mathbf x^*)>0)\le\epsilon$; and, for part (b), the witness $f(\mathbf u,x)=\mathbf v^T\mathbf u-x$ at $x^*=\delta^*(\mathbf v\mid\mathcal U)$.

Companions: Theorems 2 and 3

Theorem 2: with probability at least $1-\alpha$ over the sample, $\mathcal U(\mathcal S)$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$. Theorem 3: if the region does not depend on $\epsilon$, then with probability at least $1-\alpha$ the whole family $\{\mathcal U(\mathcal S,\epsilon):0<\epsilon<1\}$ implies the guarantee simultaneously (a), and every $\mathbf x$ satisfying the level-optimized constraints (9) satisfies the joint chance constraint

(b).

Significance

Theorem 1(a) is what certifies every uncertainty set in the paper: the $\chi^2$ and $G$ sets for discrete distributions, the Kolmogorov–Smirnov and forward–backward sets for independent marginals, the marginal-sample box and the moment sets. Each construction reduces to proving one inequality between a support function and a Value at Risk, which is a statement about a single linear functional, and Theorem 1(a) lifts it to every concave constraint at once. Part (b) shows the condition cannot be dropped even for bi-affine constraints. Theorems 2 and 3 separate the statistical input (coverage of a confidence region) from the convex-analytic input (the support-function bound), and Theorem 3(b) is what allows the levels $\epsilon_j$ of a system of constraints to be optimized after seeing the data.

The results are proved in the paper. None of them has a machine-checked proof; the only formalized ingredient is the attainment property of VaR, which is on the platform as a proved theorem. The formalization provides a checked bridge from support-function bounds to probabilistic guarantees that the other missions of this series (II–VI) use to state their own results in the criterion form $\mathrm{VaR}\le\delta^*$.

Difficulty

The informal argument is short; the difficulty is in the infinite-dimensional bookkeeping that the page leaves implicit. The superlevel set $\{f(\cdot,\mathbf x^*)\ge t\}$ need not be bounded, so the strict separation must use compactness of $\mathcal U$ alone. Closedness of this set and measurability of $\{f(\tilde{\mathbf u},\mathbf x^*)\le0\}$ depend on concave functions on $\mathbb R^d$ being continuous. The passage $t\downarrow0$ is continuity of a measure along an increasing union. The attainment of the infimum in the definition of VaR requires right-continuity of distribution functions. A naive attempt to separate $\mathcal U$ from the zero superlevel set $\{f\ge0\}$ directly fails, because the two sets may touch.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ; $\tilde{\mathbf u}$ is the identity map; $\mathbf v^T\mathbf u$ is the dot product u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$, and the support function is the published RobustMDP.Shared.supportFunction. Both are real-valued sInf/sSup, which return $0$ on empty or unbounded sets, so every statement assumes $0<\epsilon<1$, a probability measure, and an uncertainty set that is nonempty and compact (Theorem 1(a), Theorems 2–3) or nonempty with $\{\mathbf v^T\mathbf u:\mathbf u\in\mathcal U\}$ bounded above in the direction considered (Theorem 1(b)). In Theorem 1(b) and its witness this is the paper's own requirement that $\delta^*(\mathbf v\mid\mathcal U)$ be finite, which its strict inequality with a real VaR forces and its proof uses by treating $\delta^*(\mathbf v\mid\mathcal U)$ as a real number. Part (b) is printed with $\mathcal U^*$, a slip for $\mathcal U$; the proof's separation step prints both inequalities in the same direction, a slip corrected in the strict separation milestone.

Property (P2) quantifies over the dimension $k$ of the decision variable, every function concave in $\mathbf u$ for each $\mathbf x$, and every $\mathbf x^*$. Restricting it to affine $f$ or to $k=0$ would trivialize part (a) and falsify part (b), and is ruled out by the definition.

In Theorems 2 and 3 the sample is Fin N → (Fin d → ℝ) with the product law Measure.pi; the confidence region and the uncertainty set are arbitrary maps of the sample, and the coverage $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P(\mathcal S))\ge1-\alpha$ is a hypothesis, never the conclusion's event. Step 2 of the schema is stated with $g=\delta^*(\cdot\mid\mathcal U(\mathcal S))$ directly. The sets are assumed nonempty and compact (Step 3 says closed and convex; a finite support function that bounds VaR forces nonemptiness and boundedness). Theorem 3(b) reads the levels $\epsilon_j$ in $(0,1)$, where the family is defined. Probabilities of events in the sample space are outer measures, so no measurability hypotheses are needed.

A complete development needs strict separation of a compact convex set from a closed convex set (Mathlib's geometric_hahn_banach_compact_closed), continuity of concave functions on finite-dimensional spaces, and the attainment property of VaR. Contributions are welcome on all milestones; the separation and limit steps are reusable for any chance-constraint argument based on support functions.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Mathematical Programming 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

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

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

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

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$,

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$,

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

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

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

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$,

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

then the open clustering process has equilibrium distribution

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

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