Convex Optimization

Motivation

Every linear program comes with a second linear program, its dual, and most of what is known about linear programming is a statement about how the two interact. Weak duality gives certificates of optimality; strong duality says those certificates always exist; complementary slackness turns optimality into a system of equations. These three facts are the core of any first course in optimization and of every correctness argument for the simplex method.

Strict complementarity is the sharpest statement of the same kind. Complementary slackness says that in each pair (a primal variable and its dual slack, a dual variable and its primal slack) at least one member vanishes at optimality. Strict complementarity says that some optimal pair can be chosen so that exactly one member vanishes in each pair. The result is due to Goldman and Tucker (1956). It is what identifies the optimal face of a linear program and its partition of the variables into those that can be positive at an optimum and those that cannot, and it is a standing ingredient in the analysis of interior-point methods, which approach this strictly complementary optimum rather than a vertex.

This mission formalizes the chain from duality to strict complementarity as it is developed in Chapters 5 and 10 of Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, doi:10.1007/978-1-4614-7630-6). It is the second mission of a series on that book.

Timeline:

• 1902 — Farkas publishes the lemma on the solvability of linear inequality systems.
• 1947–1951 — von Neumann, and Gale, Kuhn and Tucker, establish linear programming duality.
• 1956 — Goldman and Tucker prove the existence of strictly complementary optimal solutions (in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38).

Setting

Fix integers $m, n \ge 0$, a real $m \times n$ matrix $A = (a_{ij})$, a vector $b \in \mathbb{R}^m$ and a vector $c \in \mathbb{R}^n$. The primal problem is

$$\text{maximize } c^T x \quad\text{subject to}\quad Ax + w = b,\quad x \ge 0,\ w \ge 0, \qquad (10.9)$$

where $w = b - Ax$ is the primal slack. The dual problem is

$$\text{minimize } b^T y \quad\text{subject to}\quad A^T y - z = c,\quad y \ge 0,\ z \ge 0, \qquad (10.10)$$

where $z = A^T y - c$ is the dual slack. A vector $x$ is primal feasible if $x \ge 0$ and $w \ge 0$; it is primal optimal if it is feasible and $c^T x' \le c^T x$ for every feasible $x'$. Dual feasibility and dual optimality are defined in the same way, with minimization. Inequalities between vectors are componentwise, and $\xi > 0$ means that every component of $\xi$ is strictly positive.

A halfspace of $\mathbb{R}^n$ is a set $\{x : a^T x \le \beta\}$ with $a \ne 0$; a polyhedron is a set $\{x : Ax \le b\}$ for some $m$, $A$ and $b$.

In the Lean development these objects live in the namespace VanderbeiLP.StrictComp: primalSlack A b x, dualSlack A c y, PrimalFeasible, DualFeasible, PrimalOptimal, DualOptimal, IsHalfspace, IsPolyhedron.

Formalization targets

Goal: Strict Complementary Slackness (Theorem 10.7)

If the primal (10.9) has an optimal solution, then there exist a primal optimal $x^*$ and a dual optimal $y^*$, with slacks $w^* = b - Ax^*$ and $z^* = A^T y^* - c$, such that

$$x^* + z^* > 0 \qquad\text{and}\qquad y^* + w^* > 0.$$

The only hypothesis is primal optimality; the existence of a dual optimum is part of the conclusion.

Milestones

1. Theorem 5.1 (Weak Duality). Primal feasible $x$ and dual feasible $y$ satisfy $c^T x \le b^T y$.
2. Theorem 5.2 (Strong Duality). If the primal has an optimal $x^*$, the dual has an optimal $y^*$ with $c^T x^* = b^T y^*$.
3. Theorem 5.3 (Complementary Slackness). Feasible $x$, $y$ are both optimal if and only if $x_j z_j = 0$ for all $j$ and $w_i y_i = 0$ for all $i$.
4. Lemma 10.5 (Farkas' Lemma). $Ax \le b$ has no solution if and only if some $y$ satisfies $A^T y = 0$, $y \ge 0$, $b^T y < 0$.
5. Theorem 10.4 (Separation of polyhedra). Two disjoint nonempty polyhedra lie in two disjoint halfspaces.
6. Theorem 10.6. If both problems are feasible, there are feasible $\bar x$, $\bar y$ with $\bar x + \bar z > 0$ and $\bar y + \bar w > 0$.

Theorem 10.6 is the feasible-solution version of the goal; Theorem 10.4 is a further consequence of Farkas' Lemma in the same chapter.

Significance

Strict complementarity determines the optimal partition: the set of indices $j$ for which some optimal $x^*$ has $x^*_j > 0$ is exactly the complement of the set for which some optimal dual slack $z^*_j$ is positive. This partition describes the optimal faces of both problems, is the object that interior-point methods recover in the limit, and is the starting point of sensitivity analysis beyond a single optimal basis. Farkas' Lemma and the separation theorem are the linear-algebraic form of convex separation and are reused across optimization, game theory and polyhedral combinatorics.

All results of this mission are classical and proved in the literature. What the mission adds is a machine-checked version of them in one fixed linear-programming form, the inequality form with explicit slacks used throughout Vanderbei's book. Weak duality, strong duality and complementary slackness are already formalized on this platform for other forms (Bertsimas–Tsitsiklis's general form, a minimization, and a covering pair with the roles of primal and dual exchanged). Those statements are equivalent to the ones here only after a transformation (negating the objective, swapping primal and dual), so they are not the same theorems. The Farkas variant for inequality systems, the separation theorem for two polyhedra, and both strict complementarity theorems have no formal counterpart on the platform.

Difficulty

Weak duality and the converse direction of complementary slackness are short computations. The substance lies elsewhere. Strong duality and Farkas' Lemma require a genuine existence argument; the book obtains them from the simplex method, whose termination is itself a nontrivial fact, and any other route needs an independent theorem of the alternative.

For strict complementarity the obvious attempt fails. Complementary slackness gives, for each optimal pair, only that one member of each complementary pair vanishes; nothing in a single optimal basic solution forces the other member to be positive, and in degenerate problems every basic optimal pair can fail strictness. A strictly complementary pair is in general not a vertex of either optimal face, so it cannot be found by inspecting basic solutions. The goal also asks for more than Theorem 10.6: the positivity must be achieved within the optimal sets, which are faces cut out by an additional objective-level constraint, so the feasible-solution argument does not transfer verbatim.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; the constraint matrix is Matrix (Fin m) (Fin n) ℝ; m and n are arbitrary natural numbers, including zero. The slacks are functions of the solution (primalSlack A b x = b - A *ᵥ x, dualSlack A c y = Aᵀ *ᵥ y - c), never free variables, so a "solution $(x, w)$" of the book is the vector $x$ with the slack it determines. Optimality is attainment of the maximum (minimum) over the feasible set; no supremum, value function or extended reals are involved. The strict inequality $\xi > 0$ is written componentwise as ∀ j, 0 < x j + dualSlack A c y j and ∀ i, 0 < y i + primalSlack A b x i.

A halfspace carries a nonzero normal vector. Without that requirement the empty set would be a halfspace and the separation theorem would be trivial; the formal definition rules this out.

The book states every result in this mission with its hypotheses explicit, and none of them asserts the existence of an unspecified constant, so no explicit-constant instantiation was needed. The remark after Theorem 10.7 refers to "the complementary slackness theorem (Theorem 5.1)"; the complementary slackness theorem is Theorem 5.3, and the milestones follow the theorem numbering.

A complete development needs a theorem of the alternative for real linear inequality systems (Mathlib has Farkas-type results for cones and the geometric Hahn–Banach theorem, but no ready-made matrix version of Lemma 10.5) and elementary convex-combination arguments on feasible sets. The definitions of this mission are self-contained and reusable for any later chapter that works in Vanderbei's inequality form. Proofs of any milestone are welcome, as are proofs that avoid the simplex method.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014. doi:10.1007/978-1-4614-7630-6
• J. Farkas, "Theorie der einfachen Ungleichungen", Journal für die reine und angewandte Mathematik 124 (1902), 1–27. doi:10.1515/crll.1902.124.1
• A. J. Goldman and A. W. Tucker, "Theory of linear programming", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• 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

Large convex programs often have a block structure: a small set of "complicating" variables $x$ couples otherwise separate subproblems in the remaining variables $y$. Decomposition with respect to variables fixes $x$, solves the subproblem in $y$, and treats the optimal subproblem value as a function of $x$ alone. The outer problem in $x$ is then small but nonsmooth, because the optimal value of a constrained program is generally not differentiable in its parameters. Shor's Chapter 4 (Shor 1985, Ch. 4) presents this reduction as a principal application of subgradient methods: once a subgradient of the outer function can be read off from the subproblem, the methods of Chapters 2–3 apply directly. The same construction underlies Benders decomposition (Benders 1962) and its convex generalization (Geoffrion 1972), and parametric decomposition schemes for linear programs.

The chapter's other numbered results serve the same programme from the dual side: the Lagrangian dual function of a program over a compact set gives a lower bound usable in branch and bound (Theorem 4.3), exact nonsmooth penalty functions turn a constrained convex program into one unconstrained nonsmooth minimization (Theorem 4.2; nonsmooth penalties were first studied systematically by I. I. Eremin, 1967), and a stochastic transportation model is shown to be a convex program before being solved through its dual (Lemma 4.3).

Setting

The variables split into $x \in E^x_l$ and $y \in E^y_m$ (Euclidean spaces, inner product $(\cdot,\cdot)$). The problem is

$$\min_{x,y} f_0(x,y) \quad \text{s.t.} \quad f_i(x,y) \le 0,\quad i = 1,\dots,n, \qquad (4.1)\text{–}(4.2)$$

with $f_0, f_1, \dots, f_n$ convex functions of $z = (x,y)$ (jointly convex), finite everywhere. For a fixed $\bar x$, the subproblem (4.3)–(4.4) is $\min_{y \in D(\bar x)} f_0(\bar x, y)$ with $D(\bar x) = \{y : f_i(\bar x,y) \le 0\}$. Where it has a solution $y(\bar x)$, the value function is

$$\Phi(\bar x) = \min_{y \in D(\bar x)} f_0(\bar x,y). \qquad (4.5)$$

The Slater condition at $\bar x$ asks for a $y$ with $f_i(\bar x,y) < 0$ for all $i$. The Lagrange function is $L_U(x,y) = f_0(x,y) + \sum_i U_i f_i(x,y)$, and $U \ge 0$ are Kuhn–Tucker multipliers at $\bar x$ when $\Phi(\bar x) = \min_y L_U(\bar x,y)$. A subgradient of a function of $(x,y)$ is written through its projections $(g^x, g^y)$ on the two blocks; a subgradient of $\Phi$ at $\bar x$ is a $g$ with $\Phi(x) - \Phi(\bar x) \ge (x - \bar x, g)$.

Formalization targets

Goal: Theorem 4.1 (p. 94)

If $W$ is a convex set of $x$-values at which the subproblem has a solution, then $\Phi$ is convex on $W$; and if $\bar x \in W$ satisfies the Slater condition, then for every optimal $y(\bar x)$, multipliers $U$ exist, $L_U$ has a subgradient at $(\bar x, y(\bar x))$ with vanishing $y$-projection, and the $x$-projection of any such subgradient satisfies

$$g_\Phi(\bar x) = g^x_{L_U}(\bar x, y(\bar x)) \in \partial \Phi(\bar x). \qquad (4.6)$$

Milestones for the goal

1. Convexity of $\Phi$ on $W$ (Theorem 4.1, first assertion).
2. Existence of Kuhn–Tucker multipliers for the subproblem under Slater (p. 95, display).
3. Existence of a subgradient of $L_U$ with vanishing $y$-projection (p. 95).
4. Formula (4.6) for a given multiplier vector and such a subgradient (p. 95, final display).

Further results of the chapter

5. Corollary (4.7): if each $f_\alpha(x,\cdot)$ is continuously differentiable in $y$, then $g^x_{f_0} + \sum_i U_i g^x_{f_i}$, built from arbitrary subgradients of the $f_\alpha$, is a subgradient of $\Phi$.
6. Lemma 4.3: the stochastic transportation problem (4.163)–(4.165) is a convex program.
7. Theorem 4.2: with nonsmooth penalties $p_i$ whose slopes $c_i = \lim_{t\to0+} p_i(t)/t$ exceed a Lagrange multiplier vector $\bar y$, the minimizers of $S = f_0 + \sum p_i \circ f_i$ are exactly the solutions of the constrained program; and if a minimizer of $S$ solves the program, some multiplier vector satisfies $\bar y \le c$.
8. Theorem 4.3: for $\Phi(u) = \min_{x\in X}[f_0 + \sum u_i f_i]$ over a compact $X$, $Q = \max_{u\ge0}\Phi(u) \le f^*$.

Significance

The result itself. Theorem 4.1 is what makes decomposition with respect to variables an instance of convex nonsmooth minimization: the outer problem is convex, and one subproblem solve returns both $\Phi(\bar x)$ and a subgradient. The algorithm on p. 96 — solve the subproblem at $x_k$, form $g_\Phi(x_k)$ by (4.6) or (4.7), take a subgradient step — is exactly this, and the step-size theory of Chapter 2 then gives convergence. The Corollary is the version used in practice for linear and quadratic subproblems, where multipliers and partial subgradients are computed directly. Theorem 4.2 justifies replacing constraints by nonsmooth penalties of finite slope, and Theorem 4.3 is the weak-duality bound behind Lagrangian relaxation in branch and bound.

Formalizing it. All results are classical and proved in the book; none is formalized as stated here. The platform already has related statements with different shapes: convexity of the perturbation value function in the constraint right-hand side (VectorSpaceOpt.perturbationValue_convex, Luenberger), Slater strong duality over the whole space (ConvexOptimization.slater_strong_duality), weak duality with an unconstrained domain (ConvexOptimization.weak_duality), weak Lagrangean duality for integer programs (LinearOptimization.integer_program_weak_lagrangean_duality), and the LP special case of convexity of the optimal cost (LinearOptimization.lp_optimal_cost_convex_in_rhs). This mission adds the partial-minimization form in which one block of variables is minimized out under joint convexity, its subgradient calculus, exact nonsmooth penalties, and weak duality over a compact domain.

Difficulty

Convexity of $\Phi$ is elementary once the minimum is attained. The subgradient formula is where the obvious argument fails: an arbitrary subgradient of $L_U$ at $(\bar x, y(\bar x))$ does not project to a subgradient of $\Phi$, because its $y$-projection contributes a term $(y(x) - y(\bar x), g^y)$ of unknown sign. The theorem needs a subgradient whose $y$-projection vanishes, and its existence is a separate fact about partial minimization of a jointly convex, everywhere-finite function. The multipliers come from the Kuhn–Tucker theorem for the subproblem, which requires the Slater condition. In the Corollary, the difficulty is to show that differentiability in $y$ forces the $y$-projection of any combination $g_{f_0} + \sum U_i g_{f_i}$ to vanish. In Theorem 4.2 the necessity part needs a subdifferential chain rule for $p_i \circ f_i$.

Formalization scope

• $E^x_l$, $E^y_m$ and $E_N$ are EuclideanSpace ℝ (Fin l), EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin N); constraints are indexed by Fin n (or Fin m). All functions are real-valued and finite everywhere; joint convexity is convexity on the product $E^x_l \times E^y_m$.
• $\Phi$ is a real infimum over $D(x)$. It is the book's minimum wherever the minimum is attained, and every statement assumes attainment at each point of $W$. A statement about $\Phi$ at points where the subproblem has no solution would be about Lean's default value $0$, and is ruled out by these hypotheses.
• "Convex on some convex subset $W$ of $E_n$" is read as convexity on every convex $W$ on which $\Phi$ is defined. A formalization quantifying over a single unspecified $W$ (e.g. a singleton) would be trivially true.
• Formula (4.6) is stated for subgradients of $L_U$ whose $y$-projection is zero, as the book's proof uses it; the subgradient inequality for $\Phi$ is stated on all of $W$.
• Kuhn–Tucker multipliers relative to an optimal $\bar y$: $U \ge 0$, $U_i f_i(\bar x,\bar y) = 0$, and $\bar y$ minimizes $L_U(\bar x,\cdot)$ over all $y$.
• Theorem 4.2: a Lagrange multiplier vector is $\bar y \ge 0$ with $f_0 + \sum\bar y_i f_i \ge f^*$ everywhere, $f^*$ the finite optimal value; the necessity clause is read as "for some multiplier vector" (for all multiplier vectors it is false); the limits $c_i$ are given as hypotheses.
• Theorem 4.3: the minimum (4.187) attained for every $u \ge 0$ (the book's "min"; no continuity assumed); $f^*$ attained; $Q$ attained as the book's "max" presupposes.
• Lemma 4.3: demands with densities and finite mean, penalty coefficients $r_j \ge 0$.

Useful infrastructure beyond this mission: partial minimization of jointly convex functions, subgradients on product spaces, and a Kuhn–Tucker saddle-point theorem for convex programs with inequality constraints. Proofs of any milestone, and reusable lemmas for these, are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Ch. 4, pp. 93–96, 131–133, 146–148. https://doi.org/10.1007/978-3-642-82118-9
• J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4, 1962, 238–252. https://doi.org/10.1007/BF01386316
• A. M. Geoffrion, Generalized Benders decomposition, Journal of Optimization Theory and Applications 10, 1972, 237–260. https://doi.org/10.1007/BF00934810
• I. I. Eremin, The penalty method in convex programming, Soviet Mathematics Doklady 8, 1967, 459–462 (Shor's reference [22]).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §29 (partial minimization and perturbation functions). https://doi.org/10.1515/9781400873173

Motivation

The ellipsoid method is the algorithm that settled the polynomial-time solvability of linear programming (Khachiyan, 1979) and that underlies the equivalence of separation and optimization in combinatorial optimization (Grötschel, Lovász and Schrijver, 1981). Its origin is in nonsmooth convex optimization. In 1976 Yudin and Nemirovskii proposed a modified method of centered sections that localizes an optimum inside a sequence of ellipsoids, and in 1977 N. Z. Shor observed independently that the same scheme is a subgradient method with space dilation along the gradient, the family of methods he had developed since 1969. Section 3.8 of Shor's monograph Minimization Methods for Non-Differentiable Functions (Springer 1985) presents the method in this second form and proves its basic localization property.

Timeline:

• 1965. A. Yu. Levin proposes the method of centered sections (cuts through the center of gravity of a polyhedron); each cut removes at least a fixed fraction of the volume, but computing centers of gravity is impractical for $n > 3$.
• 1969–1972. Shor introduces subgradient methods with space dilation along the gradient (SDG methods).
• 1976. Yudin and Nemirovskii replace the polyhedron by a minimal ellipsoid containing a half-ellipsoid, obtaining a geometric volume decrease depending only on the dimension ([Yudin–Nemirovskii 1976]).
• 1977. Shor shows that the same method is an SDG algorithm with coefficient $\beta = \sqrt{(n-1)/(n+1)}$ ([Shor 1977]).
• 1979. Khachiyan applies the method to linear inequalities with integer data, obtaining the first polynomial-time algorithm for linear programming ([Khachiyan 1979]).

Setting

Let $E_n$ be $n$-dimensional Euclidean space with inner product $(x, y)$, and $n > 1$. For a unit vector $\xi$ and a number $\alpha$, the operator of space dilation along $\xi$ with coefficient $\alpha$ is $R_\alpha(\xi) = I + (\alpha - 1)\xi\xi^T$: it multiplies the component of a vector along $\xi$ by $\alpha$ and leaves the orthogonal component unchanged.

Let $g : E_n \to E_n$ be a vector field, not necessarily continuous. The problem is to find a point $x^*$ with

$$(g(x), x - x^*) \ge 0 \quad \text{for all } x \in E_n,$$

where it is known that such an $x^*$ exists in the closed ball $S(x_0, R)$ of radius $R > 0$ about a given point $x_0$. Put $\beta = \sqrt{(n-1)/(n+1)}$ and $r = n/\sqrt{n^2-1}$. The algorithm (3.57)–(3.60) starts from $x_0$, $B_0 = I_n$, $h_0 = R/(n+1)$, and at iteration $k+1$ stops if $g(x_k) = 0$, and otherwise sets

$$\xi_k = \frac{B_k^T g(x_k)}{\|B_k^T g(x_k)\|}, \quad x_{k+1} = x_k - h_k B_k \xi_k, \quad B_{k+1} = B_k R_\beta(\xi_k), \quad h_{k+1} = r h_k .$$

With $A_k = B_k^{-1}$, the localizing ellipsoid is $\Phi_k = \{x : \|A_k(x - x_k)\| \le (n+1)h_k\}$, and the dimension-dependent ratio is

$$q_n = \sqrt{\frac{n-1}{n+1}}\left(\frac{n}{\sqrt{n^2-1}}\right)^n < 1 .$$

Three problems produce such a field: minimizing a convex $f$ on a ball (the field (3.62), a subgradient inside the ball and the outward radial direction outside); the convex program $\min f_0$ s.t. $f_i \le 0$ (the field (3.65), a subgradient of the objective at feasible points and of a most violated constraint otherwise); and a convex–concave saddle point problem (the field $\{g_f^x, -g_f^y\}$).

Formalization targets

Goal: Theorem 3.14 (p. 86)

For every $k$,

$$\|A_k(x_k - x^*)\| \le h_k (n+1), \tag{3.61}$$

that is, $x^* \in \Phi_k$. The statement holds for every field $g$ satisfying the monotonicity condition at $x^*$; nothing about continuity or convexity is assumed.

Milestones

1. Eq. (3.4): $\|R_\alpha(\xi)x\| = \sqrt{\|x\|^2 + (\alpha^2-1)(x,\xi)^2}$ for unit $\xi$.
2. Volume of $\Phi_k$ (p. 87): $(n+1)h_k = R r^k$ and $v(\Phi_k) = v_0 R^n r^{nk}/\det A_k$, $v_0$ the volume of the unit ball.
3. Volume ratio (p. 87–88): $v(\Phi_{k+1}) = q_n\, v(\Phi_k)$ with $q_n < 1$, the volumes being positive and finite.
4. Eq. (3.62): the ball field satisfies $(g(x), x - x^*) \ge 0$.
5. Eq. (3.65): the convex-programming field satisfies $(g(x), x - x^*) \ge 0$.
6. Saddle point field (p. 90): $(g(z), z - z^*) \ge 0$.

Significance

The result. Theorem 3.14 with the volume identity says that after $k$ steps the solution is confined to an ellipsoid of volume $q_n^k$ times that of the initial ball, for any field of the above kind. Milestones 4–6 turn this into localization guarantees for constrained convex minimization, general convex programming and convex–concave saddle points, with a rate that depends only on the dimension. The same localization underlies the complexity bounds of the ellipsoid method for linear programming and the polynomial equivalence of separation and optimization.

Formalizing it. The results are classical and proved in the book. No machine-checked proof of the space-dilation form of the method is known to exist. The platform already contains a proved version of the Bertsimas–Tsitsiklis form (LinearOptimization.ellipsoid_update_halfspace_subset, LinearOptimization.ellipsoid_update_volume_lt: a half-ellipsoid $E(z, D) \cap \{a^Tx \ge a^Tz\}$ is covered by an updated ellipsoid whose volume is smaller by a factor below $e^{-1/(2(n+1))}$), and Khachiyan's feasibility algorithm (SmaleNinth.khachiyan_ellipsoid_decides). Those statements are about a center/shape-matrix update and give a volume inequality; this mission is about the iterates of Shor's matrix recursion $B_{k+1} = B_k R_\beta(\xi_k)$ and the exact ratio $q_n$. Relating the two parametrizations ($D_k = (n+1)^2 h_k^2 B_k B_k^T$) is a welcome side result.

Difficulty

The obvious approach, tracking the ellipsoid through the center and shape matrix and invoking a minimum-volume covering argument, is not what the algorithm computes: here the iterate is updated through the factor $B_k$ and the stepsize $h_k$ is fixed in advance, independent of the field, so the induction must be carried out in the transformed coordinates $z_k = A_k(x_k - x^*)$ in which the ellipsoid is a ball. The difficulty is that the monotonicity condition gives only the sign of one inner product, $(z_k, \xi_k) \ge 0$, while the norm of $z_{k+1}$ depends on both $(z_k,\xi_k)$ and $\|z_k\|$; the constants $\beta$ and $r$ are exactly those for which the resulting quadratic estimate closes. For the volume identity, the main technical step is computing $\det R_\beta(\xi) = \beta$ and the Lebesgue measure of a linear image of a ball in EuclideanSpace.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); matrices act through Matrix.toEuclideanLin; $B_k^*$ is the transpose. $R_\alpha(\xi)$ is the matrix $I + (\alpha-1)\xi\xi^T$ (the book's property 10); for unit $\xi$ this is the operator of the book's definition.
• The algorithm is the definition ellipsoidMethod g R x₀ : ℕ → EllState n, with state $(x_k, B_k, h_k)$, $B_0 = I$, $h_0 = R/(n+1)$. If $g(x_k) = 0$ the state is repeated from then on (the book stops); the normalization in (3.57) is only performed when $g(x_k) \ne 0$. $A_k$ is the matrix inverse of $B_k$, which is nonsingular.
• Theorem 3.14 is stated for $n > 1$, $R > 0$, $x^*$ with $\|x_0 - x^*\| \le R$ and $(g(x), x - x^*) \ge 0$ for all $x$, for every $k$. The book's additional assumption that $g(x) \ne 0$ for $x \ne x^*$ is not used by its proof and is omitted. The iterates are those of the recursion; a statement about an arbitrary ellipsoid containing $x^*$, or about an arbitrary invertible matrix in place of $B_k$, would not be this theorem and is ruled out by the definitions.
• Volumes are Lebesgue measure in ℝ≥0∞. The ellipsoid is given for an arbitrary center (the book writes $x^*$ in one place and $x_k$ in another; the volume is the same). The volume formula requires the first $k$ iterations to have been performed ($g(x_j) \ne 0$, $j < k$); the ratio requires iteration $k+1$ to be performed.
• The printed chain on p. 87 has misprints (exponents $2$ and $1$ on $n/\sqrt{n^2-1}$ where $n$ is meant, and $(n-1)/(n+1)$ for $\sqrt{(n-1)/(n+1)}$); the statement follows the value of $q_n$ given on p. 88. The estimate for $x \notin S(x_0,R)$ before (3.62) has a sign misprint; only the conclusion is stated.
• Needed infrastructure: determinant of a rank-one perturbation of the identity ($\det(I + c\,\xi\xi^T) = 1 + c\|\xi\|^2$, available in Mathlib as the matrix determinant lemma), the measure of a linear image (MeasureTheory.Measure.addHaar_image_linearMap), and elementary real inequalities for $q_n < 1$. The space-dilation lemmas are reusable in the other Shor missions on SDG methods and the $r$-algorithm.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §3.8. https://doi.org/10.1007/978-3-642-82118-9
• D. B. Yudin and A. S. Nemirovskii, Informational complexity and efficient methods for the solution of convex extremal problems, Ekonomika i Matematicheskie Metody 12 (1976), 357–369 (English translation: Matekon 13 (1977), 25–45).
• N. Z. Shor, Cut-off method with space extension in convex programming problems, Cybernetics 13 (1977), 94–96.
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20 (1979), 191–194.
• R. G. Bland, D. Goldfarb and M. J. Todd, The ellipsoid method: a survey, Operations Research 29 (1981), 1039–1091. https://doi.org/10.1287/opre.29.6.1039
• M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

Many optimization problems of operations research have objectives that are convex but not differentiable: Lagrangian duals of integer and combinatorial programs, maxima of finitely many affine or smooth functions, penalty functions for systems of inequalities, and the value functions produced by decomposition. For such functions the gradient method and steepest descent fail. Constant steps cannot work because the subgradients need not tend to zero at a nondifferentiable minimum, and exact line search along the negative gradient can converge to a point that is not a minimizer (the example on pp. 22–23 of the source).

The subgradient method replaces the gradient by an arbitrary subgradient and gives up monotone decrease of the objective. Its convergence theory is the foundation of nondifferentiable optimization and of Lagrangian relaxation in integer programming.

Timeline. N. Z. Shor proposed the method with normalized steps in 1962 (Kiev). Yu. M. Ermoliev proved convergence in finite dimensions with divergent-series stepsizes (Kibernetika, 1966), and B. T. Polyak proved it for constrained problems in Hilbert space (Doklady Akad. Nauk SSSR, 1967). Held, Wolfe and Crowder (Mathematical Programming, 1974) brought the method to large combinatorial problems through Lagrangian relaxation. This mission formalizes the exposition of Section 2.1–2.2 of Shor's monograph (Springer, 1985), which gives self-contained proofs of these results.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. Let $f : E_n \to \mathbb{R}$ be a convex function finite everywhere. A vector $g$ is a subgradient of $f$ at $x_0$ if

$$f(x) - f(x_0) \ge (g, x - x_0) \quad \text{for all } x \in E_n.$$

Every convex $f$ has at least one subgradient at every point. Let $M^* = \{x : f(x) \le f(y) \ \forall y\}$ be the set of minimum points and, when it is nonempty, $f^* = \min f$.

A subgradient selection $g_f$ assigns to each $x$ some subgradient $g_f(x)$ of $f$ at $x$. No particular choice is made: every result holds for every selection. Given stepsizes $h_1, h_2, \dots > 0$ and a starting point $x_0$, 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, \dots \tag{2.4}$$

If $g_f(x_k) = 0$, then $x_k$ is a minimizer and the computation stops. The unnormalized method is $x_{k+1} = x_k - h_{k+1} g_f(x_k)$ (2.5), and the method with restarts takes that step when $h_{k+1}\|g_f(x_k)\| \le c$ and returns to $x_0$ otherwise.

Formalization targets

Goal: Theorem 2.2 (p. 25)

If $M^*$ is nonempty and bounded, $h_k > 0$, $h_k \to 0$ and $\sum_{k \ge 1} h_k = +\infty$, then for every $x_0$ and every subgradient selection, the method (2.4) either reaches $M^*$ at some index $\bar k$ or

$$\lim_{k \to \infty} \min_{y \in M^*} \|x_k - y\| = 0, \qquad \lim_{k \to \infty} f(x_k) = f^*.$$

Milestones

1. Eq. (2.3), the one-step inequality $\|x_{k+1} - x^*\|^2 \le \|x_k - x^*\|^2 + h^2 - 2h\,\rho(x^*, U_k)$, where $U_k = \{x : f(x) = f(x_k)\}$.
2. Theorem 2.1: with constant step length $h$, some level surface $\{f = f(x_{k^*})\}$ passes within $h(1+\varepsilon)/2$ of any $x^* \in M^*$.
3. Corollaries 1 and 2: a suitable constant step length yields a subsequence with $f(x_{k_i}) - f^* < \delta$. If $M^*$ contains a ball of radius $r > h/2$, the method terminates in $M^*$.
4. Theorem 2.5: if $M^*$ contains a ball of radius $r$, $\sum h_k = \infty$ and $\limsup h_k < 2r$, then (2.4) terminates in $M^*$.
5. Theorem 2.3: for the unnormalized method (2.5), bounded subgradients along the trajectory imply convergence, and unbounded subgradients rule it out.
6. Theorem 2.4: the method with restarts converges for every $c > 0$.

Significance

Theorem 2.2 is the basic convergence guarantee for first-order methods on general nonsmooth convex functions. It needs no Lipschitz constant, no bound on the subgradients and no smoothness: normalizing the step makes the step length independent of the size of the subgradient. The divergent-series rule $h_k \to 0$, $\sum h_k = \infty$ is the standard stepsize condition of stochastic approximation and of Lagrangian relaxation codes. Theorems 2.3–2.5 mark its boundaries. The unnormalized method needs bounded subgradients (Theorem 2.3), restarts remove that need (Theorem 2.4), and a solution set with nonempty interior gives finite termination (Theorem 2.5). The last result is the basis of the finite methods for systems of convex inequalities and for the dual of an assignment problem with a unique solution (pp. 28–29).

All of these results are classical and proved in the source. None of them is formalized in Lean's Mathlib. The platform has neighbouring results that are not the same statements: Poljak's divergent-series theorem for concave piecewise-linear maximization (in Validation of Subgradient Optimization I), and rate bounds for Lipschitz objectives (First-Order and Stochastic Optimization Methods for ML II, Understanding Machine Learning X). This mission adds the general convex case with normalized steps, the dichotomy for unnormalized steps, and finite termination.

Difficulty

The standard rate analysis of the subgradient method bounds $\|x_{k+1} - x^*\|^2 - \|x_k - x^*\|^2$ by $-2h_{k+1}(f(x_k) - f^*)/\|g_f(x_k)\| + h_{k+1}^2$. It then needs a uniform bound on $\|g_f(x_k)\|$, which is exactly what is not assumed here. Nothing a priori keeps the iterates in a bounded set, and the subgradients of a general convex function (for instance $f(x) = x^4$, the source's example on p. 26) grow without bound away from $M^*$; with unnormalized steps this makes the method diverge. Even with normalized steps, the distance to a minimizer decreases only outside a neighbourhood of $M^*$ whose size is of the order of the current step, so a monotone decrease argument gives at best a subsequence with small function values. Convergence of the whole sequence $\min_{y \in M^*}\|x_k - y\|$ to zero is a stronger statement, and boundedness of $M^*$ is essential to it.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere) with ConvexOn ℝ Set.univ f.
• The subgradient selection g is arbitrary, with the hypothesis ∀ x, IsSubgradient f x (g x). The starting point is arbitrary.
• The iterations are defined recursively (normalizedIter, plainIter, resetIter); the stepsize sequence is h : ℕ → ℝ with h (k+1) used at step $k$. In (2.4), a zero subgradient is handled by an explicit branch that repeats the current iterate (which is then in $M^*$). No statement relies on Lean's convention $x/0 = 0$.
• $M^*$ is required to be nonempty wherever the book writes $\min_{y \in M^*}$ or $f^* = \min f$. $\min_{y \in M^*}\|x_k - y\|$ is Metric.infDist, and $f^*$ is ⨅ y, f y.
• $\sum_{k \ge 1} h_k = +\infty$ is Tendsto (fun N => ∑ k ∈ Finset.range N, h (k+1)) atTop atTop. $\limsup h_k < 2r$ is "for some $q < 2r$, eventually $h_k \le q$", so it cannot hold vacuously for an unbounded sequence.
• Corollary 1's step length $h_\delta$ is quantified before the selection and the starting point: it depends only on $f$ and $\delta$.
• Theorem 2.3 is stated as two implications, (bounded subgradients ⇒ convergence) and (unbounded ⇒ no convergence), not as a disjunction that one case could satisfy trivially.
• A formalization of Theorem 2.2 that assumes bounded subgradients, a Lipschitz $f$, or a specific subgradient choice (such as the minimal-norm one) proves a different and weaker theorem, and does not close the goal.

Needed infrastructure: continuity of convex functions on $E_n$ (in Mathlib), compactness of sublevel sets when $M^*$ is bounded, and the geometry of level surfaces relative to supporting hyperplanes. The one-step inequality (2.3) and the level-set compactness lemma are reusable by the later missions of this series (linear rate, Polyak's stepsize, stochastic subgradient). Contributions that prove Eq. (2.3) or Theorem 2.1 first are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Chapter 2, pp. 22–30. https://doi.org/10.1007/978-3-642-82118-9
• B. T. Polyak, A general method for solving extremal problems, Doklady Akademii Nauk SSSR 174 (1967), 33–36 (the source's reference [64]).
• Yu. M. Ermoliev, Methods for solving nonlinear extremal problems, Kibernetika (Kiev), no. 4 (1966), 1–17 (the source's reference [24]).
• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223

Motivation

Gradient methods assume a continuous gradient; subgradient methods assume convexity. Many objective functions met in practice satisfy neither. Shor's example is economic planning, where components of the objective are piecewise-smooth, not necessarily convex functions of a parameter describing the productivity of a unit, and where minimax formulations produce kinks as a rule (Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, §1.4, p. 17, DOI 10.1007/978-3-642-82118-9). Such problems need a class of functions wide enough to contain piecewise-smooth and minimax functions and narrow enough to carry a usable replacement for the gradient.

Shor's answer is the class of almost differentiable functions, introduced in his 1972 work and presented in §1.4 of the book, together with the almost-gradient, a limit of gradients taken at nearby points of differentiability. The capstone of the section, Theorem 1.15, connects this class with convex analysis: every convex function on $E_n$ is almost differentiable, and its almost-gradients are subgradients. This is what lets the later chapters treat convex minimization and almost-differentiable minimization with one set of tools. Clarke's generalized gradient of locally Lipschitz functions (Clarke 1975) is the closest relative; Shor's definition differs in requiring the gradient to be continuous on its domain (p. 19).

Setting

Let $E_n$ denote $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. For $f : E_n \to \mathbb{R}$, write $M = \{x \in E_n : f \text{ is differentiable at } x\}$ and $\nabla f(x)$ for the gradient at $x \in M$.

A function $f$ is almost differentiable if

1. on every bounded set $S$ it is Lipschitz: $|f(x) - f(y)| \le L_S \|x - y\|$ for $x, y \in S$, with a constant $L_S$ depending on $S$;
2. it is differentiable at Lebesgue-almost every point of $E_n$;
3. the map $x \mapsto \nabla f(x)$, restricted to $M$, is continuous.

An almost-gradient of $f$ at $x_0$ is a vector $g$ that is an accumulation point of a sequence $\nabla f(x_1), \nabla f(x_2), \dots$ with $x_k \in M$ and $x_k \to x_0$. The set of almost-gradients is $G(x_0)$. A generalized almost-gradient is a point of the closure of the convex hull of $G(x_0)$.

A vector $g$ is a subgradient of $f$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x \in E_n$; for convex $f$ the set of subgradients is the subdifferential $G_f(x_0)$.

In Lean these objects are AlmostDifferentiable f, almostGradients f x₀ and IsSubgradient f x₀ g in the namespace ShorNonsmooth.AlmostDiff, with $E_n$ = EuclideanSpace ℝ (Fin n).

Formalization targets

Goal: Theorem 1.15 (p. 18)

For convex $f : E_n \to \mathbb{R}$,

$$f \text{ is almost differentiable} \quad\text{and}\quad G(x_0) \subseteq G_f(x_0) \ \text{ for every } x_0 \in E_n .$$

The printed statement says the almost-gradients "coincide with" the subgradients. As a set equality this is false (for $f(x) = |x|$ on $E_1$, $G(0) = \{-1, 1\}$ while $G_f(0) = [-1, 1]$), and the book's proof establishes the inclusion. The goal is the inclusion.

Milestones

1. Proof of Theorem 1.15, display (p. 18). For convex $f$ differentiable at $x_k$: $f(x) - f(x_k) \ge (\nabla f(x_k), x - x_k)$ for all $x$.
2. Proof of Theorem 1.15 (p. 18). For convex $f$ and bounded $S$ there is $C$ with $|f'_v(x)| \le C\|v\|$ for all $x \in S$ and all $v$, the one-sided directional derivatives existing.
3. Proof of Theorem 1.15 (p. 18). A convex $f$ is differentiable almost everywhere and $\nabla f$ is continuous on $M$.
4. Theorem 1.14 (p. 18). For almost differentiable $f$, $G(x)$ is nonempty, bounded and closed at every $x$.
5. p. 19. For almost differentiable $f$, $\overline{\operatorname{conv}}\, G(x)$ is convex, bounded and closed.

Significance

The result. Theorem 1.15 embeds convex functions into the almost differentiable class and identifies each almost-gradient of a convex function as a subgradient. Consequently any method that only needs almost-gradients (limits of gradients at nearby differentiable points, which is what a numerical procedure can actually compute) produces valid subgradients when applied to a convex function. Theorem 1.14 supplies the compactness that makes $G(x)$ usable as a set-valued substitute for the gradient.

Formalizing it. All results here are classical and proved on paper. Mathlib contains Rademacher's theorem for Lipschitz functions (LipschitzWith.ae_differentiableAt) and local Lipschitz continuity of convex functions on open sets; it does not contain the continuity of the gradient of a convex function on its domain of differentiability, nor any notion of almost-gradient. The mission produces those, together with a formal record that the printed "coincide" is an inclusion. A formal proof of the true equality $G_f(x_0) = \overline{\operatorname{conv}}\, G(x_0)$ would be a welcome further contribution.

Difficulty

Two parts of the goal carry real content. The first is condition (c): the gradient of a convex function, restricted to the set where it exists, is continuous. The book cites this from the literature; it is not a consequence of Rademacher's theorem, which gives differentiability almost everywhere and says nothing about how gradients at nearby points relate. The second is condition (b) in a form Lean accepts: Rademacher's theorem in Mathlib is stated for globally Lipschitz functions, while a convex function on $E_n$ is only Lipschitz on bounded sets, so the almost-everywhere statement has to be assembled from local pieces. The passage from gradients to subgradients in the second conjunct is comparatively routine.

The analogous closure properties claimed on the same pages for sums, products and maxima of almost differentiable functions (Theorems 1.16 and 1.17) are false as printed and are not targets; see the formalization scope.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $n = 0$ is allowed and harmless. Functions are total and real-valued; convexity is ConvexOn ℝ Set.univ f.
• The gradient is Mathlib's gradient f x; condition (c) is ContinuousOn (gradient f) {x | DifferentiableAt ℝ f x}, continuity of the restriction in the subspace topology.
• Condition (a) is quantified over every bounded set with a set-dependent constant: ∀ S, Bornology.IsBounded S → ∃ L, LipschitzOnWith L f S. Condition (b) is ∀ᵐ x ∂volume, DifferentiableAt ℝ f x.
• An almost-gradient is a cluster point (MapClusterPt) of the gradient sequence, not its limit; the points $x_k$ may equal $x_0$.
• Subgradients are taken relative to the whole space, the domain of every function in this mission.
• The goal states the inclusion $G(x_0) \subseteq G_f(x_0)$ proved in the book. Stating the printed set equality would make the goal false; weakening the first conjunct to "locally Lipschitz and differentiable almost everywhere" would drop condition (c) and with it the substance of the theorem. Neither is acceptable.
• Theorem 1.16 (sums, differences, products) and Theorem 1.17 (maxima) are omitted: both are false for the class as defined. With $h(x) = x^2 \sin(1/x)$, the functions $h + |x|$ and $-|x|$ are almost differentiable but their sum $h$ is differentiable everywhere with a derivative discontinuous at $0$; and $\max(h - |x|,\, h - |x| + 2x) = h + x$. Theorem 1.18 (Mifflin's superposition theorem for semismooth functions) is cited from the literature without proof and rests on Clarke's generalized gradient; it is outside this mission.

Infrastructure that is reusable beyond this mission: continuity of the gradient of a convex function on its domain; Rademacher's theorem for locally Lipschitz functions on $E_n$; the almost-gradient set and its compactness. Contributions that prove these as standalone lemmas are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 25.5 (continuity of the gradient of a convex function). https://doi.org/10.1515/9781400873173
• F. H. Clarke, Generalized gradients and applications, Transactions of the American Mathematical Society 205 (1975), 247–262. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• H. Rademacher, Über partielle und totale Differenzierbarkeit von Funktionen mehrerer Variabeln und über die Transformation der Doppelintegrale, Mathematische Annalen 79 (1919), 340–359. https://doi.org/10.1007/BF01498415

Motivation

Service parts networks (spare parts for aircraft, military systems, industrial equipment) hold stock at several echelons: a depot, intermediate stocking facilities, and bases or warehouses that face demand. Two questions recur in their planning. First, how should a given amount of stock be split among locations whose expected costs are convex in the stock they hold? Second, does adding an echelon, a depot that pools the demand of several warehouses, raise or lower the stock the system needs?

Chapter 7 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879), treats both. For the second it follows Eppen and Schrage (1981, reference [78] of the book): with normal demands, a depot that places orders every period and allocates stock so that all warehouses face the same stockout probability reduces the choice of system stock to a single critical-fractile equation. For the first, the chapter's multi-echelon pooling model (Section 7.3) evaluates nested cost functions of the form "holding and shortage cost plus the minimum over allocations of a sum of convex costs", and its appendix (Section 7.4) gives the marginal allocation algorithm AllocOpt that computes these minima exactly for every stock level at once.

Marginal analysis for separable convex resource allocation is classical (Fox, Management Science, 1966); the monograph of Ibaraki and Katoh (MIT Press, 1988) surveys it.

Setting

Allocation data (Section 7.4). There is a set $M = \{1, \dots, \bar M\}$ of locations and an augmented set $M_0 = \{0\} \cup M$. Each location $m \in M_0$ has integer gridpoints $0 = r^m_0 < r^m_1 < \dots < r^m_{n(m)}$. For $m \in M$, the value $c^m_n$ of a convex function is given at each gridpoint. The slopes (7.19) are $\hat c^m_n = (c^m_{n+1} - c^m_n)/(r^m_{n+1} - r^m_n)$ for $n < n(m)$, and $\hat c^m_{n(m)}$ repeats the last one. The piecewise linear approximation $\tilde C_m$ of (7.20)–(7.21) interpolates the values $c^m_n$ at the gridpoints and continues with slope $\hat c^m_{n(m)}$ beyond the last one. A convex function $f$ on $\mathbb R_+$ is also given.

The allocation optimization (7.22) asks, for each $n \in N_0 = \{0, \dots, n(0)\}$, for

$$c^0_n = f(r^0_n) + \min\Bigl\{ \sum_{m \in M} \tilde C_m(r_m) : r_m \ge 0 \text{ integer},\ \sum_{m \in M} r_m = r^0_n \Bigr\}.$$

Algorithm AllocOpt (Definition 4) keeps a current gridpoint index $n^*(m)$ and allocation $r^*(m)$ per location. For each increment $r^0_n - r^0_{n-1}$ of the target, it repeatedly gives units to a location $m^*$ whose current slope $\hat c^{m^*}_{n^*(m^*)}$ is minimal, up to that location's next gridpoint, and records the accumulated cost.

Pooling system (Section 7.2.1). One depot supplies $m$ warehouses. The demand $d_{jt}$ at warehouse $j$ in period $t$ is normal with mean $\mu_j$ and variance $\sigma_j^2$, independent across periods and warehouses. The supplier-to-depot lead time is $D$ periods, the depot-to-warehouse lead time $A$ periods, and holding and backorder costs $h, b$ are equal at all warehouses. Positions $I_j$ are in balance when $\Phi((I_j - A\mu_j)/(\sqrt A\,\sigma_j))$ is the same for all $j$. For system inventory position $s$, with $Y_0$ the system demand over $D$ periods and $Y_j$ the demand at $j$ over the next $A + 1$ periods, the balanced allocation gives each warehouse a share proportional to $\sigma_j$, and $z_j$ is its end-of-period net inventory.

Formalization targets

Goal: Proposition 2 (correctness)

For every tie-breaking rule in its arg min steps, AllocOpt returns values $c^0_n$ that satisfy (7.22) for every $n \in N_0$: some feasible integer allocation attains $c^0_n - f(r^0_n)$, and no feasible integer allocation does better.

Milestones

1. Slope monotonicity (p. 178): $\hat c^m_n \ge \hat c^m_{n-1}$ for $0 < n \le n(m)$.
2. Convexity of $\tilde C_m$ on $[0, \infty)$ (proof of Proposition 2, p. 179).
3. Remark 2 (p. 179): with the inner loop run only while the current slope is $\le 0$, AllocOpt solves (7.22) with $\sum_m r_m \le r^0_n$.
4. Lemma 3 (p. 152): if the positions are in balance and

$$\sum_{j} d_{j,t-1} \ge \max_{i} \Bigl\{ \sum_{j \ne i} d_{j,t+D-1} + d_{i,t+D-1}\Bigl(1 - \frac{\sum_j \sigma_j}{\sigma_i}\Bigr)\Bigr\},$$

then a nonnegative allocation of the arriving $\sum_j d_{j,t-1}$ units restores balance. 5. Net inventory law (pp. 156–157): $z_j$ is normal with mean $(s - (D + A + 1)\sum_i \mu_i)\,\sigma_j / \sum_i \sigma_i$ and variance $(A + 1)\sigma_j^2 + (\sigma_j / \sum_i \sigma_i)^2 D \sum_i \sigma_i^2$. 6. Critical fractile (pp. 157–158): $s$ minimizes $\sum_j E[h (z_j)^+ + b (z_j)^-]$ if and only if $\Phi(z) = b/(b+h)$, where

$$z = \frac{s - (D + A + 1)\sum_i \mu_i}{\bigl[(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2\bigr]^{1/2}}.$$

Significance

The goal certifies an algorithm that the chapter uses as a subroutine three times: in the pool cost (7.14), the subsystem cost (7.15) and the system cost (7.17), and hence in the claim of Section 7.3 that the system-wide cost function can be computed in time $n \log n$ in the number of locations. Because AllocOpt produces the whole vector $(c^0_n)_{n \in N_0}$ in one pass, its correctness gives the nested value functions at every gridpoint of the next echelon, which is what allows the recursion up the echelons. The Eppen–Schrage milestones give the classical quantitative form of risk pooling: the system stock is set by one critical fractile, and the standard deviation term $(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2$ is what the book compares with the single-warehouse and the decentralized systems.

On formalization: the book states Proposition 2 with a two-sentence argument and Remark 2 without proof. The Eppen–Schrage computations are displayed derivations. None of these results has a machine-checked proof on the platform. A verified AllocOpt, stated for an explicit algorithm rather than for an abstract greedy procedure, is reusable for any separable convex integer allocation with a sum constraint.

Difficulty

The usual greedy exchange argument assumes that units are allocated one at a time. AllocOpt allocates in blocks, up to the next gridpoint of the chosen location, and it carries its state across successive targets $r^0_{n-1} \to r^0_n$ without restarting. The proof must therefore show that the state after each outer step is itself an optimal allocation for the current target, and that block moves never step past a breakpoint where the arg min would change. The slopes can be negative, and the equality constraint forces allocation even when every marginal cost is positive. Remark 2 needs an additional argument: under the inequality constraint the loop may stop before $u$ reaches zero, and that point is optimal only because the slopes are nondecreasing.

For the pooling results, the balanced allocation mixes the depot-lead-time demand $Y_0$ of all warehouses with the local demand $Y_j$, and the Gaussian law of $z_j$ rests on the independence of disjoint blocks of periods. The fractile statement requires strict monotonicity of each warehouse's expected cost derivative in $s$, not only a first-order condition.

Formalization scope

• Indices and types. Locations of $M$ are Fin Mbar; gridpoints are integers, values and slopes real numbers; allocations are functions Fin Mbar → ℕ. The standing assumptions of Section 7.4 form the predicate WellFormed: $\bar M \ge 1$, $n(m) \ge 1$ for $m \in M$ (a slope (7.19) needs two gridpoints), gridpoints starting at $0$ and strictly increasing at every location of $M_0$, each $c^m_n$ the value of a function convex on $[0, \infty)$, and $f$ convex on $[0, \infty)$.
• The minimum in (7.22) is stated as attainment plus a lower bound over the finite, nonempty set of feasible integer allocations, never as an unconstrained infimum.
• Ties. The book's arg min fixes no tie-breaking rule. Results are stated for every selection rule that returns a minimizing location.
• Termination. AllocOpt is a total Lean function. The inner loop is given more passes than it can use, so it always exits through its own condition.
• Not stated. The operation count of Proposition 2, $O((1 + \log_2 \bar M)\sum_{m \in M_0} n(m))$, and Proposition 1 and Remark 1 (p. 177) are operation counts with no machine model and are left out.
• Corrections. The first expected-cost display on p. 157 has $+\,b\int_{-\infty}^0 z\,dF_{z_j}(z)$, which is negative. The formalization uses $b\,E[(z_j)^-]$, as in the book's next display.
• Pinnings. Lemma 3 is deterministic: the demands are arbitrary reals, and "in balance following the allocation" means that some $x_j \ge 0$ with $\sum_j x_j = \sum_j d_{j,t-1}$ exists. The critical-fractile milestone is the characterization "minimizer if and only if $\Phi(z) = b/(b+h)$" of the book's "can be found by setting".
• Trivialization ruled out. The allocation problem (7.22) is defined independently of the algorithm, as a minimum over explicit integer allocations, and the $\tilde C_m$ are built from the data by (7.19)–(7.21). Neither (7.22) nor the $\tilde C_m$ are defined as, or required to agree with, what AllocOpt returns.
• Welcome contributions. Lemmas on the invariants of AllocOpt, in particular that after each outer step the allocation $r^*$ is feasible for $r^0_n$ with cost $z$ and all slopes to the left of $n^*(m)$ are at most those to the right. Also Gaussian sum lemmas over finite index sets and a general newsvendor first-order characterization.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005. DOI 10.1007/b138879
• G. D. Eppen and L. Schrage, "Centralized ordering policies in a multi-warehouse system with lead times and random demand", in L. B. Schwarz (ed.), Multi-Level Production/Inventory Control Systems: Theory and Practice, Studies in the Management Sciences, North-Holland, Amsterdam, 1981, pp. 51–67.
• G. D. Eppen, "Effects of centralization on expected costs in a multi-location newsboy problem", Management Science 25(5), 1979, 498–501. DOI 10.1287/mnsc.25.5.498
• B. Fox, "Discrete optimization via marginal analysis", Management Science 13(3), 1966, 210–216. DOI 10.1287/mnsc.13.3.210
• T. Ibaraki and N. Katoh, Resource Allocation Problems: Algorithmic Approaches, MIT Press, 1988.

Motivation

Many optimization problems in operations research have an objective that is an expectation, $F^0(x)=E f^0(x,\omega)$, over a random parameter $\omega$ whose distribution is known only through samples or is too complex to integrate. Two-stage stochastic programs, inventory and reliability models, and simulation-based design all have this form. Neither $F^0$ nor its subgradients can be evaluated exactly, but a random vector whose conditional mean is close to a subgradient is often cheap to compute: a sample subgradient of $f^0(\cdot,\omega)$, or a finite-difference quotient of two sampled values.

Stochastic quasigradient (SQG) methods, developed by Ermoliev and co-workers in Kiev from the late 1960s, use such vectors in place of subgradients. They extend the stochastic approximation procedures of Robbins–Monro (1951) and Kiefer–Wolfowitz (1952) to nonsmooth convex objectives, general convex constraints, and directions whose conditional mean is biased by a vanishing amount. This mission formalizes the basic convergence theory of the simplest SQG method, the projection method, as presented by Yu. Ermoliev in Chapter 6 of the IIASA volume Numerical Techniques for Stochastic Optimization (Springer 1988).

Timeline (as cited in the chapter's bibliography).

• 1951–1954: Robbins and Monro, Kiefer and Wolfowitz, Dvoretzky and Blum prove convergence of stochastic approximation for unconstrained smooth problems.
• 1962–1967: Shor introduces the generalized gradient (subgradient) method; Ermoliev (Kibernetika 4, 1966) and Polyak (Soviet Math. Doklady 8, 1967) prove its convergence.
• 1967–1969: Ermoliev and Nekrylova introduce stochastic subgradients; Ermoliev ("On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2, 1969) introduces stochastic quasi-Féjer sequences.
• 1976: Ermoliev's monograph Stochastic Programming Methods (Nauka) contains the proof of Theorem 6.1 (p. 98).
• 1988: the survey chapter formalized here presents the projection method, Theorems 6.1 and 6.2, and an efficiency estimate for the averaged iterate.

Setting

Let $X\subseteq\mathbb R^n$ be a nonempty convex compact set and $F^0:\mathbb R^n\to\mathbb R$ convex and continuous on $X$. The optimal set is $X^*=\{x\in X: F^0(x)\le F^0(y)\ \forall y\in X\}$. The projection onto $X$ is $\pi_X(y)=\operatorname{argmin}\{\|y-x\|^2:x\in X\}$.

On a probability space, the stochastic quasigradient projection method produces random vectors $x^0,x^1,\dots$ by

$$x^{s+1}=\pi_X\big[x^s-\rho_s\,\xi^0(s)\big],\qquad s=0,1,\dots \tag{6.11}$$

where $\rho_s\ge0$ is a step size and $\xi^0(s)$ a random direction. Write $E\{\cdot\mid x^0,\dots,x^s\}$ for conditional expectation given the history $\sigma(x^0,\dots,x^s)$. The direction is a stochastic quasigradient if, for every $x^*\in X^*$,

$$F^0(x^*)-F^0(x^s)\ge\big\langle E\{\xi^0(s)\mid x^0,\dots,x^s\},\,x^*-x^s\big\rangle+\gamma_0(s)\quad\text{a.s.}, \tag{6.12}$$

where the error $\gamma_0(s)$ is a function of the history. If the conditional mean of $\xi^0(s)$ is a subgradient plus a bias $b^0(s)$, then (6.12) holds with $\gamma^0(s)=-\langle b^0(s),x^*-x^s\rangle$ (6.13).

A sequence of random vectors $z^0,z^1,\dots$ is a stochastic quasi-Féjer sequence for $Z\subseteq\mathbb R^n$ if $E\|z^0\|^2<\infty$ and there are random $r_s\ge0$ with $\sum_s E r_s<\infty$ such that for all $z\in Z$

$$E\{\|z-z^{s+1}\|^2\mid z^0,\dots,z^s\}\le\|z-z^s\|^2+r_s. \tag{6.14}$$

Formalization targets

Goal: Theorem 6.2

If, with probability 1, $\rho_s\ge0$ and $\sum_s\rho_s=\infty$, and

$$\sum_{s=0}^\infty E\{\rho_s|\gamma_0(s)|+\rho_s^2\|\xi^0(s)\|^2\}<\infty, \tag{6.15}$$

then with probability 1 the iterates converge and $\lim_s x^s\in X^*$.

Milestones

1. Theorem 6.1 (a)–(c). For a stochastic quasi-Féjer sequence for $Z$: $\|z-z^{s+1}\|^2$ converges a.s. and $E\|z-z^s\|^2$ is bounded, for each $z\in Z$; accumulation points exist a.s. (for $Z\ne\emptyset$); and a.s. $Z$ lies in the hyperplane equidistant from any two distinct accumulation points outside $Z$.
2. Eq. (6.13). Biased stochastic subgradients satisfy (6.12).
3. One-step inequality (p. 145): $E\{\|x^*-x^{s+1}\|^2\mid\cdot\}\le\|x^*-x^s\|^2+2\rho_s\langle E\{\xi^0(s)\mid\cdot\},x^*-x^s\rangle+E\{\rho_s^2\|\xi^0(s)\|^2\mid\cdot\}$ for $x^*\in X$.
4. Quasi-Féjer property (p. 145): the iterates of (6.11) form a stochastic quasi-Féjer sequence for $X^*$.
5. Efficiency estimate (p. 147), for deterministic $\rho_k$ and $\bar x^s=\sum_{k\le s}\rho_kx^k/\sum_{k\le s}\rho_k$:

$$E F^0(\bar x^s)-F^0(x^*)\le\Big(2\sum_{k=0}^s\rho_k\Big)^{-1}\Big[E\|x^*-x^0\|^2+\sum_{k=0}^s E\big(2\rho_k|\gamma_0(k)|+\rho_k^2\|\xi^0(k)\|^2\big)\Big].$$

Significance

Theorem 6.2 is the prototype convergence theorem for SQG methods. Its hypotheses allow random step sizes chosen from the history, nonsmooth objectives, and directions with a bias that vanishes fast enough; its conclusion is convergence of the iterates themselves to a single optimal point, not only convergence of function values or of $\operatorname{dist}(x^s,X^*)$. The later chapters of the same volume (adaptive step sizes, Chapters 17–18; nonstationary problems, §6.4) reuse the same framework. Theorem 6.1 isolates the probabilistic content in a form that applies to any algorithm with a quasi-Féjer inequality. The efficiency estimate gives a non-asymptotic accuracy bound for the averaged iterate.

The results are classical and proved in the literature: Theorem 6.1 in Ermoliev (1976, p. 98), Theorem 6.2 in this chapter (pp. 145–146). To our knowledge none of them has a machine-checked proof. Mathlib has conditional expectations and the a.s. martingale convergence theorem, but no Robbins–Siegmund-type almost-supermartingale lemma and no stochastic subgradient method. A formal proof of this mission would supply both.

Difficulty

The deterministic argument for projected subgradient methods compares $\|x^*-x^{s+1}\|$ with $\|x^*-x^s\|$ for a fixed $x^*$. In the stochastic setting this comparison holds only in conditional mean, with a perturbation $r_s$ that is random, and the distances converge only almost surely, with an exceptional null set that depends on $x^*$. Since $X^*$ is typically uncountable, "for every $x^*$, almost surely" does not immediately give "almost surely, for every $x^*$", and it is the second form that identifies a single limit. A second difficulty is that $\sum\rho_s(F^0(x^s)-F^0(x^*))<\infty$ only yields a subsequence along which $F^0$ approaches its minimum; passing from there to convergence of the whole sequence is exactly what part (c) of Theorem 6.1 is for.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The probability space is an arbitrary measurable space with a probability measure. $\pi_X$ is a chosen minimizer of $\|y-x\|^2$ over $X$ (unique for nonempty closed convex $X$). The history is the $\sigma$-algebra generated by $x^0,\dots,x^s$; $\rho_s$ and $\gamma_0(s)$ are measurable with respect to it.
• Directions $\xi^0(s)$ are integrable and random vectors are measurable; conditional expectations are Mathlib's condExp. The quasi-Féjer definition requires square integrability of every $z^s$ (implied by the book's definition when $Z\ne\emptyset$), so no conditional expectation is taken of a non-integrable function.
• $X\ne\emptyset$ and $x^0\in X$ are stated; $Z\ne\emptyset$ is added in Theorem 6.1 (b), which is false without it.
• $\gamma_0(s)$ does not depend on $x^*$; the $x^*$-dependent error of (6.13) is dominated on a bounded $X$ by $\|b^0(s)\|\operatorname{diam}X$.
• (6.15) keeps its mixed form: $\rho_s\ge0$ and $\sum\rho_s=\infty$ almost surely, and a deterministic sum of expectations (lower Lebesgue integrals) finite.
• Explicit constants. The book's "$C$" in the efficiency estimate is instantiated from its proof: $2$ on $\rho_k|\gamma_0(k)|$ and $1$ on $\rho_k^2\|\xi^0(k)\|^2$. The unspecified $C$ before the quasi-Féjer sentence is replaced by the existence of summable $r_s$.
• Typo corrections. The one-step inequality on p. 145 prints $\rho_sE\{\|\xi^0(s)\|^2\mid\cdot\}$; it is $\rho_s^2$. The efficiency estimate on p. 147 omits $E$ before the last sum; it is restored. "$\rho_k$ independent of $(x^0,\dots,x^k)$" is read as deterministic step sizes.
• A trivializing formalization is excluded: the goal does not replace $\xi^0(s)$ by an exact subgradient, does not set $\gamma_0\equiv0$, and concludes convergence of $x^s$ to a point of $X^*$ rather than $\operatorname{dist}(x^s,X^*)\to0$.
• Reusable infrastructure: a Robbins–Siegmund lemma for nonnegative almost-supermartingales, the nonexpansiveness of $\pi_X$, and Theorem 6.1 itself, which applies to any quasi-Féjer algorithm (Chapter 6 §6.4 and Chapters 17–18 of the same book). Contributions of these general lemmas are welcome.

Selected references

• Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, §6.1–6.2 (pp. 141–147). https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, "On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2 (1969) (in Russian; English translation in Cybernetics). Reference [3] of the chapter.
• Yu. Ermoliev, Stochastic Programming Methods, Nauka, Moscow, 1976 (in Russian); Theorem 6.1 is on p. 98. Reference [5] of the chapter.
• H. Robbins and D. Siegmund, "A convergence theorem for non negative almost supermartingales and some applications", in J. S. Rustagi (ed.), Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• H. Robbins and S. Monro, "A stochastic approximation method", Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586