The OR Formalization Drive

Motivation

The economic order quantity (EOQ) is the most widely used formula in inventory management. It assumes that demand is a deterministic constant stream. Real demand is random, and the model that accounts for this, the continuous-review $(Q, r)$ policy with stochastic demand, has no closed-form optimum: for decades its optimal parameters were computed numerically, one instance at a time, which gave little insight into how the stochastic system behaves. Practitioners nevertheless kept using the EOQ quantity in stochastic systems and observed that the cost penalty was small (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), without an analytical explanation.

Zheng (Management Science 38(1), 1992) supplied that explanation. By minimising the average cost first over the reorder point and then over the order quantity, he obtained two simple optimality equations and compared the stochastic model with the EOQ model under the same cost structure. One of the results is the goal of this mission: for every leadtime-demand distribution, using the EOQ order quantity in the stochastic system raises the average cost by at most one eighth. The paper extends Federgruen and Zheng (1988), who treated the discrete-demand version of the cost function.

Setting

A single item faces demand at rate $\lambda > 0$. Orders are delivered after a fixed leadtime $L > 0$, and stockouts are backordered. Each order costs a fixed $K > 0$. Inventory is held at cost rate $h > 0$ per unit and backorders are penalised at cost rate $p > 0$ per unit. Let $D \ge 0$ be the demand during a leadtime, with mean $E(D) = \lambda L$. The newsvendor cost

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

is the rate at which expected inventory costs accrue at time $t + L$ when the inventory position at time $t$ is $y$. It is convex, and it is assumed, as in the paper, to attain its minimum at a unique point $y^0$.

A $(Q, r)$ policy orders $Q$ units whenever the inventory position falls to the reorder point $r$. Its long-run average cost is

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

For a fixed $Q > 0$ let $r(Q)$ be an optimal reorder point, and set

$$H(Q) = G(r(Q)) \ (Q > 0),\quad H(0) = G(y^0),\quad C(Q) = c(Q, r(Q)),\quad A(Q) = Q H(Q) - \int_0^Q H(y)\,dy .$$

$C(Q)$ is the average cost when the reorder point is chosen optimally for $Q$; an order quantity $Q^* > 0$ minimising $C$ over $Q > 0$ is the optimal order quantity, and $C^* = C(Q^*)$ is the optimal cost.

The EOQ model is the special case in which the leadtime demand is the constant $\lambda L$. Its cost rate is $G_d(y) = h(y - \lambda L)^+ + p(\lambda L - y)^+$, and its optimal order quantity is

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

The subscript $d$ marks every object of the EOQ model ($r_d$, $H_d$, $A_d$).

Formalization targets

Goal: Theorem 5

$$R = \frac{C(Q^*_d) - C^*}{C^*} \;\le\; \frac18 - \frac12\left(\frac12 - \frac{Q^*_d}{Q^*}\right)^2 \;\le\; \frac18 .$$

$C(Q^*_d)$ is the stochastic cost at the EOQ quantity with the reorder point re-optimised for it. The bound holds for every leadtime-demand distribution and every value of the parameters.

Milestones

In the order the goal's proof uses them:

• Lemma 1 (joint convexity of $c$), Lemma 2 ($r = r(Q) \iff G(r) = G(r+Q)$), Lemma 3 (properties of $r(Q)$), Corollary 1 ($G(r(Q)) \le \max(G(r), G(r+Q))$);
• Eq. (7) ($C(Q) = (\lambda K + \int_0^Q H)/Q$), Lemma 4 ($H$ increasing, convex, asymptotic slope $hp/(h+p)$), Lemma 5 ($C$ convex), Eq. (8) ($H(Q^*) = C(Q^*)$), Theorem 1 ($(Q, r)$ optimal iff $c(Q,r) = G(r) = G(r+Q)$), Lemma 6 ($A$ increasing convex, $Q = Q^* \iff A(Q) = \lambda K$, comparative statics in $K$);
• Eqs. (18), (20) (the EOQ model: $H_d(Q) = hpQ/(h+p)$ and the formula for $Q^*_d$), Eq. (22) ($G_d \le G$), Lemma 7 ($H_0 \le H_d \le H$, $A \le A_d$), and the first inequality of Theorem 2, $Q^*_d \le Q^*$.

Significance

The theorem is a distribution-free worst-case guarantee for the most common heuristic in inventory practice. It says that the EOQ formula, which needs only the mean demand rate and three cost parameters, loses at most $12.5\%$ against the true optimum, and that the loss is smaller when $Q^*_d/Q^*$ is close to $\frac12$ or to $1$. Combined with the paper's Theorem 2 (the gap $Q^* - Q^*_d$ is bounded as $K$ grows), it implies that the relative loss vanishes as the fixed ordering cost grows. The milestones along the way (the optimality conditions of Theorem 1, the monotonicity of the optimal reorder point, the comparison of $H$ with its EOQ counterpart) are the standard structural facts about continuous $(Q, r)$ systems and are reused throughout the inventory literature.

The result is proved in the paper. No machine-checked version of it, or of the $(Q, r)$ optimality conditions for the continuous cost (1), is known to exist. The platform has related but different formalizations: the discrete cost function with integer $Q$ (InventoryControl_rqDiscrete), the $(R, Q)$ cost under normal demand (InventoryControl_rq), and the EOQ without backorders (InventoryControl_eoq). A complete development here provides the continuous $(Q, r)$ machinery for an arbitrary leadtime-demand distribution.

Difficulty

The paper's proofs differentiate $r(Q)$ and $H(Q)$ twice (Eqs. (4), (5)), which presupposes a leadtime demand with a smooth density. The formalization does not assume one, so that discrete demand, such as the Poisson demand of the paper's own numerical study, is covered. Every step that the paper takes through derivatives, in particular the convexity of $H$ and the slope bound $H' \le hp/(h+p)$, has to be established by other means: through one-sided derivatives or chord arguments for the convex function $G$, whose kinks are where the derivative-based argument breaks. The definition of $r(Q)$ as a minimiser also means its existence and uniqueness must be proved before any property of $H$, $C$ or $A$ can be used.

Formalization scope

• The model is a probability measure $\mu$ on $\mathbb{R}$ (the law of $D$), concentrated on $[0,\infty)$, integrable, with mean $\lambda L$; $G$ is the integral of $h\max(y-x,0) + p\max(x-y,0)$ against $\mu$. The standing assumptions are bundled in IsQRModel: $\lambda, L, h, p > 0$, the conditions on $\mu$, and the unique minimiser of $G$ (paper, p. 90). $K > 0$ is a separate hypothesis. No density is assumed.
• $c$, $r(Q)$, $y^0$, $H$, $H_0$, $C$, $A$ and optimality of an order quantity are defined for an arbitrary cost rate $G$ and applied both to the newsvendor cost and to $G_d$; the EOQ objects $r_d$, $H_d$, $A_d$ are these definitions at $G_d$, and Eqs. (18), (20) are theorems.
• $r(Q)$ is a chosen minimiser of $c(Q,\cdot)$ (never defined by $G(r) = G(r+Q)$, which is Lemma 2). $H(0) := G(y^0)$; right-continuity of $H$ at $0$ is part of the Lemma 4 milestone. Order quantities range over $(0,\infty)$ for $c$ and $C$ and over $[0,\infty)$ for $H$, $H_0$, $A$.
• $Q^*$ in the goal is any $Q > 0$ with $C(Q) \le C(Q')$ for all $Q' > 0$; Lemma 6 asserts that exactly one exists, so the goal is not vacuous. $Q^*_d$ is the explicit square-root formula.
• Readings of informal words: "increasing" in Lemmas 4 and 6 means strictly increasing on $[0,\infty)$; "$Q^*$ increasing, $r^*$ decreasing in $K$" means strictly; "asymptotic slope $hp/(h+p)$" means that every chord of $H$ on $[0,\infty)$ has slope at most $hp/(h+p)$ and $H(Q)/Q \to hp/(h+p)$; Lemma 3 part 3 is stated as strict monotonicity of $r(Q)$ and $r(Q) + Q$, and its derivative clause $-1 < r'(Q) < 0$ is omitted because $r$ need not be differentiable without a density; "the optimal order quantity" means existence and uniqueness; Lemma 7 is stated for $Q \ge 0$.
• A trivializing formalization is ruled out: $C(Q^*_d)$ is the stochastic cost with the reorder point re-optimised in the stochastic model (not the EOQ reorder point $r^*_d$), and no positivity of $C^*$ is assumed (it follows from the model).
• Out of scope: the discrete cost (2), the §4 numerical study, and the unnumbered remarks after Theorem 5.
• Needed infrastructure: interval integrals of convex functions, partial minimisation of jointly convex functions, Jensen's inequality for $\mu$, and one-sided derivatives of convex functions. The generic $(Q, r)$ machinery (optimality conditions for arbitrary convex $G$) is reusable for other continuous-review models. Proofs of any milestone, and alternative proofs that avoid the paper's differentiability assumptions, are welcome.

Selected references

• Yu-Sheng Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• Awi Federgruen and Yu-Sheng 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
• Paul 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
• George Hadley and Thomson M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• Daniel P. Heyman and Matthew J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.

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

The continuous-review $(Q, r)$ policy — order a fixed quantity $Q$ whenever the inventory position falls to the reorder point $r$ — is the textbook policy for a single item with random demand and a positive replenishment leadtime (Hadley and Whitin 1963). Its optimal parameters have no closed form, so practice routinely falls back on the deterministic economic order quantity (EOQ) model with backorders, whose optimum is explicit. How much the deterministic model misjudges the stochastic system's cost is therefore a practical question, and before Zheng (1992) it had been studied only numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978).

Zheng's paper answers it analytically. This mission targets its Theorem 3, which brackets the optimal cost of the stochastic model by the optimal cost of the EOQ model with the same parameters.

Setting

Demands arrive at rate $\lambda>0$ and orders arrive after a fixed leadtime $L>0$. Each order costs $K>0$; holding and backorder costs accrue at rates $h>0$ and $p>0$ per unit per unit time. The leadtime demand $D$ is a nonnegative random variable with $E(D)=\lambda L$. The inventory cost rate at inventory position $y$ is the newsvendor cost

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

assumed to attain its minimum at a unique point $y^0$.

For order quantity $Q>0$ and reorder point $r$, the long-run average cost is

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

Let $r(Q)$ be a reorder point minimizing $c(Q,\cdot)$, and define $H(Q)=G(r(Q))$ for $Q>0$, $H(0)=G(y^0)$, and $C(Q)=c(Q,r(Q))$. The optimal order quantity $Q^*$ minimizes $C$ over $Q>0$, and $C^*=C(Q^*)$. Write $H_0(Q)=H(Q)-G(y^0)$ and

$$C_0(Q)=\frac{\lambda K+\int_0^Q H_0(y)\,dy}{Q},$$

the controllable cost, so that $C(Q)=G(y^0)+C_0(Q)$; $C^*_0=C_0(Q^*)$. The constant $G(y^0)$ is the newsboy cost.

The EOQ model is the same construction with demand constant at $\lambda L$: $G_d(y)=h(y-\lambda L)^+ + p(\lambda L-y)^+$, with functions $H_d$, $C_d$, optimal quantity $Q^*_d=\sqrt{2\lambda K(h+p)/(hp)}$ and optimal cost $C^*_d=C_d(Q^*_d)$.

Formalization targets

Goal: Theorem 3 (p. 97)

$$C^*_0\le\frac{Q^*_d}{Q^*}\,C^*_d,\qquad C^*_d\le C^*\le G(y^0)+\frac{Q^*_d}{Q^*}\,C^*_d.$$

All three inequalities are part of the goal. The weaker remark after the proof, $C^*_d\le C^*\le C^*_d+G(y^0)$, drops the factor $Q^*_d/Q^*$ and is not the goal.

Milestones

1. Eq. (7): $C(Q)=\big(\lambda K+\int_0^Q H(y)\,dy\big)/Q$ for $Q>0$.
2. Eq. (8): $Q>0$ is optimal iff $H(Q)=C(Q)$.
3. Eqs. (13)–(15): $C(Q)=G(y^0)+C_0(Q)$, and $H_0(Q^*)=C_0(Q^*)$.
4. Lemma 6: $A(Q)=QH(Q)-\int_0^QH$ is increasing and convex; $Q=Q^*$ iff $A(Q)=\lambda K$; $Q^*$ increases and $r^*$ decreases in $K$.
5. Eqs. (18), (20): $H_d(Q)=\frac{hp}{h+p}Q$, and $Q^*_d$ is the EOQ optimum.
6. Lemma 8: $\int_0^QH\ge\tfrac12QH(Q)\ge A(Q)\ge\tfrac12QH_0(Q)\ge\int_0^QH_0$, with equalities for deterministic demand.
7. Eq. (22): $G_d(y)\le G(y)$ for all $y$.

Significance

Theorem 3 says that randomness of leadtime demand raises the total optimal cost above the EOQ's, yet the controllable part of that cost — the part the order quantity actually trades off — is smaller than the EOQ's cost, scaled by $Q^*_d/Q^*$. Combined with $Q^*_d\le Q^*$ (Theorem 2 of the paper), the gap $C^*-C^*_d$ is at most the newsboy cost $G(y^0)$, independent of $K$, so the EOQ cost is a good proxy when $K$ is large relative to $G(y^0)$. The same machinery yields the paper's Theorem 5, that using $Q^*_d$ in the stochastic model costs at most $1/8$ more than the optimum.

The result was proved in 1992; no machine-checked proof is known to exist. Formalizing it requires the continuous $(Q,r)$ model as a whole — optimal reorder points, the one-variable reduction through $H$, and the area function $A$ — none of which is in Mathlib. The companion missions of this series formalize Theorems 2, 4 and 5 of the same paper on the same model.

Difficulty

The middle inequality compares minima of two different functions: $C_d\le C$ pointwise follows from Jensen's inequality, but only after the reorder point of each model is chosen optimally, so the comparison has to pass through the definition of $C$ as a minimum over $r$. The outer inequalities depend on Lemma 8, whose proof uses convexity of $H$ and a slope comparison $H'\le H_d'$ (Lemmas 4 and 7). The paper argues these through first and second derivatives of $r(Q)$ and $G$, which exist only when the leadtime demand has a smooth distribution; the formal statements assume no density, so a proof must either avoid derivatives or handle one-sided ones. Existence of optimal reorder points and of $Q^*$ is asserted in the paper without a separate argument.

Formalization scope

Everything lives in the namespace ZhengQR.CostBounds. The machinery (qrCost, reorderPt, idealPt, Hfun, Cfun, Afun, H0fun, C0fun, IsOptQty) is defined for an arbitrary $G:\mathbb R\to\mathbb R$ and instantiated at the stochastic $G$ and at $G_d$. A structure QRModel holds the parameters, the demand distribution $\mu$ (a probability measure on $\mathbb R$) and the standing assumptions.

Conventions committed to:

• Positivity of $\lambda,L,K,h,p$; $D\ge0$ almost surely; $D$ integrable with $E(D)=\lambda L$; $G$ has a unique minimizer (p. 90). No density is assumed.
• $r(Q)$ is a chosen minimizer of $c(Q,\cdot)$ over $\mathbb R$, not a solution of $G(r)=G(r+Q)$; $y^0$ is a chosen minimizer of $G$. Both use junk value $0$ when no minimizer exists, which never happens under the assumptions.
• $H(0)=G(y^0)$; statements about $H$ and $A$ are on $[0,\infty)$, about $c$, $C$, $C_0$ for $Q>0$.
• "Optimal order quantity" means $Q>0$ and $C(Q)\le C(Q')$ for all $Q'>0$; the goal takes any such $Q^*$ and Lemma 6 states that exactly one exists, so the goal is not vacuous.
• $C^*_d$ is $C_d(Q^*_d)$, with $Q^*_d$ the explicit formula (20); milestone 5 proves it is the EOQ optimum. $C^*_0$ is $C_0(Q^*)$, which equals $\min_{Q>0}C_0$ by (13).
• "Increasing" in Lemma 6 is read strictly, as the proof gives. Lemma 8 is stated for $Q\ge0$; "deterministic" means $\mu$ is the Dirac mass at $\lambda L$.

A formalization in which $C^*_d$ were an arbitrary number, or $Q^*$ an arbitrary positive real, would make the goal false or empty; both are tied to the model above.

Needed infrastructure: existence of minimizers of convex coercive functions on $\mathbb R$, differentiation of parametric integrals $\int_{r(Q)}^{r(Q)+Q}G$, and properties of the newsvendor cost (convexity, coercivity, Jensen). Most of it is reusable for any continuous-review inventory model. Proofs of any milestone, and of lemmas the paper uses but this mission does not list (Lemmas 2–5, 7), 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
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• P. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• 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 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

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