Operations Research

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

Motivation

Two-stage stochastic linear programs choose a first-stage decision $x$ before a random parameter is revealed and a recourse decision $w$ afterwards. The classical model assumes the distribution of the random data is known. In practice it is estimated, and often only its first two moments are trusted. The minimax (distributionally robust) approach hedges against this ambiguity by minimizing the worst-case expected cost over all distributions consistent with the known information; it goes back to Žáčková (1966) and Dupačová (1987). A second concern is risk: a decision maker who is not risk neutral evaluates the random second-stage cost through a nondecreasing convex disutility, not through its mean.

Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) combine both: the distribution of the second-stage data is known only through its mean and second-moment matrix, and the second-stage cost is passed through a piecewise-linear convex disutility. For the case where the randomness is in the objective of the second-stage problem, they show that the resulting minimax problem is exactly a single semidefinite program of polynomial size. This mission formalizes that result, Theorem 2.1 of the paper, and the steps of its proof.

Setting

The first-stage feasible region is $X=\{x\in\mathbb R^n : Ax=b,\ x\ge 0\}$ for $A\in\mathbb R^{m_1\times n}$, $b\in\mathbb R^{m_1}$, with first-stage cost vector $c\in\mathbb R^n$. Given a recourse matrix $W\in\mathbb R^{r\times d}$, a technology matrix $T\in\mathbb R^{r\times n}$ and $h\in\mathbb R^r$, the recourse set of $x$ is $X(x)=\{w\in\mathbb R^d : Ww=h-Tx,\ w\ge 0\}$. For an objective vector $q\in\mathbb R^d$, the second-stage cost is the value of a linear program,

$$\mathcal Q(q,x)=\min_{w}\ q'w\quad\text{s.t.}\quad Ww=h-Tx,\ w\ge 0 .$$

The disutility is $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge 0$, a nondecreasing convex piecewise-linear function; $K=1$, $\alpha_1=1$, $\beta_1=0$ is the risk-neutral case.

The objective $\tilde q$ of the second stage is random, the right-hand side $h$ is constant. The moment class $\mathcal P$ consists of all probability distributions of $\tilde q$ on $\mathbb R^d$ with $\mathbb E_P[\tilde q]=\mu$ and $\mathbb E_P[\tilde q\tilde q']=Q$. The problem studied is

$$Z=\min_{x\in X}\Big(c'x+Z(x)\Big),\qquad Z(x)=\sup_{P\in\mathcal P}\mathbb E_P\big[\mathbb U(\mathcal Q(\tilde q,x))\big]. \tag{2}$$

The inner supremum is an infinite-dimensional linear program over distributions (the paper's (5)). Its dual (6) is the semi-infinite program

$$Z_D(x)=\min_{Y,y,y_0}\ Q\cdot Y+\mu'y+y_0\quad\text{s.t.}\quad q'Yq+q'y+y_0\ge\mathbb U(\mathcal Q(q,x))\ \ \forall q\in\mathbb R^d,$$

over symmetric $Y$, where $Q\cdot Y=\sum_{i,j}Q_{ij}Y_{ij}$. The paper's standing assumptions are: $X$ is nonempty and bounded (Assumption 1); complete recourse (Assumption 2); $\{\pi\in\mathbb R^r : W'\pi\le q\}\neq\emptyset$ for all $q$ (Assumption 3); and $Q-\mu\mu'\succ 0$ (Assumption 4).

Formalization targets

Goal: Theorem 2.1

Under the assumptions, with $M_k=\begin{pmatrix}Y&\frac12(y-\alpha_k w_k)\\ \frac12(y-\alpha_k w_k)'&y_0-\beta_k\end{pmatrix}$,

$$Z=Z_{\mathrm{SDP}}=\min_{x,Y,y,y_0,w_k}\ c'x+Q\cdot Y+\mu'y+y_0\ \ \text{s.t.}\ \ M_k\succeq 0,\ Ww_k+Tx=h,\ w_k\ge0\ (k=1,\dots,K),\ Ax=b,\ x\ge 0, \tag{7}$$

and, for every $x\in X$, $Z(x)$ equals the value of the program (8) obtained from (7) by fixing $x$. The Lean goal also asserts that both $Z$ and $Z_{\mathrm{SDP}}$ are genuine greatest lower bounds of their sets of objective values.

Milestones, in the order the proof uses them

1. Weak duality $Z(x)\le Z_D(x)$ (§2.1, p. 583).
2. Strong duality $Z(x)=Z_D(x)$ under Assumption 4 (§2.1, p. 583, citing Isii).
3. Any $(Y,y,y_0)$ satisfying the $k$-th constraint $(\mathcal C_k)$ of (6) has $Y\succeq 0$.
4. Under Assumption 3, $X(x)$ is bounded and convex.
5. The minimax exchange $\inf_q\max_{w\in X(x)}=\max_{w\in X(x)}\inf_q$ for $q'Yq+q'y+y_0-\alpha_kq'w-\beta_k$.
6. $(\mathcal C_k)$ holds iff a single $w_k\in X(x)$ satisfies the inequality for every $q$.
7. The matrix inequality form: a quadratic $[q;1]'M[q;1]$ is nonnegative for all $q$ iff $M\succeq 0$ (a published, proved theorem, referenced).
8. The dual (6) and the semidefinite program (8) have the same objective values (p. 584).

Significance

Theorem 2.1 turns a minimax problem over an infinite-dimensional set of distributions, with a nonlinear risk measure applied to an LP value function, into one semidefinite program whose size is polynomial in $n$, $d$, $r$ and $K$. Off-the-shelf interior-point solvers then compute the risk-averse minimax decision, and the dual of (8) yields an explicit worst-case distribution (Theorem 2.2, formalized in the companion mission). The paper contrasts this with Delage and Ye's ellipsoid-method result, which covers a larger class of functions but gives no single compact program, and with the random right-hand-side case, which it shows to be NP-hard.

The result is proved in the paper; nothing here is open mathematics. As far as a search of the platform shows, none of it is formalized: no moment-problem duality theorem, no reformulation of a distributionally robust two-stage program, and no instance of the S-lemma-type step "$\forall q\ \exists w$ becomes $\exists w\ \forall q$" exist in machine-checked form. A complete development would provide the moment-problem strong duality for a specific continuous integrand with linear growth, which other distributionally robust optimization results reuse.

Difficulty

The obvious argument dualizes the moment problem and then substitutes the formula for $\mathcal Q$. Two steps resist this. First, strong duality for the moment problem is not a finite-dimensional LP fact: it needs the moment vector $(\mu,Q)$ to lie in the interior of the moment cone, and passing from that to "no duality gap" requires a separation argument in an infinite-dimensional space together with integrability of the integrand under every distribution with finite second moments. Second, constraint (6) is a "for every $q$ there is a $w$" statement, because $\mathcal Q(q,x)$ is a minimum over $w$. Replacing it with one $w_k$ that works for all $q$ is not a formal manipulation: it needs $Y\succeq 0$, which is not a constraint of (6) but a consequence of it, then a minimax theorem with the compact side $X(x)$, then attainment of the outer maximum. Both the boundedness of $X(x)$ and the convexity in $q$ are derived, not assumed.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ; indices $k$ run over Fin K with $K\ge 1$. The paper's letter $p$ denotes both the dimension of $q$ and the LP dual vector; here the dimension is $d$ and dual vectors are $\pi$. Distributions are probability measures with square-integrable coordinates (the platform's MomentDRO.Conf moment objects), not the densities written in (5). Every printed min/max is a real infimum/supremum of the set of objective values; attainment is not claimed except where a statement says so. $\mathcal Q(q,x)$ is a real infimum and is only used where $X(x)\neq\emptyset$ and Assumption 3 hold, which make it finite. Positive semidefiniteness is Matrix.PosSemidef on matrices indexed by Fin d ⊕ Fin 1. The minimax exchange is stated in EReal, since $\inf_q$ can be $-\infty$.

As printed, Assumptions 2 and 3 contradict each other whenever $r\ge1$: complete recourse produces a nonzero $u\ge0$ with $Wu=0$, and Assumption 3 at $q=-u$ is then infeasible. A statement assuming both would be vacuous. The formalization therefore uses what the proof of Theorem 2.1 uses: Assumption 3 for all $q$, and $X(x)\neq\emptyset$ for every $x\in X$ in place of Assumption 2. The hypotheses of the goal are satisfiable (e.g. $W=1$, $T=0$, $h=0$, $X=\{0\}$, $\mu=0$, $Q=1$). Program (7) is defined as one joint program over $(x,Y,y,y_0,w_1,\dots,w_K)$, never through $Z_D(x)$, so the goal is not strong duality plus unfolding.

Needed infrastructure: integrability of LP value functions under second-moment distributions, the moment-problem strong duality, Sion's minimax theorem (available in Mathlib and on the platform), and the bordered-matrix characterization of nonnegative quadratics (already proved on the platform). Proofs of any milestone, and reusable lemmas about LP value functions, are welcome.

Selected references

• D. Bertsimas, X. V. Doan, K. Natarajan, C.-P. Teo, Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion, Mathematics of Operations Research 35(3):580–602, 2010. https://doi.org/10.1287/moor.1100.0445
• K. Isii, On the sharpness of Chebyshev-type inequalities, Annals of the Institute of Statistical Mathematics, 185–197, 1963 (reference [15] of the paper; volume as printed there). https://doi.org/10.1287/moor.1100.0445
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• J. Dupačová, The minimax approach to stochastic programming and an illustrative application, Stochastics 20(1):73–88, 1987. https://doi.org/10.1080/17442508708833436

Motivation

Most stochastic programs cannot be solved as stated, because the objective is an expectation over a distribution that is high-dimensional, continuous or known only through a simulator. The standard remedy is the sample average approximation (SAA), also called the Monte Carlo or sample-path method: draw an i.i.d. sample, replace the expectation by the sample mean, and solve the resulting deterministic problem. The method is the workhorse of two-stage stochastic programming, and its statistical behaviour decides how large a sample a practitioner must draw.

For smooth problems with a unique optimum, the classical theory says the SAA solution converges at rate $N^{-1/2}$ and is asymptotically normal. Shapiro and Homem-de-Mello (SIAM J. Optim. 11 (2000)) observed that two-stage linear programs with finitely many scenarios behave quite differently: their optimal solutions are typically sharp, the objective grows linearly away from the minimizer, and then the SAA problem does not just approach the true solution but returns it exactly once the sample is large enough. This mission formalizes that first observation, Theorem 2.1 of the paper. Its sequels in the same series show that the probability of failure decays exponentially in $N$ (mission 2) and extend the picture to multiple optimal solutions in the finite polyhedral case (mission 3).

Setting

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

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

Let $\omega^1,\omega^2,\dots$ be an i.i.d. sequence of random elements of $\Omega$ with law $P$, defined on some probability space $(S,Q)$. The approximating problem (1.2) uses the first $N$ of them:

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

For a function $g$ on $\mathbb R^m$ write $\operatorname{argmin}_\Theta g = \{x\in\Theta : g(x)\le g(y)\ \forall y\in\Theta\}$; the optimal set of the true problem is $A=\operatorname{argmin}_\Theta f$. The directional derivative of $g$ at $x$ in direction $d$ is $g'(x,d)=\lim_{t\downarrow0}(g(x+td)-g(x))/t$; for the cost of a single scenario it is written $h'_\omega(x,d)$. The tangent cone $T_\Theta(\bar x)$ to a convex set $\Theta$ at $\bar x\in\Theta$ is the closure of $\{t(x-\bar x): t\ge0,\ x\in\Theta\}$.

Assumption (A). The true problem has a unique optimal solution $\bar x$, i.e. $A=\{\bar x\}$, and there is $c>0$ with

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

An optimal solution with this linear growth is a sharp minimum.

A statement holds w.p.1 for $N$ large enough if for $Q$-almost every sample path there is $N^*$, depending on the path, such that it holds for every $N\ge N^*$.

Formalization targets

Goal: Theorem 2.1 (p. 5)

Suppose (i) $h(\cdot,\omega)$ is convex for every $\omega$; (ii) $f$ is well defined and finite valued; (iii) $\Theta$ is closed and convex; (iv) Assumption (A) holds. Then w.p.1 for $N$ large enough

$$\operatorname*{argmin}_{x\in\Theta}\ \hat f_N(x) = \{\bar x\},$$

that is, the approximating problem has a unique optimal solution $\hat x_N$ and $\hat x_N=\bar x$.

Milestones

1. (A) ⇔ (2.3) (p. 4): for a convex problem, $\bar x$ is a sharp unique minimum iff $f'(\bar x,d)>0$ for all $d\in T_\Theta(\bar x)\setminus\{0\}$.
2. Uniform positivity (p. 4): (2.3) implies $f'(\bar x,d)\ge\varepsilon\|d\|$ for some $\varepsilon>0$ and all $d\in T_\Theta(\bar x)$.
3. Proposition 2.2 (2.5) (p. 5): $f'(x,d)=\mathbb E_P\{h'_\omega(x,d)\}$.
4. (2.10) (p. 5): $\hat f'_N(x,d)=N^{-1}\sum_{j=1}^N h'_{\omega^j}(x,d)$.
5. Proposition 2.2 (2.6) (p. 5): $\lim_N \sup_{\|d\|\le1}|f'(x,d)-\hat f'_N(x,d)|=0$ w.p.1.
6. Proposition 2.2 (2.7) (p. 5): $\lim_N\mathcal H(\partial\hat f_N(x),\partial f(x))=0$ w.p.1, with $\mathcal H$ the Hausdorff distance.
7. (2.11) (p. 6): w.p.1 for $N$ large enough, $\hat f'_N(\bar x,d)>0$ for all $d\in T_\Theta(\bar x)\cap S^{m-1}$.

Significance

The result. Theorem 2.1 says that for convex stochastic programs with a sharp optimum, SAA is not an estimator with sampling error in the usual sense: almost every sample path eventually produces the true solution itself. This is the qualitative statement behind the paper's main quantitative result (Theorem 3.1, mission 2 of this series), that the probability of not obtaining the exact solution decays like $e^{-\beta N}$. Together they explain why, in two-stage linear programs with finitely many scenarios, modest sample sizes often recover the optimal first-stage decision exactly, a phenomenon the paper documents numerically. The proposition on directional derivatives (Proposition 2.2) is of independent use: it is the almost-sure uniform convergence of first-order information of a sample average, which recurs in the asymptotic analysis of SAA estimators.

Formalizing it. The theorem is proved in the paper; nothing here is open. Machine-checked SAA theory is thin: the existing platform material treats uniform convergence of the objective on compact sets, not directional derivatives or exactness at sharp minima. A complete development supplies, on top of Mathlib, the strong law of large numbers applied to directional derivatives of convex integrands, the passage from pointwise to uniform convergence for convex functions, and the characterization of sharp minima by directional derivatives on the tangent cone. Each of these is reusable well beyond this paper.

Difficulty

The obvious argument fails at the step from convergence to exactness. Strong consistency of SAA ($\hat x_N\to\bar x$ w.p.1) says nothing about $\hat x_N$ equalling $\bar x$; for a smooth objective it never does. Exactness has to come from a first-order condition at $\bar x$ that holds with a margin, and that margin must be transferred to $\hat f_N$ uniformly over all tangent directions at once, not one direction at a time, since there are uncountably many directions and each carries its own null set. The second difficulty is that $\hat f_N$ and $f$ are typically nonsmooth (piecewise linear in the motivating examples), so the first-order objects are one-sided directional derivatives, and differentiation under the integral sign, in its usual smooth form, does not apply to them.

Formalization scope

• $\mathbb R^m$ is EuclideanSpace ℝ (Fin m). The sample is one infinite i.i.d. sequence on a separate probability space $(S,Q)$: each $\omega^j$ is measurable with law $P$, and the family is mutually independent. $\hat f_N$ uses the first $N$ terms (0-based in Lean). "W.p.1 for $N$ large enough" is ∀ᵐ s ∂Q, ∀ᶠ N in atTop, …; a fresh sample for each $N$ is not used.
• Hypothesis (ii), "$f$ well defined and finite valued", is encoded as integrability of $h(x,\cdot)$ for every $x$ (a disclosed pin, which includes measurability).
• $f$ is the Bochner integral; directional derivatives are one-sided limits (limUnder along $t\downarrow0$), used only for convex finite functions, where the limits exist. Optimal sets are defined directly as argmin sets, without infima.
• The tangent cone is Mathlib's posTangentConeAt, the cone of limits of $c_n d_n$ with $c_n\ge0$; for convex $\Theta$ it is the closure of $\mathbb R_+(\Theta-\bar x)$. Mathlib's tangentConeAt ℝ, which allows negative scalings and is symmetric, is not the paper's cone and is not used.
• Supremum limits over the unit ball are stated as uniform convergence on the closed unit ball; the Hausdorff distance is the extended-valued Metric.hausdorffEDist. Subdifferentials use the published definition ShorNonsmooth.Subdiff.subdifferential.
• Uniqueness in the goal is the set equality $\operatorname{argmin}_\Theta\hat f_N=\{\bar x\}$; the weaker "$\bar x$ is optimal for (1.2)" is not the theorem. The goal's quantifier order is "almost surely, eventually in $N$"; "for each $N$, almost surely" is a different and false statement.
• Milestones 1 and 2 are stated for an arbitrary finite convex function, which covers both $f$ and $\hat f_N$.

Contributions welcome: proofs of any milestone; in particular the convex-analysis lemmas (milestones 1, 2 and 4) need no probability, and (2.5)–(2.6) need only Mathlib's strong law.

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 (the mission cites the authors' preprint, Stochastic Programming E-Print Series).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorem 10.8, uniform convergence of convex functions). https://doi.org/10.1515/9781400873173
• J.-B. Hiriart-Urruty and C. Lemaréchal, Convex Analysis and Minimization Algorithms I, Springer, 1993 (Theorem V.3.3.8, support functions and Hausdorff distance). https://doi.org/10.1007/978-3-662-02796-7
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009 (Chapter 5, statistical inference for SAA). https://doi.org/10.1137/1.9780898718751