Convex Optimization

Motivation

Many optimization problems in operations research are posed on an expectation: a two-stage or multistage stochastic program minimizes $f(x) = E\,F(x,\xi)$, where $F(\cdot,\xi)$ is convex but nonsmooth and the expectation cannot be computed exactly. What can be computed is a stochastic subgradient, a random vector whose mean is a subgradient of $f$. The stochastic subgradient method replaces the exact subgradient in the classical method by such a random vector. It was introduced by Yu. M. Ermoliev and N. Z. Shor in 1968 and developed by Ermoliev, Nurminski and others into a standard tool of stochastic programming; the same scheme, under the name stochastic (sub)gradient descent, underlies most of large-scale machine learning.

This mission formalizes Section 2.6 of N. Z. Shor, Minimization Methods for Non-Differentiable Functions (Springer 1985): the almost-sure convergence theorem for the stochastic subgradient method (Theorem 2.19), together with two deterministic results of the same section on perturbed and restarted variants of the subgradient method (Theorems 2.18 and 2.20).

Timeline, as recorded in the book:

• 1968, Ermoliev and Shor: the notion of a stochastic subgradient, introduced for a random search method for two-stage stochastic programs; the convergence theorem reproduced as Theorem 2.19.
• 1972, Bazhenov: convergence of a subgradient method with restarts for almost differentiable (in general nonconvex) functions, Theorem 2.18.
• 1976, Shepilov: stability of the subgradient method with respect to errors in the point where the subgradient is computed, Theorem 2.20.

Setting

$E_n$ is $n$-dimensional Euclidean space with inner product $(x,y)$. A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$; $M^*$ is the set of minimum points of $f$.

Stochastic subgradient method. Fix a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_k)_{k \ge 0}$, a deterministic starting point $x_0$, stepsize rules $h_k : E_n \to \mathbb{R}$ and random vectors $g_k : \Omega \to E_n$. The iterates are

$$x_{k+1} = x_k - h_k(x_k)\, g_k, \qquad k = 0,1,\dots$$

In the book's notation $g_k = g_\omega(x_k)$: a random vector whose expectation, given the state at step $k$, is a subgradient of $f$ at $x_k$. In the Lean development the iterates are stochIter h G x₀ k ω.

Perturbed subgradient method (Shepilov). Given a subgradient selection $g_f$, points $\tilde x_k$ with $\|\tilde x_k - x_k\| \le \delta_k$, and steps $h_k > 0$: $x_{k+1} = x_k - h_k\, g_f(\tilde x_k)/\|g_f(\tilde x_k)\|$.

Restarted method (Bazhenov). For a function $f$ that is almost differentiable (Lipschitz on bounded sets, differentiable almost everywhere, with gradient continuous where it exists) and a selection $g_f(x)$ of almost-gradients (limit points of gradients at nearby points of differentiability), with $S_r = \{x : \|x - x^*\| \le r\}$: take the normalized step $\bar x_{k+1} = x_k - h_k\, g_f(x_k)/\|g_f(x_k)\|$ and restart from $x_0$ whenever $\bar x_{k+1}$ leaves $S_r$ (resetIter).

Formalization targets

Goal: Theorem 2.19 (p. 46)

Let $f$ be convex with a unique minimum point $x^*$. Suppose $E\{g_k \mid \mathcal F_k\}$ is a subgradient of $f$ at $x_k$, $E\{\|g_k\|^2 \mid \mathcal F_k\} \le c$, and almost surely $h_k(x_k) > 0$, $\sum_k h_k(x_k) = +\infty$, $\sum_k h_k^2(x_k) < \infty$. Then

$$P\Big(\lim_{k\to\infty} \|x_k - x^*\| = 0\Big) = 1 .$$

Milestones

1. Eq. (2.42), the conditional one-step inequality

$$E\{\|x_{k+1} - x^*\|^2 \mid \mathcal F_k\} \le \|x_k - x^*\|^2 + c\,h_k^2(x_k).$$

2. Proof of Theorem 2.19, pp. 46–47: with probability one $\|x_k - x^*\|^2$ converges to a finite limit (no divergence condition on the steps).
3. Theorem 2.20 (Shepilov): under $\delta_k \to 0$, $\sum h_k\delta_k < \infty$, $\sum h_k^2 < \infty$, $\sum h_k = \infty$, the perturbed method converges to a point of $M^*$.
4. Theorem 2.18 (Bazhenov): if $f(x^*) = \min_{S_r} f$ and $\inf_{S_r\setminus S_\varepsilon} (g_f(x), x - x^*) > 0$ for every $0 < \varepsilon < r$, the restarted method with $h_k \to 0$, $\sum h_k = \infty$ converges to $x^*$ from any $x_0 \in S_r$.

Significance

Theorem 2.19 is the basic justification of stochastic subgradient methods: without computing $f$ or any exact subgradient, the method reaches the minimizer with probability one, under stepsize conditions that are met by $h_k = 1/(k+1)$. It is the nonsmooth convex counterpart of the Robbins–Monro theorem and the prototype of the almost-sure convergence results for stochastic quasi-gradient methods used in stochastic programming. Theorem 2.20 shows that the deterministic method tolerates summable errors in the point where the subgradient is evaluated, which is what allows subgradients to be approximated by finite differences (Section 1.3). Theorem 2.18 extends the convergence of the normalized method to local minima of a class of nonconvex functions.

All four results are proved in the literature. To the best of the platform search (September 2026), none is machine-checked: the platform has almost-sure convergence theorems for smooth stochastic approximation under ODE-type hypotheses (Borkar–Meyn) and in-expectation bounds for stochastic gradient descent, neither of which covers this recursion. A formal proof of the goal would give a reusable almost-sure convergence argument for nonsmooth stochastic methods on top of Mathlib's martingale theory.

Difficulty

The deterministic proof of convergence of the subgradient method compares $\|x_{k+1}-x^*\|^2$ with $\|x_k - x^*\|^2$ along the whole trajectory. With random directions this comparison holds only in conditional expectation, and the term $h_k(g_k - E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ is not controlled pathwise. Taking expectations of the one-step inequality and summing gives only bounds on $E\|x_k - x^*\|^2$, which do not yield almost-sure convergence. Moreover the stepsize $h_k(x_k)$ depends on the random iterate, so the conditions $\sum h_k^2(x_k) < \infty$ and $\sum h_k(x_k) = \infty$ hold only almost surely, not uniformly, and the iterates need not be square-integrable. Identifying the almost-sure limit as $0$ requires using the uniqueness of the minimizer to bound $(E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ away from zero outside a neighbourhood of $x^*$.

In Theorems 2.18 and 2.20 the difficulty is that the distance to $x^*$ is not monotone: steps taken near the solution, or with a perturbed subgradient, can increase it, and a restart can move the iterate far away.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere); convexity is ConvexOn ℝ Set.univ f; uniqueness of $x^*$ is a separate hypothesis.
• Probabilistic model. The book assumes the distribution of $g_\omega(x_k)$ is determined by $x_k$ and independent of the past, and remarks this is inessential. The formalization uses a filtration: $g_k$ is $\mathcal F_{k+1}$-measurable, each $h_k$ is Borel measurable, $x_0$ is deterministic, and the hypotheses are on conditional expectations given $\mathcal F_k$. This contains the book's model.
• Condition (iii) is printed as $E\|g_\omega(x_k)\|^2 \le c$; the proof uses the conditional bound in (2.42), and the formalization assumes the conditional bound $E\{\|g_k\|^2\mid\mathcal F_k\} \le c$ almost surely.
• Every expectation carries an integrability hypothesis ($g_k$ and $\|g_k\|^2$ integrable), so no conditional expectation defaults to Lean's junk value $0$. The one-step milestone assumes $\|x_k - x^*\|^2$ integrable and a bounded stepsize rule at that step, and concludes integrability of $\|x_{k+1}-x^*\|^2$.
• Conditions (i)–(ii) on the random stepsizes are required almost surely. "With probability one $\lim\|x_k - x^*\| = 0$" is ∀ᵐ ω ∂μ, Tendsto (fun k => ‖x k ω - x*‖) atTop (𝓝 0).
• Division by zero. In Theorems 2.18 and 2.20 the normalized step is undefined when the subgradient vanishes; the formalization skips the step (the iterate is repeated) by an explicit branch, not through Lean's convention $x/0 = 0$. When the subgradient never vanishes the sequences are exactly the book's.
• The printed display (2.42) has $x_k$ where $x_{k+1}$ is meant on its left-hand side; the corrected inequality is stated.
• A trivializing formalization, for instance dropping the integrability hypotheses so that the conditional expectations vanish, or quantifying the stepsize conditions so that they cannot hold, is excluded by the hypotheses above; the hypotheses are satisfiable (deterministic subgradients of $f(x) = \|x\|$ with $h_k = 1/(k+1)$).
• Mathlib supplies conditional expectation (MeasureTheory.condExp), filtrations, and almost-sure convergence of $L^1$-bounded (sub/super)martingales; the supermartingale convergence theorem the book cites from Doob is used from Mathlib, not restated. A Robbins–Siegmund-type lemma for nonnegative almost-supermartingales would be the natural reusable contribution. The almost-differentiability and subgradient definitions duplicate drafts of other missions in this series.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Section 2.6, pp. 44–47. https://doi.org/10.1007/978-3-642-82118-9
• Yu. M. Ermoliev and N. Z. Shor, A random search method for two-stage problems of stochastic programming and its generalization, Kibernetika (Kiev), no. 1, 90–92, 1968.
• L. G. Bazhenov, On the conditions for convergence of methods for minimizing almost differentiable functions, Kibernetika (Kiev), no. 4, 71–72, 1972.
• M. A. Shepilov, On a method of generalized gradient for finding the absolute minimum of a convex function, Kibernetika (Kiev), no. 4, 52–57, 1976.
• Yu. M. Ermoliev, Methods of Stochastic Programming, Nauka, Moscow, 1976.
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971, pp. 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953 (supermartingale convergence theorem).

Motivation

The subgradient method for a convex function $f$ moves from $x_k$ against a subgradient $g_f(x_k)$, and everything hinges on the step length. Divergent-series stepsizes guarantee convergence but are slow and need no information about $f$. When the optimal value $f^*$, or any level $c$ that is known to be attainable, is available, B. T. Polyak proposed in 1969 the step

$$x_{k+1} = x_k - \frac{\gamma\,[f(x_k) - c]}{\|g_f(x_k)\|^2}\, g_f(x_k),$$

which uses the current gap $f(x_k) - c$ to scale the move. This Polyak stepsize is still the reference adaptive rule in nonsmooth convex optimization, in the solution of convex feasibility problems, and in the Lagrangian relaxation heuristics of integer programming (Held–Wolfe–Crowder, Camerini–Fratta–Maffioli), where it is known under the name "relaxation step".

Section 2.4 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) places Polyak's rule in the framework of Fejér-type approximations developed by I. I. Eremin: an iteration whose map strictly decreases the distance to every point of a target set. It then proves convergence of the rule, linear rates under growth conditions, its behaviour when the level is set too low, and a property of the conjugate-subgradient direction of Camerini, Fratta and Maffioli (1975).

Timeline:

• 1965–1969: Eremin introduces Fejér mappings for systems of convex inequalities.
• 1969: Polyak, Minimization of unsmooth functionals, proposes the step with the known optimal value and proves convergence and a linear rate under a sharp-minimum condition.
• 1975: Camerini, Fratta and Maffioli combine the Polyak step with a conjugate direction for Lagrangian relaxation.
• 1985: Shor's book collects these results in Section 2.4 (Theorems 2.10–2.16).

Setting

$E_n$ is the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$. A subgradient selection is a map $g_f$ with $g_f(x)$ a subgradient at every $x$; nothing else is assumed about it, in particular not continuity.

For a nonempty set $M \subseteq E_n$, a map $\varphi : E_n \to E_n$ is $M$-Fejér if $\varphi(y) = y$ and $\|\varphi(x) - y\| < \|x - y\|$ for all $y \in M$ and $x \notin M$.

For a convex $f$ with $f^* = \inf f$ and a level $c \ge f^*$, let $M(c) = \{x : f(x) \le c\}$. Polyak's method (2.32) is the iteration $x_{k+1} = \varphi_c(x_k)$ with the map displayed above for $x \notin M(c)$ and $\varphi_c(y) = y$ on $M(c)$; the factor $\gamma$ is fixed in $(0, 2)$.

The conjugate-subgradient procedure (2.38), for a convex $f$ with minimum point $x^*$ and $f^* = f(x^*)$, is

$$x_{k+1} = x_k - h_k s_k, \quad h_k = \frac{[f(x_k) - f^*]\gamma_k}{\|s_k\|^2}, \qquad s_0 = g_f(x_0),\quad s_k = g_f(x_k) + \beta_k s_{k-1}.$$

Formalization targets

Goal: Theorem 2.11

If $0 < \gamma < 2$ and $M(c) \neq \emptyset$, then for any $x_0 \in E_n$

$$\exists k^* : x_{k^*} \in M(c) \qquad \text{or} \qquad \lim_{k \to \infty} x_k \text{ exists and lies in } M(c).$$

The goal fixes no constant and no rate; it asserts only that the method finds a point of the level set, in finite time or in the limit.

Milestones

1. Theorem 2.10. Iterates of a continuous $M$-Fejér map converge to a point of $M$.
2. Inequality (2.33). For $x_k \notin M(c)$ and $y \in M(c)$,

$$\|x_{k+1} - y\|^2 \le \|x_k - y\|^2 - \gamma(2-\gamma)\frac{[f(x_k) - c]^2}{\|g_f(x_k)\|^2} < \|x_k - y\|^2 .$$

3. Theorem 2.12. Under $f(x) - f^* \ge m\|x - x^*\|^2$ and an $L$-Lipschitz gradient near $x^*$, with $c = f^*$: $\|x_k - x^*\| \le q^k \|x_0 - x^*\|$, $q = (1 - \gamma(2-\gamma)m^2/L^2)^{1/2} < 1$.
4. Theorem 2.13. Under the sharp-minimum condition $f(x) - f(x^*) \ge m\|x - x^*\|$ and subgradients bounded by $L$ near $x^*$, with $c = f(x^*)$: $\|x_{k+1} - x^*\| \le q\|x_k - x^*\|$.
5. Theorem 2.14. If $\min \psi = d > 0$ and the method runs with $c = 0$, then $\lim_k \min_{0 \le i \le k} \psi(x_i) \le 2d/(2-\gamma)$.
6. Theorem 2.15. For (2.38) with $0 < \gamma_k \le 1$, $\beta_k \ge 0$: $(x_k - x^*, s_k) \ge (x_k - x^*, g_f(x_k))$.
7. Theorem 2.16. With the Camerini–Fratta–Maffioli coefficient $\beta_k$ and $0 \le \alpha_k \le 2$: $(x_k - x^*, s_k)/\|s_k\| \ge (x_k - x^*, g_f(x_k))/\|g_f(x_k)\|$.

Significance

Theorem 2.11 is the convergence guarantee of the most widely used adaptive step rule for nonsmooth convex problems. With $c = f^*$ it yields a minimizer; with $c > f^*$ it solves the convex inequality $f(x) \le c$, and applied to $\psi = \max_i f_i^+$ it solves consistent systems of convex inequalities. The linear rates of Theorems 2.12–2.13 are the prototype of the "sharpness implies linear convergence" results of modern first-order methods, and Theorem 2.14 quantifies the loss when the level is underestimated, which is the situation of every practical variant that estimates $f^*$ on the fly. Theorems 2.15–2.16 are the justification of the conjugate-subgradient directions used in Lagrangian relaxation.

All results are classical and proved on paper. None of them is formalized on Prove2Me: the platform has a smooth, strongly convex Polyak gradient-descent bound (a different theorem) and Fejér-monotonicity statements for polyhedral relaxation methods, but no Polyak subgradient step, no $M$-Fejér map and no conjugate-subgradient procedure. The mission produces machine-checked versions of the whole section, with the page's misprints corrected where the proof and the statement disagree.

Difficulty

The obvious argument for the goal is to observe that $\varphi_c$ is $M(c)$-Fejér, by (2.33), and invoke Theorem 2.10. That argument fails: Theorem 2.10 needs a continuous map, and $\varphi_c$ depends on an arbitrary subgradient selection, which is discontinuous wherever $f$ is not differentiable. The book says so explicitly. Fejér monotonicity gives boundedness and a limit of each distance $\|x_k - y\|$, but convergence of the whole sequence to a single point of $M(c)$, and the fact that an accumulation point cannot lie outside $M(c)$, have to be obtained without continuity of the map.

For Theorem 2.14 the level $c = 0$ lies strictly below the minimum, so $M(0) = \emptyset$, the target set of the iteration as run is empty, no Fejér property is available for it, and the theorem controls only the best value found, not the iterates.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued on all of $E_n$ and ConvexOn ℝ Set.univ f.
• The subgradient selection is universally quantified; no theorem assumes continuity of it.
• Iterations are sequences x : ℕ → E_n with the recursion as a hypothesis; the first term is arbitrary.
• Polyak's step map is defined piecewise: it returns $x$ on $M(c)$ (as the book sets $\varphi_c(y) = y$) and at $g_f(x) = 0$. No statement relies on Lean's convention $x/0 = 0$. The same holds for $h_k$ when $s_k = 0$.
• $M(c) \neq \emptyset$ is a hypothesis of the goal: the book's proof picks $y \in M(c)$, and for $c = f^*$ not attained the conclusion is false (for $f = e^x$, $c = 0$, the method moves by $\gamma$ each step and diverges).
• "$\lim x_k \in M(c)$" is the existence of a limit in $M(c)$, not a statement about cluster points.
• $\gamma \in (0, 2)$ is stated in every theorem on Polyak's method; the book fixes this range at Theorem 2.11.
• Theorem 2.12's "strongly convex" is used through its displayed growth condition only; the statement is made for convex $f$ satisfying it, with $L > 0$ and $q$ computed with Real.sqrt.
• Theorem 2.13 assumes the bound $\|g\| \le L$ on subgradients in the ball, which is what the proof uses; a Lipschitz constant on the closed ball alone does not give it, and the printed statement fails without it.
• Theorem 2.14 is stated with "$\le 2d/(2-\gamma)$"; the printed "$=$" is false in general.
• Theorem 2.16's inequality is stated at indices where $s_k \neq 0$ and $g_f(x_k) \neq 0$.

A formalization in which $M(c)$ may be empty, the selection is assumed continuous, or the step divides by zero through Lean's conventions would be a different theorem; these are ruled out above.

Needed infrastructure: Fejér monotone sequences in finite dimensions (bounded, with convergent distances), the subgradient inequality, and the fact that a zero subgradient characterizes a minimum. These are reusable for every subgradient-type method. Contributions of general lemmas on Fejér-monotone sequences are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §2.4, pp. 36–42. https://doi.org/10.1007/978-3-642-82118-9
• B. T. Polyak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9(3), 1969, 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
• I. I. Eremin, The relaxation method of solving systems of inequalities with convex functions on the left-hand side, Soviet Mathematics Doklady 6, 1965, 219–222.
• P. M. Camerini, L. Fratta, F. Maffioli, On improving relaxation methods by modified gradient techniques, Mathematical Programming Study 3, 1975, 26–34.

Motivation

The subgradient method minimizes a convex function $f$ on $\mathbb{R}^n$ that need not be differentiable, by stepping against an arbitrary subgradient. With stepsizes $h_k \to 0$, $\sum h_k = \infty$ it converges (Shor, Theorem 2.2), but in general only slowly: no stepsize rule that ignores the structure of $f$ gives a geometric rate. Section 2.3 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) identifies geometric conditions on $f$ under which a simple geometric stepsize rule does give linear convergence — convergence with the speed of a geometric progression — and computes the rate explicitly.

The results are the origin of what is now studied as sharpness or error-bound conditions for nonsmooth optimization. Their practical content is that nonsmooth problems whose level sets are not too elongated near the minimum (piecewise-linear functions, maxima of finitely many well-conditioned pieces, positive definite quadratics) can be solved by the subgradient method at a linear rate, with a stepsize rule that needs only one or two scalar parameters.

Timeline. Shor proposed the subgradient method in 1962. The book presents the geometric stepsize rule under an angle condition (Theorem 2.7) and its level-surface form (Theorem 2.8), and attributes the block-halving rule of Theorem 2.9 to its reference [94]. Goffin (Math. Programming 13, 1977) gave the sharp rate in terms of a condition number of the level sets. The book compares the quadratic case with L. V. Kantorovich's rate for steepest descent.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and $f : E_n \to \mathbb{R}$ convex. A vector $g$ is a subgradient of $f$ at $x$ if $f(y) - f(x) \ge (g, y - x)$ for all $y$; $g_f(x)$ denotes an arbitrary subgradient at $x$, chosen once for each $x$. Let $M^*$ be the set of minimum points of $f$, assumed nonempty; for $x \in E_n$, $x^*(x)$ is the point of $M^*$ nearest to $x$.

Given a starting point $x_0$ and positive stepsizes $h_1, h_2, \dots$, the normalized subgradient method is

$$x_{k+1} = x_k - h_{k+1}\frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, 2, \dots,$$

stopped when $g_f(x_k) = 0$ (then $x_k \in M^*$).

Two shape conditions are used. The angle condition (2.12) with angle $0 \le \varphi < \pi/2$ asks that every subgradient make an angle at most $\varphi$ with the direction to the nearest minimum point:

$$(g_f(x), x - x^*(x)) \ge \cos\varphi\,\|g_f(x)\|\,\|x - x^*(x)\|.$$

The level-surface ratio condition (2.20), for a function with unique minimum point $x^*$, asks that on a ball $Y$ around $x^*$ any two points $x, z$ on a common level surface $f(x) = f(z) \ne f(x^*)$ satisfy $\|x - x^*\| \le \sigma\|z - x^*\|$.

Formalization targets

Goal: Theorem 2.8 (p. 32)

If $f$ has a unique minimum point $x^*$, $\sigma \ge \sqrt2$, $h_1 \ge \|x_0 - x^*\|/\sigma$, and (2.20) holds on $Y = \{y : \|y - x^*\| \le \sigma h_1\}$, then with $h_{k+1} = h_k\sqrt{\sigma^2-1}/\sigma$

$$\|x_k - x^*\| \le h_{k+1}\,\sigma, \qquad k = 0, 1, 2, \dots$$

Milestones

1. Theorem 2.7 (pp. 30–31): under (2.12) and the geometric rule $h_{k+1} = h_k r(\varphi)$ with $r(\varphi) = \sin\varphi$ for $\varphi \ge \pi/4$ and $r(\varphi) = 1/(2\cos\varphi)$ for $\varphi < \pi/4$,

$$\|x_k - x^*(x_k)\| \le h_{k+1}/\cos\varphi \quad\text{resp.}\quad 2h_{k+1}\cos\varphi .$$

2. Remark after Theorem 2.7 (p. 32): the same conclusion when (2.12) holds only at the iterates.
3. Inequality (2.22) (p. 33): (2.20) on $Y$ implies $(g, x - x^*) \ge \sigma^{-1}\|g\|\,\|x - x^*\|$ for every $x \in Y$ and every subgradient $g$ at $x$.
4. Example (p. 33): for $A$ symmetric positive definite with extreme eigenvalues $\lambda \le \mu$,

$$\min_{x \ne 0}\frac{(Ax, x)}{\|Ax\|\,\|x\|} = \frac{2\sqrt{\lambda\mu}}{\lambda + \mu},$$

attained at $x = \sqrt{\mu/(\lambda+\mu)}\,s_1 + \sqrt{\lambda/(\lambda+\mu)}\,s_2$. 5. Theorem 2.9 (p. 34): under the assumptions of Theorem 2.8 with $\sigma \ge 2$, the rule $h_{k+1} = h_0 2^{-[(k+1)/N]}$ with $N \ge 3\sigma^2 + 1$ gives $\|x_k - x^*\| \le 2\sigma h_{k+1}$.

Significance

The results. Theorem 2.7 shows that the subgradient method, often dismissed as sublinear, converges linearly once the geometry of $f$ is controlled and the stepsizes decrease geometrically at the right ratio; the rate $r(\varphi)$ depends only on the angle. Theorem 2.8 restates the hypothesis in terms of the shape of level surfaces, a condition that can be checked for concrete functions, and gives rate $\sqrt{\sigma^2-1}/\sigma$. The Example computes the angle for positive definite quadratics, yielding rate $(\varrho - 1)/(\varrho + 1)$ with $\varrho = \mu/\lambda$ the condition number — the same rate as steepest descent with exact line search in Kantorovich's analysis, obtained with less storage. Theorem 2.9 removes the need to know $\sigma$ exactly in the stepsize ratio.

Formalizing them. All five results are proved in the book; none is formalized, and no linear-rate result for a nonsmooth first-order method is on the platform. The formalization pins the constants (2.13)–(2.19), the stepsize indexing, and the treatment of the stopped iteration; the Example is a Kantorovich-type inequality for symmetric operators that is reusable beyond this mission.

Difficulty

The obvious one-step estimate $\|x_{k+1} - x^*\|^2 = \|x_k - x^*\|^2 - 2h_{k+1}(g, x_k - x^*)/\|g\| + h_{k+1}^2$ alone does not contract: the step length is fixed in advance and does not shrink with the distance, so a step may overshoot the minimum. The rate argument has to track the ratio between the current distance and the current stepsize, and the admissible ratio of stepsizes is dictated by the worst case of this quadratic in the distance; in the two regimes $\varphi \ge \pi/4$ and $\varphi < \pi/4$ the worst case sits at different ends. For Theorem 2.8, the shape condition is only assumed on the ball $Y$, so the iterates must be shown to stay in $Y$, and the passage from level surfaces to subgradients needs the distance from $x^*$ to a level surface, which is not a quantity the iteration computes. Theorem 2.9's constant stepsize blocks are not monotone in distance at all, and the count $3\sigma^2 + 1$ must be matched against a worst-case phase.

Formalization scope

The space $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued and ConvexOn ℝ Set.univ. A subgradient selection is an arbitrary function g with g x a subgradient at every x, quantified universally. Stepsizes are h : ℕ → ℝ with h (k+1) used at step k; the recursions $h_{k+1} = h_k r$ are imposed for $k \ge 1$, $h_1$ being the chosen initial step (the book's "$k = 0, 1, 2, \dots$" in Theorem 2.8 is read this way). The iteration stops at $g_f(x_k) = 0$ by an explicit branch that repeats $x_k$, never through $x/0 = 0$; the bounds are asserted for every $k$, which implies the book's "either the method stops or …" form. $x^*(x)$ is a definition (the nearest point of the set of minima), and the set of minima is assumed nonempty. Unique minimum is stated as $M^* = \{x^*\}$. The ball $Y$ is closed, and (2.20) is assumed only for pairs in $Y$ with a common value different from $f(x^*)$. In (2.16) the ratio is $1/(2\cos\varphi)$, as the proof requires, where the page prints "1/2 cos φ". In Theorem 2.9, "the assumptions of Theorem 2.8" are taken with $h_1 = h_0$, which fixes $h_0 \ge \|x_0 - x^*\|/\sigma$ and $Y$ of radius $\sigma h_0$. In the Example, the extreme eigenvalues are pinned by $\lambda\|x\|^2 \le (Ax,x) \le \mu\|x\|^2$ together with unit eigenvectors, and the minimum is stated with IsLeast.

A statement in which the stepsizes or the bound constants could be chosen after the iterates, or in which the shape condition quantified over an empty set of pairs, would be trivially true; here every constant is fixed by the hypotheses before the sequence is generated, and the conditions are the book's.

Needed infrastructure: the subgradient inequality, continuity of convex functions on $\mathbb{R}^n$, nearest points of closed convex sets, and elementary trigonometry. The nearest-point map and the stepsize ratio are defined within the mission; the subgradient inequality, the set of minima and the iteration come from the series' shared definitions. Contributions welcome: proofs of the milestones, and a reusable Kantorovich-type cosine bound for symmetric positive definite operators.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §2.3, pp. 30–36. https://doi.org/10.1007/978-3-642-82118-9
• J.-L. Goffin, On convergence rates of subgradient optimization methods, Mathematical Programming 13 (1977) 329–347. https://doi.org/10.1007/BF01584346
• L. V. Kantorovich, Functional analysis and applied mathematics, Uspekhi Mat. Nauk 3 (1948) 89–185 (steepest descent rate for quadratics, cited by Shor as [45]).

Motivation

Stochastic quasigradient (SQG) methods minimize an expectation $F(x)=E_\omega f(x,\omega)$ over a constraint set $X\subseteq\mathbb R^n$ when neither $F$ nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with $\rho_s\to0$, $\sum\rho_s=\infty$, $\sum\rho_s^2<\infty$. Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.

Timeline:

• 1951: Robbins and Monro, stochastic approximation with programmed steps.
• 1976: Ermoliev, Methods of Stochastic Programming: the SQG projection method and its a.s. convergence through stochastic quasi-Féjer sequences.
• 1983: Mirzoakhmedov and Uryasev (Zh. Vychisl. Mat. i Mat. Fiz., cited as [7] in Ch. 18 and [14] in Ch. 17): Cesàro convergence of the weighted mean with $\rho_s\to0$ and $\sum\rho_s=\infty$ only, under the two measurability regimes. Chapter 17 states it as Theorem (ii); Chapter 18 as Theorem 1.
• 1988: Uryasev, Ch. 18, applies it to the adaptive rule (18.5) (Theorem 2).
• 1992: Polyak and Juditsky, averaging of iterates for smooth stochastic approximation, with optimal asymptotic variance.

Setting

Let $X\subseteq\mathbb R^n$ be nonempty, convex and compact, $C_1=\max_{x,y\in X}\|x-y\|$ its diameter, and $F$ convex on an open convex set $U\supseteq X$, with subdifferential $\partial F(x)$. The projection $\pi_X(y)$ is the point of $X$ nearest to $y$. On a probability space, the SQG method generates

$$x^{s+1}=\pi_X(x^s-\rho_s\xi^s),\qquad s=0,1,\dots\qquad(18.2)$$

from $x^0\in X$, where the direction $\xi^s$ is a stochastic quasigradient: $E(\xi^s\mid B_s)=F_x(x^s)+b^s$ with $F_x(x^s)\in\partial F(x^s)$, a bias $b^s$, and $B_s$ the $\sigma$-algebra induced by $(x^0,\dots,x^s,\xi^0,\dots,\xi^{s-1})$.

The adaptive stepsize rule of the chapter is, for fixed $a>1$, $\delta>0$ and $\rho_0>0$,

$$\rho_{s+1}=\rho_s\,a^{\langle\xi^{s+1},\,x^s-x^{s+1}\rangle-\delta\rho_s}\qquad(18.5).$$

The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are

$$\bar x^s=\sum_{\ell=0}^s\rho_\ell x^\ell\Big/\sum_{\ell=0}^s\rho_\ell\qquad(18.6).$$

The sequence $x^s$ is Cesàro convergent when $\bar x^s$ converges to the solution set.

Chapter 17 (Pflug) uses the same method for $f(x)=E_P\,q(x,\xi)$ over a closed convex $S\subseteq\mathbb R^k$, with $Y=\nabla q(X_n,\xi_n)$ from i.i.d. $\xi_n$ and stepsizes adapted to $\sigma(\xi_0,\dots,\xi_{n-1})$.

Formalization targets

Goal: Theorem 2 of Chapter 18

Under $\sup_s\|\xi^s\|<C_2$ (18.15), $\limsup\|b^s\|\le\bar b$ (18.16) and $\delta>C_2\limsup_s\inf_{h\in\partial F(x^s)}\|\xi^s-h\|$ (18.17), almost surely,

$$\limsup_{s\to\infty}\Big(F(\bar x^s)-\min_{x\in X}F(x)\Big)\le\bar b\,C_1,$$

and if $b^s\to0$ a.s., then $F(\bar x^s)\to\min_XF$ and all accumulation points of $\bar x^s$ are minimizers, almost surely.

Milestones

1. Chapter 17, Theorem (i): $\sum\rho_n=\infty$ and $\sum\rho_n^2<\infty$ a.s. imply $X_n\to x^*$ a.s.
2. Chapter 17, Theorem (ii): for convex $f$ and bounded $S$, $\rho_n\to0$ and $\sum\rho_n=\infty$ a.s. imply $\bar X_n\to x^*$ a.s.
3. Chapter 18, Theorem 1: for any stepsizes with $\rho_s>0$, $E\rho_s^2<\infty$, $\rho_s\to0$, $\sum\rho_s=\infty$ and measurability condition (1) or (2), $\limsup F(\bar x^s)-F(x^*)\le\bar bC_1$ a.s.
4. Chapter 18, Corollary: with $b^s\to0$, the accumulation points of $\bar x^s$ are solutions.
5. Eq. (18.18): $\|x^{s+1}-x^s\|\le\|\rho_s\xi^s\|\le\rho_sC_2$.
6. Proof of Theorem 2, step 1: the adaptive steps satisfy $\sum\rho_s=\infty$.
7. Proof of Theorem 2, step 2: under (18.17), $\rho_s\to0$.
8. End of step 2: $\rho_s\to0$ implies $\rho_{s+1}/\rho_s\to1$.

Significance

Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only $\rho_s\to0$ and $\sum\rho_s=\infty$. It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to $1$.

The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).

Difficulty

The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls $\|x^s-x^*\|^2$ and needs $\sum\rho_s^2\|\xi^s\|^2<\infty$, which is exactly what is not available here. The averaged analysis has to show that the martingale term $\sum_\ell\rho_\ell\langle\xi^\ell-E(\xi^\ell\mid B_\ell),x^*-x^\ell\rangle$ is $o(\sum_\ell\rho_\ell)$ almost surely, and that $\sum_\ell\rho_\ell^2\|\xi^\ell\|^2$ is $o(\sum_\ell\rho_\ell)$, when the stepsizes are themselves random. Under condition (2) of Theorem 1, $\rho_s$ is not even measurable with respect to the $\sigma$-algebra of the conditional expectation. So $E(\rho_s\xi^s\mid B_s)\ne\rho_sE(\xi^s\mid B_s)$, and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither $\sum\rho_s=\infty$ nor $\rho_s\to0$ is given, and both must be derived path by path.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Sequences are indexed from $0$. Chapter 17 is shifted by one against the page: its $X_n,\xi_n,\mathcal F_n$, $n\ge1$, become indices $n-1$. Conditional expectations are Mathlib's condExp with respect to the history $\sigma$-algebras of the definition file. Every $\limsup$ bound is written out as "for every $\varepsilon>0$, eventually $\dots\le\dots+\varepsilon$", or in (18.17) as a bound $L$ with $C_2L<\delta$. Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.

Readings of the page, each recorded in the item's Formalization Note:

• (18.17) prints $C_1$. The proof's estimate gives $(C_2C_s-\delta)\rho_s$, and only $C_2$ is invariant under rescaling of $\mathbb R^n$, so $C_2$ is stated.
• (18.5) has two forms that agree only without projection. The proof uses the second, $a^{\langle\xi^{s+1},x^s-x^{s+1}\rangle-\delta\rho_s}$, which is stated.
• (18.8) prints $F_s(x^s)$ for $F_x(x^s)$. (18.11) prints $E\rho_s^s$, read as $E\rho_s^2<\infty$.
• Theorem 2's "$F(x^s)-\min z\in XF(x)\to0$" is read as $F(\bar x^s)-\min_XF\to0$.
• The end of step 2 prints $\rho_{s+1}/\rho_s\to0$, read as $\to1$.
• Chapter 17, assumption (ii) prints $\|\nabla f(x)\|\le A+B\|x-x^*\|^2$. The proof uses $\|\nabla f(x)\|^2$, and the printed form makes part (i) false, so the squared form is stated. $\mathrm{Var}(Y_x)\le C$ is read as $E\|Y_x-EY_x\|^2\le C$.
• The Corollary adds lower semicontinuity of $F$ on $X$, without which it fails.
• $x^0\in X$ is assumed, and $\rho_0$ in Theorem 2 is a fixed positive number.

No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.

A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the $\delta$ of (18.17) is the $\delta$ of the rule.

Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.

Selected references

• G. Ch. Pflug, Stepsize Rules, Stopping Times and their Implementation in Stochastic Quasigradient Algorithms, in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer 1988, Ch. 17. https://doi.org/10.1007/978-3-642-61370-8
• S. Uryasev, Adaptive Stochastic Quasigradient Procedures, ibid., Ch. 18. https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, Stochastic Quasigradient Methods, ibid., Ch. 6. https://doi.org/10.1007/978-3-642-61370-8
• F. Mirzoakhmedov and S. P. Uryasev, Adaptive step size control for stochastic optimization algorithm, Zh. Vychisl. Mat. i Mat. Fiz. 23(6) (1983) 1314–1325 (in Russian); cited in the volume above, no online copy linked.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• B. T. Polyak and A. B. Juditsky, Acceleration of Stochastic Approximation by Averaging, SIAM J. Control Optim. 30 (1992) 838–855. https://doi.org/10.1137/0330046

Motivation

Decisions under uncertainty are often required to satisfy a constraint $\theta \in \Theta_\delta$ that depends on a random parameter $\delta$, and requiring it for every possible $\delta$ is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of $\delta$ by $N$ independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.

Enforcing all $N$ sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards $k$ of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.

Setting

A decision $\theta$ ranges over $\mathbb R^d$ (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain $\Theta$ and a linear cost $c^{\mathsf T}\theta$. An uncertain parameter $\delta$ takes values in a measurable space $\Delta$ with probability $\mathbb P$, and each $\delta$ determines a closed convex constraint set $\Theta_\delta$. The violation probability of a decision is

$$V(\theta) = \mathbb P\{\delta \in \Delta : \theta \notin \Theta_\delta\}.$$

Given independent samples $\delta_1,\dots,\delta_N$ with joint law $\mathbb P^N$, the scenario program minimizes $c^{\mathsf T}\theta$ over $\theta \in \Theta \cap \bigcap_{i=1}^N \Theta_{\delta_i}$. For a set $I$ of indexes, the program without the constraints in $I$ minimizes the same cost over $\Theta \cap \bigcap_{i \notin I} \Theta_{\delta_i}$; its solution is written $\theta^*_I$. A removal procedure selects, as a function of the whole sample, a set of $k$ indexes, and $\theta^*_k$ denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the $k$ removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that $\Theta$ and every $\Theta_\delta$ are convex and closed, and Assumption 3.6, that for every sample size $m$ and every sample the scenario program has exactly one solution.

Formalization targets

Goal: Theorem 3.9

For $N \ge d$, under Assumptions 3.4 and 3.6, for every removal procedure and every $\varepsilon \in [0,1]$,

$$\mathbb P^N\{V(\theta^*_k) > \varepsilon\} \le \binom{k+d-1}{k} \sum_{i=0}^{k+d-1} \binom Ni \varepsilon^i (1-\varepsilon)^{N-i}.$$

The bound depends on the problem only through $d$, and on the removal procedure not at all. For $k = 0$ it is Theorem 3.7.

Milestones

1. Theorem 3.7 (no removal): $\mathbb P^N\{V(\theta^*) > \varepsilon\} \le \sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$, used for the program with the $N-k$ kept constraints.
2. Eq. (5.11): up to a zero probability set, the event $\{V(\theta^*_k) > \varepsilon\}$ is contained in the union over all $k$-element index sets $I$ of the events "$\theta^*_I$ violates all constraints in $I$ and $V(\theta^*_I) > \varepsilon$".
3. Eq. (5.13): for a fixed $I$, the probability of that event equals $\int_{(\varepsilon,1]} \alpha^k F_V(d\alpha)$, where $F_V$ is the law of $V(\theta^*_I)$.
4. Eq. (5.14) and Theorem 3.9 for $d = 2$: the book's complete proof in the plane.
5. Eqs. (3.15)–(3.17) and the conclusion of Section 3.3.1: with the explicit level $\varepsilon_k$ of (1.9), the right-hand side of (3.13) is at most $\beta$.
6. Theorem 1.2: with probability at least $1-\beta$, $V(\theta^*_k) \le \varepsilon_k$, where

$$\varepsilon_k = \frac{k}{N} + \left[\frac{\sqrt k}{N} + \frac{\sqrt k+1}{N}\left((d-1)\ln(k+d-1) + \frac{d-1}{\sqrt k} + \ln\frac1\beta\right)\right].$$

Significance

Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of $k$ before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when $k/N$ is held fixed, the violation exceeds the empirical risk $k/N$ by a margin of order $\ln N/\sqrt N$, only slightly worse than the $1/\sqrt N$ rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).

Theorem 3.9 is proved in the literature for general $d$ (Campi and Garatti, 2011); the textbook proves it for $d = 2$. To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.

Difficulty

The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to $\theta^*_k$ directly. The argument must pass through all $\binom Nk$ fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor $\binom Nk$ and does not give (3.13). For a fixed index set, the probability that the $k$ removed scenarios are all violated involves the distribution of $V(\theta^*_I)$, which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function $\alpha \mapsto \alpha^k$ is needed. In general dimension the combinatorial constant $\binom{k+d-1}{k}$ comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin d), samples of size $m$ are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:

• $d \ge 1$, $d \le N$, $k \le N$ and $\varepsilon \in [0,1]$;
• Assumption 3.6 for every $m$, including $m = 0$, and for every sample (not almost every);
• the removed constraints are violated with probability one (∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for $1 \le k < N$ (on a sample with all $\delta_i$ equal a kept constraint coincides with a removed one) and would make the results vacuous;
• measurability, which the book glosses over (p. 33): the constraint relation $\{(\theta,\delta) : \theta \in \Theta_\delta\}$ is jointly measurable, the solution map of the scenario program with $m$ constraints is measurable for every $m$, and $\theta^*_k$ is measurable;
• for Theorem 1.2 and Section 3.3.1: $k \ge 1$ (formula (1.9) divides by $\sqrt k$), $N \ge 1$, $\beta \in (0,1)$; Section 3.3.1 additionally assumes $\varepsilon_k \le 1$, the range in which its chain of inequalities holds.

Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for $d = 2$ only, as in the book.

A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict $V(\theta^*_k) > \varepsilon$; a statement for one fixed rule, or with $\theta^*_k$ unconstrained, would be a different theorem.

A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size $N-k$, the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general-$d$ counting argument of the cited paper, are welcome.

Selected references

• M. C. Campi and S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi and S. Garatti, A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality, Journal of Optimization Theory and Applications 148(2), 257–280, 2011. https://doi.org/10.1007/s10957-010-9754-6
• M. C. Campi and S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 1211–1230, 2008. https://doi.org/10.1137/07069821X
• G. C. Calafiore and M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

Motivation

The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample $N$ instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in $N$ and in the number $d$ of optimization variables. To reach a failure level $\varepsilon$ with confidence $1-\beta$, the number of scenarios grows roughly like $\frac{2}{\varepsilon}\big(\ln\frac1\beta+d-1\big)$ (Theorem 1.1 of the book). The product of $d$ and $1/\varepsilon$ is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.

FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number $N_1$ of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers $N_2$ further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.

Timeline:

• 2006, Calafiore and Campi: violation bounds for the solution of convex scenario programs.
• 2008, Campi and Garatti: the exact binomial bound, tight for fully supported problems (Theorem 3.7 of the book).
• 2014, Carè, Garatti and Campi: FAST and its two-stage bound, Eq. (8.5).
• 2018, Campi and Garatti's textbook, §8.3, the source of this mission.

Setting

Let $\Delta$ be a measurable space carrying a probability measure $\mathbb P$, and let $\ell(\nu,\delta)$ be a real loss of a decision $\nu\in\mathbb R^{d-1}$ under the uncertain parameter $\delta\in\Delta$. As a standing assumption of the book, $\ell(\cdot,\delta)$ is convex for every $\delta$.

Given scenarios $\delta_1,\dots,\delta_m$ drawn independently from $\mathbb P$, the scenario program (1.4) is

$$\min_{\nu\in\mathbb R^{d-1}}\ \Big[\max_{i=1,\dots,m}\ \ell(\nu,\delta_i)\Big].$$

Its solution is $\nu^*$ and its optimal value $\ell^*$. Assumption 3.6 requires that for every $m$ and every sample the solution exist and be unique. The pair $(\nu,\ell)$ has $d$ components, and $d$ is the number that enters every bound.

The risk (Definition 8.2) of a decision $\nu$ with cost level $\ell$ is

$$R(\nu,\ell)=\mathbb P\{\delta\in\Delta:\ \ell(\nu,\delta)>\ell\},$$

the probability that a new instance costs more than promised. It is the violation $V(\nu,\ell)$ of the epigraphic constraint $\ell\ge\ell(\nu,\delta)$.

FAST takes $N_1+N_2$ independent scenarios. It solves (1.4) with the first $N_1$ of them, obtaining $\nu^*_{N_1}$. In the detuning step it then sets

$$\ell^*_F=\max_{i=1,\dots,N_1+N_2}\ \ell(\nu^*_{N_1},\delta_i),$$

the smallest level that covers every scenario seen. The output is $(\nu^*_F,\ell^*_F)$ with $\nu^*_F=\nu^*_{N_1}$.

Formalization targets

Goal: Theorem 8.5, Eq. (8.5)

For every $\varepsilon\in[0,1]$,

$$\mathbb P^{N_1+N_2}\{V(\nu^*_F,\ell^*_F)>\varepsilon\}\ \le\ (1-\varepsilon)^{N_2}\sum_{i=0}^{d-1}\binom{N_1}{i}\varepsilon^i(1-\varepsilon)^{N_1-i}.$$

No relation between $N_1$ and $d$ is required. When $N_1<d$ the sum equals $1$ and the bound reads $(1-\varepsilon)^{N_2}$.

Milestone: Theorem 3.7 for program (1.4)

The first stage is an ordinary scenario program with $N_1$ scenarios. For $N\ge d$,

$$\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\ \le\ \sum_{i=0}^{d-1}\binom{N}{i}\varepsilon^i(1-\varepsilon)^{N-i},$$

that is, $R(\nu^*,\ell^*)$ is dominated by a $B(d,N-d+1)$ distribution (recalled on p. 90).

Milestone: the $N_2$ rule

For $\varepsilon,\beta\in(0,1)$, $N_2\ge\frac1\varepsilon\ln\frac1\beta$ makes the right-hand side of (8.5) at most $\beta$ (p. 95).

Significance

The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With $N_1=Kd$ (the book suggests $K\approx20$) and $N_2\ge\frac1\varepsilon\ln\frac1\beta$, the total number of scenarios is $Kd+\frac1\varepsilon\ln\frac1\beta$. This is additive in $d$ and $1/\varepsilon$ rather than multiplicative, and the added $N_2$ scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: $\ell^*_F$ is in general higher than the value a classical scenario program with the same confidence would return.

Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The $N_2$ rule is an elementary but explicit sample-size certificate.

Difficulty

The obvious route treats the detuning step as a fresh scenario program with $N_1+N_2$ scenarios and applies Theorem 3.7 to it. That fails: $\nu^*_F$ is not the solution of that program, and Theorem 3.7 with $N_1+N_2$ scenarios gives a bound that is not of the product form (8.5). The level $\ell^*_F$ depends on all $N_1+N_2$ scenarios at once, including those that determined $\nu^*_{N_1}$, and the map $c\mapsto R(\nu,c)$ is monotone but need not be continuous, so the event $V(\nu^*_F,\ell^*_F)>\varepsilon$ is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.

Formalization scope

Lean representation:

• The decision space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin n); the book's $d$ is written $n+1$, never with natural-number subtraction.
• A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same $\mathbb P$ defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.
• The maximum in (1.4) and in $\ell^*_F$ is Finset.sup' over a nonempty index set. $\ell^*_F$ runs over all $N_1+N_2$ scenarios, not over the $N_2$ new ones only.
• The risk is (P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event $V>\varepsilon$ of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.
• The first-stage solution is a map νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.

Hypotheses the book leaves implicit, stated explicitly:

1. $\ell(\cdot,\delta)$ is convex for every $\delta$ (standing assumption, p. 6).
2. Existence and uniqueness of the solution (Assumption 3.6) for every $m\ge1$ and every sample. The program with no scenario has no minimum, so $m=0$ is excluded.
3. $N_1\ge1$, since the first stage needs a scenario.
4. $\varepsilon\in[0,1]$; for $\varepsilon>1$ the factor $(1-\varepsilon)^{N_2}$ can be negative.
5. The loss is jointly measurable in $(\nu,\delta)$ and the first-stage solution map is measurable. The book glosses over measurability (p. 6, footnote 1; p. 33).

A formalization that bounds only the $N_2$ new scenarios is ruled out, because $\ell^*_F$ is defined as a maximum over all $N_1+N_2$ scenarios. So is one that takes $\ell^*_F$ as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.

A complete development needs the scenario program in loss form, product-measure conditioning on $\Delta^{N_1}\times\Delta^{N_2}$, and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018, §8.3 and Theorem 3.7. https://doi.org/10.1137/1.9781611975444
• A. Carè, S. Garatti, M. C. Campi, FAST—Fast Algorithm for the Scenario Technique, Operations Research 62(3):662–671, 2014. https://doi.org/10.1287/opre.2014.1257
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3):1211–1230, 2008. https://doi.org/10.1137/07069821X
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5):742–753, 2006. https://doi.org/10.1109/TAC.2006.875041