Optimization

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

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