Convex Optimization

Motivation

Consider a decision maker who must choose, at each of $T$ rounds, between two actions on the advice of $N$ "experts," none of which is known in advance to be reliable. This is the prediction-from-expert-advice problem, introduced by Littlestone and Warmuth [Littlestone & Warmuth, The Weighted Majority Algorithm, FOCS 1989/Inf. Comput. 1994] and generalized to real-valued losses by Freund and Schapire's Hedge algorithm [Freund & Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, JCSS 1997]. It is one of the two founding problems of online learning (the other being universal portfolio selection, also introduced in this book's first chapter) and the historical origin of the multiplicative-weights update method, later recognized as a single algorithmic idea underlying results across game theory, optimization, and computational complexity [Arora, Hazan & Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 2012]. This mission formalizes the chapter's three central guarantees: a matching deterministic lower bound, the Weighted Majority mistake bound, and Hedge's loss bound — the earliest instance, in the book's own development, of the "online convex optimization" phenomenon that its later chapters generalize to arbitrary convex losses.

Setting

At each round $t = 1, \dots, T$, a decision maker chooses one of two actions, $A$ or $B$. After the choice, the true outcome for that round is revealed, and any action that disagrees with it is charged a mistake. $N$ experts also each commit to a prediction every round, and the decision maker may consult their record.

The Weighted Majority (WM) algorithm maintains a weight $W_t(i)$ for each expert $i$, initialized to $W_1(i) = 1$. It predicts whichever action currently carries at least half the total weight, and after seeing the outcome, multiplies the weight of every expert who erred by $(1-\varepsilon)$ for a fixed parameter $\varepsilon \in (0, 1/2)$, leaving correct experts' weights unchanged. $M_T$ denotes the algorithm's own mistake count through round $T$, and $M_T(i)$ expert $i$'s.

The Randomized Weighted Majority (RWM) algorithm uses the same weights, but instead of following the majority it samples an expert with probability proportional to its weight, $p_t(i) = W_t(i) / \sum_j W_t(j)$, and follows that expert's prediction; $\mathbb E[M_T]$ is its expected mistake count.

Hedge generalizes further, from binary mistakes to arbitrary non-negative real-valued losses $\ell_t(i) \ge 0$ suffered by expert $i$ at round $t$. It samples expert $i_t$ with probability $x_t(i) = W_t(i)/\sum_j W_t(j)$ from weights updated multiplicatively in the loss, $W_{t+1}(i) = W_t(i) \, e^{-\varepsilon \ell_t(i)}$. Writing losses and the mixed strategy as vectors, the algorithm's expected loss at round $t$ is $x_t^\top \ell_t$.

Formalization targets

Goal — Theorem 1.5 (Hedge's loss bound)

where $\ell_t^2(i) := \ell_t(i)^2$. This is the chapter's most general result and the one the book reuses later on; it leaves $\varepsilon$ free (no asymptotic tuning), so it survives whatever later chapters do with $\varepsilon$.

Milestones

• Theorem 1.1 (deterministic lower bound). With $L \le T/2$ the best expert's mistake count, no deterministic algorithm can guarantee fewer than $2L$ mistakes on every instance.
• Lemma 1.3 (Weighted Majority): $M_T \le 2(1+\varepsilon) M_T(i) + 2\log N/\varepsilon$ for every expert $i$.
• Lemma 1.4 (Randomized Weighted Majority): $\mathbb E[M_T] \le (1+\varepsilon) M_T(i) + \log N /\varepsilon$ for every expert $i$.

Significance

Theorem 1.1 shows the mistake-bound question has no trivial answer: even against only two maximally simple experts, any deterministic strategy is beaten by a factor of $2$ by an adversary who knows its code. Lemmas 1.3 and 1.4 show this factor is essentially removable — first by relaxing "guarantee" to "guarantee in expectation" (RWM halves the deterministic penalty from $2(1+\varepsilon)$ to $(1+\varepsilon)$), then Theorem 1.5 removes the binary-mistake restriction altogether, replacing it with an explicit second-moment correction term $\varepsilon \sum_t x_t^\top \ell_t^2$ that vanishes as losses shrink. Together they trace the chapter's own narrative arc from "no algorithm beats $2L$" to "an explicit, parameter-free family of algorithms gets within $(1+\varepsilon)$ of the best expert for any $\varepsilon$." All four results are proved by the book via the same device — a potential function $\Phi_t = \sum_i W_t(i)$ — one of the first instances of the potential-function method that recurs throughout the rest of the book (e.g. Online Gradient Descent's regret proof) and throughout online learning generally. None of these four statements, in this exact form, has a formalized proof on Prove2Me or (to the extent searchable) elsewhere: the platform's closest existing result, BanditAlgorithm.ftrl_simplex_exp_weights_regret (see Formalization scope below), proves an asymptotically similar bound by an entirely different route and under a different loss model.

Difficulty

The natural first attempt at any of these bounds is to track $M_T$ (or $\mathbb E[M_T]$, or $\sum_t x_t^\top \ell_t$) directly and induct on $T$; this fails because the quantity itself has no useful recursive structure — knowing the algorithm's mistake count through round $t$ says nothing about round $t+1$'s outcome, which the adversary chooses to inflict maximum damage. The proofs instead introduce an auxiliary potential $\Phi_t = \sum_i W_t(i)$ that is not the quantity being bounded, track it in two directions — an upper bound in terms of the algorithm's own performance (using $1+x \le e^x$, or, for Hedge, $e^{-x} \le 1-x+x^2$ for $x \ge 0$) and a lower bound via the single best expert's weight, $W_T(i^\star) \le \Phi_T$ — and only convert back to the mistake/loss bound at the very end via one logarithm. Getting the direction of every inequality right (each of the four proofs chains four or five inequalities, each valid only in the stated parameter range) is the entire difficulty; there is no shortcut that avoids introducing $\Phi_t$.

Formalization scope

Each algorithm is represented as a Prop-valued run predicate parametrizing over the weight sequence, the input (expert predictions/losses and true outcomes), and the algorithm's own output (predictions or mixed strategy), rather than as an executable program: IsHedgeRun fixes W 0 i = 1, the update W (t+1) i = W t i * exp(-ε * ℓ t i), and x t i = W t i / ∑ j, W t j; IsWeightedMajorityRun additionally fixes the majority-vote prediction rule explicitly (per the triage rubric, the algorithm is part of the audited statement here, not a black box the proof is free to instantiate). Randomization in RWM and Hedge is captured exactly as the book itself does — as a deterministic expectation, i.e. the inner product of the probability vector with the {0,1}-mistake or loss vector — rather than as a measure-theoretic random variable; the book's own Section 1.3.3 makes this identification explicit ("denote in vector notation the expected loss of the algorithm by $\mathbb E[\ell_t(i_t)] = x_t^\top \ell_t$"), so no probability space is introduced. Theorem 1.1's "deterministic algorithm" is a causal map from an outcome history to a prediction (prediction at round $t$ depends only on outcomes before $t$), instantiated at the book's own two-expert construction (one expert always predicts $A$, the other always $B$) rather than a fully general $N$-expert adversary argument — a strictly weaker instance of the general claim, but the exact one the book's proof establishes, so no scope is lost relative to what is proved. $\varepsilon$ is kept as an explicit free parameter throughout, per the book's own presentation (no substitution of the corollary's optimized $\varepsilon^\star = \sqrt{\log N / M_T(i^\star)}$ into the milestone statements).

A trivializing formalization to rule out: fixing $N = 1$ (a single expert) would make Lemmas 1.3–1.5 hold vacuously with $M_T = M_T(i)$ regardless of the potential-function argument; every formal statement here quantifies over an unconstrained $N : \mathbb N$ with $N > 0$, not a hard-coded small case.

The mission needs no Mathlib infrastructure beyond finite sums, Real.log, and Real.exp; the book's own OCO protocol and regret definition (§1.1) are not needed, since this chapter's proofs work directly with mistake/loss counts (per the chunk brief). BanditAlgorithm.ftrl_simplex_exp_weights_regret (Bandit Algorithms XII, Prop. 28.7, arXiv:2003.05963 §28) proves $R_n \le \sqrt{2n\log d}$ for exponential weights on the simplex against $[0,1]$-valued losses, via an FTRL/mirror-descent instantiation — the same asymptotic phenomenon as Theorem 1.5, but a different proof technique, a different (bounded, not merely non-negative) loss assumption, and stated for simplex-comparator regret rather than the per-expert loss comparator here; it is listed as a reference/comparison point, not reused.

Selected references

• N. Littlestone, M. Warmuth, The Weighted Majority Algorithm, FOCS 1989 / Information and Computation 108(2), 1994. https://doi.org/10.1006/inco.1994.1009
• Y. Freund, R. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, Journal of Computer and System Sciences 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
• S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8(1), 2012. https://doi.org/10.4086/toc.2012.v008a006
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter
  1. https://arxiv.org/abs/1909.05207

Motivation

Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables $x$) followed by a corrective decision made after (the second-stage, or recourse, variables $y$). Solving such a program means minimizing $c^{\mathsf T}x + Q(x)$, where $Q(x)$ is the expected cost of the best recourse action given $x$ -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that $Q$ is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that $Q$ itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.

Setting

Fix natural numbers $n_1, n_2, m_1, m_2$ and a finite scenario count $K$. A two-stage recourse instance consists of first-stage data $A \in \mathbb{R}^{m_1 \times n_1}$, $b \in \mathbb{R}^{m_1}$, $c \in \mathbb{R}^{n_1}$, a fixed recourse matrix $W \in \mathbb{R}^{m_2 \times n_2}$, and, for each scenario $k = 1,\dots,K$, a cost vector $q_k \in \mathbb{R}^{n_2}$, a right-hand side $h_k \in \mathbb{R}^{m_2}$, a technology matrix $T_k \in \mathbb{R}^{m_2 \times n_1}$, and a probability $p_k \ge 0$ with $\sum_k p_k = 1$ (Eq. (1.1)). The first-stage feasible region is $K_1 = \{x \mid Ax = b,\ x \ge 0\}$.

For a fixed $x$ and scenario $k$, the second-stage value is

(Eq. (1.6)), taken as an extended real: $+\infty$ if no feasible $y$ exists, $-\infty$ if the inner program is unbounded below. The expected recourse value is $Q(x) = \sum_k p_k\, Q(x,\xi_k)$ (Eq. (1.3)), combined so that $+\infty + (-\infty) = +\infty$ -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is $K_2 = \{x \mid Q(x) < \infty\}$, and the deterministic-equivalent objective is $z(x) = c^{\mathsf T}x + Q(x)$ (Eq. (1.2)). For $x$ with $Q(x)$ finite, the subdifferential $\partial Q(x)$ is the set of $\eta$ satisfying $Q(x) + \eta^{\mathsf T}(y-x) \le Q(y)$ for every $y$ (p. 115).

A simple-recourse instance is the special case $W = [I,-I]$: the recourse cost splits as $q = (q^+,q^-)$, and $Q(x)$ decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions $F_i^-, F_i^+$ of each $h_i$.

Formalization targets

Goal -- Chapter 3, Theorem 9 (p. 116)

given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of $Q$ (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of $K_2$ (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes "$x^*$ is optimal" a statement about a point that exists rather than an infimum that may not be reached.

Supporting milestones

• Theorem 5(a) (p. 111): $K_2$ is closed and convex.
• Theorem 6(a) (p. 112): $Q$ is finite on $K_2$, and Lipschitzian and convex there.
• Theorem 8 (p. 115): under boundedness of $K_1 \cap K_2$ or eventual linearity of $Q$ along recession directions, a finite optimal value is attained.
• Corollary 10 (p. 116): Theorem 9 specialized to simple recourse, with $\partial Q(x^*)$ replaced by its explicit componentwise description.

Significance

Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of $\partial Q(x)$; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), $c + \nabla Q(x^*) = A^{\mathsf T}\lambda^* + \mu^*$) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing $Q$ is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of $Q$ as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of $Q$, and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.

Difficulty

The obvious shortcut is to treat $Q$ as an opaque convex function and apply a textbook convex-KKT theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the specific function $Q(x) = \sum_k p_k \min_y\{q_k^{\mathsf T}y \mid Wy = h_k - T_k x,\ y \ge 0\}$, built from finitely many parametric linear programs, each of which can be infeasible ($Q(x,\xi_k) = +\infty$) or unbounded ($Q(x,\xi_k) = -\infty$) depending on $x$. Convexity of $Q$ must come from convexity of the value function of a parametric LP in its right-hand side (the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed hypothesis. Handling $\pm\infty$ correctly is a second, easy-to-miss source of error: the book fixes an explicit, non-default convention ($+\infty$ dominates $-\infty$) for combining per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses, so any formalization that reaches for EReal's built-in addition to aggregate $Q$ silently states a different theorem. Theorem 8's attainment condition is a genuine existence result, not an automatic consequence of convexity: continuity alone does not give attainment on an unbounded feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with infimum $0$ attained by no finite $x$) shows the boundedness/recession hypotheses are load-bearing.

Formalization scope

The scenario set is modeled as Fin K, a finite discrete random variable, matching Section 3.1b's development; under this model "$\xi$ has finite second moments" (the standing hypothesis of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is ⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner minimization rather than assumed convex; this rules out the chapter's trivializing formalization, which the paper-level triage explicitly warns against: taking Q(x) as an opaque convex-function hypothesis instead of deriving its properties from the inner LP's structure. Aggregating the $K$ per-scenario values into $Q(x)$ uses a bespoke bookAdd operation implementing the book's stated convention $+\infty+(-\infty)=+\infty$, since Mathlib's EReal addition is defined with the opposite convention ($\bot+\top=\top+\bot=\bot$). $\partial Q(x)$ is the ordinary subgradient-inequality set for this extended-real-valued function.

Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold $\bar\lambda$ and the recession value depend on the point $x$ and direction $v$ exactly as written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the closed form of $\partial Q_i(x)$ from Eq. (1.10) as a hypothesis on an abstract $Q$, matching how the book itself uses (1.10) as an already-established fact rather than re-deriving it from the second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result ($\partial Q(x) = E_\omega[\partial Q(x,\xi(\omega))] + N(K_2,x)$) is deliberately left out of this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces, not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over the specific polyhedral set $K_1$, so none is a faithful match and all items here are original drafts.

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• R.J-B. Wets, "Programming Under Uncertainty: The Equivalent Convex Program," SIAM Journal on Applied Mathematics 14 (1966), 89-105 (Lipschitz continuity of the recourse function, cited by the book as Wets [1972] for the closely related result used in Theorem 6). https://doi.org/10.1137/0114008
• D.P. Walkup and R.J-B. Wets, "Stochastic Programs with Recourse," SIAM Journal on Applied Mathematics 15 (1967), 1299-1314 (finiteness of the recourse function and coincidence of the possibility and expectation feasibility sets, underlying Proposition 3 and Theorem 4). https://doi.org/10.1137/0115113

The classical convergence theory of smooth convex minimization. For a function that is $m$-strongly convex and $M$-smooth ($mI \preceq \nabla^2 f(x) \preceq MI$), gradient descent converges linearly, while Newton's method exhibits its famous two phases: a damped phase in which every backtracking step decreases the objective by a fixed amount $\gamma$, and a quadratically convergent phase in which the scaled gradient norm squares at each step, $\tfrac{L}{2m^2}\lVert \nabla f(x^{+})\rVert_2 \le \bigl(\tfrac{L}{2m^2}\lVert \nabla f(x)\rVert_2\bigr)^2$. Together they give the iteration count of B&V (9.36),

with $L$ the Lipschitz constant of the Hessian and $\alpha,\beta$ the backtracking parameters. This mission formalizes Chapters 9–10 of Boyd & Vandenberghe with every constant exactly as printed — a quantitative theory entirely absent from Mathlib.

The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.

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

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

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

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

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

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

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

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

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

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$,

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

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