Theorem 5 — $R = (C(Q^_d) - C^)/C^* \le 1/8 - \frac12(\frac12 - Q^_d/Q^)^2 \le 1/8$

Proved

ZhengQR.EOQHeuristic.eoq_relative_cost_increase_le

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

eoqinventoryp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1qr-policy

Consider a single-item continuous-review $(Q, r)$ inventory system with demand rate $\lambda > 0$ , leadtime $L > 0$ , fixed ordering cost $K > 0$ , holding cost rate $h > 0$ and backorder penalty rate $p > 0$ . The leadtime demand $D \ge 0$ has mean $E(D) = \lambda L$ , and the newsvendor cost $G(y) = E[h(y-D)^+ + p(D-y)^+]$ attains its minimum at a unique point. For an order quantity $Q > 0$ let

C(Q) = \min_r \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}

be the average cost when the reorder point is chosen optimally for $Q$ . Let $Q^*$ be an optimal order quantity, $C^* = C(Q^*)$ , and let $Q^*_d = \sqrt{2\lambda K(h+p)/(hp)}$ be the order quantity of the EOQ model with backorders. Then the relative cost increase from using $Q^*_d$ instead of $Q^*$ satisfies

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

Using the deterministic EOQ quantity in the stochastic model, with the reorder point re-optimised for it, therefore never costs more than $12.5\%$ above the optimum, for every leadtime-demand distribution.

Formalization Note $C(Q^*_d)$ is the stochastic cost at the EOQ quantity, with the reorder point chosen optimally for $Q^*_d$ in the stochastic model (not the EOQ model's reorder point). $Q^*$ is any order quantity with $Q^* > 0$ and $C(Q^*) \le C(Q)$ for all $Q > 0$ ; its existence and uniqueness is the Lemma 6 milestone. No positivity of $C^*$ is assumed: it follows from the model.

Preamble

import Mathlib
import Definitions.Def_ZhengQR_EOQHeuristic_qrCost
import Definitions.Def_ZhengQR_EOQHeuristic_costCurves
import Definitions.Def_ZhengQR_EOQHeuristic_stochasticModel
open MeasureTheory Filter Topology

Formal statement

namespace ZhengQR.EOQHeuristic

theorem eoq_relative_cost_increase_le {lam L K h p : ℝ} {μ : Measure ℝ} (hM : IsQRModel lam L h p μ) (hK : 0 < K) (Qs : ℝ)
    (hQs : IsOptQty (newsvendorCost μ h p) lam K Qs) :
    (optCost (newsvendorCost μ h p) lam K (eoqQty lam K h p) - optCost (newsvendorCost μ h p) lam K Qs) / optCost (newsvendorCost μ h p) lam K Qs
        ≤ 1 / 8 - 1 / 2 * (1 / 2 - eoqQty lam K h p / Qs) ^ 2 ∧
      1 / 8 - 1 / 2 * (1 / 2 - eoqQty lam K h p / Qs) ^ 2 ≤ (1 / 8 : ℝ) := by sorry

end ZhengQR.EOQHeuristic

Source

Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1), 1992, p. 98, Theorem 5 (proof pp. 98–99)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

We assume real numbers $\lambda, L, K, h, p$ and a measure $\mu$ on the real line. All of these are implicit parameters, so the statement covers every choice of them. We also assume a real number $Q^*$ and three hypotheses:

Model hypothesis: $\mathrm{IsQRModel}(\lambda, L, h, p, \mu)$ holds. This predicate comes from an imported definitions module whose body is not shown, so the read-back cannot say what it requires of $\lambda$ , $L$ , $h$ , $p$ and $\mu$ . For example, it cannot say whether they must be positive, or whether $\mu$ must be a probability measure. Whatever it requires is the only constraint on these five parameters. $K$ is not an argument of this predicate. $L$ appears only here and nowhere in the conclusion.
Positive setup cost: $K > 0$ .
Optimality of $Q^*$ : $\mathrm{IsOptQty}(G, \lambda, K, Q^*)$ holds. Here $G = \mathrm{newsvendorCost}(\mu, h, p)$ is a function built from $\mu$ , $h$ and $p$ . Neither $\mathrm{IsOptQty}$ nor $\mathrm{newsvendorCost}$ is unfolded here, because their definitions are also in modules that are not shown. In particular, the read-back cannot say whether "optimal" means a global minimiser of the cost defined next, whether $Q^*$ must be positive, or whether $Q^*$ is required to be unique.

Write

C(Q) = \mathrm{optCost}(G, \lambda, K, Q)

for the cost of order quantity $Q$ , where $\mathrm{optCost}$ is an unseen imported definition. Write

Q_E = \mathrm{eoqQty}(\lambda, K, h, p)

for the quantity given by the imported definition $\mathrm{eoqQty}$ , which depends on $\lambda, K, h, p$ but not on $\mu$ . Set $r = Q_E / Q^*$ .

The theorem states both of the following inequalities:

\frac{C(Q_E) - C(Q^*)}{C(Q^*)} \;\le\; \frac18 - \frac12\Bigl(\frac12 - r\Bigr)^2 \qquad\text{and}\qquad \frac18 - \frac12\Bigl(\frac12 - r\Bigr)^2 \;\le\; \frac18 .

The middle expression simplifies to $\tfrac12\, r(1-r)$ . The second inequality holds for every real $r$ , because a square is never negative, so none of the hypotheses are needed for it. All the content is in the first inequality. It bounds the relative cost increase of $Q_E$ over $Q^*$ by $\tfrac12 r(1-r)$ , and taken together the two inequalities bound that increase by $\tfrac18$ .

Where the right-hand side $\tfrac12 r(1-r)$ is negative, that is when $r < 0$ or $r > 1$ , the first inequality requires the relative change to be strictly negative. The statement does not rule these cases out itself. Whether they can happen depends on the hidden definitions.

Degenerate cases:

$Q^* = 0$ : division by zero returns $0$ , so $r = 0$ and the right-hand side is $\tfrac18 - \tfrac18 = 0$ . The claim becomes: the relative change is $\le 0$ .
$C(Q^*) = 0$ : the left-hand quotient is $0$ by the same rule, so the claim becomes $0 \le \tfrac12 r(1-r)$ , which is the same as $0 \le r \le 1$ .
$Q^* = 0$ and $C(Q^*) = 0$ together: the claim is $0 \le 0$ , which holds automatically.
$C(Q^*) < 0$ : dividing by a negative number reverses the sense of the comparison between $C(Q_E)$ and $C(Q^*)$ . The statement allows this case unless the hidden definitions exclude it.
Vacuous cases: if $\mathrm{IsQRModel}$ or $\mathrm{IsOptQty}$ cannot be satisfied for some parameter values, the theorem says nothing about those values. That cannot be checked without the definition bodies.
Other defaults: whether the hidden definitions of $C$ , $G$ or $Q_E$ use integrals of non-integrable functions, square roots of negative numbers, or other default-valued operations cannot be determined from the code shown.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 5 — R=(C(Qd∗)−C∗)/C∗≤1/8−12(12−Qd∗/Q∗)2≤1/8R = (C(Q^*_d) - C^*)/C^* \le 1/8 - \frac12(\frac12 - Q^*_d/Q^*)^2 \le 1/8R=(C(Qd∗​)−C∗)/C∗≤1/8−21​(21​−Qd∗​/Q∗)2≤1/8

Theorem 5 — $R = (C(Q^_d) - C^)/C^* \le 1/8 - \frac12(\frac12 - Q^_d/Q^)^2 \le 1/8$