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

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

Motivation

Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.

The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.

Timeline:

• Karlin and Scarf (1958), Scarf (1960): structure of optimal single-source backlog policies with a lead time.
• Sheopuri, Janakiraman and Seshadri (2010): reduction of dual-sourcing policies to the truncated regular pipeline and the expedited inventory position (Lemma 1 here).
• Allon and Van Mieghem (2010): the TBS policy, with conjectures and numerical evidence.
• JSS (2015): the TBS cost formula and a convex program for its parameters.
• Xin and Goldberg (2018): proof of the conjecture with an explicit rate (Management Science 64(1), 2018). This mission formalizes that result.

Setting

Let $D$ be a nonnegative random variable with finite mean $\mathbb E[D]$ that is not almost surely constant. Demands $D_1, D_2, \dots$ are i.i.d. copies of $D$. The regular source has lead time $L$, the express source has lead time $L_0 \ge 0$, and $L > L_0 + 1$. In period $t$ the controller orders $q^R_t \ge 0$ and $q^E_t \ge 0$; then $q^R_{t-L} + q^E_{t-L_0}$ arrives and $D_t$ is realized, so the on-hand inventory evolves as $I_{t+1} = I_t + q^R_{t-L} + q^E_{t-L_0} - D_t$ and may be negative. Initially nothing is on order and $I_1 = -\sum_{i=1}^{\hat G} D'_{-i}$, where the $D'_{-i}$ are further i.i.d. copies of $D$ and $\mathbb P(\hat G = k) = 2^{-k}$, $k \ge 1$.

The per-period cost is $c\,q^E_{t-L_0} + G(I_{t+1})$ with $G(y) = h y^+ + b y^-$, where $b, h > 0$ and $c > 0$ is the express premium (the regular unit cost is normalized to $0$). An admissible policy $\pi \in \Pi$ chooses the two orders in period $t$ as deterministic measurable functions of $(q^R_{t-L}, \dots, q^R_{t-1}, q^E_{t-L_0}, \dots, q^E_{t-1}, I_t)$. Its long-run average cost is

$$C(\pi) = \limsup_{T\to\infty}\frac1T\sum_{t=L_0+1}^T \mathbb E[C^\pi_t], \qquad \mathrm{OPT}(L) = \inf_{\pi\in\Pi}C(\pi).$$

With the expedited inventory position $\hat I_t = I_t + \sum_{k=t-L_0}^{t-1}q^E_k + \sum_{k=t-L}^{t-L+L_0}q^R_k$, the TBS policy $\pi_{r,S}$ orders $q^R_t = r$ and $q^E_t = \max(0, S - \hat I_t)$. A best TBS pair $(r^*, S^*)$ minimizes $C(\pi_{r,S})$ over $0 \le r \le \mathbb E[D]$ and $S \in \mathbb R$ (first in $r$ through $F^\infty(r) = \inf_S C(\pi_{r,S})$, then in $S$).

The constants $\epsilon_0$ and $Y_0$ are explicit functionals of the law of $D$ and of $L_0, b, h, c$. They are built from $g = \inf_x\mathbb E[G(x - \sum_{i=1}^{L_0+1}D'_i)]$, $U = c\,\mathbb E[D] + \mathbb E[G(-\sum_{i=1}^{L_0+1}D'_i)]$, $p_0 = \mathbb P(D < \mathbb E[D])$, the mean absolute deviation $\eta_0$, and the large-deviation quantities $\gamma_\epsilon, \vartheta_\epsilon$ of $\phi_\epsilon(\theta) = e^{\theta(\mathbb E[D]-\epsilon)}\mathbb E[e^{-\theta D}]$ (p. 441).

Formalization targets

Goal: Theorem 1 (p. 441)

For all $L_0 \ge 0$, $\epsilon \in (0,1)$ and $L > \epsilon_0^{-2} + Y_0\epsilon^{-2}$,

$$\frac{C(\pi_{r^*,S^*})}{\mathrm{OPT}(L)} < 1 + \epsilon.$$

The threshold does not depend on $L$, so the statement gives an explicit, inverse-polynomial rate. Its limit form $C(\pi_{r^*,S^*})/\mathrm{OPT}(L) \to 1$ is Corollary 1 of the paper.

Milestones

In the order the proof uses them:

• the bound $g \le \mathrm{OPT}(L) \le U$;
• Lemma 1, the reduction to $\hat\Pi$ (quoted from Sheopuri et al.);
• Eq. (3), the TBS cost formula $C(\pi_{r,S}) = c(\mathbb E[D]-r) + \mathbb E[G(I^r_\infty + S - \sum_{i=1}^{L_0+1}D'_i)]$ (quoted from JSS);
• Theorem 2, the existence of a stationary-like vector $(\chi^{*,L}, q^{*,L}, \mathcal I^{*,L})$ with $r_L = \mathbb E[\chi^{*,L}_1]$;
• Corollary 2 and Lemma 2, the lower bound $\mathrm{OPT}(L) \ge c(\mathbb E[D]-r_L) + (1-\alpha)V^{L-L_0}_\alpha(r_L,-\infty)$ through a discounted single-source problem;
• Lemma 3, the Bellman equation and structure of that problem (quoted from JSS and Scarf 1960);
• Lemma 4 (8) and (9), and Corollary 3, the passage to the infinite horizon and to base-stock policies;
• Lemma 5, the random-walk maxima $M^r_k$ (proof omitted in the paper);
• Lemmas 8–9 and Corollary 4: $r_L < \mathbb E[D] - \epsilon_0$ once $L > \epsilon_0^{-2} + L_0 + 1$.

Significance

The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of $L$, so the result yields an algorithm whose running time does not grow with $L$ and whose optimality gap is bounded explicitly for every finite $L$. It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.

Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.

Difficulty

An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding $r_L$ away from $\mathbb E[D]$ requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.

Formalization scope

Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):

• The law of $D$ is a probability measure on $\mathbb R$ with no mass on $(-\infty,0)$, finite mean, and no atom of mass $1$. The paper's "strictly positive (possibly infinite) variance" is read as "not almost surely constant".
• $c_R = 0$, $b > 0$, $h > 0$, $c > 0$, and $L, L_0$ are natural numbers. The paper's standing assumption $L > L_0 + 1$ is a hypothesis wherever the paper states it; in Theorem 1 it follows from the threshold.
• Costs, expectations, $C(\pi)$, $\mathrm{OPT}(L)$, $V^n_\alpha$ and $V^\infty_\alpha$ take values in $[0,\infty]$, so infinite costs are never truncated. The ratio in Theorem 1 is stated as $C(\pi_{r^*,S^*}) < (1+\epsilon)\mathrm{OPT}(L)$, which is equivalent because $0 < g \le \mathrm{OPT}(L) \le U < \infty$.
• $\Pi$ is exactly the paper's class: deterministic, time-dependent, measurable, nonnegative orders that depend on the pipeline and inventory. It is neither restricted to stationary policies nor enlarged to randomized ones. TBS policies are members, so $C(\pi_{r,S}) \ge \mathrm{OPT}(L)$ by construction.
• $\vartheta_\epsilon \in [0,\infty]$ is the supremum of the minimizers of $\phi_\epsilon$ on $[0,\infty)$, and it is $\infty$ if the infimum is not attained; $1/\infty = 0$.
• The existence of a best TBS pair is asserted in the paper via JSS. The goal therefore also asserts that some TBS policy with $0 \le r \le \mathbb E[D]$ meets the bound, so it cannot hold vacuously when no minimizer exists.
• $r_L$ belongs to a witness of Theorem 2, and the results that use it hold for every witness.
• The single-source class $\bar\Pi$ ("feasible nonanticipative policies, as typically defined") is read as nonnegative orders that are measurable functions of past demands. In Lemma 3 "increasing" is read as nondecreasing, and convexity in $x$ includes finiteness.
• The paper states Eq. (3) without a range for $r$; it is stated here for $0 \le r \le \mathbb E[D]$, the TBS parameters over which the paper optimizes. At $r = \mathbb E[D]$ both sides are $+\infty$. In Lemma 8, the range's upper end is $+\infty$ when $\epsilon = 0$.
• Differences such as $V^\infty_\alpha - V^n_\alpha$ and $M^r_\infty - M^r_n$ are stated additively, and the negative terms of (9) and Corollary 3 are moved to the other side.

Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.

A trivializing formalization is ruled out: $\mathrm{OPT}(L)$ ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.

Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.

Selected references

• L. Xin and D. A. Goldberg, Asymptotic Optimality of Tailored Base-Surge Policies in Dual-Sourcing Inventory Systems, Management Science 64(1):437–452, 2018. https://doi.org/10.1287/mnsc.2016.2607
• G. Janakiraman, S. Seshadri and A. Sheopuri, Analysis of Tailored Base-Surge Policies in Dual Sourcing Inventory Systems, Management Science 61(7):1547–1561, 2015.
• G. Allon and J. A. Van Mieghem, Global Dual Sourcing: Tailored Base-Surge Allocation to Near- and Offshore Production, Management Science 56(1):110–124, 2010.
• A. Sheopuri, G. Janakiraman and S. Seshadri, New Policies for the Stochastic Inventory Control Problem with Two Supply Sources, Operations Research 58(3):734–745, 2010.
• H. Scarf, The Optimality of (s, S) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960, pp. 196–202.
• L. Xin and D. A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6):1556–1565, 2016.