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

$$\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v).$$

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

$$\omega^\circ(p)=\min_{x\in B_1}\big(\langle p,x\rangle-\omega(x)\big),\qquad \zeta^\bullet(p)=\max_{x\in B_2}\big(\langle p,x\rangle-\zeta(x)\big),$$

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

$$\max_{x\in B_1\cap B_2}\big(\omega(x)-\zeta(x)\big)=\max_{b\in\overline{B_1}\cap\overline{B_2}}\big(\hat\omega(b)-\check\zeta(b)\big)=\inf_{p\in\mathbb R^V}\big(\zeta^\bullet(p)-\omega^\circ(p)\big),$$

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

$$\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v).$$

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

$$\omega\ \text{satisfies (EXC)}\iff\exists\,\bar\omega:\overline B\to\mathbb R\ \text{concave},\ \bar\omega|_B=\omega,\ \forall p:\ \operatorname{argmax}_{\overline B}(\bar\omega[p])\ \text{is an integral base polytope}.$$

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

$$Q_0 = 1,\ \ Q_{k+1} = \eta_k Q_k + 1,\qquad C_0 = f(x_0),\ \ C_{k+1} = \frac{\eta_k Q_k C_k + f(x_{k+1})}{Q_{k+1}},$$

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

$$f(x_k + \alpha_k d_k) \le C_k + \delta\alpha_k g_k^{\mathsf T} d_k,\qquad \nabla f(x_k + \alpha_k d_k) d_k \ge \sigma g_k^{\mathsf T} d_k,$$

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

$$f(x) \ge f(y) + \nabla f(y)(x - y) + \frac{1}{2\gamma}\|x - y\|^2\quad\text{for all } x, y.$$

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

$$f(x_k) - f(x^*) \le \theta^k\big(f(x_0) - f(x^*)\big)\quad\text{for each } k.$$

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

$$\beta = \min\left\{\frac{\delta\mu c_1}{\rho},\ \frac{2\delta(1-\delta)c_1^2}{L\rho c_2^2},\ \frac{\delta(1-\sigma)c_1^2}{Lc_2^2}\right\}.$$

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

$$C_{k+1} - f(x^*) \le \theta\,(C_k - f(x^*)),\qquad \theta = 1 - \beta b_2(1-\eta_{\max}),\quad b_2 = \frac{1}{\beta + \gamma b^2}.$$

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

$$\Bigl\lceil \sqrt{m}\,\log_2\bigl(m/(t^{(0)}\varepsilon)\bigr)\Bigr\rceil$$

centering steps, each of uniformly bounded Newton cost.

Motivation

Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of $\mathrm{conv}(X)$ does not give back the integer program, because an optimal integer point may lie in the interior of $\mathrm{conv}(X)$.

Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.

Setting

Let $D$ be an $m \times n$ matrix and $\mathbf d$ an $m$-vector with rational entries. The polyhedron is

$$P = \{\mathbf x \in \mathbb R^n \mid D\mathbf x \geqslant \mathbf d,\ \mathbf x \geqslant \mathbf 0\},$$

and its set of integer points is $X = P \cap \mathbb Z^n$, the points of $P$ whose coordinates are all integers. Because $P \subseteq \mathbb R^n_+$, $X = P \cap \mathbb Z^n_+$.

The recession cone of $P$ is $\{\mathbf r \in \mathbb R^n \mid D\mathbf r \geqslant \mathbf 0,\ \mathbf r \geqslant \mathbf 0\}$. An integer ray of $P$ is a nonzero vector of $\mathbb Z^n$ in this cone. Extreme rays are not required.

In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.

Formalization targets

Goal: Theorem 1 (pp. 1011–1012)

If $P \neq \emptyset$, there exist a finite set of integer points $\{\mathbf p_q\}_{q \in Q} \subseteq X$ and a finite set of integer rays $\{\mathbf p_r\}_{r \in R}$ of $P$ such that

$$X = \Bigl\{\mathbf x \in \mathbb R^n_+ \ \Big|\ \mathbf x = \sum_{q \in Q} \mathbf p_q \lambda_q + \sum_{r \in R} \mathbf p_r \lambda_r,\ \sum_{q \in Q} \lambda_q = 1,\ \boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}\Bigr\}. \qquad (24)$$

Since the multipliers are nonnegative integers summing to one over $Q$, (24) says that $X$ is the union, over $q \in Q$, of the translates $\mathbf p_q + \mathbb Z_+\{\mathbf p_r\}_{r\in R}$ of the monoid generated by the rays. No bound on $|Q|$ or $|R|$ is part of the goal.

Milestone: Remark in §3.3 (p. 1012)

If $X \subseteq [0,1]^n$, every point of $X$ is a vertex of $\mathrm{conv}(X)$. In this case convexification and discretization coincide.

Significance

The result. Theorem 1 converts an integer program $\min\{c(\mathbf x) \mid A\mathbf x \geqslant \mathbf b,\ \mathbf x \in X\}$ into the integer master program (25) over the multipliers $\boldsymbol\lambda$, with one column per generating point and per generating ray. When $X$ is bounded the rays disappear, exactly one $\lambda_q$ equals one, and (25) is a linear integer program even for a nonlinear cost $c$. The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.

Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over $\mathrm{conv}(X)$, is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.

Difficulty

The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of $P$ need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of $P$ generate the recession cone over $\mathbb R_+$, but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of $Q$ is also not automatic: $X$ itself is typically infinite, and taking $Q = X$ trivializes the statement.

Rationality of the data is essential. For $P = \{\mathbf x \in \mathbb R^2_+ \mid \sqrt2\,x_1 - x_2 \geqslant 0\}$, every integer ray has slope below $\sqrt 2$, so finitely many base points and rays generate only points with $x_2 \leqslant \rho x_1 + C$ for some $\rho < \sqrt 2$, while $X$ contains $(k, \lfloor\sqrt2 k\rfloor)$ for every $k$.

Formalization scope

• Vectors are Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.
• $D$ and $\mathbf d$ are ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.
• The hypothesis $P \neq \emptyset$ is kept as on the page. $X$ may still be empty (e.g. $P = \{1/2\}$); then $Q = \emptyset$ and both sides of (24) are empty. The statement allows this.
• $Q$ and $R$ are Fin k and Fin l for existentially chosen $k, l \in \mathbb N$; the finiteness is the content of the theorem. The multiplier vector $\boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}$ is written as a pair of ℕ-valued vectors.
• "Integer rays of $P$" is read as nonzero integer vectors in the recession cone $\{D\mathbf r \geqslant \mathbf 0, \mathbf r \geqslant \mathbf 0\}$; extremality is not required, as the page does not require it (contrast (8), which says "extreme rays").
• The constraint $\mathbf x \in \mathbb R^n_+$ on the right side of (24) is kept although it is implied.
• In the Remark, "vertices of $\mathrm{conv}(X)$" is read as extreme points of the convex hull; $X$ is finite there, so the two notions agree.

A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with $Q$ or $R$ infinite would be trivial; both are excluded by the statement.

Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.

Selected references

• M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
• G. L. Nemhauser and L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• R. R. Meyer, On the existence of optimal solutions to integer and mixed-integer programming problems, Mathematical Programming 7:223–235, 1974. https://doi.org/10.1007/BF01585518
• F. Vanderbeck, On Dantzig–Wolfe decomposition in integer programming and ways to perform branching in a branch-and-price algorithm, Operations Research 48(1):111–128, 2000. https://doi.org/10.1287/opre.48.1.111.12453
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

Nonlinear programming algorithms are routinely advertised as finding a local minimum. Most of them only certify first-order conditions (a KKT point), and the natural next question is whether a given feasible point is in fact a local minimum. For smooth problems where the Hessian is nonsingular this is a second-order test, but in the degenerate case the test itself becomes a combinatorial question about a quadratic form restricted to a cone.

K. G. Murty and S. N. Kabadi (Math. Programming 39 (1987) 117–129) showed that this question is intractable already in its simplest instance: deciding whether $x = 0$ is a local minimum of a quadratic form $x^{\mathsf T}Dx$ on the nonnegative orthant is NP-complete, and so is deciding whether a square integer matrix is copositive. The paper is the standard reference for the hardness of copositivity testing, which matters for copositive programming, for second-order optimality checks in constrained optimization, and for the complexity of local search in nonconvex optimization.

Setting

Let $D$ be a real square matrix of order $n$ and $Q(x) = x^{\mathsf T}Dx$. The matrix $D$ is copositive if $Q(x) \ge 0$ for every $x \ge 0$ (coordinatewise). The paper considers the quadratic program

$$\text{(7)}\qquad \text{minimize } Q(x) \quad \text{subject to } x \ge 0,$$

and the following questions, each phrased so that "yes" is the interesting answer:

• Problem 1. Is $x = 0$ not a local minimum of (7)?
• Problem 2. Is $Q$ not bounded below on $\{x \ge 0\}$?
• Problem 3. Is there an $x \ge 0$ with $Q(x) < 0$ (is $D$ not copositive)?
• Problem 4. Given $a_0 > 0$, is there an $x \ge 0$ with $e^{\mathsf T}x = a_0$ and $Q(x) < 0$? Here $e$ is the all-ones vector.
• Problems 11, 12. With $h(u) = (u_1^2, \dots, u_n^2)\,D\,(u_1^2, \dots, u_n^2)^{\mathsf T}$, the objective of the unconstrained problem (15): is $u = 0$ not a local minimum of $h$ on $\mathbb R^n$, and is $h$ not bounded below?

The source problem is subset sum (Problem 5): given positive integers $d_0; d_1, \dots, d_n$, is there $y \in \{0,1\}^n$ with $\sum_j d_j y_j = d_0$? Let $l$ be the total number of digits in the data. The paper fixes an integer $\delta > 4\big(d_0\sum_j d_j\big)^2 n^3$ and a rational $\varepsilon$ with $0 < \varepsilon < 2^{-nl^2}$, and defines functions of $2n$ nonnegative variables $(y, s)$:

$$f_1(y,s) = \Big(\sum_j d_j y_j - d_0\Big)^2 + \delta\sum_j (y_j + s_j - 1)^2 + \sum_j y_j s_j,$$

$f_2 = f_1 + 2d_0\sum_j d_j y_j(1 - y_j)$, a homogeneous quadratic $f_4$ that agrees with $f_2$ on the set

$$P = \Big\{(y,s) : y \ge 0,\ s \ge 0,\ \sum_j (y_j + s_j) = n\Big\},$$

and $f_5 = f_4 - (\varepsilon/n^2)\big(\sum_j (y_j + s_j)\big)^2$. The function $f_5$ is a quadratic form $x^{\mathsf T}Mx$ in $x = (y, s) \in \mathbb R^{2n}$; the symmetric matrix $M$, with entries computed explicitly from $d_0, d, \delta, \varepsilon$, is the output of the reduction.

Formalization targets

Goal: the reduction is correct

For positive integer data $d_0; d_1, \dots, d_n$ and $\delta, \varepsilon$ as above, with $M$ the matrix of $f_5$, the following are equivalent:

$$\text{subset sum is solvable} \iff \text{P1}(M) \iff \text{P2}(M) \iff \text{P3}(M) \iff M \text{ not copositive} \iff \text{P4}(M, n) \iff \text{P11}(M) \iff \text{P12}(M).$$

This is the mathematical content of Theorems 1–3 and §4: a polynomially computable map from subset sum instances to matrices under which every one of these questions has the answer of the subset sum instance.

Milestones along the paper's chain

1. Problems 5 and 6 are equivalent: subset sum is solvable iff some $(y,s) \in P$ has $f_1 \le 0$.
2. Problems 6 and 7 are equivalent ($f_1$ vs. $f_2$ on $P$).
3. Problems 7 and 8 are equivalent ($f_2$ vs. $f_4$ on $P$).
4. Lemma 2: for an integer symmetric $D$ of size $L$, the minimum of $Q$ over $[0,1]^n$ is $0$ or at most $-2^{-L}$.
5. Problems 8 and 9 are equivalent: $\exists\,(y,s)\in P$ with $f_4 \le 0$ iff $\exists\,(y,s)\in P$ with $f_5 < 0$.
6. Problem 9 is a special case of Problem 4: $f_5(y,s) = x^{\mathsf T}Mx$, and Problem 9 is Problem 4 for $(M, a_0 = n)$.
7. Problems 3 and 4 are equivalent, for any $D$ and $a_0 > 0$.
8. Problems 1 and 2 are equivalent to Problem 3, for any $D$.
9. Problems 11 and 12 are equivalent to Problems 1 and 2, for any $D$.

Significance

The result. The equivalence shows that checking local optimality of a feasible point, checking boundedness of a quadratic objective on a cone, and checking copositivity are all at least as hard as subset sum, hence NP-hard. Through (15) the same holds for local minimality and boundedness of a quartic polynomial with no constraints at all. These facts are the standard justification for why nonconvex solvers settle for KKT points, and the copositivity part underlies the hardness of copositive programming.

The formalization. The paper's claims are proved, and have been cited for decades, but the proof as printed is a sketch: several steps are stated as "clearly" or "it can be verified", and one step of the proof of Theorem 1 (p. 125) is false as written. The inequality $(\delta/2)(y_j + s_j - 1)^2 + 2d_0 d_j y_j(1 - y_j) \ge 0$ for $y_j > 1$ fails for $y_j$ slightly above $1$, and the pointwise implication "$f_2 \le 0 \Rightarrow f_1 \le 0$ on $P$" has an explicit counterexample. The equivalence of Problems 6 and 7 itself survives numerical checks. A machine-checked proof of the goal settles the correctness of the reduction with the paper's own constants. No machine-checked proof of these statements exists on the platform.

Difficulty

The combinatorial direction (a subset sum solution gives a point with $f_5 < 0$) is a computation. The converse direction carries the content, in two places.

First, passing from $f_1$ to $f_2$ trades the linear penalty for a quadratic one. This is harmless on the box $0 \le y \le 1$ but not for $y_j > 1$, where $2d_0d_jy_j(1-y_j)$ is negative. The printed argument handles this coordinate by coordinate and is wrong there; a correct argument has to show that no point of $P$ with $f_2 \le 0$ exists unless a point with $f_1 \le 0$ does, which requires a global use of the size of $\delta$.

Second, passing from $f_4 \le 0$ to $f_5 < 0$ requires a quantitative gap: if $f_4 > 0$ on $P$ then $\min_P f_4 \ge \varepsilon$ with $\varepsilon$ of only polynomially many bits. Lemma 2 provides such a gap for the unit box and integer matrices, but $P$ is not the box and $f_4$ has rational coefficients, so the lemma does not apply verbatim.

The remaining equivalences (Problems 1, 2, 3, 4, 11, 12 for a fixed matrix) follow from homogeneity of the quadratic form and the substitution $x_j = u_j^2$, and are routine.

Formalization scope

The data $d_0, d_j, \delta$ are natural numbers and $\varepsilon$ is rational; all are cast to $\mathbb R$ in $f_1, \dots, f_5$ and $M$. The index $j = 1, \dots, n$ is Fin n, and the $2n$ variables of $M$ are indexed by Fin n ⊕ Fin n with $x =$ Sum.elim y s. Standing hypotheses: $d_j > 0$ and $d_0 > 0$ (the paper's "all positive integers"); $\delta > 4(d_0\sum_j d_j)^2n^3$ in $\mathbb N$; $\varepsilon > 0$ and $\varepsilon \cdot 2^{nl^2} < 1$ in $\mathbb Q$. The size $l$ counts decimal digits. Problem 1 is local minimality relative to the orthant, Problem 11 is unconstrained local minimality, both in the Euclidean topology. Lemma 2 is stated for integer symmetric $D$ (as §4 of the paper says, "as before … symmetric"), with $L$ Schrijver's encoding size, since the paper does not define "the size of $D$"; the "optimum is $0$ or $\le -2^{-L}$" is stated as a disjunction without an infimum. The milestones on $f_2, f_4, f_5$ over $P$ assume $n \ge 1$, which the paper assumes tacitly; the goal needs no such hypothesis.

Not formalized: membership in NP (Lemma 1), the polynomial-time computability of $M$ and its encoding size, the NP-completeness of subset sum (cited by the paper from Garey–Johnson), Theorem 4, and any of the words "NP-complete" or "NP-hard". The platform's complexity layer (Turing machines over bitstrings) has no subset sum problem and no encoding of rational matrices. The matrix $M$ has rational entries; a positive integer multiple of it is the integer matrix of Theorem 3, has the same answer to every question, and the rescaling is not formalized. The §3 standing assumption "D is not PSD" is not imposed; the constructed matrix can be PSD and the equivalence holds regardless.

The goal is about the explicit matrix $M$, whose entries are given in the definitions; it is not about "some matrix whose quadratic form is $f_5$", and the constants $\delta$ and $\varepsilon$ are the paper's explicit bounds, not "sufficiently large" or "for some $\varepsilon$". A formalization that quantifies existentially over the matrix or the precision would be trivially true and is ruled out.

Contributions welcome: proofs of the matrix identity and the homogeneity arguments (milestones 6–9), a proof of Lemma 2 (which needs a Cramer/Hadamard bound on basic solutions of the linear complementarity system (9)), and a correct proof of the $f_1 \leftrightarrow f_2$ step. The copositivity definitions and milestones 7–9 are reusable for any later work on copositive programming.

Selected references

• K. G. Murty and S. N. Kabadi, Some NP-complete problems in quadratic and nonlinear programming, Mathematical Programming 39 (1987) 117–129. https://doi.org/10.1007/BF02592948
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (subset sum, problem [SP13]).
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986 (encoding sizes, §2.1).

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))

$$V_{\mathcal P}(w) = \min\Big\{\gamma \;:\; \sup_{P\in\mathcal P} P(\mathcal S) \le \varepsilon\Big\}.$$

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))

$$\Sigma = \begin{bmatrix} S & \hat x \\ \hat x^\top & 1\end{bmatrix}, \qquad S = \Gamma + \hat x\hat x^\top.$$

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

$$V_{\mathcal P}(w) = \kappa(\varepsilon)\,\|\Gamma^{1/2}w\|_2 - \hat x^\top w.$$

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