Probability

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

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

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/

Why variance-regularized risk bounds

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

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

Setting

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

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

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

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

Formalization targets

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

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

When many self-interested users share resources whose cost grows with use (links of a network, servers, machines), each user picks the option that is cheapest for them given what the others do, and the resulting equilibrium can be worse for the group than a centrally planned allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures this loss as the worst ratio between the social cost of an equilibrium and the optimal social cost. Congestion games (Rosenthal 1973) are the standard finite model of such resource sharing: they always have pure Nash equilibria, and they cover atomic routing, load balancing and many network design questions.

Timeline of the linear-latency case:

• 2002: Roughgarden and Tardos (J. ACM) bound the price of anarchy of nonatomic selfish routing with linear latencies by $4/3$.
• 2005: Awerbuch, Azar and Epstein (STOC 2005) and, independently, Christodoulou and Koutsoupias (STOC 2005) show that for atomic (finite) congestion games with linear latencies the pure price of anarchy of the total cost is $5/2$. Awerbuch, Azar and Epstein also obtain $(3+\sqrt5)/2 \approx 2.618$ for weighted players.
• 2005: Christodoulou and Koutsoupias observe that their argument for $5/2$ extends to mixed Nash equilibria, at the price of the larger constant $(3+\sqrt5)/2$ (their Theorem 14, the goal of this mission).

Setting

A congestion game consists of a finite set $N$ of players, a finite set $E$ of facilities, for each player $i$ a collection $\Sigma_i$ of pure strategies, each a subset of $E$, and for each facility $e$ a latency function $f_e : \mathbb N \to \mathbb R$. In a pure profile $A = (A_1, \dots, A_n)$, $A_i \in \Sigma_i$, the load $n_e(A)$ is the number of players whose set contains $e$, and player $i$ pays

$$c_i(A) = \sum_{e \in A_i} f_e\bigl(n_e(A)\bigr).$$

The social cost of a pure profile is $\mathrm{SUM}(A) = \sum_{i\in N} c_i(A)$ ($N$ times the average cost). Latencies are linear: $f_e(k) = a_e k + b_e$ with $a_e, b_e \ge 0$.

A mixed strategy $p_i$ of player $i$ is a probability distribution on $\Sigma_i$. The players randomize independently, so the pure profile $s$ occurs with probability $\Pr(s) = \prod_j p_j(s_j)$. Player $i$'s expected cost is $\mathbb E[c_i] = \sum_s \Pr(s)\, c_i(s)$, and the expected load of $e$ is $\mathbb E[n_e] = \sum_s \Pr(s)\, n_e(s)$. A mixed profile is a mixed Nash equilibrium if no player can lower their expected cost by switching unilaterally to another distribution on their strategies. The social cost of a mixed profile is the sum of the expected costs, $\mathrm{SUM}(p) = \sum_i \mathbb E[c_i]$.

In Lean: CongestionGame ι E with fields strategies and latency, load, cost, IsProfile, sumCost, IsLinear, expCost, expLoad, mixedSumCost and IsMixedNash, all in the namespace CongestionPoA.Mixed; lotteries and independent randomization come from the platform definition agt_games (AGT.IsLottery, AGT.profileProb, AGT.IsMixedNash).

Formalization targets

Goal: Theorem 14

For every congestion game with linear latencies, every mixed Nash equilibrium $p$ and every pure profile $P$ with $P_i \in \Sigma_i$,

$$\sum_{i\in N} \mathbb E[c_i] \;\le\; \frac{3+\sqrt5}{2}\,\mathrm{SUM}(P).$$

Taking $P$ optimal, the mixed price of anarchy of the average social cost is at most $(3+\sqrt5)/2$.

Milestones

1. Lemma 3 (corrected). For real $x \ge 0$ and integer $y \ge 0$, $y(x+1) \le \frac{\sqrt5-1}{4}x^2 + \frac{\sqrt5+5}{4}y^2$.
2. Deviation inequality (Theorem 1's proof, mixed). At a mixed Nash equilibrium, for every player $i$,

$$\mathbb E[c_i] \le \sum_{e\in P_i}\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).$$

3. Summing step (Theorem 1's proof, mixed).

$$\sum_i \mathbb E[c_i] \le \sum_{e\in E} n_e(P)\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).$$

Significance

The bound says that randomization by the players cannot make linear congestion games much worse than pure play: the loss stays within a constant factor independent of the number of players and facilities. Mixed equilibria matter because they always exist in every finite game and because they model populations of users whose individual choices are not known in advance. The same authors report (PDF p. 2) extending these bounds to correlated equilibria with the same values, which places the mixed bound in a hierarchy of equilibrium notions whose worst cases coincide.

The result is proved in the paper, in one sentence that defers to the proof of Theorem 1. The work here is a complete machine-checked version: the expected-cost layer for congestion games on top of agt_games, the deviation and summing inequalities under product distributions, and the corrected Lemma 3. The paper prints Lemma 3 for all nonnegative reals $x, y$, where it is false (at $x = 0$, $y = 1/10$ the left side is $0.1$ and the right side about $0.018$); the formal statement keeps $y$ an integer, which is how the lemma is used. No formalization of congestion-game price-of-anarchy bounds was on the platform when this mission was drafted.

Difficulty

The pure proof compares $n_e(P)(n_e(A)+1)$ with $n_e(A)^2$ and $n_e(P)^2$ through an integer inequality (Lemma 1). Under a mixed equilibrium the equilibrium side is an expectation, so the cost of a facility is no longer a function of one integer load, and Lemma 1's constant $1/3$ is not available for real arguments: a real-variable version is needed, and the constant degrades from $5/2$ to $(3+\sqrt5)/2$. A second obstacle is bookkeeping: the deviating player's load changes only on their own deviation, while the other players' randomization stays independent, and the expected cost of a player has to be related to expected facility loads, which uses linearity of the latencies in an essential way. The naive idea of applying Theorem 1 to each pure profile in the support of the equilibrium fails, because those profiles are not themselves Nash equilibria.

Formalization scope

Players and facilities are finite types ι and E; profiles are functions ι → Finset E, with feasibility IsProfile a separate predicate. Latencies are real-valued on natural-number loads, and "linear" means affine with nonnegative coefficients, $f_e(k) = a_e k + b_e$; the paper displays only the identity latency $f_e(k)=k$ and states that its proofs extend. Mixed strategies are real weight functions on the finite strategy type $\Sigma_i$; independence is built into AGT.profileProb; Nash deviations range over all lotteries, which is equivalent to pure deviations. agt_games maximizes payoffs, so the game is passed to it with payoff $-c_i$. The goal is stated against every feasible pure profile rather than as a ratio, so no division by an optimum that may be $0$ occurs. The social cost is the expected sum of the players' costs; the paper's second option, $\sum_e \mathbb E[n_e^2]$, is not part of this mission. A version with correlated distributions on profiles, or one that bounds the cost of an "averaged" profile instead of the expected cost, is a different statement and does not discharge the goal.

A complete development needs elementary finite-sum manipulation of product distributions (marginals of AGT.profileProb, expectations of loads), and a Jensen-type inequality $(\mathbb E[n_e])^2 \le \mathbb E[n_e^2]$ for finite distributions. The expectation lemmas for congestion games are reusable for the other mixed results of the literature (weighted games, polynomial latencies). Proofs of the milestones, of the expectation layer, and alternative arguments are all welcome.

Selected references

• G. Christodoulou, E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, STOC 2005, pp. 67–73. https://doi.org/10.1145/1060590.1060600
• B. Awerbuch, Y. Azar, A. Epstein, The Price of Routing Unsplittable Flow, STOC 2005, pp. 57–66. https://doi.org/10.1145/1060590.1060599
• E. Koutsoupias, C. Papadimitriou, Worst-case Equilibria, STACS 1999, LNCS 1563, pp. 404–413. https://doi.org/10.1007/3-540-49116-3_38
• R. W. Rosenthal, A Class of Games Possessing Pure-Strategy Nash Equilibria, International Journal of Game Theory 2 (1973), pp. 65–67. https://doi.org/10.1007/BF01737559
• T. Roughgarden, É. Tardos, How Bad Is Selfish Routing?, Journal of the ACM 49 (2002), pp. 236–259. https://doi.org/10.1145/506147.506153