Operations Research

Motivation

A retailer that sets both its replenishment quantities and its prices over a finite selling season faces a coupled decision: the price shapes the demand that the inventory must serve, and the inventory position shapes which price is worth charging. With a fixed cost per order, the classical inventory answer is the (s, S) policy of Scarf (1960): when the stock falls below a reorder point $s$, order up to the level $S$. Thomas (1974) asked what happens when the price is also a decision, and conjectured that an (s, S, p) policy — an (s, S) ordering rule together with a price that depends on the stock level — is optimal "under fairly general conditions". He also gave a counterexample when prices are restricted to a discrete set.

Chen and Simchi-Levi (Operations Research 52(6), 2004) settled the conjecture for the finite horizon. When demand is additive in a random shock, $w_t = D_t(p_t) + \beta_t$, the conjecture holds (§3, Theorem 3.1). When the shock is not additive, it fails, and a weaker policy class is optimal (§4, the second mission of this series). This mission formalizes the additive case.

Timeline:

• Scarf (1960): (s, S) policies are optimal for the fixed-cost inventory problem, through k-convexity.
• Thomas (1974): conjectures (s, S, p) optimality with a continuous price range.
• Federgruen and Heching (1999): joint pricing and inventory without a fixed cost; base-stock list-price policies are optimal.
• Polatoglu and Sahin (2000): the lost-sales variant; sufficient conditions for (s, S, p) optimality.
• Chen and Simchi-Levi (2004): (s, S, p) optimality for additive demand with backlogging, and its failure in general.

Setting

There are $T$ periods $t = 1, \dots, T$. In period $t$ the firm starts with inventory $x$, orders up to a level $y \ge x$ at cost $k\,\delta(y - x) + c_t(y - x)$, where $k \ge 0$ is a fixed cost, $c_t$ a unit cost and $\delta(u) = 1$ if $u > 0$ and $0$ otherwise, and sets a price. Demand is $w_t = \alpha_t D_t(p_t) + \beta_t$ for a random pair $\epsilon_t = (\alpha_t, \beta_t)$ with $\mathbb E\alpha_t = 1$, $\mathbb E\beta_t = 0$; in the additive case $\alpha_t = 1$. Unmet demand is backlogged, and an end-of-period inventory $x$ costs $h_t(x)$, a convex function.

Since price and expected demand determine each other, the decision is an expected demand $d \in [\underline d_t, \bar d_t]$, with price $P_t(d) = D_t^{-1}(d)$ and expected revenue $R_t(d) = d\,P_t(d)$, assumed concave. With $G_t(y, d) = \mathbb E\,h_t(y - \alpha_t d - \beta_t)$, the profit-to-go functions satisfy $v_{T+1} \equiv 0$ and, for $t = T, \dots, 1$,

$$v_t(x) = c_t x + \max_{y \ge x}\Big[-k\,\delta(y - x) + g_t\big(y, d_t(y)\big)\Big], \qquad (2)$$ $$g_t(y, d) = R_t(d) - c_t y + \mathbb E\big\{-h_t(y - \alpha_t d - \beta_t) + v_{t+1}(y - \alpha_t d - \beta_t)\big\}, \qquad (3)$$

where $d_t(y)$ maximizes $g_t(y, \cdot)$ over $[\underline d_t, \bar d_t]$. A function $f$ is k-convex if $k + f(z + y) \ge f(y) + \frac{z}{b}\big(f(y) - f(y - b)\big)$ for all $z \ge 0$, $b > 0$, $y$ (Definition 2.1), and k-concave if $-f$ is k-convex. Assumptions 3–5 of the paper give $G_t$ the stated one-sided growth limits and polynomial growth $O(|y|^\rho)$, and give demand a finite $\rho$-th moment.

Formalization targets

Goal: Theorem 3.1(c)–(d)

For additive demand and every period $t$: $g_t(y, \cdot)$ attains its maximum at some $d_t(y)$, the functions $y \mapsto g_t(y, d_t(y))$ and $x \mapsto v_t(x)$ are k-concave, and there exist $s_t \le S_t$ such that

$$y^*(x) = \begin{cases} S_t, & x < s_t,\\ x, & x \ge s_t,\end{cases}$$

maximizes $-k\,\delta(y - x) + g_t(y, d_t(y))$ over $y \ge x$, $v_t(x) = c_t x - k\,\delta(y^*(x) - x) + g_t(y^*(x), d_t(y^*(x)))$, and a best expected demand exists at $y^*(x)$; the price is $D_t^{-1}$ of it.

Milestones

1. Definitions 2.1 and 2.2 of k-convexity are equivalent.
2. Lemma 1(d): a continuous coercive k-convex function has the (s, S) shape (already proved on the platform).
3. Lemma 2: a maximizer $d_t(y)$ can be chosen with $y - d_t(y)$ nondecreasing.
4. Theorem 3.1(a): $g_t(y, d) = O(|y|^\rho)$ and $v_t(x) = O(|x|^\rho)$.
5. Theorem 3.1(b): $g_t$ is continuous, $g_t(y, d) \to -\infty$ as $|y| \to \infty$, and $d_t(y)$ exists.
6. Inequality (7): $g_t(y, d_t(y))$ is k-concave when the continuation value is.
7. The display of $v_t$: its (s, S) form and the transfer of k-concavity from $g_t(y, d_t(y))$ to $v_t$.

Significance

The theorem identifies the structure of an optimal policy for a basic model of coordinated pricing and replenishment: two numbers per period determine the ordering decision, and the price is a function of the post-order stock. It confirms Thomas's conjecture in the additive case and tells a computation or an approximation scheme which policy class it may restrict to; §5 of the paper extends it to a nonincreasing fixed cost, the infinite horizon and Markovian demand.

The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization adds checked versions of the k-convexity toolkit (the equivalence of the two standard definitions; the (s, S) structure lemma), a checked monotone-selection argument for a parametric maximization, and a checked finite-horizon induction in which an expectation, a maximization over a continuous action and a fixed cost interact. The proof of part (a) is omitted in the paper ("similar to that of Theorem 1 in Federgruen and Heching (1999)"), so formalizing it supplies a missing argument.

Difficulty

The obvious argument fails at the expectation. A k-concave function composed with a shift $y \mapsto y - d - \beta$ is k-concave for a fixed $d$, but here the demand decision depends on $y$, and k-concavity, unlike concavity, is not preserved under an arbitrary reparametrization: Definition 2.2 is asymmetric in its two points. The inequality needed for the continuation value requires the post-demand levels $y - d_t(y) - \beta_t$ to be ordered like the inventory levels $y$. That is the content of Lemma 2, and it uses additivity; for multiplicative demand the ordering fails, and so does the theorem (§4).

The second difficulty is analytic: each step of the induction needs a continuous continuation value of polynomial growth, so that the expectation in (3) is finite and continuous, the maximum over $d$ is attained, and $g_t$ is coercive.

Formalization scope

The model is a structure of real data indexed by $t \in \mathbb N$, with periods $1, \dots, T$; the law of $(\alpha_t, \beta_t)$ is a probability measure on $\mathbb R^2$ and expectations are Bochner integrals. The formalization works in expected-demand space $d \in [\underline d_t, \bar d_t]$, equivalent to price space because $D_t$ is a continuous strictly decreasing bijection. Additivity is "$\alpha_t = 1$ almost surely". The profit-to-go is defined by recursion on the number of periods to go, with $v_{T+1} = 0$. Maxima are written as real suprema; every target that uses them asserts that they are attained, so the convention that an unbounded supremum is $0$ never enters. k-convexity is the platform's BertsekasKConvex (Definition 2.1); k-concavity of $f$ is k-convexity of $-f$.

Conventions and restrictions relative to the printed page:

• $O(|y|^\rho)$ is an explicit bound $C(1 + |y|^\rho)$ with $\rho \in \mathbb N$, uniform in $d$.
• Assumption 5, printed $E\{D_t(p, \epsilon_t)\}^\rho < \infty$, is read as $\mathbb E|\alpha_t d + \beta_t|^\rho < \infty$.
• Integrability of $h_t(y - \alpha_t d - \beta_t)$ is part of Assumption 4, and Theorem 3.1(a) also asserts that the expectation of $v_{t+1}$ in (3) is finite.
• Added hypotheses: $c_{T+1} = 0$ (the paper uses $c_{T+1}$ without defining it), $c_t \ge 0$ (used in the proof of part (b); without it $g_t$ need not tend to $-\infty$), and $k \ge 0$.
• Independence across periods is not stated; the dynamic program uses only each period's marginal law.
• The paper writes $s_t < S_t$ in the proof; for $k = 0$ equality is possible, so the targets use $s_t \le S_t$.

A trivializing formalization is ruled out: the targets assert attainment of every maximum they mention and the identity between $v_t(x)$ and the maximized objective, so a supremum that defaults to $0$, or an integral of a non-integrable function, cannot make them hold vacuously; and the assumptions are satisfiable (a one-period instance with $h(x) = |x|$ meets all of them).

A complete development needs: continuity of parametric integrals under polynomial domination; attainment of maxima over compact intervals; Topkis-style monotone selection for functions with increasing differences; the (s, S) structure lemma for k-convex functions (proved on the platform); and the closure of k-concavity under the operations above. The k-convexity results and the monotone-selection lemma are reusable for the general-demand mission of this series and for other fixed-cost inventory models. Contributions to any milestone are welcome, including proofs that rely on platform results by Topkis (Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences).

Selected references

• X. Chen, D. Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. https://doi.org/10.1287/opre.1040.0127
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• L. J. Thomas, Price and Production Decisions with Random Demand, Operations Research 22, 513–518, 1974.
• E. L. Porteus, On the Optimality of Generalized (s, S) Policies, Management Science 17, 411–426, 1971.
• A. Federgruen, A. Heching, Combined Pricing and Inventory Control Under Uncertainty, Operations Research 47(3), 454–475, 1999. https://doi.org/10.1287/opre.47.3.454
• H. Polatoglu, I. Sahin, Optimal Procurement Policies under Price-Dependent Demand, International Journal of Production Economics 65, 141–171, 2000.
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, Athena Scientific, 1995.

Motivation

Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy $\varepsilon$. In fixed dimension $n$ the answer is of order $n\log(1/\varepsilon)$, and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.

Timeline:

• 1960: B. Grünbaum proves that every half-space whose boundary passes through the centroid of a convex body in $\mathbb R^n$ contains at least a fraction $(n/(n+1))^n \ge 1/e$ of its volume.
• 1965: A. Levin and D. J. Newman independently introduce the center of gravity method and prove its linear rate.
• 1983: A. Nemirovski and D. Yudin show that $\Omega(n\log(1/\varepsilon))$ oracle calls are necessary for small $\varepsilon$, so the method's oracle complexity is optimal.

Setting

Let $\mathcal X\subset\mathbb R^n$ be a convex body: a compact convex set with non-empty interior. Let $f:\mathcal X\to[-B,B]$ be continuous and convex, and let $x^*\in\mathcal X$ be a minimizer of $f$ on $\mathcal X$. A vector $w$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le w^\top(x-y)$ for every $y\in\mathcal X$. The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of $f$.

For a set $\mathcal S$ of finite positive volume, its center of gravity is

$$c(\mathcal S)=\frac{1}{\mathrm{vol}(\mathcal S)}\int_{x\in\mathcal S}x\,dx .$$

The center of gravity method sets $\mathcal S_1=\mathcal X$ and, for $t\ge1$, computes $c_t=c(\mathcal S_t)$, queries the first order oracle at $c_t$ to obtain a subgradient $w_t$, and sets

$$\mathcal S_{t+1}=\mathcal S_t\cap\{x\in\mathbb R^n:(x-c_t)^\top w_t\le0\}.$$

After $t$ steps it outputs $x_t\in\operatorname{argmin}_{1\le r\le t}f(c_r)$, found with $t$ calls to the zeroth order oracle.

The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.

Formalization targets

Goal: Theorem 2.1 (p. 245)

For every run of the method and every $t\ge1$,

$$f(x_t)-\min_{x\in\mathcal X}f(x)\le 2B\Big(1-\frac1e\Big)^{t/n}.$$

Milestones (proof of Theorem 2.1, pp. 246–247)

1. Lemma 2.2 (Grünbaum). If $\mathcal K$ is centered, $\int_{\mathcal K}x\,dx=0$, then for every $w\ne0$,

$$\mathrm{Vol}\big(\mathcal K\cap\{x:x^\top w\ge0\}\big)\ge\tfrac1e\,\mathrm{Vol}(\mathcal K).$$

2. (2.2). $\mathcal S_t\setminus\mathcal S_{t+1}\subset\{x\in\mathcal X:(x-c_t)^\top w_t>0\}\subset\{x\in\mathcal X:f(x)>f(c_t)\}$, hence $x^*\in\mathcal S_t$ for every $t$.
3. Volume decay. If $w_s\ne0$ for $s\le t$, then $\mathrm{vol}(\mathcal S_{t+1})\le(1-1/e)^t\,\mathrm{vol}(\mathcal X)$.
4. Shrunk copies. For $\varepsilon\in[0,1]$ and $\mathcal X_\varepsilon=\{(1-\varepsilon)x^*+\varepsilon x: x\in\mathcal X\}$, $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\,\mathrm{vol}(\mathcal X)$.
5. Values on shrunk copies. Every $x_\varepsilon\in\mathcal X_\varepsilon$ satisfies $f(x_\varepsilon)\le f(x^*)+2\varepsilon B$.

Significance

Theorem 2.1 is a linear rate whose number of queries to reach accuracy $\varepsilon$, $O(n\log(2B/\varepsilon))$, depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ($O(n^2\log(1/\varepsilon))$ queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.

On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.

Difficulty

The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to $1/e$ of the volume as $n\to\infty$, so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in $[0,\infty]$ in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with $|f|\le B$, continuity and convexity required on $\mathcal X$ only; its values off $\mathcal X$ are irrelevant. Subgradients are relative to $\mathcal X$ (Definition 1.2). A run is a predicate on sequences indexed from $1$; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer $x^*$ is a hypothesis, as in the book's standing notation; it exists here by compactness. The output $x_t$ is any argmin, so the goal bounds the minimum $\min_{1\le r\le t}f(c_r)$.

Added hypotheses, all disclosed in the statements: $n\ge1$ in the goal, because the exponent $t/n$ is undefined for $n=0$; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is $0$, which would make every unbounded convex set "centered". The milestone on volume decay assumes $w_s\ne0$, which is the book's own reduction.

The center of gravity is defined with the real volume $\mathrm{vol}(\mathcal S)$ and is meaningless when that volume is $0$ or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.

Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §2.1. https://arxiv.org/abs/1405.4980
• B. Grünbaum, Partitions of mass-distributions and of convex bodies by hyperplanes, Pacific Journal of Mathematics 10(4):1257–1261, 1960. https://doi.org/10.2140/pjm.1960.10.1257
• A. Yu. Levin, On an algorithm for the minimization of convex functions, Soviet Mathematics Doklady 6:286–290, 1965.
• D. J. Newman, Location of the maximum on unimodal surfaces, Journal of the ACM 12(3):395–398, 1965. https://doi.org/10.1145/321281.321291
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

Motivation

In robust optimization, a constraint is checked against every parameter value in an uncertainty set. This turns uncertainty into a deterministic optimization problem, but the set must be chosen carefully: a large set can make decisions unnecessarily conservative, while a small one can miss likely outcomes. Bertsimas, Gupta and Kallus use data to calibrate sets through statistical confidence regions. Their question is whether feasibility for every parameter in the set protects a decision against a fresh uncertain outcome with a specified probability. This mission treats the part of their construction based on estimated first and second moments. Bertsimas, Gupta and Kallus, §8.1.

The moment region originates in a concentration result attributed in the paper to Shawe-Taylor and Cristianini. That result bounds the distance between sample and population means and covariances when the uncertain vector is supported in a Euclidean ball. Bertsimas, Gupta and Kallus also discuss replacing those analytic thresholds with bootstrap thresholds; they describe the resulting coverage as approximate. The present target concerns the mathematical relation between a fixed moment region and its uncertainty set, leaving the statistical calibration of the thresholds to its cited source. Shawe-Taylor and Cristianini, 2003; Bertsimas, Gupta and Kallus, pp. 24–25.

Setting

Let the uncertain vector $\tilde u$ take values in $\mathbb R^d$. A probability law $P$ belongs to the moment confidence region $\mathcal P^{CS}$ when it is supported in the Euclidean ball of radius $R$, its mean $m_P$ is within $\Gamma_1$ of an estimate $\hat\mu$, and its covariance $S_P$ is within $\Gamma_2$ of an estimate $\hat\Sigma$ in Frobenius norm. The covariance is $S_P=\mathbb E_P[\tilde u\tilde u^\top]-m_Pm_P^\top$. The thresholds $\Gamma_1,\Gamma_2$ are nonnegative and can be chosen by either calibration procedure discussed in the paper. Bertsimas, Gupta and Kallus, Theorem 9 and (33).

For a vector $v$, Value at Risk $\operatorname{VaR}^{P}_{\varepsilon}(v)$ is the smallest threshold $t$ for which $P(\tilde u^\top v\le t)\ge1-\varepsilon$. The support function of a set $\mathcal U$ is $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$. The authors construct the set

$$\mathcal U^{CS}_{\varepsilon} =\{\hat\mu+y+C^\top w:\|y\|_2\le\Gamma_1,\ \|w\|_2\le\sqrt{1/\varepsilon-1}\}, \qquad C^\top C=\hat\Sigma+\Gamma_2 I.$$

Here $0<\varepsilon<1$ is the allowed violation probability, $I$ is the identity matrix, and $C$ is a matrix factor of the adjusted covariance. The estimates and $C$ stay fixed while $\varepsilon$ varies. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization targets

The first milestone bounds the quantile for every law in the moment region:

$$\operatorname{VaR}^{P}_{\varepsilon}(v)\le \hat\mu^\top v+\Gamma_1\|v\|_2+ \sqrt{\frac{1-\varepsilon}{\varepsilon}} \sqrt{v^\top(\hat\Sigma+\Gamma_2I)v} \quad(P\in\mathcal P^{CS}).$$

The second milestone evaluates the two linear maxima over the Euclidean balls in $\mathcal U^{CS}_{\varepsilon}$ and identifies $\|Cv\|_2$ with the quadratic form above. The goal, the deterministic part of Theorem 10, says the displayed bound equals $\delta^*(v\mid\mathcal U^{CS}_{\varepsilon})$ for every $v$, while the set is nonempty, convex and compact. This gives the support-function criterion of Theorem 1 for each law in the region. A companion formalizes Theorem 13(a): the resulting support constraint is separately convex in $(v,t)$ and in $\varepsilon$ for $0<\varepsilon<3/4$. Bertsimas, Gupta and Kallus, Theorems 10 and 13(a).

Significance

The support formula turns a distributional statement about an entire region of probability laws into a deterministic bound on a linear projection. It gives the robust model an explicit quantity to compare with a constraint threshold. The companion convexity result describes which risk levels allow separate convex optimization in the decision variables and the violation probability. Together they explain why the particular set in (35) is useful beyond the fact that it contains plausible uncertain vectors. Bertsimas, Gupta and Kallus, §§8.1 and 9.

The paper proves the mathematical construction and cites statistical results for the region's coverage. In Lean, the published Value-at-Risk and support-function definitions are already available, while this paper's moment region and set (35) need their own definitions. Formalizing the result therefore establishes a reusable interface between moment bounds, quantiles and set support. The theorem statements in this proposal are open proof targets; compiling them checks their types, not their proofs.

Difficulty

A bound on the mean and covariance does not directly bound a high quantile of every projection. The bound must work simultaneously for every probability law in the moment region, including discrete laws and singular covariances. The factor $\sqrt{(1-\varepsilon)/\varepsilon}$ is essential: replacing it by a standard deviation or a Gaussian quantile would change the claim. On the set side, the ordinary norm of a Lean function vector is a sup norm, whereas both balls in (35) are Euclidean. Getting the norm wrong changes the support function. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization scope

Vectors are functions on Fin d, whose coordinates start at zero. enorm and frob explicitly compute the Euclidean and Frobenius norms. The ball-support condition in $\mathcal P^{CS}$ secures finite first and second moments; no density is assumed. The goal fixes $R\ge0$, $\Gamma_1,\Gamma_2\ge0$, $0<\varepsilon<1$, and $C^\top C=\hat\Sigma+\Gamma_2I$. This factor relation makes the quadratic form nonnegative; a separate positive-semidefinite assumption on $\hat\Sigma$ is unnecessary. The matrix need not be triangular because (35) and its support depend on $C^\top C$. The uncertainty set's nonemptiness and compactness appear in the goal so the real support-function supremum cannot take Lean's default value for an empty or unbounded set.

Theorem 10's sampling claim is represented by its deterministic criterion for each $P\in\mathcal P^{CS}$. The confidence-region coverage of Theorem 9 is cited, and the bootstrap coverage discussed on p. 25 is approximate; neither is asserted as an exact probability theorem here. Equation (34) prints an equality for a supremum over $\mathcal P^{CS}$, yet that region restricts support to a ball, and the page does not establish attainment under that restriction. This mission uses the upper-bound direction needed for Theorem 10 and does not assert the equality or Remark 16's exact equivalence. The scope includes a sharp quantile bound, the exact support formula and the $3/4$ convexity range; a definition that merely makes the claim true by construction would miss these targets. Bertsimas, Gupta and Kallus, pp. 24–25 and 29.

Selected references

• D. Bertsimas, V. Gupta and N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised in Mathematical Programming 167 (2018), 235–292. arXiv preprint.
• J. Shawe-Taylor and N. Cristianini, Estimating the Moments of a Random Vector with Applications, 2003. University of Southampton ePrint.
• G. C. Calafiore and L. El Ghaoui, On Distributionally Robust Chance-Constrained Linear Programs, Journal of Optimization Theory and Applications 130 (2006), 1–22. DOI.

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

$$f(\mathbf u,\mathbf x)\le 0\qquad\forall\,\mathbf u\in\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

$$\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u,\qquad\mathbf v\in\mathbb R^d .$$

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

$$\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\ \mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge 1-\epsilon\}.$$

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

$$f(\mathbf u,\mathbf x^*)\le0\ \ \forall\mathbf u\in\mathcal U\quad\Longrightarrow\quad\mathbb P\big(f(\tilde{\mathbf u},\mathbf x^*)\le0\big)\ge1-\epsilon. \tag{2}$$

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

$$\delta^*(\mathbf v\mid\mathcal U)\ge\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\qquad\forall\,\mathbf v\in\mathbb R^d,$$

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

$$\mathbb P^*\Big(\max_{j=1,\dots,m}f_j(\tilde{\mathbf u},\mathbf x)\le0\Big)\ge1-\bar\epsilon \tag{7}$$

(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

Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision $x$ is fixed before an uncertain parameter is revealed, and a second-stage decision $y(b)$ is chosen after the parameter $b$ is observed, so that the second stage may depend on $b$ arbitrarily. The objective is the worst case over an uncertainty set $\mathcal U$ of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.

Optimizing over all functions $y(\cdot)$ is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in $b$ with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) $y(b)=Pb+q$; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.

Timeline of the relevant results:

• 2004. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduce affinely adjustable robust counterparts and show that the best affine policy is tractable for many uncertainty sets (doi:10.1007/s10107-003-0454-y).
• 2010. Bertsimas, Iancu and Parrilo prove that affine policies are optimal for a class of multistage robust problems with one-dimensional uncertainty per stage and box uncertainty sets (doi:10.1287/moor.1100.0444).
• 2012. Bertsimas and Goyal, the source of this mission, prove that an affine policy is optimal for model (1) whenever $\mathcal U$ is a simplex (Theorem 1), and show that this exactness breaks down for slightly larger sets (doi:10.1007/s10107-011-0444-4).

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$ and $d\in\mathbb R^{n_2}_+$. The problem $\Pi_{Adapt}(\mathcal U)$ of model (1) is

$$z_{Adapt}(\mathcal U)=\min\ c^Tx+\max_{b\in\mathcal U}d^Ty(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U,$$

where inequalities between vectors are componentwise. A pair $(x,y)$ satisfying the constraints is feasible; its worst-case cost is $c^Tx+\max_{b\in\mathcal U}d^Ty(b)$. A feasible pair is optimal when its worst-case cost equals $z_{Adapt}(\mathcal U)$, and an affine policy is a second stage of the form $y(b)=Pb+q$ with $P\in\mathbb R^{n_2\times m}$, $q\in\mathbb R^{n_2}$, still required to be nonnegative on $\mathcal U$. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine policies.

A simplex in $\mathbb R^m$ is the convex hull

$$\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$$

of $m+1$ affinely independent points, that is, points for which $b^1-b^{m+1},\dots,b^m-b^{m+1}$ are linearly independent. The proof works with the $m\times m$ matrix $Q=[(b^1-b^{m+1})\cdots(b^m-b^{m+1})]$, the matrix $Y=[(y^*(b^1)-y^*(b^{m+1}))\cdots(y^*(b^m)-y^*(b^{m+1}))]$ of display (2), and the affine rule $\tilde y(b)=YQ^{-1}(b-b^{m+1})+y^*(b^{m+1})$. In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.

Formalization targets

Goal: Theorem 1

If $\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$ with affinely independent $b^j\in\mathbb R^m_+$ and $\Pi_{Adapt}(\mathcal U)$ is feasible, then there exist $\hat x$, $P\in\mathbb R^{n_2\times m}$ and $q\in\mathbb R^{n_2}$ such that

$$(\hat x,\ \hat y),\qquad \hat y(b)=Pb+q\ \ (b\in\mathcal U),$$

is an optimal solution of $\Pi_{Adapt}(\mathcal U)$, optimal among all (not only affine) two-stage solutions. In particular $z_{Aff}(\mathcal U)=z_{Adapt}(\mathcal U)$.

Milestones

The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:

1. $Q$ is invertible (PDF p. 6).
2. For $b=\sum_j\alpha_jb^j$ with $\sum_j\alpha_j=1$: $Q^{-1}(b-b^{m+1})=(\alpha_1,\dots,\alpha_m)^T$ (PDF p. 6).
3. $\tilde y\big(\sum_j\alpha_jb^j\big)=\sum_j\alpha_j\,y^*(b^j)$ (PDF pp. 6–7).
4. Displays (3)–(5): for any feasible $(x^*,y^*)$, the pair $(x^*,\tilde y)$ is feasible and every bound on the worst-case cost of $(x^*,y^*)$ also bounds that of $(x^*,\tilde y)$ (PDF p. 7).

Significance

The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix $A$ and $B$ and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with $m+3$ extreme points the best affine policy can already be worse by a factor $2-\delta$, and that on sets with exponentially many extreme points the gap can be $\Omega(m^{1/2-\delta})$; Section 6 uses a dominating simplex, on which affine policies are exact, to build an $O(\sqrt m)$-approximation for general $\mathcal U$. The theorem also says that on a simplex the whole adaptive problem reduces to $m+1$ scenario copies of a linear program.

Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.

Difficulty

Two steps are not routine to formalize. First, the paper starts from "an optimal solution $x^*,y^*(b)$", that is, it assumes the minimum in (1) is attained. Over arbitrary functions $y(\cdot)$ this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of $m+1$ points to invertibility of the $m\times m$ matrix $Q$, and the identity $Q^{-1}(b-b^{m+1})=\alpha$ requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing $z_{Aff}$ and $z_{Adapt}$ as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.

Formalization scope

Vectors in $\mathbb R^m$ are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at $1$, Lean's at $0$: $b^j$ is v (j-1) and $b^{m+1}$ is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of $\mathcal U$ is the hypothesis that all $m+1$ vertices are nonnegative (the page writes $j=1,\dots,m$, a slip for $m+1$). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values $z_{Adapt}$ and $z_{Aff}$ are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.

The goal must not be replaced by $z_{Aff}(\mathcal U)\le z_{Adapt}(\mathcal U)$, by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention $Q$, $Y$ or the interpolant.

A complete development needs: linear-programming attainment for a finite system of linear inequalities with a cost bounded below (reusable well beyond this mission), the linear-algebra lemmas relating affine independence to an invertible edge matrix (reusable for barycentric coordinates in general), and the convex-hull representation of points of a simplex. Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2012. doi:10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99(2), 351–376, 2004. doi:10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35(2), 363–394, 2010. doi:10.1287/moor.1100.0444
• A. Bemporad, F. Borrelli, M. Morari, Min–max control of constrained uncertain discrete-time linear systems, IEEE Trans. Autom. Control 48(9), 1600–1606, 2003. doi:10.1109/TAC.2003.816984

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/