Convex Optimization

Motivation

Gradient descent is a basic method for minimizing a differentiable function when evaluating its gradient is practical but solving the optimization problem directly is not. The rate at which its iterates approach an optimizer depends on the assumptions about the function. For a convex function with a Lipschitz gradient, the value error decreases at a sublinear rate. Adding strong convexity changes the behavior: the distance from the optimizer contracts at each step, giving an exponential bound on the value error. This section of Bubeck's monograph identifies a fixed step size that uses both the smoothness and curvature constants and gives the corresponding rate.

The result matters when a high-accuracy answer is needed. A sublinear bound makes each extra digit progressively more expensive; an exponential bound says that a fixed number of additional gradient evaluations reduces the error by a fixed factor. The theorem is a textbook result, already proved mathematically. This mission asks for its precise machine-checked statement and the source's supporting inequalities, rather than for a new optimization method.

Setting

Work in Euclidean space $\mathbb R^n$ with $n\ge1$, equipped with its usual inner product and norm. A differentiable function $f:\mathbb R^n\to\mathbb R$ has gradient $g(x)=\nabla f(x)$. It is $\beta$-smooth when its gradient is $\beta$-Lipschitz: $\|g(x)-g(y)\|\le\beta\|x-y\|$ for every $x,y$. It is $\alpha$-strongly convex when, for every $x,y$,

$$f(y)\ge f(x)+\langle g(x),y-x\rangle+\frac\alpha2\|y-x\|^2.$$

The first condition limits how rapidly the gradient changes. The second gives a quadratic lower bound on the function around any point. Here $\alpha>0$ and $\beta\ge0$. In positive dimension, the two conditions together entail $\beta\ge\alpha$, so the condition number $\kappa=\beta/\alpha$ is at least one. The case $\alpha=\beta$ remains part of the target.

A point $x^*$ is a global minimizer when $f(x^*)\le f(y)$ for every $y$. The book assumes such a point exists as a standing convention. A gradient descent run is a sequence $(x_t)_{t\ge1}$ satisfying $x_{t+1}=x_t-\eta g(x_t)$ at each positive index. Its first iterate $x_1$ is arbitrary. The step size in this mission is fixed at $\eta=2/(\alpha+\beta)$, rather than chosen by line search or adapted along the run.

Formalization targets

The central target is Theorem 3.12 of Bubeck, p. 279. For every integer $t\ge0$, the gradient descent run satisfies

$$f(x_{t+1})-f(x^*)\le \frac\beta2\exp\!\left(-\frac{4t}{\kappa+1}\right)\|x_1-x^*\|^2.$$

At $t=0$ this is a smoothness bound on the initial value gap. For subsequent iterations it gives a linear convergence rate with the explicit exponential factor stated in the book. No initial-radius bound or bounded domain is imposed: the actual squared distance $\|x_1-x^*\|^2$ appears in the conclusion.

The milestones trace the mathematical claims stated in the source. Equation (3.6) is the co-coercivity inequality for gradients of convex smooth functions. The proof of Lemma 3.11 introduces $\phi(z)=f(z)-(\alpha/2)\|z\|^2$, and identifies it as convex and $(\beta-\alpha)$-smooth. Lemma 3.11 combines curvature and smoothness into a sharper inequality for two gradients. The proof of Theorem 3.12 then gives a value-gap bound, a one-step distance contraction, and its iterated exponential form. These statements are separately useful: the co-coercivity and contraction bounds can be reused in analyses of related first-order methods.

Significance

The theorem states a complete guarantee for the algorithm: an explicit rule, the hypotheses on the objective, and a bound valid for every iteration count. It makes the role of $\kappa$ visible. When $\kappa$ is close to one, the contraction is strong; when the smoothness constant is much larger than the curvature constant, more iterations are needed for the same error reduction. The stated dependence supports comparisons with projected and accelerated gradient methods elsewhere in the same monograph.

Formalizing the result requires a common interface for actual gradients, smoothness, strong convexity, and algorithm runs. The strong-convexity predicate is an existing published definition, while the local smoothness and run definitions use Bubeck's conventions. Once these interfaces and the inequalities are proved, later missions can use the resulting declarations to compare rates without translating between informal meanings of “smooth” or changing the iterate index. The source provides a mathematical proof; these draft Lean theorems carry sorry and do not yet constitute machine-checked proofs.

Difficulty

The main issue is getting the sharp contraction factor from two assumptions that control different parts of the gradient step. A direct Lipschitz estimate on the update map does not by itself express the mixed inner-product term with the constants needed for the stated factor. Lemma 3.11 is the source's precise bridge between the gradient difference, the point displacement, and their inner product. The case $\alpha=\beta$ also needs to remain valid: a proof route that divides by $\beta-\alpha$ cannot cover that boundary by the same calculation.

The last display in the proof of Theorem 3.12 joins a one-step inequality involving $x_t$ to an exponential inequality involving $x_1$. The latter is the cumulative statement after $t$ steps. Keeping these as separate milestones makes each quantified claim explicit while preserving the theorem's bound.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with $n>0$. The gradient is an explicit map $g$ required to be the actual gradient of $f$ at every point. Smoothness is the gradient Lipschitz condition, not a quadratic upper bound used as a definition. Strong convexity uses the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn predicate on the whole space; its formula is the book's (3.13). Iterates are indexed from one, and index zero imposes no condition. The norm, inner product, constants, and real exponential follow the printed formulas.

The added explicit conditions are $n>0$, $\alpha>0$, and $\beta>0$ where Equation (3.6) divides by $\beta$. Positive dimension excludes a degenerate space where curvature imposes no restriction on smoothness. The positivity of $\alpha$ makes $\kappa$ meaningful; the source treats it as a positive strong-convexity parameter. The minimizer hypothesis is the book's standing convention. There is no assumption that $g(x^*)=0$: that property follows from global minimality and differentiability. A gradient map unrelated to $f$ would trivialize the model, so the smoothness definition includes the gradient identity.

The local development needs Euclidean inner-product identities, convexity, differentiability, Lipschitz gradient bounds, and real exponential estimates. The auxiliary function and the two co-coercivity inequalities are reusable outside this chapter. Contributions should prove the exact milestone statements and the final theorem, including $t=0$ and $\alpha=\beta$, without weakening constants or substituting another gradient descent step.

Selected references

• Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2; DOI:10.1561/2200000050.

Motivation

Gradient descent goes back to Cauchy (1847). It is the simplest method for minimizing a differentiable function, and most of the first-order methods in large-scale optimization and machine learning are variants of it. Its appeal in high dimension is that its oracle complexity, the number of gradient evaluations needed to reach a given accuracy, can be bounded independently of the dimension. For a merely Lipschitz convex function the projected subgradient method needs on the order of $1/\varepsilon^2$ steps to reach accuracy $\varepsilon$ (Theorem 3.2 of the book). Under a smoothness assumption gradient descent does much better, because the gradients shrink near the optimum and the steps adapt automatically.

This mission formalizes the basic result of that kind: Theorem 3.3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). It states that gradient descent with step size $1/\beta$ on a convex $\beta$-smooth function on $\mathbb R^n$ has optimality gap $O(1/t)$ after $t$ steps. The result and its proof are standard; versions appear in Nesterov's Introductory Lectures on Convex Optimization (2004, §2.1.5). It is the fourth mission in a series that formalizes the capstone results of Bubeck's monograph.

Setting

Write $\mathbb R^n$ for Euclidean space with inner product $x^\top y$ and norm $\|\cdot\|$. Let $f:\mathbb R^n\to\mathbb R$ be differentiable with gradient $\nabla f$.

• $f$ is convex if $f((1-\lambda)x+\lambda y)\le(1-\lambda)f(x)+\lambda f(y)$ for all $x,y$ and $\lambda\in[0,1]$.
• For $\beta\ge0$, $f$ is $\beta$-smooth if its gradient is $\beta$-Lipschitz:

$$\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad\text{for all }x,y\in\mathbb R^n.$$

• A minimizer is a point $x^*$ with $f(x^*)\le f(y)$ for every $y$. Throughout the book a minimizer is assumed to exist.
• Gradient descent with step size $\eta>0$, started at $x_1\in\mathbb R^n$, is the sequence

$$x_{t+1}=x_t-\eta\nabla f(x_t),\qquad t\ge1. \tag{3.1}$$

The optimality gaps are $\delta_s=f(x_s)-f(x^*)\ge0$.

Formalization targets

Goal: Theorem 3.3 (p. 267)

If $f$ is convex and $\beta$-smooth with $\beta>0$, $x^*$ is a minimizer, and $(x_t)$ is gradient descent with $\eta=1/\beta$, then for every $t\ge2$

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

Milestones

These are the statements the book's proof uses, in the book's order:

1. Lemma 3.4 (p. 267). For any $\beta$-smooth $f$, with no convexity: $|f(x)-f(y)-\nabla f(y)^\top(x-y)|\le\frac\beta2\|x-y\|^2$.
2. (3.4) (p. 267). For convex $\beta$-smooth $f$: $0\le f(x)-f(y)-\nabla f(y)^\top(x-y)\le\frac\beta2\|x-y\|^2$.
3. (3.5) (p. 267). For convex $f$, one step of length $1/\beta$ decreases $f$ by at least $\frac1{2\beta}\|\nabla f(x)\|^2$.
4. Lemma 3.5 (p. 268). If (3.4) holds, then $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac1{2\beta}\|\nabla f(x)-\nabla f(y)\|^2$.
5. (3.6) (p. 269). Co-coercivity: $(\nabla f(x)-\nabla f(y))^\top(x-y)\ge\frac1\beta\|\nabla f(x)-\nabla f(y)\|^2$.
6. Distances decrease (proof of Theorem 3.3, p. 269). $\|x_{s+1}-x^*\|\le\|x_s-x^*\|$ for every $s\ge1$.
7. The recursion (p. 268). $\delta_{s+1}\le\delta_s-\frac{1}{2\beta\|x_1-x^*\|^2}\delta_s^2$.
8. From the recursion to the rate (p. 269). For $\omega>0$ and non-negative reals, $\omega\delta_s^2+\delta_{s+1}\le\delta_s$ for all $s\ge 1$ implies $1/\delta_t\ge\omega(t-1)$.

Stronger companion: footnote 4 (p. 269)

Under the same hypotheses, $f(x_t)-f(x^*)\le 2\beta\|x_1-x^*\|^2/(t+3)$ for every $t\ge1$.

Significance

Theorem 3.3 is the reference rate for first-order methods on smooth convex problems. Several later results in the book are measured against it. Nesterov's accelerated gradient descent (§3.7) improves $1/t$ to $1/t^2$, the lower bounds of §3.5 show that $1/t^2$ cannot be beaten by any black-box first-order method, and adding strong convexity (§3.4) upgrades $1/t$ to a linear rate. Its ingredients are reused throughout the book and the optimization literature: the descent lemma (Lemma 3.4), the one-step improvement (3.5) and co-coercivity (3.6). Co-coercivity is the finite-dimensional case of the Baillon–Haddad theorem.

The result is classical and fully proved on paper. To our knowledge Mathlib does not contain this rate for gradient descent on convex smooth functions, and no published Prove2Me theorem states it. The mission provides it, together with Lemma 3.4 and co-coercivity as reusable statements on EuclideanSpace ℝ (Fin n). These are the facts that later missions of the series on projected gradient descent, strong convexity and acceleration need. Formalizing the improved constant of footnote 4 is a welcome addition.

Difficulty

Two steps are not routine. The first is Lemma 3.4, where the book integrates the gradient along a segment. In Lean this needs a mean-value or fundamental-theorem-of-calculus argument for a function on a Euclidean space, together with a Cauchy–Schwarz estimate, and Mathlib's HasGradientAt interface has to be connected to one-variable derivatives along lines.

The second is the monotonicity of $\|x_s-x^*\|$. The natural first attempt is to telescope the one-step improvement (3.5) together with the convexity bound $\delta_s\le\|x_s-x^*\|\|\nabla f(x_s)\|$. That gives a recursion involving $\|x_s-x^*\|$, which is not controlled by $\|x_1-x^*\|$ without further work. Making the recursion uniform requires co-coercivity (3.6), which comes from Lemma 3.5. That lemma's hypothesis is the two-sided inequality (3.4), not smoothness directly. The final numerical step divides by the gaps $\delta_s$, so zero gaps need separate handling.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), and $x^\top y$ is ⟪x, y⟫_ℝ.
• The gradient is an explicit map $g:\mathbb R^n\to\mathbb R^n$ with the hypothesis ∀ x, HasGradientAt f (g x) x.
• $\beta$-smoothness (IsBetaSmooth f g β) is the book's definition: $\beta\ge0$, the gradient-existence hypothesis, and the Lipschitz bound $\|g(x)-g(y)\|\le\beta\|x-y\|$. The book's "continuously differentiable" follows from it.
• Convexity is Mathlib's ConvexOn ℝ Set.univ f. A minimizer is a point xstar with ∀ y, f xstar ≤ f y; its existence is the book's standing assumption, and $\nabla f(x^*)=0$ is derived, not assumed.
• A gradient-descent run (IsGDRun g η x) is a sequence x : ℕ → ℝⁿ with $\eta>0$ and $x_{t+1}=x_t-\eta g(x_t)$ for every $t\ge1$. The book's $x_1$ is x 1, and index $0$ is unused. Every theorem quantifies over all runs with $\eta=1/\beta$.

Disclosed side conditions:

• $\beta>0$ wherever the page divides by $\beta$. Convexity is retained for (3.5), as in its source context.
• $t\ge2$ in the goal, where the page's bound has denominator $t-1$.
• Statements in which the page divides by $\delta_s$ or by $\|x_1-x^*\|^2$ are multiplied through, so that they stay true and meaningful when those quantities vanish.

A trivializing formalization is ruled out. Smoothness is the Lipschitz condition on the gradient, so Lemma 3.4 and (3.4) are not restatements of the definition, as they would be if the quadratic upper bound (3.4) were taken as the definition of smoothness. The run predicate also fixes the step size $1/\beta$.

A complete development needs:

• the segment integral or mean-value estimate for HasGradientAt functions;
• first-order characterizations of convexity for differentiable functions;
• elementary inner-product algebra.

Lemma 3.4, Lemma 3.5 and (3.6) are reusable well beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–357, 2015. arXiv:1405.4980v2; §3.2, pp. 266–269.
• A. Cauchy, Méthode générale pour la résolution des systèmes d'équations simultanées, C. R. Acad. Sci. Paris 25:536–538, 1847.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9
• J.-B. Baillon and G. Haddad, Quelques propriétés des opérateurs angle-bornés et n-cycliquement monotones, Israel J. Math. 26:137–150, 1977. doi:10.1007/BF03007664

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

A robust linear constraint $a'x \ge b$ for all $a \in \mathcal U$ protects a decision $x$ against every realization of the data $a$ in an uncertainty set $\mathcal U$. Robust optimization took this form in the work of Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Oper. Res. Lett. 1999), where $\mathcal U$ is chosen by the modeller. Bertsimas and Brown (Oper. Res. 2009) tie the choice of $\mathcal U$ to the decision maker's attitude towards risk: on a finite sample $\mathcal A = \{a_1,\dots,a_N\}$, a coherent risk measure constraint $\mu(\tilde a'x - b) \le 0$ is equivalent to a robust constraint over a convex set built from $\mathcal A$, and for the distortion risk measures (the law-invariant, comonotone coherent measures, which include CVaR) that set is a polytope of a special kind, a permutohull.

An uncertainty set in practice is often an arbitrary polyhedron, given by the modeller or by previous analysis. Section 4.5 of the paper asks which distortion risk measure best approximates such a polyhedron from inside: the largest permutohull of a given shape contained in it. A positive answer quantifies how conservative a given polyhedral uncertainty set is relative to a distortion risk measure, and gives the risk measure that is closest to it. This mission is the third of a series of three on the paper; the first establishes the permutohull representation of distortion risk constraints, the second the generators of the centrally symmetric distortion measures.

Setting

Fix $N \ge 1$ and data $a_1,\dots,a_N \in \mathbb R^n$, the columns of a matrix $A$. Let $e_N \in \mathbb R^N$ have $1/N$ at each entry, so the sample mean is $\hat a = Ae_N$.

• The restricted simplex $\hat\Delta^N$ is the set of probability vectors $q \in \mathbb R^N$ with $q_1 \ge \dots \ge q_N$. Under the uniform probability on $N$ points, the distortion risk measures are exactly the maps $\mu_q(X) = -\sum_i q_i x_{(i)}$, $q \in \hat\Delta^N$, with $x_{(1)} \le \dots \le x_{(N)}$ the ordered values of $X$ (Theorem 4.2 of the paper).
• For $q \in \mathbb R^N$, the $q$-permutohull is $\Pi_q(\mathcal A) = \operatorname{conv}\{\sum_i q_{\sigma(i)} a_i : \sigma \in S_N\}$. The robust constraint over $\Pi_q(\mathcal A)$ is the risk constraint for $\mu_q$.
• The symmetric restricted simplex $\hat\Delta^N_{\mathrm{sym}}$ is the set of $q \in \hat\Delta^N$ with $q = 2e_N - q_\sigma$ for some permutation $\sigma$, where $(q_\sigma)_i = q_{\sigma(i)}$. For these $q$ the permutohull is centrally symmetric about $\hat a$.
• With $\tilde\pi_q(\mathcal A) = \Pi_q(\mathcal A) - \hat a$, the Minkowski functional

$$\|w\|_{q,\mathcal A} = \inf\{\alpha > 0 : w/\alpha \in \tilde\pi_q(\mathcal A)\}$$

measures $w = a - \hat a$ against the shifted permutohull (12).

• The polyhedron is $\mathcal U = \{a \in \mathbb R^n : u_k'a \ge v_k,\ k = 1,\dots,m\}$ (14), with $\hat a \in \mathcal U$.

The family of candidate inner approximations is obtained by mixing a fixed $\hat q \in \hat\Delta^N_{\mathrm{sym}}$ with the uniform generator: $q = \lambda\hat q + (1-\lambda)e_N$, $\lambda \in \mathbb R$.

Formalization targets

Goal: Theorem 4.5

Let $\lambda^*$ be the optimal value of the linear program

$$\max\ \lambda\quad\text{s.t.}\quad q = \lambda\hat q + (1-\lambda)e/N,\quad e'(s_k + t_k) \ge v_k\ \forall k,\quad s_{k,i} + t_{k,j} \le (u_k'a_j)\,q_i\ \forall i,j,k, \tag{15}$$

in $s_k, t_k, q \in \mathbb R^N$ and $\lambda \in \mathbb R$, and $q^* = \lambda^*\hat q + (1-\lambda^*)e_N$. Then

$$\Pi_{q^*}(\mathcal A) \subseteq \mathcal U,\qquad \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \mathcal U \implies \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \Pi_{q^*}(\mathcal A),$$

and, when $\hat q \ne e_N$, $q^* \in \hat\Delta^N$ if and only if

$$\lambda^* \le \frac{1}{1 - N\hat q_{\min}}. \tag{16}$$

Milestones

1. Proposition 4.2: for $q \in \hat\Delta^N_{\mathrm{sym}}$ with $\Pi_q(\mathcal A)$ of nonempty interior, $\|\cdot\|_{q,\mathcal A}$ is a norm.
2. Scaling (proof of Lemma 4.2): $\Pi_{\lambda q + (1-\lambda)e_N}(\mathcal A) = \hat a + \lambda\,\tilde\pi_q(\mathcal A)$ for every $q \in \mathbb R^N$, $\lambda \in \mathbb R$.
3. Lemma 4.2: $\|a - \hat a\|_{\lambda q + (1-\lambda)e_N,\mathcal A} = \frac{1}{|\lambda|}\|a - \hat a\|_{q,\mathcal A}$ for $q \in \hat\Delta^N_{\mathrm{sym}}$, $\lambda \ne 0$.
4. Containment as linear constraints (proof of Theorem 4.5): $\Pi_q(\mathcal A) \subseteq \mathcal U$ iff vectors $s_k, t_k$ satisfying the constraints of (15) exist, for every $q \in \mathbb R^N$.
5. Nonnegativity (proof of Theorem 4.5): for $\lambda \ge 0$ and $N\hat q_{\min} < 1$, $\lambda\hat q + (1-\lambda)e_N \in \hat\Delta^N$ iff $\lambda \le 1/(1 - N\hat q_{\min})$.

Significance

The theorem reduces a geometric question — the largest member of a one-parameter family of centrally symmetric polytopes, each with $N!$ potential vertices, that fits inside an arbitrary polyhedron — to a linear program with $O(mN)$ variables and $O(mN^2)$ constraints. Its solution identifies a distortion risk measure $\mu = \lambda^*\mu_{\hat q} + (1-\lambda^*)\mathbb E[-X]$, which the paper reads as a mean–deviation measure in the style of a Sharpe ratio, and the bound (16) decides whether the optimal set is itself a distortion set or must be shrunk further.

The results are proved in the paper, with short proofs that pass over several points: the scaling identity is asserted, the duality step leaves the assignment-problem structure implicit, and the norm claim requires a nondegeneracy condition that the page does not state. No machine-checked proof of any of them is known. A formalization fixes the exact hypotheses (nonempty interior for the norm, $\lambda \ne 0$ in (13), $\hat q \ne e_N$ in (16)), and the containment equivalence for arbitrary real weight vectors $q$ is a reusable fact about permutohulls and assignment duality.

Difficulty

The goal combines three ingredients of different nature. The containment equivalence needs that minimizing a linear function over the permutohull is a linear program over the Birkhoff polytope of doubly stochastic matrices, followed by linear programming duality for that program; neither the Birkhoff–von Neumann theorem nor assignment duality is a one-line consequence of what is in Mathlib. The scaling identity is a statement about convex hulls under an affine map and holds for all real $\lambda$, including the reflected case $\lambda < 0$; the maximality claim then needs the central symmetry of $\Pi_{\hat q}(\mathcal A)$ about $\hat a$, which is a property of $\hat\Delta^N_{\mathrm{sym}}$ (Proposition 4.1 of the paper) and not of a general $q$. The tempting shortcut — comparing gauges directly — fails at $\lambda = 0$, where the permutohull is the single point $\hat a$ and the gauge is degenerate.

Formalization scope

Vectors in $\mathbb R^N$ and $\mathbb R^n$ are Fin N → ℝ and Fin n → ℝ, with $0$-based indices; $a_i$ is a i, $u_k'a$ is a dot product. $\hat\Delta^N$ uses Mathlib's stdSimplex and Antitone. The permutohull is convexHull of the range over Equiv.Perm (Fin N), defined for every real $q$ because (15) evaluates it at mixtures with possibly negative entries. The Minkowski functional is Mathlib's gauge, which takes the value $0$ (not $+\infty$) on points no positive multiple of the set reaches; this is why Proposition 4.2 assumes $\Pi_q(\mathcal A)$ has nonempty interior and why the goal states "largest" as set containment. $\hat q_{\min}$ is $\min_i \hat q_i$. The optimal value $\lambda^*$ is a hypothesis (it is the greatest element of the feasible set of (15)), not a supremum defined by sSup.

Standing assumptions and disclosed additions: $N \ge 1$; the polyhedron (14) is not assumed bounded (a generalization); in (13) the right-hand norm is that of $q$, not $\tilde q$ as printed, and $\lambda \ne 0$; in (16), $N\hat q_{\min} < 1$; "corresponds to a distortion risk measure" is read, as the proof reads it, as $q^* \in \hat\Delta^N$. A formalization that assumes $\Pi_{q^*}(\mathcal A) \subseteq \mathcal U$ or the maximality of $\lambda^*$ trivializes the theorem: both are conclusions, and the linear program enters only through its constraints and its optimal value.

A complete development needs: convex hulls under affine maps; the Birkhoff–von Neumann theorem (doubly stochastic matrices are convex combinations of permutation matrices); duality for the assignment linear program; gauge calculus for centrally symmetric convex bodies. The containment equivalence and the scaling identity are reusable beyond this mission. Proofs of any milestone, and of the Birkhoff and assignment-duality infrastructure, are welcome.

Selected references

• D. Bertsimas and D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
• A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal and A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

Motivation

The data of a linear program are often not known exactly: they are measured or estimated, or they are forecasts. The robust counterpart approach, going back to Soyster (1973), asks for a solution that is feasible for every data matrix in a prescribed uncertainty set and is best among such solutions. Ben-Tal and Nemirovski's 1999 paper [1] showed that the method stays computationally tractable for a broad class of uncertainty sets, the ellipsoidal uncertainties: the robust counterpart of an uncertain LP is then a conic quadratic program (CQP), solvable by interior point methods at roughly the cost of an LP of similar size. This result is the basis of robust linear optimization as it is used today [2], [3]. It is also the reason ellipsoidal sets are the default choice in robust portfolio selection (§4 of the paper) and in many later robust models.

Timeline. Soyster (1973) treated column-wise box uncertainty, for which the counterpart is again an LP [4]. Ben-Tal and Nemirovski (1998) developed the general theory of robust convex optimization [5]. The present paper (1999) proved the ellipsoidal-to-CQP reduction for LPs (Theorem 3.1). Its proof relies on the conic duality theory of Nesterov and Nemirovski (1994) [6].

Setting

An uncertain linear program in the homogeneous form (6) is

$$\min\{c^Tx \mid Ax \ge 0,\ f^Tx = 1\},$$

where $c, f \in \mathbb R^n$ are fixed and the matrix $A \in \mathbb R^{m\times n}$ lies in an uncertainty set $\mathcal U$. A point $x$ is robust feasible if $f^Tx = 1$ and $Ax \ge 0$ for every $A \in \mathcal U$. The robust counterpart $(P_{\mathcal U})$ minimizes $c^Tx$ over the robust feasible set

$$G_{\mathcal U} = \{x \mid Ax \ge 0\ \forall A \in \mathcal U,\ f^Tx = 1\}.$$

An ellipsoid in $\mathbb R^{m\times n}$ (display (14)) is a set

$$U(\Pi, Q) = \{\Pi(u) \mid \|Qu\| \le 1\},$$

where $\Pi(u) = P^0 + \sum_{j=1}^L u_jP^j$ is affine in $u \in \mathbb R^L$, $Q$ is an $M\times L$ matrix, and $\|\cdot\|$ is the Euclidean norm. A singular $Q$ gives an ellipsoidal cylinder, which may be unbounded. An ellipsoidal uncertainty is a set

$$\mathcal U = \bigcap_{\ell=0}^k U(\Pi_\ell, Q_\ell)$$

(condition A) that is bounded (condition B) and contains a matrix $A$ with $A = \Pi_\ell(u^\ell)$ and $\|Q_\ell u^\ell\| < 1$ for every $\ell$ (condition C, a Slater condition).

Formalization targets

Goal: Theorem 3.1

For every $x \in \mathbb R^n$,

$$x \in G_{\mathcal U} \iff f^Tx = 1 \ \text{ and }\ \forall i \le m\ \ \exists\, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)} :\ (x, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)}) \text{ satisfies } (\mathcal C_i).$$

Here $(\mathcal C_i)$ is an explicit system: linear equations and one linear inequality in $(x, \lambda, \mu, \nu)$, together with the second-order cone constraints $\|\mu^{(i)}_\ell\| \le \nu^{(i)}_\ell$. Its coefficients are the matrices $P^j_\ell$ and $Q_\ell$. The robust feasible set is therefore the projection of the feasible set of the conic quadratic program (CQP), which minimizes $c^Tx$ subject to $(\mathcal C_1), \dots, (\mathcal C_m)$ and $f^Tx = 1$.

Milestones, in the order of the Appendix's proof

1. $\mathcal U$ equals the image of the feasible set of the problem $(P_i[x])$ under $u \mapsto \Pi_0(u^0)$ (p. 15).
2. Claim (I): with $f^Tx = 1$, $x$ is robust feasible iff every $(P_i[x])$ has nonnegative optimal value (p. 15).
3. Claim (II): conic quadratic duality. A strictly feasible primal that is bounded below has a solvable dual with equal optimal value (p. 15).
4. Conditions B and C make every $(P_i[x])$ strictly feasible and bounded below (p. 16).

Companion results

The CQP forms (16) and (17) of the simplest cases (a single ellipsoid; constraint-wise ellipsoids), Remark 3.1 (bounded polytopes are ellipsoidal uncertainties), and the robust portfolio counterpart (22).

Significance

The result. Theorem 3.1 turns a semi-infinite constraint system (one constraint for every $A \in \mathcal U$) into finitely many conic quadratic constraints whose size is polynomial in the data. Robust LPs with ellipsoidal uncertainty, which by Remark 3.1 include polytopic uncertainty, can therefore be solved by standard conic solvers. Later robust optimization results, such as budgeted uncertainty, affinely adjustable policies and distributionally robust LPs, refine this pattern.

Formalizing it. The theorem is classical and its proof is complete, but no machine-checked proof exists. A formal proof needs a conic quadratic strong duality theorem with dual attainment (claim (II)), which Mathlib does not have in this form. That duality theorem can be reused well beyond this mission. The companion results (16), (17) and (22) are self-contained computations of a minimum of a linear function over a Euclidean ball.

Difficulty

The "if" direction is weak duality: a solution of $(\mathcal C_i)$ certifies that the $i$-th constraint holds for all of $\mathcal U$. The content is the "only if" direction. It requires dual attainment, not merely equality of optimal values, because a solution of $(\mathcal C_i)$ must exist. Dual attainment fails without a constraint qualification. Condition C must hold strictly for every ellipsoid, including $\ell = 0$, and the ellipsoids may be cylinders, so the variables $u^\ell$ can range over unbounded sets even though $\mathcal U$ is bounded. Projecting the problem onto a single parameter space is not available in general, because the maps $\Pi_\ell$ need not be injective.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The indices $\ell = 0, \dots, k$ are Fin (k + 1), and the $k$ equality multipliers $\lambda_\ell$, $\ell \ge 1$, are indexed by Fin k. Every norm is Euclidean, written out as euclidNorm v = √(∑ v_j²), because Mathlib's norm on Fin M → ℝ is the sup norm, under which ellipsoids would become boxes. Condition B is a uniform bound on all matrix entries, and condition C is required for every $\ell = 0, \dots, k$. The page's words say "$\ell = 1, \dots, k$", but its display and the proof use every $\ell$. Injectivity of $\Pi_\ell$ is not assumed, and neither is §2.1's standing assumption that $\mathcal U$ is convex and closed. An ellipsoidal uncertainty is convex automatically, and closedness is not used, so both omissions generalize the statement. Three printed slips are corrected and disclosed: the sum in the equality constraint of (CQP$_d$) runs over $\ell = 0, \dots, k$; $(\mathcal C_i)$ has $\varphi^{(i)}[x]$ where the page prints $f^{(i)}[x]$; and Remark 3.1 has the factor $2/(r_i - s_i)$ where the page prints $(r_i - s_i)/2$.

The goal is not the contentless statement "some conic quadratic program has $G_{\mathcal U}$ as a projection", which holds for every closed convex set. It names the system $(\mathcal C_i)$ built from the data $P^j_\ell$, $Q_\ell$. The goal also does not mention optimal values, (CQP$_p$) or strict feasibility; those are milestones.

Contributions are welcome on the conic duality theorem (II) as a standalone result, on the finite-dimensional facts that minimize a linear function over a Euclidean ball (used in (16), (17) and (22)), and on the goal itself.

Selected references

1. A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
2. A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
3. D. Bertsimas, D. B. Brown, C. Caramanis, Theory and applications of robust optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510
4. A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
5. A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
6. Yu. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

A linear decision made with uncertain coefficients can be protected by requiring the constraint to hold for every coefficient vector in an uncertainty set. Choosing that set determines how conservative the decision is. Bertsimas and Brown connect this choice to a risk measure: a functional that assigns a cost to the random reward left by a decision. Their construction turns certain risk constraints into robust linear constraints over a convex hull of weighted samples. This mission isolates the structural question asked in §4.4 of their paper: which such risk measures always produce uncertainty sets that are centrally symmetric about the sample mean? The answer matters because this symmetric family is the class used in the paper's subsequent approximation of general polyhedral uncertainty sets. Bertsimas and Brown (2009), §§4.3–4.5.

Setting

There are $N\ge1$ observations, indexed by $i=1,\ldots,N$, with equal reference probabilities. A probability weight vector $q=(q_1,\ldots,q_N)$ has nonnegative entries summing to one. The restricted simplex $\widehat\Delta^N$ contains those vectors whose entries are nonincreasing: $q_1\ge\cdots\ge q_N$. For a reward vector $X=(x_1,\ldots,x_N)$, write $x_{(1)}\le\cdots\le x_{(N)}$ for its increasing order statistics. The associated distortion risk measure is $\mu_q(X)=-\sum_iq_i x_{(i)}$. A larger reward therefore reduces risk. Under the uniform distribution, the paper's Theorem 4.2 identifies these functionals, for $q\in\widehat\Delta^N$, with its distortion risk measures. Bertsimas and Brown (2009), Theorem 4.2.

Take arbitrary sample vectors $a_1,\ldots,a_N\in\mathbb R^n$. For a permutation $\sigma$ of their indices, form the weighted vector $\sum_iq_{\sigma(i)}a_i$. The $q$-permutohull $\Pi_q(\mathcal A)$ is the convex hull of all these vectors. Its center of interest is the sample mean $\widehat a=N^{-1}\sum_i a_i$. A set $P$ is centrally symmetric through $x_0\in P$ when $x_0+x\in P$ implies $x_0-x\in P$ for every $x$. The quantifier “for any data” ranges over every dimension $n$ and every choice of $N$ sample vectors. It is stronger than symmetry for one selected data set. Bertsimas and Brown (2009), Definitions 4.7–4.8.

Formalization targets

The first target is Proposition 4.1's characterization of weights giving universal symmetry. If $e_N$ is the vector with every entry $1/N$, then

$$\bigl[\Pi_q(\mathcal A)\text{ is centrally symmetric through }\widehat a \text{ for every }n,\mathcal A\bigr] \quad\Longleftrightarrow\quad \exists\sigma\in S_N:\ q=2e_N-q_\sigma.$$

This condition defines the symmetric restricted simplex $\widehat\Delta^N_{\mathrm{sym}}$ inside $\widehat\Delta^N$. Bertsimas and Brown (2009), Proposition 4.1 and Definition 4.9.

The main target is Theorem 4.4. Put $\widehat N=\lfloor N/2\rfloor+1$. For $1\le j\le\widehat N$, define a generator $\bar q^{\,j}$ by

$$\bar q_i^{\,j}= \begin{cases} 2/N,&i<j,\\ 1/N,&j\le i\le N-j+1,\\ 0,&\text{otherwise}. \end{cases}$$

A functional represented by a $q\in\widehat\Delta^N$ whose permutohull is symmetric for every data set is exactly a convex mixture of the $\widehat N$ generator functionals:

$$\mu(X)=\sum_{j=1}^{\widehat N}\lambda_j\mu_{\bar q^{\,j}}(X), \qquad \lambda_j\ge0,\qquad\sum_{j=1}^{\widehat N}\lambda_j=1.$$

The milestones also state the two set inclusions behind the equality of $\widehat\Delta^N_{\mathrm{sym}}$ with the convex hull of these generators, including the coordinate reversal identity. Bertsimas and Brown (2009), Theorem 4.4 and its proof.

Significance

The result gives a finite list of risk functionals from which every member of the universally symmetric distortion subclass can be formed. The number of generators is $\lfloor N/2\rfloor+1$, rather than an unspecified family. It also connects a geometric property of a robust uncertainty set to a checkable condition on its weights. The paper uses this symmetric subclass to formulate the inner approximation problem in §4.5, where a symmetric permutohull is fitted inside another polytope. Bertsimas and Brown (2009), §§4.4–4.5.

The mathematical result is proved in the 2009 paper. This formalization task is to obtain Lean proofs of the classification and its source-stated intermediate claims. The definition layer is a reusable interface for finite distortion risk measures, permutohulls, and symmetry under coordinate permutations. Formal proofs here would provide a checked foundation for later robust optimization statements using the same finite sample model. The proposed goal and milestones are open Lean statements; compiling them verifies their syntax and types, not their proofs.

Difficulty

Symmetry of one pictured polygon does not determine its weight vector. The hypothesis demands symmetry for every possible collection of sample vectors, so the converse in Proposition 4.1 must recover a relation among weights from a universal geometric property. Another difficulty is that the explicit generators change shape at the midpoint, and the odd and even cases have different middle ranges. The paper writes the calculation for odd $N$ and says the even case is analogous; the theorem itself makes no parity restriction. A proof therefore has to cover the even boundary, including the generator whose $1/N$ band is empty. Bertsimas and Brown (2009), Proposition 4.1 and proof of Theorem 4.4.

Formalization scope

The Lean sample space is Fin N, with $N>0$. Its indices start at zero; the prose and source formulas above start at one. The source's $\widehat N$ is N / 2 + 1 in natural numbers. Probability vectors use Mathlib's standard simplex together with antitone coordinate order. Permutohulls use convexHull of the finite permutation family, and order statistics use Tuple.sort. The reference distribution is uniform, as in the paper's Assumption 4.1. Real vector spaces of dimension zero are allowed because the claim quantifies over every dimension; the nonempty sample condition excludes division by zero.

The goal takes an arbitrary functional $\mu$ and requires an actual representation $\mu=\mu_q$ by a restricted-simplex weight. This is the paper's Theorem 4.2 parametrization of distortion risk measures, stated directly because that theorem is being drafted in a separate mission of the same series. Universal symmetry is derived from the data quantifier; it is not assumed as a condition on $q$. The generator mixture is likewise the conclusion, with its coefficients nonnegative and summing to one. Central symmetry includes membership of the center in the set.

Useful contributions include proofs of the source's permutation characterization, validity and symmetry of generator mixtures, and their converse spanning property. The definitions of finite probability weights and weighted permutation hulls can support further finite sample robust optimization results. The paper's inconsistent accent on the generator risk measure in Theorem 4.4 is read as the functional of the displayed generator vector; its intermediate sum on p. 1492 does not alter the stated normalized mixture.

Selected references

• Dimitris Bertsimas and David B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6), 1483–1495, 2009. DOI: 10.1287/opre.1080.0646.

Motivation

Many large convex programs have far more constraints than can be handled at once, but each constraint on its own is simple: a single linear equation or inequality. Row-action methods exploit this by touching one constraint per iteration. L. M. Bregman's 1967 paper (DOI 10.1016/0041-5553(67)90040-7) introduced the general framework behind most of them. A strictly convex function $f$ induces the "distance" $D(x,y)=f(x)-f(y)-(g(y),x-y)$, now called the Bregman distance, and the method moves from point to point by $D$-projections onto one constraint at a time. For $f(x)=\|x\|^2/2$ this reduces to Hildreth's method for quadratic programming; for entropy-type $f$ it gives the balancing (matrix scaling) methods used for transportation and traffic problems. The later literature on Bregman projections, mirror descent and entropic regularisation starts from this paper.

This mission formalizes the last main result of the paper, Theorem 4 (p. 212), which treats linear inequality constraints. Here a plain projection cycle does not minimize $f$. Bregman's fix carries a vector of nonnegative multipliers $u^n$ along with the primal point $x^n$ and lets each step either move towards a violated constraint or relax a multiplier. The result is a primal–dual method.

Timeline. Hildreth (1957) gave the quadratic case. Bregman (1967) proved the general theorem stated here. Censor and Lent (1981) revisited the method for interval constraints under explicit assumptions on Bregman functions (DOI 10.1007/BF00934676).

Setting

Let $E^p$ be $p$-dimensional Euclidean space and $S\subset E^p$ a convex set. Let $f$ be strictly convex on $S$, continuously differentiable over $S$ with gradient $g(x)$, and continuous over the closure $\bar S$. Let $A$ be an $m\times p$ matrix ($m\ge1$) with nonzero rows $A_1,\dots,A_m$, and $b\in E^m$. The inequality program (2.11)–(2.13) is

$$\text{minimize } f(x)\quad\text{subject to}\quad Ax\ge b,\quad x\in\bar S,$$

with feasible set $R=\{x \mid Ax\ge b,\ x\in\bar S\}$, assumed nonempty. The Bregman function is $D(x,y)=f(x)-f(y)-(g(y),x-y)$ (1.4). The $D$-projection $P_iy$ of $y\in S$ onto the hyperplane $A_i=\{x \mid (A_i,x)=b_i\}$ minimizes $D(\cdot,y)$ over $A_i\cap S$. The standing hypotheses ("the conditions of Theorem 3") are that $D$ satisfies the abstract conditions I–VI of §1 for these hyperplanes, together with condition (2) of Note 1: $y^n\to y^*\in\bar S$ implies $D(y^*,y^n)\to0$. In addition, $D$-projections of interior points of $S$ stay in the interior. Condition V (compact sublevel sets of $D(z,\cdot)$) is used for $z\in R$.

Write $Z_0=\{x\in S \mid g(x)=uA \text{ for some } u\ge0\}$, where $uA=\sum_iu_iA_i$, and $\varphi(x,u)=f(x)-(u,Ax-b)$. A run of the method is a sequence of pairs $(x^n,u^n)$ with $x^0\in\operatorname{int}S$, $u^0\ge0$, $g(x^0)=u^0A$, and cyclic indices $i_n$. Each step with $i=i_n$ is one of the following:

• (a) if $(A_i,x^n)<b_i$: $g(x^{n+1})=g(x^n)+\lambda_nA_i$, $(A_i,x^{n+1})=b_i$, and $u_i$ increases by $\lambda_n$;
• (b) if $(A_i,x^n)=b_i$, or $(A_i,x^n)>b_i$ with $u_i=0$: nothing changes;
• (c) if $(A_i,x^n)>b_i$ and $u_i>0$: $g(x^{n+1})=g(x^n)-\mu_nA_i$ with $\mu_n=\min(\mu_n',u_i)$, where $\mu_n'$ is the step that would reach the hyperplane, and $u_i$ decreases by $\mu_n$.

Formalization targets

Goal: Theorem 4

For every run of the method,

$$x^n\to x^*,\qquad x^*\in R,\qquad f(x^*)=\min_{y\in R}f(y).$$

Milestones (steps 1–4 of the proof)

1. $u^n\ge0$ and $g(x^n)=u^nA$ for all $n$ (step 1, (2.20)–(2.21)).
2. $\varphi(x^{n+1},u^{n+1})-\varphi(x^n,u^n)\ge D(x^{n+1},x^n)$ (step 2, (2.22)–(2.24)).
3. For $z\in R$: $D(z,x^n)\le f(z)-\varphi(x^0,u^0)$ and $\varphi(x^n,u^n)\le f(z)$ (step 3, (2.25)–(2.26)).
4. $\{x^n\}$ lies in a compact set, and $\lim\varphi(x^n,u^n)$ exists and is at most $f(z)$ for every $z\in R$ (step 3, (2.27)).
5. $D(x^{n+1},x^n)\to0$, and every limiting point of $\{x^n\}$ lies in $R$ (step 4).

Significance

Theorem 4 says that a method using one constraint per step and only $f$'s gradient converges to the minimizer of a strictly convex function over a polyhedron intersected with $\bar S$. Its multipliers $u^n$ form a dual sequence. Note 4 of the paper deduces from the theorem that the optimal value equals $\sup\varphi(x,u)$ over dual-feasible pairs ($g(x)=uA$, $u\ge0$). The theorem is the convergence statement behind Hildreth's algorithm, behind entropy-based balancing for linear inequality systems, and behind the later "interval convex programming" methods.

The theorem is proved on paper, but no machine-checked proof of it, or of any Bregman-projection row-action method, is known to exist. The formalization adds two things. It makes the paper's standing hypotheses explicit, since several are stated once or left implicit. It also forces a complete argument for the convergence of the whole sequence: the printed proof gets this from condition (2) by an argument that assumes a monotonicity property established in §1 for the pure projection method but not for the primal–dual one. A Lean proof of the goal therefore also supplies a complete proof of the paper's claim.

Difficulty

The standard argument for projection methods uses a Fejér-type property: $D(z,x^n)$ decreases for every feasible $z$. That fails here. In case (c) the point moves away from the hyperplane of a satisfied constraint, and $D(z,x^n)$ can increase. So any argument has to control primal and dual quantities together. To pass from "every limiting point is feasible" to "the whole sequence converges to an optimal point", complementary slackness has to hold in the limit, and this depends on the cyclic order and on the cap $\mu_n\le u_i$. The naive route, applying the §1 convergence theorems to the hyperplanes $A_i$, does not apply, because the iterates are not $D$-projections onto fixed sets in case (c).

Formalization scope

• $E^p$ is EuclideanSpace ℝ (Fin p); the rows are vectors $a_i$, and $uA$ is $\sum_iu_ia_i$. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt on $S$. $S$ is not assumed open, and $f$ is continuous on $\bar S$.
• The $D$-projections form a fixed map $P$. Condition IV is assumed in the one-sided form the proofs use, which the paper's two-sided IV implies. "Compact" means sequentially compact, which agrees with compact in $E^p$. Condition (2) is read with $y^*\in\bar S$.
• Condition V is assumed for $z\in R$, the inequality-feasible set, where the proof applies it. The §1 form (for $z$ in the intersection of the hyperplanes) could hold vacuously for an inequality system.
• Step (a) is encoded by its defining conditions (2.14)–(2.15). Every new point, and the auxiliary point of case (c), lies in $S$. The run starts with $u^0\ge0$, and the cyclic control is $i_n=n\bmod m$ over indices $0,\dots,m-1$.
• Translation slips are corrected: the $Z_0$ set-builder, which breaks off, is completed; "$\mu_n'=u_{i_n}^n$" is read as $\mu_n''=u_{i_n}^n$; "Theorems 1–3" in Theorem 3 means Theorems 1–2.
• The goal quantifies over every run from every admissible start and asserts convergence of the whole sequence together with optimality of the limit. Neither "some limiting point is optimal" nor a single constructed run is an acceptable substitute. The hypotheses are jointly satisfiable, for example by Hildreth's case $f=\|x\|^2/2$, $S=E^p$ with a run that takes a case (a) step, so the goal is not vacuous.
• Needed infrastructure: Bregman distances of differentiable strictly convex functions on non-open convex sets, the strict monotonicity of the gradient, and subsequence and compactness arguments in $E^p$. These are reusable for the companion missions on Theorems 1–3 of the same paper. Contributions are welcome: proofs of the milestones, the full-convergence argument, and the duality statement of Note 4.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• C. Hildreth, A quadratic programming procedure, Naval Res. Logist. Quart. 4 (1957) 79–85. https://doi.org/10.1002/nav.3800040113
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

Motivation

In robust optimization, a decision must satisfy a constraint for every parameter value in a prescribed uncertainty set. A nonlinear uncertain constraint can be difficult to use directly because it contains a universal condition over a continuum of parameters. Ben-Tal, den Hertog, and Vial study constraints whose value is concave in the uncertain parameter. Their Theorem 2 replaces the universal condition by one inequality involving a new vector and two conjugate functions. The replacement is the general framework used for the paper's later examples, including uncertainty regions assembled from simpler sets and nonlinear functions whose conjugates have explicit forms. The discussion paper, §§2–4 is the source for this mission; theorem and page numbers refer to that 2012 version.

The paper's result extends a more specialized counterpart for a linear uncertain constraint under a φ-divergence uncertainty region. That 2013 result has a proved formalization on Prove2Me, but its divergence-specific conjugate and uncertainty set are different objects. The same earlier formalization also supplies a proved version of the self-concordant-barrier statement that this paper quotes as Lemma 33, with a differently printed constant. Neither earlier theorem supplies the general concave-constraint result here.

Setting

Fix dimensions $m,n,L$. The nominal vector is $a^0\in\mathbb R^m$, and $A\in\mathbb R^{m\times L}$ maps a primitive uncertainty $\zeta\in Z\subseteq\mathbb R^L$ to an uncertain parameter $a=a^0+A\zeta$. Thus the uncertainty set is $U=\{a^0+A\zeta:\zeta\in Z\}$. The paper assumes that $Z$ is nonempty, convex, and compact, with $0$ in its relative interior $\operatorname{ri}Z$. Relative interior is taken inside the affine hull of a set, so $Z$ may lie in a lower-dimensional plane.

A decision is $x\in\mathbb R^n$. For each decision, $D(x)$ is the effective domain of the uncertain constraint $f(\cdot,x)$: $f(a,x)$ is real on $D(x)$ and is interpreted as $-\infty$ outside it. The function is concave in $a$ on $D(x)$ for every $x$; the paper imposes no convexity assumption in the decision $x$. The robust constraint (RC) is $f(a,x)\le0$ for every $a\in U$. In the domain representation used here, this means every $a\in U\cap D(x)$. The nominal vector is regular when $a^0\in\operatorname{ri}D(x)$ for every decision $x$, as in Definition 1.

The support function of $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y^Ta$. The partial concave conjugate is $f_*(v,x)=\inf_{a\in D(x)}(a^Tv-f(a,x))$. Both have extended-real values: an empty support set has support value $-\infty$, and the conjugate can be $-\infty$ when its infimum is unbounded below. These values matter in the equivalence; replacing them by a default real number changes the constraint.

Formalization targets

The goal is the paper's Theorem 2. Under the standing assumptions and regularity, for every decision $x$,

$$\left[\forall a\in U\cap D(x),\ f(a,x)\le0\right] \quad\Longleftrightarrow\quad \left[\exists v\in\mathbb R^m:\ (a^0)^Tv+\delta^*(A^Tv\mid Z)-f_*(v,x)\le0\right].$$

The right-hand inequality is the Fenchel robust counterpart (FRC). Its existence claim is essential: equality of primal and dual infima alone would not show that an auxiliary vector satisfying FRC exists.

Four source statements form the milestone path. Remark 5 gives the weak-duality inequality and the FRC-to-RC implication without concavity. Equations (16)–(18) calculate the support function of $U$. Equation (7) states the relative-interior qualification. Equations (13)–(15) state the worst-case/dual-value identity and, through the printed minimum, attainment of the dual infimum. The milestone list quotes those source passages and identifies their printed pages. Theorem 2 and its proof appear on pp. 4–5.

Significance

The equivalence gives an exact way to replace an infinite family of uncertain inequalities by an existential constraint. In examples where the support function and concave conjugate can be evaluated or represented with standard optimization constraints, it yields a finite robust counterpart. The conclusion remains a mathematical equivalence even when such an explicit representation has not been found. It is also independent of any convexity of $f$ in the decision variable, a point the paper makes after Corollary 3.

This mission supplies reusable, domain-aware support and conjugate definitions and formal statements for the duality path in the paper's central result. The new goal and milestones are open proof obligations: their Lean declarations compile, but they do not yet have machine-checked proofs. The proved 2013 φ-divergence case is narrower and does not close them. A completed development would make the general relative-interior and attained-duality steps reusable for other robust optimization models.

Difficulty

The delicate point is the direction from RC to the existence of an FRC vector. Weak duality gives only a one-sided bound. Identifying the two optimal values still leaves an existence question when an infimum is not attained. The paper invokes Fenchel duality under a relative-interior intersection condition; replacing relative interior by ordinary interior would exclude lower-dimensional uncertainty sets and effective domains that the source permits. A second difficulty is keeping finite and infinite conjugate values distinct while subtracting them in the counterpart inequality. An unbounded-below conjugate must make a finite-support FRC value $+\infty$, not a plausible finite number.

Formalization scope

Vectors are functions on Fin m, Fin n, and Fin L; $A$ is a real matrix, and dot products use the finite-vector dot product. Mathlib's intrinsicInterior ℝ represents relative interior. The domain map $D(x)$ is explicit, with the concavity hypothesis imposed on that domain. The real representative of $f$ outside $D(x)$ is ignored everywhere. The paper's Notation paragraph calls its generic concave functions closed, but the statements here omit closedness: the finite-dimensional duality qualification used for Theorem 2 needs relative-interior overlap, not that extra regularity. This is a stated strengthening of the source theorem, not a change of its feasible points.

Support functions, conjugates, worst-case values, and dual values use EReal. The paper's “max” in (8), (13), and Remark 5 is read as an extended-real supremum; its “min” in (15) is an infimum accompanied by an attaining vector. The support identity includes $Z=\varnothing$, where both sides are $-\infty$, although Theorem 2 keeps the paper's nonempty, convex, compact $Z$. On the theorem's hypotheses the support value is finite and $D(x)$ is nonempty, so the undefined-looking combinations $+\infty-(+\infty)$ and $-\infty+(+\infty)$ cannot occur in FRC. No all-space real-valued substitute for $f_*$ is used, and the theorem still quantifies over every decision and every allowed uncertainty vector.

The proof development needs finite-dimensional relative-interior behavior under affine maps and Fenchel duality with attainment. General convex conjugates and support functions can serve later missions. Corollary 3 and the paper's complexity discussion are outside this mission. Theorem A.1 is not separately made a milestone here: as printed, its domain-restricted dual maximum has a problematic $-\infty$ case; the directly used, attained identity (13)–(15) is the target under the main theorem's standing assumptions.

Selected references

• A. Ben-Tal, D. den Hertog, J.-P. Vial, Deriving robust counterparts of nonlinear uncertain inequalities, CentER Discussion Paper 2012-053, Tilburg University, 2012. Discussion-paper PDF; journal version, Mathematical Programming, 2015, DOI 10.1007/s10107-014-0750-8.
• A. Ben-Tal et al., Robust solutions of optimization problems affected by uncertain probabilities, Management Science, 2013. Prove2Me formalization of its φ-divergence case.