Optimization

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.

Why processor speed changes the scheduling problem

A processor can save energy by running slowly when work is light, but a deadline may force it to run faster. Yao, Demers, and Shenker formulated this tradeoff as an offline and online scheduling problem for a variable-speed processor in their 1995 FOCS paper. Their Average Rate Heuristic (AVR) uses only each job's arrival, deadline, and required work to set speed. This mission formalizes their quadratic-power analysis: AVR's worst-case energy is at least four and at most eight times the minimum possible energy. The authors prove these bounds in Theorem 2, rather than an exact value.

The question matters when an online scheduler must choose speed before seeing later jobs. Deadline feasibility alone does not measure energy: processing the same number of cycles at twice the speed for half as long can cost more when power grows superlinearly. The paper's model isolates that dependence in a power function $P(s)$, so the competitive guarantee measures the energy price of AVR's speed choices. The initial motivation, model, and heuristic are in §§1–4 of the paper.

Jobs, schedules, and the average-rate rule

Fix a nondegenerate time window $[t_0,t_1]$. A finite job instance $J$ assigns each job $j$ an arrival time $a_j$, deadline $b_j>a_j$, and nonnegative required work $R_j$ in CPU cycles. Every job window $[a_j,b_j]$ lies inside $[t_0,t_1]$. A schedule $S=(s,\operatorname{job})$ has nonnegative processor speed $s(t)$ and selects at most one job at each time. Speed and job selection are constant between finitely many breakpoints. The schedule is feasible if each job receives its full work inside its own window:

$$\int_{a_j}^{b_j}s(t)\,\mathbf 1\{\operatorname{job}(t)=j\}\,dt=R_j \qquad\text{for every }j.$$

For a power function $P$, its energy is $E_P(S)=\int_{t_0}^{t_1}P(s(t))\,dt$. An optimal schedule minimizes this quantity among feasible schedules. These definitions follow §2, p. 375. The intensity of an interval $[z,z']$ is the total work of jobs whose full windows it contains, divided by $z'-z$. An interval with maximum intensity is critical; Theorem 1 identifies the processor speed on that interval in an optimal schedule §3, p. 375.

Each job's density is $d_j=R_j/(b_j-a_j)$, extended as a step function equal to $d_j$ on $[a_j,b_j]$ and zero elsewhere. AVR runs at speed $\sum_j d_j(t)$ and chooses the earliest-deadline available job. For quadratic power, its energy is

$$\operatorname{AVR}(J)=\int_{t_0}^{t_1}\left(\sum_jd_j(t)\right)^2dt.$$

The competitive ratio is the least upper bound of $\operatorname{AVR}(J)/\operatorname{OPT}(J)$ over instances, where $\operatorname{OPT}(J)$ is the least feasible energy §4, p. 376, Eq. (2).

Formalization targets

The goal is the paper's Theorem 2, p. 381:

$$4\le r\le 8\qquad(P(s)=s^2).$$

The upper bound compares AVR with every feasible schedule. The lower bound says that every constant strictly below four is exceeded by the AVR-to-feasible-energy ratio on some instance. This formulation does not claim that one finite instance attains four.

The milestone path follows the paper: Theorem 1 characterizes optimal speed; Lemma 5.1 reduces to jobs of type A or B; Eq. (5) splits their costs; Lemma 5.2 and Eq. (7) control the A contribution; Lemmas 5.3–5.6 reduce the analysis to canonical instances; Lemma 5.8 supplies a matrix bound; Lemma 5.7 gives $F_A\le4\operatorname{OPT}_A$ and $F_B\le4\operatorname{OPT}_B$; Example 2 approaches the lower constant. These statements and their order come from §5, pp. 378–381. The paper also states a higher-power result, Theorem 3, for real $p\ge2$:

$$p^p\le r_p\le 2^{p-1}p^p.$$

That result is a companion item. The extended abstract leaves its full proof to a longer paper §6, pp. 381–382.

What the bounds provide

The upper bound guarantees that AVR's energy is controlled by a fixed multiple of the offline optimum for every finite job set, even though AVR sets speed from individual job densities. The lower family rules out a guarantee below four for this heuristic. Together they delimit the performance of AVR under quadratic power; they do not give its exact worst-case ratio. The A/B reductions and the tree-induced matrix estimate are useful mathematical interfaces for later analyses of interval-structured schedules.

The paper proves Theorem 2 in the mathematical sense. This mission supplies machine-checkable statements and definitions, with proofs left open for solvers. Closing it requires formal proofs of the reduction steps, the matrix estimate, and the limiting example, plus an explicit connection from the optimal-schedule analysis to comparison with every feasible schedule. No completed Lean proof is claimed here.

The main difficulty

The simple calculation $\left(\sum_j d_j(t)\right)^2$ exposes overlap between job windows but does not say how that overlap compares with an optimal schedule. An optimal schedule may run jobs in a different order and may preempt them. The paper therefore changes the instance while preserving the optimal speed profile: it first separates cumulative execution into two types, then reduces to single execution intervals and specially aligned, nested windows. The matrix inequality controls the resulting expression. A pointwise comparison of AVR speed with optimal speed cannot replace these reductions, because an optimal schedule can concentrate work on critical intervals while AVR spreads each job's density across its entire window §5, pp. 377–381.

Formalization scope

Jobs use Fin n, allowing the empty instance. The instance requires $t_0<t_1$, $a_j<b_j$, containment in the window, and $R_j\ge0$. A schedule uses real-valued speed and an optional job label; none denotes no assigned job. Its piecewise-constant requirement is witnessed by finitely many increasing breakpoints. Values at breakpoints are unrestricted by the piecewise-constant clauses, and speed comparisons in the theorems are almost-everywhere statements. Job windows are closed, as printed; endpoints do not affect the integrals. A schedule may have positive speed while no job is assigned, since the source does not equate idleness with zero speed.

Every energy expression is a real interval integral. The schedule conditions ensure the integrands in theorem hypotheses are piecewise constant away from finitely many points. Density denominators are positive. An execution-speed quotient for a zero-work job can have zero denominator, in which case Lean returns zero; such a job contributes no executed work. The goal uses quantified comparisons with feasible schedules rather than a real infimum, and Lemma 5.6 uses all upper bounds on a nonempty canonical family rather than a real supremum. The lower bounds quantify over every smaller constant, avoiding a false attainment claim. These choices guard against default values for empty or unbounded extrema.

Theorem 1's printed convexity hypothesis is strengthened to strict convexity and nondecreasing power on nonnegative speeds: its stated speed uniqueness fails for a linear power function, and a decreasing power function rewards idle speed. This repair is explicit in that item's description. Existence of a quadratic optimum is included as a milestone from the algorithm of §3, although it is not a separately numbered theorem. Example 2 includes the variable exponent $e\ge1$, the limiting ratios at $e=1$ and $e=3/2$, and an eventual upper bound of four across the family. The A-job order resolves exact ties by index. For canonical and tree-induced nesting, intervals that meet only at an endpoint count as disjoint; this admits the paper's displayed four-interval matrix.

The development needs Mathlib's real interval integrals, finite sums, measures of intervals, matrix eigenvalues, and real-power limits. The finite schedule model, canonical-instance data, and tree-induced matrix interface can be reused beyond this particular ratio bound. Contributions may establish these interfaces' elementary properties, the paper's milestone theorems, or independent proofs of the goal, provided they preserve the stated job and schedule classes.

Selected references

• Frances Yao, Alan Demers, and Scott Shenker, A Scheduling Model for Reduced CPU Energy, Proceedings of the 36th IEEE Symposium on Foundations of Computer Science, 1995, pp. 374–382. DOI 10.1109/SFCS.1995.492493.

Motivation

Many optimization models combine a smooth loss with a convex penalty or constraint. The penalty can be nonsmooth: an absolute-value penalty encourages sparse solutions, while an indicator function enforces a feasible set. A coordinate gradient descent (CGD) method updates selected coordinates by minimizing a quadratic model and then applies a line search. Tseng and Yun studied this method for an extended-valued convex penalty, including penalties that separate by blocks of coordinates. Their global convergence result addresses a basic question for such an iteration: if its iterates have an accumulation point, must that point satisfy the first-order stationarity condition? The result and examples appear in Tseng and Yun (2009).

Coordinate updates are appealing when changing a small block is cheaper than changing the whole vector. Their convergence is delicate when the penalty is nonsmooth: a direction can be useful on one block without revealing whether the full point is stationary. The paper's Theorem 1(e) establishes a guarantee for a generalized Gauss–Seidel selection rule and a block-separable penalty. The authors note that this rules out cycling on Powell's coordinate-minimization example under their stated conditions Tseng and Yun (2009), p. 404.

Setting

Let $x\in\mathbb R^n$, $c>0$, and let $P:\mathbb R^n\to(-\infty,+\infty]$ be proper, convex and lower semicontinuous. Its effective domain $D=\operatorname{dom}P$ contains precisely the points where $P$ is finite. Let $f$ be continuously differentiable on an open set containing $D$. The objective is $F_c(x)=f(x)+cP(x)$, with value $+\infty$ outside $D$. No convexity of $f$ is assumed.

At iteration $k$, choose a nonempty set of coordinates $\mathcal J^k$ and a positive-definite symmetric matrix $H^k$. The search direction $d^k$ minimizes

$$\nabla f(x^k)^\top d+\tfrac12 d^\top H^k d+cP(x^k+d) \quad\text{subject to }d_j=0\text{ for }j\notin\mathcal J^k.$$

The next iterate is $x^{k+1}=x^k+\alpha^k d^k$. The Armijo rule tests the geometric sequence $\alpha^k_{\mathrm{init}}\beta^j$ and takes its largest accepted member, using the paper's decrease quantity $\Delta^k=\nabla f(x^k)^\top d^k+\gamma(d^k)^\top H^kd^k+cP(x^k+d^k)-cP(x^k)$. Its parameters satisfy $\alpha^k_{\mathrm{init}}>0$, $0<\beta,\sigma<1$, and $0\le\gamma<1$. The accepted step obeys $F_c(x^{k+1})\le F_c(x^k)+\sigma\alpha^k\Delta^k$.

The generalized Gauss–Seidel rule means that some fixed number $T\ge1$ of consecutive coordinate sets covers every coordinate, starting at every iteration. The penalty is block-separable with respect to $\mathcal J^k$ when it is the sum of a proper closed convex function of the selected coordinates and another of their complement. A point $\bar x$ is stationary when it lies in $D$ and the one-sided directional derivative $F_c'(\bar x;v)$ is nonnegative for every direction $v\in\mathbb R^n$.

Formalization targets

Global convergence under generalized Gauss–Seidel selection

The goal is Theorem 1(e) Tseng and Yun (2009), p. 399. Under the CGD and Armijo rules, Assumption 1's uniform matrix bounds, a positive lower bound on the initial trial steps, block separability for each chosen coordinate set, and a finite upper bound on the accepted steps,

$$\bar x\text{ a cluster point of }\{x^k\}_{k\ge0} \quad\Longrightarrow\quad F_c'(\bar x;v)\ge0\text{ for every }v\in\mathbb R^n.$$

The mission milestones state the paper's Lemma 1, its Armijo existence claim after equation (10), Lemmas 2 and 3, and Theorem 1(a) and (b). They connect the direction subproblem, descent, stationarity and subsequence behavior to the goal. The theorem asserts stationarity of every cluster point; it does not assert that a cluster point exists or that the full sequence converges.

Significance

The result supplies a global first-order guarantee for a block update method even when the smooth part $f$ is nonconvex. It applies to extended-valued convex penalties, so the same statement covers both nonsmooth regularization and constraints represented by indicator functions. The bounded-window coverage condition allows varying coordinate sets rather than a fixed cyclic schedule Tseng and Yun (2009), Theorem 1(e).

The paper proves the theorem. This mission asks for a machine-checked Lean proof of that known claim and its selected supporting results. The reusable output includes a precise interface for an extended-valued penalty, the exact quadratic coordinate subproblem, Armijo backtracking with first accepted exponent, and the distinction between a convergent subsequence and a cluster point. The current draft statements compile with proof placeholders; they are proof obligations, not completed machine-checked results.

Difficulty

The descent bound alone controls decrease in objective value; it does not directly show that every coordinate has a vanishing stationarity residual. The coordinate set may vary at each iteration, and the penalty need only separate with respect to the current block. A cluster point may be reached along a subsequence that samples only one of those blocks. The argument therefore has to connect behavior along a convergent subsequence to nearby iterations within a full coverage window. The nonsmooth penalty also prevents replacing directional stationarity by a statement solely about an ordinary gradient.

Formalization scope

Vectors use EuclideanSpace ℝ (Fin n) and its Euclidean norm; Fin n starts at zero, whereas the paper numbers coordinates from one. A penalty is represented by its effective domain $D$ and finite values $P$ on $D, using the published `ProxNewton.Inexact.IsProperClosedConvex` definition. Every objective comparison includes domain membership; values outside$D$are interpreted as$+\infty$. The smoothness assumption names an open neighborhood of$D$. The direction$d_H(x;\mathcal J)$is chosen from the exact minimizers; all theorem uses place$x$in$D$and$H$ positive definite. A CGD run records the chosen minimizers, so it does not rely on any unspecified value of that choice outside its valid inputs.

The Armijo predicate records the first successful geometric trial, including rejection of all earlier trials. The matrix bounds in Assumption 1 are quadratic-form bounds. Lemma 3 represents eigenvalue extremes by Rayleigh quotients on the selected coordinates; its generalized spectrum is that of the pair of principal submatrices. These extrema are used only with a nonempty block and positive-definite matrices. The paper's $o(\alpha)$ is represented by a remainder whose quotient by $\alpha$ tends to zero from the right. In Lemma 1 the line segment remains in $D$. A convergent subsequence is indexed by a strictly increasing map; a cluster point is represented separately by MapClusterPt.

No convergence of the entire iterate sequence is assumed. Stationarity requires the nonnegative directional derivative in every direction, not only the coordinates selected at one step. A valid development needs convex analysis of the subproblem, estimates for positive-definite quadratic forms, properties of lower semicontinuity and directional derivatives, and finite-dimensional subsequence arguments. Contributions proving those reusable facts and the named milestones are within scope.

Selected references

• Paul Tseng and Sangwoon Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming, Series B 117 (2009), 387–423. DOI: 10.1007/s10107-007-0170-0.

Motivation

Demand for many products is not stationary: it rises and falls with the economy, the season, a product's life cycle or a customer's state. Song and Zipkin (1993) (DOI 10.1287/opre.41.2.351) model this by a world-driven demand process: an exogenous Markov chain $A$ (the "state of the world") whose current state sets the rate of a Poisson demand stream. The model contains the classical stationary inventory model as the case of one world state, and it is a standard example of a Markov-modulated decision problem in operations research.

For stationary demand with a fixed order cost, optimal $(s, S)$ policies go back to Scarf (1960) for finite horizons and Iglehart (1963) for the infinite horizon; Veinott (1966) bounded the optimal parameters by quantities computed from the one-period cost alone. This mission formalizes the extension of both results to the fluctuating-demand model (§3.2 of the paper). A companion mission treats the linear order-cost case, in which a world-dependent basestock policy is optimal.

Setting

The world $A$ is a continuous-time Markov chain on a countable set $I$ with generator $(q_{ij})$, $q_i = -q_{ii} = \sum_{j\neq i} q_{ij}$, and bounded rates. While $A = i$, unit demands arrive at Poisson rate $\lambda_i$; shortages are backlogged. An order arrives after a random lead time $L$, independent of the world and the demand. The inventory position $x \in \mathbb Z$ is on-hand stock minus backorders plus stock on order.

Costs: a fixed cost $\bar K$ per order and a unit cost $\bar c$, both paid on arrival; a holding cost rate $h > 0$ and a penalty cost rate $p > 0$; a discount rate $\alpha > 0$. With $\tilde F_L(\alpha) = E[e^{-\alpha L}]$, the discounted costs are $c = \bar c\tilde F_L(\alpha)$ and $K = \bar K\tilde F_L(\alpha)$. If $D^i_L$ is the demand during a lead time from world state $i$ and $\hat C(x) = \max\{-px, hx\}$,

$$C(i, y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big].$$

Uniformization at a rate $\mu \ge \sup_i q_i + \sup_i\lambda_i$ turns the problem into a discrete-time dynamic program with $\beta = 1/(\mu+\alpha)$, $\gamma = \beta\mu$ and the myopic cost $G^+(i, y) = (1-\gamma)cy + \beta C(i, y)$. For a terminal cost $W_0$ the $n$-stage costs satisfy the recursion (10):

$$W_n(i, x) = \min_{y\ge x}\{K\delta(y-x) + G_n(i, y)\},$$ $$G_n(i, y) = G^+(i, y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i, y-1) + \sum_{j\neq i} q_{ij}W_{n-1}(j, y) + (\mu - \lambda_i - q_i)W_{n-1}(i, y)\Big\},$$

where $\delta(z) = 1$ if $z > 0$ and $\delta(0) = 0$. Throughout, Assumption 1, $\alpha\bar c < p$, holds and $K > 0$. The terminal cost is the optimal cost $W_\infty$ of the linear model ($K = 0$); its $G_\infty$ is written $G_0$, and $y^*(i)$ is the smallest minimizer of $G_0(i, \cdot)$.

A function $f : \mathbb Z \to \mathbb R$ is $K$-convex (Definition 2) if $\frac{f(x)-f(x-b)}{b}a + f(x) \le f(x+a) + K$ for all $x$ and all integers $a, b > 0$. The $(r, S)$ policy with parameters $\{(r(i), S(i))\}$ orders up to $S(i)$ when $x \le r(i)$ and the world is in state $i$, and does not order otherwise. With $y^+(i)$ the smallest minimizer of $G^+(i,\cdot)$ and $y^+_{\min} = \min_i y^+(i)$, the paper defines

$$\begin{aligned} S^+(i) &= \min\{y \ge y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > \gamma K\},\\ r^+(i) &= \max\{y < y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > (1-\gamma)K\},\\ r^-(i) &= \max\{y < y^*(i) : G_0(i, y) - G_0(i, y^*(i)) > K\},\\ r^{--}(i) &= \max\{y < y^+_{\min} : G^+(i, y) - G^+(i, y^+_{\min}) > K\}. \end{aligned}$$

Formalization targets

Goal: Theorems 5(e) and 6

Let $S^*_n(i)$ be the smallest minimizer of $G_n(i,\cdot)$ and $r^*_n(i)$ the largest $y < S^*_n(i)$ with $G_n(i, y) > K + G_n(i, S^*_n(i))$. For every $i$ the sequence $(r^*_n(i), S^*_n(i))$ has limit points; for any choice of limit points $(r^*(i), S^*(i))$, the world-dependent $(r, S)$ policy with these parameters is optimal for the infinite-horizon discounted problem, and

$$y^*(i) \le S^*(i) < S^+(i),\qquad r^{--}(i) \le r^-(i) \le r^*(i) \le r^+(i).$$

Milestones

Lemma 4 (uniform bounds on the iterates); Theorem 3 ($K$-convexity of $G_n$, $W_n$ and optimality of an $(r, S)$ rule for each $n$-stage problem); Lemmas 5 and 6 (difference comparisons); Theorem 4 (the bounds above for every $n$); Theorem 5(a)–(d) (convergence of $W_n$, $G_n$, the $(r, S)$ property of limit points, and the optimality equation (2)).

Significance

The result shows that the classical $(s, S)$ structure survives Markov modulation of demand with an infinite world space and stochastic lead times: a stationary policy whose two parameters depend only on the current world state is optimal over the infinite horizon. The bounds of Theorem 6 locate those parameters in an interval computed from the myopic cost $G^+$ and the linear model alone, uniformly in the horizon.

The results are proved in the paper, except that Theorem 5 refers to Iglehart (1963) and Lemma 4 to Song's thesis. To our knowledge none of them has a machine-checked proof. A formalization would also produce reusable machinery: $K$-convexity on the integers, the Scarf-type inductive argument with a countable world state, and the passage from finite-horizon to infinite-horizon optimality for a nonnegative-cost Markov decision process with unbounded costs.

Difficulty

The one-period cost is unbounded in $x$ and the world space may be infinite, so the usual contraction argument for discounted dynamic programs does not apply. Convergence of $W_n$ needs the uniform bound of Lemma 4. Optimality of the limit policy needs a separate argument, because a pointwise limit of $(r, S)$ rules need not exist: the parameter sequences are only known to have limit points. The lower bounds $r^-$ and $r^{--}$ hold only because the terminal cost is the linear model's optimal cost, which makes the difference comparisons of Lemma 6 possible; the paper notes that Lemma 6 depends on this choice of $W_0$.

Formalization scope

All definitions live in the namespace SongZipkinFluct.FixedCost. Inventory positions and order-up-to levels are integers. The demand law $D^i_L$ is defined through uniformization at rate $\mu$, as an exact series representation of the Markov-modulated Poisson count, and the lead time is a probability law on $[0,\infty)$ independent of the rest. The standing conventions $h, p, \alpha > 0$, $\bar c, \bar K \ge 0$, $\mu > 0$ and $\mu \ge q^* + \lambda^*$ are hypotheses of the model. Assumption 1 and $\bar K > 0$ are hypotheses of each theorem.

The iterates $W_n$ are defined by the recursion (10), with the minimum written as an infimum over integers $y \ge x$. $W_\infty$ and $G_\infty$ are the suprema over $n$, which are finite and equal the limits by Lemma 4 and Theorem 3. Every minimizer and every extremal integer ($y^+$, $y^+_{\min}$, $y^*$, $S^*_n$, $r^*_n$, $S^+$, $r^+$, $r^-$, $r^{--}$) is passed through its defining property, never through sInf/sSup on $\mathbb Z$. The goal also asserts that all of them exist, so its hypotheses can be met. A limit point of an integer sequence is a value taken infinitely often.

Optimality is over all deterministic history-dependent feasible policies and from every initial state. Costs are valued in $[0,\infty]$, and a policy's cost is the supremum of its finite-horizon discounted costs in the uniformized problem (1). Restricting the comparison to $(r, S)$ or stationary policies would trivialize the goal and is ruled out. $K$-convexity is the integer version of Definition 2, not convexity over $\mathbb Z$-scalars.

Welcome contributions: $K$-convexity calculus on $\mathbb Z$, convergence of the uniformized demand series, Lemma 4, and an Iglehart-type limit argument for countable-state Markov decision processes with nonnegative costs.

Selected references

• J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• A. F. Veinott, Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.