Convex Optimization

Motivation

Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.

Timeline:

• 1970: Edmonds proves the polymatroid intersection theorem.
• 1982: Frank proves the discrete separation theorem for submodular/supermodular set functions, with integrality.
• 1984: Fujishige proves a Fenchel-type min-max theorem for submodular functions.
• 1976–1981: Iri and Tomizawa characterize optimality for independent assignment by potentials; Frank proves the weight splitting theorem for weighted matroid intersection (1981).
• Early 1990s: Dress and Wenzel introduce valuated matroids.
• 1995–1996: Murota proves the valuated matroid intersection theorem (SIAM J. Discrete Math. 9, 1996) and the M-concave intersection theorem (Bonn report, 1995), and in the present paper the Fenchel-type duality (Theorem 6.4).
• Later: the result becomes the central duality theorem of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM, 2003).

Setting

Let $V$ be a finite nonempty set. For $u\in V$, $\chi_u\in\mathbb Z^V$ is its characteristic vector; for $x\in\mathbb R^V$, $\operatorname{supp}^{\pm}(x)$ are the sets of coordinates where $x$ is positive or negative, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v\in B$. These are exactly the integer points of integral base polytopes of submodular systems. $\overline B$ is the convex hull of $B$.

A function $\omega:B\to\mathbb R$ has the exchange property (EXC), and is called M-concave, if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and

A function $\zeta$ is M-convex when $-\zeta$ is M-concave.

For $\omega:B_1\to\mathbb R$ and $\zeta:B_2\to\mathbb R$ the concave conjugate and convex conjugate are

and the concave closure and convex closure are $\hat\omega(b)=\inf_p(\langle p,b\rangle-\omega^\circ(p))$ and $\check\zeta(b)=\sup_p(\langle p,b\rangle-\zeta^\bullet(p))$; they are finite exactly on $\overline{B_1}$ and $\overline{B_2}$.

The primal problem maximizes $\omega(x)-\zeta(x)$ over $x\in B_1\cap B_2$; the relaxed primal problem maximizes $\hat\omega(b)-\check\zeta(b)$ over $b\in\overline{B_1}\cap\overline{B_2}$; the dual problem minimizes $\zeta^\bullet(p)-\omega^\circ(p)$ over $p\in\mathbb R^V$. A maximum over an empty family is $-\infty$.

Formalization targets

Goal: Theorem 6.4

If $\omega$ and $-\zeta$ satisfy (EXC), then

with (P1) a finite dual infimum forces $B_1\cap B_2\neq\emptyset$, and (P2) if $B_1\cap B_2\neq\emptyset$ all values are finite and equal and the infimum is attained. If $\omega,\zeta$ are integer-valued, the infimum may be taken over $p\in\mathbb Z^V$ and is attained there when finite.

Milestones

1. Lemma 6.3 (weak duality): for arbitrary $\omega,\zeta$ on finite nonempty sets, primal $\le$ relaxed $=$ dual (the Fenchel identity (6.5)).
2. Lemma 6.1: $(-f)^\circ(p)=-f^\bullet(-p)$ and $(-f)^\wedge=-\check f$ on $\overline B$.
3. Lemma 4.5: an M-concave $\omega$ satisfies $\hat\omega=\omega$ on $B$.
4. Theorem 2.1: (B1) is equivalent to being the integer points of an integral submodular (or supermodular) base polytope, with the describing functions $\max_{x\in B}x(X)$ and $\min_{x\in B}x(X)$.
5. Theorem 6.5 (Frank's discrete separation theorem, cited in the paper).
6. Lemma 6.7: four equivalent forms of boundedness of the dual problem.
7. Theorem 6.6 (the M-concave intersection theorem, cited in the paper): optimality of $x^*$ for $\omega_1+\omega_2$ is equivalent to a potential $p^*$ with $x^*$ maximizing both $\omega_1[-p^*]$ and $\omega_2[p^*]$, integral when the data are.

Significance

The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.

All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.

Difficulty

Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope $\overline{B_1}\cap\overline{B_2}$ must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of $\overline{B_1}\cap\overline{B_2}$ (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that $p$ can be taken integral, is again specific to (EXC) and fails for general concave extensions.

Formalization scope

Lean conventions, all in namespace SteinitzExchange.Duality:

• $V$ is a type with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).
• A function on $B$ is a total (V → ℤ) → ℝ used only at points of $B$. M-convexity of $\zeta$ is (EXC) for fun x => -ζ x; $\omega$ lives on $B_1$ and $\zeta$ on $B_2$, which are distinct sets in general.
• Conjugates are real-valued min/max over the finite set. The closures are real ⨅/⨆ over $p\in\mathbb R^V$ and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of $\mp\infty$, which no statement uses.
• The three optimal values are in EReal, as suprema and infima of coerced reals, so no $\infty-\infty$ occurs. EReal's supremum of the empty family is $-\infty$, the paper's convention. The dual infimum is never a real ⨅ (which would return $0$ when unbounded and make (P1) meaningless).
• Every "max" of the page includes attainment: (P2) asserts points $x$, $b$, $p$ at which the three values are achieved; the integral dual infimum is attained when it is not $-\infty$.
• "Integer-valued" means $\omega(x)\in\mathbb Z$ on $B_1$ and $\zeta(x)\in\mathbb Z$ on $B_2$; integral potentials and separating vectors are V → ℤ.
• Theorem 2.1's "$\forall X\subset V$" is read as all $X\subseteq V$.

Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from $\zeta^\circ$ instead of $\zeta^\bullet$, a single base set for both functions, and a relaxed maximum taken over all of $\mathbb R^V$ instead of $\overline{B_1}\cap\overline{B_2}$.

Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
• K. Murota, Valuated matroid intersection I: optimality criteria, SIAM J. Discrete Math. 9 (1996) 545–561.
• K. Murota, Submodular flow problem with a nonseparable cost function, Report 95843-OR, Forschungsinstitut für Diskrete Mathematik, Universität Bonn, 1995 (source of Theorem 6.6).
• A. Frank, An algorithm for submodular functions on graphs, Annals of Discrete Mathematics 16 (1982) 97–120 (source of Theorem 6.5).
• A. Frank, A weighted matroid intersection algorithm, J. Algorithms 2 (1981) 328–336.
• J. Edmonds, Submodular functions, matroids and certain polyhedra, in: Combinatorial Structures and Their Applications, Gordon and Breach, New York, 1970, 69–87.
• S. Fujishige, Theory of submodular programs: a Fenchel-type min-max theorem and subgradients of submodular functions, Mathematical Programming 29 (1984) 142–155.
• M. Iri and N. Tomizawa, An algorithm for finding an optimal "independent assignment", J. Oper. Res. Soc. Japan 19 (1976) 32–57.
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

Motivation

Linear optimization over the bases of a matroid, over the integer points of a polymatroid, or over the flows of a network is well understood: the greedy algorithm is exact, the feasible sets are the integer points of polytopes described by submodular functions, and min-max theorems of Edmonds and Frank hold with integrality. Nonlinear objectives on the same sets are much less uniform. Valuated matroids (Dress and Wenzel, 1990; see Murota 2003) showed that a quantitative form of the Steinitz exchange axiom is exactly what keeps the greedy algorithm exact for a nonlinear weight. Kazuo Murota's paper Convexity and Steinitz's Exchange Property (Adv. Math. 124 (1996) 272–311) extends this exchange axiom from matroid bases to the integer points of arbitrary integral base polytopes, names the resulting functions M-concave, and proves that they are the discrete counterpart of concave functions. The paper is the starting point of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003), which is now used in auction theory (gross-substitutes valuations are M♮-concave), inventory and resource allocation, and combinatorial optimization.

This mission covers the first of the paper's three characterizations of M-concavity: the Extension Theorem (Theorem 4.6).

Setting

Let $V$ be a finite nonempty set. For $u\in V$, $\chi_u\in\mathbb Z^V$ is the characteristic vector of $u$. For $x\in\mathbb R^V$, $\operatorname{supp}^+(x)=\{v\mid x(v)>0\}$, $\operatorname{supp}^-(x)=\{v\mid x(v)<0\}$, $\|x\|=\sum_v|x(v)|$, and $\langle p,x\rangle=\sum_v p(v)x(v)$.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v\in B$ (axiom (B1)). Examples are the incidence vectors of the bases of a matroid. Its convex hull $\overline B$ is an integral base polytope; in general, an integral base polytope is the convex hull of some finite integral base set.

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC), and is called M-concave, if for all $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v\in B$, $y+\chi_u-\chi_v\in B$ and

The local exchange property (EXC$_{\mathrm{loc}}$) asks only, for $x,y\in B$ with $\|x-y\|=4$, for some $u\in\operatorname{supp}^+(x-y)$ and some $v\in\operatorname{supp}^-(x-y)$ with the same conclusion.

For $p\in\mathbb R^V$, $\omega[p](x)=\omega(x)+\langle p,x\rangle$, and $\operatorname{argmax}(\omega)=\{x\in B\mid\omega(x)\ge\omega(y)\ \forall y\in B\}$. For any $g:B\to\mathbb R$, the concave conjugate is $g^\circ(p)=\min_{x\in B}(\langle p,x\rangle-g(x))$ and the concave closure is $\hat g(b)=\inf_{p\in\mathbb R^V}(\langle p,b\rangle-g^\circ(p))$, a concave function that is finite exactly on $\overline B$. A function $\bar\omega:\overline B\to\mathbb R$ extends $\omega$ if $\bar\omega=\omega$ on $B$.

Formalization targets

Goal: the Extension Theorem (Theorem 4.6)

For a finite integral base set $B$ and $\omega:B\to\mathbb R$,

Milestones

• Lemma 3.2 (p. 282): under (EXC$_{\mathrm{loc}}$), for $y=x-\chi_{u_0}-\chi_{u_1}+\chi_{v_0}+\chi_{v_1}\in B$, $\omega_p(y)-\omega_p(x)\le\max(\pi_{00}+\pi_{11},\pi_{01}+\pi_{10})$ with $\pi_{ij}=\omega_p(x-\chi_{u_i}+\chi_{v_j})-\omega_p(x)$ ($-\infty$ off $B$).
• Theorem 3.1 (p. 282): (EXC) $\iff$ (EXC$_{\mathrm{loc}}$).
• Theorem 2.2 (p. 280): (EXC) for $\omega$ implies (EXC) for every $\omega[p]$.
• Lemma 4.3 (p. 285): under (EXC), $\operatorname{argmax}(\omega)$ is an integral base set.
• Lemma 4.1 (p. 285): $\hat g\ge g$ on $B$; $\max_{\overline B}\hat g=\max_B g$; $\operatorname{argmax}(\hat g)=\overline{\operatorname{argmax}(g)}$.
• Lemma 4.2 (p. 285): $(g[p_0])^\circ(p)=g^\circ(p-p_0)$ and $(g[p_0])^\wedge=\hat g+\langle p_0,\cdot\rangle$ on $\overline B$.
• Theorem 4.4 (p. 286): (EXC) $\iff$ $\operatorname{argmax}(\omega[p])$ is an integral base set for every $p$.
• Lemma 4.5 (p. 288): under (EXC), $\hat\omega=\omega$ on $B$.

Significance

The Extension Theorem identifies a combinatorial axiom with a convex-analytic property: M-concave functions are exactly the restrictions to lattice points of concave functions on the base polytope whose linear perturbations are all maximized on integral base polytopes. It is the reason the M-concave class supports a convex-analysis-style theory at all: local optimality implies global optimality, maximizers of linear perturbations are well behaved, and conjugacy (the paper's Theorems 5.3 and 6.4, separate missions of this series) can be developed. Theorem 3.1 on its own is widely used to verify M-concavity in applications, since it reduces the exchange axiom to pairs at distance four.

All results here were proved in 1996. To our knowledge none of them has a machine-checked proof; Mathlib has matroids on sets but no integral base sets in $\mathbb Z^V$, no M-concave functions and no concave closure of a function on a finite set. A formal proof of this chain would be a first formal development of discrete convex analysis.

Difficulty

The equivalence of (EXC) with its local version (Theorem 3.1) is not a routine induction on $\|x-y\|$: the exchange inequality for a far pair does not follow from the inequalities along a path of distance-4 pairs, because the exchange partner $v$ must be chosen consistently with the prescribed $u$. For the "if" direction of Theorem 4.4, knowing that every maximizer set is an integral base set says nothing directly about the values of $\omega$ at non-maximizing points; turning this global information on maximizers into the local inequality (EXC$_{\mathrm{loc}}$) requires a supporting hyperplane of the concave closure at a well-chosen point and the integrality of the intersection of an integral base polytope with a box (a cited result on submodular systems). Theorem 4.6 then needs the concave closure to agree with $\omega$ on $B$ (Lemma 4.5), which fails for general $\omega$.

Formalization scope

All declarations live in the namespace SteinitzExchange.Extension. The ground set is a type V with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ, and toReal embeds the former into the latter. $B$ is a Finset (V → ℤ). A function $\omega:B\to\mathbb R$ is a total (V → ℤ) → ℝ whose values are only ever read at points required to be in $B$. $\overline B$ is Mathlib's convexHull ℝ of the image of $B$. Pinned readings:

1. Integral base polytope means the convex hull of a finite nonempty set satisfying (B1) (by the paper's Theorem 2.1 this is its meaning), not "a polytope with integer vertices".
2. The concave closure is a real infimum; it is the paper's value on $\overline B$ and a junk value $0$ off $\overline B$ (the paper's $-\infty$), so every statement uses it only on $\overline B$. $\operatorname{argmax}(\hat g)$ and $\operatorname{argmax}(\bar\omega[p])$ range over $\overline B$ only; the concave conjugate is a minimum over the nonempty finite $B$.
3. Lemma 3.2's maximum with $-\infty$ entries is stated as: for one of the two pairings both exchanged points lie in $B$ and the bound holds for that pairing.
4. Theorem 4.4 and Lemma 4.3 conclude that $\operatorname{argmax}(\omega[p])$ is itself an integral base set. Read literally ("its convex hull is an integral base polytope") the "if" direction of Theorem 4.4 is false: $B=\{(2,0),(1,1),(0,2)\}$ with $\omega=(0,-1,0)$ is a counterexample. The paper's proof, its gloss in Lemma 4.3 and its use on p. 292 all take the integral-base-set reading. Theorem 4.6 needs no such adjustment and is stated as printed.
5. Theorem 2.2 carries the standing assumption of §2.3 that $\omega$ satisfies (EXC).

Trivializing formalizations are ruled out: the extension $\bar\omega$ must agree with $\omega$ on $B$ and be concave on $\overline B$, the argmax is over $\overline B$ and not over $\mathbb R^V$, and an integral base polytope is never empty.

A complete development needs basic facts on integral base sets (the equivalence of (B1) with the simultaneous exchange (B2), $B=\mathbb Z^V\cap\overline B$, and the paper's cited Theorem 2.1 relating them to submodular functions), the representation (4.3) of the concave closure as a maximum of convex combinations, and supporting hyperplanes of polyhedral concave functions. The layer of integral base sets and M-concave functions is reusable for the two other missions of this series and for any later formalization of discrete convex analysis; contributions of general-purpose lemmas about it are welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
• K. Murota, Discrete Convex Analysis, SIAM Monographs on Discrete Mathematics and Applications, 2003. https://doi.org/10.1137/1.9780898718508

Motivation

Line search methods for unconstrained minimization of a smooth function $f : \mathbb{R}^n \to \mathbb{R}$ choose a direction $d_k$ and a step $\alpha_k > 0$ and set $x_{k+1} = x_k + \alpha_k d_k$. Classical rules (Armijo, Wolfe) insist that every step decrease $f$. For quasi-Newton and conjugate gradient directions this monotonicity requirement often forces short steps, and nonmonotone line searches, which only ask for a decrease relative to some reference value built from past iterates, have been used since Grippo, Lampariello and Lucidi (1986) to let such methods take longer steps.

Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum of recent function values used by Grippo et al. with a weighted average $C_k$ of all past function values. The paper proves two results: global convergence to stationary points (the companion mission) and, the subject of this mission, R-linear convergence of the function values when $f$ is strongly convex.

Timeline:

• 1986, Grippo, Lampariello, Lucidi: nonmonotone line search based on the maximum of the last $M$ function values; global convergence.
• 2002, Dai: R-linear convergence of the max-based scheme for strongly convex $f$.
• 2004, Zhang and Hager: the averaged reference value $C_k$; global convergence (Theorem 2.2) and R-linear convergence for strongly convex $f$ (Theorem 3.1).

Setting

Fix parameters $0 \le \eta_{\min} \le \eta_{\max} \le 1$, $0 < \delta < \sigma < 1 < \rho$ and $\mu > 0$. Write $g_k = \nabla f(x_k)$ and $\nabla f(x)d = \langle \nabla f(x), d\rangle$. The Nonmonotone Line Search Algorithm (NLSA) keeps weights $Q_k$ and reference values $C_k$:

with $\eta_k \in [\eta_{\min}, \eta_{\max}]$ chosen freely at each step. A step $\alpha_k$ is accepted either by the nonmonotone Wolfe conditions

or by the nonmonotone Armijo rule $\alpha_k = \bar\alpha_k \rho^{h_k}$, where $\bar\alpha_k > 0$ is a trial step and $h_k$ is the largest integer such that the first inequality holds and $\alpha_k \le \mu$. With $\eta_k = 0$ one recovers the monotone rules.

The direction assumption asks for constants $c_1, c_2 > 0$ with $g_k^{\mathsf T} d_k \le -c_1\|g_k\|^2$ and $\|d_k\| \le c_2\|g_k\|$. The function $f$ is strongly convex with constant $\gamma > 0$ if

Let $x^*$ be the minimizer, $\mathcal L = \{x : f(x) \le f(x_0)\}$, $d_{\max} = \sup_k\|d_k\|$, and $\bar{\mathcal L}$ the set of points within distance $\mu d_{\max}$ of $\mathcal L$.

Formalization targets

Goal: Theorem 3.1

Let $f$ be strongly convex with minimizer $x^*$, let $\nabla f$ be Lipschitz continuous on bounded sets, let $\eta_{\max} < 1$, let the directions satisfy the direction assumption at every iteration, and let $\alpha_k \le \mu$ for all $k$. Then there is $\theta \in (0,1)$ with

The goal fixes no value of $\theta$: it asserts only the existence of a linear rate.

Milestones

In the paper's order of use:

1. Lemma 1.1: $f(x_k) \le C_k \le A_k$ when $g_k^{\mathsf T}d_k \le 0$ for each $k$.
2. $C_{k+1} \le C_k$, so all iterates lie in $\mathcal L$.
3. (3.4): $f(x) - f(x^*) \le \gamma\|\nabla f(x)\|^2$.
4. (2.15): $Q_{k+1} \le 1/(1 - \eta_{\max})$.
5. (3.6): $f(x_{k+1}) \le C_k - \beta\|g_k\|^2$, with

6. (3.7): $\|g_{k+1}\| \le b\|g_k\|$, $b = 1 + \mu c_2 L$.
7. (3.8): the explicit contraction

Here $L$ is a Lipschitz constant of $\nabla f$ on $\bar{\mathcal L}$. A further result on the same definitions is Theorem 3.2: if $f(x_k)$ converges R-linearly with ratio $\theta < \eta_{\min}$ inside a compact convex set on which $f$ is strongly convex, then the sufficient decrease condition with reference value $C_k$ holds for all large $k$.

Significance

Theorem 3.1 shows that averaging past function values costs nothing in the rate: on strongly convex functions the nonmonotone method keeps the linear rate of monotone descent, for any direction sequence satisfying the direction assumption (steepest descent, L-BFGS with bounded condition numbers, and so on). Theorem 3.2 is the converse side: for weights close enough to 1, the averaged test eventually accepts the steps of any R-linearly convergent iteration of this kind. The paper contrasts this with the max-based test of Grippo et al.

These results are proved in the paper. As far as the platform catalogue shows, no line search with the Wolfe conditions or a nonmonotone reference value has been formalized. The only related item is a monotone backtracking gradient descent rate, which is a different theorem. Machine-checked proofs would give reusable Lean statements of the nonmonotone Wolfe and Armijo rules and of the averaged reference value. They would also give the explicit constants $\beta$, $b$ and $\theta$ in checked form, and a checked record of the repair of the printed statement described below.

Difficulty

The obvious argument would show that $f(x_k) - f(x^*)$ contracts at each step. It fails: the method is nonmonotone, and $f(x_{k+1})$ may exceed $f(x_k)$. The quantity that contracts is $C_k - f(x^*)$, and only $C_k$ is controlled by the line search. The contraction must be derived by relating $\|g_k\|^2$ to $C_k - f(x^*)$ in two regimes, and the second regime needs a bound on $f(x_{k+1}) - f(x^*)$ from the gradient at the previous iterate. That bound requires the Lipschitz constant on a region containing every point the line search examines, which is why the region $\bar{\mathcal L}$ and the step bound $\mu$ enter. In Lean, the sufficient decrease (3.6) also rests on the step-length lower bounds of Lemma 2.1 for both rules, including the integer-exponent Armijo rule with its maximality condition.

Formalization scope

Conventions:

• The space is EuclideanSpace ℝ (Fin n), $f$ is ContDiff ℝ 1, and $\nabla f(x)d$ is ⟪gradient f x, d⟫_ℝ.
• A run is infinite, uses one rule throughout (Wolfe or Armijo), and has arbitrary directions subject to the stated hypotheses.
• $Q_k$ and $C_k$ are defined by recursion from the run.
• The Armijo exponent ranges over $\mathbb{Z}$ and "largest" is IsGreatest.
• $d_{\max}$ and distances are taken in $[0,\infty]$, so unbounded directions make $\bar{\mathcal L}$ the whole space.
• Strong convexity keeps the paper's constant $\gamma$, the inverse modulus.
• "Lipschitz on bounded sets" means that every bounded set admits a Lipschitz constant for $\nabla f$.

Repair of the printed statement: the paper's direction assumption holds only for all sufficiently large $k$, but Theorem 3.1 concludes (3.5) for each $k$, and its proof uses the assumption at every $k$. As printed the theorem is false: $d_0 = 0$ with the Wolfe step $\alpha_0 = 1$ gives $x_1 = x_0$, which violates (3.5) at $k = 1$ whenever $x_0 \ne x^*$. The goal therefore requires the direction assumption for every $k \ge 0$.

The step bound "there exists $\mu > 0$ with $\alpha_k \le \mu$" is stated with $\mu$ the algorithm's parameter. For the Armijo rule this holds by construction. The Wolfe rule does not use $\mu$, so nothing is lost.

Trivializing formalizations are ruled out:

• the printed hypotheses with "for each $k$" (false, as shown above);
• a $\theta$ allowed to equal 1, or an unspecified constant factor in front of $\theta^k$ (weaker than (3.5));
• a globally Lipschitz gradient, or a step bound different from the $\mu$ used to build $\bar{\mathcal L}$.

A complete development needs:

• the NLSA model and Lemma 1.1;
• the step-length lower bounds of Lemma 2.1 for both rules (via the descent lemma for Lipschitz gradients);
• the geometric bound on $Q_k$;
• boundedness of level sets of strongly convex functions.

The NLSA definitions are reusable by any later mission on nonmonotone line searches. Proofs of the milestones in any order are welcome, as are a proof of the counterexample to the printed statement and a proof that the platform theorem ConvexOptimization.strong_convexity_quadratic_lower_bound implies (3.4).

Selected references

• H. Zhang, W. W. Hager, A Nonmonotone Line Search Technique and Its Application to Unconstrained Optimization, SIAM J. Optim. 14(4):1043–1056, 2004. https://doi.org/10.1137/S1052623403428208
• L. Grippo, F. Lampariello, S. Lucidi, A Nonmonotone Line Search Technique for Newton's Method, SIAM J. Numer. Anal. 23(4):707–716, 1986. https://doi.org/10.1137/0723046
• Y.-H. Dai, On the Nonmonotone Line Search, J. Optim. Theory Appl. 112:315–330, 2002 (reference [4] of the paper).

Why do interior-point methods solve convex programs in $O(\sqrt{m}\log(1/\varepsilon))$ Newton steps? Nesterov and Nemirovskii's answer is self-concordance: a convex function whose third derivative is controlled by its second, $|\varphi'''(t)| \le 2\,\varphi''(t)^{3/2}$ along every line, admits a Newton analysis with absolute constants and no condition number — and the logarithmic barrier is self-concordant. This mission formalizes §9.6 and Chapter 11 of Boyd & Vandenberghe: the self-concordance calculus, the Newton-decrement analysis, the duality gap $m/t$ along the central path, the per-centering work bound $m(\mu - 1 - \log\mu)/\gamma + c$, and the crown result — with the aggressive schedule $\mu = 1 + 1/\sqrt{m}$ the barrier method reaches duality gap $\varepsilon$ after

centering steps, each of uniformly bounded Newton cost.

Motivation

Value-at-Risk (VaR) is the standard regulatory measure of downside risk of a portfolio: the loss level that is exceeded only with a prescribed small probability $\varepsilon$. Computing it requires the full distribution of asset returns, which is rarely known. In practice one estimates a mean vector and a covariance matrix and then assumes a Gaussian distribution, which understates the probability of large losses when returns are heavy-tailed or skewed.

El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the distributional assumption by a worst case: the VaR is computed against every distribution consistent with the known moments. For known mean and covariance they obtain an exact closed form and several semidefinite (SDP) representations of this worst-case VaR. The SDP forms are what make the approach extend to moment uncertainty (moments only known to lie in a set, §2.2 of the paper) and to robust portfolio optimization. The equivalence between the probabilistic statement and the closed form is also a multivariate one-sided Chebyshev bound, related to Bertsimas and Popescu (SIAM J. Optim. 15(3), 2005; working paper 2000).

Setting

There are $n$ assets. Their returns over one period form a random vector $x \in \mathbb R^n$, and a portfolio $w \in \mathbb R^n$ earns $r(w,x) = w^\top x$. The paper restricts $w$ to an admissible set that does not contain $0$; only $w \neq 0$ is used.

The distribution of $x$ is unknown except for its mean $\hat x \in \mathbb R^n$ and covariance matrix $\Gamma$, with $\Gamma \succ 0$ (positive definite). Let $\mathcal P$ be the set of all probability distributions on $\mathbb R^n$ with these two moments. For a loss level $\gamma$, the loss set is $\mathcal S = \{x \mid \gamma \le -x^\top w\}$. The worst-case VaR at level $\varepsilon$ is (Eq. (4))

Further notation: $\kappa(\varepsilon) = \sqrt{(1-\varepsilon)/\varepsilon}$ (Eq. (8)); for symmetric matrices, $A \succeq B$ means $A - B$ is positive semidefinite and $\langle A, B\rangle = \operatorname{Tr}(AB)$. The second-moment matrix is (Eq. (6))

Formalization targets

Goal: Theorem 1 (pp. 545–546)

For $\Gamma \succ 0$, $w \neq 0$, $\varepsilon \in (0,1)$ and $\gamma \in \mathbb R$, the following five propositions are equivalent:

1. $\sup_{P \in \mathcal P} P\{\gamma \le -w^\top x\} \le \varepsilon$;
2. $\kappa(\varepsilon)\,\|\Gamma^{1/2} w\|_2 - \hat x^\top w \le \gamma$;
3. there are a symmetric $M$ and $\tau \in \mathbb R$ with $\langle M, \Sigma\rangle \le \tau\varepsilon$, $M \succeq 0$, $\tau \ge 0$, and $M + \begin{bmatrix} 0 & w\\ w^\top & -\tau + 2\gamma\end{bmatrix} \succeq 0$;
4. every $x$ with $\begin{bmatrix}\Gamma & x - \hat x\\ (x-\hat x)^\top & \kappa(\varepsilon)^2\end{bmatrix} \succeq 0$ satisfies $-x^\top w \le \gamma$;
5. there are a symmetric $\Lambda$ and $v \in \mathbb R$ with $\langle \Lambda, \Gamma\rangle + \kappa(\varepsilon)^2 v - \hat x^\top w \le \gamma$ and $\begin{bmatrix}\Lambda & w/2\\ w^\top/2 & v\end{bmatrix} \succeq 0$.

In particular

Milestones (the steps of the paper's proof)

• Condition C.1 ($l(x) = [x^\top\,1] M [x^\top\,1]^\top \ge 0$ for all $x$) is equivalent to $M \succeq 0$ (p. 546).
• Conditions C.1 and C.2 are equivalent to the existence of $\tau \ge 0$ with $M \succeq 0$ and $M + \begin{bmatrix} 0 & \tau w\\ \tau w^\top & -1+2\tau\gamma\end{bmatrix} \succeq 0$ (p. 546).
• The worst-case probability $\sup_{P\in\mathcal P} P(\mathcal S)$ equals the value of the SDP $\inf \langle M, \Sigma\rangle$ under the constraints above (Eq. (14), pp. 546–547).
• The Schur-complement reduction (19)–(20) of the constraints of the dual problem (18) (p. 547).
• The closed form of $\phi(y)$ and its maximum at $y = \varepsilon$ (p. 547).
• Condition (10) describes the ellipsoid $\{x \mid (x-\hat x)^\top\Gamma^{-1}(x-\hat x) \le \kappa(\varepsilon)^2\}$, and the maximal loss $-x^\top w$ over it is $\kappa(\varepsilon)\sqrt{w^\top\Gamma w} - \hat x^\top w$ (p. 546).

Significance

The result. Proposition 2 turns the worst-case VaR into a second-order cone function of $w$, so minimizing it over a polytope of portfolios is a second-order cone program (Eq. (12)). The SDP forms 3 and 5 are the basis of the paper's §2.2–§3: they extend, with the moments only known to lie in a convex set, to a single SDP whose value is the worst-case VaR over that set. Proposition 4 gives a deterministic reading: the worst-case VaR is the largest loss when the return vector is only known to lie in an ellipsoid, which connects distributional robustness to robust optimization with ellipsoidal uncertainty.

Formalizing it. The result is proved in the paper, with two imported steps: strong duality for the moment problem (Smith 1995; Bonnans and Shapiro 2000) and a Slater-type strong duality for the one-constraint quadratic condition. No machine-checked version is known. A formal proof would supply these steps with explicit hypotheses and would produce a Lean statement of the multivariate one-sided Chebyshev (Cantelli) bound with tightness over the full moment class.

Difficulty

The matrix equivalences (2 ⇔ 4 ⇔ 5 and 2 ⇔ 3) are Schur complements and finite-dimensional SDP duality. The difficulty is Proposition 1. The upper bound (Cantelli's inequality for $w^\top x$) handles one direction, but the converse requires tightness: for every $\gamma$ below the closed form, a distribution on $\mathbb R^n$ with exactly the prescribed mean and full covariance matrix $\Gamma$ that puts probability more than $\varepsilon$ on the loss set. A scalar extremal distribution for $w^\top x$ does not by itself have the right covariance in the other directions, and a Gaussian does not reach the bound. The paper's route through the moment problem instead needs strong duality between a supremum over measures and an infimum over matrices, which is where the positive definiteness of $\Sigma$ enters.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin n); $x^\top w$ is the inner product, and matrices are Matrix (Fin n) (Fin n) ℝ. Matrices of size $n+1$ are indexed by Fin n ⊕ Fin 1 and built with Matrix.fromBlocks (the helper bordered A v c is $[[A, v],[v^\top, c]]$). $A \succeq 0$ is PosSemidef, $\Gamma \succ 0$ is PosDef, $\langle A, B\rangle$ is (A * B).trace, and $\|\Gamma^{1/2}w\|_2$ is written $\sqrt{w^\top\Gamma w}$.
• The class $\mathcal P$ (HasMeanCov) contains every Borel probability measure on $\mathbb R^n$ whose coordinates are square-integrable, with mean $\hat x$ and centred covariance $\Gamma$. It is not restricted to densities or to Gaussians: the Gaussian class gives a different constant, $-\Phi^{-1}(\varepsilon)$.
• Sup, inf and max: "$\sup_{P\in\mathcal P}P(\mathcal S) \le \varepsilon$" is stated as "$P(\mathcal S) \le \varepsilon$ for every $P \in \mathcal P$". The worst-case probability SDP is stated as IsLUB/IsGLB of one real number (no attainment is claimed). The maxima over $v$, over $y \in [\varepsilon,1]$ and over the ellipsoid are IsGreatest.
• Corrections to the printed statement. The paper prints $\varepsilon \in (0,1]$; at $\varepsilon = 1$ Proposition 1 holds for every $\gamma$ while Propositions 2–5 require $\gamma \ge -\hat x^\top w$, so the goal assumes $0 < \varepsilon < 1$. The goal also assumes $w \neq 0$, the paper's standing assumption; with $w = 0$, $\gamma = 0$ Proposition 1 fails and Proposition 2 holds. Milestones that remain true at $\varepsilon = 1$ keep $\varepsilon \le 1$.
• A goal that omits Proposition 1 would only be matrix algebra and is not this theorem. The five-way equivalence must be proved with the probabilistic statement included.
• Useful infrastructure, reusable beyond this mission: the homogenization lemma for quadratic functions, the S-lemma with one affine constraint, the Schur-complement criteria for bordered PSD matrices, and duality for the moment problem. Proofs of any milestone, and of lemmas building a distribution with prescribed mean and covariance, are welcome.

Selected references

• L. El Ghaoui, M. Oks, F. Oustry, Worst-Case Value-at-Risk and Robust Portfolio Optimization: A Conic Programming Approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM J. Optim. 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903
• J. E. Smith, Generalized Chebychev Inequalities: Theory and Applications in Decision Analysis, Operations Research 43(5):807–825, 1995. https://doi.org/10.1287/opre.43.5.807
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• L. Vandenberghe, S. Boyd, K. Comanor, Generalized Chebyshev Bounds via Semidefinite Programming, SIAM Review 49(1):52–64, 2007. https://doi.org/10.1137/S0036144504440543

Motivation

Online convex optimization is a repeated game between a learner and an adversary. In each round $t=1,\dots,T$ the learner commits to a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$; only then is a convex cost function $f_t$ revealed, and the learner pays $f_t(x_t)$. The learner is judged by its regret: its total cost minus the total cost of the best fixed point chosen in hindsight. The model covers online portfolio selection, online regression, prediction with expert advice and the analysis of stochastic gradient methods, and it is the standard language of online learning theory.

Zinkevich (ICML 2003) showed that projected gradient descent with step sizes of order $1/\sqrt t$ has regret $O(GD\sqrt T)$ for any convex costs with gradients bounded by $G$ on a set of diameter $D$, and this rate cannot be improved for linear costs. Hazan, Agarwal and Kale (Machine Learning 69, 2007) asked what curvature buys. Their first result, the subject of this mission, is that the same algorithm with the faster step sizes $1/(Ht)$ has regret only logarithmic in $T$ once every cost function is $H$-strongly convex. The paper's other three results (the Online Newton Step, Follow the Approximate Leader and Exponentially Weighted Online Optimization, for exp-concave costs) are the subject of the other missions of this series.

Setting

Fix $n\in\mathbb N$ and a nonempty, closed, bounded, convex set $\mathcal P\subseteq\mathbb R^n$, with the Euclidean norm $\|\cdot\|_2$ (§2.1, p. 171).

• Cost functions. A sequence $f_1,f_2,\dots:\mathbb R^n\to\mathbb R$. Write $\nabla f_t(x)$ for the gradient and $\nabla^2 f_t(x)$ for the Hessian.
• Gradient bound. A number $G$ with $\|\nabla f_t(x)\|_2\le G$ for all $x\in\mathcal P$ and all rounds $t$ (p. 172).
• $H$-strong convexity (p. 172). For $H>0$, $f$ is $H$-strongly convex on $\mathcal P$ when it is twice differentiable and $\nabla^2 f(x)\succeq H I_n$ for every $x\in\mathcal P$, i.e. $v^\top\nabla^2 f(x)v\ge H\|v\|_2^2$ for all $v$.
• Euclidean projection. $\Pi_{\mathcal P}(y)$ is the point of $\mathcal P$ nearest to $y$, $\Pi_{\mathcal P}(y)=\arg\min_{x\in\mathcal P}\|x-y\|_2$ (IsProj P y z).
• Online Gradient Descent (Fig. 1, p. 174), with step sizes $\eta_1,\eta_2,\dots$: $x_1\in\mathcal P$ is arbitrary, and in iteration $t>1$

(IsOGDRun P η f x).

• Regret (p. 171): $\mathrm{Regret}_T=\sum_{t=1}^T f_t(x_t)-\min_{x\in\mathcal P}\sum_{t=1}^T f_t(x)$, and $\mathrm{Regret}_T(\mathrm{OGD})$ is its supremum over all cost sequences.

Formalization targets

Goal: Theorem 1 (p. 175)

For $H>0$, cost functions that are $H$-strongly convex on $\mathcal P$ with gradients bounded by $G$ on $\mathcal P$, and any run of Online Gradient Descent whose step after round $t$ is $\eta_{t+1}=1/(Ht)$, for every $T\ge1$ and every $u\in\mathcal P$:

This is LogRegretOCO.OGD.ogd_regret_bound. The constant is the paper's, and at $T=1$ the bound reads $G^2/(2H)$.

Milestones

1. Eq. (1), the strong-convexity inequality: for $x,y\in\mathcal P$, $2(f(x)-f(y))\le 2\nabla f(x)^\top(x-y)-H\|y-x\|_2^2$.
2. Lemma 8 with $A=I_n$: for a convex $\mathcal P$, $z=\Pi_{\mathcal P}(y)$ and $a\in\mathcal P$, $\|y-a\|_2^2\ge\|z-a\|_2^2$. This is already on the platform, proved, as UnderstandingML.projection_lemma, and is reused as a reference item.
3. Eq. (2), the one-step inequality: for $z=\Pi_{\mathcal P}(x-\eta g)$, $\eta>0$, $\|g\|_2\le G$ and $u\in\mathcal P$, $2g^\top(x-u)\le(\|x-u\|_2^2-\|z-u\|_2^2)/\eta+\eta G^2$.

The last step of the argument is the harmonic-sum bound $\sum_{t=1}^T 1/t\le 1+\log T$, which Mathlib already provides (harmonic_le_one_add_log).

Significance

The result. Theorem 1 separates two regimes of online convex optimization: $\Theta(\sqrt T)$ regret for general convex costs and $O(\log T)$ for strongly convex ones, with an algorithm that costs one gradient and one projection per round. Through the online-to-batch conversion, the same step-size schedule gives the $O(\log T/T)$ rate of stochastic gradient descent on strongly convex objectives. The theorem is also the reference point for the paper's weaker exp-concavity assumption, under which the other three algorithms obtain $O(n\log T)$ regret.

Formalizing it. The result is proved and well known; what this mission adds is a machine-checked proof with the paper's exact constant. The Prove2Me platform holds a statement of the textbook version of this theorem (Hazan, Introduction to Online Convex Optimization, Theorem 3.3), OnlineConvexOpt.FirstOrder.online_gradient_descent_strongly_convex_regret, but it is Disproved: its regret is written with a real infimum over the decision set, which Lean evaluates to a junk value. No proved version of the logarithmic bound is on the platform. The strong-convexity inequality, the one-step projected-gradient inequality and the telescoping argument are reusable by every later formalization of gradient methods on the platform.

Difficulty

The argument is short, and its difficulty lies in the bookkeeping. The telescoping sum of squared distances cancels exactly only with the right step-size indexing: the step taken after round $t$ must be $1/(Ht)$. Reading Fig. 1 literally with $\eta_t=1/(Ht)$ makes the step after round $t$ equal to $1/(H(t+1))$, and the sum then leaves an uncancelled term $\frac H2\|x_1-x^*\|_2^2$ that the printed bound does not contain. Strong convexity is a statement about the Hessian, so the curvature inequality (1) needs a second-order Taylor expansion along a segment of $\mathcal P$; convexity of $\mathcal P$ keeps the segment inside the set where the Hessian bound holds. The projection step needs the obtuse-angle property of Euclidean projection onto a convex set.

Formalization scope

Points are EuclideanSpace ℝ (Fin n), so $\|\cdot\|$ is the Euclidean norm (the sup norm of Fin n → ℝ would change the gradient bound). Cost functions are functions on all of $\mathbb R^n$, as the paper's use of gradients and Hessians presupposes; the gradient is Mathlib's gradient, and the Hessian quadratic form is the second Fréchet derivative applied to $(v,v)$. Rounds are 1-based: x 0, f 0 and η 1 are never read, and sums run over Finset.Icc 1 T. The run of the algorithm is a predicate on the whole trajectory, required at every round; the projection is a predicate (nearest point of $\mathcal P$), which is unique for nonempty closed convex $\mathcal P$.

Choices and corrections relative to the printed text:

• Step-size index. Theorem 1 prints "step sizes $\eta_t=\frac1{Ht}$", while its proof sets $\eta_{t+1}=1/(Ht)$ for the step after round $t$. The goal uses the proof's indexing, as a hypothesis η (t + 1) = 1 / (H * t) for $t\ge1$ on the step sizes of Fig. 1.
• Eq. (2). The paper prints "$5\nabla_t^\top(x_t-x^*)$"; the $5$ is a typo for $2$, and the milestone states $2$. The verbatim milestone text keeps the printed $5$.
• Regret. Regret is stated against every comparator $u\in\mathcal P$; the minimum over the compact set $\mathcal P$ is attained, so this is the paper's statement. The expectation in the paper's regret is vacuous for this deterministic algorithm, and the supremum over cost sequences is the universal quantifier over $f$.
• Hypotheses. Strong convexity and the gradient bound are required for the rounds $1,\dots,T$ only. Convexity of each $f_t$, a standing assumption of §2.2, follows from $H$-strong convexity on the convex set $\mathcal P$ and is not added. No diameter bound enters Theorem 1.

A regret bound written with a real ⨅/sInf over $\mathcal P$, or a bound for an arbitrary sequence satisfying Eq. (2) instead of a run of the paper's algorithm, would not be Theorem 1; the goal quantifies over every comparator in $\mathcal P$ and carries the run predicate, the Hessian hypothesis and the gradient bound. The hypotheses are jointly satisfiable: on the closed unit ball, $f_t(x)=\frac H2\|x\|_2^2$ with $G=H$ meets all of them.

Contributions welcome: proofs of the two inequalities and of the goal; a general projection lemma for positive semidefinite $A$ (Lemma 8 in full, needed by the Online Newton Step mission) is reusable beyond this mission.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022 (Theorem 3.3). https://arxiv.org/abs/1909.05207
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014 (Lemma 14.9, the projection lemma). https://doi.org/10.1017/CBO9781107298019

Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication

holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, $\lambda \begin{bmatrix} F_1 & g_1 \\ g_1^{T} & h_1\end{bmatrix} \succeq \begin{bmatrix} F_2 & g_2 \\ g_2^{T} & h_2\end{bmatrix}$ for some $\lambda \ge 0$. It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.

Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.

Motivation

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

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

Setting

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

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