Optimization

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the objective only through its values: the function is computed by a black-box code, and derivatives are unavailable or too expensive to program. Zeroth-order (derivative-free) methods address this setting. Classical derivative-free methods (pattern search, Nelder–Mead, model-based trust regions) come with weak or no global complexity guarantees for convex problems.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that replacing the gradient by a finite difference along a random Gaussian direction yields methods whose expected complexity is that of the corresponding gradient method multiplied by a factor proportional to the dimension. Their paper is a standard reference for zeroth-order convex optimization and for Gaussian smoothing, and its oracle and analysis are reused in bandit convex optimization, zeroth-order stochastic optimization (e.g. Ghadimi–Lan 2013) and derivative-free reinforcement learning.

This mission concerns Section 5 of the paper: the random gradient method $\mathcal{RG}_\mu$ for smooth convex functions and its linear rate for strongly convex ones.

Setting

Let $E$ be a real inner product space of finite dimension $n$, with norm $\|\cdot\|$. (The paper works with a space carrying an operator $B = B^* \succ 0$ and norm $\|x\| = \langle Bx, x\rangle^{1/2}$; choosing $\langle B\cdot,\cdot\rangle$ as the inner product gives exactly this setting, and the dual norm $\|\cdot\|_*$ becomes the norm of the Riesz representative.)

A function $f : E \to \mathbb R$ belongs to $C^{1,1}(E)$ with constant $L_1$ if it is differentiable and $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ for all $x, y$. It is strongly convex with parameter $\tau > 0$ if $f(y) \ge f(x) + \langle \nabla f(x), y - x\rangle + \frac{\tau}{2}\|y-x\|^2$ for all $x, y$.

Let $u$ be a standard Gaussian vector of $E$ (coordinates in any orthonormal basis are independent $N(0,1)$). The Gaussian approximation of $f$ with parameter $\mu \ge 0$ is $f_\mu(x) = \mathbb E_u f(x + \mu u)$, and the moments are $M_p = \mathbb E_u\|u\|^p$. The random gradient-free oracle returns, for a sampled direction $u$,

$$B^{-1}g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u \quad (\mu > 0), \qquad B^{-1}g_0(x) = f'(x,u)\, u,$$

and the symmetric oracle is $B^{-1}\hat g_\mu(x) = \frac{f(x+\mu u) - f(x - \mu u)}{2\mu}u$.

Consider $f^* = \min_{x\in E} f(x)$ for a convex $f \in C^{1,1}(E)$, assumed solvable with a minimizer $x^*$, and $n \ge 2$. The random gradient method $\mathcal{RG}_\mu$ (Eq. (54), p. 546) is:

Method $\mathcal{RG}_\mu$: Choose $x_0 \in E$. Iteration $k \ge 0$. a). Generate $u_k$ and corresponding $g_\mu(x_k)$. b). Compute $x_{k+1} = x_k - hB^{-1}g_\mu(x_k)$.

The directions $u_0, u_1, \dots$ are independent standard Gaussian vectors, and $\phi_k = \mathbb E f(x_k)$ (with $\phi_0 = f(x_0)$).

Formalization targets

Goal: Theorem 8 (p. 546)

With step size $h = \frac{1}{4(n+4)L_1}$ and any $\mu \ge 0$, for every $N \ge 0$,

$$\frac{1}{N+1}\sum_{k=0}^{N}(\phi_k - f^*) \le \frac{4(n+4)L_1\|x_0-x^*\|^2}{N+1} + \frac{9\mu^2(n+4)^2L_1}{25},$$

and, if $f$ is strongly convex with parameter $\tau > 0$, then with $\delta_\mu = \frac{18\mu^2(n+4)^2}{25\tau}L_1$,

$$\phi_N - f^* \le \frac12 L_1\left[\delta_\mu + \left(1 - \frac{\tau}{8(n+4)L_1}\right)^{N}\big(\|x_0-x^*\|^2 - \delta_\mu\big)\right].$$

Both bounds are one theorem with one proof in the paper, so the goal states their conjunction, with every constant as printed.

Milestones

The milestones are the results the paper's proof of Theorem 8 rests on, in attack order:

1. Lemma 1 (p. 534): $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$.
2. Theorem 3.1, (32) (p. 537): $\mathbb E_u\|g_0(x)\|_*^2 \le (n+4)\|\nabla f(x)\|_*^2$ at a point of differentiability.
3. Theorem 4.2, (35) (p. 538): $\mathbb E_u\|g_\mu(x)\|_*^2 \le \frac{\mu^2}{2}L_1^2(n+6)^3 + 2(n+4)\|\nabla f(x)\|_*^2$, and the same with $\frac{\mu^2}{8}$ for $\hat g_\mu$.
4. Eq. (21) (pp. 534–535): for $\mu > 0$, $f_\mu$ is differentiable with $\nabla f_\mu(x) = \mathbb E_u B^{-1}g_\mu(x)$.
5. Eq. (25) (p. 535): $\mathbb E_u \langle\nabla f(x), u\rangle u = \nabla f(x)$, the $\mu = 0$ counterpart.
6. Convexity of $f_\mu$ (p. 533) and Eq. (11): $f \le f_\mu$ for convex $f$.
7. Theorem 1, (19) (p. 534): $|f_\mu(x) - f(x)| \le \frac{\mu^2}{2}L_1 n$.

Significance

The result. Theorem 8 shows that a method using two function values per iteration reaches accuracy $\epsilon$ on a smooth convex problem in $O(\frac{n}{\epsilon}L_1\|x_0 - x^*\|^2)$ iterations, and in $O(\frac{nL_1}{\tau}\ln\frac{L_1\|x_0-x^*\|^2}{\epsilon})$ iterations under strong convexity, provided $\mu$ is small enough. This is $n$ times the complexity of the deterministic gradient method, which is the natural price for replacing an $n$-dimensional gradient by one directional estimate. The strongly convex bound makes explicit the bias floor $\frac12 L_1\delta_\mu$ caused by the finite-difference step, and shows that it vanishes for the limiting method $\mathcal{RG}_0$.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. A formalization produces a reusable Gaussian-smoothing layer on Mathlib's stdGaussian (moments of the Gaussian norm, differentiation of $f_\mu$ under the integral, variance bounds of random oracles) and a complete expected-complexity proof of a randomized first-order method, in which the probabilistic structure (independent directions, iterates depending only on past directions, tower property) has to be handled explicitly.

Difficulty

The deterministic part of the argument is the textbook analysis of gradient descent. The difficulty is in the Gaussian facts it uses. The obvious bound on the oracle's second moment, $\mathbb E\langle\nabla f(x),u\rangle^2\|u\|^2 \le \|\nabla f(x)\|^2 M_4 \le (n+4)^2\|\nabla f(x)\|^2$, loses a factor of $n$ and would give a quadratic dependence on dimension; the $(n+4)$ of (32) needs a sharper computation. The moment bounds of Lemma 1 for non-integer $p$ and the differentiation under the integral in (21) are measure-theoretic steps that Mathlib does not package. Finally, the step from per-iteration inequalities to bounds on $\phi_k$ requires conditioning on the past directions, which must be set up on a probability space carrying the whole sequence $u_0, u_1, \dots$.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space with MeasurableSpace and BorelSpace, $n$ is Module.finrank ℝ E, and $\nabla f$ is Mathlib's gradient. Expectations over $u$ are Bochner integrals against ProbabilityTheory.stdGaussian E. A run of $\mathcal{RG}_\mu$ lives on a probability space $(\Omega, P)$: measurable directions $u_k$, jointly independent (iIndepFun) with law stdGaussian E, iterates with $x_0$ deterministic and the update holding for every $k$ and outcome. $\phi_k$ is ∫ ω, f (x k ω) ∂P. The oracle is defined by cases, with $f'(x,u)u$ at $\mu = 0$ ($f'(x,u)$ the one-sided directional derivative of Eq. (23), a Filter.limUnder, which equals fderiv ℝ f x u for differentiable $f$), so the goal covers every $\mu \ge 0$ as the paper claims. $L_1$ and $\tau$ are any constants satisfying the defining inequalities. The standing assumptions of Section 5 (convexity, a global minimizer $x^*$, $n \ge 2$) and $L_1 > 0$ are explicit hypotheses; $n \ge 2$ is needed for the constant $9/25$.

A trivializing formalization is ruled out: the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the true gradient (which would be deterministic gradient descent), and every expectation in the statements is of a quantity that is integrable under the stated hypotheses, so no bound holds through a junk value of a non-integrable integral.

A complete development needs Gaussian moment computations in finite dimension, differentiation under the integral sign for $f_\mu$, the variance bounds of the oracles, and a conditional-expectation argument for the iteration. The smoothing layer is reusable for the companion missions on random search for nonsmooth problems and on the accelerated random method, and for other zeroth-order methods. Contributions of any of the milestones, of general Gaussian-integrability lemmas, or of alternative proofs are welcome.

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4):2341–2368, 2013. https://doi.org/10.1137/120880811
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the values of an objective function but not to its gradient: the function is computed by a black-box program, by a simulator, or by a model whose derivatives are unavailable or too expensive. Zeroth-order (or derivative-free) methods use only function values. Classical direct-search methods of this kind usually come without complexity bounds.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that a very simple randomized scheme has explicit, dimension-dependent worst-case complexity bounds. The idea is to replace the gradient by a finite difference of $f$ along a random Gaussian direction. The resulting oracle is an unbiased estimate of the gradient of a smoothed version of $f$. Their analysis is the reference point for the later literature on zeroth-order stochastic optimization, bandit convex optimization and gradient-free training.

This mission covers the paper's result for nonsmooth convex problems over a closed convex set: the projected random search method $\mathcal{RS}_\mu$ and its convergence bound, Theorem 6.

Setting

Let $E$ be a real inner product space of finite dimension $n$, with norm $\|\cdot\|$. (The paper works with a space carrying a positive definite operator $B$ and the norm $\langle Bx, x\rangle^{1/2}$. This is the same thing as an arbitrary finite-dimensional inner product space, with $B$ encoding the inner product, and the development is written in that generality.)

A function $f : E \to \mathbb R$ is Lipschitz continuous with constant $L_0 \ge 0$ if $|f(x) - f(y)| \le L_0 \|x - y\|$ for all $x, y$. The paper calls this class $C^{0,0}(E)$ and writes $L_0(f)$ for the constant.

Let $u$ be a standard Gaussian vector in $E$: its coordinates in any orthonormal basis are independent $N(0,1)$ variables. For $\mu \ge 0$ the Gaussian smoothing of $f$ is

$$f_\mu(x) = \mathbb E_u\, f(x + \mu u),$$

and the Gaussian moments are $M_p = \mathbb E_u \|u\|^p$.

For $\mu > 0$ the random gradient-free oracle at $x$ draws $u$ and returns the vector

$$g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u .$$

It costs two function values.

The problem is

$$f^* = \min_{x \in Q} f(x),$$

where $Q \subseteq E$ is closed and convex, $f$ is convex and Lipschitz, and $x^* \in Q$ is a minimizer. With $\pi_Q$ the Euclidean projection onto $Q$, positive steps $h_0, h_1, \ldots$ and a starting point $x_0 \in Q$, the random search method $\mathcal{RS}_\mu$ iterates

$$x_{k+1} = \pi_Q\big(x_k - h_k\, g_\mu(x_k)\big),$$

drawing a fresh independent Gaussian direction $u_k$ at every iteration. The iterates are random. Write $\phi_k = \mathbb E f(x_k)$ and $S_N = \sum_{k=0}^N h_k$.

Formalization targets

Goal: Theorem 6

For every $N \ge 0$,

$$\frac{1}{S_N}\sum_{k=0}^{N} h_k(\phi_k - f^*) \le \mu L_0\, n^{1/2} + \frac{1}{S_N}\left[\frac12\|x_0 - x^*\|^2 + \frac{(n+4)^2}{2} L_0^2 \sum_{k=0}^{N} h_k^2\right].$$

The step sizes, the smoothing parameter and the horizon are left free, so every step-size rule in the paper follows from this one inequality. The constants are the paper's.

Milestones

The facts about smoothing and the oracle on which the goal rests, in the paper's order:

1. Lemma 1: $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$.
2. Theorem 1 (18): $|f_\mu(x) - f(x)| \le \mu L_0 n^{1/2}$.
3. Convexity of $f_\mu$ for convex $f$.
4. Eq. (11): $f_\mu \ge f$ for convex $f$.
5. Eq. (21): $\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)$ for $\mu > 0$.
6. Theorem 4.1 (34): $\mathbb E_u \|g_\mu(x)\|^2 \le L_0^2 (n+4)^2$.
7. Theorem 2 ($\mu \ge 0$): $f(y) \ge f(x) - \mu L_0 n^{1/2} + \langle \nabla f_\mu(x), y - x\rangle$ for all $y$, where at $\mu = 0$ the vector is the limiting $\nabla f_0(x) = \mathbb E_u[f'(x,u)\,u]$ of Eq. (24).

Significance

Theorem 6 shows that a method using only function values, with no subgradient, solves nonsmooth convex problems with the classical projected-subgradient guarantee. Two things change: $L_0^2$ is multiplied by $(n+4)^2$, and a bias $\mu L_0 n^{1/2}$ appears, which can be made as small as desired. With suitable $\mu$, $h_k$ and $N$ an $\epsilon$-accurate expected value is reached in $O(n^2 L_0^2 R^2/\epsilon^2)$ oracle calls. The factor $n^2$ quantifies the cost of not having gradients. The same analysis carries over to stochastic objectives (the paper's Theorem 7).

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. The mission produces a Lean development of Gaussian smoothing on an arbitrary finite-dimensional inner product space: the moment bounds, the approximation, convexity and gradient identities, and the oracle variance bound. On top of it sits the full convergence theorem for a randomized projected method, stated for the actual random process rather than for an idealized expectation recursion. The smoothing layer is reusable: the same facts underlie the smooth and accelerated random methods of the same paper and most Gaussian-smoothing analyses in zeroth-order optimization.

Difficulty

A plain subgradient analysis does not apply. The vector $g_\mu(x_k)$ is not a subgradient of $f$, nor an unbiased estimate of one. It is an unbiased estimate of the gradient of a different function, $f_\mu$, and its second moment grows with the dimension. The argument therefore has to move between $f$ and $f_\mu$ at exactly the right places, using properties of $f_\mu$ that hold for every nonsmooth Lipschitz $f$.

Those properties are genuinely analytic. Differentiating $f_\mu$ requires differentiating a Gaussian integral of a function that need not be differentiable. The moment bounds need estimates of $\mathbb E\|u\|^p$ for real $p$. In the probabilistic part, $x_k$ depends on $u_0, \ldots, u_{k-1}$, and each one-step estimate has to be integrated using the independence of $u_k$ from the past. Mathlib provides the standard Gaussian measure and independence, but no Gaussian smoothing, no projection onto convex sets and no conditional-expectation argument for this kind of recursion.

Formalization scope

The space is E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E], and $n$ is Module.finrank ℝ E. No lower bound on $n$ is assumed. The Gaussian is ProbabilityTheory.stdGaussian E, and expectations are Bochner integrals against it. $f_\mu$ is the definition smoothing, $M_p$ is moment (with real exponent Real.rpow), and $g_\mu$ is oracle.

The projection is the relation IsMetricProjection Q y z ($z \in Q$ and $z$ is a nearest point of $Q$ to $y$). The run is the predicate IsRandomSearchRun: directions $u_k : \Omega \to E$ on a probability space $(\Omega, P)$, measurable, mutually independent (iIndepFun) and each with law stdGaussian E; a deterministic $x_0 \in Q$; and the update above for every $k$ and every outcome.

$\phi_k$ is $\int f(x_k)\,dP$. The Lipschitz constant $L_0 \ge 0$ is any constant satisfying the Lipschitz inequality. It is an explicit hypothesis, because the paper's bound uses $L_0(f)$, which presupposes $f \in C^{0,0}(E)$. The smoothing parameter satisfies $\mu > 0$ and every step satisfies $h_k > 0$.

Two trivializing formalizations are ruled out. First, an expectation of a non-integrable function would be $0$ as a Bochner integral; Lipschitz continuity of $f$ makes every expectation in the mission integrable, and no statement relies on the junk value. Second, a run whose directions are not independent standard Gaussians, or whose update uses a subgradient instead of the finite difference, is a different theorem (the projected subgradient method). The run predicate fixes the paper's process exactly. A run exists for every closed $Q$ containing $x_0$ (on the countable product of Gaussians), so the goal is not vacuous.

A complete development needs:

• Gaussian integration by parts, or differentiation under the integral, for Lipschitz integrands;
• moment estimates for the standard Gaussian norm;
• existence and nonexpansiveness of projections onto closed convex sets;
• an expectation argument for the random recursion.

The smoothing lemmas, the moment bounds and the projection facts are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, general lemmas about stdGaussian and projections, and alternative proofs of Lemma 1 (for example through the chi distribution).

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
• J. C. Duchi, M. I. Jordan, M. J. Wainwright, A. Wibisono, Optimal rates for zero-order convex optimization: the power of two function evaluations, IEEE Trans. Inf. Theory 61(5):2788–2806, 2015. https://arxiv.org/abs/1312.2139

Motivation

The capacitated vehicle routing problem (CVRP) asks for delivery routes of minimum cost. Each route starts and ends at a depot, every customer is visited exactly once, and the demand served on a route does not exceed the vehicle capacity. The problem is central in logistics and one of the most studied problems in combinatorial optimization. Its standard exact methods are branch-and-cut algorithms built on the two-index vehicle flow formulation, a 0/1 program over arcs whose capacity constraints are the rounded capacity inequalities (RCIs); see Laporte, Nobert and Desrochers (1985) and Semet, Toth and Vigo (2014).

In practice customer demands are uncertain. A chance-constrained CVRP requires each route to respect its capacity with probability at least $1-\epsilon$ under a known distribution. That distribution is rarely known. Most solution methods also need independent demands. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP. There the chance constraint must hold for every distribution in an ambiguity set $\mathcal P$ of plausible distributions. The ambiguity set may contain dependent distributions and uncountably many of them, so it is not clear a priori that the problem can be solved by the usual branch-and-cut machinery. This mission formalizes the paper's answer to that question: its Theorem 1 and the counterexample that precedes it.

Setting

The graph is complete and directed. Its nodes are $V=\{0,\dots,n\}$ and its arcs are $A=\{(i,j)\in V\times V:i\neq j\}$. Node $0$ is the depot and $V_C=\{1,\dots,n\}$ are the customers. There are $m$ vehicles, indexed by $K=\{1,\dots,m\}$, each of capacity $Q>0$. Traversing the arc $(i,j)$ costs $c(i,j)\ge 0$; costs may be asymmetric.

A route $\mathbf R_k=(R_{k,1},\dots,R_{k,n_k})$ is an ordered list of customers, with $R_{k,0}=R_{k,n_k+1}=0$. A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)\in\mathfrak P(V_C,m)$ partitions $V_C$ into $m$ nonempty ordered routes. Its cost is $c(\mathbf R)=\sum_{k}\sum_{l=0}^{n_k}c(R_{k,l},R_{k,l+1})$.

The demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ is random. The ambiguity set $\mathcal P$ is a set of probability distributions of $\tilde{\boldsymbol q}$ and $\epsilon\in(0,1)$ is the risk level. The problem RVRP($\mathcal P$) minimizes $c(\mathbf R)$ over route sets such that

$$\mathbb P\Big[\textstyle\sum_{i\in\mathbf R_k}\tilde q_i\le Q\Big]\ge 1-\epsilon\qquad\forall\,\mathbb P\in\mathcal P,\ \forall\,k\in K .$$

With $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x:\mathbb Q[\tilde X\le x]\ge1-\epsilon\}$, the demand estimator of the paper's Eq. (2) is

$$d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .$$

The problem 2VF($\mathcal P$) minimizes $\sum_{(i,j)\in A}c(i,j)x_{ij}$ over $x\in\{0,1\}^A$ with in- and out-degree $1$ at every customer and $m$ at the depot, and with the RCIs

$$\sum_{i\in V\setminus S}\sum_{j\in S}x_{ij}\ge d_{\mathcal P}(S)\qquad\forall\,S\subseteq V_C,\ S\neq\emptyset .$$

A route set induces the arc vector with $x_{ij}=1$ exactly when $(i,j)=(R_{k,l},R_{k,l+1})$ for some $k,l$ (the paper's Eq. (3)). The estimator satisfies the subadditivity condition (S) if $d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)$ for all $S,T\subseteq V_C$.

Formalization targets

Goal: Theorem 1

Assume $\tilde{\boldsymbol q}\ge\mathbf 0$ $\mathbb P$-a.s. for all $\mathbb P\in\mathcal P$, and assume $d_{\mathcal P}$ is real valued and satisfies (S). Then:

$$\begin{aligned} &\text{(i)}\ \ \mathbf R \text{ feasible in RVRP}(\mathcal P)\ \Longrightarrow\ x(\mathbf R)\text{ feasible in 2VF}(\mathcal P),\ \ c(x(\mathbf R))=c(\mathbf R);\\ &\text{(ii)}\ \ x\text{ feasible in 2VF}(\mathcal P)\ \Longrightarrow\ x=x(\mathbf R)\text{ for an RVRP}(\mathcal P)\text{-feasible }\mathbf R,\text{ unique up to reordering routes},\ c(x)=c(\mathbf R). \end{aligned}$$

Milestones

1. The chance constraint $\mathbb Q[\tilde X\le\tau]\ge1-\epsilon$ is equivalent to $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]\le\tau$ (p. 720).
2. Eq. (1): a route satisfies its robust chance constraint if and only if the worst-case VaR of its cumulative demand is at most $Q$.
3. Example 1: an instance with two customers where a route set is RVRP($\mathcal P$)-feasible, yet its induced flow violates the RCI for $S=\{1,2\}$, since $d_{\mathcal P}(\{1,2\})\ge3$.
4. Example 1 (continued): on that instance $d_{\mathcal P}$ violates (S).
5. Theorem 1 (i) and 6. Theorem 1 (ii), stated separately.

Significance

Theorem 1 separates the modeling question from the algorithmic one. Whenever the ambiguity set yields a subadditive estimator, the distributionally robust CVRP is solved exactly by a two-index flow branch-and-cut. The only change from the deterministic case is the right-hand side $d_{\mathcal P}(S)$ of the RCIs, however many distributions $\mathcal P$ contains. The companion missions of this series show that (S) holds for every moment ambiguity set (Theorem 2 of the paper) and compute $d_{\mathcal P}$ for several classes of such sets. Example 1 shows that the hypothesis cannot be dropped: ambiguity sets that pin down each customer's marginal distribution break the equivalence.

The paper's proofs are in its online supplement; no machine-checked version of these statements exists. Formalizing them produces a checked reduction between a stochastic routing model and an integer program. It also produces reusable definitions of route sets, induced arc flows and RCIs over directed graphs with a depot.

Difficulty

Direction (ii) is a graph decomposition. A 0/1 vector with the prescribed degrees splits into $m$ depot cycles plus possibly depot-free subtours. The RCIs, through the $\max\{\cdot,1\}$ in $d_{\mathcal P}$, must exclude the subtours, and the RCI on the customers of a single route must enforce that route's chance constraint. Uniqueness up to reordering requires that directed routes are recovered from arcs.

Direction (i) is where (S) enters. The naive argument bounds the number of vehicles entering $S$ by $d_{\mathcal P}(S)$ directly from the chance constraints. It fails because the chance constraints control each route separately, while $d_{\mathcal P}(S)$ looks at the joint worst case of the demands in $S$; Example 1 is exactly this failure. A set $S$ is typically visited by several routes, each covering only part of it. Relating the per-route guarantees to the joint quantity $d_{\mathcal P}(S)$ needs both hypotheses of the theorem: nonnegative demands and (S).

Formalization scope

Customers are Fin n (0-based; the paper's customer $i$ is i - 1). Nodes are Fin (n+1) with the depot 0 and customer i at i.succ, and vehicles are Fin m. A route set is R : Fin m → List (Fin n): every route is nonempty and the concatenated routes are a permutation of all customers. Arc vectors are ℕ-valued functions on ordered node pairs, with values in $\{0,1\}$ and the non-arcs $(i,i)$ fixed to $0$.

Distributions are measures on Fin n → ℝ, and the ambiguity set is a set of probability measures. Chance constraints are written ENNReal.ofReal (1 - ε) ≤ P {q | …}. Value-at-risk is the published MultistageStochastic.valueAtRisk at level 1 - ε. The worst-case VaR is a real sSup and $d_{\mathcal P}$ is integer valued.

Two conventions implicit on the page are explicit hypotheses:

• $Q>0$, because (2) divides by $Q$;
• boundedness of the VaR values for every customer set, which encodes the paper's declaration $d_{\mathcal P}:2^{V_C}\to\mathbb R_+$.

A real sSup of an unbounded set is $0$ in Lean. Without the boundedness hypothesis every such estimator would silently equal $1$ and (ii) would fail. For an empty ambiguity set the Lean estimator equals $1$ on nonempty sets, as the paper's does.

The RCIs range over all nonempty customer sets with the depot on the outside. The estimator keeps the ceiling and the $\max\{\cdot,1\}$. 2VF feasibility mentions neither routes nor chance constraints. RVRP feasibility does not mention $d_{\mathcal P}$. A formalization in which either side refers to the other, or in which $d_{\mathcal P}$ drops the $\max\{\cdot,1\}$, is not this theorem.

Useful contributions include lemmas on the decomposition of degree-constrained 0/1 arc vectors into depot cycles, monotonicity of VaR under almost-sure ordering, and the CDF right-continuity behind milestone 1.

Related platform work: SupplyChainTheory_vrp formalizes a different, symmetric, unit-demand VRP and is not reused.

Selected references

• S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• G. Laporte, Y. Nobert, M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
• F. Semet, P. Toth, D. Vigo, Classical exact algorithms for the capacitated vehicle routing problem, in P. Toth, D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014, 37–57. https://doi.org/10.1137/1.9781611973594.ch2
• J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100(2):423–445, 2004. https://doi.org/10.1007/s10107-003-0481-8

Motivation

In a combinatorial auction a seller offers several indivisible items at once, and bidders value bundles of items rather than items one at a time. Allocating the items to maximize total value is the central optimization problem of the area, and it arises in spectrum licensing, procurement and transport contracting (Cramton, Shoham and Steinberg, Combinatorial Auctions, MIT Press, 2006). Two obstacles meet. Computationally, a valuation has $2^m$ numbers, so an algorithm can only query it, and even then optimization is hard. Strategically, the valuations are private: a bidder reports whatever maximizes its own utility, so an algorithm that is a good approximation on true inputs may be useless on reported ones.

The classical answer to the strategic obstacle is the VCG payment scheme, which makes truthful reporting a dominant strategy but requires the exact optimum. Nisan and Ronen (2007) showed that an approximation algorithm becomes truthful under VCG payments essentially only when it is maximal in range: it fixes a restricted set of allocations in advance and optimizes exactly over that set. Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010, §5) give such an algorithm for complement-free (subadditive) bidders that uses only value queries and loses a factor of order $\sqrt m$. For general valuations in the value-query model the paper cites a lower bound of order $m/\log m$ (Dobzinski and Schapira, working paper 2005; Blumrosen and Nisan, Hebrew University Discussion Paper 381, 2005; see the paper's references [7] and [2]), and the same paper (Theorem 6.1) shows that even XOS bidders cannot be approximated within $m^{1/2-\epsilon}$ with polynomially many value queries.

Setting

A set $M=\{1,\dots,m\}$ of items is sold to $n$ bidders. Bidder $i$ has a valuation $v_i$ that assigns a real number $v_i(S)$ to every bundle $S\subseteq M$. Throughout, valuations are normalized, $v_i(\emptyset)=0$, and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$. A valuation is complement free (CF) if $v(S\cup T)\le v(S)+v(T)$ for all bundles $S,T$. An allocation $A=(A_1,\dots,A_n)$ gives the bidders pairwise disjoint bundles (items may stay unallocated), and its social welfare is $\sum_i v_i(A_i)$.

The mechanism receives reports $b=(b_1,\dots,b_n)$ and runs the following algorithm $\mathrm{ALG}$:

1. query $b_i(M)$ and $b_i(\{j\})$ for every bidder $i$ and item $j$;
2. compute a maximum-weight matching $P$ in the complete bipartite graph between items and bidders, where the edge between item $j$ and bidder $i$ costs $b_i(\{j\})$;
3. if the bidder $t$ maximizing $b_i(M)$ has $b_t(M)$ strictly larger than the weight $|P|$, give all items to $t$; otherwise give every item matched by $P$ to its matched bidder.

Its range $R$ is the set of allocations that give all of $M$ to one bidder, together with the allocations in which every bidder receives at most one item. Under VCG payments bidder $i$ receives $\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$, so its utility is $v_i(\mathrm{ALG}(b)_i)+\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$. The mechanism is incentive compatible on a class of valuations if no bidder can raise its utility by misreporting within that class, whatever the others report.

Formalization targets

Goal: Theorem 5.1 (p. 11)

For every choice of the maximum-weight matching and of the top bidder as functions of the reports, for every profile $v$ of normalized, monotone, CF valuations and every allocation $O$,

$$\sum_{i=1}^n v_i(O_i)\;\le\;2\sqrt m\,\sum_{i=1}^n v_i\big(\mathrm{ALG}(v)_i\big),$$

and the mechanism $(\mathrm{ALG},\text{VCG payments})$ is incentive compatible on the CF valuations.

Milestones, in attack order

1. §5.1, VCG. Welfare maximization with Groves payments is incentive compatible (a published platform theorem, AGT.vcg_incentive_compatible).
2. §5.1, maximal in range. Any allocation rule that optimizes reported welfare exactly over a fixed range is incentive compatible under VCG payments on the same domain.
3. ALG is maximal in range with range $R$ on normalized reports.
4. The CF single-item bound. For a CF valuation and $c\in T$ maximizing $v(\{j\})$ over $T$: $v(T)\le\sum_{j\in T}v(\{j\})\le|T|\,v(\{c\})$.
5. First case. If bidders with $|O_i|\ge\sqrt m$ carry at least half the welfare of $O$, then $\sum_i v_i(O_i)\le 2\sqrt m\,v_t(M)$ for the top bidder $t$.
6. Second case. Otherwise some allocation in which every bidder gets at most one item has welfare at least $\sum_i v_i(O_i)/(2\sqrt m)$.

Significance

The theorem shows that, for subadditive bidders, the $\sqrt m$ barrier known for general valuations can be matched by a truthful mechanism that asks each bidder only $m+1$ value queries. It is one of the early examples of maximal-in-range mechanism design, a template later used for many truthful approximation mechanisms in combinatorial auctions, and it sits against Theorem 6.1 of the same paper, which shows that for XOS bidders no value-query algorithm with polynomially many queries does better than $m^{1/2-\epsilon}$.

The result is proved in the paper. What this mission adds is a machine-checked proof: a formal model of VCG-based mechanisms over a restricted range, a proof that the §5.2 algorithm is maximal in range for every tie-breaking of its two optimization steps, and the explicit constant $2$ in the $O(\sqrt m)$ bound. To our knowledge neither half of Theorem 5.1 is formalized elsewhere; the general VCG theorem exists on the platform in the setting of arbitrary outcome sets.

Difficulty

The approximation argument partitions the bidders of a reference allocation by whether their bundles have at least $\sqrt m$ items, and the two cases need different facts: disjointness bounds the number of large bundles by $\sqrt m$, and subadditivity bounds each small bundle by its size times its best item. A naive transcription breaks at degenerate inputs: the page divides by $|T_i|$ and writes strict inequalities, both of which fail when a bundle is empty or all values are zero, so the formal statement must be organized around non-strict bounds.

Incentive compatibility has a different obstacle. It holds only if the allocation rule depends on the reports alone and optimizes exactly over its range, including at ties between the grand bundle and the matching. The matching and the top bidder are not unique, so the proof must work for an arbitrary but fixed tie-breaking, and the welfare of the matching allocation must be identified with the matching weight, which uses normalization of every bidder who receives nothing.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity (the paper's standing assumptions, p. 1) and complement freedom are hypotheses; IsCFValuation bundles all three. An allocation is a family of pairwise disjoint bundles; unallocated items are allowed. A matching is a partial map Fin m → Option (Fin n) with no bidder matched twice.

Conventions the formalization commits to:

• Explicit constant. The paper writes $O(\sqrt m)$; its proof yields $2\sqrt m$ (both cases end with $|OPT|/(2\sqrt m)$), and the goal states $2\sqrt m$ with Real.sqrt m.
• Oracles and ties. The maximum-weight matching and the top bidder enter as functions mat, top of the report profile, each with a specification hypothesis; the goal is stated for every such pair. The algorithm reads only the reports; the tie between $b_t(M)$ and $|P|$ goes to the matching, as on the page.
• Payments. The mechanism pays each bidder $\sum_{k\ne i}b_k(\cdot)$, the paper's convention (footnote 2, p. 11); incentive compatibility is stated on the CF domain, the paper's. The local definition mirrors AGT.MechIncentiveCompatible on outcomes $a\mapsto v_i(a_i)$.
• Reference allocation. The approximation is stated against every allocation $O$, not only an optimal one; this is equivalent and avoids a junk maximum.
• Printed slips. The strict inequalities and the division by $|T_i|$ in the second case are replaced by non-strict, multiplied forms; the first case concludes for a bidder maximizing $v_i(M)$ rather than $v_i(O_i)$.
• Degenerate sizes. At $m=0$ everything is zero and the bound holds trivially; with $n=0$ no top-bidder rule exists.
• Out of scope. "In polynomial time" is a running-time claim and is not modelled.

A trivializing formalization is ruled out: the ratio is the explicit $2\sqrt m$ rather than an existential constant, incentive compatibility is over the full CF domain (not additive reports only) for a rule that cannot see true valuations, and the rules mat, top are satisfiable (a maximum over the finitely many matchings exists; a top bidder exists when $n\ge1$).

Useful infrastructure: finite maximum-weight matchings on complete bipartite graphs, subadditivity bounds over Finset sums, and a reusable lemma that maximal-in-range rules with VCG payments are truthful. Contributions of any milestone are welcome; milestones 2 and 4 are self-contained.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29:19–47, 2007. https://doi.org/10.1613/jair.2046
• S. Dobzinski, M. Schapira, Optimal Upper and Lower Approximation Bounds for k-Duplicates Combinatorial Auctions, working paper, The Hebrew University of Jerusalem, 2005 (reference [7] of the paper).
• L. Blumrosen, N. Nisan, On the Computational Power of Iterative Auctions I: Demand Queries, Discussion Paper 381, Center for the Study of Rationality, The Hebrew University of Jerusalem, 2005 (reference [2] of the paper).
• N. Nisan, Introduction to Mechanism Design (for Computer Scientists), in N. Nisan, T. Roughgarden, E. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, pp. 209–242.
• P. Cramton, Y. Shoham, R. Steinberg (eds.), Combinatorial Auctions, MIT Press, 2006.

Motivation

A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.

Timeline:

• Bagnell, Ng and Schneider (2001) considered the max–min value $\psi_\infty(\Pi, \mathcal T)$ and stated without proof that it is computed by the recursion below.
• Iyengar (Math. Oper. Res. 30(2), 2005; technical report 2003) independently proved the robust Bellman recursion for the discounted infinite-horizon case.
• Nilim and El Ghaoui (2005), Theorem 3, prove the recursion and perfect duality of the stationary discounted game. This mission formalizes that theorem.

Setting

The state space is $\mathcal X = \{1,\dots,n\}$ and the action set $\mathcal A$ is finite and nonempty. Each state–action pair has a cost $c(i,a) \ge 0$, and costs are discounted by a factor $\nu \in [0,1)$: the cost at stage $t$ is $\nu^t c(i,a)$.

Write $\Delta_n = \{p \in \mathbb R^n_+ : p^T\mathbf 1 = 1\}$ for the probability simplex. For each action $a$ and state $i$ a nonempty set $\mathcal P_i^a \subseteq \Delta_n$ is given. It is the set of distributions of the next state that nature may use from state $i$ under action $a$. No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action $a$ form the product $\mathcal P^a = \mathcal P_1^a \times \cdots \times \mathcal P_n^a$, so every row is chosen independently.

A stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ applies one decision rule $\mathbf a : \mathcal X \to \mathcal A$ at every stage; $\Pi_s$ is the set of them. A stationary policy of nature $\tau \in \mathcal T_s$ fixes one matrix $P^a \in \mathcal P^a$ for each action and uses it forever. Nature chooses after the controller.

From an initial state $i_0$, the state distribution evolves as $\mu_0 = e_{i_0}$, $\mu_{t+1}(j) = \sum_i \mu_t(i) P^{\mathbf a(i)}(i,j)$. The discounted cost is

$$C_\infty(\pi,\tau) = \sum_{t\ge 0} \nu^t \sum_i \mu_t(i)\, c(i,\mathbf a(i)).$$

The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v) = \sup\{p^T v : p \in \mathcal P\}$. The robust Bellman operator $g$ and, for a stationary policy $\pi$, the robust evaluation operator $g_\pi$ act on $v \in \mathbb R^n$ by

$$g(v)_i = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \qquad g_\pi(v)_i = c(i,\mathbf a(i)) + \nu\,\sigma_{\mathcal P_i^{\mathbf a(i)}}(v).$$

The two values of the game are

$$\phi_\infty(\Pi_s,\mathcal T_s) = \min_{\pi\in\Pi_s}\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau), \qquad \psi_\infty(\Pi_s,\mathcal T_s) = \sup_{\tau\in\mathcal T_s}\min_{\pi\in\Pi_s} C_\infty(\pi,\tau).$$

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

There is a unique $v \in \mathbb R^n$ with $v = g(v)$, i.e.

$$v(i) = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \quad i \in \mathcal X, \tag{19}$$

value iteration $v_{k+1} = g(v_k)$ converges to $v$ from every starting vector (20), and

$$\phi_\infty(\Pi_s,\mathcal T_s) = v(i_0) = \psi_\infty(\Pi_s,\mathcal T_s).$$

In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain $\sigma_{\mathcal P_i^a}(v)$ is optimal for nature (22), and for each stationary $\pi$ the worst-case cost $\sup_\tau C_\infty(\pi,\tau)$ is $v^\pi(i_0)$, where $v^\pi$ is the unique fixed point of $g_\pi$ (23).

Milestones

1. Lemma 2 (corrected): for a nondecreasing sup-norm contraction $g$ and $q \ge 0$, the program $\max q^T v$ s.t. $v \le g(v)$ has value $q^T v_\infty$ at the fixed point $v_\infty$, every feasible $v$ satisfies $v \le v_\infty$, and $v_\infty$ is the unique optimizer when $q > 0$.
2. The operators $g$ of (29) and $g_\pi$ of (30) are nondecreasing and $\nu$-Lipschitz in $\|\cdot\|_\infty$.
3. (26): $C_\infty(\pi,\tau) = \max\{v(i_0) : v(i) \le c(i,\mathbf a(i)) + \nu \sum_j P^{\mathbf a(i)}(i,j) v(j)\}$.
4. (28) ⇒ (23): $\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau) = v^\pi(i_0)$.
5. (27) ⇒ (19): $\psi_\infty(\Pi_s,\mathcal T_s) = v(i_0)$.

Significance

The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.

The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.

Difficulty

The fixed-point half is a direct application of the Banach fixed-point theorem once the $\nu$-contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.

• $C_\infty(\pi,\tau)$ is an infinite series along a Markov chain. Identifying it with the solution of a linear system requires summing a matrix geometric series.
• Nature's sets are neither closed nor convex, so its maxima are suprema that need not be attained. The worst case over $\mathcal T_s$ must be approached by rows that nearly attain the support function, with an error controlled through the contraction.
• The min–max and max–min values are taken over different information structures. Equality has to come from the fixed point, not from a minimax theorem: the policy set is finite and discrete and nature's set is not convex, so no convexity argument applies.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is $\|\cdot\|_\infty$.
• The model (RobustMDP.Discounted.Model) carries the costs, the discount $\nu \in [0,1)$ (the range printed in Theorem 3; §4 prints $(0,1)$) and the row sets. The row sets are assumed nonempty and contained in $\Delta_n$ and nothing else. Nonemptiness is implicit in the paper.
• $\Pi_s$ is Fin n → A. $\mathcal T_s$ is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.
• $C_\infty$ is a tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most $\nu^t\max c$, so the series is summable and the tsum is the limit of the $N$-stage costs, the paper's definition.
• $\sigma_{\mathcal P}$ is a real sSup. It is the genuine supremum because every set it is applied to is nonempty and inside $\Delta_n$.
• Every "max" over nature is a supremum: IsLUB, or ⨆ inside $\min_\pi\sup_\tau$, whose inner sets are shown bounded by conclusion (23). Minima over the finite $\Pi_s$ and over $\mathcal A$ are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.
• Corrected statements:
  • Lemma 2 is false as printed for $q$ with zero entries, so uniqueness of the optimizer is stated only for $q > 0$.
  • In (30), $\sigma(v^\pi)$ is read as $\sigma(v)$.
  • The proof's references to "Lemma 1", "(15) and (16)" and "(14)" are read as Lemma 2, (27)–(28) and (26).
• Defining $C_\infty(\pi,\tau)$ as the fixed point of $w = c_\pi + \nu P_\pi w$ would make milestone (26) a tautology and conclusion (23) nearly so. The cost here is the probabilistic series, and the fixed-point characterizations must be proved.
• Welcome contributions include a reusable library of discounted Markov chain costs on finite state spaces (the geometric-series identity behind (26)) and support-function lemmas on the simplex (monotonicity, the bound $\sigma_{\mathcal P}(u) - \sigma_{\mathcal P}(v) \le \|u-v\|_\infty$). Both are needed by the other missions of this series.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-processes/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

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).