Motivation

Many optimization problems in statistics, machine learning and operations research ask to minimize a smooth convex function over a simple convex set: a box, a ball, a simplex, a cone of positive semidefinite matrices. Projected gradient descent is the most basic first-order method for such problems. It takes a gradient step and then returns to the feasible set by Euclidean projection. Its cost per iteration is one gradient evaluation and one projection, independent of the dimension apart from the cost of manipulating vectors, which is why it remains a workhorse in very high dimension.

This mission is the fifth in a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980). Chapter 3 of the monograph treats "dimension-free" convex optimization. Its §3.2 first proves that gradient descent on a convex $\beta$-smooth function on $\mathbb R^n$ has rate $O(\beta\|x_1-x^*\|^2/t)$ (Theorem 3.3, the subject of mission IV), and then turns to the constrained case, which is the subject of this mission. The analysis follows Nesterov's Introductory Lectures on Convex Optimization (2004).

Setting

Write $x^\top y$ for the Euclidean inner product on $\mathbb R^n$ and $\|\cdot\|$ for the Euclidean norm. The constraint set $\mathcal X\subseteq\mathbb R^n$ is compact and convex; this is the standing assumption of Chapter 3. The Euclidean projection of $y\in\mathbb R^n$ onto $\mathcal X$ is

$$\Pi_{\mathcal X}(y)=\operatorname*{argmin}_{z\in\mathcal X}\|y-z\| ,$$

which exists and is unique for a nonempty closed convex set.

A differentiable function $f:\mathbb R^n\to\mathbb R$ is $\beta$-smooth on $\mathcal X$ if its gradient is $\beta$-Lipschitz there:

$$\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad(x,y\in\mathcal X).$$

It is $\alpha$-strongly convex on $\mathcal X$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac\alpha2\|x-y\|^2$ for $x,y\in\mathcal X$. A minimizer $x^*\in\mathcal X$ of $f$ over $\mathcal X$ is assumed to exist, as everywhere in the monograph.

Projected gradient descent with step size $\eta=1/\beta$ starts at $x_1\in\mathcal X$ and iterates

$$x_{t+1}=\Pi_{\mathcal X}\Bigl(x_t-\tfrac1\beta\nabla f(x_t)\Bigr)\qquad(t\ge1).$$

For a point $x$ with projected step $x^+=\Pi_{\mathcal X}\bigl(x-\frac1\beta\nabla f(x)\bigr)$, the gradient mapping is $g_{\mathcal X}(x)=\beta(x-x^+)$. Without constraints it equals $\nabla f(x)$.

Formalization targets

Goal: Theorem 3.7 (p. 270)

For $f$ convex and $\beta$-smooth on $\mathcal X$, projected gradient descent with $\eta=1/\beta$ satisfies, for every $t\ge1$,

$$f(x_t)-f(x^*)\le\frac{3\beta\|x_1-x^*\|^2+f(x_1)-f(x^*)}{t}.$$

Milestones

1. Lemma 3.1 (p. 263): for $x\in\mathcal X$ and $y\in\mathbb R^n$, $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$, and hence $\|\Pi_{\mathcal X}(y)-x\|^2+\|y-\Pi_{\mathcal X}(y)\|^2\le\|y-x\|^2$. The first claim is an already proved platform theorem.
2. (3.7) (p. 270): $\nabla f(x)^\top(x^+-y)\le g_{\mathcal X}(x)^\top(x^+-y)$ for $y\in\mathcal X$.
3. Lemma 3.6 (p. 270): for $x,y\in\mathcal X$,

$$f(x^+)-f(y)\le g_{\mathcal X}(x)^\top(x-y)-\frac1{2\beta}\|g_{\mathcal X}(x)\|^2 .$$

4. Descent and gap (pp. 270–271): $f(x_{s+1})-f(x_s)\le-\frac1{2\beta}\|g_{\mathcal X}(x_s)\|^2$ and $f(x_{s+1})-f(x^*)\le\|g_{\mathcal X}(x_s)\|\,\|x_s-x^*\|$.
5. Distances decrease (p. 271): $\|x_{s+1}-x^*\|\le\|x_s-x^*\|$.
6. Recursion and induction (p. 271): with $\delta_s=f(x_s)-f(x^*)$, $\delta_{s+1}\le\delta_s-\frac{1}{2\beta\|x_1-x^*\|^2}\delta_{s+1}^2$, and an induction on this recursion gives the bound of Theorem 3.7.

Companion: Theorem 3.10 (p. 278)

If $f$ is in addition $\alpha$-strongly convex on $\mathcal X$, with condition number $\kappa=\beta/\alpha$, then the strengthened Lemma 3.6, display (3.14), gives for every $t\ge0$

$$\|x_{t+1}-x^*\|^2\le\exp\Bigl(-\frac t\kappa\Bigr)\|x_1-x^*\|^2 .$$

Significance

Theorem 3.7 shows that a constraint set with a cheap projection costs nothing in the order of convergence: the $O(\beta\|x_1-x^*\|^2/t)$ rate of unconstrained gradient descent survives, with a constant that depends on $f(x_1)-f(x^*)$. Lemma 3.6 is the reusable part. It isolates the gradient mapping as the quantity that measures progress under constraints, and the same inequality, with a strong-convexity term added, gives the linear rate of Theorem 3.10. It is also the starting point of the analysis of proximal gradient methods for composite objectives.

All of these results are classical and proved in the textbook. As far as a search of the platform shows, none of them is formalized there. A related platform theorem on constrained gradient descent for well-conditioned functions (from Hazan's Introduction to Online Convex Optimization) bounds function values with a different exponent. It is not Theorem 3.10, which bounds distances with rate $\exp(-t/\kappa)$. This mission adds machine-checked statements of the constrained analysis in Bubeck's formulation, with the book's constants. The definitions of $\beta$-smoothness on a set, the gradient mapping and the run predicate can be reused by later missions on accelerated and proximal methods.

Difficulty

The obvious attempt is to copy the unconstrained proof, which rests on the descent inequality $f(x-\frac1\beta\nabla f(x))\le f(x)-\frac1{2\beta}\|\nabla f(x)\|^2$. That inequality fails under constraints: the projection can cut the step short, so the decrease in $f$ is not controlled by $\|\nabla f(x)\|$. At a boundary minimizer, for instance, $\nabla f(x^*)\neq0$ while no step makes progress. The proof has to replace the gradient by the gradient mapping throughout. It also has to show separately that the iterates do not move away from $x^*$, a fact that came for free without constraints from co-coercivity of the gradient (display (3.6)).

The closing induction is not routine either. The step from $s$ to $s+1$ works only from $s=2$ on, and the step from $1$ to $2$ needs a direct computation that uses the term $f(x_1)-f(x^*)$ in the numerator.

Formalization scope

• Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), and $x^\top y$ is ⟪x, y⟫_ℝ.
• Constraint set and minimizer. Every statement assumes $\mathcal X$ compact (IsCompact X) and convex (Convex ℝ X), the standing assumption of Chapter 3. Every statement about a run assumes a minimizer $x^*\in\mathcal X$ with $f(x^*)\le f(y)$ for all $y\in\mathcal X$, the monograph's standing assumption.
• Gradient. The gradient is an explicit map g with HasGradientAt f (g x) x at every point of $\mathbb R^n$, so $\nabla f(x)$ is defined at boundary points of $\mathcal X$. $\beta$-smoothness on $\mathcal X$ (IsBetaSmoothOn X f g β) asks this together with $\beta\ge0$ and the Lipschitz bound on $\mathcal X$ only. It is not the quadratic upper bound (3.4), which is a consequence.
• Strong convexity. It is the published predicate OnlineConvexOpt.ConvexBasics.StronglyConvexOn X f g α, which is display (3.13) with the same gradient map. Display (3.14) and Theorem 3.10 use $\alpha>0$.
• Projection. The projection is the published relation IsMetricProjection X y p: $p\in\mathcal X$ and $\|y-p\|\le\|y-z\|$ for every $z\in\mathcal X$. No choice function is used.
• Run. A run is IsProjGDRun X g β x: $\beta>0$, $x_1\in\mathcal X$, and for every $t\ge1$ the iterate $x_{t+1}$ is a projection of $x_t-\beta^{-1}g(x_t)$. Indices start at $1$ as in the book, and x 0 is unused.
• Gradient mapping. gradMap β x xplus $=\beta(x-x^+)$ takes the projected point of the run as an argument.
• Positivity. $\beta>0$ is assumed, as the step size $1/\beta$ requires, and $\alpha>0$ for Theorem 3.10, as $\kappa=\beta/\alpha$ requires.
• The recursion. The recursion of milestone 6 is stated multiplied by $2\beta\|x_1-x^*\|^2$, so the case $x_1=x^*$ needs no division.
• No trivial readings. A run predicate with a free step size, or $\beta$-smoothness replaced by the quadratic bound (3.4), would change the content. Both are excluded: the step is fixed to $1/\beta$, and smoothness is the Lipschitz condition on the gradient.

Contributions are welcome on any milestone. Lemma 3.1 and (3.7) need only the variational characterization of the projection. Lemma 3.6 needs the quadratic upper bound for a function whose gradient is Lipschitz on a convex set, together with the first-order characterization of convexity relative to a set. Both are of independent use. The induction milestone is a self-contained statement about real sequences.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer Academic Publishers, 2004. doi:10.1007/978-1-4419-8853-9
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press, 2022. arXiv:1909.05207

Motivation

Many convex optimization problems in machine learning and statistics have objectives that are convex but not differentiable: hinge losses, $\ell_1$ penalties, maxima of finitely many affine functions, and the dual functions of Lagrangian relaxations. Methods that rely on gradients do not apply to them directly, while cutting-plane methods such as the ellipsoid method pay a price that grows with the dimension. The projected subgradient method replaces the gradient by an arbitrary subgradient and restores feasibility by a Euclidean projection. Its guarantee depends on the dimension only through two constants, a radius $R$ and a Lipschitz constant $L$. This is the reason it, and its descendants (mirror descent, stochastic gradient descent, online gradient descent), are the standard tools for large-scale nonsmooth problems.

The rate analysed here goes back to the subgradient methods of Shor and Polyak in the 1960s and 1970s and to the lower bounds of Nemirovski and Yudin (1983). The book follows the presentation of Nesterov, Introductory Lectures on Convex Optimization (2004). The strongly convex variant with weights proportional to $s$ is from Lacoste-Julien, Schmidt and Bach (2012).

This mission is the third of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), and covers the preamble of Chapter 3, Section 3.1 and Section 3.4.1.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$. Let $\mathcal X\subseteq\mathbb R^n$ be compact and convex, and let $f$ be a convex function on $\mathcal X$ with a minimizer $x^*\in\mathcal X$.

A vector $g$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)$ for every $y\in\mathcal X$. The set of subgradients at $x$ is written $\partial f(x)$. The projection $\Pi_{\mathcal X}(y)$ of a point $y\in\mathbb R^n$ is the point of $\mathcal X$ nearest to $y$.

Fix step sizes $\eta_s>0$. Projected subgradient descent starts at some $x_1\in\mathcal X$ and iterates, for $s\ge1$,

$$y_{s+1}=x_s-\eta_s g_s,\quad g_s\in\partial f(x_s),\qquad x_{s+1}=\Pi_{\mathcal X}(y_{s+1}).$$

Any subgradient may be chosen at each step. In Section 3.1 the step is constant, $\eta_s=\eta$. The set $\mathcal X$ lies in the Euclidean ball of radius $R$ centred at $x_1$, and the subgradients have norm at most $L$.

A function $f$ is $\alpha$-strongly convex on $\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y\in\mathcal X$ and $g\in\partial f(x)$.

Formalization targets

Goal: Theorem 3.2

For every horizon $t\ge1$, projected subgradient descent with the constant step $\eta=R/(L\sqrt t)$ satisfies

$$f\Big(\frac1t\sum_{s=1}^{t}x_s\Big)-f(x^*)\le\frac{RL}{\sqrt t}.$$

Milestones

1. Lemma 3.1. For $x\in\mathcal X$ and $y\in\mathbb R^n$: $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$, already on the platform as a published theorem. The mission also states its consequence

$$\|\Pi_{\mathcal X}(y)-x\|^2+\|y-\Pi_{\mathcal X}(y)\|^2\le\|y-x\|^2 .$$

2. The per-step inequality in the proof of Theorem 3.2:

$$f(x_s)-f(x^*)\le\frac1{2\eta}\big(\|x_s-x^*\|^2-\|y_{s+1}-x^*\|^2\big)+\frac\eta2\|g_s\|^2 .$$

3. The summed inequality for any constant step $\eta>0$:

$$\sum_{s=1}^{t}\big(f(x_s)-f(x^*)\big)\le\frac{R^2}{2\eta}+\frac{\eta L^2t}{2}.$$

Companion: Theorem 3.9

If $f$ is $\alpha$-strongly convex and its subgradients are bounded by $L$, then with $\eta_s=2/(\alpha(s+1))$,

$$f\Big(\sum_{s=1}^{t}\frac{2s}{t(t+1)}x_s\Big)-f(x^*)\le\frac{2L^2}{\alpha(t+1)}.$$

Significance

Theorem 3.2 gives an oracle complexity of $O(R^2L^2/\varepsilon^2)$ for reaching an $\varepsilon$-optimal point, independent of the ambient dimension. Section 3.5 of the book shows this rate is unimprovable for black-box first-order methods once the dimension is large. Theorem 3.9 shows how strong convexity improves the rate to $O(1/t)$, with the averaging weights changed from uniform to linear. These two bounds are the reference points against which the rest of Chapter 3 and Chapters 4 to 6 (smooth, accelerated, mirror, stochastic methods) are measured.

The results are classical and their proofs are short. Formalizing them produces a reusable, machine-checked account of the basic projected first-order step: the projection inequality, the one-step distance recursion, and the telescoping argument with Jensen's inequality for averaged iterates. To our knowledge, no machine-checked proof of the averaged-iterate bound for the projected subgradient method exists in Mathlib. Related platform items cover other algorithms or other averaging schemes.

Difficulty

The arithmetic is elementary, and the obvious argument works. The care is in the bookkeeping. The projection must be shown not to increase the distance to $x^*$, which needs convexity of $\mathcal X$ and the variational characterization of the nearest point. The sum must telescope with a horizon-dependent constant step. Jensen's inequality must be applied to a finite convex combination of points of $\mathcal X$, which requires showing that the average lies in $\mathcal X$. In Theorem 3.9 the step sizes and the averaging weights are coupled, so neither can be changed independently. In Lean, the iterates are indexed from $1$ with natural-number horizons, and the bounds involve $\sqrt t$, so these casts need care.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The iterates are sequences ℕ → EuclideanSpace ℝ (Fin n) with the first iterate at index $1$. The projection is the published relation OnlineConvexOpt.FirstOrder.IsMetricProjection ($x_{s+1}\in\mathcal X$ is a nearest point to $y_{s+1}$). Subgradients are taken relative to $\mathcal X$ (Definition 1.2). A run is a predicate on the steps $s=1,\dots,t$, and every theorem holds for all runs, that is, for every choice of subgradients. Compactness and convexity of $\mathcal X$, convexity of $f$ on $\mathcal X$ and the existence of the minimizer $x^*$ are the book's standing assumptions and appear as hypotheses. $R>0$, $L>0$ and $\alpha>0$ are explicit, because Lean's division by zero would otherwise turn the step size into a junk value.

The book assumes $\|g\|\le L$ for every subgradient at every point of $\mathcal X$. With subgradients relative to a compact $\mathcal X$, that assumption can never hold at a boundary point, since every outward normal can be added to a subgradient. Stated that way the theorems would be vacuous. The mission therefore assumes the bound only for the subgradients $g_1,\dots,g_t$ that the run uses. This is a weaker hypothesis and gives a stronger, non-vacuous statement. Bounding only these subgradients is a deliberate choice, not a trivialization: the bound still constrains every quantity the conclusion depends on.

Contributions welcome: proofs of the four inequalities and of the two rates, and a reusable lemma that the convex combination of finitely many points of a convex set lies in the set, together with Jensen's inequality in the form used here.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• S. Lacoste-Julien, M. Schmidt and F. Bach, A simpler approach to obtaining an O(1/t) convergence rate for the projected stochastic subgradient method, 2012. https://arxiv.org/abs/1212.2002
• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9

Motivation

Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy $\varepsilon$. In fixed dimension $n$ the answer is of order $n\log(1/\varepsilon)$, and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.

Timeline:

• 1960: B. Grünbaum proves that every half-space whose boundary passes through the centroid of a convex body in $\mathbb R^n$ contains at least a fraction $(n/(n+1))^n \ge 1/e$ of its volume.
• 1965: A. Levin and D. J. Newman independently introduce the center of gravity method and prove its linear rate.
• 1983: A. Nemirovski and D. Yudin show that $\Omega(n\log(1/\varepsilon))$ oracle calls are necessary for small $\varepsilon$, so the method's oracle complexity is optimal.

Setting

Let $\mathcal X\subset\mathbb R^n$ be a convex body: a compact convex set with non-empty interior. Let $f:\mathcal X\to[-B,B]$ be continuous and convex, and let $x^*\in\mathcal X$ be a minimizer of $f$ on $\mathcal X$. A vector $w$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le w^\top(x-y)$ for every $y\in\mathcal X$. The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of $f$.

For a set $\mathcal S$ of finite positive volume, its center of gravity is

$$c(\mathcal S)=\frac{1}{\mathrm{vol}(\mathcal S)}\int_{x\in\mathcal S}x\,dx .$$

The center of gravity method sets $\mathcal S_1=\mathcal X$ and, for $t\ge1$, computes $c_t=c(\mathcal S_t)$, queries the first order oracle at $c_t$ to obtain a subgradient $w_t$, and sets

$$\mathcal S_{t+1}=\mathcal S_t\cap\{x\in\mathbb R^n:(x-c_t)^\top w_t\le0\}.$$

After $t$ steps it outputs $x_t\in\operatorname{argmin}_{1\le r\le t}f(c_r)$, found with $t$ calls to the zeroth order oracle.

The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.

Formalization targets

Goal: Theorem 2.1 (p. 245)

For every run of the method and every $t\ge1$,

$$f(x_t)-\min_{x\in\mathcal X}f(x)\le 2B\Big(1-\frac1e\Big)^{t/n}.$$

Milestones (proof of Theorem 2.1, pp. 246–247)

1. Lemma 2.2 (Grünbaum). If $\mathcal K$ is centered, $\int_{\mathcal K}x\,dx=0$, then for every $w\ne0$,

$$\mathrm{Vol}\big(\mathcal K\cap\{x:x^\top w\ge0\}\big)\ge\tfrac1e\,\mathrm{Vol}(\mathcal K).$$

2. (2.2). $\mathcal S_t\setminus\mathcal S_{t+1}\subset\{x\in\mathcal X:(x-c_t)^\top w_t>0\}\subset\{x\in\mathcal X:f(x)>f(c_t)\}$, hence $x^*\in\mathcal S_t$ for every $t$.
3. Volume decay. If $w_s\ne0$ for $s\le t$, then $\mathrm{vol}(\mathcal S_{t+1})\le(1-1/e)^t\,\mathrm{vol}(\mathcal X)$.
4. Shrunk copies. For $\varepsilon\in[0,1]$ and $\mathcal X_\varepsilon=\{(1-\varepsilon)x^*+\varepsilon x: x\in\mathcal X\}$, $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\,\mathrm{vol}(\mathcal X)$.
5. Values on shrunk copies. Every $x_\varepsilon\in\mathcal X_\varepsilon$ satisfies $f(x_\varepsilon)\le f(x^*)+2\varepsilon B$.

Significance

Theorem 2.1 is a linear rate whose number of queries to reach accuracy $\varepsilon$, $O(n\log(2B/\varepsilon))$, depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ($O(n^2\log(1/\varepsilon))$ queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.

On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.

Difficulty

The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to $1/e$ of the volume as $n\to\infty$, so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in $[0,\infty]$ in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with $|f|\le B$, continuity and convexity required on $\mathcal X$ only; its values off $\mathcal X$ are irrelevant. Subgradients are relative to $\mathcal X$ (Definition 1.2). A run is a predicate on sequences indexed from $1$; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer $x^*$ is a hypothesis, as in the book's standing notation; it exists here by compactness. The output $x_t$ is any argmin, so the goal bounds the minimum $\min_{1\le r\le t}f(c_r)$.

Added hypotheses, all disclosed in the statements: $n\ge1$ in the goal, because the exponent $t/n$ is undefined for $n=0$; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is $0$, which would make every unbounded convex set "centered". The milestone on volume decay assumes $w_s\ne0$, which is the book's own reduction.

The center of gravity is defined with the real volume $\mathrm{vol}(\mathcal S)$ and is meaningless when that volume is $0$ or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.

Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §2.1. https://arxiv.org/abs/1405.4980
• B. Grünbaum, Partitions of mass-distributions and of convex bodies by hyperplanes, Pacific Journal of Mathematics 10(4):1257–1261, 1960. https://doi.org/10.2140/pjm.1960.10.1257
• A. Yu. Levin, On an algorithm for the minimization of convex functions, Soviet Mathematics Doklady 6:286–290, 1965.
• D. J. Newman, Location of the maximum on unimodal surfaces, Journal of the ACM 12(3):395–398, 1965. https://doi.org/10.1145/321281.321291
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

Motivation

The vertices and edges of a convex polytope form a graph, and much of polyhedral combinatorics and of the theory of the simplex method is about that graph: how far apart two vertices can be (the Hirsch question), which graphs arise (Steinitz's theorem in dimension 3), and how robust the graph is. In 1961 M. L. Balinski proved that the graph of a full-dimensional polytope in $n$-space cannot be disconnected by deleting fewer than $n$ vertices (Pacific J. Math. 11 (1961) 431–434). The result, now called Balinski's theorem, is a standard entry in textbooks on polytopes (Grünbaum, Convex Polytopes, §11.3; Ziegler, Lectures on Polytopes, Thm 3.14) and is the starting point of the study of connectivity of polytope graphs. Its proof uses only linear programming: the improving-edge step of the simplex method and the connectivity of the graph of a face.

Timeline. Steinitz (1922) characterised the graphs of 3-polytopes as the 3-connected planar graphs, so the case $n=3$ is contained in his theorem. Balinski (1961) proved $n$-connectivity in every dimension. Whitney (1932) had shown that $n$-connectivity is equivalent to the existence of $n$ disjoint paths between any two points; Balinski gives a new proof of that equivalence through max-flow min-cut and draws the corollary that any two vertices of a full-dimensional polytope in $\mathbb R^n$ are joined by $n$ disjoint edge paths.

Setting

Fix integers $n$ (the dimension of the space) and $m$ (the number of inequalities), vectors $a_1,\dots,a_m\in\mathbb R^n$ (the rows of a matrix $A$) and $b\in\mathbb R^m$. Balinski's system (1) describes

$$S=\{X\in\mathbb R^n : AX\le b\}=\{x : \langle a_i,x\rangle\le b_i,\ i=1,\dots,m\},$$

written Hirsch.Hpoly a b in Lean. The paper assumes throughout two standing assumptions (StandingAssumptions a b):

1. the only solution to $AX\le0$ is $X=0$;
2. some $X^0$ satisfies $AX^0<b$.

A vertex of $S$ is an extreme point. An edge is a segment $[u,v]$, $u\neq v$, that is an extreme subset of $S$ (Hirsch.Adj S u v). The graph $G(S)$ (polyGraph S) has the vertices as points and the edges as lines.

A graph is $n$-tuply connected (IsNTuplyConnected G n) if it has at least $n+1$ points and remains connected after dropping out any $n-1$ or fewer points. Two points are joined by $n$ disjoint paths (HasDisjointPaths G u v n) if there are $n$ distinct paths from $u$ to $v$ which share no point other than $u$ and $v$.

Formalization targets

Goal: the THEOREM (p. 432)

$$\text{(i), (ii)}\ \Longrightarrow\ G(S)\ \text{is } n\text{-tuply connected}.$$

That is, $|\operatorname{ext} S|\ge n+1$ and $G(S)-X$ is connected for every set $X$ of at most $n-1$ vertices.

Milestones, in the order the proof uses them

1. $S$ has finitely many vertices, $S=\operatorname{conv}(\operatorname{ext}S)$, and $S$ lies in no hyperplane $\{\langle c,x\rangle=d\}$, $c\neq0$ (p. 432).
2. $|\operatorname{ext}S|\ge n+1$ (p. 432).
3. Preliminary remark: every vertex has degree at least $n$ in $G(S)$ (p. 432).
4. Improving neighbour: if $\langle c,\cdot\rangle$ is not maximal on $S$ at a vertex $v$, some neighbour $w$ of $v$ has $\langle c,w\rangle>\langle c,v\rangle$ (p. 432, case (a)).
5. The graph of a face is connected (p. 433, case (a)); this is the published, proved Hirsch.face_connected.
6. Two vertices with $\langle c,\cdot\rangle>d$ are joined by a path in $G(S)$ all of whose points satisfy $\langle c,\cdot\rangle>d$ (pp. 432–433, case (a)).
7. COROLLARY (p. 434): any two distinct vertices are joined by $n$ disjoint paths:

$$u\neq v\ \Longrightarrow\ \exists\,P_1,\dots,P_n:\ P_i\cap P_j\subseteq\{u,v\}\ (i\neq j).$$

Significance

The result. Balinski's theorem says that polytope graphs are highly connected, which constrains which graphs can be graphs of $n$-polytopes and is the base case of later results on the connectivity of polytope graphs. Together with Whitney's theorem it gives $n$ vertex-disjoint edge paths between any two vertices. The improving-neighbour step is the local optimality criterion of the simplex method.

Formalizing it. The theorem is classical and proved; it has not been formalized. On this platform the case $n=1$ (the graph of a polytope is connected) is proved as Hirsch.graph_connected_general, and connectivity of the graph of each face as Hirsch.face_connected, both by Shuze Chen; LinearOptimization.polyhedron_bounded_convex_hull_extreme proves the convex-hull clause of milestone 1 for a matrix-form polyhedron under the hypotheses "nonempty and bounded", and ConnPreservingHamPath.IsKConnected.le_ncard_neighborSet proves "connectivity at most minimum degree" for its own notion of $k$-connectivity. This mission adds vertex $n$-connectivity in every dimension, the simplex improving-neighbour lemma for H-polytopes, and the corollary on disjoint paths. The corollary needs Whitney's theorem, which is the goal of the companion mission On the Graph Structure of Convex Polyhedra in n-Space II.

Difficulty

An induction on dimension through facets does not directly control where the deleted vertices lie. Balinski's argument leans on several facts the paper calls obvious or clear: that a vertex with no improving neighbour is optimal, that the graph of a face is connected, that $n$ points of $\mathbb R^n$ lie on a common hyperplane while $S$ does not, and that $S$ has at least $n+1$ vertices. Each needs its own development from the two algebraic assumptions, in particular the passage from (i)–(ii) to a bounded full-dimensional polytope with finitely many vertices, and the identification of extreme segments with edges. Deleting fewer than $n-1$ vertices, which the definition requires and the proof's text does not treat, needs a separate argument. The proof also tacitly needs the affine function to take a nonzero value at some vertex.

Formalization scope

• Space: EuclideanSpace ℝ (Fin n); rows a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ. The published Hirsch_model names the dimension d and the number of rows n; here $n$ is the dimension, as in the paper.
• The two standing assumptions are hypotheses of every theorem, stated literally, not replaced by "bounded and full-dimensional".
• Vertices are Set.extremePoints ℝ S; edges are Hirsch.Adj (extreme segments). $G(S)$ is a SimpleGraph on the vertex subtype.
• Counts use Set.encard; "$n-1$ or fewer points" is X.encard < n. A path of the paper is a Mathlib Walk (consecutive points distinct).
• Explicit readings of loose phrases: "form a graph" includes finiteness of the vertex set (milestone 1); "lies within no hyperplane" is "for every $c\neq0$ and $d$ some point of $S$ has $\langle c,x\rangle\neq d$"; "whose graph is clearly connected" is the referenced Hirsch.face_connected; the affine function $y_0$ of the proof is an arbitrary $x\mapsto\langle c,x\rangle-d$, and only the "maximum"/"$>$" forms are stated (the others follow for $-c,-d$); "at least $n$ disjoint paths between any pair of vertices" is a family of $n$ pairwise distinct paths without repeated points, sharing only their endpoints, between two distinct vertices.
• Trivializing formalizations are ruled out: edges are not arbitrary pairs of vertices (that makes the goal nearly free), $n$-tuply connected requires both the point count and connectivity after deletion, and the disjoint paths must be pairwise distinct (otherwise $n$ copies of one edge would do).
• Welcome contributions: the passage from (i)–(ii) to a polytope (finiteness of vertices, Krein–Milman in this setting), the simplex optimality criterion for H-polytopes, and conversion between Hirsch walk vocabulary and Mathlib Walks; all are reusable beyond this mission.

Selected references

• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
• A. W. Tucker, Linear inequalities and convex polyhedral sets, Proc. Second Symposium in Linear Programming, Washington D.C., 1955, 569–602.
• B. Grünbaum, Convex Polytopes, 2nd ed., Springer GTM 221, 2003, §11.3. https://doi.org/10.1007/978-1-4613-0019-9
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Theorem 3.14. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

In robust optimization, a constraint is checked against every parameter value in an uncertainty set. This turns uncertainty into a deterministic optimization problem, but the set must be chosen carefully: a large set can make decisions unnecessarily conservative, while a small one can miss likely outcomes. Bertsimas, Gupta and Kallus use data to calibrate sets through statistical confidence regions. Their question is whether feasibility for every parameter in the set protects a decision against a fresh uncertain outcome with a specified probability. This mission treats the part of their construction based on estimated first and second moments. Bertsimas, Gupta and Kallus, §8.1.

The moment region originates in a concentration result attributed in the paper to Shawe-Taylor and Cristianini. That result bounds the distance between sample and population means and covariances when the uncertain vector is supported in a Euclidean ball. Bertsimas, Gupta and Kallus also discuss replacing those analytic thresholds with bootstrap thresholds; they describe the resulting coverage as approximate. The present target concerns the mathematical relation between a fixed moment region and its uncertainty set, leaving the statistical calibration of the thresholds to its cited source. Shawe-Taylor and Cristianini, 2003; Bertsimas, Gupta and Kallus, pp. 24–25.

Setting

Let the uncertain vector $\tilde u$ take values in $\mathbb R^d$. A probability law $P$ belongs to the moment confidence region $\mathcal P^{CS}$ when it is supported in the Euclidean ball of radius $R$, its mean $m_P$ is within $\Gamma_1$ of an estimate $\hat\mu$, and its covariance $S_P$ is within $\Gamma_2$ of an estimate $\hat\Sigma$ in Frobenius norm. The covariance is $S_P=\mathbb E_P[\tilde u\tilde u^\top]-m_Pm_P^\top$. The thresholds $\Gamma_1,\Gamma_2$ are nonnegative and can be chosen by either calibration procedure discussed in the paper. Bertsimas, Gupta and Kallus, Theorem 9 and (33).

For a vector $v$, Value at Risk $\operatorname{VaR}^{P}_{\varepsilon}(v)$ is the smallest threshold $t$ for which $P(\tilde u^\top v\le t)\ge1-\varepsilon$. The support function of a set $\mathcal U$ is $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$. The authors construct the set

$$\mathcal U^{CS}_{\varepsilon} =\{\hat\mu+y+C^\top w:\|y\|_2\le\Gamma_1,\ \|w\|_2\le\sqrt{1/\varepsilon-1}\}, \qquad C^\top C=\hat\Sigma+\Gamma_2 I.$$

Here $0<\varepsilon<1$ is the allowed violation probability, $I$ is the identity matrix, and $C$ is a matrix factor of the adjusted covariance. The estimates and $C$ stay fixed while $\varepsilon$ varies. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization targets

The first milestone bounds the quantile for every law in the moment region:

$$\operatorname{VaR}^{P}_{\varepsilon}(v)\le \hat\mu^\top v+\Gamma_1\|v\|_2+ \sqrt{\frac{1-\varepsilon}{\varepsilon}} \sqrt{v^\top(\hat\Sigma+\Gamma_2I)v} \quad(P\in\mathcal P^{CS}).$$

The second milestone evaluates the two linear maxima over the Euclidean balls in $\mathcal U^{CS}_{\varepsilon}$ and identifies $\|Cv\|_2$ with the quadratic form above. The goal, the deterministic part of Theorem 10, says the displayed bound equals $\delta^*(v\mid\mathcal U^{CS}_{\varepsilon})$ for every $v$, while the set is nonempty, convex and compact. This gives the support-function criterion of Theorem 1 for each law in the region. A companion formalizes Theorem 13(a): the resulting support constraint is separately convex in $(v,t)$ and in $\varepsilon$ for $0<\varepsilon<3/4$. Bertsimas, Gupta and Kallus, Theorems 10 and 13(a).

Significance

The support formula turns a distributional statement about an entire region of probability laws into a deterministic bound on a linear projection. It gives the robust model an explicit quantity to compare with a constraint threshold. The companion convexity result describes which risk levels allow separate convex optimization in the decision variables and the violation probability. Together they explain why the particular set in (35) is useful beyond the fact that it contains plausible uncertain vectors. Bertsimas, Gupta and Kallus, §§8.1 and 9.

The paper proves the mathematical construction and cites statistical results for the region's coverage. In Lean, the published Value-at-Risk and support-function definitions are already available, while this paper's moment region and set (35) need their own definitions. Formalizing the result therefore establishes a reusable interface between moment bounds, quantiles and set support. The theorem statements in this proposal are open proof targets; compiling them checks their types, not their proofs.

Difficulty

A bound on the mean and covariance does not directly bound a high quantile of every projection. The bound must work simultaneously for every probability law in the moment region, including discrete laws and singular covariances. The factor $\sqrt{(1-\varepsilon)/\varepsilon}$ is essential: replacing it by a standard deviation or a Gaussian quantile would change the claim. On the set side, the ordinary norm of a Lean function vector is a sup norm, whereas both balls in (35) are Euclidean. Getting the norm wrong changes the support function. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization scope

Vectors are functions on Fin d, whose coordinates start at zero. enorm and frob explicitly compute the Euclidean and Frobenius norms. The ball-support condition in $\mathcal P^{CS}$ secures finite first and second moments; no density is assumed. The goal fixes $R\ge0$, $\Gamma_1,\Gamma_2\ge0$, $0<\varepsilon<1$, and $C^\top C=\hat\Sigma+\Gamma_2I$. This factor relation makes the quadratic form nonnegative; a separate positive-semidefinite assumption on $\hat\Sigma$ is unnecessary. The matrix need not be triangular because (35) and its support depend on $C^\top C$. The uncertainty set's nonemptiness and compactness appear in the goal so the real support-function supremum cannot take Lean's default value for an empty or unbounded set.

Theorem 10's sampling claim is represented by its deterministic criterion for each $P\in\mathcal P^{CS}$. The confidence-region coverage of Theorem 9 is cited, and the bootstrap coverage discussed on p. 25 is approximate; neither is asserted as an exact probability theorem here. Equation (34) prints an equality for a supremum over $\mathcal P^{CS}$, yet that region restricts support to a ball, and the page does not establish attainment under that restriction. This mission uses the upper-bound direction needed for Theorem 10 and does not assert the equality or Remark 16's exact equivalence. The scope includes a sharp quantile bound, the exact support formula and the $3/4$ convexity range; a definition that merely makes the claim true by construction would miss these targets. Bertsimas, Gupta and Kallus, pp. 24–25 and 29.

Selected references

• D. Bertsimas, V. Gupta and N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised in Mathematical Programming 167 (2018), 235–292. arXiv preprint.
• J. Shawe-Taylor and N. Cristianini, Estimating the Moments of a Random Vector with Applications, 2003. University of Southampton ePrint.
• G. C. Calafiore and L. El Ghaoui, On Distributionally Robust Chance-Constrained Linear Programs, Journal of Optimization Theory and Applications 130 (2006), 1–22. DOI.

Motivation

A robust linear constraint $u^\top v \le t$ with $u$ ranging over an uncertainty set $\mathcal U\subseteq\mathbb R^d$ is tractable whenever the support function $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ is. Robust optimization gains a probabilistic meaning when $\mathcal U$ is chosen so that every robustly feasible decision also satisfies the constraint with probability at least $1-\varepsilon$ under the true distribution $\mathbb P^*$ of the uncertain parameter $\tilde u$. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region $\mathcal P$ of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over $\mathcal P$.

Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set $\mathcal U^{FB}_\varepsilon$ of Theorem 6, whose support function has a closed form.

Setting

The uncertain parameter $\tilde u$ takes values in $\mathbb R^d$ and $\mathbb P$ is its law. For $\varepsilon\in(0,1)$ and $v\in\mathbb R^d$, the Value at Risk is

$$\mathrm{VaR}^{\mathbb P}_\varepsilon(v)=\inf\{t:\mathbb P(\tilde u^\top v\le t)\ge1-\varepsilon\}.$$

For a probability measure $\mathbb P_i$ on $\mathbb R$ with mean $\mu_i$, the forward deviation and the backward deviation are

$$\sigma_f(\mathbb P_i)=\sup_{x>0}\sqrt{-\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{x\tilde u_i}]},\qquad\sigma_b(\mathbb P_i)=\sup_{x>0}\sqrt{\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{-x\tilde u_i}]}.$$

From a sample, a bootstrap produces thresholds $t_i$, $\bar\sigma_{fi}$, $\bar\sigma_{bi}$. With the sample mean $\hat\mu_i$ put $m_{bi}=\hat\mu_i-t_i$ and $m_{fi}=\hat\mu_i+t_i$. The confidence region $\mathcal P^{FB}$ consists of the distributions of vectors with independent components $\tilde u_i\sim\mathbb P_i$, each $\mathbb P_i$ having bounded support, mean in $[m_{bi},m_{fi}]$, $\sigma_f(\mathbb P_i)\le\bar\sigma_{fi}$ and $\sigma_b(\mathbb P_i)\le\bar\sigma_{bi}$.

The uncertainty set is

$$\mathcal U^{FB}_\varepsilon=\Big\{y_1+y_2-y_3:\ y_2,y_3\in\mathbb R^d_+,\ \sum_{i=1}^d\Big(\frac{y_{2i}^2}{2\bar\sigma_{fi}^2}+\frac{y_{3i}^2}{2\bar\sigma_{bi}^2}\Big)\le\log(1/\varepsilon),\ m_{bi}\le y_{1i}\le m_{fi}\Big\}.$$

Formalization targets

Goal: Theorem 6

For $m_b\le m_f$, $\bar\sigma_f,\bar\sigma_b>0$ and $\varepsilon\in(0,1)$, the set $\mathcal U^{FB}_\varepsilon$ is nonempty, convex and compact,

$$\delta^*(v\mid\mathcal U^{FB}_\varepsilon)=\sum_{i:v_i\ge0}m_{fi}v_i+\sum_{i:v_i<0}m_{bi}v_i+\sqrt{2\log(1/\varepsilon)\Big(\sum_{i:v_i\ge0}\bar\sigma_{fi}^2v_i^2+\sum_{i:v_i<0}\bar\sigma_{bi}^2v_i^2\Big)}\qquad(24)$$

for every $v$, and $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)$ is at most the right-hand side of (24) for every $\mathbb P\in\mathcal P^{FB}$ and every $v$.

Milestones

1. The Chen–Sim–Sun bound (22): for independent components with known means $\mu_i$ and deviations, $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\sum_i\mu_iv_i+\sqrt{2\log(1/\varepsilon)(\sum_{v_i<0}\sigma_{bi}^2v_i^2+\sum_{v_i\ge0}\sigma_{fi}^2v_i^2)}$.
2. The right-hand side of (24) is the worst case of (22) over the parameters allowed by $\mathcal P^{FB}$.
3. Lagrangian strong duality for $\max_{u\in\mathcal U^{FB}_\varepsilon}u^\top v$.
4. The three one-dimensional sub-subproblems and their optimal values.
5. The combined formula: $\delta^*$ equals a linear term plus $\inf_{\lambda>0}\{\lambda\log(1/\varepsilon)+S/(2\lambda)\}$.
6. $\inf_{\lambda>0}\{\lambda L+S/(2\lambda)\}=\sqrt{2LS}$, attained at $\lambda^*=\sqrt{S/(2L)}$ when $S>0$.

Companions

• Remark 9: when (24) exceeds $t$, an explicit point of $\mathcal U^{FB}_\varepsilon$ gives a violated cut $u^\top v\le t$.
• Theorem 13(b): the constraint $\delta^*(v\mid\mathcal U^{FB}_\varepsilon)\le t$ is convex in $(v,t)$ and convex in $\varepsilon$ for $0<\varepsilon<1/\sqrt e$.

Significance

Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level $\varepsilon$ for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, $\mathcal U^{FB}_\varepsilon$ needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels $\varepsilon_j$ across several constraints.

The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values $v_i\bar\sigma^2/(2\lambda)$, which should be $v_i^2\bar\sigma^2/(2\lambda)$, and the bound $m_b\le y_1\le m_b$). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.

Difficulty

The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over $\mathcal P^{FB}$ is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of $v_i$. The Value at Risk bound needs independence of the components; without it (22) fails. When $v=0$ or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.

Formalization scope

Vectors are Fin d → ℝ, with 0-based coordinates; $\tilde u^\top v$ is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\varepsilon$, and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of $\mathcal U^{FB}_\varepsilon$, so the supremum is a true maximum and cannot hold through the value $0$ of an empty or unbounded set.

The statement is formalized in the criterion form: $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\delta^*(v\mid\mathcal U^{FB}_\varepsilon)$ for all $v$ and every $\mathbb P$ in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability $1-\alpha$ with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.

Conventions and added hypotheses:

• $\bar\sigma_{fi},\bar\sigma_{bi}>0$, so that the denominators of (23) are genuine; with $\bar\sigma=0$ Lean's $x/0=0$ would leave $y_2$ unconstrained instead of forcing $y_2=0$.
• $m_b\le m_f$, which holds because $t_i\ge0$.
• The region is built from a product measure (independence) of probability measures with bounded support. These are the hypotheses of Theorem 6 on $\mathbb P^*$ and the section's standing assumption; the page's set-builder for $\mathcal P^{FB}$ omits independence. Without bounded support, the Bochner integral of a non-integrable exponential is $0$ in Lean and the deviation conditions would lose their meaning.
• "$\sigma_f(\mathbb P_i)\le\bar\sigma$" is the predicate "the expression under the root is at most $\bar\sigma^2$ for every $x>0$", which is equivalent and avoids an unbounded supremum.
• Dual minimisations over $\lambda\ge0$ are infima over $\lambda>0$, stated with IsGLB.

A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about $0$.

The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

Motivation

Robust optimization replaces uncertain data by a set of possible values and requires a decision to work for every value in that set. A central question is how to choose the set from data so that robust feasibility also gives a specified chance of satisfying the original constraint. Bertsimas, Gupta, and Kallus study this question for several sampling models in Data-Driven Robust Optimization. Their finite-support construction addresses a practical case: the uncertain vector can take one of finitely many known outcomes, while their probabilities must be inferred from observations. The resulting sets use classical goodness-of-fit tests to account for uncertainty in those probabilities. Bertsimas, Gupta, and Kallus, §§2–4, pp. 2–13.

In this case the support vectors are known in advance, so the problem is not to discover which outcomes are possible. The question is how much confidence to place in their estimated frequencies and how to turn that confidence region into a set of uncertain vectors suitable for a robust constraint. The paper gives two answers, one based on Pearson's chi-square statistic and one based on the likelihood-ratio, or G, statistic. Both answers are meant to work at every requested risk level $0<\epsilon<1$ for the same observed sample. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13.

Setting

Let $a_0,\ldots,a_{n-1}\in\mathbb R^d$ be the listed possible outcomes. A probability vector $p=(p_j)$ belongs to the simplex $\Delta_n$ when all $p_j$ are nonnegative and $\sum_jp_j=1$. It determines the finite-support law $P_p=\sum_jp_j\delta_{a_j}$. From a sample one obtains the empirical frequencies $\hat p\in\Delta_n$. A nonnegative number $\rho$ records the test threshold; in the paper it is $\chi^2_{n-1,1-\alpha}/(2N)$, where $N$ is sample size and $\alpha$ is the test's significance level. Bertsimas, Gupta, and Kallus, (10), p. 12.

The Pearson confidence region $\mathcal P^{\chi^2}$ contains candidates $p\in\Delta_n$ satisfying $\sum_j(p_j-\hat p_j)^2/(2p_j)\le\rho$. The G confidence region $\mathcal P^G$ instead requires $D(\hat p,p)\le\rho$, with relative entropy $D(r,p)=\sum_jr_j\log(r_j/p_j)$. In either region, a candidate $p_j=0$ is excluded when $\hat p_j>0$: the source's divergence is then infinite. If both entries are zero, that coordinate contributes zero. These conventions matter because ordinary real division and logarithm in Lean have total values at zero. Bertsimas, Gupta, and Kallus, (10), p. 12.

For a direction $v\in\mathbb R^d$, value at risk $\operatorname{VaR}^{P_p}_\epsilon(v)$ is the lower $1-\epsilon$ quantile of the scalar loss $u^{\mathsf T}v$. Conditional value at risk is the minimum over real $t$ of $t+\epsilon^{-1}\sum_jp_j(a_j^{\mathsf T}v-t)^+$. The paper's auxiliary set $U^{\operatorname{CVaR}_{P_p}}_\epsilon$ reweights the outcomes with another probability vector $q$ constrained by $q_j\le p_j/\epsilon$. The two data-driven uncertainty sets $U^{\chi^2}_\epsilon$ and $U^G_\epsilon$ allow such a reweighting for some $p$ in the corresponding confidence region. Their support function $\delta^*(v\mid U)$ is the largest $u^{\mathsf T}v$ over $u\in U$. Bertsimas, Gupta, and Kallus, (11)–(13), pp. 12–13; Theorem EC.1, p. ec2.

Formalization targets

The first target is the paper's finite-support CVaR identity and the comparison between the two risk measures:

$$\operatorname{VaR}^{P_p}_\epsilon(v) \le \operatorname{CVaR}^{P_p}_\epsilon(v) =\delta^*(v\mid U^{\operatorname{CVaR}_{P_p}}_\epsilon).$$

The goal is Theorem 4's deterministic claim, simultaneously for all $0<\epsilon<1$. For each $p$ in the relevant confidence region, it asks for both bounds

$$\operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^{\chi^2}_\epsilon), \qquad \operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^G_\epsilon)$$

for every $v$, with each uncertainty set nonempty, convex, and compact. A supporting milestone identifies each support function as the supremum of CVaR over its confidence region. The paper also displays conic optimization programs for these support functions in (14) and (15); those programs are outside this mission's drafted statements. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13; proof, p. ec2.

Significance

The bounds give a way to certify the directional risk of every candidate distribution accepted by a goodness-of-fit test. For a nonempty convex compact uncertainty set, the paper's Theorem 1 turns this directional condition into a probabilistic guarantee for every constraint concave in the uncertain vector. Theorem 4 adds the sampling claim through coverage of the confidence region: when the true finite-support distribution belongs to that region, the whole family indexed by $\epsilon$ receives the guarantee. The statistical tests use chi-square approximations, so their advertised coverage is asymptotic rather than an exact finite-sample result. Bertsimas, Gupta, and Kallus, Theorems 1–4, pp. 10–13.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its finite-dimensional definitions, the CVaR identity, the worst-case support identities, and the deterministic risk bounds. The drafted Lean statements are open goals. A completed development would also give reusable facts about finite-support risk measures and support functions under divergence-constrained probabilities. It would leave the test coverage calculation and the explicit programs (14)–(15) for separate work.

Difficulty

The risk comparison alone does not identify a robust uncertainty set: the support function must agree with the worst-case CVaR over an entire region of probability vectors. This brings a finite-dimensional optimization identity into the formal proof, including attainment and the relationship between reweightings and distributions. Boundary coordinates create another difficulty. The Pearson expression divides by $p_j$, and the G expression contains $\log(\hat p_j/p_j)$; silently accepting Lean's values at zero would enlarge the regions and change the theorem. The support function and CVaR are real infima or suprema, so their nonempty, bounded domains must also be established. Bertsimas, Gupta, and Kallus, (10)–(13), pp. 12–13; proof, p. ec2.

Formalization scope

Lean represents outcomes and probability vectors as functions on Fin d and Fin n; indices start at zero. The simplex is Mathlib's stdSimplex. The law is a finite sum of point masses. If two listed vectors coincide, their point masses aggregate; the paper's notation $p_j=P_p(\tilde u=a_j)$ is recovered with the intended distinct listing. Value at risk and the support function reuse published Prove2Me definitions; the finite-vector relative entropy also reuses a published definition, guarded at zero in this mission's G region. CVaR uses a real sInf, equal to the paper's minimum for a simplex law and $0<\epsilon<1$. No statement applies it outside that domain.

The goal assumes $\hat p\in\Delta_n$ and $\rho\ge0$. These express, respectively, that the center is an empirical probability vector and that the chi-square threshold is nonnegative. It quantifies over every $0<\epsilon<1$, with the same confidence regions for all levels. The paper's sample size, chi-square quantile, and significance level are compressed into $\rho$; coverage of the true distribution by the test is a separate statistical premise and is not formalized here. The source's $\mathbb P^*$ is represented by $P_{p^*}$ for a supported probability vector $p^*$. The draft does not treat an arbitrary unsupported law as a member of the confidence region.

The nonempty and compact conclusions rule out a zero returned by a support function on an empty or unbounded set. The zero-denominator guards rule out candidates the paper assigns infinite divergence. Contributions needed to close the mission include finite-simplex geometry, the finite-support CVaR identity, continuity of the divergence regions at boundary coordinates, and the risk-bound theorem. Those facts can be reused in later data-driven robust optimization developments.

Selected references

• Dimitris Bertsimas, Vishal Gupta, and Nathan Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised version in Mathematical Programming 167 (2018), 235–292. Preprint.

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$, whose parameter $\tilde{\mathbf u}\in\mathbb R^d$ is random, by the requirement that the constraint hold for every $\mathbf u$ in a chosen uncertainty set $\mathcal U$:

$$f(\mathbf u,\mathbf x)\le 0\qquad\forall\,\mathbf u\in\mathcal U .$$

The resulting problem is deterministic and, for many shapes of $\mathcal U$, tractable (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009). The modelling question it leaves open is how to choose $\mathcal U$. A set that is too large makes every solution conservative; a set that is too small gives no protection. The practitioner's real requirement is usually probabilistic: a robust feasible $\mathbf x$ should violate the uncertain constraint with probability at most $\epsilon$.

Bertsimas, Gupta and Kallus (Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167, 2018) build uncertainty sets directly from data so that this requirement holds with high confidence. Their whole construction rests on one characterization, Theorem 1 of the paper, of when a set carries such a guarantee. This mission formalizes that characterization and the two results (Theorems 2 and 3) that turn it into a data-driven recipe.

Earlier work used the "if" direction of the characterization for bi-affine constraints when designing sets for specific distributional assumptions (Ben-Tal et al., 2009; Chen, Sim and Sun, Oper. Res. 55, 2007). The extension to every constraint concave in $\mathbf u$ is due to Bertsimas, Gupta and Kallus.

Setting

Let $\mathbb P$ be a probability measure on $\mathbb R^d$, the law of $\tilde{\mathbf u}$, and fix a level $0<\epsilon<1$. Throughout, $f(\mathbf u,\mathbf x)$ is concave in $\mathbf u$ for every value of the decision variable $\mathbf x\in\mathbb R^k$.

The support function of a set $\mathcal U\subseteq\mathbb R^d$ is

$$\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u,\qquad\mathbf v\in\mathbb R^d .$$

The Value at Risk of the linear loss $\tilde{\mathbf u}^T\mathbf v$ at level $\epsilon$ is

$$\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\ \mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge 1-\epsilon\}.$$

A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P$ (property (P2) of the paper) if for every $k$, every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ for each $\mathbf x\in\mathbb R^k$, and every $\mathbf x^*\in\mathbb R^k$,

$$f(\mathbf u,\mathbf x^*)\le0\ \ \forall\mathbf u\in\mathcal U\quad\Longrightarrow\quad\mathbb P\big(f(\tilde{\mathbf u},\mathbf x^*)\le0\big)\ge1-\epsilon. \tag{2}$$

A function is bi-affine if it has the form $f(\mathbf u,\mathbf x)=\mathbf u^TF\mathbf x+\mathbf f_u^T\mathbf u+\mathbf f_x^T\mathbf x+f_0$.

In the data-driven setting, $\mathbb P^*$ is unknown and a sample $\mathcal S=(\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N)$ is drawn i.i.d. from it. The paper's schema fixes $0<\alpha<1$, takes the confidence region $\mathcal P(\mathcal S)$ of a hypothesis test at level $\alpha$, and builds a closed convex set $\mathcal U(\mathcal S)$ whose support function bounds $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)$ for every $\mathbb P\in\mathcal P(\mathcal S)$ and every $\mathbf v$.

Formalization targets

Goal: Theorem 1

(a) If $\mathcal U$ is nonempty, convex and compact and

$$\delta^*(\mathbf v\mid\mathcal U)\ge\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\qquad\forall\,\mathbf v\in\mathbb R^d,$$

then $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P$.

(b) If $\mathcal U$ is nonempty and $\delta^*(\mathbf v\mid\mathcal U)<\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)$ for some $\mathbf v$ at which $\delta^*(\mathbf v\mid\mathcal U)$ is finite, then some bi-affine $f$ violates (2).

Milestones toward the goal

The proof in the electronic companion (EC.1.1) is a short chain, and its steps are the milestones: the attainment property of VaR, $\mathbb P(\tilde{\mathbf u}^T\mathbf v>\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v))\le\epsilon$ (already proved on the platform); a strict separating hyperplane between $\mathcal U$ and the superlevel set $\{f(\cdot,\mathbf x^*)\ge t\}$; the bound $\mathbb P(f(\tilde{\mathbf u},\mathbf x^*)\ge t)\le\epsilon$ for $t>0$; its limit $\mathbb P(f(\tilde{\mathbf u},\mathbf x^*)>0)\le\epsilon$; and, for part (b), the witness $f(\mathbf u,x)=\mathbf v^T\mathbf u-x$ at $x^*=\delta^*(\mathbf v\mid\mathcal U)$.

Companions: Theorems 2 and 3

Theorem 2: with probability at least $1-\alpha$ over the sample, $\mathcal U(\mathcal S)$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$. Theorem 3: if the region does not depend on $\epsilon$, then with probability at least $1-\alpha$ the whole family $\{\mathcal U(\mathcal S,\epsilon):0<\epsilon<1\}$ implies the guarantee simultaneously (a), and every $\mathbf x$ satisfying the level-optimized constraints (9) satisfies the joint chance constraint

$$\mathbb P^*\Big(\max_{j=1,\dots,m}f_j(\tilde{\mathbf u},\mathbf x)\le0\Big)\ge1-\bar\epsilon \tag{7}$$

(b).

Significance

Theorem 1(a) is what certifies every uncertainty set in the paper: the $\chi^2$ and $G$ sets for discrete distributions, the Kolmogorov–Smirnov and forward–backward sets for independent marginals, the marginal-sample box and the moment sets. Each construction reduces to proving one inequality between a support function and a Value at Risk, which is a statement about a single linear functional, and Theorem 1(a) lifts it to every concave constraint at once. Part (b) shows the condition cannot be dropped even for bi-affine constraints. Theorems 2 and 3 separate the statistical input (coverage of a confidence region) from the convex-analytic input (the support-function bound), and Theorem 3(b) is what allows the levels $\epsilon_j$ of a system of constraints to be optimized after seeing the data.

The results are proved in the paper. None of them has a machine-checked proof; the only formalized ingredient is the attainment property of VaR, which is on the platform as a proved theorem. The formalization provides a checked bridge from support-function bounds to probabilistic guarantees that the other missions of this series (II–VI) use to state their own results in the criterion form $\mathrm{VaR}\le\delta^*$.

Difficulty

The informal argument is short; the difficulty is in the infinite-dimensional bookkeeping that the page leaves implicit. The superlevel set $\{f(\cdot,\mathbf x^*)\ge t\}$ need not be bounded, so the strict separation must use compactness of $\mathcal U$ alone. Closedness of this set and measurability of $\{f(\tilde{\mathbf u},\mathbf x^*)\le0\}$ depend on concave functions on $\mathbb R^d$ being continuous. The passage $t\downarrow0$ is continuity of a measure along an increasing union. The attainment of the infimum in the definition of VaR requires right-continuity of distribution functions. A naive attempt to separate $\mathcal U$ from the zero superlevel set $\{f\ge0\}$ directly fails, because the two sets may touch.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ; $\tilde{\mathbf u}$ is the identity map; $\mathbf v^T\mathbf u$ is the dot product u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$, and the support function is the published RobustMDP.Shared.supportFunction. Both are real-valued sInf/sSup, which return $0$ on empty or unbounded sets, so every statement assumes $0<\epsilon<1$, a probability measure, and an uncertainty set that is nonempty and compact (Theorem 1(a), Theorems 2–3) or nonempty with $\{\mathbf v^T\mathbf u:\mathbf u\in\mathcal U\}$ bounded above in the direction considered (Theorem 1(b)). In Theorem 1(b) and its witness this is the paper's own requirement that $\delta^*(\mathbf v\mid\mathcal U)$ be finite, which its strict inequality with a real VaR forces and its proof uses by treating $\delta^*(\mathbf v\mid\mathcal U)$ as a real number. Part (b) is printed with $\mathcal U^*$, a slip for $\mathcal U$; the proof's separation step prints both inequalities in the same direction, a slip corrected in the strict separation milestone.

Property (P2) quantifies over the dimension $k$ of the decision variable, every function concave in $\mathbf u$ for each $\mathbf x$, and every $\mathbf x^*$. Restricting it to affine $f$ or to $k=0$ would trivialize part (a) and falsify part (b), and is ruled out by the definition.

In Theorems 2 and 3 the sample is Fin N → (Fin d → ℝ) with the product law Measure.pi; the confidence region and the uncertainty set are arbitrary maps of the sample, and the coverage $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P(\mathcal S))\ge1-\alpha$ is a hypothesis, never the conclusion's event. Step 2 of the schema is stated with $g=\delta^*(\cdot\mid\mathcal U(\mathcal S))$ directly. The sets are assumed nonempty and compact (Step 3 says closed and convex; a finite support function that bounds VaR forces nonemptiness and boundedness). Theorem 3(b) reads the levels $\epsilon_j$ in $(0,1)$, where the family is defined. Probabilities of events in the sample space are outer measures, so no measurability hypotheses are needed.

A complete development needs strict separation of a compact convex set from a closed convex set (Mathlib's geometric_hahn_banach_compact_closed), continuity of concave functions on finite-dimensional spaces, and the attainment property of VaR. Contributions are welcome on all milestones; the separation and limit steps are reusable for any chance-constraint argument based on support functions.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Mathematical Programming 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441