Operations Research

Motivation

Linear decision rules are a standard device for making multistage optimization under uncertainty computationally tractable: a recourse decision is restricted to be an affine function of the uncertain data observed so far. Their weakness is that a recourse variable that must stay nonnegative forces the rule to be very conservative. Goh and Sim, Distributionally Robust Optimization and Its Tractable Approximations (Operations Research, 2010), repair this with deflected linear decision rules, in which the violated part of an affine rule is corrected and paid for. The cost of the correction is the expected positive part $\mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ of an affine function of the uncertainty.

The distribution $\mathbb P$ is not known. The paper assumes only partial distributional information (a support set, a set containing the mean, a covariance, directional deviations) and bounds the worst case of this expectation over every distribution consistent with that information. Such worst-case bounds go back to Scarf's 1958 mean–variance newsvendor bound and form the core of distributionally robust optimization. This mission formalizes the first bound of §5, which uses support and mean information only.

Setting

Let $\tilde\zeta$ be a random vector in $\mathbb R^{n}$ (in the paper, the segregated uncertainty vector of dimension $n = N_E$). Two sets describe what is known about it:

• a support set $\mathcal V \subseteq \mathbb R^n$ with $\mathbb P(\tilde\zeta \in \mathcal V) = 1$;
• a mean set $\widehat{\mathcal V} \subseteq \mathbb R^n$ containing the mean $\hat\zeta = \mathbb E_{\mathbb P}(\tilde\zeta)$. A known mean is the case where $\widehat{\mathcal V}$ is a single point.

The family of distributions consistent with this information is

$$\mathbb F_1 = \{\mathbb P : \hat\zeta = \mathbb E_{\mathbb P}(\tilde\zeta) \in \widehat{\mathcal V},\ \mathbb P(\tilde\zeta \in \mathcal V) = 1\}.$$

For data $r^0 \in \mathbb R$ and $r \in \mathbb R^n$ the worst-case value is $\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$, with $x^+ = \max\{x, 0\}$. The paper's candidate for this value is the deterministic quantity of (21),

$$\pi^1(r^0, r) = \inf_{s \in \mathbb R^{n}} \Phi(s), \qquad \Phi(s) = \sup_{\hat\zeta \in \widehat{\mathcal V}} \{s'\hat\zeta\} + \sup_{\zeta \in \mathcal V} \max\{r^0 + r'\zeta - s'\zeta,\ -s'\zeta\}.$$

Both quantities live in the extended reals: following the paper (p. 909), an infeasible maximization has value $-\infty$ and an infeasible minimization $+\infty$.

Formalization targets

Goal: Theorem 1 (p. 909)

For closed convex $\mathcal V, \widehat{\mathcal V}$ with $\widehat{\mathcal V} \cap \operatorname{int} \mathcal V \neq \emptyset$, and all $r^0, r$,

$$\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big) = \pi^1(r^0, r).$$

Milestones

1. Upper-bound part of Theorem 1. $\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+) \le \pi^1(r^0, r)$, for arbitrary sets $\mathcal V, \widehat{\mathcal V}$.
2. Remark after Theorem 1, first case (p. 910). If $\widehat{\mathcal V} \subseteq \mathcal V$ is nonempty and $r^0 + r'\zeta \ge 0$ on $\mathcal V$, then the worst-case value equals $r^0 + \sup_{\hat\zeta \in \widehat{\mathcal V}} r'\hat\zeta$, and $\Phi(r) = \pi^1(r^0, r)$.
3. Remark after Theorem 1, second case (p. 910). If $\widehat{\mathcal V} \subseteq \mathcal V$ is nonempty and $r^0 + r'\zeta \le 0$ on $\mathcal V$, then the worst-case value is $0$, and $\Phi(0) = \pi^1(r^0, r) = 0$.
4. Tightness part of Theorem 1. Under the goal's hypotheses, $\pi^1(r^0, r) \le \sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$.

Significance

The result itself. Theorem 1 converts an optimization over an infinite-dimensional set of probability measures into a finite-dimensional convex program over the given sets. When $\mathcal V$ and $\widehat{\mathcal V}$ are representable by linear and second-order cone constraints, the epigraph of $\pi^1$ is a pair of robust constraints over those sets and is again tractable (Remark, p. 910). The bound is tight, so no better bound can be built from support and mean information alone. In the paper, $\pi^1$ is one of three building blocks; their infimal convolution (Theorem 4) prices the deflection in the deflected linear decision rules of §6, and the experiments there compare these rules against plain linear decision rules.

Formalizing it. The proof of Theorem 1 is in the paper's online appendix, not in the main text. A search of the Prove2Me library (October 2026) found no formal statement of this or any other mean-and-support bound. A formal proof has to settle the extended-real bookkeeping (empty families, unbounded suprema) and the exact hypotheses under which tightness holds. As printed, the theorem omits a condition: with no constraint qualification it fails when $\mathbb F_1$ is empty, which can happen for disjoint closed convex sets. This mission states the corrected version.

Difficulty

The upper-bound part is weak duality and needs no structure on the sets. The difficulty is tightness. It amounts to a strong-duality statement between the worst case over distributions and the infimum over the multiplier $s$, and strong duality for convex problems over unbounded sets needs a constraint qualification. Two obvious approaches fail. The first is to search for a single worst-case distribution: for unbounded $\mathcal V$ the supremum over $\mathbb F_1$ is generally not attained, and it may be $+\infty$. The second is to restrict to compact $\mathcal V$, which excludes the paper's main use, a segregation of an unbounded support such as $(-\infty, -1] \cup [-1, 1] \cup [1, \infty)$. Mathlib has separating-hyperplane theorems but no Fenchel duality theorem, so this duality has to be built.

Formalization scope

• A distribution is a measure $P$ on Fin n → ℝ with IsProbabilityMeasure P, and the random vector is the identity map. Every coordinate is required to be $P$-integrable, so the mean is a genuine expectation; the mean is MomentDRO.Conf.meanVec from the published definition MomentDRO_Conf_Setting.
• $\mathbb P(\tilde\zeta \in \mathcal V) = 1$ is the almost-everywhere statement ∀ᵐ ζ ∂P, ζ ∈ V, which needs no measurability of $\mathcal V$.
• The positive part is max (r0 + r ⬝ᵥ ζ) 0.
• The worst-case value, both suprema and the infimum in (21) are taken in EReal. An empty supremum is $-\infty$, an empty infimum $+\infty$, and an unbounded supremum $+\infty$. The paper's "inf" is ⨅; attainment is claimed only where the Remark claims it, via the objective $\Phi$ (pi1Obj) at $s = r$ and $s = 0$.
• The paper's tractable conic representable sets are modelled as closed and convex sets. The goal and its tightness part also assume $\widehat{\mathcal V} \cap \operatorname{int}\mathcal V \ne \emptyset$. This condition is not on the page; it is consistent with the paper's full-dimensionality assumptions (pp. 905–906), and it implies $\mathbb F_1 \neq \emptyset$.
• The Remark's two cases assume $\widehat{\mathcal V} \subseteq \mathcal V$ and $\widehat{\mathcal V} \ne \emptyset$. The paper's construction of $\mathcal V, \widehat{\mathcal V}$ from one set $\mathcal H$ (§4.5) gives the inclusion, and without it the first case is false.
• The segregation map, the matrices $F$, $g$ and the set $\mathcal H$ of §4 are context only and are not formalized: the theorem is stated for an arbitrary random vector with the listed properties.
• A real-valued supremum, a family without integrability (for which the mean would be a junk value), or a $\pi^1$ defined through the worst case would each trivialize the statement; the definitions avoid all three, and $\pi^1$ is defined directly from the sets.

Needed infrastructure: finite mixtures of Dirac masses as members of $\mathbb F_1$, integration of almost-surely bounded functions, separation of convex sets in $\mathbb R^n$, and a Fenchel-type duality for a concave function over a closed convex set under an interior-point condition. The duality and the concave-envelope facts are reusable well beyond this mission, including for Theorems 2–4 of the same paper. Proofs of any milestone, and reusable lemmas on extended-real suprema of integrals, are welcome.

Selected references

• J. Goh and M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4, Part 1 of 2):902–917, 2010. https://doi.org/10.1287/opre.1090.0795
• H. Scarf, A Min–Max Solution of an Inventory Problem, in K. Arrow, ed., Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958, 201–209.
• W. Chen and M. Sim, Goal-Driven Optimization, Operations Research 57(2):342–357, 2009 (cited by the paper for the infimal convolution of bounds).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorem 31.1, Fenchel duality). https://doi.org/10.1515/9781400873173

Motivation

Scheduling jobs on identical parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$, the problem $P\,|\,|\sum w_jC_j$, is one of the basic NP-hard problems of machine scheduling. On a single machine it is solved by Smith's ratio rule (Smith 1956); with several machines the only hard decision is which jobs share a machine. Section 6 of M. Skutella's paper Convex quadratic and semidefinite programming relaxations in scheduling (J. ACM 48 (2001)) observes that this decision is a graph partitioning problem: the cost of a schedule is, up to a constant, the weight of the edges that a partition of a weighted complete graph does not cut. Minimizing $\sum_j w_jC_j$ on $m$ machines is therefore equivalent to Max-$m$-Cut on that graph, and the paper shows that the equivalence preserves approximation in a quantified way.

The reduction explains, from the graph side, why semidefinite rounding works for two machines: with the 0.878-approximation for MaxCut of Goemans and Williamson (1995) it gives a 1.122-approximation for $P2\,|\,|\sum w_jC_j$ (Corollary 6.2 of the paper). For general $m$, the uniform random partition is both a $(1-1/m)$-approximation for Max-$m$-Cut and randomized rounding of the optimum of the convex quadratic relaxation (CQP).

Setting

There are $n$ jobs $J=\{1,\dots,n\}$ and $m\ge 1$ identical machines. Job $j$ has a processing time $p_j>0$ and a weight $w_j\ge 0$. Smith's order $\prec$ puts $j\prec k$ when $w_j/p_j>w_k/p_k$, ties broken by index. An assignment $\sigma:J\to\{1,\dots,m\}$ is a partition $J_1,\dots,J_m$ of the jobs; each machine processes its jobs in the order $\prec$ without idle time, so the completion time of $j$ is

$$C_j(\sigma)=p_j+\sum_{k\prec j,\ \sigma(k)=\sigma(j)}p_k .$$

The value of $\sigma$ is $\sum_j w_jC_j(\sigma)$, and $Z^*$ is the minimum value over all assignments.

The graph $G_J$ is the complete graph on $J$ in which the edge $\{j,k\}$ with $k\prec j$ has weight $c(jk)=w_jp_k$; $c(E_J)$ is its total weight. A partition induces the $m$-cut $E_{\mathrm{cut}}$, the edges whose endpoints lie in different parts, of weight $c(E_{\mathrm{cut}})$; $Z^*_{\mathrm{cut}}$ is the maximum weight of an $m$-cut.

The convex quadratic relaxation (CQP) of §2.2, specialised to identical machines, has variables $a_{ij}\ge 0$ with $\sum_i a_{ij}=1$ and objective $Z_{CQP}(a)=\sum_j w_jC_j$ where

$$C_j=\sum_{i=1}^m a_{ij}\Big(\frac{1+a_{ij}}{2}\,p_j+\sum_{k\prec j}a_{ik}\,p_k\Big)\qquad(11).$$

Its optimum value is $Z^*_{CQP}$.

Formalization targets

Goal: Theorem 6.1

For $\rho\le 1$, any assignment $\sigma$ whose $m$-cut weighs at least $\rho\cdot Z^*_{\mathrm{cut}}$ satisfies

$$\sum_j w_jC_j(\sigma)\le\big(\rho+m(1-\rho)\big)\,Z^* .$$

That is, a $\rho$-approximation algorithm for Max-$m$-Cut translates into a $(\rho+m(1-\rho))$-approximation algorithm for $Pm\,|\,|\sum w_jC_j$. The constant $\rho$ is a parameter, so the goal does not depend on the best known cut algorithm.

Milestones

1. (36): for every partition, $c(E_J)=\sum_j w_jC_j-\sum_j w_jp_j+c(E_{\mathrm{cut}})$.
2. Lemma 2.5: $\bar a_{ij}=1/m$ is an optimum of (CQP), unique when the ratios $w_j/p_j$ are pairwise different and positive.
3. (37): $Z^*\ge Z^*_{CQP}=\frac1m c(E_J)+\big(\frac12+\frac1{2m}\big)\sum_j w_jp_j$.
4. (38): $Z^*_{\mathrm{cut}}\le\frac{m-1}{m}c(E_J)+\big(\frac12-\frac1{2m}\big)\sum_j w_jp_j$.
5. Theorem 2.6 b) (supplementary): assigning each job independently and uniformly at random has expected value at most $\big(\frac32-\frac1{2m}\big)Z^*$.

Significance

The result. Theorem 6.1 makes Max-$m$-Cut algorithms usable for scheduling with an explicit loss: a cut algorithm with ratio $\rho$ close to $1$ yields a schedule within $1+m(1-\rho)$ of optimal. For $m=2$ and the Goemans–Williamson ratio $0.878$ the guarantee is $1.122$, better than the $5/4$ of Theorem 2.6 b) and the $1.2752$ of the paper's semidefinite rounding in §5. In the other direction, (38) bounds the maximum cut of $G_J$ by the scheduling lower bound $Z^*_{CQP}$, which is how a relaxation for scheduling becomes a bound for a cut problem. The problem itself is better understood today: $P\,|\,|\sum w_jC_j$ has a polynomial-time approximation scheme (Skutella and Woeginger 2000), and a fully polynomial one for fixed $m$ (Sahni 1976). The reduction remains of interest as a structural identity between the two problems and as the source of the closed-form relaxation bound (37).

Formalizing it. All statements are proved in the paper; none is known to have a machine-checked proof. The mission produces a formal model of identical-machine scheduling under Smith's rule, of the weighted graph $G_J$ and its $m$-cuts, and of (CQP) for identical machines, together with the closed-form optimum of (CQP) (Lemma 2.5), which is the basis of the $\frac32-\frac1{2m}$ guarantee of Theorem 2.6 b).

Difficulty

The bookkeeping identity (36) and the final chain of inequalities are finite-sum manipulations. The substance is Lemma 2.5: that the uniform vector $\bar a$ minimizes the quadratic objective (11) over the product of simplices. The objective is not separable, since the term $\sum_{k\prec j}a_{ik}p_k$ couples jobs through Smith's order, and its convexity on the feasible region (the positive semidefiniteness established in Lemma 2.4 of the paper) is the fact on which optimality and, with distinct positive ratios, uniqueness rest. The relaxation half of (37), that $Z^*_{CQP}$ is at most the value of every schedule, needs the observation that $Z_{CQP}$ evaluated at the 0/1 vector of an assignment equals the value of that assignment.

Formalization scope

Jobs are Fin n and machines Fin m, 0-based; Smith's order is cross-multiplied ($w_jp_k>w_kp_j$, or equality and $j<k$), equal to the ratio definition because $p>0$. Assignments are functions Fin n → Fin m, and every machine is sequenced by $\prec$; by Smith's rule (p. 7 of the paper, a classical result it cites) this loses no optimality, so $Z^*$ is the minimum over assignments and is never a primitive: "within factor $\alpha$ of $Z^*$" is stated against the value of every assignment. Likewise "weight at least $\rho\cdot Z^*_{\mathrm{cut}}$" is stated as $\rho\,c(E_{\mathrm{cut}}(\tau))\le c(E_{\mathrm{cut}}(\sigma))$ for every assignment $\tau$, so no supremum of an empty or unbounded set can enter. The edge weight is attached to the ordered pair $(j,k)$ with $k\prec j$ and is zero on the other orientation, so each edge of $G_J$ is counted once. Standing hypotheses on every theorem: $p_j>0$, $w_j\ge 0$ (p. 2 of the paper) and $m>0$ (needed for $1/m$). Theorem 6.1 keeps the page's $\rho\le 1$.

Not formalized: polynomial running time, the phrase "approximation algorithm" beyond the value bound it asserts, and the semidefinite results of §5 and Corollary 6.2. A trivializing reading, such as stating the cut condition against a junk-valued supremum or replacing $Z^*$ by a free variable, is excluded by the encodings above.

The development needs only finite sums over Fin types and real arithmetic; the model of identical-machine scheduling under Smith's rule and the closed form of (CQP) are reusable for other results on $P\,|\,|\sum w_jC_j$. Proofs of the milestones, alternative proofs of Lemma 2.5 (the KKT argument the paper mentions, or Goemans' symmetrization argument it gives), and a proof of Theorem 2.6 b) are all welcome.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
• M. X. Goemans and D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
• A. Frieze and M. Jerrum, Improved approximation algorithms for MAX k-CUT and MAX BISECTION, Algorithmica 18, 1997. https://doi.org/10.1007/BF02523689
• M. Skutella and G. J. Woeginger, A PTAS for minimizing the total weighted completion time on identical parallel machines, Mathematics of Operations Research 25(1), 2000. https://doi.org/10.1287/moor.25.1.63.15212
• S. Sahni, Algorithms for scheduling independent tasks, Journal of the ACM 23(1), 1976. https://doi.org/10.1145/321921.321934

Motivation

The sample average approximation (SAA) method replaces an expectation in a stochastic program by the average over a random sample and solves the resulting deterministic problem. It is the standard way to solve two-stage stochastic linear programs with large or continuous scenario sets, and it underlies the stochastic counterpart and sample-path optimization methods of the 1990s. A basic question is how large the sample has to be.

For smooth problems the SAA optimal solution $\hat x_N$ converges to the true one at the rate $N^{-1/2}$ of the central limit theorem. A. Shapiro and T. Homem-de-Mello (SIAM J. Optim. 11(1), 2000) observed that for problems whose optimum is a sharp minimum, as is typical of two-stage linear programs with finitely many scenarios, the picture is different. In §2 of the paper they prove that the SAA problem then returns the exact true solution with probability one for all sufficiently large $N$. In §3, formalized here, they show that the probability of the complementary event, the SAA solution not being exactly $\bar x$, decays exponentially in $N$. One consequence they draw is that a modest sample can find the optimum of a problem with an astronomically large number of scenarios. This mission is the second of three on the paper; the first formalizes the almost sure statement (Theorem 2.1), the third the polyhedral case with multiple optima (Theorem 3.2).

Setting

Let $P$ be a probability measure on a sample space $(\Omega,\mathcal F)$, $\Theta\subseteq\mathbb R^m$, and $h:\mathbb R^m\times\Omega\to\mathbb R$. The true problem (1.1) is

$$\min_{x\in\Theta}\ f(x):=\mathbb E_P\,h(x,\omega).$$

Given an i.i.d. sample $\omega^1,\omega^2,\dots$ with law $P$, the SAA problem (1.2) is

$$\min_{x\in\Theta}\ \hat f_N(x):=\frac1N\sum_{j=1}^N h(x,\omega^j).$$

$A$ and $A_N$ denote the sets of optimal solutions of (1.1) and (1.2). For a function $g$, $g'(x,d)=\lim_{t\downarrow0}(g(x+td)-g(x))/t$ is its directional derivative, and $h'_\omega(x,d)$ is that of $h(\cdot,\omega)$. $T_\Theta(\bar x)$ is the tangent cone of $\Theta$ at $\bar x$, and $S^{m-1}=\{d:\|d\|=1\}$.

The standing hypotheses are those of Theorem 2.1 of the paper: (i) $h(\cdot,\omega)$ is convex for every $\omega$; (ii) $f$ is finite valued; (iii) $\Theta$ is closed and convex; (iv) Assumption (A): $A=\{\bar x\}$ and $\bar x$ is a sharp minimum, i.e. there is $c>0$ with

$$f(x)\ge f(\bar x)+c\|x-\bar x\|\qquad\text{for all }x\in\Theta. \tag{2.2}$$

Section 3 adds Assumption (B): with $\eta(d,\omega):=h'_\omega(\bar x,d)$ (3.1), there is $\kappa>0$ such that $\sup_{d\in S^{m-1}}|\eta(d,\omega)|\le\kappa$ for $P$-almost every $\omega$. It holds whenever $\Omega$ is finite.

The event of interest is

$$\mathcal E_N:=\{A_N\neq\emptyset\text{ and }A_N=\{\bar x\}\},\tag{3.7}$$

that the SAA problem has the unique optimal solution $\hat x_N=\bar x$.

For a direction $d$, $M_d(t)=\mathbb E_P e^{t\eta(d,\omega)}$ and $I_d(\alpha)=\sup_{t\in\mathbb R}[t\alpha-\log M_d(t)]$ (3.5) is the one-dimensional rate function of $\eta(d,\omega)$. On the Banach space $Z=C(S^{m-1})$, $I(z)=\sup_{z^*\in Z^*}\{z^*(z)-\log M(z^*)\}$ (3.4) is the rate function of the random element $\eta(\cdot,\omega)$.

Formalization targets

Goal: Theorem 3.1 (p. 11)

Under (i)–(iv) and Assumption (B) there is a constant $\beta>0$ with

$$\limsup_{N\to\infty}\frac1N\log P(\mathcal E_N^c)\le-\beta.\tag{3.8}$$

The goal asserts the existence of an exponential rate and does not fix its value.

Stronger: the explicit rate (p. 12)

With $c$ from (2.2) and $\kappa$ from (B),

$$\limsup_{N\to\infty}\frac1N\log P(\mathcal E_N^c)\le-\frac{c^2}{2\kappa^2},$$

which is (3.8) combined with (3.15).

Milestones

In the order of the proof:

• the reduction $P(\mathcal E_N^c)\le P(\zeta_N\in F)$ with $\zeta_N=\hat f'_N(\bar x,\cdot)$ and $F=\{z:\inf_{T_\Theta(\bar x)\cap S^{m-1}}z\le0\}$ (p. 11);
• for a random variable $X$ with $|X|\le\kappa$ and $\Lambda(t)=\log\mathbb E e^{tX}$, the bounds $|\Lambda'|\le\kappa$, $|\Lambda''|\le\kappa^2$ (3.11) and $|\Lambda'(t)-\Lambda'(s)|\le\kappa^2|t-s|$ (3.12);
• the quadratic lower bound $I_d(\alpha)\ge|\alpha-\bar\alpha_d|^2/(2\kappa^2)$ (3.13);
• $I_d(0)\ge c^2/(2\kappa^2)$ on $T_\Theta(\bar x)\cap S^{m-1}$ (3.14);
• the comparison $I(z)\ge\sup_{d}I_d(z(d))$ (3.6);
• $\beta=\inf_{z\in F}I(z)\ge c^2/(2\kappa^2)$ (3.15).

Significance

Theorem 3.1 says that at a sharp minimum the SAA method is exact except on an event of probability $O(e^{-\beta N})$. The sample size needed for a given confidence therefore grows only logarithmically in the confidence level, and it does not depend on the number of scenarios. This is the basis of the paper's numerical observation that problems with very many scenarios are solved exactly from samples of a few hundred. The explicit constant $c^2/(2\kappa^2)$ relates the rate to two interpretable quantities: the sharpness $c$ of the optimum and the bound $\kappa$ on the subgradients of $h(\cdot,\omega)$ at $\bar x$.

The result is proved in the paper. As far as is known it has no machine-checked proof. A complete formalization produces three things. First, a Lean proof that the SAA problem recovers a sharp optimum exactly with exponentially small failure probability. Second, the elementary facts about cumulant generating functions of bounded variables, (3.11)–(3.13), which are reusable in any Chernoff-type argument. Third, the link between the rate function of a $C(K)$-valued random element and its one-dimensional projections, (3.6).

Difficulty

The event $\mathcal E_N^c$ is controlled by the positivity of a whole function, $\zeta_N(d)=\hat f_N'(\bar x,d)$, on the infinite set $T_\Theta(\bar x)\cap S^{m-1}$. A Chernoff bound for each fixed direction $d$ is easy, but there are uncountably many directions, so a union bound over $d$ is not available. The paper handles this with Cramér's theorem in the separable Banach space $C(S^{m-1})$, and that infinite-dimensional large deviations upper bound is not in Mathlib. A proof must either develop that bound or find a finite-dimensional substitute that keeps an exponential rate.

A second difficulty is conversion. Cramér's theorem gives a rate in terms of $\inf_{z\in F}I(z)$, and that infimum must be shown positive. Positivity comes from the sharpness constant $c$ through the strong convexity of the one-dimensional rate functions, which needs the bounds (3.11)–(3.13) on the cumulant generating function.

Formalization scope

• The decision space is EuclideanSpace ℝ (Fin m). The scenario space $(\Omega,\mathcal F,P)$ carries the law of one scenario. The sample is one i.i.d. sequence of $\Omega$-valued maps on a separate probability space $(S,Q)$, and $\hat f_N$ uses its first $N$ terms. Optimal sets are written without infima: $A_N=\{\bar x\}$ encodes "nonempty and equal to $\{\bar x\}$".
• Directional derivatives are the limUnder of the difference quotient as $t\downarrow0$. Every statement assumes (i), under which the limit exists. The tangent cone is Mathlib's tangentConeAt, which for convex $\Theta$ is the closure of the cone of feasible directions.
• Disclosed pins.
  • "f finite valued" is $P$-integrability of every $h(x,\cdot)$, which includes measurability.
  • Assumption (B) is stated pointwise in $d\in S^{m-1}$ under the almost sure quantifier.
  • $\mathcal E_N^c$ is not shown measurable, so its probability is an outer measure, and an upper bound on it is the stronger claim.
  • The rate (3.8) is stated in the equivalent form: there is $\beta>0$ such that for every $\varepsilon>0$, eventually $Q(\mathcal E_N^c)\le e^{-(\beta-\varepsilon)N}$. A logarithm of a real probability is never taken.
  • Rate functions $I_d$ and $I$ take values in $(-\infty,+\infty]$. They use the published extended-real logMGF and legendre, under which $I_d(\alpha)=+\infty$ for $|\alpha|>\kappa$ is a genuine value, not a default.
  • The one-dimensional bounds (3.11)–(3.13) are stated for an arbitrary bounded measurable random variable.
• Trivializing readings are ruled out. The goal's $\beta$ is fixed before $\varepsilon$ and $N$, so it cannot depend on them. The event is uniqueness and equality, $A_N=\{\bar x\}$, not $\bar x\in A_N$. The standing hypotheses are jointly satisfiable: a sorry-free check exhibits them for $h(x,\omega)=\|x\|$, $\Theta=\mathbb R^m$ and a product-measure sample.
• Infrastructure. A complete development needs: directional derivatives of finite convex functions and their continuity in the direction; interchange of directional derivative and expectation (Proposition 2.2 of the paper, formalized in the first mission of the series); derivatives of the cumulant generating function (Mathlib's ProbabilityTheory.cgf and its analyticity); and an exponential upper bound for empirical means in $C(S^{m-1})$ or a substitute. The cumulant generating function lemmas and any Banach-space Cramér bound are reusable beyond this mission. Contributions are welcome for any milestone, and for alternative proofs of the goal that avoid Cramér's theorem in function space.

Selected references

• A. Shapiro and T. Homem-de-Mello, On the rate of convergence of optimal solutions of Monte Carlo approximations of stochastic programs, SIAM J. Optim. 11(1):70–86, 2000. https://doi.org/10.1137/S1052623498349541 (formalized from the authors' preprint, Stochastic Programming E-Print Series)
• J.-D. Deuschel and D. W. Stroock, Large Deviations, Academic Press, 1989 (Cramér's theorem in Banach spaces, cited as [8]).
• J.-B. Hiriart-Urruty and C. Lemaréchal, Convex Analysis and Minimization Algorithms II, Springer, 1993, Theorem X.4.2.2 (strong convexity of conjugates, cited as [12]). https://doi.org/10.1007/978-3-662-06409-2
• A. J. Kleywegt, A. Shapiro and T. Homem-de-Mello, The sample average approximation method for stochastic discrete optimization, SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220

Motivation

In a road or communication network where each unit of traffic picks its own route, the outcome is a Nash flow (Wardrop equilibrium): no traffic can lower its own latency by switching paths. It is well known since Pigou (1920) that such selfish routing can be inefficient: the total latency of a Nash flow may exceed that of the best centrally planned flow. The ratio between the two, maximized over a family of instances, is the price of anarchy. Network designers, transportation economists and computer scientists use it to decide when central coordination (tolls, routing protocols) is worth its cost.

Timeline:

• 1920–1956. Pigou's two-road example shows inefficiency; Wardrop (1952) and Beckmann, McGuire and Winsten (1956) formalize equilibrium flows and characterize optimal flows by marginal costs.
• 2002. Roughgarden and Tardos (J. ACM 49(2), 2002) prove that with affine latencies $\ell(x)=ax+b$ the price of anarchy is exactly $4/3$ in every network.
• 2002–2003. Roughgarden (STOC 2002; journal version J. Comput. Syst. Sci. 67(2), 2003) shows that for any class of latency functions satisfying mild conditions the price of anarchy does not depend on the network: two parallel links are already worst possible. This mission formalizes that paper.
• 2004. Correa, Schulz and Stier-Moses (Math. Oper. Res. 29(4), 2004) give a geometric proof of the same bound and extend it to capacitated networks.

Setting

A network is a finite directed multigraph $G=(V,E)$; parallel edges are allowed. There are $k$ commodities; commodity $i$ has a source $s_i$, a sink $t_i$, a rate $r_i>0$, and at least one simple $s_i$–$t_i$ path. A flow $f$ assigns a nonnegative amount $f^i_P$ to each simple $s_i$–$t_i$ path $P$; it is feasible if $\sum_P f^i_P=r_i$ for every $i$. The edge flow is $f_e=\sum_i\sum_{P\ni e}f^i_P$.

Each edge carries a latency function $\ell_e:[0,\infty)\to\mathbb R$, nonnegative, differentiable and nondecreasing. The latency of a path is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$ and the cost of a flow is $C(f)=\sum_i\sum_P\ell_P(f)f^i_P$. A feasible flow of least cost is optimal. A flow is a Nash flow (Definition 2.1) if moving any amount $\delta\in(0,f^i_{P_1}]$ of commodity $i$ from a used path $P_1$ to another path $P_2$ yields a flow $\tilde f$ with $\ell_{P_1}(f)\le\ell_{P_2}(\tilde f)$. The ratio between the cost of a Nash flow and of an optimal flow is $\rho(G,r,\ell)$.

A latency function is standard if $x\,\ell(x)$ is convex on $[0,\infty)$; its marginal cost is $\ell^*(x)=\frac{d}{dx}(x\,\ell(x))$. A class $\mathcal L$ of latency functions is standard if it contains a nonzero function and all its members are standard. The anarchy value of a standard $\ell$ is

$$\alpha(\ell)=\sup_{r>0:\ \ell(r)>0}\bigl[\lambda\mu+(1-\lambda)\bigr]^{-1},\qquad \ell^*(\lambda r)=\ell(r),\ \lambda\in[0,1],\ \mu=\frac{\ell(\lambda r)}{\ell(r)},$$

and $\alpha(\mathcal L)=\sup_{0\neq\ell\in\mathcal L}\alpha(\ell)\in[1,\infty]$. It is the worst ratio in a Pigou-type network: two parallel links, one with a constant latency and one with $\ell$. Finally, $G_2$ is the network with one source, one sink and two edges from source to sink.

Formalization targets

Goal: Theorem 4.2

For a standard class $\mathcal L$ that contains the constant functions $\ell(x)=c$, $c>0$, with $\mathcal I$ the set of all instances with latencies in $\mathcal L$ and $\mathcal I_2\subseteq\mathcal I$ the single-commodity instances on $G_2$,

$$\sup_{(G_2,r,\ell)\in\mathcal I_2}\rho(G_2,r,\ell)=\alpha(\mathcal L)=\sup_{(G,r,\ell)\in\mathcal I}\rho(G,r,\ell).$$

It is stated as two parts: every ratio $C(f)/C(f^*)$ of a feasible Nash flow to a feasible flow of positive cost, in any network with any number of commodities, is at most $\alpha(\mathcal L)$; and every value below $\alpha(\mathcal L)$ is exceeded by such a ratio on $G_2$.

Milestones

The milestones follow the paper's proof: the edge form of the cost (§2.1), the shortest-path characterization of Nash flows (Proposition 2.2), the cost of a Nash flow (Proposition 2.3), monotonicity and continuity of marginal costs (§2.3), existence of $\lambda$ (§3.1), Lemmas 3.5–3.7, the upper bound $\rho\le\alpha(\mathcal L)$ (Theorem 3.8) and the two-link lower bound (Lemma 4.1).

Companion results

Lemma 4.4 and Theorem 4.5 replace "contains the constants" by diversity (for each $c>0$ some $\ell\in\mathcal L$ has $\ell(0)=c$) and show that networks of parallel links are worst possible among single-commodity instances. Proposition 5.1 computes the price of anarchy of polynomials of degree at most $p$ with nonnegative coefficients:

$$\sup_{\mathcal I_p}\rho=\bigl[1-p\,(p+1)^{-(p+1)/p}\bigr]^{-1}=\Theta\!\left(\frac{p}{\ln p}\right).$$

Significance

The theorem reduces a combinatorial question (the worst instance over all networks and all commodity structures) to a one-dimensional calculus problem: computing $\alpha(\ell)$ for the steepest functions of the class. It yields exact prices of anarchy for polynomial latencies (Proposition 5.1), for M/M/1 delay functions and others, and it shows that the inefficiency of selfish routing is never caused by the interaction of commodities or by network structure: Pigou's two-link example already captures it. The bound has become a standard reference point for later work on smoothness arguments, tolls and Stackelberg routing.

The result is proved; it has not been formalized. This mission produces a machine-checked model of nonatomic multicommodity routing on directed multigraphs (simple paths, path flows, Nash flows in the paper's own definition, marginal costs), the general upper bound for an arbitrary standard class, and the matching lower bound in two-link and parallel-link networks. Alternative arguments, such as the variational-inequality proof of Correa, Schulz and Stier-Moses, are equally welcome as proofs of the same statements.

Difficulty

The obvious approach, following Roughgarden–Tardos for affine latencies, scales the Nash flow down by a constant factor and shows the result is optimal for reduced rates. For nonlinear latencies no single factor works. The paper's proof scales each edge by its own factor $\lambda_e$, which produces a pseudoflow that obeys no conservation constraints, and the augmentation from it to an optimal flow must then be priced edge by edge. Formally, the scaling factors are solutions of $\ell_e^*(\lambda_e f_e)=\ell_e(f_e)$ that need not be unique, marginal costs are one-sided derivatives at $0$, and the anarchy value may be infinite, so every comparison has to be valid in the extended reals.

Formalization scope

All declarations live in PoAIndep.Topology. A network is a pair of finite types with endpoint maps src tgt : E → V; parallel edges are free. Simple paths are nonempty edge lists with a repetition-free vertex sequence, so commodities with $s_i=t_i$ are excluded. A flow stores one finitely supported path flow per commodity. Latency functions are maps $\mathbb R\to\mathbb R$ whose properties (nonnegative, differentiable, nondecreasing; for standard ones, $x\ell(x)$ convex) are required on $[0,\infty)$ only, and $\ell^*$ is the derivative within $[0,\infty)$. The standing assumptions of §2.1 ($r_i>0$, $\mathcal P_i\neq\emptyset$, latency properties) are fields of the Instance structure; standardness of the latencies enters through the class $\mathcal L$.

The anarchy values live in $[0,\infty]$; $\alpha(\ell)$ is the supremum over all admissible pairs $(r,\lambda)$, which equals the page's value because the expression does not depend on the choice of $\lambda$. Instead of $\rho$, which presupposes existence and uniqueness of the Nash cost (Proposition 2.4, cited by the paper), statements bound $C(f)/C(f^*)$ for every feasible Nash flow $f$ and every feasible $f^*$ with $C(f^*)>0$. The networks $G_2$ and $G_m$ are instances of the general model, so $\mathcal I_2\subseteq\mathcal I$ holds literally.

The Nash condition is Definition 2.1, not the shortest-path characterization, and the cost is the path sum, not the edge sum; both alternatives would make milestones trivial. The goal is not satisfied by the two-link lower bound alone: its upper part quantifies over every network and every number of commodities.

Reusable beyond this mission: the routing model, Nash flows, marginal costs and the anarchy value, which also underlie the companion paper on the $4/3$ bound and later work on tolls and Stackelberg strategies. Proofs of any milestone, and supporting lemmas about convex functions with one-sided derivatives, are welcome.

Selected references

• T. Roughgarden, The price of anarchy is independent of the network topology, STOC 2002, pp. 428–437; journal version J. Comput. Syst. Sci. 67(2):341–364, 2003. https://doi.org/10.1145/509967.509971
• T. Roughgarden and É. Tardos, How bad is selfish routing?, J. ACM 49(2):236–259, 2002. https://doi.org/10.1145/506147.506153
• J. R. Correa, A. S. Schulz and N. E. Stier-Moses, Selfish routing in capacitated networks, Math. Oper. Res. 29(4):961–976, 2004. https://doi.org/10.1287/moor.1040.0098
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Inst. Civil Engineers, Part II, 1:325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259

Motivation

A telephone call center must decide how many agents $N$ to staff against an offered load $R=\lambda/\mu$ (arrival rate over service rate). Staff too few and callers wait and hang up; staff too many and agents sit idle. For large centers the industry rule of thumb is square-root safety staffing, $N\approx R+\beta\sqrt R$, and the question is what service level such a rule buys.

For the model without abandonment, the $M/M/N$ queue, the answer is the theorem of Halfin and Whitt (Oper. Res. 1981): the probability of waiting has a nondegenerate limit in $(0,1)$ exactly when $\sqrt N(1-\rho_N)\to\beta>0$. Real callers are impatient, and Garnett, Mandelbaum and Reiman (M&SOM 2002) prove the analogue for the Erlang-A queue, where abandonment changes both the limits and the admissible range of $\beta$. Their Theorem 4 is the theoretical basis of the "quality-and-efficiency-driven" (QED) staffing regime used in call-center practice.

Timeline. Palm (1943) introduced exponential patience; Riordan (1962) computed the conditional mean wait of the model; Jagerman (1974) gave the asymptotics of the Erlang-B formula; Halfin and Whitt (1981) proved the square-root law for $M/M/N$ ($\beta>0$ only); Fleming, Stolyar and Simon (1994) found the limiting stationary law of the scaled Erlang-A queue; Garnett, Mandelbaum and Reiman (2002) proved the three-way equivalence below, for $\beta$ of either sign.

Setting

The Erlang-A queue ($M/M/N+M$) has Poisson arrivals of rate $\lambda>0$, $N\ge1$ identical agents with exponential service of rate $\mu>0$, an unlimited waiting room served in order of arrival, and independent exponential patience times of rate $\theta>0$: a caller whose wait exceeds their patience abandons. The number in system is a birth–death process with birth rate $\lambda$ and death rate $\min(k,N)\mu+(k-N)^+\theta$; its stationary law is

$$\pi_k\propto\frac{(\lambda/\mu)^k}{k!}\ (k\le N),\qquad \pi_k\propto\prod_{j=N+1}^{k}\frac{\lambda}{N\mu+(j-N)\theta}\cdot\frac{(\lambda/\mu)^N}{N!}\ (k>N).$$

The three performance measures are:

• the delay probability $P_N\{W>0\}=\sum_{k\ge N}\pi_k$, the chance an arriving caller must wait;
• the abandonment probability $P_N\{Ab\}=\sum_{n\ge0}\pi_{N+n}\,\frac{(n+1)\theta}{N\mu+(n+1)\theta}=\frac{\theta}{\lambda}\sum_{k>N}(k-N)\pi_k$;
• the Erlang-B blocking probability $P_N\{Bl\}=E(\lambda/\mu,N)$ of the loss system $M/M/N/N$.

Write $\varphi,\Phi$ for the standard normal density and distribution function, $h(x)=\varphi(x)/[1-\Phi(x)]$ for its hazard rate, and

$$w(x,y)=\Bigl[1+\frac{h(-xy)}{y\,h(x)}\Bigr]^{-1}.$$

In the asymptotic statements the $N$-th system has $N$ agents, arrival rate $\lambda_N$, the fixed service rate $\mu$, patience rate $\theta_N$, and traffic intensity $\rho_N=\lambda_N/(N\mu)$.

Formalization targets

Goal: Theorem 4 (p. 219)

With $\theta_N\equiv\theta\in(0,\infty)$, the following are equivalent:

$$\lim_{N\to\infty}\sqrt N(1-\rho_N)=\beta\in\mathbb R,\qquad \lim_{N\to\infty}P_N\{W>0\}=\alpha\in(0,1),\qquad \lim_{N\to\infty}\sqrt N\,P_N\{Ab\}=\Delta\in(0,\infty),$$

in which case $\alpha=w(-\beta,\sqrt{\mu/\theta})$ and $\Delta=[\sqrt{\theta/\mu}\,h(\beta\sqrt{\mu/\theta})-\beta]\,\alpha$.

Milestones

1. The weak limit of the scaled stationary queue $(Q_N(\infty)-N)/\sqrt N$ (proof of Theorem 2*, Part 2, p. 225).
2. Lemma 1: $P_N\{W>0\}\to w(-\beta,\sqrt{\mu/\theta})$.
3. Three exact finite-$N$ identities for $P_N\{Ab\}$ (Riordan, Palm, and the final form in $P_N\{W>0\}$ and $P_N\{Bl\}$), p. 226.
4. The Erlang-B asymptotic $\sqrt N\,P_N\{Bl\}\to h(-\beta)$.
5. Lemma 2: $\sqrt N\,P_N\{Ab\}\to[\sqrt{\theta/\mu}\,h(\beta\sqrt{\mu/\theta})-\beta]\,w(-\beta,\sqrt{\mu/\theta})$.
6. The Remark on the extremes: $\beta=-\infty$ iff $\alpha=1$ iff $\Delta=\infty$, and $\beta=+\infty$ iff $\alpha=0$ iff $\Delta=0$.

Lemmas 1 and 2 and the stationary limit are stated with $\theta_N\to\theta\in(0,\infty)$, the paper's setting for them.

Significance

The result. Theorem 4 states that a single parameter, the scaled staffing gap $\beta$, determines both service measures in the limit, and that no other staffing sequence gives a nondegenerate delay probability or abandonment of order $1/\sqrt N$. Because $\beta$ may be negative, a call center with impatient callers can be staffed below the offered load and still keep abandonment at order $1/\sqrt N$, which is impossible without abandonment. The explicit $\alpha(\beta)$ and $\Delta(\beta)$ turn a target delay probability or abandonment level into a value of $\beta$, which is the staffing rule of Table 4 of the paper.

Formalizing it. The theorem is proved in the paper, partly by citation (Fleming et al. for the stationary limit, Jagerman for Erlang-B, Riordan and Palm for exact formulas); none of it has been machine-checked. A formalization supplies the cited inputs, the exact identities, and the converse directions, which the paper treats briefly. The $\theta=0$ counterpart, the Halfin–Whitt theorem, is posed separately on the platform (QueueingFundamentals.BirthDeath.halfin_whitt, HalfinWhitt81.Stationary.theorem_1) and is not a target here.

Difficulty

Every quantity is an explicit series, but its limit is a local-limit problem. The $N$ terms below $N$ form a Poisson-type sum whose normalized tail must be shown to converge to a Gaussian integral uniformly enough to pass through the normalization. The terms above $N$ form a product whose logarithm must be expanded to second order in $(k-N)/\sqrt N$. The two pieces enter with comparable weight, so neither can be dropped. Termwise convergence alone does not suffice: the series need tail bounds uniform in $N$. The converse directions require monotonicity of $\alpha$ and $\Delta$ in $\beta$ and the extreme regimes, not only the limits at finite $\beta$.

Formalization scope

• Model. All objects are explicit functions of $(N,\lambda,\mu,\theta)$ defined in ErlangA.Staffing.Model; the stationary law is the explicit normalized sequence, not an arbitrary steady state. The sequences are $\lambda,\theta:\mathbb N\to\mathbb R$ with $\lambda_N,\theta_N>0$ for $N\ge1$, and $\mu>0$ is fixed.
• Delay. $P_N\{W>0\}=\sum_{k\ge N}\pi_k$ (arrivals finding all agents busy). The paper's proof writes $P\{Q_N(\infty)>N\}$, which differs by $\pi_N\to0$.
• Abandonment. $P_N\{Ab\}$ is the arrival form above. It equals the balance form $(\theta/\lambda)\sum_{k>N}(k-N)\pi_k$ of equation (2).
• Limits. Every limit is Filter.Tendsto … atTop of the $N$-th quantity; $\pm\infty$ limits use atTop/atBot. The ranges $\beta\in\mathbb R$, $\alpha\in(0,1)$, $\Delta\in(0,\infty)$ are part of the goal: without them the equivalence is false (the delay probability also converges, to $1$, when $\sqrt N(1-\rho_N)\to-\infty$).
• Goal shape. A conjunction of List.TFAE of the three existential conditions with the "in which case" clause. Neither part may be dropped, and the equivalence may not be weakened to one direction or to $\beta>0$.
• Misprints. Two printed formulas are corrected: the Riordan term $(\lambda_N\theta)$ is read as $(\lambda_N/\theta)$, and a parenthesis is restored in the density $f$ on p. 225.
• Infrastructure. Needed: tail bounds for Poisson-type series, a local central limit estimate for the Poisson distribution near its mean, Gaussian tail asymptotics $h(t)\sim t$, and the incomplete gamma function. The Erlang-B asymptotic and the Gaussian facts are reusable for every many-server queue. Solutions to any milestone, and to auxiliary lemmas such as summability of the stationary weights, are welcome.

Selected references

• O. Garnett, A. Mandelbaum, M. Reiman, Designing a call center with impatient customers, Manufacturing & Service Operations Management 4(3), 208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–587, 1981. https://doi.org/10.1287/opre.29.3.567
• D. L. Jagerman, Some properties of the Erlang loss function, Bell System Technical Journal 53, 1974 (as cited in the paper's reference list).
• P. J. Fleming, A. Stolyar, B. Simon, Heavy traffic limit for a mobile phone system loss model, Proc. 2nd Int. Conf. Telecommunication Systems, Modeling and Analysis, Nashville, 158–176, 1994.

Motivation

Many decision problems in operations research have a finite set of alternatives and an objective that is an expectation: choose a configuration, a route or a stocking level $x$ from a finite set $\mathcal S$ to minimize the expected cost $\mathbb E\,G(x, W)$, where $W$ is random. When the expectation cannot be computed in closed form, the sample average approximation (SAA) method draws an i.i.d. sample $W^1, \dots, W^N$, replaces the expectation by the sample average, and solves the resulting deterministic problem. Its optimal value $\hat v_N$ is used in practice as an estimate of the true optimal value $v^*$, and statistical bounds on the quality of a candidate solution are built from replications of $\hat v_N$ (Mak, Morton and Wood, 1999). Confidence statements of that kind need the distribution of $\hat v_N$, at least asymptotically.

Kleywegt and Shapiro (preprint, two-author version; published with Homem-de-Mello in SIAM J. Optim. 12 (2002)) gave the asymptotic distribution of $\hat v_N$ for discrete problems in their Proposition 2.3. The analogous result for problems with continuous decision variables is due to Shapiro (1991); the discrete statement needs neither compactness nor Lipschitz continuity in $x$, and requires finite variances only at the optimal solutions.

Setting

Let $\mathcal S$ be a nonempty finite set, $\mathcal W$ a measurable space, and $G : \mathcal S \times \mathcal W \to \mathbb R$ a function such that for every $x \in \mathcal S$ the map $G(x, \cdot)$ is measurable and $\mathbb E\,|G(x, W)| < \infty$, where $W$ is a random element of $\mathcal W$. The true problem (1.1) is

$$v^* = \min_{x \in \mathcal S} g(x), \qquad g(x) = \mathbb E\, G(x, W),$$

and its set of optimal solutions is $\mathcal S^* = \{x \in \mathcal S : g(x) = v^*\}$. Given an i.i.d. sample $W^1, W^2, \dots$ of $W$, the sample average function and the SAA problem (2.1) are

$$\hat g_N(x) = \frac1N \sum_{n=1}^N G(x, W^n), \qquad \hat v_N = \min_{x \in \mathcal S} \hat g_N(x),$$

with optimal set $\hat{\mathcal S}_N$. Because $\mathcal S$ is finite, all minima are attained. For $x \in \mathcal S$ the variance $\sigma^2(x) = \operatorname{Var}\{G(x, W)\}$ of (2.7) may or may not exist; when the variances exist on a subset $T \subseteq \mathcal S$, the autocovariance of $G$ on $T$ is the matrix $\big(\operatorname{Cov}(G(x, W), G(x', W))\big)_{x, x' \in T}$. Convergence in distribution is written $\Rightarrow$.

Formalization targets

Goal: Proposition 2.3, (2.8)

If the variances $\sigma^2(x)$ exist for every $x \in \mathcal S^*$, then

$$\sqrt N\,(\hat v_N - v^*) \;\Rightarrow\; \min_{x \in \mathcal S^*} Y(x),$$

where $(Y(x))_{x \in \mathcal S^*}$ is a Gaussian vector with zero mean and $\operatorname{Cov}(Y(x), Y(x')) = \operatorname{Cov}(G(x, W), G(x', W))$. The statement is general in the number of optimal solutions: when $\mathcal S^*$ has more than one point, the limit is the minimum of a correlated Gaussian vector, which is not normal and has negative mean.

Milestones (in the order of the paper's argument)

1. Almost surely, $\hat v_N - \min_{x \in \mathcal S^*} \hat g_N(x) = 0$ for all $N$ large enough.
2. (2.6): $\sqrt N\,[\hat v_N - \min_{x \in \mathcal S^*} \hat g_N(x)] \to 0$ almost surely and in probability.
3. $\sqrt N\,[\min_{x \in \mathcal S^*} \hat g_N(x) - v^*] = \min_{x \in \mathcal S^*} \{\sqrt N\,[\hat g_N(x) - g(x)]\}$.
4. The joint central limit theorem: for $T \subseteq \mathcal S$ with finite variances,

$$\Big(\sqrt N\,[\hat g_N(x) - g(x)]\Big)_{x \in T} \;\Rightarrow\; (Y(x))_{x \in T}.$$

Companions

• (2.9): if $\mathcal S^* = \{x^*\}$, then $\sqrt N\,(\hat v_N - v^*) \Rightarrow N(0, \sigma^2(x^*))$.
• Negative bias (pp. 4–5): for every $N \ge 1$, $\mathbb E[\hat v_N] \le v^*$.

Significance

The result. Proposition 2.3 identifies the first-order fluctuations of the SAA optimal value. It shows that $\hat v_N$ is $\sqrt N$-consistent, that it is asymptotically normal when the true optimum is unique, and that its asymptotic bias is of order $N^{-1/2}$ and equal to $\mathbb E[\min_{x \in \mathcal S^*} Y(x)] < 0$ when several solutions are optimal and their costs are not perfectly correlated. Confidence intervals and stopping rules for SAA, and the statistical lower bounds used to assess candidate solutions, rest on this description.

Formalizing it. The result is classical and proved on paper; it has not been machine-checked. A formal proof requires a multivariate central limit theorem, which this Mathlib does not contain (only the one-dimensional CLT is available), together with the transfer of convergence in distribution through the continuous map $y \mapsto \min_x y(x)$ and through perturbations that vanish in probability. These components are general probability results whose use extends well beyond stochastic programming. The negative-bias inequality and the singleton case (2.9) are included as companion targets.

Difficulty

The argument on the page is short, and each step names a standard theorem. The formal difficulty is that two of those theorems are not available in the needed form. The central limit theorem is used for a random vector indexed by $\mathcal S^*$, with an arbitrary, possibly singular, covariance matrix; a coordinatewise application of the one-dimensional CLT gives only the marginal limits, which do not determine the law of the minimum. The step from (2.6) to (2.8) combines convergence in distribution with a term that tends to zero in probability, which requires a Slutsky-type lemma on the real line. The tempting simplification of assuming a unique optimal solution removes exactly the case in which the limit is not normal, and is therefore not the goal.

Formalization scope

The feasible set is a Finset of an arbitrary type X, assumed nonempty; minima over it and over $\mathcal S^*$ are Finset.inf', so they are attained. $\mathcal S^*$ is the Finset of minimizers of $g$. The sample is a sequence W : ℕ → Ω → 𝒲 of measurable maps on a probability space, mutually independent (iIndepFun) and identically distributed with W 0; the paper's $W^n$ is W (n - 1), and $g(x)$ is the expectation of $G(x, W^1)$. Measurability of $G(x, \cdot)$ is Borel measurability. "The variance exists" is square integrability (MemLp … 2), assumed in the goal only on $\mathcal S^*$, exactly as in the Proposition. Convergence in distribution is Mathlib's TendstoInDistribution; the limit is any random vector $Y$, on any probability space, whose law is multivariateGaussian 0 Σ on the Euclidean space $\mathbb R^{\mathcal S^*}$, with $\Sigma$ the autocovariance matrix of $G$ on $\mathcal S^*$. That matrix is positive semidefinite under the variance hypothesis, so the Gaussian law is genuine (Mathlib's multivariateGaussian degenerates to a point mass only for a matrix that is not positive semidefinite). The milestone CLT is stated jointly, for every subfamily $T \subseteq \mathcal S$ with finite variances; the page states it for $T = \mathcal S$ in terms of marginals plus covariances.

A trivializing formalization is ruled out: the limit is indexed by $\mathcal S^*$ and not by $\mathcal S$, its covariance is the autocovariance of $G$ and not a free matrix, square integrability is assumed wherever a covariance is used, and the negative-bias statement asserts integrability of $\hat v_N$ so that the Bochner integral is not its junk value $0$.

A complete development needs the multivariate central limit theorem for i.i.d. square-integrable vectors (for instance through characteristic functions or the Cramér–Wold device), the continuous mapping theorem, a Slutsky lemma, and the strong law of large numbers applied to finitely many functions. The multivariate CLT and the Slutsky lemma are reusable beyond this mission. Contributions to any of these, and proofs of any item, are welcome.

Selected references

• A. J. Kleywegt and A. Shapiro, The sample average approximation method for stochastic discrete optimization, preprint (two-author version), https://edoc.hu-berlin.de/server/api/core/bitstreams/2dcf2d5b-5fb9-44d1-b36a-5e378c803717/content. Published with T. Homem-de-Mello in SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220
• A. Shapiro, Asymptotic analysis of stochastic programs, Annals of Operations Research 30:169–186, 1991. https://doi.org/10.1007/BF02204815
• W. K. Mak, D. P. Morton and R. K. Wood, Monte Carlo bounding techniques for determining solution quality in stochastic programs, Operations Research Letters 24:47–56, 1999. https://doi.org/10.1016/S0167-6377(98)00054-6
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751