Convex Optimization

Motivation

The subgradient method for a nonsmooth convex function converges, but slowly: when the level sets of the objective are elongated, the subgradient is nearly orthogonal to the direction towards the minimum, and the method zigzags. For smooth functions the remedy is a change of metric (Newton and quasi-Newton methods); for nonsmooth functions no Hessian exists to supply one. N. Z. Shor's answer was to learn a metric from the subgradients themselves: after each step, stretch the space along the latest (transformed) subgradient, so that components of future subgradients parallel to it are damped. These subgradient methods with space dilation along the gradient (SDG methods) are the ancestors of Shor's r-algorithm and of the ellipsoid method, which the book (p. 49) describes as a special case of the same family and which Khachiyan later used to show that linear programming is solvable in polynomial time.

Section 3.4 of Shor's monograph (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński, doi:10.1007/978-3-642-82118-9) proves that, under a two-sided condition on the objective, a suitable SDG method decreases function values at the speed of a geometric progression whose ratio is invariant under nonsingular linear changes of variables. This mission formalizes that chain of results.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x,y)$. For a unit vector $\xi$ and a coefficient $\alpha \ge 0$, the operator of space dilation along $\xi$ is

$$R_\alpha(\xi)\,x = x + (\alpha - 1)(x,\xi)\,\xi ,$$

which multiplies the component of $x$ along $\xi$ by $\alpha$ and leaves the orthogonal complement fixed.

Let $f : E_n \to \mathbb{R}$ and let $g : E_n \to E_n$ be a generalized gradient: a subgradient of $f$ when $f$ is convex, an almost-gradient when $f$ is almost differentiable. The SDG method starts from $x_0$ and a nonsingular operator $B_0 = A_0^{-1}$. At step $k = 0, 1, \dots$: if $g(x_k) = 0$ it stops; otherwise it forms the transformed gradient $\tilde g_k = B_k^* g(x_k)$, the direction $\xi_{k+1} = \tilde g_k/\|\tilde g_k\|$, and

$$x_{k+1} = x_k - h_{k+1} B_k \xi_{k+1}, \qquad B_{k+1} = B_k R_{1/\alpha_{k+1}}(\xi_{k+1}), \qquad A_{k+1} = R_{\alpha_{k+1}}(\xi_{k+1}) A_k ,$$

with a stepsize $h_{k+1}$ and a dilation coefficient $\alpha_{k+1}$. So $A_k$ is the accumulated space transformation, $B_k = A_k^{-1}$, and each step is a subgradient step for $\varphi_k(y) = f(B_k y)$ in the variables $y = A_k x$.

The quantitative results assume, for a point $x^*$ and the ball $S_d = \{x : \|x - x^*\| \le d\}$, the two-sided condition

$$N\,[f(x) - f(x^*)] \le (g(x),\, x - x^*) \le M\,[f(x) - f(x^*)], \qquad x \in S_d, \quad M > N > 0. \qquad (3.18)$$

For a convex function the lower inequality holds with $N = 1$; the upper one bounds how far $f$ is from a positively homogeneous function around $x^*$.

Formalization targets

Goal: Theorem 3.4

Under (3.18), with $B_0 = I$, $x_0 \in S_d$, stepsizes $h_{k+1} = \frac{2MN}{M+N}\frac{f(x_k)-f(x^*)}{\|\tilde g_k\|}$, a constant coefficient $1 < \alpha \le \frac{M+N}{M-N}$, and $G$ a bound for $\|g\|$ on $S_d$: there are $c > 0$ and indices $k_1 < k_2 < \cdots$ with

$$f(x_{k_p}) - f(x^*) \le c\,\alpha^{-k_p/n},$$

and for every $k \ge 1$

$$\min_{0 \le i \le k-1}\,[f(x_i) - f(x^*)] \le \frac{G\sqrt{k(\alpha^2-1)}\,d}{N\sqrt{\alpha^{2k/n}-1}} .$$

Milestones

1. Eq. (3.4): $\|R_\alpha(\xi)x\| = \sqrt{\|x\|^2 + (\alpha^2-1)(x,\xi)^2}$.
2. Theorem 3.1: if $\|g(x_k)\| \le d$ and $1+\delta \le \alpha_k \le \alpha^*$, then $\|\tilde g_{k_p}\| < c\,(\prod_{j\le k_p}\alpha_j)^{-1/n}$ along a subsequence.
3. Theorem 3.2: for constant $\alpha > 1$ and $B_0 = I$, $\min_{0\le r\le k-1}\|\tilde g_r\| \le d\sqrt{k(\alpha^2-1)}/\sqrt{\alpha^{2k/n}-1}$.
4. Theorem 3.3: under (3.18) and the rules above, $\|A_k(x_k - x^*)\| \le d$ for all $k$.

Significance

The result shows that one fixed rule, depending only on $M$, $N$ and $n$, yields linear convergence of function values for every objective satisfying (3.18), at a ratio $\alpha^{-1/n}$ that does not deteriorate when the problem is badly scaled: the method, and hence its rate, is invariant under nonsingular linear changes of variables. This is the property the ellipsoid method inherits (Section 3.8 of the book), and the same space-dilation machinery drives the r-algorithm (Section 3.7), still used for large nonsmooth problems such as Lagrangian duals of integer programs.

The theorems are proved in the book; none of them, and no space-dilation method, has a machine-checked proof to our knowledge, and the platform has no statement about variable-metric subgradient methods. The mission provides a reusable formal model of the SDG iteration, the eigenvalue-growth arguments behind Theorems 3.1–3.2, and the one-step invariant of Theorem 3.3. The formalization also corrects two points of the printed text (see Formalization scope).

Difficulty

Theorem 3.3 is a one-step computation, but Theorems 3.1 and 3.2 are not: they relate the size of the transformed gradients to the growth of the singular values of $A_k$, whose determinant is $\prod_j \alpha_j$. A bound on $\|\tilde g_k\|$ at a single step says nothing, since the dilations can concentrate in few directions; the argument has to control the largest singular value of $A_k$ over many steps against the geometric-mean lower bound $(\det A_k)^{1/n}$. The dimension $n$ enters the rate exactly through this comparison. Theorem 3.4 then needs the invariant of Theorem 3.3 to keep every iterate inside $S_d$, where (3.18) and the bound $G$ are available.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ in the rate statements. Operators are continuous linear maps; $B_0$ is a continuous linear equivalence and $A_0$ its inverse. The state $(x_k, B_k, A_k)$ is produced by a defined recursion sdg, not assumed; $\tilde g_k$ is gTilde.
• The stepsize rule receives the index, the current point and $\tilde g_k$; the dilation coefficient at step $k$ is α (k+1). When $g(x_k) = 0$ the state is repeated, which encodes the book's stop; no division by zero is used.
• The book states Theorems 3.1–3.4 for almost differentiable $f$ with $g$ an almost-gradient; the proofs use only the bounds on $\|g\|$ and (3.18), so the Lean statements quantify over every map $g$ with those properties. $G$ is any bound for $\|g\|$ on $S_d$ in place of the maximum.
• Theorems 3.2–3.4 take $B_0 = I$, as their proofs do; Theorem 3.1 allows any nonsingular $B_0$.
• Two corrections to the printed statements, both following the proofs: Theorem 3.4's record bound carries the factor $1/N$ that the proof derives, and the record minima in Theorems 3.2 and 3.4 range over the indices $0, \dots, k-1$ that the proof controls, rather than $1, \dots, k$.
• Constants $c$ and subsequences are existential and chosen after the data of the run, before the index $p$. A statement placing $c$ after $p$, or dropping (3.18) on $S_d$, would be trivially true or false and is ruled out.

Useful infrastructure, reusable for the r-algorithm and ellipsoid chapters: identities for $R_\alpha(\xi)$, determinants and singular values of products of rank-one dilations, and the invariance of the SDG iteration under a linear change of variables. Proofs of any milestone, and alternative arguments for Theorem 3.1, are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§3.2–3.4, pp. 49–62 (translated by K. C. Kiwiel and A. Ruszczyński). https://doi.org/10.1007/978-3-642-82118-9

Motivation

Many optimization problems in operations research have objectives that are convex but not differentiable: the maximum of finitely many linear or smooth functions, the value function of a Lagrangian dual, the cost of a two-stage linear program as a function of the first-stage decision. Gradient methods do not apply to these directly. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer Series in Computational Mathematics 3, 1985; translated by K. C. Kiwiel and A. Ruszczyński from the 1979 Russian edition) develops the algorithms that replace the gradient by a subgradient, and its first chapter sets up the calculus of subgradients these algorithms rely on.

This mission is the first of a series formalizing the book. It covers §1.2 (convex functions and the concept of subgradient) and §1.3 (rules for computing subgradients), printed pages 7–16. Every later mission in the series (the subgradient method, space dilation, the ellipsoid method, decomposition) assumes that a subgradient of the objective can be computed, and §1.3 is where the book explains how: by combining subgradients of simpler pieces.

Setting

Write $E_n$ for $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. A function $f$ with domain a convex set $M \subseteq E_n$ is convex if its epigraph $\{(u, x) : u \ge f(x),\ x \in M\}$ is convex, equivalently $(1-\alpha) f(x_1) + \alpha f(x_2) \ge f((1-\alpha)x_1 + \alpha x_2)$ for $x_1, x_2 \in M$ and $\alpha \in [0,1]$.

Let $x_0$ be an interior point of $M$. A vector $g$ is a subgradient (or generalized gradient) of $f$ at $x_0$ if

$$f(x) - f(x_0) \ge (g, x - x_0) \qquad \text{for all } x \in M. \tag{1.3}$$

The set of all subgradients is the subdifferential, written $G(x_0)$ or $G_f(x_0)$. For $f$ differentiable at $x_0$ it is the single gradient; for $f(x) = |x|$ on $E_1$ it is $[-1, 1]$ at $x_0 = 0$.

The one-sided directional derivative of $f$ at $x_0$ in direction $\eta$ is

$$f'_\eta(x_0) = \lim_{t \to 0+} \frac{f(x_0 + t\eta) - f(x_0)}{t}.$$

A direction $\eta \ne 0$ is a direction of steepest descent at $x_0$ if $\min_{\|\xi\| = 1} f'_\xi(x_0) = f'_\eta(x_0)/\|\eta\|$.

Formalization targets

Goal: Theorem 1.12 (p. 13), the subdifferential of a nonnegative combination

For convex $f_1, \dots, f_k$ on $E_n$ and $a_1, \dots, a_k \ge 0$, the function $f = \sum_{i=1}^k a_i f_i$ is convex and, at every $x_0$,

$$G_f(x_0) = \Big\{ \sum_{i=1}^k a_i g_i \;:\; g_i \in G_{f_i}(x_0),\ i = 1, \dots, k \Big\}.$$

Both inclusions are part of the goal.

Milestones

1. Theorem 1.7 (p. 9): at an interior point $x_0$ of the domain, $G(x_0)$ is nonempty, bounded, convex and closed.
2. Theorem 1.8 (p. 9): at an interior point, $f'_\eta(x_0)$ exists for every $\eta$ and $f'_\eta(x_0) = \max_{g \in G(x_0)} (g, \eta)$, with the maximum attained.
3. Corollary (p. 12): an interior point $x_0$ minimizes $f$ on $M$ if and only if $0 \in G(x_0)$.
4. Theorem 1.11 (p. 12): if $0 \notin G(x_0)$ and $g_0$ is the element of $G(x_0)$ nearest the origin, then $-g_0$ is a direction of steepest descent.
5. Theorem 1.9 (p. 11): $f$ is convex on $E_n$ if and only if $f'_\eta(x)$ exists everywhere and $t \mapsto f'_\eta(x + t\eta)$ is nondecreasing for all $x, \eta$.
6. Theorem 1.10 (p. 11): a twice continuously differentiable $f$ is convex if and only if its Hessian is positive semidefinite everywhere.
7. Theorem 1.13 (p. 14): for convex $f_1, \dots, f_m$, the function $\varphi = \max_i f_i$ is convex and $G_{f_i}(x_0) \subseteq G_\varphi(x_0)$ for every index $i$ active at $x_0$.

Significance

The result. Theorem 1.12 is the finite-dimensional, finite-valued case of the Moreau–Rockafellar sum rule. With Theorem 1.13 it is the book's recipe for computing subgradients of functions assembled from simple pieces by nonnegative combinations and pointwise maxima, the two operations that produce most nonsmooth convex objectives in practice (Lagrangian duals, penalty functions, piecewise-linear costs). Theorem 1.8 identifies the directional derivative with the support function of the subdifferential; the Corollary and Theorem 1.11 give the optimality condition and the steepest-descent direction that every descent method for nonsmooth convex functions starts from.

Formalizing it. These results are classical and have been proved many times in textbooks (Rockafellar, Convex Analysis, 1970, §23). Mathlib at the pinned revision has convexity, separation theorems and Carathéodory's theorem, but no subdifferential of a convex function on $E_n$ and no max formula. The mission builds that layer: a subdifferential with the book's inequality (1.3), a one-sided directional derivative defined as a right-hand limit, and the calculus rules above. The platform has a Clarke-gradient analogue of Theorem 1.8 for locally Lipschitz functions and a Banach-space sum rule for $f + \tfrac12\|\cdot\|^2$; neither states the convex, finite-dimensional results here.

Difficulty

The inclusion "$\supseteq$" in Theorem 1.12 is immediate from (1.3). The inclusion "$\subseteq$" is the content: a subgradient of the sum is a global object, and nothing in (1.3) splits it into subgradients of the pieces. Adding the inequalities of the pieces only produces vectors of the right form; it does not show every subgradient of $f$ arises this way. Any argument has to use the finite dimension and the interior-point setting, which is where Theorems 1.7 and 1.8 (existence of subgradients, compactness of $G(x_0)$, existence of one-sided derivatives) come in.

Theorem 1.8 in turn needs the existence of a finite right-hand limit of the difference quotient, which requires both monotonicity of the quotient and a lower bound, and the existence of a subgradient attaining the maximum, which is a separation statement. Theorem 1.9's "if" direction must rebuild convexity from one-sided derivative information alone, with no differentiability assumption.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) and $(x, y)$ is inner ℝ x y. A function is f : EuclideanSpace ℝ (Fin n) → ℝ; the domain $M$ is a set, convexity on it is ConvexOn ℝ M f (which includes convexity of $M$), and interior points are x₀ ∈ interior M. Theorems 1.9, 1.10, 1.12 and 1.13 are stated on all of $E_n$ (Set.univ), as the book proves them.
• The subdifferential subdifferential M f x₀ is the set of $g$ with $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x \in M$. It is defined for any $x_0$; the interior-point assumption is a hypothesis of each theorem that needs it.
• HasOneSidedDirDeriv f x₀ η d is the right-hand limit Tendsto … (𝓝[>] 0) (𝓝 d), not Mathlib's two-sided lineDeriv. Maxima and minima are stated with IsGreatest/IsLeast (attained), never with sSup/sInf.
• Theorem 1.12 is an equality of sets over indices Fin k; $k = 0$ and zero coefficients are allowed, as in the book. Theorem 1.13's maximum is Finset.sup' over Fin m with $m \ge 1$, and it asserts only the inclusion the book states.
• Theorem 1.11 is stated as the book's proof establishes it: the steepest-descent direction is minus the minimal-norm subgradient. The printed statement names the minimal-norm subgradient itself, along which the directional derivative is positive.
• A formalization that states only "$\supseteq$" in Theorem 1.12, or only that each $\sum a_i g_i$ is a subgradient, is the easy half and does not count as the goal.
• Theorems 1.1–1.6 (supporting hyperplane, separation, representation by extremal points, the convexity inequality, continuity on the interior) are Mathlib-level (geometric_hahn_banach_*, Carathéodory and Krein–Milman, ConvexOn.continuousOn_interior) and are not restated.

Contributions welcome: proofs of any milestone, a reusable lemma that the difference quotient of a convex function is monotone in $t$, and a general max formula; these are reusable in the later missions of the series, which define subgradients the same way.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§1.2–1.3, pp. 7–16. https://doi.org/10.1007/978-3-642-82118-9
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §23 (subgradients) and Theorem 23.8 (sum rule). https://doi.org/10.1515/9781400873173
• J.-J. Moreau, "Fonctionnelles sous-différentiables", Comptes Rendus de l'Académie des Sciences 257 (1963), 4117–4119.

Motivation

A zero-sum two-person game in normalized form is a real matrix $\mathcal H(\tau_1, \tau_2)$: player 1 chooses a row $\tau_1$, player 2 simultaneously chooses a column $\tau_2$, and player 2 pays player 1 the amount $\mathcal H(\tau_1, \tau_2)$. Matrix games are the base case of non-cooperative game theory, the prototype of every minimax statement in optimization, statistics (Wald's decision theory) and online learning, and, through their equivalence with linear programming, a standard tool of operations research.

Chapter III of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; third edition 1953) gives the book's complete solution of these games. Timeline:

• 1928. J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Math. Annalen 100, proves that every matrix game has a value in mixed strategies (the minimax theorem), by a topological argument. https://doi.org/10.1007/BF01448847
• 1937. von Neumann's growth-model paper gives a second proof via a fixed-point argument, later generalized by Kakutani (1941).
• 1938. J. Ville gives the first elementary proof, based on convexity.
• 1944. The Theory of Games presents Ville's route: a theorem of the alternative for matrices (§16) yields the minimax theorem (17:6), from which §17 derives the structure of the sets of good strategies.
• 1951. Gale, Kuhn and Tucker, and Dantzig, relate matrix games to linear-programming duality.

Setting

Player 1 has $\beta_1 \ge 1$ pure strategies $\tau_1$, player 2 has $\beta_2 \ge 1$ pure strategies $\tau_2$, and $\mathcal H$ is an arbitrary real $\beta_1 \times \beta_2$ matrix (14.1.1). A mixed strategy of player 1 is a probability vector $\xi$ in the simplex

$$S_{\beta_1} = \Big\{ \xi \in \mathbb R^{\beta_1} : \xi_{\tau_1} \ge 0,\ \sum_{\tau_1} \xi_{\tau_1} = 1 \Big\},$$

and similarly $\eta \in S_{\beta_2}$ for player 2. The pure strategy $\tau$ is the coordinate vector $\delta^{\tau}$. The expected payoff is the bilinear form (17:2)

$$K(\xi, \eta) = \sum_{\tau_1=1}^{\beta_1} \sum_{\tau_2=1}^{\beta_2} \mathcal H(\tau_1, \tau_2)\, \xi_{\tau_1} \eta_{\tau_2}.$$

The good strategies of player 1 form the set $\bar A$ of those $\xi \in S_{\beta_1}$ at which $\operatorname{Min}_\eta K(\xi, \eta)$ assumes its maximum; those of player 2 form the set $\bar B$ of those $\eta \in S_{\beta_2}$ at which $\operatorname{Max}_\xi K(\xi, \eta)$ assumes its minimum ((17:B:a), (17:B:b)). A saddle point of $K$ is a pair with $K(\xi', \eta) \le K(\xi, \eta) \le K(\xi, \eta')$ for all $\xi', \eta'$. With pure strategies alone one has $v_1 = \operatorname{Max}_{\tau_1}\operatorname{Min}_{\tau_2}\mathcal H$ and $v_2 = \operatorname{Min}_{\tau_2}\operatorname{Max}_{\tau_1}\mathcal H$; the game is specially strictly determined when $v_1 = v_2$.

For a general real function $\phi(x, y)$ (§13) the same notions are $\operatorname{Max}_x \operatorname{Min}_y \phi$, $\operatorname{Min}_y \operatorname{Max}_x \phi$, saddle points, and the sets $A^\phi$ (maximizers of $\operatorname{Min}_y \phi$) and $B^\phi$ (minimizers of $\operatorname{Max}_x \phi$), always under the book's standing hypothesis that these maxima and minima exist.

Formalization targets

Goal: (17:D), good strategies characterized by their supports

For all $\xi \in S_{\beta_1}$ and $\eta \in S_{\beta_2}$: $\xi \in \bar A$ and $\eta \in \bar B$ if and only if

$$\xi_{\tau_1} = 0 \text{ whenever } \sum_{\tau_2} \mathcal H(\tau_1, \tau_2)\eta_{\tau_2} < \max_{\tau_1'} \sum_{\tau_2} \mathcal H(\tau_1', \tau_2)\eta_{\tau_2},$$ $$\eta_{\tau_2} = 0 \text{ whenever } \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1} > \min_{\tau_2'} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2')\xi_{\tau_1}.$$

The statement fixes no value and no constant; it says which pairs of mixed strategies are optimal.

Milestones, in attack order

1. (13:A*) $\operatorname{Max}_x \operatorname{Min}_y \phi \le \operatorname{Min}_y \operatorname{Max}_x \phi$.
2. (13:D*) If $\operatorname{Max}\operatorname{Min} = \operatorname{Min}\operatorname{Max}$, the saddle points of $\phi$ are exactly $A^\phi \times B^\phi$.
3. (17:A) $\operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_{\tau_2} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1}$, and dually for $\operatorname{Max}_\xi$.
4. (16:C) For every matrix $a(i, j)$ exactly one of: some $x \in S_m$ with $\sum_j a(i,j)x_j \le 0$ for all $i$; some $w \in S_n$ with $\sum_i a(i,j)w_i > 0$ for all $j$.
5. (16:F) The weak form with $\ge 0$ in place of $> 0$.
6. (17:6) The minimax theorem: a saddle point of $K$ exists (already on the platform as AGT.zero_sum_minimax, proved).
7. (17:C:f) $\xi \in \bar A$ and $\eta \in \bar B$ iff $\xi, \eta$ is a saddle point of $K$.

After the goal: (17:E) the game is specially strictly determined iff each player has a pure good strategy.

Significance

(17:D) is the complementary-slackness description of the optimal strategy pairs of a matrix game: a good strategy puts weight only on pure strategies that are best replies to the opponent's good strategy, and conversely any pair of mutually supported best replies is optimal. It is the basis of support-enumeration methods for matrix games, of the equalizing arguments used to solve small games by hand (the book's Chapter IV applies it to Matching Pennies, Stone–Paper–Scissors and Poker), and of the rectangular structure $\bar A \times \bar B$ of the set of optimal pairs. (17:E) connects the mixed-strategy solution to the pure-strategy theory of §14 and to the perfect-information games of §15.

The results are classical and proved in the book. The minimax theorem itself is already machine-checked on the platform (AGT.zero_sum_minimax), and Mathlib contains Sion's minimax theorem and the basic saddle-point lemmas for extended-real functions on sets. This mission adds the book's own chain: the §13 saddle-point calculus under its standing attainment hypothesis, the theorems of the alternative (16:C) and (16:F) in the simplex-normalized form the book uses, the reduction (17:A) to pure strategies, and the characterizations (17:C:f), (17:D), (17:E) of good strategies, which are not on the platform in any form.

Difficulty

The "if" direction of (17:D) cannot be proved from the support conditions alone by local reasoning: that a pair of mutual best replies consists of good strategies uses that the value $\operatorname{Max}_\xi \operatorname{Min}_\eta K$ equals $\operatorname{Min}_\eta \operatorname{Max}_\xi K$, i.e. the minimax theorem. Without that equality the "if" direction of (13:D*) fails (points of $A^\phi \times B^\phi$ exist but are not saddle points), so the calculus of §13 alone does not suffice. Likewise (16:C) is not a direct instance of the Farkas lemma forms on the platform: its alternatives are normalized to the simplex and the second one is strict, and both the existence and the mutual exclusion must be shown.

Formalization scope

Lean conventions, fixed throughout:

• Pure strategies are Fin β₁, Fin β₂ (numbered from $0$), the matrix is H : Fin β₁ → Fin β₂ → ℝ, and $S_\beta$ is Mathlib's stdSimplex ℝ (Fin β).
• Nonempty strategy sets ($\beta \ge 1$, from "τ = 1, …, β" in 14.1.1): every theorem assumes 0 < β₁, 0 < β₂, or mixed strategies $\xi \in S_{\beta_1}$, $\eta \in S_{\beta_2}$, which force it. The theorems of the alternative assume $n, m \ge 1$ (a matrix with rows and columns).
• Standing hypothesis of 13.2.1 ("we are restricting our considerations to such functions, for which Max and Min exist"): the §13 results (13:A*), (13:D*) are stated for an arbitrary $\phi : X \times Y \to \mathbb R$ under the predicate MaxMinAttained φ, which says that $\operatorname{Min}_y \phi(x, y)$, $\operatorname{Max}_x \phi(x, y)$, $\operatorname{Max}_x \operatorname{Min}_y \phi$ and $\operatorname{Min}_y \operatorname{Max}_x \phi$ are attained. (13:D*) also carries the hypothesis of 13.5.2 that saddle points exist, stated as $\operatorname{Max}_x \operatorname{Min}_y \phi = \operatorname{Min}_y \operatorname{Max}_x \phi$.
• $\operatorname{Max}$ and $\operatorname{Min}$ are the real ⨆, ⨅; they are the book's attained values under the hypotheses above (compactness of the simplex and continuity of $K$ for the mixed game). (17:A) asserts attainment explicitly (IsLeast, IsGreatest). "Does not assume its maximum at $\tau_1$" in the goal is written without any Max operator.
• $\bar A$, $\bar B$ are defined as maximizers and minimizers directly from $K$, not through an assumed value $v'$.

A trivializing formalization is ruled out: $\bar A$ and $\bar B$ are not taken as hypotheses or defined through the support conditions, strategy sets cannot be empty, and no Max over an empty or unbounded set occurs.

Contributions welcome: proofs of the milestones, especially (16:C) (from Mathlib's convex separation or from a platform Farkas lemma) and the bridge from AGT.zero_sum_minimax to (17:C:f). The §13 lemmas and the (17:A) reduction are reusable by any mission about matrix games or bilinear saddle points.

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§13, 16, 17. https://doi.org/10.1515/9781400829460
• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
• J. Ville, "Sur la théorie générale des jeux où intervient l'habileté des joueurs", in É. Borel, Traité du calcul des probabilités et de ses applications, IV.2, Gauthier-Villars, 1938, 105–113.
• S. Kakutani, "A generalization of Brouwer's fixed point theorem", Duke Mathematical Journal 8 (1941), 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
• D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.

Motivation

Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least $0.95$, a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least $p$.

The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.

Timeline:

• 1959: Charnes and Cooper, individual chance constraints.
• 1971: Prékopa, logarithmic concave measures with application to stochastic programming (Acta Sci. Math. Szeged 32).
• 1973: Prékopa, logarithmic concave measures and functions (Acta Sci. Math. Szeged 34), containing the marginal theorem: marginals of log-concave functions are log-concave.
• 1970s–1980s: nonlinear programming methods for (5.1) (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) combined with Monte Carlo evaluation of $h_0$; the chapter surveys them.

Setting

Let $\xi$ be a random vector in $\mathbb R^q$ on a probability space $(\Omega, \mathcal F, P)$ and let $g_1, \dots, g_r : \mathbb R^n \times \mathbb R^q \to \mathbb R$. The chapter studies problem (5.1):

$$\min h(x) \quad \text{s.t.} \quad h_0(x) = P\bigl(g_1(x,\xi) \ge 0, \dots, g_r(x,\xi) \ge 0\bigr) \ge p, \quad h_1(x) \ge p_1, \dots, h_m(x) \ge p_m .$$

The function $h_0$ is the probability function (chanceProb in Lean). In the special case $g_i(x,y) = T_i x - y_i$ it equals $F(Tx)$, where $F$ is the joint distribution function of $\xi$.

A function $f \ge 0$ is logarithmically concave on a convex set $S$ if

$$f(\lambda u + (1-\lambda) v) \ge f(u)^{\lambda} f(v)^{1-\lambda}, \qquad u, v \in S,\ 0 < \lambda < 1 .$$

Where $f > 0$ this is concavity of $\log f$; the power form also makes sense where $f = 0$. Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.

Section 5.7 introduces the polynomial distribution (5.19) on the cube $0 < z_j \le 1$:

$$F(z_1, \dots, z_n) = \frac{1}{\sum_{i=1}^{N} c_i z_1^{\alpha_{i1}} \cdots z_n^{\alpha_{in}}}, \qquad c_i > 0,\ \alpha_{ij} \le 0,\ \textstyle\sum_j \alpha_{ij} < 0$$

(polyDistF in Lean).

Formalization targets

Goal: Theorem 5.1

If $g_1, \dots, g_r$ are jointly concave on $\mathbb R^{n+q}$ and $\xi$ has a log-concave density $f$ on $\mathbb R^q$, then

$$h_0 \text{ is logarithmically concave on } \mathbb R^n .$$

Its immediate consequence is that the feasible set $\{x : h_0(x) \ge p\}$ is convex for every $p$.

Milestones

1. Theorem 5.2.1: if $h$ is log-concave on the convex set $H = \{h \ge p\}$, $0 < p < 1$, then $h - p$ is log-concave on $H$. This makes the logarithmic penalty function (5.5) of the SUMT method convex.
2. Theorem 5.2.2: under the standing assumptions of §5.2, every interior point $z$ of the feasible set of (5.1) satisfies $h_i(z) > p_i$, $i = 0, \dots, m$.
3. Theorem 5.7.1 (proved content, (5.21)): for $n = 2$ and oppositely ordered exponents, $\partial^2 F / \partial z_1 \partial z_2 \ge 0$ on $(0,1)^2$.
4. Theorem 5.7.2: the polynomial distribution function is log-concave on $(0,1]^n$.

The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.

Significance

Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.

On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.

Difficulty

The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each $g_i$ separately in $x$ and in $y$ is not enough; joint concavity in $(x, y)$ is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.

For Theorem 5.2.2 the naive argument fails at the index $i = 0$: nothing about $h_0$ is assumed directly, and log-concavity of $h_0$ is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.

Formalization scope

$\mathbb R^n$ and $\mathbb R^q$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs $(x, y)$ in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density $f$" is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with $\xi$ and $f$ measurable and $P$ a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint $i = 0$ of Theorem 5.2.2 is stated separately from $h_1, \dots, h_m$. The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.

No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.

Corrections of the printed text, recorded in each item's Formalization Note:

• Theorem 5.1 states the density condition "for every $x_1, x_2 \in \mathbb R^n$"; the density lives on $\mathbb R^q$ and the condition is imposed there.
• (5.19) prints the first factor as $z_i^{\alpha_{i1}}$ and the domain index as $i = 1, \dots, N$; they are read as $z_1^{\alpha_{i1}}$ and $j = 1, \dots, n$.
• Theorem 5.7.1 prints its ordering hypothesis with transposed indices ($\alpha_{11} \le \alpha_{12} \le \dots \le \alpha_{1n}$); following the proof, it is read as: across the $N$ terms the $z_1$-exponents increase and the $z_2$-exponents decrease.
• Theorem 5.7.1 claims "is a probability distribution function"; the book proves only (5.21), and normalization would need $\sum_i c_i = 1$, which is not assumed. The formal statement is (5.21), the mixed derivative as an iterated deriv.

Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of $h_0$, which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.

Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are welcome.

Selected references

• A. Prékopa, "Numerical Solution of Probabilistic Constrained Programming Problems", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 5, pp. 123–139. https://doi.org/10.1007/978-3-642-61370-8
• A. Prékopa, "Logarithmic concave measures with application to stochastic programming", Acta Sci. Math. (Szeged) 32 (1971), 301–316.
• A. Prékopa, "On logarithmic concave measures and functions", Acta Sci. Math. (Szeged) 34 (1973), 335–343.
• A. Charnes and W. W. Cooper, "Chance-constrained programming", Management Science 6 (1959), 73–79. https://doi.org/10.1287/mnsc.6.1.73
• B. L. Miller and H. M. Wagner, "Chance constrained programming with joint constraints", Operations Research 13 (1965), 930–945. https://doi.org/10.1287/opre.13.6.930
• A. Prékopa, Stochastic Programming, Kluwer 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

In a two-stage stochastic linear program a decision $x$ is taken before random data $\xi$ are observed, and a corrective recourse decision $y$ is taken afterwards at a cost. The objective contains the expectation of an optimal value of a linear program, $\int Q(x,\xi(\omega))\,P(d\omega)$, and for continuous or high-dimensional $\xi$ that integral cannot be evaluated exactly. Practical methods therefore replace $\xi$ by a discrete random vector and control the error by computable lower and upper bounds on the expected recourse cost. Chapter 2 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by P. Kall, A. Ruszczyński and K. Frauendorfer, surveys these bounds as they were used in the codes of the time: Jensen's inequality from below, the Edmundson–Madansky inequality from above, and the special structure of simple recourse, where the expected cost is available in closed form.

Timeline. Jensen's inequality (1906) gives the lower bound for a convex integrand. A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Ann. Math. Statist. 30 (1959), and H. P. Edmundson (RAND report, 1956) gave the upper bound by the two-point law on the endpoints of an interval, and its product version for independent components. Kall and Stoyan (1982), Huang, Ziemba and Ben-Tal (1977), Frauendorfer and Kall (1988) developed partition refinement of both bounds, the scheme this chapter describes; Frauendorfer (1988) extended the upper bound to dependent data on boxes.

Setting

The two-stage problem (2.11) is: minimize $\psi(x)=c^Tx+\int_\Omega Q(x,\xi(\omega))\,P(d\omega)$ subject to $Ax=b$, $x\ge 0$. The recourse cost $Q(x,\xi)$ is the optimal value of the second-stage problem (2.12),

$$Q(x,\xi)=\min\{q^Ty : Wy=h-Tx,\ y\ge 0\},\qquad \xi=(q,h,T),$$

with a deterministic $m_2\times n_2$ matrix $W$ (fixed recourse), and $Q=+\infty$ when (2.12) is infeasible. Throughout the chapter the book assumes complete recourse, $\{Wy:y\ge0\}=\mathbb R^{m_2}$, and dual feasibility: for every realization of $q$ some $u$ satisfies $W^Tu\le q$. Under these assumptions $Q$ is finite. The expected recourse function is $\mathcal Q(x)=\int Q(x,\xi(\omega))\,P(d\omega)$.

The Edmundson–Madansky law of an interval $[a,b]$, $a<b$, with mean $\xi^0$ puts mass $p_1=(b-\xi^0)/(b-a)$ at $a$ and $p_2=(\xi^0-a)/(b-a)$ at $b$ (2.32). For a box $\Xi=\times_{j=1}^m[a_j,b_j]$ and means $\xi^0_j$, the vector $\hat\xi$ with independent components of these two-point laws sits at the vertex $v$ with probability $\prod_j p_j(v_j)$.

Simple recourse is the case $W=[I,-I]$, $q=[q^+,q^-]$ with $q^+_j+q^-_j\ge0$, deterministic $T$ and random $h$ only. With $\chi=Tx$ the recourse cost splits into one-row costs $Q_j(\chi_j,h_j)=q^+_j(h_j-\chi_j)$ if $h_j\ge\chi_j$, and $q^-_j(\chi_j-h_j)$ otherwise.

Formalization targets

Goal: the Edmundson–Madansky bound for independent components (p. 46)

If $\xi$ has independent components $\xi_j\in[a_j,b_j]$ with means $\xi^0_j$, and $\varphi$ is convex on $\Xi=\times_j[a_j,b_j]$, then

$$E\varphi(\xi)\le\sum_{v\in\mathrm{vert}\,\Xi}\Big(\prod_{j=1}^m p_j(v_j)\Big)\varphi(v).$$

The book applies it to $\varphi=Q(x,\cdot)$; the goal is stated for every convex $\varphi$, with the explicit weights of (2.32).

Milestones

1. Properties (b), (d), (e) of p. 40: $Q(x,\cdot)$ is piecewise linear and convex in $(h,T)$; $Q(\cdot,\xi)$ is convex piecewise linear in $x$; the expected recourse function is finite and convex under finite second moments.
2. The Jensen lower bound (2.26)–(2.27) on a partition (a published, proved theorem, reused).
3. The dual-multiplier lower bound (2.30)–(2.31).
4. The one-dimensional Edmundson–Madansky inequality (2.32)–(2.34).
5. For simple recourse: separability (2.46)–(2.49), the closed form (2.51) of $EQ_j$, and the bounds (2.55)–(2.56) from the one-block problem.

Significance

The upper bound is the half of the bounding scheme that is not automatic. Jensen's inequality needs only a mean; an upper bound on the expectation of a convex function needs a bounded support and, in the product form, independence. Together they give a certified interval for the optimal value of a two-stage problem, and repeated partitioning of the support shrinks that interval; this is the basis of the sequential approximation methods of §2.2.4 and of later codes. The dual-multiplier bound and the simple-recourse formulas are the pieces that make those intervals cheap to compute.

The results are classical and proved in the literature cited on the page. The one-dimensional Edmundson–Madansky inequality and the general extreme-point form of the upper bound (a measure on the extreme points reproducing the barycentre) are already formalized on Prove2Me in the Introduction to Stochastic Programming series, as is the partition Jensen bound. The product form for independent components is not: deriving it from the extreme-point form requires constructing the product kernel, which is the content of this mission. The recourse properties (b), (d), (e) for a general distribution with finite second moments, the dual-multiplier bound and the simple-recourse formulas are not formalized anywhere known to this mission.

Difficulty

The obvious argument inducts on the dimension, applying the one-dimensional inequality in one coordinate while the others are held fixed. That step needs the conditional law of the remaining coordinates given the first to be their unconditional law, i.e. independence expressed as a product decomposition of the joint law, and it needs $\varphi$ with one coordinate replaced by an endpoint to remain convex on the lower-dimensional box and integrable. For dependent components the inequality is false with these weights: on $[0,1]^2$ with means $(\tfrac12,\tfrac12)$ and $\varphi(x,y)=(x-y)^2$, the product law gives $\tfrac12$ while mass $\tfrac12$ at $(1,0)$ and at $(0,1)$ gives $1$. The book's remark that the product law is extremal among all laws on $\Xi$ with the given mean fails for this reason when $m\ge2$, and is not part of this mission.

For the recourse properties the difficulty is bookkeeping: $Q$ is an extended-real optimal value, and finiteness, measurability in $\omega$ and integrability must be derived from complete recourse, dual feasibility and the moment hypothesis rather than assumed.

Formalization scope

Vectors are functions from finite index types to $\mathbb R$ (ι → ℝ), matrices are Mathlib Matrix, and random data live on a probability space (Ω, P). The recourse cost is an EReal infimum over the feasible set, so infeasibility gives $+\infty$ and unboundedness $-\infty$ exactly as on p. 39; theorems that integrate it carry complete recourse and dual feasibility, which make it finite. The expected recourse function integrates the real part of the recourse cost. Independence of the components is ProbabilityTheory.iIndepFun; the box is Set.pi univ (fun j => Icc (a j) (b j)), with $a_j<b_j$, and values in the box are required almost surely. The upper bound is the explicit sum over Boolean vertex labels of products of the weights (2.32); no abstract extremal measure is used.

Conventions fixed where the page is silent or ambiguous:

• Properties (b), (d), (e) are stated on all of $\mathbb R^{n_1}$: under the standing complete-recourse assumption $K_2=\mathbb R^{n_1}$. "Convex piecewise linear" is rendered as a maximum of finitely many affine functions.
• The book's hypothesis of finite second moments in (e) is kept as stated, componentwise.
• The book writes $Q$ for both $Q(x,\xi)$ and $\mathcal Q(x)$, and reuses $\tilde Q$, $\tilde\psi$ for different functions in (2.27) and (2.30)–(2.31); the Lean names are recourseCost, expectedRecourse and dualLowerBound.
• In (2.51) a conditional mean on a null event is $0$ in Lean; it always appears multiplied by that event's probability, so the formula is unchanged.
• In (2.56) the minimum is a real infimum over the nonempty first-stage feasible set; attainment is not claimed.
• No constant of the chapter is hidden behind $O(\cdot)$; all bounds are explicit.

A goal stated for affine $\varphi$ (where it is an equality), or with $\hat\xi$ allowed to be any discrete law with the right mean, would be trivial or a different theorem; the weights are the products of (2.32), and independence of the components is a hypothesis.

A complete development needs: finite-dimensional LP duality with extended-real values (reusable across all recourse missions), measurability and integrability of optimal-value functions, the conditional-independence step for product measures, and the one-dimensional chord inequality. The partitioned upper bound (2.37) and the discrete reformulation (2.21), (2.28) are natural follow-up statements on the same definitions.

Selected references

• P. Kall, A. Ruszczyński, K. Frauendorfer, "Approximation Techniques in Stochastic Programming", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 2, pp. 33–64. https://doi.org/10.1007/978-3-642-61370-8
• A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Annals of Mathematical Statistics 30 (1959), 743–746. https://doi.org/10.1214/aoms/1177706203
• P. Kall, Stochastic Linear Programming, Springer 1976. https://doi.org/10.1007/978-3-642-66252-2
• R. J-B Wets, "Stochastic programs with fixed recourse: the equivalent deterministic program", SIAM Review 16 (1974), 309–339. https://doi.org/10.1137/1016053
• K. Frauendorfer, "Solving SLP recourse problems with arbitrary multivariate distributions — the dependent case", Mathematics of Operations Research 13 (1988), 377–394. https://doi.org/10.1287/moor.13.3.377
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, Springer 1997, Ch. 8. https://doi.org/10.1007/b97617

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access only to function values: the objective is the output of a simulator or a black-box program, and its gradient is unavailable or too expensive. Derivative-free (or zeroth-order) methods address this setting. Nesterov and Spokoiny (Found. Comput. Math. 17 (2017)) showed that a very simple oracle, the finite difference of $f$ along a random Gaussian direction, can replace the gradient in standard first-order schemes at the price of a factor depending only on the dimension. Their analysis became the reference point for later work on zeroth-order stochastic optimization and on gradient-free methods in reinforcement learning and adversarial attacks.

This mission covers Section 6 of the paper: the accelerated random method $\mathcal{FG}_\mu$ and its rate, Theorem 9. It is the third mission of a series; the first covers random search for nonsmooth problems (Theorem 6), the second the random gradient method for smooth problems (Theorem 8).

Setting

Let $E$ be a real inner product space of dimension $n \ge 2$ with norm $\|\cdot\|$ (the paper's space with operator $B$ is $E$ with the inner product $\langle Bx, y\rangle$). Let $u$ be a standard Gaussian vector in $E$, and write $\mathbb E_u$ for expectation over $u$.

The objective $f : E \to \mathbb R$ is differentiable with Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ with $L_1 > 0$, and strongly convex with parameter $\tau \ge 0$:

$$f(y) \ge f(x) + \langle\nabla f(x), y - x\rangle + \tfrac{\tau}{2}\|y - x\|^2 .$$

The value $\tau = 0$ is allowed (plain convexity). The condition number is $\kappa = \tau/L_1$. The problem $f^* = \min_{x \in E} f(x)$ is assumed solvable, with minimizer $x^*$.

For $\mu \ge 0$ the Gaussian approximation is $f_\mu(x) = \mathbb E_u f(x + \mu u)$, and the random gradient-free oracle is

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

The paper (p. 548) sets $\theta_n = 1/(16(n+1)^2L_1(f))$ and $h_n = 1/(4(n+4)L_1(f))$. This mission uses $\theta_n = 1/(16(n+4)^2L_1)$; the reason is given under Formalization scope. Method $\mathcal{FG}_\mu$ (Eq. (60)) chooses $x_0 \in E$, $v_0 = x_0$ and $\gamma_0 > 0$ with $\gamma_0 \ge \tau$, and at every iteration $k \ge 0$:

1. computes $\alpha_k > 0$ with $\theta_n^{-1}\alpha_k^2 = (1 - \alpha_k)\gamma_k + \alpha_k\tau \equiv \gamma_{k+1}$;
2. sets $\lambda_k = \alpha_k\tau/\gamma_{k+1}$, $\beta_k = \alpha_k\gamma_k/(\gamma_k + \alpha_k\tau)$ and $y_k = (1-\beta_k)x_k + \beta_k v_k$;
3. draws a fresh Gaussian direction $u_k$, independent of the past, and computes $g_\mu(y_k)$;
4. sets $x_{k+1} = y_k - h_n B^{-1}g_\mu(y_k)$ and $v_{k+1} = (1-\lambda_k)v_k + \lambda_k y_k - (\theta_n/\alpha_k)B^{-1}g_\mu(y_k)$.

Write $\phi_k = \mathbb E f(x_k)$ (expectation over $u_0, \dots, u_{k-1}$), $\psi_k = \prod_{i=0}^{k-1}(1-\alpha_i)$ and $C_k = 1 + \sum_{i=1}^{k-1}\prod_{j=k-i}^{k-1}(1-\alpha_j)$ for $k \ge 1$, with $\psi_0 = 1$ and $C_0 = 0$ (p. 550).

Formalization targets

Goal: Theorem 9 (p. 549)

For all $k \ge 0$,

$$\phi_k - f^* \le \psi_k\Big[f(x_0) - f(x^*) + \frac{\gamma_0}{2}\|x_0 - x^*\|^2\Big] + \mu^2 L_1\Big(n + \frac{3(n+8)}{16}C_k\Big), \tag{62}$$

where

$$\psi_k \le \min\Big\{\Big(1 - \frac{\kappa^{1/2}}{4(n+4)}\Big)^k,\ \Big(1 + \frac{k}{8(n+4)}\sqrt{\frac{\gamma_0}{L_1}}\Big)^{-2}\Big\}, \qquad C_k \le \min\Big\{k,\ \frac{4(n+4)}{\kappa^{1/2}}\Big\}.$$

The two regimes are a rate $O(n^2/k^2)$ for convex $f$ and a linear rate with ratio $1 - \kappa^{1/2}/(4(n+4))$ for strongly convex $f$, both up to a bias proportional to $\mu^2$.

Milestones

In attack order: Lemma 1 (Gaussian moments, (16)–(17)); Theorem 3.1 (the bound (32) on the second moment of $g_0$); Theorem 1's (19), $|f_\mu - f| \le \frac{\mu^2}{2}L_1 n$; Eq. (12), $L_1(f_\mu) \le L_1(f)$; Lemma 5, the bound (37) on $\mathbb E_u\|g_\mu(x)\|_*^2$ in terms of $\nabla f_\mu(x)$; Eq. (21), $\nabla f_\mu = \mathbb E_u g_\mu$; and Eq. (11), $f_\mu \ge f$ for convex $f$.

Significance

Theorem 9 shows that the $n$-fold slowdown of gradient-free methods relative to their gradient counterparts survives acceleration: $\mathcal{FG}_\mu$ reaches accuracy $\epsilon$ in $O(n L_1^{1/2}R/\epsilon^{1/2})$ iterations for convex $f$, against $O(nL_1R^2/\epsilon)$ for the non-accelerated random gradient method. The analysis also quantifies how small the finite-difference step $\mu$ must be for this to hold. The result is used as the baseline accelerated zeroth-order rate in later work.

The theorem is proved in the paper. As far as is known it has not been machine-checked, and Mathlib has no Gaussian smoothing, no random gradient-free oracle and no analysis of an accelerated method driven by random directions. A formal proof also settles the constant question raised by the printed $\theta_n$ (see below).

Difficulty

The deterministic fast gradient method is analysed by an estimate-sequence argument in which the gradient step is exact. Here the step uses $g_\mu(y_k)$, which is an unbiased estimate of $\nabla f_\mu(y_k)$ and not of $\nabla f(y_k)$, and whose second moment is of order $n\|\nabla f_\mu\|^2$ plus a bias term. The step size and the coupling parameter $\theta_n$ must absorb this second moment, and the argument must be run for $f_\mu$ rather than $f$. The estimate sequence then has to be passed through expectations over the history $u_0, \dots, u_{k-1}$, which requires the independence of $u_k$ from $x_k, v_k, y_k$ and integrability of every quantity involved. Transporting the result from $f_\mu$ back to $f$ uses (11) and (19), and requires that $f_\mu$ inherits strong convexity with the same parameter $\tau$, a fact the paper uses without stating it.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space (InnerProductSpace ℝ E, FiniteDimensional ℝ E, Borel measurable), $n$ is Module.finrank ℝ E, and the Gaussian is Mathlib's stdGaussian E. The operator $B$ is absorbed into the inner product, so $\nabla f$ is gradient f and $B^{-1}g_\mu$ is $\frac{f(x+\mu u)-f(x)}{\mu}u$. This is not a restriction to $B = I$ on $\mathbb R^n$. All expectations are Bochner integrals; under the hypotheses every integrand is integrable, so no integrability hypothesis is added.

The run is a structure over a probability space $(\Omega, \mathbb P)$: directions $u_k$ that are measurable, mutually independent (iIndepFun) and standard Gaussian; deterministic sequences $\gamma, \alpha$ satisfying step a) as equations; and random points $x_k, v_k$ satisfying steps b)–d) for every outcome. The smoothing parameter satisfies $\mu \ge 0$, and at $\mu = 0$ the oracle is $g_0$. The goal pins $\theta = 1/(16(n+4)^2L_1)$ and $h = 1/(4(n+4)L_1)$. $\psi_k$ and $C_k$ are definitions computed from $\alpha$.

The constant $\theta_n$. The paper prints $\theta_n = \frac{1}{16(n+1)^2L_1(f)}$. The proof (pp. 549–550) needs $\frac{h_n}{4(n+4)} - \frac{h_n^2L_1}{2} = \frac{1}{32(n+4)^2L_1} = \frac{\theta_n}{2}$, $\alpha_k \ge [\tau\theta_n]^{1/2} = \frac{\kappa^{1/2}}{4(n+4)}$ and $\theta_n^{1/2} = \frac{1}{4(n+4)L_1^{1/2}}$, which hold only with $(n+4)$. With the printed value $\theta_n$ is larger than the first inequality allows, and the argument does not go through. The mission therefore states Theorem 9 with $\theta_n = \frac{1}{16(n+4)^2L_1}$; all other constants are as printed.

Two trivializing formalizations are ruled out. First, the bound $C_k \le 4(n+4)/\kappa^{1/2}$ carries the hypothesis $\tau > 0$: at $\tau = 0$ the paper's value is $+\infty$, while Lean's division by zero would turn it into $C_k \le 0$, which is false. $\psi_k$ and $C_k$ are definitions from the run, not free variables that only satisfy the bounds. Second, the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the exact gradient (which would give Nesterov's deterministic method) and not an arbitrary direction sequence.

A complete development needs Gaussian integration by parts in an inner product space, moment bounds for $\|u\|$, differentiation under the integral sign for $f_\mu$, and conditional expectation along an i.i.d. sequence. The smoothing layer (Lemma 1, (11), (12), (19), (21), (32), (37)) is reusable for any zeroth-order method, and contributions of these components as separate lemmas are welcome.

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Lemma 2.2.4 and Section 2.2.1, the estimate-sequence analysis the proof of Theorem 9 follows). https://doi.org/10.1007/978-1-4419-8853-9