Inventory and Supply Chain

Motivation

The newsvendor problem is the basic model of inventory under uncertain demand. A decision maker orders $q$ units before demand $D$ is observed, and pays a unit backordering cost $b$ for each unit of unmet demand and a unit holding cost $h$ for each unit left over. When the demand distribution is known, the optimal order is a quantile of it. In practice the distribution is unknown and the decision maker holds historical data, often including features: observable covariates such as the day of the week, the weather or a recent sales trend, recorded alongside each past demand.

Rudin and Vahn (MIT Sloan Working Paper 5036-13, version of February 6, 2014, from MIT DSpace; published as Ban and Rudin, Operations Research 67(1), 2019, doi:10.1287/opre.2018.1757) propose to learn the order quantity directly as a linear function of the features, by minimizing the empirical newsvendor cost over the training data, with or without a regularization penalty. Their question is the one any data-driven decision rule must answer: how much worse can the learned rule do on new data than it did on the data it was fitted to? When the number of features $p$ is comparable to the sample size $n$ ("big data"), a bound that grows with $p$ says nothing, and the paper's Theorem 2 gives one for the regularized rule that does not depend on $p$.

This mission formalizes that bound, Theorem 2 of the working paper, together with the results its proof is assembled from. All page and result numbers refer to the 2014 working paper, not to the published article.

Setting

Cost. For an order $q$ and a demand $d$, the newsvendor cost is

$$C(q;d)=b\,(d-q)^+ + h\,(q-d)^+ ,\qquad b,h>0 .$$

Write $b\vee h=\max(b,h)$.

Data. A data point is a pair $z=(x,d)$ of a feature vector $x\in\mathbb R^p$ and a demand $d\in\mathbb R$. Features lie in a domain $\mathcal X$ inside the ball $\|x\|_2^2\le X_{\max}^2$, and demands lie in $\mathcal D=[0,\bar D]$. A sample $S_n=\{(x_i,d_i)\}_{i=1}^n$ consists of $n$ independent draws from an unknown probability distribution $\mu$ concentrated on $\mathcal X\times\mathcal D$.

Rules and risks. A vector $q\in\mathbb R^p$ defines the linear decision rule $q(x)=q^\top x$. Its true risk and empirical risk are

$$R_{true}(q)=\mathbb E_{(x,d)\sim\mu}\bigl[C(q^\top x;d)\bigr],\qquad \hat R(q;S_n)=\frac1n\sum_{i=1}^n C(q^\top x_i;d_i).$$

The regularized algorithm (NV-reg). For a parameter $\lambda>0$, the rule $\hat q=\hat q(S_n)$ minimizes

$$\hat R(q;S_n)+\lambda\|q\|_2^2\qquad\text{over } q\in\mathbb R^p .$$

The objective is strictly convex, so the minimizer is unique. Following Appendix B of the paper, the rules the algorithm outputs on samples from $\mathcal X\times\mathcal D$ are assumed to map $\mathcal X$ into $\mathcal D$ (the paper's $\mathcal Q\subset\mathcal D^{\mathcal X}$): the learned order quantity is never negative and never exceeds the demand cap.

Uniform stability. An algorithm is uniformly stable with parameter $\alpha_n$ if removing one observation from any sample changes the loss of its output at any test point by at most $\alpha_n$ (Bousquet and Elisseeff's Definition 6, the paper's Definition 1).

Formalization targets

Goal: Theorem 2 (p. 9)

For every $\delta\in(0,1)$ and $n\ge1$, with probability at least $1-\delta$ over $S_n$,

$$|R_{true}(\hat q)-\hat R(\hat q;S_n)|\le\frac{(b\vee h)^2X_{\max}^2}{n\lambda}+\Bigl(\frac{2(b\vee h)^2X_{\max}^2}{\lambda}+(b\vee h)\bar D\Bigr)\sqrt{\frac{\ln(2/\delta)}{2n}} .$$

The dimension $p$ appears nowhere in the bound.

Milestones, in the order of the proof (p. 32)

1. Lemma 5 (p. 28). For $q,d\in[0,\bar D]$, $|C(q;d)|\le(b\vee h)\bar D$, and the bound is attained.
2. Display (31) (p. 31). $C$ is convex in its first argument and $(b\vee h)$-Lipschitz in it, i.e. $(b\vee h)$-admissible in the sense of Definition 2.
3. Theorem 5 (p. 31), Bousquet and Elisseeff's Theorem 22: regularization in a reproducing kernel Hilbert space with a $\sigma$-admissible loss and kernel bound $\kappa^2$ has uniform stability $\sigma^2\kappa^2/(2\lambda n)$. This is an existing platform statement, referenced rather than restated.
4. Theorem 4 (p. 30). (NV-reg) is uniformly stable with parameter $\alpha_n^r=(b\vee h)^2X_{\max}^2/(2n\lambda)$.
5. Theorem 6 (p. 31). Any algorithm with uniform stability $\alpha_n$ and loss in $[0,M]$ satisfies, with probability at least $1-\delta$,

$$|R_{true}(A,S_n)-\hat R(A,S_n)|\le2\alpha_n+(4n\alpha_n+M)\sqrt{\frac{\ln(2/\delta)}{2n}} .$$

Significance

The result. Theorem 2 bounds the generalization gap of the regularized feature-based newsvendor rule at rate $O(1/\sqrt n)$ with constants that depend on the costs, the demand cap, the feature radius and $\lambda$, but not on the number of features. It gives a theoretical basis for regularizing when $p/n$ is not small, and it indicates how to scale $\lambda$ with the feature radius. The companion bound for the unregularized rule (Theorem 1) grows linearly in $p$.

Formalizing it. The theorem is proved in the paper, but its proof is short and relies on cited results: Theorem 5 and Theorem 6 are stated with references to Bousquet and Elisseeff and no proof of their own, and the paper's Theorem 6 is a two-sided variant of Bousquet and Elisseeff's Theorem 12 that is only sketched. None of these results has a machine-checked proof. A formalization produces a checked two-sided stability-to-generalization theorem for general algorithms (reusable for any stable learner), a checked stability bound for a regularized piecewise-linear loss, and the newsvendor bound itself, with the constants the proof actually supports.

Difficulty

The bound is not a uniform-convergence argument: the class of linear rules on $\mathbb R^p$ has complexity growing with $p$, so any bound that holds simultaneously for all rules in the class depends on $p$. The bound must exploit the specific rule produced by the algorithm. The two analytic steps that carry this are the stability of the regularized minimizer, which needs a strong-convexity comparison between the full and the leave-one-out objective, and a concentration inequality of bounded-differences type for a function of the whole sample whose differences are controlled only through stability.

The leave-one-out comparison is a known pitfall. If the leave-one-out problem is run literally on $n-1$ points it carries the weight $1/(n-1)$, and the comparison argument then gives twice the constant of Theorem 4. The stated constant holds for the leave-one-out objective that keeps the weight $1/n$, which is the form of Theorem 5.

Formalization scope

Representation. Features are EuclideanSpace ℝ (Fin p), rules are vectors acting by the inner product, and data points live in EuclideanSpace ℝ (Fin p) × ℝ. The cost is the published newsboy loss with overage cost $h$ and underage cost $b$; the empirical and true risks are the published empirical and generalization errors, and the (NV-reg) objective and its $1/n$-weighted leave-one-out version are the published regularized objectives of Bousquet and Elisseeff. The regularizer is $\lambda\|q\|_2^2$ (the display prints both $\lambda\|q\|_2^2$ and $\lambda\|q\|_2$; the text calls the problem a quadratic program). "With probability at least $1-\delta$" is stated as: the event on which the gap exceeds the bound has measure at most $\delta$ under the product measure $\mu^n$.

Standing assumptions and pinned hypotheses.

1. $b,h,\lambda>0$, $X_{\max},\bar D\ge0$, $n\ge1$, $\delta\in(0,1)$.
2. $\mu$ is a probability measure giving full mass to $\mathcal X\times[0,\bar D]$, with $\|x\|_2^2\le X_{\max}^2$ on $\mathcal X$ (§3, p. 9; the page writes the ball as $\|x\|_2^2\le X_{\max}$, while Theorem 2's "$X_{\max}^2$ as the largest possible value of $\|x\|_2^2$" and Theorem 5's note fix the reading).
3. The algorithm is any map $S_n\mapsto\hat q(S_n)$ whose value minimizes the (NV-reg) objective, measurable in $S_n$ (Appendix B: "all functions are measurable").
4. The range assumption of Appendix B: for samples from $\mathcal X\times\mathcal D$, $\hat q^\top x\in[0,\bar D]$ for $x\in\mathcal X$.
5. The last constant is $(b\vee h)\bar D$, the loss bound $M$ from Lemma 5 that the proof feeds into Theorem 6; display (6) prints $\bar D$ there.
6. The convention that all sets are countable, and the intercept convention $x^1=1$, are not imposed.

Trivializing formalization ruled out. The range assumption is quantified only over feature vectors in $\mathcal X$ and over samples drawn from $\mathcal X\times\mathcal D$; stated over the whole ball $\|x\|_2\le X_{\max}$, it would force $\hat q=0$ (both $\hat q^\top x$ and $\hat q^\top(-x)$ would lie in $[0,\bar D]$) and the goal would be nearly empty.

What is needed and reusable. McDiarmid's two-sided bounded-differences inequality under product measures; integrability of bounded measurable losses; existence and properties of minimizers of strongly convex objectives on $\mathbb R^p$; the comparison argument behind Theorem 5. Theorem 6 is stated for an arbitrary data space and hypothesis space and is reusable for any uniformly stable algorithm. Contributions to the Theorem 5 reference and to McDiarmid's inequality benefit other missions as well.

Selected references

• C. Rudin and G.-Y. Vahn, The Big Data Newsvendor: Practical Insights from Machine Learning, MIT Sloan School Working Paper 5036-13, version of February 6, 2014 (MIT DSpace). The version formalized here.
• G.-Y. Ban and C. Rudin, The Big Data Newsvendor: Practical Insights from Machine Learning, Operations Research 67(1):90–108, 2019. https://doi.org/10.1287/opre.2018.1757
• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2:499–526, 2002. https://jmlr.org/papers/v2/bousquet02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, London Math. Soc. Lecture Note Series 141, 148–188, 1989. https://doi.org/10.1017/CBO9781107359949.008

Motivation

Periodic-review inventory systems face a simple choice each period: how much to order before the next demand is known. When unmet demand is lost, the order can affect the stock available several periods later without preserving a backlog that records earlier shortages. This makes the optimal policy difficult to describe when replenishment takes time. An order-up-to policy offers a practical rule: order enough to bring the inventory position to a fixed level. Huh, Janakiraman, Muckstadt and Rusmevichientong ask when that simple rule performs as well as the best admissible lost-sales policy as the penalty for a lost unit grows. Their working paper, pp. 3–4 and 17–18, proves asymptotic optimality for a particular level obtained from a related backorder system.

The motivating costs are concrete. A lost sale may represent an expedited service part or a missed sale whose cost is much larger than one period of holding inventory. The paper's central comparison concerns the high-penalty regime while holding the demand law, lead time and holding rate fixed. The fixed-level policy can be computed from the distribution of demand over the lead time plus the order period; it does not require solving the full lost-sales control problem. The paper also supplies a finite-penalty bound, which this mission retains as a milestone. Huh et al., pp. 3–4, 17–18.

Setting

Let $D_1,D_2,\ldots$ be independent, identically distributed nonnegative demands with finite positive mean. An order takes a fixed integer lead time $\tau\ge1$ to arrive. At the start of period $t$, the order placed $\tau$ periods earlier arrives; then a new order is placed, and demand $D_t$ is observed. Unmet demand is lost. At period end, each unit remaining on hand incurs holding cost $h>0$, and each lost unit incurs penalty $b>0$. The inventory position counts on-hand units and outstanding orders. An order-up-to-$S$ policy raises this position to $S\ge0$ whenever possible.

Write $C^{\mathcal L,S}(h,b)$ for the long-run average cost of that policy and $C^{\mathcal L*}(h,b)$ for the infimum over admissible policies. The corresponding backorder system retains unmet demand as negative net inventory and charges $b$ per backordered unit per period. For an order-up-to level $S$, its stationary average cost is

$$C^{\mathcal B,S}(h,b)=h\mathbb E[(S-\mathbf D)^+]+b\mathbb E[(\mathbf D-S)^+],\qquad \mathbf D=\sum_{i=1}^{\tau+1}D_i.$$

The newsvendor level $S^{\mathcal B*}(h,b)$ is the smallest nonnegative $S$ with $\Pr(\mathbf D\le S)\ge b/(b+h)$; it attains the best backorder order-up-to cost $C^{\mathcal B*}(h,b)$. The paper's Assumption 1 concerns this lead-time demand $\mathbf D$: if $m_{\mathbf D}(t)=\mathbb E[\mathbf D-t\mid\mathbf D>t]$ when the conditioning event has positive probability and zero otherwise, then $m_{\mathbf D}(t)/t\to0$ as $t\to\infty$. Huh et al., pp. 3–4, 9, 11–12.

Formalization targets

Asymptotically optimal order-up-to level

Fix $h$, $\tau$ and the demand law satisfying Assumption 1. Set $S_{b+\tau h}=S^{\mathcal B*}(h,b+\tau h)$. The goal is the equivalent multiplicative form of Theorem 15(b): for every $\varepsilon>0$, all sufficiently large $b$ satisfy

$$\inf_{S\ge0}C^{\mathcal L,S}(h,b)\le C^{\mathcal L,S_{b+\tau h}}(h,b)\le(1+\varepsilon)C^{\mathcal L*}(h,b).$$

The infimum over order-up-to levels captures the paper's best such policy. The right-hand comparator remains the infimum over all admissible lost-sales policies. The multiplicative form also covers an almost-surely constant demand law, where both costs can be zero and a literal ratio would be undefined. Huh et al., Theorem 15(b), p. 17.

Explicit finite-penalty bound

Theorem 15(a) is a milestone. With $S'=S^{\mathcal B*}(h,b/(\tau+1))$ and $\psi(S';h,q)=q\mathbb E[(\mathbf D-S')^+]/(h\mathbb E[(S'-\mathbf D)^+])$, its factor is

$$\frac{1+\nu_b\psi(S';h,b/(\tau+1))}{1+\psi(S';h,b/(\tau+1))},\qquad \nu_b=\frac{(b+\tau h)(\tau+1)}{b}.$$

The milestone states the bound where the expected holding quantity in $\psi$ is positive. Earlier milestones state the pathwise comparison of the systems, the two-sided average-cost comparison with penalties $b/(\tau+1)$ and $b+\tau h$, the lower bound on unrestricted lost-sales optimal cost, the newsvendor formula, and the backorder sensitivity results used by the theorem. Huh et al., Lemmas 5, 9, 13 and Theorems 6, 15, pp. 11–18.

Significance

The theorem gives a specific computable stock level whose relative cost loss vanishes in the high-penalty regime. It addresses the gap between a tractable backorder benchmark and the more difficult lost-sales control problem. The finite-penalty factor states how the comparison depends on lead time, holding cost, penalty and the shortage-to-holding ratio; the asymptotic statement alone would not quantify that dependence. The paper establishes these mathematical results; the mission asks for machine-checked proofs of the stated Lean targets. Huh et al., pp. 17–18.

Formalizing the result would also supply reusable infrastructure for coupled inventory systems: measurable demand-path laws, pathwise recursions with delayed delivery, extended nonnegative long-run costs, and a clean comparison between an explicit policy and the infimum over unrestricted policies. The backorder newsvendor and mean-residual-life components can be reused beyond this particular lost-sales model.

Difficulty

The backorder system has a closed stationary cost formula, while a lost-sales order-up-to process generally cannot be replaced directly by that formula. The paper notes that its on-hand inventory distribution need not converge from every starting state, even under a fixed order-up-to policy. One must therefore justify the long-run comparison without assuming stationarity from an arbitrary start. A second difficulty is the benchmark: comparing only against other order-up-to policies is too weak to establish Theorem 15, because the goal uses the optimal cost over all admissible lost-sales policies. Huh et al., pp. 14–16, 18.

Formalization scope

Lean reuses the published CappedBaseStock lost-sales model. Its demands are nonnegative and i.i.d. with finite positive mean; $\tau\ge1$ and $h,b>0$. Period zero in Lean is period one in the paper. Both coupled processes start with zero on-hand stock and an empty pipeline. Inventory $X_t$ is read immediately after delivery, before current demand. Lost-sales costs lie in $[0,\infty]$ and use the limsup of expected Cesàro averages; the backorder closed form uses real Bochner expectations under finite-mean demand. The paper's stationary lost-sales cost and this Cesàro cost are identified using its long-run results, but those convergence results are outside this proposal. Huh et al., pp. 14–16.

The paper prints nonnegative rates in Theorem 15, while its displayed newsvendor fraction and shortage-to-holding ratios require positive denominators. Theorem 6(a) therefore states the ratio limit for nonconstant demand laws. The main theorem uses a multiplicative limit bound that also covers constant demand, where the printed ratio is undefined.

The quantity $C^{\mathcal L*}$ is an infimum over measurable, history-dependent policies with private randomization; no attaining policy is assumed. The backorder optimum is an infimum over nonnegative order-up-to levels. Assumption 1 is imposed on the sum of $\tau+1$ demands, and the limit $b\to\infty$ is expressed by a positive threshold uniform over all parameter records with the fixed lead time and holding rate. The mission excludes a restricted policy comparator, a fixed penalty, a one-period lead-time specialization, and Assumption 1 on single-period demand. Solvers may contribute proofs of any milestone, along with finite-mean and measurability lemmas needed to connect the model to the backorder benchmarks.

Selected references

• W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-up-to Policies in Lost Sales Inventory Systems, working paper, December 4, 2006; published in Management Science 55(3), 2009. DOI: 10.1287/mnsc.1080.0945.
• G. Janakiraman, S. Seshadri and G. Shanthikumar, A Comparison of the Optimal Costs of Two Canonical Inventory Systems, working paper, Stern School of Business, New York University, 2005; bound quoted in Huh et al., §5, p. 13. Quoted source.

Motivation

Many supply chains move stock through a central warehouse to the retail locations that face customer demand. Deciding how much the warehouse should order from outside, and how much it should ship to each retailer and when, is a stochastic dynamic program whose state contains every stock level and every outstanding order. Exact solution is out of reach except for the smallest systems, so structural results that reduce such a problem to single-location problems matter in practice.

Timeline.

• Clark and Scarf (Management Science 1960) showed that the finite-horizon, discounted problem of a serial system decomposes: an optimal policy is obtained by solving the most downstream location alone, charging its shortfalls to the upstream location through an induced penalty cost, and then solving the upstream location as a single-location problem with that penalty.
• Iglehart (Management Science 1963, and a 1963 chapter in Multistage Inventory Models and Techniques) established the infinite-horizon theory of the single-location problem with a fixed order cost: optimality of stationary $(s,S)$ policies under discounted and average costs, and the convergence of value iteration.
• Federgruen and Zipkin (Operations Research 1984) carried the decomposition to the infinite horizon for a depot and one retail outlet, under discounted costs (Theorem 1) and under the average-cost criterion (Theorem 2). This mission is about the average-cost case, §3 of that paper.

Setting

Time is divided into periods. A depot orders from an outside supplier with lead time $L \ge 0$ and supplies a retail outlet with shipment lead time $l \ge 0$. The demand $u$ in each period is a nonnegative random variable with law $\nu$ and finite mean $\mu$; demands in different periods are independent and identically distributed. Unmet demand at the outlet is backordered.

The state is $(\tilde y, v^d, x^r)$:

• $\tilde y = (y^1,\dots,y^L)$ lists the orders placed $1,\dots,L$ periods ago;
• $v^d$ is the depot's echelon inventory, its own stock plus the outlet's inventory position;
• $x^r$ is the outlet's inventory position, its stock plus shipments in transit.

In each period the decision is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$, where $y^L$ is the order arriving now. The state then moves to $((y, y^1,\dots,y^{L-1}),\, v^d + y^L - u,\, x^r + z - u)$.

Costs are a fixed order cost $K$, proportional order and shipment rates $c^d$ and $c^r$, a holding rate $h^d$ on system inventory, an extra holding rate $h^r$ at the outlet and a backorder penalty rate $p^r$. After the paper's accounting transformation, the one-period cost is

$$c^d(y) + D(v^d + y^L) + c^r z + R(x^r + z),$$

with $c^d(y) = K + c^d y$ for $y > 0$ and $c^d(0) = 0$, $D(v) = h^d v$, and, at $\alpha = 1$,

$$R(x) = -h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r) E[x - u^{(l+1)}]^+ ,$$

where $u^{(l+1)}$ is the demand over $l + 1$ periods. The critical number $x^{r*}$ is a minimizer of $R$. The stationary induced penalty is $P(x) = R(x) - R(x^{r*})$ for $x < x^{r*}$ and $0$ otherwise.

For a policy $\pi$ and initial state $s$, $B_n(s \mid \pi)$ is the expected cost of the first $n$ periods and $B(s \mid \pi) = \limsup_n B_n(s \mid \pi)/n$ is the average cost. Problem IH asks for a policy minimizing $B(s\mid\cdot)$ from every state. The depot problem IH$^d$ has states $(\tilde y, v^d)$, orders $y \ge 0$ and one-period cost $c^d(y) + D(v^d + y^L) + P(v^d + y^L)$. Its minimal average cost is $a^d$. The outlet problem has states $x^r$, shipments $z \ge 0$ and one-period cost $c^r z + R(x^r + z)$. The policy $\pi^*$ orders by an optimal stationary policy of IH$^d$ and ships $z = \max(0, \min(x^{r*}, v^d + y^L) - x^r)$: up to the critical number if the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 2 (p. 828)

With $\alpha = 1$ and $c^d = c^r = 0$, the policy $\pi^*$ is measurable and feasible from every physical state, and for every such state $s$ and every measurable feasible policy $\pi$,

$$B(s \mid \pi^*) \le B(s \mid \pi).$$

Milestones

• Property (f) (p. 824): $g^r_n(x)/n \to B^r(x) = c^r\mu + R(x^{r*})$ for the outlet program $g^r_n$.
• Eq. (4) (p. 823), for $0 \le \alpha \le 1$: $\hat g_n(\tilde y, v^d, x^r) = \hat g^d_n(\tilde y, v^d) + g^r_n(x^r)$.
• §3 claims (p. 828): with $c^r = 0$, $x^{r*}$ is the critical number of every period, $g^r_n(x) = nR(x^{r*})$ for $x \le x^{r*}$, $\hat P_n = P$, $\hat g^d_n = g^d_n$ and $\hat g_n = g_n$.
• §3 display (p. 828): $\hat g_n(\tilde y, v^d, x^r)/n \to a = a^d + R(x^{r*})$.
• Lemma 5 (p. 828): $B(s \mid \pi^*) = a$.
• Proof of Theorem 2 (p. 828): $\hat g_n(s) \le B_n(s \mid \pi)$ for every measurable feasible $\pi$.

Significance

The result. Theorem 2 reduces an average-cost problem with a multidimensional state to two problems with smaller states: a single-location $(s,S)$-type problem for the depot with a known convex penalty $P$, and a myopic critical-number rule for the outlet. The optimal system cost is the sum $a^d + a^r$ of their optimal costs. The paper uses this to compute optimal policies with standard single-location software, and its §5 builds heuristics for several outlets on the same decomposition.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal proof has to make precise what the paper leaves to "standard arguments":

• the class of measurable history-dependent policies;
• the expected costs of policies with unbounded one-period costs;
• the passage from history-dependent to Markov policies;
• the transient of $\pi^*$ when the outlet starts above its critical number.

Difficulty

The obvious argument would identify the average-cost optimal value through an average-cost optimality equation on the full state space and verify that $\pi^*$ attains it. No such equation is available here. The state space is unbounded, the one-period costs are unbounded both above and below in the state, and the depot's fixed cost makes its value functions $K$-convex rather than convex.

The paper's route avoids that equation but needs three separate facts:

• value iteration for the whole system, divided by $n$, converges to $a^d + a^r$, which rests on Iglehart's convergence for the depot and on the stationarity of the penalties when $c^r = 0$;
• the finite-horizon value bounds the cost of every history-dependent policy, not only of Markov ones;
• $\pi^*$ achieves $a$ from every state, including states with $x^r > x^{r*}$, where it does not ship at all until demand has brought the outlet below its critical number.

Formalization scope

• Representation. A state is a triple in $(\mathrm{Fin}\,L \to \mathbb R) \times \mathbb R \times \mathbb R$. For $L = 0$ the order placed now arrives at once. Time runs forward in Lean; the paper numbers periods backward. Finite-horizon value functions keep the paper's index $n$ (periods remaining). Each "min" of programs (1), (2), (3), (5) is a real infimum over the constraint set.
• Policies and costs. Policies are deterministic, history-dependent and measurable, and they must be feasible along every demand realization. $B_n$ is an extended real (expected positive part minus expected negative part of each period's cost). $B$ is a $\limsup$ in the extended reals, and the optimal average costs are infima in the extended reals.
• Standing assumptions (p. 821):
  • $K, h^d, h^r, p^r > 0$;
  • demands i.i.d., nonnegative, without atoms ("for convenience we shall assume $u$ is continuous") and with finite mean.
• Added hypotheses.
  • States are restricted to the physical ones, $\tilde y \ge 0$ and $x^r \le v^d$.
  • $c^d = c^r = 0$. The paper reduces to this case "without loss of generality", on the grounds that average proportional costs equal $c^d\mu$ and $c^r\mu$ "under all interesting policies" (p. 827). That class is never specified, and the proofs are written for $c^d = c^r = 0$. The general-cost version is the paper's informal reduction and is not part of the goal.
  • Eq. (4) is stated for $0 \le \alpha \le 1$ with $K, h^d, h^r, p^r > 0$ and $c^d, c^r \ge 0$ (so that it covers §3's case $c^d = c^r = 0$), and with the relation $\alpha^l p^r \ge (1 - \alpha^l)h^d$, which the paper names on p. 827; it holds automatically at $\alpha = 1$.
• Ruling out trivial readings.
  • $\pi^*$ is built from a depot rule $\sigma^d$ assumed optimal for IH$^d$ from every depot state. Its existence is Iglehart's theorem, cited and not formalized; no $(s,S)$ form is required.
  • The goal quantifies over all measurable feasible policies, and $\pi^*$'s own feasibility is a conclusion, so a vacuous policy class cannot satisfy it.
  • A sorry-free check in the workspace exhibits an instance (exponential demand) meeting every standing hypothesis other than the optimality of $\sigma^d$, including the existence of $x^{r*}$.
• Reusable infrastructure. The definitions of history-dependent policies and of extended-real expected and average costs for controlled processes driven by i.i.d. real noise are generic, and could be reused for other inventory and queueing models. Contributions are welcome on any milestone, and especially on a formal version of the Markov reduction (Dynkin–Yushkevich III.1) for this setting and on Iglehart's convergence of $g^d_n/n$.

Selected references

• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. L. Iglehart, Dynamic Programming and Stationary Analyses of Inventory Problems, Chapter 1 in H. Scarf, D. Gilford and M. Shelly (eds.), Multistage Inventory Models and Techniques, Stanford University Press, 1963.
• E. B. Dynkin and A. A. Yushkevich, Controlled Markov Processes, Springer, 1979.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

Motivation

Multiechelon inventory theory studies supply systems in which stock is held at several levels: here, a depot that orders from an outside supplier and a retail outlet that is replenished from the depot and faces random customer demand. The question is how much to order and ship in each period so as to minimize expected holding, shortage and ordering costs over an infinite horizon. Clark and Scarf (Management Science, 1960) showed that the finite-horizon problem of a serial system decomposes into single-location problems linked by an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) extended the decomposition to the infinite horizon under discounted and average costs, and then asked what it costs to compute an optimal policy.

In the reduced single-location problem the only nonlinear part of the one-period cost is the expected induced penalty $P^L$. Any algorithm for the reduced problem (Veinott–Wagner type policy computations, for instance) evaluates $P^L$ many times. In general each evaluation is a numerical integral. Section 4 of the paper shows that when demand is normal, $P^L$ has a closed form in the univariate and bivariate standard normal distribution functions. This mission formalizes that closed form, eq. (13) on p. 830.

Setting

Time is discrete. One-period demand is $u\sim N(\mu,\sigma^2)$ with $\sigma>0$, independent across periods. For $i\ge1$, $u^{(i)}$ is the total demand over $i$ periods. It is normal with mean $\mu^{(i)}=i\mu$ and standard deviation $\sigma^{(i)}=i^{1/2}\sigma$, density $f^{(i)}$ and cdf $F^{(i)}$. The shipment lead time from depot to outlet is $l\ge0$ and the order lead time from the supplier is $L\ge1$. The cost factors are a system-wide holding cost $h^d>0$, a retailer holding cost $h^r>0$ and a retailer shortage penalty $p^r>0$. Write $p^s=h^d+p^r$. Costs are average costs, so the discount factor is $\alpha=1$ throughout.

The retailer's one-period cost (p. 822) is

$$R(x)=-h^d(x-\mu^{(l)})+p^rE[u^{(l+1)}-x]^++(h^d+h^r)E[x-u^{(l+1)}]^+ .$$

The critical number $x^{r*}$ is a global minimizer of $R$ (property (b), p. 824). The induced penalty cost is $P(x)=0$ for $x\ge x^{r*}$ and $P(x)=R(x)-R(x^{r*})$ for $x<x^{r*}$. Its expectation over the order lead time is

$$P^L(x)=E\,P[x-u^{(L)}]\qquad\text{(eq. (10))}.$$

Let $\Phi$ and $\phi$ be the standard normal cdf and density, $\Theta(z)=z\Phi(z)+\phi(z)$, and $\Phi(\xi_1,\xi_2;\rho)$ the cdf of a bivariate normal pair with standard normal marginals and correlation $\rho$. The paper defines (p. 830)

$$\tau_1(x)=-\frac{x-(x^{r*}+\mu^{(L)})}{\sigma^{(L)}},\quad \tau_2(x)=\frac{x-\mu^{(L+l+1)}}{\sigma^{(L+l+1)}},\quad \nu^{r*}=\frac{x^{r*}-\mu^{(l+1)}}{\sigma^{(l+1)}},$$ $$\tau_3(x)=-\frac{x-(x^{r*}+\mu^{(L)})-[\sigma^{(L)}/\sigma^{(l+1)}]^2[x^{r*}-\mu^{(l+1)}]}{\sigma^{(L)}\sigma^{(L+l+1)}/\sigma^{(l+1)}},$$ $$\epsilon_1(x)=\frac{\Phi[\tau_3(x)]\phi[\tau_2(x)]}{\sigma^{(L+l+1)}},\qquad \epsilon_2(x)=\frac{\Phi(\nu^{r*})\phi[\tau_1(x)]}{\sigma^{(L)}},\qquad \iota(x)=\sigma^{(L)}\Theta[\tau_1(x)],$$ $$\kappa(x)=\sigma^{(l+1)}\Theta(\nu^{r*})\Phi[\tau_1(x)]-\{[\sigma^{(L+l+1)}]^2\epsilon_1(x)-[\sigma^{(L)}]^2\epsilon_2(x)\}-[x-\mu^{(L+l+1)}]\,\Phi[\tau_1(x),\tau_2(x);\rho],$$

with $\rho=-\sigma^{(L)}/\sigma^{(L+l+1)}$.

Formalization targets

Goal: eq. (13)

For every real $x$,

$$P^L(x)=p^s\,\iota(x)-(p^s+h^r)\,\kappa(x).$$

This is an exact identity for every admissible parameter value. It holds with no constants left free.

Milestones

The milestones follow the paper's outline of the derivation on pp. 829–831:

1. eq. (11), $R(x)=p^s[\mu^{(l+1)}-x]+(p^s+h^r)\int_{-\infty}^xF^{(l+1)}(t)\,dt-h^d\mu$;
2. eq. (12), $P^L(x)=\int_{x-x^{r*}}^\infty[R(x-t)-R(x^{r*})]f^{(L)}(t)\,dt$;
3. eq. (14), $P^{L\prime}(x)=-p^s\Phi[\tau_1(x)]+(p^s+h^r)\int_{x-x^{r*}}^\infty F^{(l+1)}(x-t)f^{(L)}(t)\,dt$;
4. eq. (15), the same derivative with the integral replaced by $\Phi[\tau_1(x),\tau_2(x);\rho]$;
5. $P^L(x)\to0$ as $x\to\infty$, hence $P^L(x)=-\int_x^\infty P^{L\prime}(t)\,dt$;
6. $\iota'(x)=-\Phi[\tau_1(x)]$ and $\iota(x)\to0$;
7. the two conditional-normal identities, which give $\Phi[\tau_3(x)]$ and $\Phi(\nu^{r*})$;
8. $\frac{d}{dx}\Phi[\tau_1(x),\tau_2(x);\rho]=\epsilon_1(x)-\epsilon_2(x)$;
9. and 10. the formulas for $\epsilon_1'$ and $\epsilon_2'$;
10. $\kappa'(x)=-\Phi[\tau_1(x),\tau_2(x);\rho]$ and $\kappa(x)\to0$.

Two side remarks of p. 830 are also included: $\Theta'=\Phi$, and the simplified form of $\tau_3$.

Significance

The result. Under normal demand, (13) replaces the numerical integral (12) with a few evaluations of $\Phi$, $\phi$ and the bivariate normal cdf, all available in standard numerical libraries. Together with the decomposition results of Sections 1–3 of the paper, it makes the policy computation for the two-echelon system with normal demand no harder than a single-location computation with an explicit cost function. The same functions reappear in the paper's Section 5 for several retail outlets, after a reinterpretation of $\sigma^{(l+1)}$.

Formalizing it. The paper proves (13) only in outline: it calls the derivation "an elementary integration problem, but … sufficiently involved to warrant an outline" and leaves "tedious algebra" and "more algebra" to the reader. A machine-checked proof turns that outline into a complete argument, including the analytic steps the outline passes over: differentiation under the integral sign, the limits at $+\infty$, and the identification of an integral of normal densities with a bivariate normal probability. To our knowledge no formal proof of (13) exists, and no bivariate normal distribution function is on the platform yet.

Difficulty

The obvious approach is to substitute (11) into (12) and integrate. The result is a double integral of normal densities over a region bounded by a line, and it does not reduce to univariate functions. The paper's route is to differentiate first, identify the derivative (14) as a probability for the correlated pair $(u^{(L)},u^{(L)}+u^{(l+1)})$, and then recover $P^L$ by integrating from $+\infty$. That route needs three things: justification for differentiating under the integral in (12), whose integrand has a kink at $t=x-x^{r*}$; control of the limits at $+\infty$; and the conditional-normal identities, which involve conditioning on a null event and so must be handled through densities. The verification of $\kappa'$ is a long computation with $\Theta$, $\epsilon_1$ and $\epsilon_2$, in which every constant matters.

Formalization scope

Everything lives in the namespace FZEchelon.NormalDemand. The model data form the structure Data (fields $\mu,\sigma,h^d,h^r,p^r,l,L,x^{r*}$). The law of $u^{(i)}$ is the platform's normal demand law InventoryControl.newsboyDemand with mean $i\mu$ and standard deviation $\sqrt i\,\sigma$. Expectations are Bochner integrals, and improper integrals are set integrals over Set.Ioi/Set.Iic. $\Phi$ is cdf (gaussianReal 0 1). The bivariate cdf is the iterated integral of the explicit bivariate density over a lower-left quadrant (meaningful for $|\rho|<1$; here $\rho\in(-1,0)$). Derivatives are HasDerivAt and limits are Tendsto … atTop (𝓝 0).

Standing hypotheses of every theorem: $\sigma>0$; $h^d,h^r,p^r>0$ (p. 821); $L\ge1$; and $x^{r*}$ minimizes $R$. Two of these are added to the page and disclosed. $\sigma>0$ is needed because every $\tau$ divides by some $\sigma^{(i)}$. $L\ge1$ is needed because $\sigma^{(0)}=0$, and the paper treats zero order lead time separately (p. 819). Demand is exactly normal, as in §4, which acknowledges that this violates $u\ge0$ and ignores the objection. No nonnegativity, truncation or approximation enters. The goal fixes $\alpha=1$, the average-cost case the section restricts to. The discounted analogue is not part of this mission.

A trivializing formalization is ruled out: every Bochner integral in the statements has an integrable integrand, since integrands grow at most linearly and the normal law has all moments. No division by a zero standard deviation can occur under the hypotheses. A sorry-free check in the workspace shows that all hypotheses hold together, with a minimizer $x^{r*}$ of $R$ proved to exist.

Needed infrastructure: properties of gaussianReal (moments, convolution of independent normals), differentiation of parametric integrals, and a bivariate normal distribution function with its partial derivatives. A reusable treatment of the bivariate normal cdf, linking the density form used here to Mathlib's multivariateGaussian, would be a contribution of independent value. Proofs of individual milestones are welcome in any order.

Selected references

• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525

Motivation

Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.

Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).

Timeline:

• 1960: Clark and Scarf, finite-horizon decomposition, with a nonstationary penalty $\hat P_n$ built from the outlet's optimal cost functions.
• 1963: Iglehart (Management Science 9) proved, for the single-location discounted problem, that the finite-horizon value functions converge uniformly and that an $(s,S)$ policy is optimal.
• 1984: Federgruen and Zipkin combine the two results and prove that a stationary policy built from the decomposition is optimal for the infinite-horizon discounted and average-cost problems.

Setting

Time is discrete. The cost data are a fixed order cost $K$, an order cost rate $c^d$, a shipment cost rate $c^r$, a holding cost rate $h^d$ on all system stock, an extra holding cost rate $h^r$ at the outlet, and a backorder penalty rate $p^r$; all are positive. The discount factor $\alpha$ satisfies $0 \le \alpha < 1$, shipments take $l$ periods and orders take $L$ periods. One-period demands are independent copies of a nonnegative continuous random variable $u$ with mean $\mu < \infty$, and $u^{(i)}$ denotes the sum of $i$ copies.

The state is $(\hat y, v^d, x^r)$:

• $\hat y = (y^1, \dots, y^L)$ lists the outstanding orders, $y^i$ placed $i$ periods ago;
• $v^d$ is the depot's echelon inventory (its own stock plus $x^r$);
• $x^r$ is the outlet's stock plus shipments in transit.

An action is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$. With demand $u$, the next state is $((y, y^1, \dots, y^{L-1}), v^d + y^L - u, x^r + z - u)$. The one-period cost is

$$c^d(y) + h^d(v^d + y^L) + c^r z + R(x^r + z),$$

where $c^d(y) = K + c^d y$ for $y > 0$, $c^d(0) = 0$, and

$$R(x) = \alpha^l\{-h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r)E[x - u^{(l+1)}]^+\}.$$

$B^\alpha(s \mid \pi)$ is the expected total discounted cost of a policy $\pi$ from state $s$.

The critical number $x^{r*}$ minimizes $(1-\alpha)c^r x + R(x)$. The stationary induced penalty is $P(x) = 0$ for $x \ge x^{r*}$ and $P(x) = (1-\alpha)c^r(x - x^{r*}) + R(x) - R(x^{r*})$ otherwise. The depot problem $IH^d_\alpha$ has state $(\hat y, v^d)$, action $y \ge 0$ and one-period cost $c^d(y) + h^d(v^d + y^L) + P(v^d + y^L)$. The policy $\pi_\alpha^*$ orders by an optimal stationary policy $\sigma^d$ of $IH^d_\alpha$ and ships $z = \max\{0, \min\{x^{r*}, v^d + y^L\} - x^r\}$: up to the critical number when the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 1 (p. 827)

Assume $\alpha^l p^r \ge (1-\alpha^l)h^d$. For every state with $\hat y \ge 0$ and $x^r \le v^d$, and every admissible policy $\pi$,

$$B^\alpha(\hat y, v^d, x^r \mid \pi_\alpha^*) \le B^\alpha(\hat y, v^d, x^r \mid \pi).$$

The goal leaves the form of $\sigma^d$ open: any optimal stationary depot policy will do, and no $(s,S)$ structure is assumed.

Milestones

The milestones follow the paper's own route. Write $\hat g_n$, $g_n^r$, $\hat g_n^d$, $g_n^d$ for the $n$-period optimal costs of the system, of the outlet, of the depot with penalties $\hat P_n$, and of the depot with penalty $P$.

• Eq. (4): $\hat g_n = \hat g_n^d + g_n^r$.
• Property (e): $g_n^r \to g^r = B^{r\alpha}$.
• §2 claim (Iglehart): $g_n^r \to g^r$ uniformly on $(-\infty, x^{r*}]$.
• Lemma 1: $\hat P_n \to P$ uniformly on $\mathbb R$.
• Lemma 2: $\hat g_n^d - g_n^d \to 0$ uniformly.
• Lemma 3: $\hat g_n \to g^d + g^r$.
• Lemma 4: $g$ satisfies the optimality equation (8), and $\pi_\alpha^*$ attains it.

Significance

The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty $P$ that is written in terms of $R$ alone. Computing $P$ does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate $P$ in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.

The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.

Difficulty

The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties $\hat P_n$, built from the outlet's optimal costs $g_{n-1}^r$, and its value functions are not those of any stationary problem. The comparison of $\hat P_n$ with $P$ needs uniform control over the whole real line. The first few $\hat P_n - P$ are in fact unbounded, since $g_0^r = 0$ has the wrong slope. The uniform control therefore holds only for large $n$, and the error has to be propagated through the depot recursion.

The second obstacle is that the one-period costs are unbounded in both directions: $h^d v$ is negative for negative $v$. Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation $\alpha^l p^r \ge (1-\alpha^l)h^d$, and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.

Formalization scope

Everything lives in the namespace FZEchelon.Discounted.

• Model. The data form a structure Model. The pipeline $\hat y$ is a vector indexed by $\{0, \dots, L-1\}$, whose index $k$ is the paper's $y^{k+1}$. For $L = 0$ the current order arrives at once.
• Policies and cost. Time runs forward with weight $\alpha^k$; the paper counts periods remaining. Policies are measurable, non-anticipative, deterministic and history dependent, and they must be feasible along every demand path. $B^\alpha$ is an extended real: the expectation of the positive part of the discounted cost sum minus that of the negative part, under the product law of the demands.
• Finite-horizon programs. These are real infima over the feasible actions.
• Hypotheses. Statements quantify over the physical states $\hat y \ge 0$, $x^r \le v^d$. The standing assumptions of §1 are bundled in StandingAssumptions: positive costs, $0 \le \alpha \le 1$, demand nonnegative, atomless and of finite mean. The §2 statements add $\alpha < 1$ and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers $x^{r*}$ and $x_n^{r*}$ enter as minimizers. The depot policy $\sigma^d$ enters as a measurable, nonnegative stationary policy that is optimal for $IH_\alpha^d$; that is the paper's definition of $\pi_\alpha^*$, and its existence is Iglehart's.
• Ruled out. Comparing $\pi_\alpha^*$ only against stationary policies, or reading $B^\alpha$ as a bare series or a truncated sum, would trivialize or change the theorem. The comparison class is all admissible history-dependent policies.
• Corrections. Where the paper says "bounded" for every $n$ (§2 claim, Lemmas 1 and 2), the statements claim boundedness only where it holds: $n \ge 1$, $n \ge 2$, and eventually, respectively. The moderation notes give the counterexample at $n = 1$. Lemma 2 also carries the standing assumption of p. 821 that never ordering is not optimal. The statement is false without it.
• Infrastructure. A complete development needs the convexity theory of the single-location newsvendor function $R$, value iteration for discounted models with costs bounded below, and the Markov property for the product measure on demand sequences. The control-system file is reusable for other inventory and queueing missions. Formalizations of Iglehart's theorem and of Bertsekas–Shreve Propositions 9.12 and 9.16 are welcome.

Selected references

• A. Federgruen, P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark, H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

Classical inventory theory chooses order quantities against a probability distribution of demand. The resulting dynamic programs are optimal in expectation but need the distribution, and they become intractable once several installations, capacities or fixed costs interact. Robust optimization replaces the distribution by an uncertainty set and asks for the order sequence whose worst-case cost over that set is smallest. Bertsimas and Thiele (Operations Research 54(1), 2006) applied the budget-of-uncertainty approach of Bertsimas and Sim (The Price of Robustness, Operations Research 52(1), 2004) to finite-horizon inventory control. Their main structural result says that robustness does not destroy the structure of the classical problem. The robust problem is a deterministic (nominal) inventory problem with an explicitly modified demand, and the price of robustness is an explicit constant.

Setting

A single item is ordered at a single installation over periods $k = 0, \dots, T-1$. The stock at the beginning of the horizon is $x_0$. Orders $u_k \ge 0$ arrive immediately, demand $w_k$ is subtracted, and excess demand is backlogged, so the stock at the end of period $k$ is

$$x_{k+1} = x_0 + \sum_{i=0}^{k} (u_i - w_i).$$

The demand of period $k$ is uncertain: $w_k = \bar w_k + \hat w_k z_k$ with a nominal demand $\bar w_k$, a maximal deviation $\hat w_k \ge 0$ and a scaled deviation $z_k \in [-1, 1]$. A budget of uncertainty $\Gamma_k$ limits the total scaled deviation up to period $k$. The budgets satisfy $0 \le \Gamma_0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

Each period costs $C(u_k) + R(x_{k+1})$. The purchasing cost is $C(u) = K + cu$ for $u > 0$ and $C(0) = 0$, with $c > 0$ and $K \ge 0$. The holding/shortage cost is $R(x) = \max(hx, -px)$, with $h \ge 0$ and $p > c$. The nominal problem with demand $w$ minimizes $\sum_{k<T} (C(u_k) + R(x_{k+1}))$ over $u \ge 0$ for a fixed demand sequence $w$.

For each $k$, $A_k$ is the optimal value of the linear program

$$A_k = \max\Big\{\sum_{i=0}^{k} \hat w_i z_i \;:\; \sum_{i=0}^{k} z_i \le \Gamma_k,\ 0 \le z_i \le 1\Big\} \qquad (13)$$

It is the worst-case deviation of the cumulative demand up to $k$ from its nominal value, with $A_{-1} = 0$. Write $\bar x_{k+1} = x_0 + \sum_{i\le k}(u_i - \bar w_i)$ for the nominal stock. The robust formulation (14) minimizes $\sum_{k<T} (C(u_k) + y_k)$ over $(u, y, q, r)$ subject to the following constraints for every $k < T$:

• $u_k \ge 0$, $q_k \ge 0$, and $r_{ik} \ge 0$, $q_k + r_{ik} \ge \hat w_i$ for $i \le k$;
• $y_k \ge h(\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$;
• $y_k \ge p(-\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$.

The variables $q, r$ are the dual of (13). Formulation (14) is equivalent to requiring the holding and shortage constraints of period $k$ for every demand whose scaled deviations satisfy $|z_i| \le 1$ and $\sum_{i \le k}|z_i| \le \Gamma_k$.

Formalization targets

Goal: Theorem 3.2 (a), (b), (d)

Let the modified demand be

$$w'_k = \bar w_k + \frac{p-h}{p+h}\,(A_k - A_{k-1}). \qquad (20)$$

Write $N_{w'}(u)$ for the nominal cost of $u$ under demand $w'$. Then:

1. For every $u \ge 0$, the minimum of the objective of (14) over the feasible $(y, q, r)$ is attained and equals

$$N_{w'}(u) + \frac{2ph}{p+h}\sum_{k=0}^{T-1} A_k.$$

2. $u$ is the order part of an optimal solution of (14) if and only if $u$ is optimal for the nominal problem with demand $w'$.
3. The optimal cost of (14) is the optimal nominal cost under $w'$ plus $\frac{2ph}{p+h}\sum_k A_k$.
4. If $K = 0$ and $w'_k \ge 0$, the order-up-to policy with levels $S_k = w'_k$ is robust-optimal.

Milestones

The milestones are the steps of the paper's proof, in order:

• LP (13) and its dual are attained with the common value $A_k$.
• The constraints of (14) are the robust counterpart of the $k$-th holding/shortage pair (10)–(11).
• For fixed orders, the value of (14) is the sum (21).
• The modified stock (22) satisfies $x'_{k+1} = \bar x_{k+1} - \frac{p-h}{p+h}A_k$.
• The max identity (23): $\max(h(\bar x+A), p(-\bar x+A)) = \max(hx', -px') + \frac{2ph}{p+h}A$.
• Lemma 3.1(b): for nonnegative demand, the nominal problem without fixed cost is solved by ordering up to $S_k = w_k$.
• Remark 1: $A_{k-1} \le A_k$, so $w'_k \ge \bar w_k$ when $p \ge h$.
• Remark 3: under i.i.d. demand, $A_k = \hat w\Gamma_k$, which gives the closed-form thresholds.

Significance

The theorem reduces robust inventory control to nominal inventory control. Every structural fact known for the deterministic problem then transfers to the robust one. These include the optimality of base-stock policies without fixed cost and the threshold structure with a fixed cost. The robust base-stock levels are explicit: they shift the nominal levels by $\frac{p-h}{p+h}(A_k - A_{k-1})$, upward when shortage is more expensive than holding. The extra cost $\frac{2ph}{p+h}\sum_k A_k$ quantifies the price of protection as a function of the budgets. The paper uses the same reduction for capacitated orders (Theorem 3.3) and for supply networks (§4).

The result has been proved since 2006, and no machine-checked proof of it, or of any budgeted robust counterpart, is known to exist. This mission provides several formalizations for reuse:

• the budgeted robust counterpart of a pair of piecewise-linear constraints;
• the duality of the fractional knapsack LP (13);
• the optimality of base-stock orders for a deterministic backlogged inventory problem.

Difficulty

The algebraic core, identity (23), is elementary. The work is in the reductions around it. The first is that (14) really is the worst case of (10)–(11): this needs strong duality for (13), together with attainment on both sides, and the observation that the minimizing and maximizing deviations of a constraint pair differ. The second is that the minimum of (14) over the auxiliary variables, for fixed orders, is (21). This requires the dual optimum to be attained with the value of (13), and $h, p \ge 0$ so that the cost is monotone in $A_k$. The third is the base-stock part, which needs Lemma 3.1(b), a global optimality statement for a $T$-period problem with backlogging. The paper proves that lemma by an explicit dual certificate. An argument through first-order conditions in each period is not enough, because orders in one period affect every later stock level.

Formalization scope

All data are real numbers and sequences are ℕ → ℝ; only indices $k < T$ matter. stock w u k denotes $x_{k+1}$, the stock at the end of period $k$. The standing assumptions of §3.1 are fields of the model:

• $c > 0$, $K \ge 0$, $h \ge 0$, $p > c$;
• $\hat w_k \ge 0$;
• $\Gamma_0 \ge 0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

The conventions and corrections are:

• Fixed cost. The paper writes it with binary variables and a big-$M$ constraint. Here it is the indicator $C(u_k)$ in the objective, as in the paper's own (21).
• "Optimal". It always means minimality over all feasible points.
• The policy. It is the order sequence chosen at time 0.
• $A_k$. It is the value of (13), as in Remark 1 after the theorem, not "the optimal $q^*, r^*$ of (14)", which need not be unique.
• The robust formulation. (14) is formalized as printed: the $k$-th constraint pair is protected by the budget $\Gamma_k$ alone, not by the intersection of all budgets up to $k$.
• Sign slip. The page's $x_{k+1} = \bar x_{k+1} + \sum \hat w_i z_i$ is a sign slip for $\bar x_{k+1} - \sum \hat w_i z_i$. The formal statements use the correct sign; the result is unaffected because the deviation set is symmetric.
• Part (b). It is stated under $w'_k \ge 0$. As printed it fails when $p < h$ makes $w'$ negative, for example $T = 2$, $\bar w = \hat w = (10, 0)$, $\Gamma = (0, 1)$, $c = 1$, $h = 4$, $p = 2$, $x_0 = 0$. Lemma 3.1(b) carries the matching hypothesis of nonnegative demand.
• Remark 3. It adds $\Gamma_0 \le 1$.
• Remark 1. Its inequalities are weak.
• Not stated. The (s, S) clause of (a) and part (c) are excluded. They rest on a stochastic theorem cited from Bertsekas (1995) and on thresholds stated through the optimal ordering times.

A trivializing formalization is ruled out: the robust cost is formulation (14) with its variables $y, q, r$, and $A_k$ is the value of LP (13). Neither is the closed-form objective (21) nor an arbitrary sequence. Contributions are welcome on the LP duality of (13) (a fractional knapsack), on the robust counterpart milestone, and on Lemma 3.1(b), each of which is independent of the others.

Selected references

• D. Bertsimas, A. Thiele, A Robust Optimization Approach to Inventory Theory, Operations Research 54(1):150–168, 2006. https://doi.org/10.1287/opre.1050.0238
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. 1, Athena Scientific, 1995.