Operations Research

Motivation

A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.

Timeline:

• Minkowski (1896, 1910): convex bodies, supporting planes and polyhedra in Geometrie der Zahlen, the setting Weyl's paper takes up.
• Farkas (1902): the lemma on homogeneous linear inequalities that is Weyl's Satz 3.
• Weyl (1935): the finite-basis theorem for cones (Hauptsatz, Satz 1), the duality between a cone and its extreme supports (§3), and the two descriptions of a convex polyhedron (§4). The paper states explicit conditions under which a finite system of inequalities defines a polytope.
• Motzkin (1936), Gale, Kuhn, Tucker (1951): systematic treatments of linear inequalities built on this foundation.

Setting

Write $(a x) = a_1 x_1 + \dots + a_n x_n$ for vectors of $\mathbb{R}^n$. A point system is a finite set $S \subseteq \mathbb{R}^n$. It is non-degenerate if no $\alpha \neq 0$ has $(\alpha s) = 0$ for all $s \in S$. A vector $\alpha \neq 0$ is a support of $S$ if $(\alpha s) \ge 0$ for all $s \in S$. A support is an extreme support if equality holds at $n-1$ linearly independent points of $S$. A point $x$ is representable by $S$ if $x = \sum_{s \in S} c_s s$ with all $c_s \ge 0$.

Read as inequalities $(a \xi) \ge 0$, $a \in S$, the same $S$ defines the cone $(S)$ of solutions. An extreme solution is a nonzero $\xi \in (S)$ at which $n-1$ linearly independent inequalities of $S$ are tight. The dual system $\Sigma$ consists of the inequalities $(\alpha x) \ge 0$, one for each extreme solution $\alpha$, and $(\Sigma)$ is the cone it defines.

For polytopes, Weyl passes to the hyperplane $x_n = -1$, identified with $\mathbb{R}^m$, $m = n-1$. A convex polyhedron is $\operatorname{conv} S$ for a finite $S \subseteq \mathbb{R}^m$ whose affine span is all of $\mathbb{R}^m$. Given a finite index set $J$, normals $A_j \in \mathbb{R}^m$ and constants $b_j \in \mathbb{R}$, the inequalities $A_j \cdot x - b_j \ge 0$ cut out a region

$$H = \{x \in \mathbb{R}^m : A_j \cdot x - b_j \ge 0 \ \text{for all } j \in J\}.$$

In Weyl's notation, row $j$ is $(\alpha x) \equiv \alpha_1 x_1 + \dots + \alpha_{n-1}x_{n-1} - \alpha_n \ge 0$, with $A_j = (\alpha_1,\dots,\alpha_{n-1})$ and $b_j = \alpha_n$.

Formalization targets

Goal: §4 II (pp. 302–303)

Assume no row is identically zero ($A_j \ne 0$ or $b_j \ne 0$). Then

$$H \text{ is a convex polyhedron} \iff \Big(\forall \pi' \in \mathbb{R}^m\ \exists \nu \ge 0:\ \pi' = \sum_j \nu_j A_j\Big) \ \wedge\ \Big(\exists c:\ A_j \cdot c - b_j > 0 \ \forall j\Big).$$

In words, the normals must positively span $\mathbb{R}^m$ and $H$ must contain an inner point. The goal is the equivalence, not either half alone.

Milestones, in the order the proof of §4 II uses them

1. Satz 1 (Hauptsatz), p. 291: for a non-degenerate $S$, every $x$ with $(\alpha x) \ge 0$ for all extreme supports $\alpha$ is representable by $S$.
2. Zusatz, pp. 294–295: a non-degenerate $S$ has no extreme support iff $0 = \sum_s c_s s$ with all $c_s > 0$.
3. Satz 3, p. 296 (Farkas): if $(p\xi) \ge 0$ on all of $(S)$, then $p$ is a nonnegative combination of $S$. This milestone is the published platform theorem LinearOptimization.farkas_cone_corollary.
4. Satz 6, p. 297: for non-degenerate $S$, $p \in (\Sigma)$ iff $(p\xi) \ge 0$ for all $\xi \in (S)$.
5. §3 II, p. 298: for non-degenerate $S$, every $\pi \in (S)$ is a nonnegative combination of finitely many extreme solutions.
6. Satz 9, p. 299: if $S$ is non-degenerate and $(S)$ has an inner point, then $\Sigma$ is non-degenerate.
7. §4 I, p. 301: a convex polyhedron $\operatorname{conv} S$ has an extreme support and equals the set cut out by its extreme supports.

Significance

The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data $(A, b)$: positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.

Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.

Difficulty

The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between $S$ and $\Sigma$. Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.

Formalization scope

• The homogeneous space is Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.
• Non-degeneracy is the literal condition "$(\alpha s)=0$ for all $s \in S$ implies $\alpha = 0$", not span = ⊤.
• Extreme supports and extreme solutions quantify over all vectors with the property. Positive multiples are not identified, and no representatives are chosen.
• Extreme solutions are required to be nonzero and to lie in $(S)$. This is implicit in the paper.
• §4 is stated in affine form on Fin m → ℝ, a point $x$ standing for Weyl's $(x,-1)$. Linear independence of $n-1$ homogenized points becomes affine independence of $m$ points, and non-degeneracy becomes affineSpan ℝ S = ⊤.
• A "convex polyhedron" is the hull of a finite set with full affine span. Dropping full-dimensionality would make the "only if" false, since a segment in $\mathbb{R}^2$ has no inner point.
• Added hypotheses: no zero row in the goal (Weyl's half-spaces have nonzero normal $(\alpha_1,\dots,\alpha_n)$, p. 291). Non-degeneracy of $S$ in Satz 6 and in the p. 298 representation, where it is inherited from Satz 4.
• Condition (i) of the goal is positive spanning, i.e. nonnegative coefficients. Linear spanning of $\mathbb{R}^m$ would be strictly weaker and would make the statement false.
• A trivializing formalization is ruled out: the goal is an equivalence, "convex polyhedron" is an existential over finite point sets with full affine span, and no hypothesis restricts $J$, $m$ or the data beyond the nonzero rows. For $m = 0$ the statement is true and non-vacuous.
• Useful infrastructure, reusable beyond this mission: a Minkowski–Weyl theorem for polyhedral cones in Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in $\mathbb{R}^{m+1}$ and polytopes in $\mathbb{R}^m$. Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.

Selected references

• H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici (1935), 290–306. https://doi.org/10.1007/bf01292722
• H. Weyl, The elementary theory of convex polyhedra, in: H. W. Kuhn, A. W. Tucker (eds.), Contributions to the Theory of Games I, Annals of Mathematics Studies 24, Princeton University Press, 1950.
• J. Farkas, Theorie der einfachen Ungleichungen, Journal für die reine und angewandte Mathematik 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• H. Minkowski, Geometrie der Zahlen, Teubner, Leipzig, 1896/1910.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (Minkowski–Weyl).

Motivation

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$. This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

$$\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}$$

Fix $r > 0$. For a constraint value $a$ and a multiplier $y$ put

$$\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}$$

(the two cases agree when $y + ra = 0$). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

$$L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).$$

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$. $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$, the limit of $V h'$ over $V \in \partial F(x + t h')$, $h' \to h$, $t \downarrow 0$, exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$, and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$:

$$L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,$$ $$\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.$$

All three clauses are the theorem; the last two together cover every point.

Milestones

1. $\eta \in C^1$, with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$, and $\nabla \eta$ is locally Lipschitz.
2. Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
3. Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$, $\alpha_j \to \alpha$, $t_j \downarrow 0$, then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$.
4. $\nabla\eta$ is semismooth, jointly in $(x, s)$, at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$, the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$, with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$, for all approaches $(h', \alpha') \to (h, \alpha)$, $t \downarrow 0$, including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

• $\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
• The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
• The paper's first sum prints $h(r_i, f_i(x), y_i)$; the single $r$ is used, as in the paper's definition of $h$.
• $\phi$ uses the first branch when $y + ra \ge 0$; the branches agree on the boundary. Every statement assumes $r > 0$.
• $C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
• $\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
• The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$–$\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$.
• Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$, or only the semismoothness of one term $\eta$, is not Theorem 4.1; the goal contains all three clauses for the full $L_r$. The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$. In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$. The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

$$U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.$$

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$, and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$. The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$, $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

$$U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},$$

with $\min$ read, as in the paper, "in the wide sense of $\inf$", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$.

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$. Its expected utility is the two-point objective (8),

$$U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).$$

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$; the set of their coefficients is $\mathcal Q$. Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$, each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$.

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$.

(a) If $u'$ is convex, then

$$U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.$$

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$.

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$. When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$.

Milestones

1. Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$.
2. For convex $u'$ and $s>0$, $U(p)$ is nonincreasing on $(0,1)$.
3. Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$, including the value $-\infty$.
4. Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$.
5. The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
6. Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$, and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$.

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$.

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ($u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$. With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$, a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step "$\lim_{y\to-\infty}u'(y)=\infty$" fails for affine $u$, where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$, gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$. Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$, a second-order asymptotic statement about $u$ at $-\infty$. The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$; showing that it lies below $u$ everywhere, not only near $m$, is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$. The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$. Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$. Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$, since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$. The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$, the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
• S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.

Motivation

Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.

A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.

This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice $\{0,1\}^V$, of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.

Setting

Let $V$ be a finite set (the ground set). A matroid on $V$ is a pair $(V, \mathcal B)$ where $\mathcal B$, the base family, is a nonempty family of subsets of $V$ satisfying the simultaneous exchange axiom (B): for every $J, J' \in \mathcal B$ and every $i \in J \setminus J'$, there exists $j \in J' \setminus J$ such that both

$$J - i + j := (J \setminus \{i\}) \cup \{j\} \in \mathcal B \quad\text{and}\quad J' + i - j := (J' \setminus \{j\}) \cup \{i\} \in \mathcal B.$$

Equivalently (Theorem 2.29 below), a matroid can be described by its rank function $\rho : 2^V \to \mathbb Z$, a set function satisfying:

• (R1) $0 \le \rho(X) \le |X|$ for every $X \subseteq V$;
• (R2) monotonicity: $X \subseteq Y \implies \rho(X) \le \rho(Y)$;
• (R3) submodularity: $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$.

A valuation of a base family $\mathcal B$ is a function $\omega : \mathcal B \to \mathbb R$ satisfying the axiom (VM): for every $J, J' \in \mathcal B$ and $i \in J \setminus J'$, there is $j \in J' \setminus J$ with $J - i + j, J' + i - j \in \mathcal B$ and

$$\omega(J) + \omega(J') \le \omega(J - i + j) + \omega(J' + i - j).$$

The pair $(V, \omega)$ is then a valuated matroid. For $p : V \to \mathbb R$, the perturbation of $\omega$ by $p$ is

$$\omega[-p](J) = \omega(J) - \sum_{j \in J} p(j).$$

Formalization targets

Goal: Theorem 2.32 (the valuated matroid characterization)

$$\omega \text{ is a valuation of } \mathcal B \iff \forall\, p : V \to \mathbb R,\ \{J \in \mathcal B : \omega[-p](J') \le \omega[-p](J)\ \forall J' \in \mathcal B\} \text{ is a nonempty family satisfying (B)}.$$

The right-hand side says: for every linear perturbation $p$, the set of $\omega[-p]$-maximal bases is again the base family of a matroid. The universal quantifier over $p$ is not optional — a version of this statement quantified over a single fixed $p$ is either vacuous or false, and does not capture what makes valuated matroids useful.

Milestone: Theorem 2.29 (the base-family / rank-function correspondence)

The maps

$$\rho(X) = \max\{|X \cap J| : J \in \mathcal B\}, \qquad \mathcal B = \{J \subseteq V : \rho(J) = |J| = \rho(V)\}$$

are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.

Significance

The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.

Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is elementary but has two independent halves (each map preserves its target axiom class, and the two maps compose to the identity in both directions) that must all be established; Theorem 2.32's proof, as given in the source, defers entirely to a later, more general chapter-6 theorem, so a solver working only from this mission must either reconstruct a direct combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions, a separate mission) and specialize its main theorem.

Difficulty

The obvious approach to Theorem 2.32 — fix an optimal basis $J$ for $\omega[-p]$ and try to show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies the maximizer property) in a few lines, since perturbing does not change which exchange moves are available. The converse is the substantial direction: from "the maximizer set is always a matroid, for every $p$," one must recover the single global inequality (VM) that must hold for all pairs $J, J' \in \mathcal B$, not just optimal ones. The standard argument constructs, for a given non-optimal pair, a perturbation $p$ under which that specific pair becomes simultaneously optimal, and this construction is exactly the step the book skips by citing chapter 6's general theorem. A formalization attempting to bypass this by only checking the maximizer property for a finite or generic sample of perturbations would trivialize the statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to prevent.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $2^V$ is represented as Finset (Finset V), and $V \to \mathbb R$ as a plain function type. The rank function is $\mathbb Z$-valued (matching the book's own convention for matroid rank, as opposed to the $\mathbb R$-valued conventions used from chapter 6 onward for general M-convex functions); RankOfFamily is implemented with Finset.sup over $\mathbb N$ rather than a partial max', so that it is a total function — its junk value at the empty family is never invoked, since every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own phrasing.

A trivializing formalization of the goal is one that quantifies over a single fixed $p$, or allows $\mathcal B$ to be empty; both are explicitly excluded by keeping $\mathcal B.\text{Nonempty}$ a hypothesis and $p$ universally quantified inside the theorem statement itself.

Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's Matroid structure is axiomatized via the single-element (asymmetric) exchange property, classically but not definitionally equivalent to Murota's simultaneous axiom (B) used throughout this book, and Mathlib provides no constructor recovering a base family or a Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine, reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only unrelated tropical-geometry and k-server results). Contributions to a shared DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome from later chunks of this series that build on matroid or base-polyhedron structure.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• H. Whitney, "On the abstract properties of linear dependence," American Journal of Mathematics, 57(3), 1935, pp. 509–533.
• A. W. M. Dress, W. Wenzel, "Valuated matroids," Advances in Mathematics, 93(2), 1992, pp. 214–250.
• R. A. Brualdi, "Comments on bases in dependence structures," Bulletin of the Australian Mathematical Society, 1(2), 1969, pp. 161–167.

Why robustify a sampled stochastic program

Many decision problems under uncertainty take the form of a stochastic program: choose a decision $v$ from a feasible set $\mathcal F$ to maximise the expected utility $\mathbb E_{x\sim\mu}[f(v,x)]$, where the distribution $\mu$ of the uncertain parameter $x\in\mathbb R^m$ is known only through i.i.d. samples $x_1,\dots,x_n$. The standard remedy, sample average approximation, maximises $\frac1n\sum_i f(v,x_i)$ instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.

Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with $\ell_\infty$ boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of $f$. This mission formalizes that result, Theorem 3.1.

Setting

Equip $\mathbb R^m$ with the sup norm $\|z\|_\infty=\max_k|z_k|$, its Borel $\sigma$-algebra and Lebesgue measure $dx$. The data are:

• a set of decisions $V$ and a nonempty feasible set $\mathcal F\subseteq V$;
• a utility $f:V\times\mathbb R^m\to\mathbb R$, Borel measurable in $x$ for each $v$;
• a true density $h^*$ on $\mathbb R^m$ (nonnegative, $\int h^*\,dx=1$) and i.i.d. samples $x_1,x_2,\dots$ with distribution $h^*(x)\,dx$;
• radii $\epsilon(n)>0$.

For a sample $x_1,\dots,x_n$ the boxes are $\mathcal Z_i=\{x_i+\delta\mid\|\delta\|_\infty\le\epsilon(n)\}$, and the box-robust sample objective is

$$J_n(v)=\frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)}f(v,x_i+\delta_i)=\sum_{i=1}^n\frac1n\inf_{x_i'\in\mathcal Z_i}f(v,x_i').$$

The RO solution $v(n)$ is a maximiser of $J_n$ over $\mathcal F$. The equicontinuity modulus of $f$ is

$$d(\epsilon)=\sup_{v,\,x,\ \|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|.$$

The proof works with the distribution set $\mathcal P_n$ of probability measures $\mu$ with $\mu(\bigcup_{i\in S}\mathcal Z_i)\ge|S|/n$ for every $S\subseteq\{1,\dots,n\}$, and with the uniform box kernel density estimator

$$h_n(x)=(n\epsilon(n)^m)^{-1}\sum_{i=1}^nK\Big(\frac{x-x_i}{\epsilon(n)}\Big),\qquad K(z)=\frac{\mathbf 1(\|z\|_\infty\le1)}{2^m}.$$

Formalization targets

Goal: Theorem 3.1 (p. 98)

Assume $|f(v,x)|\le C$ for all $v,x$; $d(\epsilon)\to0$ as $\epsilon\downarrow0$; $\epsilon(n)\downarrow0$ and $n\epsilon(n)^m\uparrow\infty$. Then for every choice of maximisers $v(n)$, with probability one,

$$\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx=\sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx .$$

Milestones (proof of Theorem 3.1, p. 99)

1. $h_n$ is the density of a probability measure in $\mathcal P_n$.
2. $J_n(v)\le\int f(v,x)\,h_n(x)\,dx$ for every $v$.
3. Oscillation over a box: $\sup_{\mathcal Z_i}f(v,\cdot)-\inf_{\mathcal Z_i}f(v,\cdot)\le d(2\epsilon(n))$.
4. Eq. (7): with $M_n=C\int|h_n-h^*|\,dx$, for every $v$,

$$J_n(v)-M_n\le\int f(v,x)h^*(x)\,dx\le J_n(v)+M_n+d(2\epsilon(n)).$$

5. Strong $L^1$ consistency of the box kernel density estimator: if $\epsilon(n)\to0$ and $n\epsilon(n)^m\to\infty$, then $\int|h_n-h^*|\,dx\to0$ almost surely.

Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.

Significance

Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: $f$ need only be bounded and equicontinuous in $x$, uniformly in $v$, and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, $\epsilon(n)\to0$ with $n\epsilon(n)^m\to\infty$, the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.

The result is proved in the paper, with the $L^1$ consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong $L^1$ consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.

Difficulty

The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume $(2\epsilon)^m$, and every infimum and supremum must be handled with care, since $f$ need not attain them.

The obstacle is milestone 5. Almost-sure $L^1$ convergence of $h_n$ to an arbitrary density $h^*$, with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: $h_n(x)$ is an average of $n$ terms whose law changes with $n$ through $\epsilon(n)$, and almost-sure convergence at each fixed $x$ does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random $L^1$ error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals $\int f(v,x)h^*(x)\,dx$ are Bochner integrals against Lebesgue measure of integrable integrands.
• The samples are a sequence X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; $x_1,x_2,\dots$ become X 0, X 1, …, and the $n$-th problem uses the first $n$. "With probability one" is ∀ᵐ ω ∂P.
• The goal quantifies over every selection $v(n)$ of maximisers, with no measurability assumed; a version with one chosen maximiser would be weaker and is ruled out.
• Readings and corrections of the printed text:
  • the kernel argument printed $(x-x_i)/\epsilon$ on p. 98 is read as $(x-x_i)/\epsilon(n)$, as the proof on p. 99 writes it;
  • "$\max_{v,x}|f(v,x)|\le C$" is read as the uniform bound $|f|\le C$ and the "max" in $d(\epsilon)$ as a supremum;
  • "$d(\epsilon)\downarrow0$" is read as $d(\epsilon)\to0$ as $\epsilon\downarrow0$;
  • implicit hypotheses made explicit: $\mathcal F\ne\emptyset$, $\epsilon(n)>0$, measurability of $f(v,\cdot)$, $h^*$ a Lebesgue density;
  • the monotonicity in "$\epsilon(n)\downarrow0$, $n\epsilon(n)^m\uparrow\infty$" is kept in the goal; milestone 5 uses the limits only, as the paper states it;
  • the paper's $M_n$ ("there exists $\{M_n\}\to0$") is made explicit as $M_n=C\int|h_n-h^*|$, so Eq. (7) is stated for every sample.
• Remark 3.2 and Appendix B (an integrable envelope in place of boundedness) are not part of this mission.
• Every real infimum and supremum ranges over a nonempty set of values bounded by $C$ in absolute value, so no statement holds through a junk value; a formalization in which the supremum over $\mathcal F$ or the box infimum could be vacuous is excluded.
• The definitions (boxes, $\mathcal P_n$, the kernel, the estimator, $J_n$, $d$) live in one definition file. $\mathcal P_n$ duplicates, with weights $1/n$, the distribution set of mission I; the duplication is deliberate because draft missions cannot import each other.
• Welcome contributions: the kernel density estimator and its strong $L^1$ consistency as reusable infrastructure, and any of the deterministic milestones.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• L. Devroye, The equivalence of weak, strong and complete convergence in $L_1$ for kernel density estimates, Annals of Statistics 11(3):896–904, 1983.
• L. Devroye, L. Györfi, Nonparametric Density Estimation: The $L_1$ View, Wiley, 1985.
• A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1), 1991 (reference [22] of the paper).

Motivation

Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.

The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:

• 1973, A. L. Soyster: the interval (worst-case, "box") counterpart, here called (IRC).
• 1998–1999, Ben-Tal and Nemirovski (Math. Oper. Res. 23; Oper. Res. Lett. 25), and independently El Ghaoui and co-authors: robust optimization with ellipsoidal uncertainty sets.
• 2000, this paper: the ellipsoid-plus-box counterpart (RC[ε, δ, Ω]) and Proposition 1, which bounds each constraint's violation probability by $\exp\{-\Omega^2/2\}$ under independent symmetric perturbations.
• 2004, Bertsimas and Sim (Oper. Res. 52): the budgeted counterpart, with an analogous probability bound.

Setting

An uncertain linear program is

$$\text{minimize } c^Tx\quad\text{s.t.}\quad Ex=e,\qquad Ax\le b,\qquad \ell\le x\le u,\tag{LP}$$

with $x\in\mathbb{R}^n$, $E\in\mathbb{R}^{p\times n}$, $A=(a_{ij})\in\mathbb{R}^{m\times n}$, and bounds $\ell_j\in\mathbb{R}\cup\{-\infty\}$, $u_j\in\mathbb{R}\cup\{+\infty\}$. For each inequality row $i$ a set $J_i\subseteq\{1,\dots,n\}$ lists the uncertain entries $a_{ij}$, $j\in J_i$. Only these entries are uncertain; $E,e,b,\ell,u,c$ are exact.

Given an uncertainty level $\epsilon>0$ and a feasibility tolerance $\delta>0$, write $b_i^+=b_i+\delta\max[1,|b_i|]$.

• $x$ is reliable if it is feasible for (LP) and $\sum_{j\notin J_i}a_{ij}x_j+\sum_{j\in J_i}\tilde a_{ij}x_j\le b_i^+$ for every $i$ and every choice of $\tilde a_{ij}$ with $|\tilde a_{ij}-a_{ij}|\le\epsilon|a_{ij}|$.
• In the random symmetric uncertainty model, the true coefficients are $\tilde a_{ij}=(1+\epsilon\xi_{ij})a_{ij}$, where $\xi_{ij}=0$ for $j\notin J_i$ and, for each row $i$, $\{\xi_{ij}\}_{j\in J_i}$ are independent random variables, each symmetrically distributed in $[-1,1]$.
• $x$ is almost reliable with level $\kappa$ if it is feasible for (LP) and $\Pr\{\sum_j\tilde a_{ij}x_j>b_i^+\}\le\kappa$ for every $i$.

The robust counterpart (RC[ε, δ, Ω]), with a safety parameter $\Omega>0$, has variables $x_j$, $y_{ij}$, $z_{ij}$ and constraints $Ex=e$, $Ax\le b$, $\ell\le x\le u$, $-y_{ij}\le x_j-z_{ij}\le y_{ij}$ for all $i,j$, and

$$\sum_j a_{ij}x_j+\epsilon\Big[\sum_{j\in J_i}|a_{ij}|y_{ij}+\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}\Big]\le b_i^+\qquad\forall i.$$

The interval robust counterpart (IRC[ε, δ]) has variables $x_j,y_j$ and the constraint $\sum_ja_{ij}x_j+\epsilon\sum_{j\in J_i}|a_{ij}|y_j\le b_i^+$ with $-y_j\le x_j\le y_j$, besides the nominal ones. Problem (∗) is the same with $y_j$ replaced by $|x_j|$.

Formalization targets

Goal: Proposition 1 (pp. 418–419)

If $x$ extends to a feasible solution $(x,y,z)$ of (RC[ε, δ, Ω]), then $x$ is feasible for (LP) and, for every $i$,

$$\Pr\Big\{\sum_j(1+\epsilon\xi_{ij})a_{ij}x_j>b_i+\delta\max[1,|b_i|]\Big\}\le\exp\{-\Omega^2/2\}.$$

Milestones

1. The reduction in the proof of Proposition 1 (p. 419), in corrected pointwise form: a violation of row $i$ forces $\sum_{j\in J_i}\xi_{ij}a_{ij}z_{ij}>\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}$.
2. Eq. (1), p. 419: for independent symmetric $\eta_j\in[-1,1]$ and reals $p_j$,

$$\Pr\Big\{\sum_j\eta_jp_j>\Omega\sqrt{\textstyle\sum_jp_j^2}\Big\}\le\exp\{-\Omega^2/2\}.$$

3. $x$ is reliable iff it is feasible for (∗) (p. 417).
4. (∗) is equivalent to (IRC[ε, δ]) (pp. 417–418).
5. Every feasible solution of (IRC) yields one of (RC) with $y_{ij}=y_j$, $z_{ij}=0$ (p. 420).
6. Feasibility for (LP) together with $\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+$, $\beta_i(x)=\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2}$, suffices to extend $x$ to (RC) (p. 420).
7. The ratio $\alpha_i(x)/\beta_i(x)$, $\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|$, is at most $\sqrt{\mathrm{card}(J_i)}/\Omega$, with equality attained (p. 420, corrected).

Significance

Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound $\exp\{-\Omega^2/2\}$ does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so $\Omega$ can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor $\sqrt{\mathrm{card}(J_i)}/\Omega$.

The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.

Difficulty

The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from $\xi_{ij}a_{ij}$ to $\xi_{ij}|a_{ij}|$ with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in $[-1,1]$, not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case $\sum_jp_j^2=0$ must be handled rather than assumed away.

Formalization scope

• Data are a structure UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective $c$ is omitted: no statement involves it.
• The probability space is $(S,\mathbb P)$ with IsProbabilityMeasure; the name $S$ avoids a clash with the safety parameter $\Omega$. Symmetry is equality of the laws of $\xi_{ij}$ and $-\xi_{ij}$; values lie in $[-1,1]$ at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.
• The hypotheses $\epsilon>0$, $\delta>0$, $\Omega>0$ are the paper's standing assumptions and are carried by every theorem that mentions the parameter.
• Corrections of the printed text: $a_{ij}x_i\to a_{ij}x_j$ in (IRC); $\sum_{j\in J}\to\sum_{j\in J_i}$ in (RC); the reduction of milestone 1 is stated with $a_{ij}$ and $z_{ij}$ in place of the printed $|a_{ij}|$, $x_i-y_{ij}$ and $y_j$, $y_{ij}$; and the ratio of milestone 7 carries the factor $1/\Omega$ that the printed "$\sqrt{\mathrm{card}(J_i)}$" omits.
• Ruling out trivializations: the violation event uses the signed multiplicative model $(1+\epsilon\xi_{ij})a_{ij}$, never $|a_{ij}|$ or an additive perturbation; the goal concludes both nominal feasibility (i) and the probability bound (ii′) for every row; no hypothesis excludes the degenerate case $\sum_{j\in J_i}a_{ij}^2z_{ij}^2=0$; and the probability model is satisfiable (e.g. by $\xi\equiv0$ or by Rademacher signs), so the goal is not vacuous.
• The numerical remarks of the paper (0.92, 5.24, $10^{-6}$, "at least 30") and the NETLIB case study are not formalized.
• Reusable beyond this mission: the uncertain-LP model and the three counterparts, and the tail bound (1). Contributions of general lemmas about symmetric bounded random variables are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424. https://doi.org/10.1007/s101070000163
• A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Oper. Res. 21 (1973) 1154–1157. https://doi.org/10.1287/opre.21.5.1154
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23 (1998) 769–805. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. Bertsimas, M. Sim, The price of robustness, Oper. Res. 52 (2004) 35–53. https://doi.org/10.1287/opre.1030.0065
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830