Optimization

Motivation

Many problems in statistics, signal processing and machine learning minimize the sum of a smooth loss and a convex, nonsmooth, separable regularizer: smooth optimization with $\ell_1$-regularization, bound-constrained optimization, the group Lasso and, through duality, support vector regression are special cases listed in §1 of the paper discussed below. For such problems, methods that update one coordinate, or one small block of coordinates, at a time are often the method of choice, because each update is cheap and exploits separability.

Paul Tseng and Sangwoon Yun (Math. Program. Ser. B 117 (2009) 387–423) introduced the coordinate gradient descent (CGD) method for this class: at each iteration it minimizes a quadratic model of the smooth part plus the exact nonsmooth part over a chosen block of coordinates, then takes an Armijo step. Their paper proves global convergence (Theorem 1) and, under a local error bound, linear convergence (Theorems 2 and 3). This mission is the second of a three-mission series on the paper; it targets the linear convergence theorem for the cyclic (Gauss–Seidel-type) choice of blocks.

The analysis follows Luo and Tseng's error-bound framework for smooth constrained problems (Ann. Oper. Res. 46 (1993) 157–178), which established linear rates for feasible descent methods without strong convexity. Tseng and Yun extend that framework to a nonsmooth convex term.

Setting

Let $\Re^n$ carry the Euclidean norm $\|\cdot\|$, let $\mathcal N=\{1,\dots,n\}$, and for $\mathcal J\subseteq\mathcal N$ let $x_{\mathcal J}$ be the subvector of coordinates in $\mathcal J$. The problem (1) is

$$\min_x\ F_c(x)=f(x)+cP(x),$$

where $c>0$, $P:\Re^n\to(-\infty,\infty]$ is proper, convex and lower semicontinuous, and $f$ is continuously differentiable on an open set containing $\operatorname{dom}P$.

Given $x\in\operatorname{dom}P$, a nonempty block $\mathcal J$ and a symmetric positive definite matrix $H$, the direction (6) is

$$d_H(x;\mathcal J)=\arg\min_d\Big\{\nabla f(x)^Td+\tfrac12d^THd+cP(x+d)\ \Big|\ d_j=0\ \forall j\notin\mathcal J\Big\}.$$

The CGD method starts at $x^0\in\operatorname{dom}P$, chooses at each iteration $k$ a block $\mathcal J^k$ and a matrix $H^k$, computes $d^k=d_{H^k}(x^k;\mathcal J^k)$, and sets $x^{k+1}=x^k+\alpha^kd^k$. The Armijo rule takes $\alpha^k$ as the largest element of $\{\alpha^k_{\rm init}\beta^j\}_{j\ge0}$ with

$$F_c(x^k+\alpha^kd^k)\le F_c(x^k)+\alpha^k\sigma\Delta^k,\qquad \Delta^k=\nabla f(x^k)^Td^k+\gamma\,d^{kT}H^kd^k+cP(x^k+d^k)-cP(x^k),$$

with $0<\beta,\sigma<1$ and $0\le\gamma<1$. The restricted Gauss–Seidel rule (12) asks for indices $0=t_0<t_1<\cdots$ (the set $\mathcal T$) such that the blocks used during each cycle $t_i\le k<t_{i+1}$ are pairwise disjoint and cover $\mathcal N$. $P$ is block-separable with respect to $\mathcal J$ if $P(x)=P_{\mathcal J}(x_{\mathcal J})+P_{\mathcal J^C}(x_{\mathcal J^C})$.

The analysis uses three assumptions: $\nabla f$ is $L$-Lipschitz on $\operatorname{dom}P$ (22); Assumption 1, $\bar\lambda I\succeq H^k\succeq\underline\lambda I$ with $0<\underline\lambda\le\bar\lambda$; and Assumption 2. Writing $\bar X$ for the set of stationary points of $F_c$ and $d_I(x)$ for the full direction with $H=I$, Assumption 2 says (a) $\bar X\ne\emptyset$ and the local Lipschitzian error bound $\operatorname{dist}(x,\bar X)\le\tau\|d_I(x)\|$ holds on every level set $\{F_c\le\zeta\}$ wherever $\|d_I(x)\|\le\epsilon$; (b) stationary points with different objective values are at least a fixed distance $\delta>0$ apart.

Formalization targets

Goal: Theorem 2(b)

Under (22), Assumptions 1 and 2, the restricted Gauss–Seidel rule, block-separability of $P$ with respect to every $\mathcal J^k$, and Armijo steps with $\sup_k\alpha^k_{\rm init}\le1$ and $\inf_k\alpha^k_{\rm init}>0$:

$$\{F_c(x^k)\}\downarrow-\infty\quad\text{or}\quad\big(\{F_c(x^k)\}_{\mathcal T}\ \text{Q-linear}\ \text{and}\ \{x^k\}_{\mathcal T}\ \text{R-linear}\big).$$

No rate constant is fixed: the goal asserts the shape of the convergence, so it is not invalidated by sharper constants.

Milestones

Lemma 4 (Hölder dependence of the subproblem's solution on its linear term), Lemma 5(a) (a per-block variational inequality), Lemma 5(b) (an explicit stepsize at which the Armijo test passes), Theorem 1(f) (Armijo stepsizes bounded away from zero, $\Delta^k\to0$, $d^k\to0$), and Theorem 2(a) (the residual $\|d_I(x^k)\|$ at the start of a cycle is bounded by the step lengths of the cycle).

Significance

Theorem 2(b) gives a linear rate for a block coordinate method on a nonsmooth, possibly nonconvex composite problem without strong convexity: the rate follows from the error bound, which holds for a large class of problems studied in §6 of the paper (the third mission of this series).

The theorem is proved in the paper; none of it has been machine-checked, as far as a search of the Prove2Me library shows. Formalizing it requires a reusable treatment of extended-valued convex functions through their effective domains, of the coordinate-restricted proximal subproblem, and of the Armijo rule for composite objectives. The milestones Lemma 4 and Lemma 5 are self-contained facts about this subproblem and are reusable for other proximal coordinate methods.

Difficulty

The classical route to a linear rate, as in Luo and Tseng's smooth analysis, derives $F_c(x^{k+1})-\bar\upsilon\le\tau'\|x^{k+1}-x^k\|^2$ from the error bound, where $\bar\upsilon$ is the limit value. With a nonsmooth $P$ this inequality is not available: the authors say so on p. 405, and work with $-\Delta^k$ in place of the quadratic term. A second obstacle is that the error bound controls the full residual $d_I(x^k)$, while each iteration only computes a block direction at a different point; relating the two over a cycle needs the disjointness of the blocks in the restricted rule and block-separability of $P$. Neither the global analysis nor the error bound alone gives the rate.

Formalization scope

$\Re^n$ is EuclideanSpace ℝ (Fin n), with 0-based coordinates. The extended-valued $P$ is encoded as a pair: its effective domain $D=\operatorname{dom}P$ and its finite values on $D$, with "proper convex lsc" given by the published definition ProxNewton.Inexact.IsProperClosedConvex; $F_c$ is never evaluated off $D$, and every statement carries membership in $D$ explicitly. The direction $d_H(x;\mathcal J)$ is the unique minimizer of (6) when $x\in D$ and $H\succ0$ (chosen by Classical.epsilon), and runs of the method carry the minimizer property itself. The Armijo rule takes the first admissible exponent $j$. $\mathcal T$ is a strictly increasing map $t$ with $t_0=0$. Stationarity is $F_c'(x;d)\ge0$ for all $d$, in liminf form. In Assumption 2, $\operatorname{dist}$ is the infimum distance and "for any $\zeta\ge\min F_c$" is "for every real $\zeta$" (equivalent, since the condition is empty below $\inf F_c$). Q-linear convergence includes convergence of the sequence; R-linear convergence is $\|x^{t_i}-\bar x\|\le Cq^i$ with $q<1$. The rates in the goal are along $\mathcal T$, as the paper states.

Explicit choices relative to the printed text:

• Theorem 2(a) is corrected. As printed, $\|d_I(x^k)\|\le\sup_j\alpha^j\,C\,r^k$ fails for small constant stepsizes and fails without block-separability (counterexamples in the item's statement). The milestone states $\|d_I(x^k)\|\le\max\{1,\sup_j\alpha^j\}\,C\,r^k$ under block-separability of $P$ with respect to every $\mathcal J^k$ (both are what the paper's proof gives and what Theorem 2(b) supplies), with the iterates in $\operatorname{dom}P$, and with $C$ quantified before the problem data, so it depends only on $n,L,\underline\lambda,\bar\lambda$.
• Lemma 5(b)'s range $0\le\alpha\le\min\{1,2\underline\lambda(1-\sigma+\sigma\gamma)/L\}$ is stated as $0\le\alpha\le1$ and $\alpha L\le2\underline\lambda(1-\sigma+\sigma\gamma)$, so that $L=0$ gives $[0,1]$ as on paper rather than $\{0\}$.
• Lemma 5(a) holds for every decomposition of $P$ in (20), and $\bar x$ ranges over $\operatorname{dom}P_{\mathcal J}$ (outside it the left side is $-\infty$).
• "$\lim F_c(x^k)>-\infty$" is "the values $F_c(x^k)$ are bounded below"; "$\{F_c(x^k)\}\downarrow-\infty$" is "nonincreasing and tending to $-\infty$"; suprema and infima of stepsizes are explicit bounds.

A statement that replaces Assumption 2 by strong convexity, claims a rate along the whole sequence rather than along $\mathcal T$, or asserts the Q-linear contraction without convergence to a limit is not this theorem and is out of scope.

Lemma 1, the claim after (10), Lemma 3 and Theorem 1(a), which the proof also uses, are milestones of the first mission of this series and are not restated here. Theorem 3 (the same conclusion along the whole sequence for the Gauss–Southwell-q rule) is not included: its proof is omitted in the paper. Contributions welcome: proofs of the milestones, and general facts about the coordinate-restricted proximal subproblem (existence and uniqueness of $d_H(x;\mathcal J)$, optimality conditions) that the milestones rely on.

Selected references

• P. Tseng and S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming Ser. B 117 (2009) 387–423. https://doi.org/10.1007/s10107-007-0170-0
• Z.-Q. Luo and P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• J. M. Ortega and W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970, Chap. 9 (Q- and R-linear convergence). https://doi.org/10.1137/1.9780898719468
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

A dynamic programming problem in Blackwell's sense describes a controller who observes the state of a system, picks an action, collects a return, and watches the system move at random to a new state, forever. Blackwell treated the discounted case, with a bounded return and a discount factor below one (Blackwell 1965), and the positive bounded case. Strauch's paper (Strauch 1966) studies the third case, the negative case: the return is non-positive and there is no discounting. Equivalently, a non-negative cost is minimized over an infinite horizon. This is the setting of stochastic shortest-path, optimal stopping with costs, and many inventory and search problems in which the total cost may be infinite.

In the negative case two standard tools of the discounted theory break down. An optimal policy need not exist, and the natural algorithm, value iteration from the zero function, need not converge to the optimal return. Strauch's §9 gives a condition on the action sets, essential finiteness, under which both are restored. The introduction (p. 872) summarizes the finite case: "In the negative case, … if A is finite, there is an optimal policy (Section 9)." In the later terminology of Bertsekas and Shreve (1978), Strauch's negative case is their positive-cost model, for which value iteration from zero is known to require such finiteness or compactness conditions.

Setting

The state space $S$ and the action space $A$ are non-empty Borel sets. The law of motion $q(\cdot\mid s,a)$ is a probability measure on $S$ depending measurably on $(s,a)$. The return $r(s,a,t)$, collected when action $a$ is taken in state $s$ and the next state is $t$, is a Borel function with $-\infty<r\le 0$ and $\int r(s,a,t)\,dq(t\mid s,a)>-\infty$ for every $(s,a)$.

A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the $n$th action at random, with a law depending measurably on the whole history $(s_1,a_1,\dots,s_n)$. A Markov policy $(f_1,f_2,\dots)$ is a sequence of measurable maps $S\to A$; the stationary policy $f^{(\infty)}$ uses one map $f$ at every stage. The expected return from the initial state $s$ is

$$I(\pi)(s)=\sum_{n=1}^\infty \pi_1q\cdots\pi_nq\,r\,(s)\in[-\infty,0],$$

the sum of the expected stage returns. The optimal return is $v^*=\sup_\pi I(\pi)$, over all policies, and $\pi^*$ is optimal if $I(\pi^*)\ge v^*$ at every state.

For a measurable $f:S\to A$ and a non-positive Borel $u$, the operator $T$ of $f$ is

$$Tu(s)=\int\big[r(s,f(s),t)+u(t)\big]\,dq(t\mid s,f(s)),$$

and the operator of a Markov policy $\pi^*=(f_1,f_2,\dots)$ is $Uu=\sup_nT_nu$, with $T_n$ the operator of $f_n$. Value iteration is the sequence $U^n0$.

Actions $a$ and $b$ are equivalent at $s$ if $r(s,a,\cdot)=r(s,b,\cdot)$ and $q(\cdot\mid s,a)=q(\cdot\mid s,b)$. $A$ is essentially finite by $\pi^*$ if there is a partition of $S$ into Borel sets $S_1,S_2,\dots$ such that for $s\in S_n$ every action is equivalent at $s$ to one of $f_1(s),\dots,f_n(s)$. A finite $A$ is essentially finite by any Markov policy whose first $|A|$ rules are the constant rules.

Formalization targets

Goal: Theorem 9.1 (N), p. 887

If $A$ is essentially finite by $\pi^*$ and $U$ is the operator of $\pi^*$, then

$$U^n0(s)\xrightarrow[n\to\infty]{}v^*(s)=\sup_\pi I(\pi)(s)\quad\text{for every } s,\qquad\text{and}\qquad \exists f:\ I(f^{(\infty)})\ge v^*.$$

Both parts are kept together, as printed. The goal fixes no constants and no rate.

Milestones

1. Lemma 6.1 (N), p. 880. For every Markov policy $\hat\pi$ with operator $U$, $\lim_nU^n0$ exists and

$$\lim_nU^n0\ \ge\ \sup_{\pi\in G(\hat\pi)}I(\pi)\ \ge\ \sup_{f^{(\infty)}\in G(\hat\pi)}I(f^{(\infty)}),$$

where $G(\hat\pi)$ is the set of $\hat\pi$-generated policies (each rule equal to $f_n$ on the $n$th piece of a Borel partition). 2. Proof of Theorem 8.4, p. 887. $\sup_\pi I(\pi)=\sup\{I(\hat\pi)\mid\hat\pi\text{ Markov}\}$ pointwise. 3. Proof of Theorem 9.1, p. 887, first step. Under essential finiteness, $U^n0$ is non-increasing and $I(\pi)\le v^\infty:=\lim_nU^n0$ for every policy $\pi$. 4. Proof of Theorem 9.1, p. 887, second step. Under essential finiteness, $Uv^\infty\ge v^\infty$.

Inside the proof of Theorem 9.1 the paper writes $v^*$ for $\lim_nU^n0$; the mission writes $v^\infty$ for it and reserves $v^*$ for $\sup_\pi I(\pi)$.

An optional extra item states the introduction's special case: if $A$ is finite, an optimal policy exists (§1, p. 872).

Significance

Theorem 9.1 gives, in the negative case, both a computational and an existential conclusion. Value iteration from zero computes the optimal return, so the optimal total cost of an essentially finite problem is the limit of the optimal finite-horizon costs. An optimal policy exists and can be taken stationary, so the controller needs only a single measurable decision rule. Without a hypothesis of this kind neither conclusion holds in the negative case; Example 6.1 of the paper exhibits a problem where the limit of value iteration, the best return among generated policies, and the best stationary return all differ.

The result is proved in the paper. What the mission adds is a machine-checked statement and, eventually, proof of it on general Borel spaces, with the return allowed to equal $-\infty$. Blackwell's discounted analogue already has a published statement on Prove2Me (DiscountedDP.Stationary.theorem7b_optimal_stationary), in a bounded-return model; the negative case is a separate statement in a separate model. No formalization of the negative case is known to exist.

Difficulty

The discounted proof rests on the contraction property of $U$ in the supremum norm, and in the negative case that property is missing: returns are unbounded below and there is no discount. The obvious argument, "$U^n0$ decreases to some $v^\infty$, and $v^\infty$ is the optimal return because finite-horizon play approximates infinite play", fails at the second step. The finite-horizon optimum can stay strictly above the infinite-horizon optimum, because a policy can postpone a cost beyond every fixed horizon; this is exactly the gap Example 6.1 exhibits. Closing it needs the essential finiteness of the actions together with the reduction of arbitrary policies to Markov ones (milestone 2), whose proof in the paper passes through the measurable-selection results of §7–§8.

Formalization scope

• The state and action spaces are non-empty standard Borel types; "Baire function" means Borel measurable.
• The law of motion is a Markov kernel; the return is real-valued, non-positive, Borel, and integrable against every $q(\cdot\mid s,a)$ (the paper's $r>-\infty$ and $qr>-\infty$).
• Returns live in EReal and are computed as minus the lintegral of the loss $-r$, which keeps the value $-\infty$. $I(\pi)$ is the sum over stages of the expected stage loss, which equals the paper's integral over futures by monotone convergence.
• $v^*$ is the supremum over every randomized history-dependent plan, never over Markov or stationary policies only, and it is not defined through $U$. Defining $v^*$ as $\lim_nU^n0$ would make part (a) of the goal hold by unfolding; this trivializing formalization is excluded.
• Optimality is against every plan, at every state.
• $U$ is the operator of the fixed $\pi^*$ of the hypothesis, applied from the zero function; convergence is pointwise in EReal.
• Stages are numbered from $0$ in Lean. Essential finiteness is zero-based: Lean's piece $n$ is the paper's $S_{n+1}$ and allows the rules $f_1,\dots,f_{n+1}$. The pieces are measurable, pairwise disjoint and cover $S$; empty pieces are allowed, as in the paper.
• Explicit choices: the existence of $\lim U^n0$ in Lemma 6.1 is part of the statement; the limit in the steps of Theorem 9.1 is written as the infimum of the non-increasing sequence.
• Only the negative case is formalized; the paper's discounted and positive parts are not.

Policies, Markov policies, stationary policies and $\hat\pi$-generated rules come from the published definitions DiscountedDP.Stationary.Model, .Return and .Operators; the negative model is defined locally because the published Problem has a bounded return and a discount factor below one. A complete development needs the Ionescu-Tulcea construction of the history laws (already encoded as iterated composition products), monotone convergence for kernels, the measurable-selection step behind milestone 2, and a pigeonhole argument over the essentially finite action classes. The model and the Markov-reduction milestone are reusable by the other missions of this series. Proofs of any milestone, and alternative routes to milestone 2, are welcome.

Selected references

• R. E. Strauch, Negative Dynamic Programming, The Annals of Mathematical Statistics 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, Discounted Dynamic Programming, The Annals of Mathematical Statistics 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. http://web.mit.edu/dimitrib/www/soc.html

Motivation

Many problems in optimization and equilibrium modelling reduce to a system of nonsmooth equations $F(x)=0$ with $F:\mathbb R^n\to\mathbb R^n$ locally Lipschitz but not differentiable: reformulations of nonlinear complementarity problems, variational inequalities and Karush–Kuhn–Tucker systems through the $\min$ function or piecewise smooth maps. Newton-type methods for such systems replace the Jacobian by a directional derivative or a generalized Jacobian and globalize with a line search on the residual $\|F(x)\|$.

Global convergence theory for these methods typically shows that every accumulation point of the iterates is a zero of $F$ (or a stationary point of $\tfrac12\|F\|^2$). That leaves open whether the whole sequence converges. L. Qi's 1993 paper in Mathematics of Operations Research (DOI 10.1287/moor.18.1.227) answers this with an attraction theorem: a zero with a nondegenerate directional derivative, once approached, captures the whole sequence of any descent method whose steps are controlled by the residual.

Timeline. Robinson (1987) introduced the B-derivative (as recounted on p. 229 of Qi's paper); Pang (1990, DOI 10.1287/moor.15.2.311) proposed the damped B-derivative Newton method and proved a global convergence theorem under strong conditions at the limit point; Han, Pang and Rangaraj (1992, DOI 10.1287/moor.17.3.586) gave two further globally convergent descent algorithms; Qi and Sun (1993, DOI 10.1007/BF01581275) developed the semismooth Newton method. Qi's 1993 §5 shows that, for convergence of the entire sequence to a zero, BD-regularity at that zero suffices for all three methods, without semismoothness.

Setting

Throughout, $F:\mathbb R^n\to\mathbb R^n$ is locally Lipschitz and $\|\cdot\|$ is the Euclidean norm. The directional derivative of $F$ at $x$ in direction $h$ is the one-sided limit

$$F'(x;h)=\lim_{t\downarrow 0}\frac{F(x+th)-F(x)}{t}.$$

$F$ is directionally differentiable at $x$ if this limit exists for every $h$, and B-differentiable at $x$ if moreover

$$F(x+h)=F(x)+F'(x;h)+o(\|h\|)\qquad(h\to 0). \tag{2.2}$$

$F$ is BD-regular at $x$ if it is directionally differentiable there and $F'(x;h)\ne 0$ for every $h\ne 0$.

A descent direction method produces iterates $x^{k+1}=x^k+\alpha_kd^k$ with step sizes $\alpha_k\ge 0$ and directions $d^k$, and is monotone in the residual:

$$\|F(x^{k+1})\|\le\|F(x^k)\|. \tag{5.1}$$

A point $x^*$ is a limiting point of $\{x^k\}$ if some subsequence converges to it.

The damped Newton method (Algorithm 4.1) is the special case where $d^k$ solves $F(x^k)+F'(x^k;d^k)=0$ and $\alpha_k=\beta^{m_k}s$ is chosen by the Armijo rule on $g=\tfrac12\|F\|^2$.

Formalization targets

Goal: the attraction theorem (Theorem 5.1)

Let $F$ be locally Lipschitz and B-differentiable, $\{x^k\}$ a descent direction method satisfying (5.1), and $x^*$ a limiting point of $\{x^k\}$ with $F(x^*)=0$ and $F$ BD-regular at $x^*$. If there are $\delta_1,s,p>0$ such that $\|x^k-x^*\|\le\delta_1$ implies $\alpha_k\le s$ and

$$\|d^k\|\le p\,\|F(x^k)\|, \tag{5.2}$$

then

$$x^k\to x^*.$$

Milestones

1. Lemma 2.4. BD-regularity at $x$ gives a constant $c$ with $\|h\|\le c\|F'(x;h)\|$ for all $h$.
2. The local error bound (5.5). Near a B-differentiable zero $x^*$ with the constant $c$ of Lemma 2.4, $\|x-x^*\|\le 2c\|F(x)\|$.
3. The trapping step. For small $\epsilon$, the set $N(x^*,\epsilon)=\{x:\|x-x^*\|\le\epsilon,\ \|F(x)\|\le\epsilon/(2c+sp)\}$ is invariant under one step of the method.

Companions

• Corollary 5.2: a run of the damped Newton method with an accumulation point $x^*$ that is a zero, at which $\|h\|\le c\|F'(x;h)\|$ holds uniformly for $x$ near $x^*$, converges to $x^*$.
• Proposition 2.5: a BD-regular, semismooth zero is locally unique.
• The Han–Pang–Rangaraj bounds: the two direction-finding subproblems of Han, Pang and Rangaraj satisfy (5.2), with $p=1/l$ and $p=2L_1/c_1$.

Significance

The result. Global convergence theorems for line-search methods usually stop at "every accumulation point is a zero". The attraction theorem upgrades that to convergence of the entire sequence whenever the zero is BD-regular, under assumptions that are checked locally and that hold for several algorithms at once. For the damped Newton method it removes the semismoothness assumption needed for the superlinear local theory, at the price of saying nothing about the rate. The same pattern (local error bound plus residual-controlled steps gives capture) recurs in the convergence analysis of Levenberg–Marquardt and projection-type methods.

Formalizing it. The result is proved in the paper; to our knowledge none of it has been machine-checked. The formalization needs the one-sided directional derivative and B-differentiability, the passage from BD-regularity to a uniform constant, and the trapping argument for sequences with cluster points. These pieces are reusable for any convergence proof of nonsmooth Newton-type methods.

Difficulty

The obvious argument says: near $x^*$, steps are small because $\|F\|$ is small, so the iterates cannot leave. This fails as stated: a small residual at $x^k$ does not by itself prevent $x^k$ from being far from $x^*$, and without a lower bound of $\|F(x)\|$ in terms of $\|x-x^*\|$ the iterates could drift along a set where $F$ is small. The step that needs work is the error bound (5.5), which requires a uniform constant from the pointwise condition $F'(x^*;h)\ne0$, valid in a whole neighbourhood of $x^*$ and not only along the directions the iterates happen to take. The set $N(x^*,\epsilon)$ must also be chosen so that both its defining inequalities are preserved, which ties the radius to the residual through $2c+sp$.

Formalization scope

Points of $\mathbb R^n$ are EuclideanSpace ℝ (Fin n); norms are 2-norms; $n=0$ is allowed. The directional derivative is the published one-sided NonsmoothNewton.Local.dirDeriv; every statement that evaluates it does so at a point where existence is assumed (BD-regularity, B-differentiability), so the junk value of an undefined limit never enters. "Limiting point" is a cluster point of the sequence, not its limit. Condition (5.2) is assumed only for iterates within $\delta_1$ of $x^*$, as on the page.

Standing assumption and added hypotheses:

• local Lipschitz continuity of $F$ (§1 of the paper) is a hypothesis of every theorem;
• $\alpha_k\ge 0$ for all $k$ is added in Theorem 5.1 and the trapping step: "descent direction method" carries nonnegative steps implicitly, and the proof's bound $\alpha_k\|d^k\|\le sp\|F(x^k)\|$ needs it;
• in the second Han–Pang–Rangaraj bound, $c_1>0$ is stated (the page divides by it), the codomain of $G$ is $\mathbb R^n$ (the page prints $\mathcal R$), and the constant is $2L_1/c_1$ (the page's display has $cL_1/c_1$ before setting $p=2L_1/c_1$).

A trivializing formalization is ruled out: the goal does not assume that $x^k$ converges, that $\{x^k\}$ is bounded, that (5.2) holds globally, or that $F$ is semismooth; the hypotheses are jointly satisfiable (for $F=\mathrm{id}$, $x^{k}=2^{-k}v$, $d^k=-x^k$, $\alpha_k=\tfrac12$).

Definitions needed: directional differentiability, B-differentiability, BD-regularity, and for Corollary 5.2 the norm function, the Armijo test (4.1) and runs of Algorithm 4.1. Contributions to the general theory of one-sided directional derivatives of locally Lipschitz maps (Lipschitz continuity and positive homogeneity of $F'(x;\cdot)$) are welcome and will serve the companion missions of this series.

Selected references

• L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Mathematics of Operations Research 18(1):227–244, 1993. https://doi.org/10.1287/moor.18.1.227
• L. Qi and J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58:353–367, 1993. https://doi.org/10.1007/BF01581275
• J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15(2):311–341, 1990. https://doi.org/10.1287/moor.15.2.311
• S.-P. Han, J.-S. Pang and N. Rangaraj, Globally convergent Newton methods for nonsmooth equations, Mathematics of Operations Research 17(3):586–607, 1992. https://doi.org/10.1287/moor.17.3.586

Motivation

The Nelder–Mead simplex method (Nelder and Mead, 1965) minimizes a function $f:\mathbb R^n\to\mathbb R$ using function values only. It is among the most widely used derivative-free methods in practice, built into standard numerical libraries, and for decades it had essentially no convergence theory. Lagarias, Reeds, Wright and Wright (1998) gave the first systematic analysis of the method with fully specified tie-breaking rules. Their results are limited to low dimensions, and the limits are genuine: McKinnon (1998) constructed strictly convex functions on $\mathbb R^2$ with continuous derivatives on which the method converges to a point that is not the minimizer.

This mission formalizes the paper's two-dimensional analysis (§5) together with the general-dimension facts of §3 on which it rests. A companion series of missions treats the one-dimensional results of §4.

Setting

Fix coefficients of reflection $\rho$, expansion $\chi$, contraction $\gamma$ and shrinkage $\sigma$ with

$$\rho>0,\quad \chi>1,\quad \chi>\rho,\quad 0<\gamma<1,\quad 0<\sigma<1\qquad(2.1).$$

A simplex in $\mathbb R^n$ is a list of $n+1$ vertices $x_1,\dots,x_{n+1}$, ordered so that $f(x_1)\le\dots\le f(x_{n+1})$; $x_1$ is the best, $x_n$ the next-worst and $x_{n+1}$ the worst vertex, and $f_i=f(x_i)$. With $\bar x=\frac1n\sum_{i\le n}x_i$, the trial points are $z(\tau)=(1+\tau)\bar x-\tau x_{n+1}$; reflection, expansion, outside and inside contraction use $\tau=\rho,\ \rho\chi,\ \rho\gamma,\ -\gamma$.

One iteration of Algorithm NM computes $f_r=f(z(\rho))$ and then: accepts $x_r$ if $f_1\le f_r<f_n$; if $f_r<f_1$, accepts the better of $x_e=z(\rho\chi)$ and $x_r$ (the expansion point only if $f_e<f_r$); if $f_n\le f_r<f_{n+1}$, accepts $x_c=z(\rho\gamma)$ if $f_c\le f_r$; if $f_r\ge f_{n+1}$, accepts $x_{cc}=z(-\gamma)$ if $f_{cc}<f_{n+1}$. If no point is accepted, it shrinks: every vertex $x_i$ is replaced by $x_1+\sigma(x_i-x_1)$. An accepted point replaces $x_{n+1}$ and is inserted after every remaining vertex with value $\le$ its own; after a shrink, the new vertices are reordered, with $x_1$ kept first if no new vertex beats it. A run is a sequence $\Delta_0,\Delta_1,\dots$ of simplices produced by successive iterations.

The edge matrix of a simplex is $M=(x_1-x_{n+1}\ \cdots\ x_n-x_{n+1})$, the simplex is nondegenerate if $\det M\ne0$, its volume is $\operatorname{vol}(\Delta)=|\det M|/n!$, and its diameter is $\operatorname{diam}(\Delta)=\max_{i\neq j}\|x_i-x_j\|$. A function has bounded level sets if every $\{x:f(x)\le\mu\}$ is bounded. The standard method has $\rho=1$, $\chi=2$, $\gamma=\tfrac12$.

Formalization targets

Goal: Theorem 5.2 (p. 144)

For $f$ strictly convex on $\mathbb R^2$ with bounded level sets and the standard coefficients, from any nondegenerate initial triangle,

$$\lim_{k\to\infty}\operatorname{diam}(\Delta_k)=0.$$

The theorem does not claim that the triangles converge to a point, and the formalization does not claim it either.

Milestones

• General $n$ (§3). Lemma 3.3 (monotonicity of vertex values, existence and ordering of the limits $f_i^*$); Lemma 3.4 (broken convergence: $f_j^*<f_{j+1}^*$ freezes the first $j$ vertices); Corollary 3.1 (if the best vertex moves infinitely often, all $f_i^*$ coincide); Lemma 3.5 (no shrink on a strictly convex $f$); Lemma 3.6 ($f_n^*=f_{n+1}^*$ when $\rho\gamma<1$); Lemma 3.1 ($\operatorname{vol}(\Delta_{k+1})=|\tau|\operatorname{vol}(\Delta_k)$ after a step of type $\tau$, $\sigma^n\operatorname{vol}(\Delta_k)$ after a shrink).
• Dimension 2 (§5). Lemma 5.1 (if the best vertex never moves, the triangles converge to it); Theorem 5.1 ($f_1^*=f_2^*=f_3^*$ for $\rho=1$, $\gamma=\tfrac12$); Lemma 5.2 ($\operatorname{vol}(\Delta_k)\to0$ for the standard method).

Significance

Theorem 5.1 and Theorem 5.2 are among the few positive convergence statements for the Nelder–Mead method beyond dimension one. They show that on strictly convex functions in the plane the standard method cannot stall with a triangle of positive size; together with McKinnon's examples they delimit what can be proved: the simplices collapse, but not necessarily at the minimizer. The general-dimension lemmas of §3 (volume change, impossibility of shrinks on strictly convex functions, broken convergence) are used throughout the later literature on the method and its variants.

The results are proved on paper; no machine-checked proof of them is known. The formalization adds a precise, executable-in-principle definition of Algorithm NM with the paper's tie-breaking rules, and checked versions of statements whose printed form has small errors (see Formalization scope). The definition layer is reusable for any later work on simplex-based direct search.

Difficulty

The §3 lemmas are elementary but require bookkeeping of orderings, ties and change indices across iterations. The two-dimensional results are not. When the best vertex is eventually fixed (Lemma 5.1), the obvious measure of progress, the distance of the other vertices to it, is not monotone: reflections and outside contractions can move a vertex away, and contractions alternate in sign. Volume is also not monotone, because expansions double it. Lemma 5.2 and Theorem 5.2 depend on the precise acceptance rules: they are not known to hold for the original 1965 rule, which may accept an expansion point worse than the reflection point.

Formalization scope

Points are EuclideanSpace ℝ (Fin n); a simplex is Fin (n+1) → E n with 0-based indices, so index 0 is $x_1$, n-1 is $x_n$ and Fin.last n is $x_{n+1}$. Runs are a relation: the paper leaves the ordering after a shrink partly open ("whatever rule"), so every theorem quantifies over all runs satisfying the iteration relation from an ordered start. Every theorem assumes (2.1) and a nondegenerate start; §3 lemmas assume exactly what each states about $f$ (bounded below, strictly convex, or nothing), and every §5 item assumes strict convexity and bounded level sets. Limits $f_i^*$ are asserted as existence of limits or taken as Tendsto hypotheses, never through a default-valued limit operator. Volume and diameter are a determinant and a finite maximum, never a supremum over an unbounded set.

Committed conventions and corrections:

• The nonshrink ordering rule prints $j=\max\{\ell\mid f(v)<f(x_{\ell+1})\}$, which always yields the last position and contradicts the paper's own example on p. 118; it is encoded with $\min$ (insertion after all vertices of value $\le f(v)$).
• Lemma 3.3 (3)(ii) is stated for iterations after the last shrink; as printed ("for all $k$") it fails when an earlier shrink raised vertex values.
• Lemma 3.6 (2) is stated for $n\ge2$; for $n=1$ the next-worst vertex is the best vertex, which can stay fixed forever.
• Theorem 5.1 and Lemma 5.1 name only $\rho=1$, $\gamma=\tfrac12$ and are stated with $\chi$ general under (2.1); throughout §5, $\sigma\in(0,1)$ is general instead of $\tfrac12$. Shrinks never occur on strictly convex functions, so this is a harmless strengthening.

A run relation that no sequence satisfies would make every theorem vacuous; it is satisfiable from every ordered start, and the hypotheses of the goal are jointly satisfied by $f=\|x\|^2$ and a concrete triangle (checked in Lean, not part of the mission). Welcome contributions: proofs of the §3 lemmas, which are independent of each other except through Lemma 3.3, and the reusable facts behind them (volume of a simplex under the Nelder–Mead moves, strict convexity along trial lines).

Selected references

• J. C. Lagarias, J. A. Reeds, M. H. Wright, P. E. Wright, Convergence properties of the Nelder–Mead simplex method in low dimensions, SIAM J. Optim. 9(1):112–147, 1998. https://doi.org/10.1137/S1052623496303470
• J. A. Nelder, R. Mead, A simplex method for function minimization, Computer Journal 7(4):308–313, 1965. https://doi.org/10.1093/comjnl/7.4.308
• K. I. M. McKinnon, Convergence of the Nelder–Mead simplex method to a nonstationary point, SIAM J. Optim. 9(1):148–158, 1998. https://doi.org/10.1137/S1052623496303482
• V. Torczon, On the convergence of pattern search algorithms, SIAM J. Optim. 7(1):1–25, 1997. https://doi.org/10.1137/S1052623493250780

Motivation

The Nelder–Mead simplex method (Nelder and Mead, 1965) is a derivative-free method for unconstrained minimization. It keeps a simplex of $n+1$ points in $\mathbb R^n$ and replaces the worst vertex by a reflected, expanded or contracted trial point, using only comparisons of function values. It is one of the most widely used methods in practice, available in standard numerical libraries and scientific software, and it is also known for having very little supporting theory. McKinnon (1998) gave a strictly convex function in dimension 2 on which the method converges to a nonstationary point.

Lagarias, Reeds, Wright and Wright (1998) gave the first convergence results for the method as originally stated. In dimension 1 they proved that, for a strictly convex function with bounded level sets, both endpoints of the Nelder–Mead interval converge to the minimizer when $\rho\chi \ge 1$ (their Theorem 4.1). For the standard reflection coefficient $\rho = 1$ they proved more: the convergence is eventually M-step linear, with a number of steps that depends only on the expansion and contraction coefficients (their Theorem 4.2). This mission formalizes that rate result and the move-sequence lemmas it rests on.

Setting

Let $f:\mathbb R\to\mathbb R$. A one-dimensional simplex is a pair of vertices $\Delta = (x_1, x_2)$ ordered so that $f(x_1)\le f(x_2)$: $x_1$ is the best and $x_2$ the worst vertex. The method has four coefficients satisfying

$$\rho>0,\qquad \chi>1,\qquad \chi>\rho,\qquad 0<\gamma<1,\qquad 0<\sigma<1. \tag{2.1}$$

This mission fixes $\rho=1$, so (2.1) becomes $\chi>1$, $0<\gamma<1$, $0<\sigma<1$. The trial points are

$$x_r = x_1 + (x_1-x_2),\quad x_e = x_1 + \chi(x_1-x_2),\quad x_c = x_1 + \gamma(x_1-x_2),\quad x_{cc} = x_1 - \gamma(x_1-x_2).$$

With $f_1=f(x_1)$, $f_2=f(x_2)$, $f_r=f(x_r)$ and so on, one iteration is:

1. if $f_r<f_1$, an expansion accepting $x_e$ when $f_e<f_r$, and otherwise a reflection accepting $x_r$;
2. if $f_1\le f_r<f_2$, an outside contraction accepting $x_c$ when $f_c\le f_r$, and otherwise a shrink;
3. if $f_r\ge f_2$, an inside contraction accepting $x_{cc}$ when $f_{cc}<f_2$, and otherwise a shrink.

A shrink replaces $x_2$ by $x_1+\sigma(x_2-x_1)$. The worst vertex is discarded and the accepted point $v$ joins $x_1$; it becomes the best vertex exactly when $f(v)<f(x_1)$. Iterating from a nondegenerate initial pair $\Delta_0$ ($x_1\neq x_2$) gives the run $\Delta_0,\Delta_1,\ldots$, and $\operatorname{diam}(\Delta_k) = |x_1^{(k)}-x_2^{(k)}|$. A contraction means an outside or inside contraction.

Under $\rho=1$ each move multiplies the diameter by a fixed factor: $1$ for a reflection, $\chi$ for an expansion and $\gamma$ for either contraction. The paper's bracketing index $K$ (its Lemma 4.2) is the first iteration with $f_1^{(K)}\le f_e^{(K)}$. Two integers control the move sequences after $K$:

$$r^* = \lceil\chi-1\rceil,\qquad j^* = \max\{\,j\ge 0 : \chi+\chi^2+\cdots+\chi^j < N_{NM}\,\},\qquad N_{NM} = \max(\chi,1/\gamma).$$

Formalization targets

Goal: Theorem 4.2 (p. 130)

For all $\chi>1$ and $0<\gamma<1$ there is an integer $M$ such that for every $0<\sigma<1$, every strictly convex $f$ with bounded level sets and every nondegenerate ordered $\Delta_0$, the index $K$ exists and

$$\operatorname{diam}(\Delta_{k+M})\le \tfrac12\operatorname{diam}(\Delta_k)\qquad\text{for all }k\ge K.$$

The goal fixes no value of $M$; the paper's proof gives one, but any $M$ depending only on $\chi$ and $\gamma$ proves the theorem.

Milestones

1. Lemma 4.6 (p. 131): at most $r^*$ consecutive reflections, and no expansion immediately after a reflection.
2. Corollary 4.1 (p. 131): a contraction occurs at some iteration in $[K, K+r^*]$.
3. Lemma 4.7 (p. 132): after a contraction, no block of consecutive expansions is longer than $j^*$.
4. Lemma 4.8 (p. 133): there is $\varphi<1$ depending only on $\chi,\gamma$ such that the simplex after a contraction and the simplex after the next contraction satisfy $\operatorname{diam}(\Delta')\le\varphi\operatorname{diam}(\Delta)$.

Significance

Theorem 4.2 is a rate statement for a method whose global behaviour is mostly unexplained. It shows that in dimension 1 with $\rho=1$ the method behaves like a bracketing line search: once the minimizer is bracketed, the interval shrinks geometrically, and the number of iterations per halving is bounded independently of $f$ and of the starting interval. With the standard coefficients $\chi=2$, $\gamma=\tfrac12$ the value of $M$ constructed in the paper's proof is $M=4$. The intermediate lemmas describe which move sequences the method can produce after the minimizer is bracketed.

The paper's results are proved; to our knowledge none of them has a machine-checked proof. This mission produces a formal model of the one-dimensional method with the paper's tie-breaking rules, and formal statements of the rate theorem and its supporting lemmas. Proving them is the remaining work, including the one-dimensional bracketing and proximity results of the paper's §4.2, which the proofs use and which are posed as a separate mission of this series.

Difficulty

The rate does not follow from a per-iteration bound: a reflection keeps the diameter and an expansion multiplies it by $\chi>1$, so the diameter can grow for several consecutive iterations. A contraction-only argument fails for this reason. The theorem needs a bound on how long the method can avoid contracting and on how much expansion can happen between two contractions. Both bounds come from strict convexity applied along the line through the current interval, together with the location of the minimizer relative to the vertices (the proximity property of §4.2), and they must hold uniformly in $f$. Making the constants uniform, so that $M$ and $\varphi$ depend only on $\chi$ and $\gamma$, is the delicate part. Before $K$ no such control holds, which is why the theorem only speaks about $k\ge K$.

Formalization scope

The state is an ordered pair p : ℝ × ℝ with p.1 the best vertex $x_1$ and p.2 the worst vertex $x_2$; run f 1 χ γ σ p0 k is $\Delta_k$, and moveAt f χ γ σ p0 k is the type of iteration $k$. The coefficient $\rho=1$ is substituted into the algorithm. The ordering rule is the paper's insertion rule (new point first iff $f(v)<f(x_1)$, ties to the higher index); the printed formula $j=\max\{\ell \mid f(v)<f(x_{\ell+1})\}$ contradicts the paper's own example on p. 118 and is read as its words describe. The expansion step accepts the better of $x_r$ and $x_e$, the outside contraction is accepted on $f_c\le f_r$, the inside contraction on $f_{cc}<f_2$.

Standing assumptions carried by every statement: (2.1) with $\rho=1$; $f$ strictly convex on $\mathbb R$ (StrictConvexOn ℝ Set.univ f); bounded level sets ($\{x : f(x)\le\mu\}$ bounded for every $\mu$); and $\Delta_0$ nondegenerate and ordered. Corollary 4.1 prints only $\rho=1$; the remaining conditions of (2.1) are the section's standing assumptions. $r^*$ is the natural-number ceiling $\lceil\chi-1\rceil$; $j^*$ is computed by a bounded search over $0\le j\le\lceil N_{NM}\rceil$, which loses nothing for $\chi>1$. The uniformity of $M$ in Theorem 4.2 and of $\varphi$ in Lemma 4.8 is encoded by quantifier order: they are chosen after $\chi,\gamma$ and before $\sigma$, $f$, $\Delta_0$.

The goal's conclusion includes the existence of the bracketing index $K$ (the paper's Lemma 4.2), so the halving claim cannot hold vacuously for a run that is never bracketed; a statement that lets $M$ depend on $f$ or $\Delta_0$ is a different and much weaker theorem and is ruled out by the quantifier order.

A complete development needs: the one-dimensional facts about strictly convex functions (the paper's Lemma 4.1), the absence of shrink steps under strict convexity (Lemma 3.5 for $n=1$), the bracketing and proximity lemmas of §4.2, and the move-sequence and diameter-product arguments of §4.3. The model of the one-dimensional method and the convexity lemmas are reusable for the series' first mission (convergence of both endpoints). Proofs of individual milestones, and of the §4.2 lemmas as local results, are welcome.

Selected references

• J. C. Lagarias, J. A. Reeds, M. H. Wright, P. E. Wright, Convergence properties of the Nelder–Mead simplex method in low dimensions, SIAM J. Optim. 9(1):112–147, 1998. https://doi.org/10.1137/S1052623496303470
• J. A. Nelder, R. Mead, A simplex method for function minimization, Computer Journal 7(4):308–313, 1965. https://doi.org/10.1093/comjnl/7.4.308
• K. I. M. McKinnon, Convergence of the Nelder–Mead simplex method to a nonstationary point, SIAM J. Optim. 9(1):148–158, 1998. https://doi.org/10.1137/S1052623496303482

Motivation

The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an $L$-dimensional vector, and no simple policy is optimal.

Its structure has a long history:

• Karlin and Scarf (1958) formulated the model and showed, for lead time one and continuous demand, that the optimal order decreases in on-hand inventory with slope bounded by one.
• Morton (1969) extended these qualitative properties to general lead times, again by differentiating the optimal cost function, which required smooth demand distributions.
• Zipkin (2008), the paper formalized here, recovered and unified both results with a change of state variables and a single structural property, L♮-convexity, from discrete convex analysis (Murota 2003). The argument needs no smoothness and works for discrete as well as continuous demand.

Setting

Time is discrete. In each period the order due arrives, a new order $z\ge0$ is placed, demand $d\ge0$ occurs, and a holding or penalty cost is charged. The lead time $L\ge1$ is an integer. The original state $x=(x_0,\dots,x_{L-1})$ records on-hand inventory $x_0$ followed by the orders in transit. Demands are independent with a common law $\mu$. The costs are linear and stationary: unit procurement cost $c$, unit holding cost $\hat h$, unit lost-sales penalty $p$, and discount factor $\gamma$.

The transformed state is the vector of partial sums $v_l=\sum_{k=l}^{L-1}x_k$, $0\le l<L$, with the convention $v_L=0$. It ranges over the cone

$$V=\{v\in\mathbb R^L : v_0\ge v_1\ge\dots\ge v_{L-1}\ge 0\}.$$

The transformed order is $\zeta=-z\le0$. With $e$ the all-ones vector, the state moves to

$$v_+=\big([v_0-v_1-d]^+ + v_1,\ v_2,\ \dots,\ v_{L-1},\ 0\big)-\zeta e .$$

The one-period cost is $\hat q(u)=\hat hu^+ + pu^-$ on $u=y-d$, where $y=v_0-v_1$ is the on-hand stock, and $\hat q^0(y)=E[\hat q(y-d)]$. With $k$ periods to go, the optimal cost functions are

$$\bar f_0\equiv0,\qquad \bar g_k(v,\zeta)=-\gamma^Lc\zeta+\hat q^0(v_0-v_1)+\gamma E\big[\bar f_k(v_+)\big],\qquad \bar f_{k+1}(v)=\inf_{\zeta\le0}\bar g_k(v,\zeta).$$

A function $\varphi$ is submodular on a set $S\subseteq\mathbb R^n$ if $\varphi(x\vee y)+\varphi(x\wedge y)\le\varphi(x)+\varphi(y)$ for all $x,y\in S$, with $\vee,\wedge$ the componentwise maximum and minimum. A function $f:V\to\mathbb R$ is L♮-convex if $\psi(v,\zeta)=f(v-\zeta e)$ is submodular on $V\times\Re^-$. A function $g(v,\zeta)$ on $V\times\Re^-$ is L♮-convex if $g\big((v,\zeta)-\xi(e,1)\big)$ is submodular in $(v,\zeta,\xi)$ over $v\in V$, $\zeta\le\xi\le0$.

Formalization targets

Goal: Theorem 4 (p. 939)

For every number of periods to go $k$,

$$\bar f_k \text{ is L♮-convex on } V \quad\text{and}\quad \bar g_k \text{ is L♮-convex on } V\times\Re^- .$$

The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.

Milestones, in the order the proof uses them

1. Lemma 1 (p. 938): if $f(v)$ is L♮-convex, so is $\psi(v,\zeta)=f(v-\zeta e)$.
2. Lemma 2 (p. 939): if $g(v,\zeta)$ is L♮-convex, so is $f(v)=\min_{\zeta\le0}g(v,\zeta)$.
3. Optimal filling (proof of Theorem 4): in the end-of-period program (3), filling as much demand as possible is optimal ($a=\min\{d,v_0-v_1\}$). Consequently $\bar\kappa_t(v,\zeta\mid d)=\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+)$.
4. $\psi_t$ is L♮-convex: the objective $\psi_t(v_+,v,\zeta)=\hat h(v_+-v_1)+p(v_+-v_0+d)+\gamma\bar f_{t+1}[(v_+,v_2,\dots,v_{L-1},0)-\zeta e]$ of program (4) is L♮-convex on its constraint set.
5. $\bar\kappa_t$ is L♮-convex: the end-of-period cost $\bar\kappa_t(v,\zeta\mid d)$ is L♮-convex in $(v,\zeta)$ for each $d$.
6. $\bar g_t$ is L♮-convex: if $\bar f_{t+1}$ is L♮-convex, so is $\bar g_t=-\gamma^Lc\zeta+E_d[\bar\kappa_t]$, by (5).

Significance

The result. L♮-convexity of $\bar f_t$ implies that $\bar f_t$ is submodular and convex in the transformed state. L♮-convexity of $\bar g_t$ yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order $\bar z_t(v)$ is nonincreasing in $v$ and changes by at most $\omega$ when every component of $v$ increases by $\omega$. These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:

• a formal L♮-convexity theory on real cones (the shift characterization, its preservation under partial minimization, and its preservation under expectation);
• a checked version of the induction behind Theorem 4;
• a verified model of the lost-sales recursion in the transformed state, which missions on Corollary 5 and the later sections can import.

Difficulty

The obvious argument works with ordinary convexity and submodularity in the original state $x$. It stalls: the lost-sales transition $[x_0-d]^+$ is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in $x$. The paper's structure appears only in the partial sums $v$. Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over $\zeta$ (Lemma 2). Proving plain submodularity of $\bar f_t$ on $V$ therefore does not close the induction.

A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.

A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of $d\mapsto\bar f_k(v_+)$, and these come from the model rather than from the definitions.

Formalization scope

• Representation. States are functions Fin L → ℝ, indexed $0,\dots,L-1$ as in the paper. A helper returns $v_l$ for $l<L$ and $0$ at $l=L$. A function $g(v,\zeta)$ is encoded on Fin (L+1) → ℝ with $\zeta$ last. The objective $\psi_t$ of (4) is encoded on Fin (L+2) → ℝ with coordinates $(v_+,v_0,\dots,v_{L-1},\zeta)$. The order is componentwise.
• L♮-convexity on a domain $D$: $(x,\xi)\mapsto f(x-\xi e)$ is submodular on $\{\xi\le0,\ x\in D,\ x-\xi e\in D\}$, with $e$ the all-ones vector on every coordinate. For $D=V$ this is the paper's definition verbatim. This is the paper's definition, not Murota's translation-submodularity form, and it is stated on real vectors. The platform's discrete-convexity library (DiscreteConvex.LConvexFunctions.*) works on $\mathbb Z^V$ with values in $\mathbb R\cup\{+\infty\}$, a different domain and definition, and is not reused.
• Time. Data are stationary, so the paper's $\bar f_t$ depends on $t$ only through the number of periods to go $k=T+L+1-t$, and "for all $t$" is "for all $k$". The minimum over $z\ge0$ is taken in every period, as printed in (1).
• Explicit readings of the paper's phrases.
  • "min" (over $\zeta\le0$, over $v_+$, over $(a,w)$) is an infimum over the constraint set. In the model every cost is nonnegative, so the infimum is genuine. The generic Lemma 2 assumes the values bounded below, and the generic milestone 5 assumes the continuation nonnegative on $V$.
  • "the $d_t$ are independent and nonnegative": one law $\mu$ with $\mu(-\infty,0)=0$, since data are stationary.
  • "unit cost", "discount rate": $c,\hat h,p\ge0$ and $0<\gamma\le1$.
  • Finite mean demand is added: without it $\hat q^0$ is infinite.
  • "the optimal $a=\min\{d,v_0-v_1\}$": stated as the equality of the infimum of program (4) with its value at $v_+=\max(v_0-d,v_1)$.
• Ruled out. A statement that holds because a value function is the junk constant $0$ (constants are L♮-convex), plain submodularity on $V$ in place of the shift condition, quantification over all of $\mathbb R^L$ instead of $V$, and a goal about an arbitrary function assumed to satisfy the recursion. None of these is the paper's theorem; the goal is stated for the recursion itself.
• Not in scope. "L♮-convex implies convex" for a generic function, which is false without regularity (a non-measurable additive function is L♮-convex in this sense); Lemma 3 and Corollary 5, for a follow-up mission that references Theorem 4; the smooth-case Hessian discussion; the infinite-horizon remarks.
• Welcome contributions. Reusable lemmas on submodularity over sublattices of $\mathbb R^n$ (partial minimization, Topkis 2.7.6), on preservation of submodularity under integration, and on measurability of the value functions.

Selected references

• P. Zipkin, On the structure of lost-sales inventory models, Operations Research 56(4) (2008) 937–944. https://doi.org/10.1287/opre.1070.0482
• S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• T. E. Morton, Bounds on the solution of the lagged optimal inventory equation with no demand backlogging and proportional costs, SIAM Review 11(4) (1969) 572–596. https://doi.org/10.1137/1011090
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.