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

Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to $0/1$ vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).

The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.

Setting

Let $V$ be a finite nonempty set, $n=|V|$. For $u\in V$ let $\chi_u\in\mathbb Z^V$ be the unit vector, for $X\subseteq V$ let $\chi_X$ be its characteristic vector, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$. For a finite $B\subseteq\mathbb Z^V$, $\overline B$ is its convex hull.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that

$$\text{(B1)}\quad x,y\in B,\ u\in\operatorname{supp}^+(x-y)\ \Rightarrow\ \exists v\in\operatorname{supp}^-(x-y):\ x-\chi_u+\chi_v\in B.$$

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC) (is M-concave) if 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,\ 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)$. Write $\omega[p](x)=\omega(x)+\langle p,x\rangle$ and $\operatorname{argmax}(g)$ for the maximizers of $g$ on $B$.

The support function of $B$ is $\psi^\circ(p)=\min\{\langle p,x\rangle\mid x\in B\}$. A positively homogeneous $h:\mathbb R^V\to\mathbb R$ is "matroidal" if

• (C1) $X\mapsto h(\chi_X)$ is supermodular, and
• (C2) $h(p)=\sum_{j=1}^n(p_j-p_{j+1})\,h(\chi_{V_j})$ whenever $V=\{v_1,\dots,v_n\}$ with $p(v_1)\ge\dots\ge p(v_n)$, $p_j=p(v_j)$, $V_j=\{v_1,\dots,v_j\}$, $p_{n+1}=0$.

The concave conjugate is $\omega^\circ(p)=\min\{\langle p,x\rangle-\omega(x)\mid x\in B\}$, the concave closure is $\hat\omega(b)=\inf_p\{\langle p,b\rangle-\omega^\circ(p)\}$, the subdifferential is $\partial\omega^\circ(p_0)=\{b\mid\omega^\circ(p)-\omega^\circ(p_0)\le\langle p-p_0,b\rangle\ \forall p\}$, and the localization of $\omega^\circ$ at $p_0$ is $\hat L(\omega^\circ,p_0)(p)=\inf\{\langle p,b\rangle\mid b\in\partial\omega^\circ(p_0)\}$.

Formalization targets

Goal: the Local Supermodularity Theorem (Theorem 5.3, corrected)

For $\omega$ on a finite integral base set $B$,

$$\omega\ \text{satisfies (EXC)}\iff\Big(\omega=\hat\omega\ \text{on}\ B\Big)\ \text{and}\ \Big(\hat L(\omega^\circ,p_0)\ \text{is "matroidal" for every}\ p_0\in\mathbb R^V\Big).$$

The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: $B=\{(2,0),(1,1),(0,2)\}$, $\omega=(0,-10,0)$.

Milestones

1. Theorem 2.1: (B1) is equivalent to $B$ being the integer points of an integral submodular (equivalently, supermodular) system, whose defining function is determined by $B$.
2. Theorem 5.1: if $B=\mathbb Z^V\cap\overline B$, then $B$ satisfies (B1) iff $\psi^\circ$ is "matroidal".
3. Lemma 5.2: sums of "matroidal" functions are "matroidal".
4. Theorem 4.4: (EXC) holds iff every $\operatorname{argmax}(\omega[p])$ satisfies (B1).
5. Eq. (5.12): $\hat L(\omega^\circ,p_0)(p)=\min\{\langle p,x\rangle\mid x\in\operatorname{argmax}(\omega[-p_0])\}$.

Significance

The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of $\omega^\circ$, in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.

The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of $\operatorname{conv}(\operatorname{argmax}\,\omega[-p_0])$ to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.

Difficulty

$\omega^\circ$ depends only on the concave closure $\hat\omega$, so any characterization of (EXC) through $\omega^\circ$ alone cannot see values of $\omega$ below $\hat\omega$. That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near $p_0$.

Formalization scope

Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of $\mathbb Z^V$ is a Finset (V → ℤ). A function on $B$ is a total function (V → ℤ) → ℝ whose values off $B$ are never used. The mission commits to the following readings:

• Minima. $\psi^\circ$, $\omega^\circ$ are real infima over the finite set $B$, hence minima for nonempty $B$ (every statement has $B$ nonempty). $\hat\omega$ is a real infimum used only at points of $B$, where it is bounded below.
• Localization. $\hat L$ is a real sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.
• (C2). It is required for every bijection Fin n ≃ V along which $p$ is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.
• Theorem 2.1. The page's "$\forall X\subset V$" is read as all $X\subseteq V$. The set functions are integer-valued, and "Moreover" is read strongly: every $f$ (resp. $g$) as in (b) (resp. (c)) equals the displayed max (resp. min).
• Theorem 4.4. "$\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope" is read as "$\operatorname{argmax}(\omega[p])$ satisfies (B1)", following Lemma 4.3 and the proof of Theorem 5.3. The literal convex-hull reading makes the "if" direction false (same counterexample).
• Theorem 5.1 keeps the page's hypothesis $B=\mathbb Z^V\cap\overline B$.

Trivializing formalizations are ruled out. Defining $\hat L$ by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An $\omega^\circ$ taken as a supremum would reverse the sign conventions.

The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all 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
• A. W. M. Dress, W. Wenzel, Valuated matroids: a new look at the greedy algorithm, Applied Mathematics Letters 3 (1990), 33–35.
• S. Fujishige, Submodular Functions and Optimization, 2nd ed., Annals of Discrete Mathematics 58, Elsevier, 2005.
• L. Lovász, Submodular functions and convexity, in Mathematical Programming: The State of the Art, Springer, 1983, 235–257. https://doi.org/10.1007/978-3-642-68874-4_10
• 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

Why closed-form ADMM updates matter

The alternating direction method of multipliers (ADMM) solves problems of the form $\min f(x)+g(z)$ subject to $Ax+Bz=c$ by alternating a minimization in $x$, a minimization in $z$ and a dual ascent step. Its practical appeal, as surveyed by Boyd, Parikh, Chu, Peleato and Eckstein in Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Foundations and Trends in Machine Learning, 2011, doi:10.1561/2200000016), rests on the fact that each of these minimizations is often trivial to carry out: a projection, a linear solve, or a componentwise formula. Chapter 4 of the book, "General Patterns", catalogues the cases that recur in every later application (lasso, basis pursuit, sparse inverse covariance selection, consensus and sharing problems). This mission formalizes the statements of that chapter, culminating in the identification of the update for an $\ell_1$ penalty with soft thresholding.

Setting

Vectors live in $\mathbb R^n$ with the Euclidean norm $\|\cdot\|_2$. An extended-real-valued function $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ is given by its effective domain $\operatorname{dom} f$ and its finite values there. Fix a penalty parameter $\rho>0$, a matrix $A\in\mathbb R^{p\times n}$ and a vector $v\in\mathbb R^p$. The $x$-update of ADMM (p. 25) is

$$x^+=\operatorname*{argmin}_x\Bigl(f(x)+\tfrac{\rho}{2}\|Ax-v\|_2^2\Bigr),$$

where "argmin" denotes a minimizer over $\operatorname{dom} f$. When $A=I$ the right-hand side, as a function of $v$, is the proximity operator $\mathbf{prox}_{f,\rho}(v)$ (§4.1).

The chapter evaluates $x^+$ in four situations:

• $f$ is the indicator function of a closed nonempty convex set $\mathcal C$ ($0$ on $\mathcal C$, $+\infty$ off it); then $x^+$ is the Euclidean projection $\Pi_{\mathcal C}(v)$, the nearest point of $\mathcal C$ to $v$;
• $f(x)=\tfrac12x^TPx+q^Tx+r$ is a convex quadratic, with $P$ symmetric positive semidefinite, possibly restricted to an affine set $\{x\mid Fx=g\}$;
• $f(x)=f_1(x_1)+\cdots+f_n(x_n)$ is componentwise separable and $A^TA$ is diagonal;
• $f(x)=\lambda\|x\|_1=\lambda\sum_i|x_i|$ with $\lambda>0$ and $A=I$.

The soft thresholding operator (§4.4.3, p. 32) is, for $\kappa\ge0$,

$$S_\kappa(a)=\begin{cases}a-\kappa & a>\kappa\\ 0 & |a|\le\kappa\\ a+\kappa & a<-\kappa,\end{cases}$$

applied componentwise to vectors.

Formalization targets

Goal: soft thresholding is the proximity operator of the ℓ1 norm (§4.4.3, p. 32)

For $\lambda>0$, $\rho>0$ and $v\in\mathbb R^n$, a vector $x$ minimizes $\lambda\|x\|_1+\tfrac{\rho}{2}\|x-v\|_2^2$ over $\mathbb R^n$ if and only if

$$x_i=S_{\lambda/\rho}(v_i)\qquad(i=1,\dots,n).$$

The statement gives both that the soft-thresholded vector is a minimizer and that it is the only one.

Milestones

1. Projection (§4.1, p. 26): for $\mathcal C$ closed, nonempty and convex, $\Pi_{\mathcal C}(v)$ exists and is unique, and for every $\rho>0$ the $x$-update of the indicator of $\mathcal C$ is exactly $\Pi_{\mathcal C}(v)$.
2. Nonnegative orthant (§4.1, p. 26): for the indicator of $\mathbf R^n_+$, $x^+=(v)_+$, uniquely.
3. Quadratic update (4.1) (p. 26): if $P+\rho A^TA$ is invertible it is positive definite, and $x^+=(P+\rho A^TA)^{-1}(\rho A^Tv-q)$ is the unique minimizer.
4. Matrix inversion lemma (§4.2.4, p. 28): $(P+\rho A^TA)^{-1}=P^{-1}-\rho P^{-1}A^T(I+\rho AP^{-1}A^T)^{-1}AP^{-1}$ when the inverses exist. This is the Woodbury identity, already proved on the platform, and is referenced rather than re-posed.
5. Equality-constrained quadratic (§4.2.5, p. 29): $x^{k+1}$ minimizes the update over $\{Fx=g\}$ iff some $\nu$ solves the KKT system; when the affine set is nonempty, $x^+$ is an affine function of $v$.
6. Component separability (§4.4.2, p. 31): with $A^TA$ diagonal, the $x$-update splits into $n$ independent scalar minimizations.
7. Positive-part form (p. 32): $S_\kappa(a)=(a-\kappa)_+-(-a-\kappa)_+$.
8. Shrinkage form (4.2) (p. 32): $S_\kappa(a)=(1-\kappa/|a|)_+a$ for $a\ne0$.
9. Scalar update (p. 32): $S_{\lambda/\rho}(v_i)$ is the unique minimizer of $\lambda|t|+\tfrac{\rho}{2}(t-v_i)^2$.

Significance

The results of this chapter are what make ADMM an implementable algorithm rather than a conceptual one. Soft thresholding is the $z$-update of the lasso (§6.4), of distributed $\ell_1$-regularized regression (§8.2) and of sparse inverse covariance selection (§6.5); projections are the updates of every constrained problem in Chapter 5; the linear-system form (4.1) and the KKT system are the updates of least squares and quadratic programming. Every later chapter of the book cites these identities without proof, so a formal library of them is the substrate on which formal statements about specific ADMM instances can be built.

None of these statements is open as a mathematical question: all are classical facts of convex analysis. The book states them without proof (the goal is justified by a reference to subdifferential calculus in Rockafellar's Convex Analysis). This mission poses their formal statements as Lean proof goals. The matrix inversion lemma already has a machine-checked proof on the platform (the Woodbury identity) and is reused. A related but distinct statement, that singular value shrinkage is the proximity operator of the nuclear norm (Cai, Candès and Shen, 2010), is posed separately on the platform and is not this mission's target.

Difficulty

The goal objective $\lambda\|x\|_1+\tfrac{\rho}{2}\|x-v\|_2^2$ is not differentiable, so setting a gradient to zero does not apply; the minimizer sits exactly on the kink of $|\cdot|$ whenever $|v_i|\le\lambda/\rho$. A proof has to handle the three regimes of $S_\kappa$ and must establish global optimality, not only stationarity, together with uniqueness. Passing from the vector problem to the scalar ones requires the separability statement, which is a statement about minimizers of sums over a product domain, not about any particular function. For the quadratic milestones, the difficulty is linear-algebraic: showing that invertibility of $P+\rho A^TA$ forces positive definiteness, and, for the equality-constrained case, that a minimizer exists and depends affinely on $v$ even when $F$ is rank deficient and the KKT matrix is singular.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so ‖·‖ is $\|\cdot\|_2$; matrices are Matrix (Fin p) (Fin n) ℝ acting through Matrix.toEuclideanLin. The conventions committed to are:

• Functions as (domain, values). An extended-real-valued $f$ is a pair: a domain set and a real function on it. An indicator function is (the set, $0$).
• Argmin as a predicate. IsXUpdate, IsProx and IsProjection say "$x$ is a minimizer"; no choice function is used. Where the book says "the solution", the theorems state an equivalence "$x$ is a minimizer $\iff$ $x$ equals the formula", which gives existence and uniqueness at once.
• Explicit hypotheses. $\rho>0$ and $\lambda>0$ (written lam, since λ is a Lean keyword); $\kappa\ge0$ for the soft thresholding identities (implicit in the book, where $\kappa=\lambda/\rho$, and false for $\kappa<0$); $a\ne0$ in (4.2), as on the page; $P$ symmetric positive semidefinite (Matrix.PosSemidef); invertibility of $P+\rho A^TA$ in (4.1); $\mathcal C$ closed, convex and nonempty for the projection; nonemptiness of $\{Fx=g\}$ for the existence part of §4.2.5; $F$ of arbitrary rank.
• ℓ1 norm. $\|x\|_1$ is defined as $\sum_i|x_i|$, separately from the Euclidean norm.
• Separability is stated for a general $A$ with $A^TA$ diagonal, with the scalar problems written out explicitly (the book does not write them).

The trivializing formalization to avoid is stating the goal as the subgradient condition $0\in\lambda\,\partial|\cdot|(x_i)+\rho(x_i-v_i)$, or as agreement of the three formulas for $S_\kappa$: the goal is global minimality and uniqueness of the soft-thresholded vector for the $\ell_1$ objective. Not formalized: the flop counts and caching remarks of §§4.2.1–4.2.4 and the iterative-solver discussion of §4.3, which make no mathematical claim.

Contributions welcome: proofs of any milestone; the general block-separability statement of §4.4.1; a lemma connecting IsProx with Mathlib's orthogonal projection onto complete convex sets.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. https://doi.org/10.1561/2200000016
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (§23, subdifferentials). https://doi.org/10.1515/9781400873173
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93, 1965, pp. 273–299. https://doi.org/10.24033/bsmf.1625
• J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM Journal on Optimization 20(4), 2010, pp. 1956–1982. https://doi.org/10.1137/080738970

Motivation

Infinite-horizon dynamic programming with positive (nonnegative) costs and no discounting, or with discount factors that do not make the Bellman operator a contraction, is the setting of Blackwell's and Strauch's positive and negative programming models and of many deterministic control and reachability problems. In this regime the classical contraction argument is unavailable: the optimal cost may be infinite at some states, value iteration may fail to converge to it, and an optimal policy may fail to exist. Chapter 5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), treats these problems in an abstract framework, a single monotone mapping $H$, so that one set of theorems covers stochastic control with additive or multiplicative costs and minimax control. The chapter is the book version of Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977).

The chapter's last structural result answers a practical question: when value iteration is run from the terminal cost, do the minimizing controls it computes at each stage lead to an optimal stationary policy?

Setting

The abstract monotone model consists of a state space $S$, a control space $C$, nonempty constraint sets $U(x)\subseteq C$, a terminal function $J_0 : S\to(-\infty,\infty]$, and a mapping $H(x,u,J)\in[-\infty,\infty]$ defined for $x\in S$, $u\in C$ and $J : S\to[-\infty,\infty]$, which is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$.

A selector is a function $\mu : S\to C$ with $\mu(x)\in U(x)$; a policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors, and it is stationary if all $\mu_k$ are equal. The operators are

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$

the cost of a policy is $J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0)(x)$, $J_\mu$ is the cost of the stationary policy $(\mu,\mu,\dots)$, and the optimal cost is $J^*(x)=\inf_\pi J_\pi(x)$. A policy is optimal if $J_\pi=J^*$.

Assumption I (uniform increase) is $J_0(x)\le H(x,u,J_0)$ for all $x$, $u\in U(x)$; under it the sequence defining $J_\pi$ is nondecreasing, so the limit exists in $[-\infty,\infty]$. Assumption I.1 says $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $J_0$, and I.2 says that for some $\alpha>0$, $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$ and $J\ge J_0$. Assumptions D, D.1, D.2 are the mirror images (uniform decrease, continuity along nonincreasing sequences below $J_0$, and a lower shift bound).

The DP algorithm (value iteration) generates $T(J_0), T^2(J_0),\dots$; for $k\ge0$ and $\lambda\in\mathbb R$ the level sets

$$U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$$

collect the controls that keep the stage-$k$ cost below $\lambda$.

Formalization targets

Goal: Proposition 5.11

Let I, I.1 and I.2 hold, let $C$ be a Hausdorff space, and let $U_k(x,\lambda)$ be compact for all $x\in S$, $\lambda\in\mathbb R$ and $k\ge\bar k$. Then (a) some policy $\pi^*=(\mu_0^*,\mu_1^*,\dots)$ satisfies

$$(T_{\mu_k^*}T^k)(J_0)=T^{k+1}(J_0)\qquad\forall k\ge\bar k;$$

(b) for every such policy, $\{\mu_k^*(x)\}$ has an accumulation point whenever $J^*(x)<\infty$; and (c) any $\mu^*$ that picks such an accumulation point at those states, and any admissible control where $J^*(x)=\infty$, defines an optimal stationary policy:

$$J_{\mu^*}=J^*.$$

Milestones

In the order of the mission's milestone list: Lemma 3.1 (compact sublevel sets give a minimum), Proposition 5.2 (Bellman's equation $J^*=T(J^*)$ under I, I.1, I.2), Proposition 5.4 (a stationary policy is optimal iff $T_{\mu^*}(J^*)=T(J^*)$), Proposition 5.10 (under the compactness hypothesis, $J_\infty=T(J_\infty)=T(J^*)=J^*$ and a stationary optimal policy exists), Proposition 5.6 ($\varepsilon$-optimal policies from approximate attainment, with explicit constants $\sum_k\alpha^k\varepsilon_k=\varepsilon$ and $\varepsilon(1-\alpha)$), Corollaries 5.3.1 and 5.7.1 (Bellman's equation and $\varepsilon$-optimal policies under D, D.2 with finite $S$ and $J^*>-\infty$), and Propositions 5.14 and 5.15 (the multiplicative-cost and minimax models satisfy I, I.1, I.2 or D, D.1/D.2 with explicitly named scalars).

Significance

Proposition 5.10 alone gives existence of an optimal stationary policy; Proposition 5.11 identifies one. It says that the minimizers computed by value iteration, which any implementation produces anyway, converge (along subsequences, state by state) to optimal controls. This is the abstract form of the classical results for deterministic and stochastic positive-cost problems with compact control sets, and through Propositions 5.14 and 5.15 it applies to multiplicative (risk-sensitive) costs and to minimax control without new arguments.

Lemma 3.1, Propositions 5.1–5.5, 5.7–5.10, Lemmas 5.1–5.2 and Corollaries 5.2.1, 5.3.2 are already formalized and proved on the platform, in the MonotoneDP.Increase and MonotoneDP.Decrease developments built from the 1977 paper; this mission reuses their model and assumption definitions and links Lemma 3.1, Proposition 5.2 and Proposition 5.10 as milestones. Propositions 5.4 (in the book's stronger form, with policies optimal state by state), 5.6, 5.11, 5.14, 5.15 and Corollaries 5.3.1, 5.7.1 are new here. All are proved in the book; none has a machine-checked proof yet.

Difficulty

The obvious route to (c) is to pass to the limit in $H[x,\mu_k^*(x),T^k(J_0)]=T^{k+1}(J_0)(x)$. That fails twice. First, $\{\mu_k^*(x)\}$ need not converge, and different subsequences may have different limits; the statement is about an arbitrary accumulation point, and in a general Hausdorff space accumulation points are not limits of subsequences. Second, $H$ is not assumed continuous in $u$ at all: the only regularity in $u$ is compactness of the level sets $U_k(x,\lambda)$, and the only regularity in $J$ is I.1 along monotone sequences. States with $J^*(x)=\infty$ need separate treatment, because there the level sets give no control on $\mu_k^*(x)$.

For Corollaries 5.3.1 and 5.7.1 the difficulty is that D.1 is not assumed; the replacement uses finiteness of $S$ and $J^*>-\infty$ essentially, and both hypotheses are needed.

Formalization scope

Functions $J$ are S → EReal. The model, Assumptions I, I.1, I.2, D, D.1, D.2 and the epigraph sets used by Proposition 5.10 are the published definitions MonotoneDP_Increase_Model, MonotoneDP_Increase_Assumptions, MonotoneDP_Increase_Epigraph, MonotoneDP_Decrease_Model and MonotoneDP_Decrease_Assumptions. In them $J_\pi$ is the limit (limUnder) of the policy compositions, which exists under I or D; $T^k$ is the iterate T^[k]; the composition $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ applies $T_{\mu_{N-1}}$ first; the model requires $S$ nonempty and $J_0>-\infty$; "I.2 holds" is the existence of a scalar $\alpha$, and results that name the scalar take it as a parameter. An accumulation point of a sequence in $C$ is a cluster point (MapClusterPt), not a limit; in Proposition 5.11(c) the conclusion includes that $\mu^*$ is admissible. $J^*+\varepsilon$ is computed pointwise in $[-\infty,\infty]$ and equals $+\infty$ where $J^*$ does.

The book computes in $[-\infty,\infty]$ with $\infty-\infty=\infty$. Mathlib's EReal gives $\top+\bot=\bot$, so the two mappings of Section 2.3 use the series' shared definitions, which follow the book's convention: the expected value on a countable $W$ (expect, positive and negative parts summed in $[0,\infty]$, $+\infty$ when the positive part diverges) and the sum inside the minimax supremum (badd, $+\infty$ when either summand is $+\infty$), both from BertsekasShreve.FiniteHorizon.SpecificModels. Propositions 5.14 and 5.15 quantify over every model whose $H$ and $J_0$ are these mappings; such models exist because the mappings are monotone.

A formalization in which $J_\pi$ or $J^*$ is introduced as an arbitrary fixed point of $T$, or in which (c) assumes that $\mu^*$ is a limit of $\mu_k^*$, would make the goal trivial or different; both are ruled out by the definitions above.

Contributions welcome: proofs of the milestones, and reusable EReal infrastructure (limits of monotone sequences, series of nonnegative extended reals) that the Part I chapters of the book share.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; reprinted Athena Scientific, 1996. Chapter 5, pp. 70–90. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977) 438–464. https://doi.org/10.1137/0315031
• D. Blackwell, "Positive dynamic programming", Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
• R. E. Strauch, "Negative dynamic programming", Ann. Math. Statist. 37 (1966) 871–890. https://doi.org/10.1214/aoms/1177699369

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