Inventory and Supply Chain

Motivation

A base-stock (order-up-to) policy orders, in every period, exactly enough to bring the inventory position (stock on hand plus stock on order minus backorders) up to a target level. It is the policy used in practice for repairable and consumable service parts, and the analysis of every later chapter of Muckstadt's book assumes it. Its optimality is therefore a foundational question, and there are three classical ways to prove it.

• 1960, Clark and Scarf proved optimality of echelon base-stock policies for finite-horizon serial systems by dynamic programming, decomposing the cost into one term per echelon (Management Science 6(4)).
• 1984, Federgruen and Zipkin gave a lower-bound argument for the infinite-horizon average-cost case (Operations Research 32(4)); Chen and Song (2001) used it for Markov-modulated demand (Operations Research 49(2)).
• 2008, Muharremoglu and Tsitsiklis introduced the single-unit single-customer approach: every unit of stock is paired with one future customer, and the inventory problem splits into countably many independent two-action problems (Operations Research 56(5)).

This mission formalizes the third approach, in the finite-horizon single-location form presented in Section 2.2.1 of Muckstadt (2005).

Setting

A single item is reviewed in periods $n = 1, \dots, N$. An exogenous, time-homogeneous Markov chain $s_n$ on a finite set $\Sigma$ is observed at the start of period $n$; given $s_n = s$, the demand $D_n \in \{0,1,2,\dots\}$ has law $\kappa(s,\cdot)$ and is independent of $s_{n+1}$. Excess demand is backordered.

Every unit of demand is a customer, and customers are indexed in arrival order, the $v_0$ initially waiting customers first. A customer's distance is $0$ once served, $1$ while waiting, and $2, 3, \dots$ for future customers in the order they will arrive. Units are indexed by location: $0$ (used), $1$ (on hand), $2, \dots, m$ (in transit) and $m+1$ (at the supplier, which holds countably many units). The state is

$$x_n = \big(s_n, (z_{1n}, y_{1n}), (z_{2n}, y_{2n}), \dots\big),$$

with $z_{jn}$ the location of unit $j$ and $y_{jn}$ the distance of customer $j$. In period $n$: units in transit move one location closer and the released units move from $m+1$ to $m$ (so an order is on hand $m-1$ periods later); the demand $D_n$ brings the customers at distances $2, \dots, D_n+1$ to distance $1$ and moves the others $D_n$ steps closer; units on hand serve waiting customers, lowest indices first; then $h$ is charged per unit on hand and $b$ per waiting customer, with $0 < h < b$. The criterion is the expected cost over the $N$ periods, discounted by $\alpha \in (0,1]$.

A policy for the whole system $\mathcal S$ chooses a finite set of units at the supplier to release. It is monotone if it releases lower-indexed units first, and committed if unit $j$ only ever serves customer $j$. The subsystem $\mathcal S_w$ is unit $w$ with customer $w$ under commitment, with state $x^w_n = (s_n, z_{wn}, y_{wn})$ and actions Release and Hold. The set $R^*_n(s,y)$ contains the optimal actions of a subsystem whose unit is at the supplier and whose customer is at distance $y$, and the critical distance is

$$y^*(n,s) = \max\{\, y : R^*_n(s,y) \ni \mathit{Release} \,\}.$$

Formalization targets

Goal: Theorem 5 (p. 29)

Every policy that, in each period $n$ and Markov state $s_n$, releases the lowest-indexed units at the supplier to raise the inventory position to

$$y^*(n, s_n) - 1$$

is optimal for $\mathcal S$ among all policies, from every starting state. Such a policy exists. The levels are not fixed numbers but the critical distances of the single-unit problem, so the goal asserts the structure of an optimal policy and identifies its levels, without committing to any constant.

Milestones

1. Lemma 1 (p. 26): some monotone policy is optimal, every monotone policy is committed, and so some committed policy is optimal.
2. Theorem 4 (p. 27): the optimal cost of $\mathcal S$ is the sum over $w$ of the optimal costs of $\mathcal S_w$,

$$V^{\mathcal S}_1(s, x_1) = \sum_{w} V_1\big(s, (z_{w1}, y_{w1})\big),$$

and managing every subsystem independently and optimally is optimal for $\mathcal S$. 3. Lemma 2 (p. 28): $R^*_n(s, y+1) = \{\mathit{Release}\}$ implies $\mathit{Release} \in R^*_n(s, y)$. 4. Section 2.2.1.2.2 (p. 29): the critical distance policy, release if and only if $y \le y^*(n,s)$, is optimal for every subsystem.

Significance

The result shows that under Markov-modulated demand a single-location system is optimally run by a state-dependent base-stock policy. The same unit–customer argument gives echelon base-stock optimality in serial systems with noncrossing stochastic lead times (Sections 2.2.2–2.2.3). The decomposition also yields the levels themselves: they are the critical distances of a two-action problem, which can be solved one customer at a time.

The theorems are proved in the literature (Muharremoglu and Tsitsiklis 2008) and in the book. To our knowledge no machine-checked proof of any base-stock optimality theorem exists, by dynamic programming or by decomposition. The book's proof is informal in three places a formalization has to settle:

• Lemma 1 is asserted as "clearly" true;
• Lemma 2's proof by contradiction covers only uniquely optimal releases, while the critical distance policy also needs the case of ties;
• the passage from the subsystem policy to the inventory position (Theorem 5) is an "intuitive argument".

A formal development makes each of these precise.

Difficulty

The obvious argument says that costs are linear, so the cost of $\mathcal S$ is the sum of unit–customer costs and everything decouples. That is only half of Theorem 4. The pairing of unit $j$ with customer $j$ holds only under monotone policies, and a general policy for $\mathcal S$ observes the whole infinite state $x_n$, not just $x^w_n$. The lower bound therefore needs Lemma 1 together with the fact that extra information about the demand history does not help a Markov decision problem. The upper bound needs the lowest-index matching to cost no more than committed matching.

The second difficulty is that the threshold structure is not the obvious consequence of Lemma 2. The set of distances at which releasing is optimal must be shown to be an initial segment $\{1, \dots, y^*\}$ when ties are allowed. Unbounded demand makes that set possibly unbounded (it is, in the last $m-1$ periods). Finally, the release decisions of the subsystems must be counted to recover an inventory position, which uses the invariant that future customers occupy consecutive distances.

Formalization scope

Everything is in the namespace ServiceParts.UnitDecomp, with three definition files.

Model. Model bundles the chain, the demand law, $m$, $h$, $b$ and $\alpha$ with the standing assumptions $1 \le m$, $0 < h < b$, $0 < \alpha \le 1$, together with the per-unit and per-customer motions and a generic finite-horizon expected-cost recursion. Costs are in $[0,\infty]$.

Subsystem. Subsystem defines a subsystem, its optimal cost, $R^*_n$, $y^*(n,s)$ and the critical distance policy.

System. System defines $\mathcal S$ with lowest-index matching, its policies (finite release sets), monotone and committed policies, starting states, the inventory position and the order-up-to release.

Conventions and pinnings:

• Indexing. Units and customers are indexed from $0$; Lean index $j$ is the book's $j+1$.
• Policy class. Policies are Markov: functions of the period, the Markov state and the configuration, as on p. 25.
• Optimality. Optimal means attaining the infimum over all policies for $\mathcal S$. Restricting the class to monotone or base-stock policies would make Theorem 5 circular and is ruled out.
• Starting states. The book's "any starting state $x_1$" is the configuration built on pp. 23–24 from $v_0$ and the stock at locations $1, \dots, m$. For arbitrarily labelled states Theorem 4 is false.
• Critical distance. $y^*(n,s)$ is a supremum in $\mathbb N \cup \{\infty\}$. Where it is $\infty$ (a released unit cannot arrive before the horizon), Theorem 5 leaves the policy free.
• Distance 0. Lemma 2 and the optimality of $R_n$ are stated for customers at distance at least 1. At distance 0 with the unit at the supplier (a configuration committed policies never reach), both are false as printed.

Corrections to the book:

• $h > 0$ is added. With $h = 0$ an optimal policy with finite orders need not exist, so Theorem 5 fails.
• Chain structure is pinned. The chain's ergodicity is unused on a finite horizon and omitted. The conditional independence of $D_n$ and $s_{n+1}$ given $s_n$ is added as a reading of "given $s_n$, the distribution of $D_n$ is known".
• Vacuous corner. If some state's demand has infinite mean, every policy may cost $\infty$ and the optimality statements hold vacuously.

Out of scope: stochastic noncrossing lead times (Section 2.2.2), serial systems (Section 2.2.3; compare the disproved platform statement SupplyChainTheory.clark_scarf_sequential), and continuous review (Section 2.2.4, which the book calls intuitive).

Proofs of any milestone are welcome. A reusable by-product would be a general lemma that Markov policies are optimal among history-dependent ones for finite-horizon problems with countable randomness and costs in $[0,\infty]$.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Section 2.2, pp. 22–31. https://doi.org/10.1007/b138879
• A. Muharremoglu and J. N. Tsitsiklis, A single-unit decomposition approach to multiechelon inventory systems, Operations Research 56(5), 2008. https://doi.org/10.1287/opre.1080.0620
• A. J. Clark and H. Scarf, Optimal policies for a multi-echelon inventory problem, Management Science 6(4), 1960. https://doi.org/10.1287/mnsc.6.4.475
• A. Federgruen and P. Zipkin, Computational issues in an infinite-horizon, multiechelon inventory model, Operations Research 32(4), 1984. https://doi.org/10.1287/opre.32.4.818
• F. Chen and J.-S. Song, Optimal policies for multiechelon inventory problems with Markov-modulated demand, Operations Research 49(2), 2001. https://doi.org/10.1287/opre.49.2.226.13528

Motivation

Service parts (spare engines, avionics modules, repairable components) are usually managed one unit at a time: whenever a customer order removes a unit from stock, a replacement is ordered at once, from a repair shop or an outside supplier. This is the (s–1, s) policy, under which the inventory position (on hand plus on order minus backorders) stays constant at the stock level $s$. Every performance measure of such a system (fill rate, expected backorders, availability) is a function of one random variable: the number of units in resupply, i.e. ordered but not yet returned. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005) computes its distribution, and the rest of the book (the METRIC-type multi-echelon models of Chapters 4 and 5, the stock-level optimization of Section 3.4) is built on that computation.

Timeline. C. Palm (1938) showed, in the setting of telephone traffic, that in an infinite-server system with Poisson arrivals the number of busy servers has, in steady state, a Poisson law whose mean is the arrival rate times the mean service time, whatever the service-time distribution. Feeney and Sherbrooke (1966) carried the result to (s–1, s) inventory systems with compound Poisson demand, and treated the lost-sales case. Sherbrooke's METRIC model (1968) made the Poisson law of units in resupply the basis of multi-echelon spare-parts planning.

Setting

A single item is stocked at one location. Customer orders arrive at epochs $T_0 < T_1 < \cdots$ of a Poisson process with rate $\lambda > 0$, started empty at time $0$: the interarrival times $A_k$ are independent and exponential with rate $\lambda$, and $T_k = A_0 + \cdots + A_k$. The $k$-th order triggers a resupply order with resupply time $L_k \ge 0$. The resupply times are independent and identically distributed, independent of the arrival process, with a density $g$, distribution function $G(u) = P[L \le u]$ and finite mean

$$\bar\tau = E[L] = \int_0^\infty [1 - G(u)]\,du .$$

With backorders allowed, the number of units in resupply at time $t$ is

$$X(t) = \#\{k : T_k \le t < T_k + L_k\},$$

and $N(t) = \#\{k : T_k \le t\}$ counts the orders placed in $[0,t]$. On-hand stock and backorders at time $t$ are $(s - X(t))^+$ and $(X(t) - s)^+$.

In the compound Poisson version the $k$-th order asks for $X_k \ge 1$ units, the sizes are i.i.d. with $u_j = P[X_k = j]$, independent of arrivals and resupply times, and all units of one order share its resupply time $L_k$. The units in resupply are $Y(t) = \sum_{k : T_k \le t < T_k + L_k} X_k$. Writing $u^{(y)}_n$ for the probability that $y$ orders ask for $n$ units in total, the compound Poisson probabilities with parameter $\mu$ are

$$p(n \mid \mu) = \sum_{y=0}^{n} \frac{\mu^y e^{-\mu}}{y!}\,u^{(y)}_n .$$

In the lost-sales version an order that finds no stock on hand is lost, so at most $s$ units are ever in resupply.

Formalization targets

Goal: Palm's theorem (Theorem 6, p. 39)

For every $x \ge 0$,

$$\lim_{t\to\infty} P[X(t) = x] = e^{-\lambda\bar\tau}\frac{(\lambda\bar\tau)^x}{x!}.$$

The resupply-time law enters only through its mean. This is the statement the book's proof establishes and every later chapter uses.

The proof's milestones (pp. 38–41)

1. Eq. (3.5): $P[N(t) = n] = e^{-\lambda t}(\lambda t)^n/n!$.
2. Eq. (3.3): given $N(t) = n$, the epochs $(T_0, \dots, T_{n-1})$ have density $n!/t^n$ on $0 < t_1 < \cdots < t_n < t$.
3. Eq. (3.7): given $N(t) = n$, $X(t)$ is binomial with parameters $n$ and $p = \frac1t\int_0^t[1-G(u)]\,du$.
4. Eq. (3.8): for every $t > 0$, $X(t)$ is Poisson with mean $\lambda\int_0^t[1-G(u)]\,du$.
5. Eq. (3.10): $\int_0^t[1-G(u)]\,du \to \bar\tau$.

Extensions in Section 3.1

6. Theorem 7 (pp. 43–44): with compound Poisson demand, $\lim_{t\to\infty}P[Y(t) = n] = p(n \mid \lambda\bar\tau)$.
7. Theorem 8 (p. 44): in the lost-sales system with exponential resupply times of rate $\beta$, the probability vectors solving the balance equations are exactly the truncated Poisson law $\pi_x \propto (\lambda/\beta)^x/x!$, $0 \le x \le s$.
8. Theorem 9 (pp. 46–47): for a due-date delay $T \ge 0$, the units in resupply that have been there for at least $T$ satisfy $\lim_{t\to\infty}P[Y_T(t) = n] = p(n \mid \lambda\bar\tau\alpha)$ with $\alpha = \frac1{\bar\tau}\int_T^\infty[1-G(t)]\,dt$.

Significance

The result. Palm's theorem turns an infinite-dimensional object (the whole resupply-time distribution) into one number, $\bar\tau$. This insensitivity is what makes spare-parts planning computable: the expected backorders at stock level $s$ are $\sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$, the fill rate is $P[X \le s - 1]$, and both can be optimized over $s$ with only the demand rate and mean repair time as data. Theorem 7 extends this to batch demand, Theorem 9 to systems allowed a response time, and Theorem 8 gives the exact law when shortages are lost instead of backordered.

Formalizing it. All of these results are classical and proved. None of them is formalized on the platform, and Mathlib has Poisson and exponential distributions but no Poisson process, no thinning theorem and no infinite-server queue. The mission produces a Poisson arrival stream built from i.i.d. exponential gaps, the conditional-uniformity property of its epochs, independent thinning, and the M/G/∞ transient law, all reusable in queueing and inventory missions.

Difficulty

The algebra of the proof (summing the binomial against the Poisson law of $N(t)$) is short. The work is in the probabilistic step the book treats in a sentence: that, given $N(t) = n$, the $n$ orders behave like independent uniform epochs, each of which independently is still in resupply at time $t$ with the same probability $p$. This needs the joint law of the partial sums of exponential variables (Eq. (3.3)), and then a symmetrization argument, since the epochs are ordered while the resupply times are attached to order indices. The naive route of computing $P[X(t) = x]$ by conditioning on individual epochs does not go through without that exchangeability step. The limit $t \to \infty$ is then elementary; stating a stationary version directly is not a substitute, since the book's "steady state" is exactly this limit.

Formalization scope

The model is a structure on a probability space $(\Omega, P)$: exponential interarrival times with rate $\lambda > 0$, nonnegative resupply times with a density and an integrable first coordinate, and mutual independence of the whole family. Orders are indexed from $0$, so the book's $X_1, \dots, X_n$ are $T_0, \dots, T_{n-1}$. Counts are cardinalities of sets of order indices, with value $0$ on the probability-zero event where infinitely many orders fall in a bounded interval.

Commitments and pinnings:

• "Steady state probability" (Theorems 6, 7, 9) is $\lim_{t\to\infty}P[\cdot(t) = x]$ for the system empty at time $0$, which is what the proofs compute via (3.8)–(3.11).
• Independence of resupply times from arrivals is not written in Theorem 6 but is used on p. 40; it is part of the model.
• The stock level $s$ does not enter the backorder model; it matters only in Theorem 8.
• Theorem 8 is stated algebraically: a vector on $\{0, \dots, s\}$ solves the balance equations (3.26), (3.25) for $0 < j < s$ and (3.32), and sums to one, if and only if it is the truncated Poisson law. The book obtains these equations by letting $t \to \infty$ in the forward equations under the unproved assumption $P_j'(t) \to 0$. The book writes (3.25) "for $0 \le j \le s$", which at $j = s$ contradicts its own (3.32); the boundary equation (3.32) is used. The sentence on p. 46 extending Theorem 8 to arbitrary resupply densities is asserted without proof and is not stated.
• Theorem 7 identifies the limit law by its probabilities (3.22)–(3.23); its mean $\lambda\bar\tau\bar u$ is a property of that law. Theorem 9 is stated for compound demand as the book states it, although the book's proof covers only the Poisson case.

A model in which $X(t)$ is postulated through its law, or in which resupply times may depend on the arrival epochs, makes the goal empty or false; here $X(t)$ is computed from the primitive arrival and resupply times, whose joint law is fully specified.

Welcome contributions: a general Poisson-process library (construction from exponential gaps, Poisson marginals, order-statistics property), independent thinning, and proofs of the milestones in the listed order.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 3. https://doi.org/10.1007/b138879
• C. Palm, "Analysis of the Erlang traffic formula for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
• G. J. Feeney and C. C. Sherbrooke, "The (s–1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
• C. C. Sherbrooke, "METRIC: A multi-echelon technique for recoverable item control", Operations Research 16(1), 1968, 122–141. https://doi.org/10.1287/opre.16.1.122
• S. M. Ross, Stochastic Processes, 2nd ed., Wiley, 1996, Section 2.3 (conditional distribution of arrival times) and Section 2.4 (the M/G/∞ queue).

Motivation

Service parts supply chains are often limited by a capacitated resource, such as a production line or a repair shop, instead of by lead times alone. Once capacity binds, the classical tools for setting stock levels (Palm's theorem and the Poisson distribution of units in resupply) no longer apply, and the quantity that determines how much stock is needed is the shortfall: the amount by which the end-of-period inventory falls below its target because capacity was insufficient. Chapter 8 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) builds its tactical planning models for capacity-limited systems on the distribution of this random variable, and on a continuous-time repair queue in which item counts are geometric.

The shortfall recursion is the Lindley recursion of queueing theory (Lindley 1952), so its stationary law is the law of the maximum of a random walk with negative drift. The exponential tail of that maximum goes back to Cramér's work on ruin probabilities; for capacitated production–inventory systems it was stated by Glasserman (1997), whose theorem the book quotes as Theorem 11. Glasserman and Tayur (1995) used the shortfall to optimize base-stock levels in multi-echelon capacitated systems, and Roundy and Muckstadt (2000) studied the mass-exponential approximation that the theorem motivates.

Setting

A single item is produced in periods $n = 1, 2, \dots$ of an infinite horizon; at most $c$ units can be produced per period. The demand of period $n$ is $D_n$; the demands are nonnegative, independent and identically distributed, with generic demand $D$ and $E[D] < c$ (the standing assumption of Section 8.1.1).

Under the modified $(s-1, s)$ policy with target level $s$, the facility observes $D_n$ and produces $\min\{c, s - I_{n-1} + D_n\}$ units, where $I_n$ is the end-of-period net inventory and $I_0 = s$. The shortfall $V_n = s - I_n$ satisfies $V_0 = 0$ and

$$V_n = \left[V_{n-1} + D_n - c\right]^+ . \tag{8.1}$$

With the random walk $S_n = \sum_{k=1}^{n} (D_k - c)$ ($S_0 = 0$), the stationary shortfall is

$$V = \sup_{n \ge 0} S_n .$$

A law on $\mathbb R$ is lattice if it is concentrated on a progression $a + d\mathbb Z$ with $d > 0$.

In the discrete case ($c$ and $D$ integer valued) $(V_n)$ is a Markov chain on $\{0, 1, 2, \dots\}$ with transition probabilities $p_{ij}$ (p. 185). In the repair model of Section 8.3.1, reparable units of item $i$ arrive at rate $\lambda_i$, $\lambda = \sum_i \lambda_i$, a single exponential server repairs at rate $\mu > \lambda$, $N$ is the number of units in repair and $N_i$ the number of item-$i$ units, and $\eta_i = \lambda_i/(\mu - \lambda + \lambda_i)$.

Formalization targets

Goal: Theorem 11, corrected (p. 191)

Assume $E[e^{\alpha D}] < \infty$ for all $\alpha < \delta$, with $\delta > 0$; $P[D > c] > 0$; the law of $D$ is non-lattice; and $E[e^{-\alpha(c-D)}] = 1$ has a root in $(0, \delta)$. Then there are $\beta > 0$ and $\alpha > 0$ with

$$\frac{P\{V > v\}}{\beta e^{-\alpha v}} \to 1 \quad (v \to \infty), \qquad \alpha \text{ the unique positive root of } E\left[e^{-\alpha(c - D)}\right] = 1 .$$

The constant $\beta$ is left unspecified, as in the book.

Milestones, in attack order

1. Eq. (8.1): under the modified policy, $s - I_n = V_n$ for every $n$, independently of $s$.
2. Section 8.1.1: $V < \infty$ almost surely, $P\{V_n > v\} \to P\{V > v\}$ for every $v$, and the law of $V$ is stationary for (8.1).
3. Eq. (8.2): for $v > 0$, $P\{V_n > v\} = P\{D_n > v + c\} + E_D[1(d \le v + c)\, P\{V_{n-1} > v + c - d\}]$.
4. Theorem 11, second sentence: $E[e^{-\alpha(c-D)}] = 1$ has at most one positive root.
5. Section 8.1.2: with integer demand, $(V_n)$ is a Markov chain with transition probabilities $p_{ij}$.
6. Section 8.1.2: $\pi_i = \lim_n P\{V_n = i\}$ exists and solves $\pi\mathcal P = \pi$, $\sum_i \pi_i = 1$, $\pi_i \ge 0$.
7. Section 8.3.1: if $N$ is geometric with parameter $\lambda/\mu$ and $N_i$ given $N = j$ is binomial$(j, \lambda_i/\lambda)$, then $P[N_i = j] = (1 - \eta_i)\eta_i^j$.
8. Section 8.3.1: $\sum_{j > s} p_i(j) = \eta_i^{s+1}$, and the smallest cost-minimising stock level is the smallest $s$ with $\eta_i^{s+1} \le h_i/(h_i + b)$.

Significance

The exponential tail is the justification the book gives for approximating the shortfall by a mass-exponential law (an atom at zero plus an exponential tail), from which target stock levels and fill rates are computed in closed form. The decay rate $\alpha$ depends only on the demand law and the capacity, so the theorem also says how the stock needed for a given service level grows as utilization approaches one. The discrete-chain milestones justify the exact computation of the shortfall distribution behind the book's Table 8.1 and Figures 8.3–8.8. The geometric law of $N_i$ reduces the multi-item repair problem to independent newsvendor problems with an explicit solution.

The asymptotics of the random-walk maximum are proved in the literature (Cramér–Lundberg theory, Feller Vol. II, XII.5; Asmussen, Applied Probability and Queues, XIII.5); no machine-checked proof is known to exist. Mathlib has neither the Lindley recursion, nor ladder-height decompositions, nor the key renewal theorem for non-lattice laws. The printed Theorem 11 is not correct as stated (see Formalization scope), so the mission also records a corrected statement.

Difficulty

The central step of the goal is the passage from the random walk to an exact asymptotic. An exponential change of measure (Esscher tilt) with the root $\alpha$ turns $P\{V > v\}$ into an expectation under a law with positive drift, but it only yields the upper bound $P\{V > v\} \le e^{-\alpha v}$ (Lundberg's inequality); it does not show that $e^{\alpha v}P\{V > v\}$ converges, nor that the limit is positive. Convergence needs a renewal theorem for the overshoot of the tilted walk, which fails for lattice laws. That is why the non-lattice hypothesis cannot be dropped. For the milestones, the existence of the stationary law needs the reversal argument that identifies the law of $V_n$ with that of $\max_{k \le n} S_k$, plus the strong law of large numbers to show $V < \infty$ from $E[D] < c$.

Formalization scope

• Model. Demands are real, nonnegative, measurable, i.i.d. (iIndepFun plus IdentDistrib with $D_1$), integrable, with $E[D] < c$; these are fields of ShortfallModel. Periods are numbered from $1$ as in the book (demand 0 is an unused i.i.d. copy). The discrete case is a separate structure with $\mathbb N$-valued demand and capacity.
• Stationary shortfall. The book's "stationary distribution ... Let $V$ represent this random variable" is pinned to $V = \sup_{n \ge 0} S_n$, taken in $[0, \infty]$ and converted to a real number; milestone 2 proves that it is the limit law of $V_n$ from $V_0 = 0$ and a stationary law of (8.1). The discrete $\pi_i$ is pinned to $\lim_n P\{V_n = i\}$.
• Corrections to Theorem 11. The printed theorem is false. For integer demand $P\{V > v\}$ is a step function, and no $\beta e^{-\alpha v}$ is asymptotic to it. If $E[e^{\alpha D}]$ is finite only for $\alpha < \delta$, the equation $E[e^{-\alpha(c-D)}] = 1$ may have no root in $(0,\delta)$. The goal therefore adds two labelled hypotheses: a non-lattice demand law, and a root in $(0, \delta)$. The mass-exponential demand of Section 8.1.3 (an atom at $0$ plus a density) is non-lattice. The approximation $\beta \approx e^{-2(.583)(c-E(D))/\sigma}$ is not stated.
• Repair model. The M/M/1 queue is not built. The geometric law of $N$ (asserted on p. 202) and the binomial split of $N$ (quoted from Chapter 3) enter milestone 7 as hypotheses, exactly as the page's proof uses them. The stability condition $\lambda < \mu$, not written on the page, is a hypothesis. "The optimal $s_i$" is read as the smallest minimiser of the cost.
• Ruled out. Stating Theorem 11 with $\alpha$ or $\beta$ allowed to depend on $v$, with $\beta = 0$ (the ratio would be a division by zero, which Lean evaluates to $0$), or for a $V$ postulated to have an exponential tail proves nothing. Here $\beta, \alpha$ are quantified before $v$, both are asserted positive, and $V$ is constructed from the demands.
• Not formalized. The mass-exponential approximations (8.3)–(8.4), the Roundy–Muckstadt refinement, the fill-rate formula $\eta(s)$ (a definition, whose steady-state identity needs uniform integrability the book does not discuss), the random-capacity chain on p. 186, and the monotonicity of $s_i$ in $\mu$.
• Reusable infrastructure. Welcome: the Lindley recursion and its reversal identity, the Loynes existence theorem, Lundberg's inequality, and a non-lattice renewal theorem. All of these are needed well beyond this mission, in queueing (GI/G/1 waiting times) and ruin theory.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 8. https://doi.org/10.1007/b138879
• P. Glasserman, Bounds and asymptotics for planning critical safety stocks, Operations Research 45(2), 244–257, 1997. https://doi.org/10.1287/opre.45.2.244
• P. Glasserman and S. Tayur, Sensitivity analysis for base-stock levels in multiechelon production-inventory systems, Management Science 41(2), 263–281, 1995 (the book's reference [97]). https://doi.org/10.1287/mnsc.41.2.263
• R. O. Roundy and J. A. Muckstadt, Heuristic computation of periodic-review base stock inventory policies, Management Science 46(1), 104–109, 2000. https://doi.org/10.1287/mnsc.46.1.104.15131
• D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971, Chapter XII.
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Chapter XIII. https://doi.org/10.1007/b97236

Motivation

Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the $(s-1, s)$ policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level $s$. A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.

The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson $(s-1,s)$ model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.

Setting

A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate $\lambda > 0$. An order is for $j$ units with probability $u_j$, where $u_0 = 0$ and the mean order size $\bar u = \sum_j j u_j$ is finite (compound Poisson demand; simple Poisson demand is $u_1 = 1$). Resupply times have mean $\bar\tau > 0$. The steady-state probability that $x$ units are in resupply is

$$p(0 \mid \lambda\bar\tau) = e^{-\lambda\bar\tau}, \qquad p(x \mid \lambda\bar\tau) = \sum_{j \ge 1} e^{-\lambda\bar\tau}\frac{(\lambda\bar\tau)^j}{j!}\,u^{(j)}_x \quad (x \ge 1),$$

where $u^{(j)}_x$ is the probability that $j$ orders total $x$ units. In this mission $p(\cdot \mid \lambda\bar\tau)$ is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is $\mu = \lambda\bar\tau\bar u$, and the book also writes $p(x \mid \mu)$.

For a stock level $s \in \{0, 1, 2, \dots\}$:

• the ready rate is $R(s) = \sum_{x \le s} p(x \mid \lambda\bar\tau)$;
• the expected backorders are $B(s) = \sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$;
• the expected on-hand inventory is $\sum_{x \le s}(s - x)\,p(x \mid \lambda\bar\tau)$;
• under simple Poisson demand the fill rate is $F(s) = \sum_{x < s} p(x \mid \lambda\bar\tau)$.

Forward differences are $\Delta f(s) = f(s+1) - f(s)$ and $\Delta^2 f(s) = \Delta f(s+1) - \Delta f(s)$; discrete convexity means $\Delta^2 f \ge 0$.

With $n$ items, unit costs $c_i > 0$ and budget $b$, Problem 4 (3.40) is

$$\min \sum_i B_i(s_i) \quad \text{s.t.} \quad \sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le b,\quad s_i \in \{0,1,\dots\}.$$

For a multiplier $\theta > 0$, the item-wise criterion defines $s_i^*(\theta)$ as the least $s$ with $\sum_{x \le s} p(x \mid \mu_i) \ge 1/(1 + \theta c_i)$, and $C(\theta) = \sum_i c_i\,[s_i^*(\theta) - \mu_i + B_i(s_i^*(\theta))]$.

Formalization targets

Goal: the Lagrangian stock levels solve Problem 4

For every $\theta > 0$, each $s_i^*(\theta)$ exists and

$$\sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le C(\theta) \ \Longrightarrow\ \sum_i B_i(s_i^*(\theta)) \le \sum_i B_i(s_i)$$

for every vector $s$ of nonnegative integer stock levels. That is, $s^*(\theta)$ is optimal for Problem 4 at budget $b = C(\theta)$. This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.

Milestones

1. Section 3.3, p. 53: $\Delta F(s) = p(s \mid \lambda\bar\tau)$ and $\Delta^2 F(s) = p(s \mid \lambda\bar\tau)\,(\lambda\bar\tau/(s+1) - 1)$, so under simple Poisson demand $F$ is discretely concave exactly on $s \ge \lfloor\lambda\bar\tau\rfloor$ (resp. $s \ge \lambda\bar\tau - 1$ for integer $\lambda\bar\tau$).
2. Section 3.3, p. 55: $\Delta B(s) = -(1 - R(s))$ and $\Delta^2 B(s) = p(s+1 \mid \lambda\bar\tau)$.
3. Theorem 10 (Everett), p. 57.
4. Section 3.4.2, p. 60: $E[\text{On-hand}] = s - \lambda\bar\tau\bar u + B(s)$.
5. Section 3.4.2, p. 61: the least $s$ with $R(s) \ge 1/(1+\theta c)$ minimizes $f(s) = (1 + \theta c)B(s) + \theta c s$.
6. Section 3.4.2, p. 61: $s^*(\theta)$ and $C(\theta)$ are nonincreasing in $\theta$.
7. Section 3.4.2, p. 63: at $\theta_{\max} = \max_i c_i^{-1}(1/p(0 \mid \mu_i) - 1)$ every $s_i^*(\theta_{\max}) = 0$.
8. Section 3.4.3, p. 65: every solution produced by the greedy marginal-analysis rule for Problem 5 (3.41), maximum average fill rate subject to $\sum_i c_i s_i \le b$ and $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$, is optimal at the budget it uses.

Significance

The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, $s \ge \lfloor\lambda\bar\tau\rfloor$, is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.

All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.

Difficulty

The algebra of first differences is elementary; the difficulties are elsewhere. $B(s)$ is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying $\sum_x x\,p(x \mid \lambda\bar\tau)$ with $\lambda\bar\tau\bar u$, requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of $s^*(\theta)$ requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every $F_i$ is concave; dropping the floor constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ makes it false.

Formalization scope

Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields $\lambda, \bar\tau > 0$, an order-size distribution $u$ with $u_0 = 0$, $u_j \ge 0$, $\sum_j u_j = 1$, and summable $j u_j$ (the finite mean is added: without it $B$ is infinite). Expected on-hand inventory is the finite sum $E[(s - X)^+]$. Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).

Pinnings and deviations, each stated in the item's Formalization Note:

• $\theta > 0$ and $c > 0$. The book allows $\theta \ge 0$ in (3.38); at $\theta = 0$ the threshold $1$ is never reached and $f = B$ has no minimizer.
• Theorem 10 without convexity and for an arbitrary set $S$: the book assumes $f, g$ convex, but its proof does not use it and the applications are to integer vectors (labelled generalization).
• $B$'s identities for compound Poisson demand. The book derives them under simple Poisson demand and uses them for compound demand on p. 61; strict convexity and strict decrease are stated only for simple Poisson demand, as in the book.
• Optimality is always against every feasible vector, never an infimum; the greedy procedure is a relation on sequences, covering every tie-breaking rule.
• Problem 5 keeps the constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$.

A trivializing formalization is ruled out: the goal is stated for the book's own backorder function $B$ built from the compound Poisson law, not for an arbitrary convex function nor for a $B$ defined through its differences.

Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 3, pp. 47–65. https://doi.org/10.1007/b138879
• H. Everett III, Generalized Lagrange multiplier method for solving problems of optimum allocation of resources, Operations Research 11(3):399–417, 1963. https://doi.org/10.1287/opre.11.3.399
• B. L. Fox and D. M. Landi, Searching for the multiplier in one-constraint optimization problems, Operations Research 18(2):253–262, 1970. https://doi.org/10.1287/opre.18.2.253
• G. J. Feeney and C. C. Sherbrooke, The (s−1, s) inventory policy under compound Poisson demand, Management Science 12(5):391–411, 1966. https://doi.org/10.1287/mnsc.12.5.391