Optimization

Motivation

A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.

Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with $N$ products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector $y^*$; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general $N$-product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).

Setting

There are $N$ products and $N$ demand classes, both numbered $1,\dots,N$. Class $i$ can be served by product $j$ whenever $j \le i$, at a unit substitution cost $b$ when $j < i$. Each class $i$ has unit revenue $p_i$ and unit backorder cost $\pi_i$; each product $j$ has unit purchase cost $c_j$ and effective unit salvage value $s_j$ (salvage value minus holding cost, possibly negative). Put $a_{ji} = p_i$ if $j = i$, $a_{ji} = p_i - b$ if $j < i$, and $T_k = p_k + \pi_k - b$. The standing assumptions are: (1) $\pi_i + p_i \ge \pi_j + p_j$ for $i < j$; (2) $s_i \ge s_j$ for $i < j$; (3) $a_{ij} + \pi_j - s_i \ge 0$ for $i \le j$.

The sequence of events: the starting inventory $x$ is observed; stock is raised to $y \ge x$ at unit costs $c$; the demand vector $d$ is realized; stock is allocated to classes; leftovers are salvaged. For fixed $y$ and $d$ the allocation is the linear program

$$G(y,d) = \max \sum_{i}\sum_{j \le i} a_{ji} w_{ji} + \sum_i s_i v_i - \sum_i \pi_i u_i$$

subject to $u_i + \sum_{j\le i} w_{ji} = d_i$, $v_j + \sum_{i \ge j} w_{ji} = y_j$, and $w, u, v \ge 0$, where $w_{ji}$ is the amount of product $j$ given to class $i$, $u_i$ the shortage of class $i$ and $v_j$ the leftover of product $j$. The expected profit is

$$P(x,y) = -\sum_k c_k (y_k - x_k) + \mathbb E\, G(y, D),$$

and the ordering problem is $\max_{y \ge x} P(x,y)$; a maximizer is an optimal level $\bar y(x)$.

Allocation Algorithm (A) serves the classes in the order $1,2,\dots,N$, class $i$ first from product $i$ and then from the leftovers of products $i-1,\dots,1$. The subproblem shortage $S^k_j$ is the unmet demand of class $j$ when (A) runs on the classes $k,\dots,j$ with the products $k,\dots,j$ only; $\vec S^k_{a,n} = 0$ means $S^k_m = 0$ for all $a \le m \le n$. The paper's first partial derivatives of $P$ are sums of salvage values, substitution costs and the $T_k$, weighted by probabilities of such shortage events.

Formalization targets

Goal: Theorem 2

With $y^*$ a maximizer of $P(0,\cdot)$ over $y \ge 0$, every optimal level $\bar y$ for every starting inventory $x \ge 0$ satisfies

$$x_i \ge y^*_i \implies \bar y_i = x_i .$$

Milestones

• Proposition 1: Algorithm (A) is feasible and optimal for the allocation LP, and its value is $G(y,d)$.
• Proposition 2: $y \mapsto P(x,y)$ is concave and submodular on $\{y \ge 0\}$.
• Eq. (4): the explicit formula for $\partial P/\partial y_i$ in terms of shortage probabilities.
• Theorem 1: there is $y^* \ge 0$ with $\bar y(x) = y^*$ whenever $0 \le x \le y^*$.
• Lemmas 1, 2, 3, 5: identities and monotonicity properties of the shortage probabilities used to compare $\partial P/\partial y_i$ and $\partial P/\partial y_{i+1}$.

Significance

Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector $y^*$, computed once, determines the decision for every starting inventory in the region $x \le y^*$ and fixes the order of every overstocked product elsewhere. The paper builds its bounds on $y^*$, its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.

The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair $j = i+1$, and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.

Difficulty

The obvious argument for Theorem 2 is the one-dimensional one: if $x_i \ge y^*_i$ then $\partial P/\partial y_i \le 0$ at $\bar y$, so product $i$ should not be raised. It fails because $\partial P/\partial y_i$ depends on the other coordinates: at $\bar y$ some products are raised above $x$ and others kept at $x_j > y^*_j$, and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product $i$ propagates through the greedy allocation of every later class.

Formalization scope

Products and classes are indexed by Fin N (the paper's index $k$ is Lean index $k-1$); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs $w_{ji}$, $i < j$, forbidden (fixed to $0$), as in the paper's proof of Proposition 1; $G$ is the supremum of the LP objective. The demand law is a product $\nu_1 \otimes \dots \otimes \nu_N$. Submodularity is the lattice inequality $P(x, y \vee y') + P(x, y \wedge y') \le P(x,y) + P(x,y')$, which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.

Hypotheses the paper uses without stating, made explicit here:

• the substitution cost is nonnegative, $b \ge 0$ (Proposition 1 is false for $b < 0$);
• the demand classes are independent (product forms in Lemma 3 and Appendix B);
• each demand is nonnegative, has finite mean and has a density;
• $s_i < c_i < p_i + \pi_i$ for every product (Theorem 1's proof);
• every demand law charges every nonempty open interval of $[0,\infty)$, standing in for the uniqueness of the optimal level $\bar y(x)$ that the notation presupposes (Theorems 1 and 2).

The goal quantifies over every maximizer $y^*$ of $P(0,\cdot)$ and every optimal $\bar y$; it is not an existence statement, and $y^*$ is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for $x_i \ge y^*_i$.

A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of $S^k_j$ in $y$ and $d$), are welcome.

Selected references

• Y. Bassok, R. Anupindi, R. Akella, Single-Period Multiproduct Inventory Models with Substitution, Operations Research 47(4):632–642, 1999. https://doi.org/10.1287/opre.47.4.632
• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• E. Ignall, A. F. Veinott, Jr., Optimality of Myopic Inventory Policies for Several Substitute Products, Management Science 15(5):284–304, 1969. https://doi.org/10.1287/mnsc.15.5.284
• A. J. Hoffman, On Simple Linear Programming Problems, in V. Klee (ed.), Convexity, Proceedings of Symposia in Pure Mathematics, Vol. 7, AMS, 1963.

Motivation

Generalized pattern search (GPS) is a class of derivative-free methods for minimizing a function that can only be evaluated, not differentiated. Such objectives arise in engineering design, where one evaluation is an expensive simulation that may fail and return no value at all. The helicopter rotor design problem of Booker et al. is one example: no value was returned for roughly 66% of the trial points (Booker et al., 1999). A method for such problems has to tolerate objectives that are discontinuous or take the value $+\infty$.

Earlier convergence theory for GPS assumed continuous differentiability of the objective on a neighbourhood of the level set. Torczon established it for unconstrained problems (SIAM J. Optim. 7, 1997), and Lewis and Torczon extended it to bound constraints (1999) and to finitely many linear constraints (SIAM J. Optim. 10, 2000). Audet and Dennis (SIAM J. Optim. 13, 2003) replaced these analyses with a single argument. Its conclusions are local and are graded by the smoothness of the objective at the limit point only, through Clarke's generalized directional derivative. That paper is the source of this mission. Its analysis is the basis of the later mesh adaptive direct search (MADS) theory (Audet, Dennis, SIAM J. Optim. 17, 2006).

Setting

The problem is

$$\min_{x\in\Omega} f(x),\qquad f:\mathbb R^n\to\mathbb R\cup\{+\infty\},\qquad \Omega=\{x\in\mathbb R^n:\ell\le Ax\le u\},$$

with $A\in\mathbb R^{m\times n}$ and $\ell\le u$ in $(\mathbb R\cup\{\pm\infty\})^m$. The algorithm works with the barrier function $f_\Omega$, equal to $f$ on $\Omega$ and to $+\infty$ elsewhere.

The algorithm uses a finite set of directions $D=G\bar Z$, the columns $d_j=G\bar z_j$ of the product of a nonsingular $G\in\mathbb R^{n\times n}$ and an integer matrix $\bar Z\in\mathbb Z^{n\times p}$. The directions form a positive spanning set: their nonnegative combinations give all of $\mathbb R^n$. At iteration $k$, with iterate $x_k$ and mesh size parameter $\Delta_k>0$, the mesh is $M_k=\{x_k+\Delta_k Dz: z\in\mathbb Z_+^{p}\}$. A poll set $\{x_k+\Delta_k d: d\in D_k\}$ is drawn from a positive spanning subset $D_k\subseteq D$. Each iteration ends in one of two ways:

1. Improved mesh point. Some $x_{k+1}\in M_k\cap\Omega$ with $f_\Omega(x_{k+1})<f_\Omega(x_k)$ was found, by the free SEARCH step or by the poll. Then $\Delta_{k+1}=\tau^{w_k}\Delta_k$ with $0\le w_k\le w^+$.
2. Mesh local optimizer. $f_\Omega(x_k)\le f_\Omega(x_k+\Delta_k d)$ for every $d\in D_k$. Then $x_{k+1}=x_k$ and $\Delta_{k+1}=\tau^{w_k}\Delta_k$ with $w^-\le w_k\le-1$.

Here $\tau>1$ is rational and $w^-\le-1\le 0\le w^+$ are integers. The assumptions are A1 $f_\Omega(x_0)<\infty$, A2 $A$ is rational, and A3 all iterates lie in a compact set. A refining subsequence is an infinite set of mesh local optimizers $\{x_k\}_{k\in K}$ along which $\Delta_k\to 0$ (Definition 3.5). For $f$ Lipschitz near $\hat x$, Clarke's derivative is

$$f^\circ(\hat x;d)=\limsup_{y\to\hat x,\ t\downarrow 0}\frac{f(y+td)-f(y)}{t}.$$

Formalization targets

Goal: Theorem 3.7

Assume A1–A3. Let $\hat x$ be the limit of a refining subsequence, and let $d\in D$ be a direction polled at a feasible point $x_k+\Delta_k d$ for infinitely many $k$ in the subsequence. If $f$ is Lipschitz near $\hat x$, then

$$f^\circ(\hat x;d)\ \ge\ 0 .$$

Milestones on the way

• Theorem 3.1: the iterates have a limit point, $\lim_k f(x_k)$ exists and dominates $f$ at lower semicontinuity limit points, and all continuity limit points share one value.
• Lemma 3.2: $\min_{u\ne v\in M_k}\|u-v\|\ge\Delta_k/\|G^{-1}\|$ for every norm giving nonzero integer vectors norm at least $1$.
• Lemma 3.3: $\Delta_k\le\Delta_0\tau^{r^+}$ for some positive integer $r^+$.
• Proposition 3.4: $\liminf_{k\to\infty}\Delta_k=0$.
• Theorem 3.6: a convergent refining subsequence exists.

Corollaries

• Theorem 3.9: if $\Omega=\mathbb R^n$ and $f$ is strictly differentiable at $\hat x$, then $\nabla f(\hat x)=0$.
• Theorem 3.14: if the poll sets conform to the boundary of $\Omega$ (Definition 3.13) and $f$ is strictly differentiable at $\hat x$, then $\nabla f(\hat x)^Tw\ge 0$ on the tangent cone $T_\Omega(\hat x)$ and $-\nabla f(\hat x)\in N_\Omega(\hat x)$. So $\hat x$ is a KKT point.

Significance

Theorem 3.7 gives a first-order conclusion at a limit point from a local hypothesis at that point alone. It does not require smoothness elsewhere, finiteness of $f$ elsewhere, or continuity. It turns the heuristic "the method stopped improving on ever finer meshes" into a statement about generalized derivatives. The unconstrained stationarity result (Theorem 3.9) and the linearly constrained KKT result (Theorem 3.14) follow from it, and they recover the Torczon and Lewis–Torczon theorems under weaker smoothness assumptions. The chain Lemma 3.2 → Lemma 3.3 → Proposition 3.4 → Theorem 3.6 shows that the goal's hypothesis is always met. Every run satisfying A1 and A3 has a refining subsequence, which rests on the rationality of $\tau$ and on the integer structure of $D$.

All results in this mission are proved in the source paper. None of them has, to the best of our knowledge, a machine-checked proof. The mission contributes a formal model of the GPS algorithm class as a class of runs, a formal Clarke directional derivative, and checked proofs of the mesh-refinement chain and the main theorem.

Difficulty

Given a refining subsequence, the goal is a comparison of limsups: the poll inequalities give nonnegative difference quotients at the points $(x_k,\Delta_k)$, which converge to $(\hat x,0^+)$. The difficulty lies in two places. First, the objective is extended-valued, and the barrier hides $f$ at infeasible poll points, where the poll inequality $f_\Omega(x_k)\le+\infty$ says nothing. The hypothesis on $d$ has to supply feasibility, and the Lipschitz hypothesis has to supply finiteness near $\hat x$. Second, the existence of refining subsequences is not a compactness argument alone. Coarsening is allowed, so $\Delta_k$ need not decrease, and with an irrational $\tau$ or a direction set that is not an integer lattice image (for instance $D=[-1,+\pi]$ in $\mathbb R$) the meshes can be dense and $\liminf\Delta_k$ can be positive. The lattice argument behind Proposition 3.4 is where the integrality hypotheses are used.

Formalization scope

Points of $\mathbb R^n$ are Fin n → ℝ, $f$ takes values in WithTop ℝ, and the bounds $\ell,u$ are EReal-valued, so $m=0$ gives $\Omega=\mathbb R^n$. The barrier is defined by cases, never by extended addition. Directions are the columns of G * Zbar indexed by Fin p, and $D_k$ is a Finset (Fin p). A GPS run is a structure of sequences $x_k,\Delta_k,D_k,w_k$ and a per-iteration predicate "mesh local optimizer", subject to exactly the two update rules above, $\Delta_0>0$, rational $\tau>1$ and the exponent bounds. The SEARCH step, the choice of $D_k$ and the exponents are left free, since the paper allows any strategy. A subsequence is a strictly increasing map $K:\mathbb N\to\mathbb N$. The Clarke derivative of a real function is an EReal-valued limit superior along $y\to\hat x$, $t\to 0^+$. "$f$ Lipschitz near $\hat x$" means that $f$ agrees near $\hat x$ with a real function Lipschitz there, and the conclusions are stated for every such function. Strict differentiability is the directional notion of Section 3.4 of the paper.

The goal is not trivialized by an empty run class: Theorem 3.6, on the same class, asserts that refining subsequences exist. The mesh-local-optimizer branch requires the complete poll inequality over $D_k$. The Clarke limit superior cannot take a default value. The direction $d$ must be polled at feasible points infinitely often, which is the paper's "$f$ was evaluated".

Contributions welcome: proofs of any milestone, and reusable lemmas on positive spanning sets, lattice points in compact sets, and the Clarke derivative (for instance, that it equals $\nabla f(\hat x)^Td$ under strict differentiability).

Selected references

• C. Audet, J. E. Dennis Jr., Analysis of Generalized Pattern Searches, SIAM J. Optim. 13(3):889–903, 2003. https://doi.org/10.1137/S1052623400378742
• V. Torczon, On the Convergence of Pattern Search Algorithms, SIAM J. Optim. 7(1):1–25, 1997. https://doi.org/10.1137/S1052623493250780
• R. M. Lewis, V. Torczon, Pattern Search Methods for Linearly Constrained Minimization, SIAM J. Optim. 10(3):917–941, 2000. https://doi.org/10.1137/S1052623497331373
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; reprinted SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309
• A. J. Booker, J. E. Dennis Jr., P. D. Frank, D. B. Serafini, V. Torczon, M. W. Trosset, A rigorous framework for optimization of expensive functions by surrogates, Structural Optimization 17:1–13, 1999. https://doi.org/10.1007/BF01197559
• C. Audet, J. E. Dennis Jr., Mesh Adaptive Direct Search Algorithms for Constrained Optimization, SIAM J. Optim. 17(1):188–217, 2006. https://doi.org/10.1137/040603371

Motivation

Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves $1/4$ of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats $1/4$ and reaches $1/3$.

Timeline. For Max Directed Cut, a random cut achieves $1/4$. Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved $1/4$ for a random set and $1/3$ nonadaptively for general nonnegative submodular functions, $1/3$ and $2/5$ by adaptive local search, and that $1/2$ requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal $1/2$ with a randomized double-greedy algorithm.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements. A function $f : 2^X \to \mathbb{R}$ is submodular (Definition 1.1) if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X .$$

Throughout, $f$ is nonnegative, the paper's standing assumption, and $OPT = \max_{S \subseteq X} f(S)$.

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; $R = X(1/2)$ is a uniformly random subset. For a set $A \subseteq X$, $A(p)$ is the analogous random subset of $A$. The averaged marginal value of an element (Definition 2.4) is

$$\omega(x) = \mathbf{E}\big[f(R \cup \{x\}) - f(R \setminus \{x\})\big], \qquad R = X(1/2).$$

Algorithm NA (p. 1139):

1. by random sampling, compute estimates $\tilde\omega(x)$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$, with high probability;
2. independently, sample $R = X(1/2)$;
3. with probability $8/9$ return $R$;
4. with probability $1/9$ return $A = \{x \in X : \tilde\omega(x) > 0\}$.

Given the estimates, the expected value NA returns is $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$.

Formalization targets

Goal: Theorem 2.6 in the explicit form of its proof

For every nonnegative submodular $f$ and every estimate $\tilde\omega$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$,

$$\frac89\,\mathbf{E}[f(X(1/2))] + \frac19\, f\big(\{x : \tilde\omega(x) > 0\}\big) \ \ge\ \Big(\frac13 - \frac{4}{9n}\Big)\, OPT .$$

The printed theorem says "at least $(1/3 - o(1))\,OPT$"; the term $4/(9n)$ is what the proof establishes (p. 1140, last display).

Milestones

1. Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$ for submodular $g$.
2. Lemma 2.3: $\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B)$ for independently sampled, possibly overlapping $A, B$.
3. For $B = X \setminus A$ and any $C$: $f(A) + f(B \cap C) + f(B \cup C) \ge f(C)$.
4. If $\omega \le OPT/n^2$ on $B$: $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$.
5. $\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B \cap C) + \tfrac14 f(C)$.
6. If $\omega \ge -OPT/n^2$ on $A$ and $B = X \setminus A$: $\mathbf{E}[f(R)] \ge \mathbf{E}[f(R \cap (B \cup C))] - OPT/(2n)$.
7. $\mathbf{E}[f(R \cap (B \cup C))] \ge \tfrac14 f(C) + \tfrac14 f(B \cup C)$.

Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of $C$.

Significance

The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a $1/3$-approximation of unconstrained nonnegative submodular maximization, strictly better than the $1/4$ of any algorithm that must return one of its queried sets (the paper shows $1/4$ is optimal in that class, §4.2). The quantity $\omega$ generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.

Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the $1/3$ argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.

Difficulty

The two regimes the proof separates, "$A$ is already good" and "one of $f(B \cap C)$, $f(B \cup C)$ is large", must be tied to the value of a uniformly random set, whereas the elements of $A$ and $B$ are chosen from estimated averages, not from the optimal set $C$. The natural attempt, comparing $f(R)$ with $f(C)$ element by element, fails because $f$ is not monotone: adding elements of $C$ to $R$ can decrease the value. The accuracy $OPT/n^2$ of the estimates must also be propagated through a sum over up to $n$ elements, which is where the error term $4/(9n)$ comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.

Formalization scope

• The ground set is a Fintype X with DecidableEq, assumed Nonempty, so $n = |X| \ge 1$ and the divisions by $n$ and $n^2$ are genuine; sets are Finset X; $f$ is real valued with nonnegativity $\forall S,\ 0 \le f(S)$ as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real $f$ with no sign condition, as printed.
• $OPT$ is Finset.univ.sup' _ f, the true maximum over all subsets.
• Every expectation over an independently sampled random set is the exact finite sum $F(x) = \sum_{S} f(S)\prod_{i \in S} x_i \prod_{i \notin S}(1 - x_i)$; $X(1/2)$ is $x \equiv 1/2$. Expectations over two independent samples (Lemma 2.3) are the corresponding iterated sums. Sampling probabilities carry the hypotheses $0 \le p, q \le 1$.
• The goal quantifies over every estimate $\tilde\omega$ satisfying the printed accuracy $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ (strict), with $A = \{x : \tilde\omega(x) > 0\}$ (strict). The "with high probability" of NA's first step is this hypothesis; the sampling estimate that makes it likely (Lemma 2.5, a Chernoff-bound argument) is not part of the goal. When $OPT = 0$ the hypothesis is unsatisfiable, but then $f \equiv 0$ and nothing is lost.
• The left-hand side is exactly the mixture $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$. A statement with the maximum of the two terms, with exact values $\tilde\omega = \omega$, or with the $o(1)$ replaced by an existential constant or a limit, is a different (and weaker or stronger) theorem and does not close this mission.
• Printed slip corrected: in the second display on p. 1140, the "$=$" before $-|A \setminus C|\,OPT/(2n^2)$ should be "$\ge$"; milestone 6 states the inequality.

Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity $\mathbf{E}[f(R \cup \{x\}) - f(R)] = \tfrac12\omega(x)$, and general lemmas about the operator $F$ (splitting a uniform random set along a partition).

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

The continuous-review $(Q, r)$ policy is the standard replenishment rule of inventory theory: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$, order a fixed order quantity $Q$. It is used in practice and taught in every operations management course, usually after the deterministic economic order quantity (EOQ) model, which is the same system with a constant demand stream.

Practitioners and textbooks rely on a robustness property of the EOQ: its cost is very insensitive to the choice of order quantity. If the order quantity is off by a factor $\alpha$, the cost rises only by the factor $\tfrac12(\alpha + 1/\alpha)$; ordering 50% too much costs about 8% extra. The insensitivity of the stochastic $(Q, r)$ system to its control parameters had been observed numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), but, as Zheng notes, no analytical result on it was known.

Timeline:

• 1963: Hadley and Whitin derive the $(Q, r)$ cost for Poisson demand.
• 1986: Zipkin proves that the average backorders of a $(Q,r)$ policy are jointly convex in $(Q, r)$ under continuous demand (Zipkin 1986).
• 1992: Zheng derives simple optimality conditions for the continuous $(Q, r)$ model and compares it with the EOQ model under the same cost structure. One of the results is that the stochastic cost curve is flatter in the order quantity than the EOQ curve (Zheng 1992). This mission formalizes that result.

Setting

Demands arrive at rate $\lambda>0$; orders arrive after a fixed leadtime $L>0$; all stockouts are backordered. Each order costs $K>0$; holding costs accrue at rate $h>0$ per unit in stock and penalty costs at rate $p>0$ per unit backordered. The leadtime demand $D\ge 0$ has distribution $\mu$ with finite mean $E(D) = \lambda L$.

The inventory cost rate at inventory position $y$ is

$$G(y) = E\big[h(y-D)^+ + p(D-y)^+\big],$$

assumed to attain its minimum at a unique point $y^0$. The long-run average cost of the policy $(Q, r)$ is

$$c(Q, r) = \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}, \qquad Q>0.$$

For fixed $Q>0$ let $r(Q)$ be a reorder point minimizing $c(Q,\cdot)$, and let

$$C(Q) = c(Q, r(Q)), \qquad H(Q) = G(r(Q))\ (Q>0), \quad H(0) = G(y^0).$$

$C$ is the cost of the order quantity $Q$ when the reorder point is always chosen optimally for it. An optimal order quantity $Q^*$ minimizes $C$ over $Q>0$, and $C^* = C(Q^*)$.

The EOQ model is the same system with the constant leadtime demand $\lambda L$. Its cost rate is $G_d(y) = h(y-\lambda L)^+ + p(\lambda L-y)^+$, and $r_d$, $H_d$, $C_d$ are the objects above at $G_d$, with optimum $Q^*_d$ and $C^*_d$.

Formalization targets

Goal: Theorem 4

$$\frac{C(\alpha Q^*)}{C^*} \le \frac12\left(\alpha + \frac1\alpha\right) \qquad \forall \alpha>0.$$

The goal holds for every demand distribution satisfying the standing assumptions and every optimal $Q^*$. Both regimes, $\alpha<1$ and $\alpha>1$, are included.

Milestones

In the order the proof uses them:

1. Eq. (7): $\int_{r(Q)}^{r(Q)+Q} G = \int_0^Q H$, hence $C(Q) = \big(\lambda K + \int_0^Q H(y)dy\big)/Q$ for $Q>0$.
2. Lemma 4: $H$ is increasing and convex on $[0,\infty)$ with asymptotic slope $hp/(h+p)$.
3. Eq. (8): an optimal $Q^*$ exists, and $Q>0$ is optimal iff $H(Q) = C(Q)$.
4. Eq. (18): $H_d(Q) = \frac{hp}{h+p}Q$, with $r_d(Q) = \lambda L - \frac{h}{h+p}Q$.
5. Lemma 7: $H_0(Q) \le H_d(Q) \le H(Q)$ and $A(Q)\le A_d(Q)$, where $H_0 = H - G(y^0)$ and $A(Q) = QH(Q) - \int_0^Q H$.
6. Eqs. (26)–(27): $H(\alpha Q)\le \alpha H(Q)$ for $\alpha>1$ and $H(\alpha Q)\ge\alpha H(Q)$ for $0<\alpha<1$.
7. Lemma 9: $\int_Q^{\alpha Q} H(y)\,dy \le \frac{\alpha^2-1}{2}\,Q H(Q)$ for all $\alpha>0$, $Q>0$.

Significance

In the EOQ model the relative cost of a scaled order quantity is exactly $C_d(\alpha Q^*_d)/C^*_d = \tfrac12(\alpha + 1/\alpha)$ (Eq. (25) of the paper). Theorem 4 shows that the stochastic system is at least as forgiving. The bound holds for every leadtime-demand distribution with a unique newsvendor minimizer, and it does not depend on the parameters $K$, $h$, $p$, $\lambda$ or $L$. Because the reorder point is re-optimized for each quantity, the bound applies to the practical question of how much a misestimated lot size costs when the safety stock is set correctly.

Together with the other results of the paper (the $1/8$ bound for the EOQ heuristic and the bounds between $Q^*$ and $Q^*_d$, which are separate missions of this series), it gives a closed-form account of why the EOQ is a good heuristic for stochastic systems.

The result has a complete published proof. It has not been machine-checked. The work that remains is a formal proof for general distributions: the paper differentiates $G$ and $r(Q)$ twice, and a formal proof has to replace those derivatives with arguments that need no density.

Difficulty

$C(Q)$ is defined through an inner minimization over the reorder point, so its shape in $Q$ is controlled by the implicitly defined function $H(Q) = G(r(Q))$ rather than by $G$ directly. The obvious approach would bound $C(\alpha Q^*)$ with the reorder point fixed at $r(Q^*)$. That approach is the wrong comparison: it bounds a larger quantity, and the resulting bound depends on the distribution.

The paper's proof uses three properties of $H$: that it is convex, that its slope never exceeds the EOQ slope $hp/(h+p)$, and that it dominates $H_d$. The paper obtains these from the derivatives $r'(Q)$ and $H'(Q)$ under a smooth demand distribution. Without a density, $r(Q)$ is only an argmin and $H$ need not be differentiable, so none of these three properties can be read off a derivative formula; the asymptotic slope in particular depends on the finite mean $E(D) = \lambda L$ and on the behaviour of $G$ at $\pm\infty$.

Formalization scope

The mission is set in Lean 4 with Mathlib. All objects are real valued.

• Model. The structure QRModel bundles $\lambda, L, K, h, p>0$, a probability measure $\mu$ on $\mathbb{R}$ with integrable identity, $\int x\,d\mu = \lambda L$, $D\ge 0$ almost surely, and the unique-minimizer hypothesis on $G$. $K>0$ is implicit in the paper and made explicit here. No density is assumed; deterministic and discrete demands are allowed, and the paper's own numerical study uses Poisson demand.
• Generic machinery. $c$, $r(Q)$, $y^0$, $H$, $H_0$, $C$ and $A$ are defined for an arbitrary cost rate and instantiated at $G$ and at $G_d$. $r(Q)$ and $y^0$ are chosen minimizers; they are never defined by the equation $G(r) = G(r+Q)$, which is a lemma of the paper. $H(0) = G(y^0)$. Values at $Q<0$ (and of $c$, $C$ at $Q\le 0$) are junk, and every statement restricts to $Q>0$ or $Q\ge 0$.
• Readings of informal words. "Increasing" in Lemma 4 is strict on $[0,\infty)$, since the proof shows $H'>0$. "Asymptotic slope $hp/(h+p)$" is stated as $H(Q)/Q\to hp/(h+p)$ together with the chord bound $H(Q_2)-H(Q_1)\le \frac{hp}{h+p}(Q_2-Q_1)$ for $0\le Q_1\le Q_2$. The chord bound is the derivative-free form of $H'\le hp/(h+p)$ that the proofs of Lemmas 7–9 use. "The optimal order quantity" is IsOptQty Q, meaning $Q>0$ and $C(Q)\le C(Q')$ for all $Q'>0$. Its existence is asserted in the Eq. (8) milestone, so the goal is not vacuous. "$\forall\alpha>0$" is a real $\alpha>0$ with real division $1/\alpha$. In Lemma 9 the integral $\int_Q^{\alpha Q}$ is oriented, as on the page.
• Ruling out trivializations. $C(\alpha Q^*)$ re-optimizes the reorder point for $\alpha Q^*$; holding it at $r(Q^*)$ would be a different theorem. $C^*>0$ is a consequence of the model, not a hypothesis.

A complete development needs the following:

• integrability and continuity of $G$;
• existence of the optimal reorder point;
• convexity of $H$;
• the asymptotics $G - G_d\to 0$ at $\pm\infty$;
• Jensen's inequality $G_d\le G$ (Eq. (22));
• existence of $Q^*$.

These facts about newsvendor cost functions are reusable in the other missions of this series. Contributions of any of them as separate lemmas are welcome.

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• P. H. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• H. M. Wagner, M. O'Hagan and B. Lundh, An Empirical Study of Exactly and Approximately Optimal Inventory Policies, Management Science 11(7):690–723, 1965. https://doi.org/10.1287/mnsc.11.7.690
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Motivation

The continuous-review $(Q, r)$ policy is the standard control rule for a single stocked item with random demand: whenever the inventory position falls to the reorder point $r$, an order of fixed size $Q$ is placed. It is implemented in a large share of commercial inventory systems. Choosing the two parameters jointly has traditionally required numerical search (Hadley and Whitin, 1963; Federgruen and Zheng, 1992). In practice the order quantity is therefore often taken from the deterministic economic order quantity (EOQ) formula with backorders, and the reorder point is then set for the random demand.

Zheng (1992) turned this practice into a question with an exact answer: how does the optimal order quantity $Q^*$ of the stochastic model compare with the EOQ quantity $Q^*_d$ computed from the same cost data and the same mean demand? Its Theorem 2 answers it with a two-sided bound. This mission formalizes that theorem. Companion missions of the same series formalize the paper's cost bounds (Theorem 3), the flatness of the cost curve (Theorem 4) and the $1/8$ bound on the cost of using the EOQ quantity (Theorem 5).

Setting

Demand arrives at rate $\lambda > 0$ and replenishment orders arrive after a fixed leadtime $L > 0$. Shortages are backordered. Holding costs accrue at rate $h > 0$ per unit held, backorder penalties at rate $p > 0$ per unit short, and every order costs $K > 0$. The leadtime demand $D$ is a nonnegative random variable with law $\mu$ and mean $\mathbb{E}(D) = \lambda L$. The expected inventory cost rate at inventory position $y$ is the newsvendor cost

$$G(y) = \mathbb{E}\big[h(y - D)^+ + p(D - y)^+\big],$$

assumed, as in the paper, to attain its minimum at a unique point $y^0$. The long-run average cost of the policy $(Q, r)$ is

$$c(Q, r) = \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}.$$

For each $Q > 0$, let $r(Q)$ be an optimal reorder point, i.e. a minimizer of $c(Q, \cdot)$. The analysis runs through the curves

$$H(Q) = G(r(Q))\ (Q > 0),\quad H(0) = G(y^0),\qquad H_0(Q) = H(Q) - G(y^0),\qquad A(Q) = QH(Q) - \int_0^Q H(y)\,dy,$$

and through the cost $C(Q) = c(Q, r(Q))$ of order quantity $Q$ with the reorder point set optimally. The optimal order quantity $Q^*$ is the minimizer of $C$ over $Q > 0$.

The EOQ model is the case of a constant leadtime demand $\lambda L$. Its cost rate is $G_d(y) = h(y - \lambda L)^+ + p(\lambda L - y)^+$, and the same construction gives $r_d$, $H_d$, $A_d$ and the optimal quantity

$$Q^*_d = \sqrt{\frac{2\lambda K(h+p)}{hp}}.$$

Formalization targets

Goal: Theorem 2 (p. 96)

For $K > 0$, let $\bar Q$, $\bar Q_1$, $\bar Q_2$ be the positive solutions of

$$Q H_0(Q) = 2\lambda K,\qquad H_0(Q) = H_d(Q^*_d),\qquad \int_0^Q H_0(y)\,dy = \lambda K.$$

Each has exactly one positive solution, and

$$Q^*_d \le Q^* \le \bar Q,\qquad \bar Q \le \bar Q_1,\qquad \bar Q \le \bar Q_2.$$

Moreover, with $\lambda, L, h, p$ and the demand law fixed, $K \mapsto \bar Q_1(K) - Q^*_d(K)$ is nondecreasing on $(0, \infty)$ and converges to a finite constant as $K \to \infty$.

Milestones

The milestones are the paper's own numbered results that feed Theorem 2, listed in the order the argument uses them:

1. Lemma 2 (p. 90): for $Q > 0$, $r$ is optimal iff $G(r) = G(r + Q)$.
2. Eq. (7) (p. 91): $C(Q) = (\lambda K + \int_0^Q H(y)\,dy)/Q$.
3. Lemma 4 (p. 91): $H$ is increasing and convex with asymptotic slope $hp/(h+p)$.
4. Lemma 6 (p. 92): $A$ is increasing and convex, and $Q = Q^*$ iff $A(Q) = \lambda K$.
5. Eqs. (18), (20) (p. 94): $H_d(Q) = \frac{hp}{h+p}Q$, and $Q^*_d$ is optimal for the EOQ model.
6. Lemma 7 (p. 95): $H_0 \le H_d \le H$ and $A \le A_d$.
7. Lemma 8 (p. 95): $\int_0^Q H \ge \tfrac12 QH(Q) \ge A(Q) \ge \tfrac12 QH_0(Q) \ge \int_0^Q H_0$, with equalities for deterministic demand.

Significance

The result. Theorem 2 says that the EOQ formula always underestimates the optimal order quantity when leadtime demand is random. The underestimate is bounded by $\bar Q_1 - Q^*_d$, a quantity that stays bounded however large the ordering cost is. So the relative error of the EOQ quantity vanishes as $K$ grows. The first inequality, $Q^*_d \le Q^*$, is also an ingredient of the paper's Theorem 3 (cost bounds) and Theorem 5 (the EOQ quantity raises costs by at most $1/8$). The explicit bounds $\bar Q$, $\bar Q_1$, $\bar Q_2$ bracket $Q^*$ and give a search interval for it.

Formalizing it. The theorem has been proved on paper since 1992. No machine-checked version of it, or of the continuous-review $(Q, r)$ cost of Eq. (1), exists on this platform. The inventory items already here treat the discrete cost with integer order quantities, a normally distributed demand, or the EOQ without backorders. This mission provides a machine-checked version of the paper's optimality conditions for a general demand distribution. The paper's argument differentiates $G$ twice, i.e. it tacitly assumes a density. The formal statements do not, so a formal proof must redo those steps with one-sided (convexity) arguments. The printed argument for the limit in part (b) shows only that a derivative tends to zero. A complete proof of convergence is part of the work.

Difficulty

The obvious route to $Q^*_d \le Q^*$ compares the two cost curves $C$ and $C_d$ directly. It fails because $C \ge C_d$ pointwise, and a pointwise inequality between two convex functions says nothing about the order of their minimizers. The stochastic curve $H$ is defined only implicitly, as $G$ evaluated at a minimizer of a parametric integral, so its growth relative to the linear $H_d$ has to be established before any comparison of order quantities. For part (b), a vanishing derivative does not imply convergence ($\log K$ also has a vanishing derivative), so the printed proof of the limit does not go through as written.

Without a density, $r(Q)$ need not be differentiable. Every derivative in the paper's proofs (of $r$, $H$ and $A$) must be replaced by monotonicity or chord arguments.

Formalization scope

The Lean development uses the namespace ZhengQR.OrderQty. Its conventions:

• Parameters. $\lambda, L, K, h, p$ are reals, all assumed strictly positive. $K > 0$ is implicit in the paper; at $K = 0$ the optimal quantity degenerates.
• Demand. The law $\mu$ of $D$ is a probability measure on $\mathbb{R}$ that is integrable, has mean $\lambda L$ and is carried by $[0, \infty)$. No density is assumed, so discrete laws such as the Poisson of the paper's §4 are allowed.
• Standing assumption. $G$ has a unique global minimizer (p. 90). It is a hypothesis of every statement about the stochastic model.
• Generic machinery. $c$, $r(Q)$, $y^0$, $H$, $C$, $A$, $H_0$ and optimality of $Q$ are defined for an arbitrary cost rate $G$ and applied to both the newsvendor cost and $G_d$. So Eqs. (18) and (20) are theorems, not definitions. $r(Q)$ and $y^0$ are chosen minimizers, never solutions of Lemma 2's equation. $r(Q)$ minimizes $\int_r^{r+Q}G$, which for $Q > 0$ has the same minimizers as $c(Q, \cdot)$, so $H$, $H_0$ and $A$ do not depend on $K$.
• Domains. $H$, $H_0$ and $A$ are used on $[0, \infty)$, $c$ and $C$ for $Q > 0$ only, and $Q^*$ is a $Q > 0$ minimizing $C$ over $(0, \infty)$.
• Readings of informal words.
  • Lemma 4's "increasing" and Lemma 6's "increasing/decreasing" mean strictly.
  • Lemma 4's "asymptotic slope $hp/(h+p)$" means $H(Q)/Q \to hp/(h+p)$ together with the chord bound $H(Q') - H(Q) \le \frac{hp}{h+p}(Q' - Q)$ for $0 \le Q < Q'$.
  • "$\bar Q \overset{\text{def}}{=} \{Q : \dots\}$" means the unique positive solution. The goal quantifies over every positive solution and separately asserts that exactly one exists.
  • Theorem 2's "increasing function of $K$" means nondecreasing, which is what the paper's proof establishes (a nonnegative derivative).
  • "Converges to a constant" means a finite real limit.
  • Lemma 8's "the leadtime demand is deterministic" means the EOQ model with cost rate $G_d$.
• Ruling out trivial readings. The goal's hypotheses are satisfiable (for example by a deterministic leadtime demand). Existence of $Q^*$ (Lemma 6) and of $\bar Q$, $\bar Q_1$, $\bar Q_2$ (the goal itself) is asserted, so neither the bounds nor the limit hold vacuously.

Infrastructure needed includes the following. Much of it is reusable for any single-item inventory model:

• differentiation under the expectation, or one-sided substitutes, for $G$;
• convexity of $H$ as the inverse of the width of the sublevel sets of $G$;
• the envelope identity behind Eq. (7);
• elementary convex-analysis facts about chords.

Contributions welcome: proofs of the milestones in any order, general lemmas on the newsvendor cost, and a complete convergence argument for part (b).

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• A. Federgruen, Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808