Operations Research

Motivation

Chess, checkers, Go and Backgammon share a feature that card games such as Poker lack: whenever a player moves, the player knows everything that has happened so far. von Neumann and Morgenstern call this perfect information and devote §15 of Theory of Games and Economic Behavior (1944; 3rd ed. 1953) to it. Their result is that such a game, viewed as a zero-sum two-person game, is strictly determined: it has a value that each player can secure with a pure strategy, without any randomization. For Chess this means that exactly one of three statements is true: White can force a win, Black can force a win, or both can force at least a draw ((15:D:a)–(15:D:c)).

Timeline. Zermelo (1913, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels) showed for Chess that either one side can force a win or both can avoid losing; his argument is not phrased in terms of strategies and a value, and was later corrected and completed by König (1927) and Kalmár (1928/29). von Neumann and Morgenstern (1944, §15) proved strict determinateness for every finite zero-sum two-person game with perfect information, including chance moves (15.7.1), and gave the explicit formula (15:12) for the value. Kuhn (1953, Extensive games and the problem of information, Annals of Mathematics Studies 28) recast games in tree form and extended the pure-strategy existence result to general-sum games with perfect information (subgame-perfect equilibria by backward induction).

Setting

A game tree $\Gamma$ is a finite rooted tree. Each leaf is a finished play $\pi$ and carries the payoff $\mathfrak F_1(\pi) \in \mathbb R$ to player 1; player 2 receives $-\mathfrak F_1(\pi)$. Each internal node is a move $\mathfrak M$ of one of three kinds $k$, with alternatives $\sigma = 1, \dots, \alpha$ leading to subtrees $\Gamma_\sigma$:

• $k = 0$, a chance move, where alternative $\sigma$ occurs with probability $p(\sigma) \geqq 0$, $\sum_\sigma p(\sigma) = 1$;
• $k = 1$, a personal move of player 1, with $\alpha \geqq 1$;
• $k = 2$, a personal move of player 2, with $\alpha \geqq 1$.

A pure strategy $\tau_1$ of player 1 is a complete plan choosing an alternative at every node of kind 1; $\tau_2$ does the same at every node of kind 2. The normalized form $\mathcal H(\tau_1, \tau_2)$ is the expected payoff to player 1, the expectation being over the chance moves. With the maxima and minima taken over the finitely many pure strategies,

$$v_1 = \operatorname{Max}_{\tau_1} \operatorname{Min}_{\tau_2} \mathcal H(\tau_1, \tau_2), \qquad v_2 = \operatorname{Min}_{\tau_2} \operatorname{Max}_{\tau_1} \mathcal H(\tau_1, \tau_2).$$

Always $v_1 \leqq v_2$; the game is strictly determined when $v_1 = v_2$ (14.4.2).

For a function $f(\sigma_1)$ of the alternatives of the first move $\mathfrak M_1$, of kind $k_1$, the operation $M^{k_1}_{\sigma_1}$ of (15:8) is $\sum_{\sigma_1} p_1(\sigma_1) f(\sigma_1)$, $\operatorname{Max}_{\sigma_1} f(\sigma_1)$ or $\operatorname{Min}_{\sigma_1} f(\sigma_1)$ for $k_1 = 0, 1, 2$. Applying these operations from the leaves back to the root gives the backward-induction value $v(\Gamma)$.

Formalization targets

Goal: 15.6.1 with (15:12)

For every finite game tree $\Gamma$,

$$v_1 = v_2 = v = M^{k_1}_{\sigma_1} M^{k_2(\sigma_1)}_{\sigma_2} \cdots M^{k_\nu(\sigma_1, \dots, \sigma_{\nu-1})}_{\sigma_\nu} \mathfrak F_1(\pi(\sigma_1, \dots, \sigma_\nu)).$$

Both the equality $v_1 = v_2$ and the value formula are part of the goal.

Milestones

• (13:E): for finite nonempty domains and $f$ ranging over all functions of $x$, $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Min}_f \operatorname{Max}_x \psi(x, f(x))$; and (13:G): $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Max}_x \operatorname{Min}_u \psi(x, u)$.
• (15:2)–(15:7): $v_k = M^{k_1}_{\sigma_1} v_{\sigma_1/k}$ for $k = 1, 2$, one milestone for each kind of first move, without assuming that any game is strictly determined.
• (15:C:a): a game of length $0$ is strictly determined with value $w$; (15:C:b): if every $\Gamma_{\sigma_1}$ is strictly determined, so is $\Gamma$.
• (15:13), (15:D:a)–(15:D:c): for games without chance moves whose plays end in $1, 0, -1$, the value is one of these three numbers, and it decides which player can force a win or whether both can force a tie.

Significance

The theorem is the first existence result for the value of a class of games in pure strategies. It shows that the whole difficulty of the general zero-sum two-person game, the need for mixed strategies (§17), comes from imperfect information. It gives a construction as well as an existence proof: the value and optimal strategies are computed by backward induction, the procedure behind retrograde analysis of endgames, minimax search in game-playing programs, and the dynamic programming recursions of sequential decision problems with an adversary. The Chess trichotomy (15:D) is its best-known consequence.

Formalizing it adds a checked account of the passage from the extensive to the normalized form for a whole class of games, which the book carries out informally (15.4.2, 15.5.1: "the reader may verify it from the formalistic point of view"). The result is classical and fully proved in the book; the work is to formalize that proof on a tree model. Mathlib has saddle points (Order/SaddlePoint) and the minimax theorem for continuous functions (Topology/Sion), but no game trees, strategies of extensive games, or backward induction. No machine-checked version of this theorem with chance moves and the normalized form over complete plans is known to the mission.

Difficulty

The recursions (15:2)–(15:7) are not formal consequences of the definitions: $v_1$ and $v_2$ are extrema over whole plans of $\Gamma$, while the right-hand sides are extrema over plans of the separate games $\Gamma_{\sigma_1}$. At a personal move of player 1, $v_2 = \operatorname{Max}_{\sigma_1} v_{\sigma_1/2}$ requires interchanging a Min over player 2's plans, which are functions of player 1's first choice, with a Max over that choice: this is exactly (13:E), a max-min equality that fails for general functions of two variables and holds here because the minimizing variable is a function of the maximizing one. A proof that treats the Max over $\tau_1$ and the Min over $\tau_2$ as interchangeable without this step is circular.

A second difficulty is the strategy spaces themselves. A complete plan chooses at nodes the plan itself excludes, so the pure strategies of $\Gamma$ are not simply pairs of a first choice and one strategy of the chosen subgame; the identification the book uses in 15.5.1 has to be justified by showing that the extra coordinates do not change $\mathcal H$.

Formalization scope

A game is an inductive type GameTree with constructors leaf w, chance α p next hp hsum, move1 α hα next, move2 α hα next; alternatives are Fin α (numbered from $0$). The conditions $p \geqq 0$, $\sum p = 1$ and $\alpha \geqq 1$ at personal moves are constructor fields, so every tree is a legitimate game. Pure strategies are dependent types Strategy1 t, Strategy2 t defined by recursion on the tree (complete plans), with Fintype and Nonempty instances; $\mathcal H$ is payoff t τ₁ τ₂, the expected leaf payoff; v1, v2 are Finset.sup'/Finset.inf' over all strategies, so every Max and Min is attained.

Standing hypotheses and conventions taken from the book:

• finite strategy sets and attained extrema (13.2.1, 14.1.1): finite trees with finitely many alternatives at every move;
• perfect information, i.e. preliminarity equals anteriority (6.4.1, (15:B)): built into the tree model, which is the sequence of games (15:1);
• zero-sum two-person (15.3.1): one payoff $\mathfrak F_1$, player 2 receives $-\mathfrak F_1$ and minimizes $\mathcal H$;
• chance probabilities nonnegative and summing to one (15.4.2, 10.1.1); $\alpha \geqq 1$ at every move;
• (15:D) additionally assumes no chance moves and outcomes $1, 0, -1$ (15.7.1).

The book's formal model is the set-theoretic one of §§9–10, with partitions of the set of plays; the tree restates it for the perfect-information case and does not formalize §§9–10. The book fixes one length $\nu$ for all plays; trees with plays of different lengths contain the book's games as a special case, so the goal is at least as strong as the book's theorem.

Strategies are plans, never responses: a strategy of player 1 is fixed before play and cannot depend on player 2's strategy, which would make $v_1 = v_2$ trivial. Chance moves are part of the goal; a version without them proves only the Chess case and is weaker than the book.

Reusable beyond this mission: the tree model, its strategy types and the normalized form, which later chapters on extensive games can import. Welcome contributions: proofs of the milestones, and a lemma identifying the strategies of $\Gamma$ with the book's recursive description (15.4.2, 15.5.1).

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §§6, 11, 13–15. https://doi.org/10.1515/9781400829460
• E. Zermelo, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels, Proc. Fifth International Congress of Mathematicians, vol. II, 1913, pp. 501–504.
• U. Schwalbe, P. Walker, Zermelo and the early history of game theory, Games and Economic Behavior 34 (2001), 123–137. https://doi.org/10.1006/game.2000.0794
• H. W. Kuhn, Extensive games and the problem of information, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton, 1953, 193–216. https://doi.org/10.1515/9781400881970-012

Motivation

Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.

What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.

Setting

Fix one item. Time is counted in whole periods $t = 0, 1, 2, \dots$, and $J$ is the finite set of bases. For each base $j$:

• $T_{i0}$ is the repair lead time, so shipments are decided in periods $t = 0, \dots, T_{i0}$;
• $T^r_{ij}$ and $T^e_{ij}$ are the regular and expedited transportation times from the depot to base $j$, integers with $1 \le T^e_{ij} < T^r_{ij}$;
• $\tilde S_{i0t}$ is the known cumulative supply at the depot through period $t$ (stock on hand plus arrivals already in the pipeline), and $\tilde S_{ijt}$ the known cumulative supply at base $j$. The latter is constant for $t \ge T^r_{ij}$, since nothing not yet shipped can arrive earlier than $T^r_{ij}$ by regular transport;
• $X_{ijt}$ is the cumulative demand at base $j$ through period $t$, a nonnegative integer random variable, nondecreasing in $t$, with finite mean;
• $h_{ij} > 0$, $b_{ij} > 0$ and $e_{ij} \ge 0$ are the incremental holding, shortage and expediting costs.

If $S_{ijt}$ units have arrived at base $j$ by period $t$, the expected cost of that period is

$$G_{ijt}(S) = h_{ij}\,E[S - X_{ijt}]^+ + b_{ij}\,E[X_{ijt} - S]^+,$$

and stock left at the end of the horizon costs

$$Q_{ij}(S) = h_{ij}\sum_{t > T^r_{ij} + T_{i0}} E[S - X_{ijt}]^+ .$$

The stock allocation model $\mathrm{SAM}_i$ chooses nonnegative integer regular shipments $y^r_{ijt}$, $t = 0, \dots, T_{i0}$, with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base $j$ is $S_{ijt} = \tilde S_{ij(T^r_{ij}-1)} + \sum_{t' \le t - T^r_{ij}} y^r_{ijt'}$, and the model minimizes $\sum_j \{\sum_{t=T^r_{ij}}^{T^r_{ij}+T_{i0}} G_{ijt}(S_{ijt}) + Q_{ij}(S_{ij(T^r_{ij}+T_{i0})})\}$. The extended model $\mathrm{ESAM}_i$ adds expedited shipments $y^e_{ijt}$, which arrive after $T^e_{ij}$ periods at an extra cost $e_{ij}$ per unit.

The constrained newsvendor problem $\mathrm{CN}_{ijt}$ minimizes $G_{ijt}(S)$ over integers $S \ge \tilde S_{ijt}$. Its largest optimal solution is written $\hat S_{ijt}$.

Formalization targets

Goal: Theorem 15 (p. 237)

In every optimal solution of $\mathrm{SAM}_i$, for every base $j$ and every $t \in [T^r_{ij}, T^r_{ij} + T_{i0}]$,

$$\tilde S_{ij(T^r_{ij}-1)} \;\le\; S^*_{ijt} \;\le\; \hat S_{ijt}.$$

The bound is uniform over optimal solutions and uses nothing but the single-period problems.

Milestones

1. Separability (Section 10.4.1, p. 236). The multi-item problem $\mathrm{SAM}$ splits into the $\mathrm{SAM}_i$: its optimal solutions are exactly the tuples of optimal item solutions, and $Z^* = \sum_i Z^*_i$.
2. Convexity of $Q_{ij}$ (p. 234) and of $G_{ijt}$ (p. 237), in the discrete sense of nondecreasing first differences on $\mathbb Z$.
3. The newsvendor solution (10.19). $\hat S_{ijt} = \max(\tilde S_{ijt}, s^0)$ with $s^0$ the least integer such that $P(X_{ijt} \le s^0) > b_{ij}/(b_{ij}+h_{ij})$.
4. Monotonicity (10.20). $\hat S_{ij(t-1)} \le \hat S_{ijt}$ on $[T^r_{ij}, T^r_{ij} + T_{i0}]$.
5. Theorem 16, corrected (p. 244). In every optimal solution of $\mathrm{ESAM}_i$, $\tilde S_{ijt} \le S^*_{ijt}$. Writing $M_{jt} = \max_{k \in [T^e_{ij}, t]}(\hat S_{ijk} - \tilde S_{ijk})$, also $S^*_{ijt} \le \tilde S_{ijt} + M_{jt}$, provided $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$.

Two supporting items state that $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.

Significance

Theorem 15 is what allows the book (pp. 238–239) to rewrite $\mathrm{SAM}_i$ with 0–1 variables $\delta_{ijtk}$ indicating $S_{ijt} = k$. Only $k$ between $\tilde S_{ij(T^r_{ij}-1)}$ and $\hat S_{ijt}$ is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.

The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With $T^r_{ij} \ge T^e_{ij} + 2$, an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.

Difficulty

The central step is the exchange. Take the first period $k$ in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at $k$. This must be shown feasible, to change only $S_{ijk}$, and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums $\min(t - T^e_{ij}, T_{i0})$, and cumulative constraints across bases.

The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For $\mathrm{ESAM}_i$ even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.

Formalization scope

• One item at a time: ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space $(\Omega, P)$, [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.
• $G$ and $Q$ are defined from the demand as in the book: Bochner integrals of $(S - X)^+$ and $(X - S)^+$, and a tsum for $Q$. The item model requires finite means and convergence of the series for $Q$ at every stock level, so that no integral or sum takes Lean's junk value $0$.
• "The largest optimal solution" is the predicate IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take $\hat S$ as a function satisfying it. Milestone (10.19) shows it exists.
• "An optimal solution" means a feasible plan with objective at most that of every feasible plan. The theorems hold for every optimal plan.
• Pinned conventions and additions. The following are not written in the book: $h_{ij}, b_{ij} > 0$ and $e_{ij} \ge 0$; nonnegative, nondecreasing depot supply; nondecreasing base supply (used in the book's proof of Theorem 16); finite mean demand; convergence of $Q$'s series. (10.19) is read with the critical fractile "least $s$ with $F(s) > b/(b+h)$", the book's $\lceil F^{-1}\rceil$/$\lfloor F^{-1}\rfloor$ with ties broken upward. Theorem 16 carries the proviso "$T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$". Separability is stated both for optimal plans and for optimal values.
• Ruled out. The feasible sets of $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ impose no upper bound on the cumulative stock, and $\hat S$ is defined from $G$ alone, never from the allocation problem. The bounds are therefore not true by definition.
• Omitted. The LP reformulations (10.22)–(10.28) and (10.45)–(10.52) and the integrality of their relaxations, which the book asserts with a reference to [68]; the greedy algorithms and their optimality conditions (asserted); the book's claim that $Q_{ij}$ is strictly increasing (p. 238), which fails when $P(X_{ijt} \le S) = 0$ beyond the horizon and is not needed; the dynamic program of Section 10.3 and the repair model of Section 10.6.
• The discrete-convexity and newsvendor facts are reusable for any single-location inventory model on $\mathbb Z$. Contributions are welcome on the convexity lemmas, the critical-fractile characterization, and a reusable exchange lemma for cumulative-shipment models.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005, Chapter 10, pp. 225–246. DOI 10.1007/b138879
• K. J. Arrow, T. Harris, J. Marschak, "Optimal inventory policy", Econometrica 19(3), 1951, 250–272 (the newsvendor critical fractile). DOI 10.2307/1906813

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 networks (spare parts for aircraft, military systems, industrial equipment) hold stock at several echelons: a depot, intermediate stocking facilities, and bases or warehouses that face demand. Two questions recur in their planning. First, how should a given amount of stock be split among locations whose expected costs are convex in the stock they hold? Second, does adding an echelon, a depot that pools the demand of several warehouses, raise or lower the stock the system needs?

Chapter 7 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879), treats both. For the second it follows Eppen and Schrage (1981, reference [78] of the book): with normal demands, a depot that places orders every period and allocates stock so that all warehouses face the same stockout probability reduces the choice of system stock to a single critical-fractile equation. For the first, the chapter's multi-echelon pooling model (Section 7.3) evaluates nested cost functions of the form "holding and shortage cost plus the minimum over allocations of a sum of convex costs", and its appendix (Section 7.4) gives the marginal allocation algorithm AllocOpt that computes these minima exactly for every stock level at once.

Marginal analysis for separable convex resource allocation is classical (Fox, Management Science, 1966); the monograph of Ibaraki and Katoh (MIT Press, 1988) surveys it.

Setting

Allocation data (Section 7.4). There is a set $M = \{1, \dots, \bar M\}$ of locations and an augmented set $M_0 = \{0\} \cup M$. Each location $m \in M_0$ has integer gridpoints $0 = r^m_0 < r^m_1 < \dots < r^m_{n(m)}$. For $m \in M$, the value $c^m_n$ of a convex function is given at each gridpoint. The slopes (7.19) are $\hat c^m_n = (c^m_{n+1} - c^m_n)/(r^m_{n+1} - r^m_n)$ for $n < n(m)$, and $\hat c^m_{n(m)}$ repeats the last one. The piecewise linear approximation $\tilde C_m$ of (7.20)–(7.21) interpolates the values $c^m_n$ at the gridpoints and continues with slope $\hat c^m_{n(m)}$ beyond the last one. A convex function $f$ on $\mathbb R_+$ is also given.

The allocation optimization (7.22) asks, for each $n \in N_0 = \{0, \dots, n(0)\}$, for

$$c^0_n = f(r^0_n) + \min\Bigl\{ \sum_{m \in M} \tilde C_m(r_m) : r_m \ge 0 \text{ integer},\ \sum_{m \in M} r_m = r^0_n \Bigr\}.$$

Algorithm AllocOpt (Definition 4) keeps a current gridpoint index $n^*(m)$ and allocation $r^*(m)$ per location. For each increment $r^0_n - r^0_{n-1}$ of the target, it repeatedly gives units to a location $m^*$ whose current slope $\hat c^{m^*}_{n^*(m^*)}$ is minimal, up to that location's next gridpoint, and records the accumulated cost.

Pooling system (Section 7.2.1). One depot supplies $m$ warehouses. The demand $d_{jt}$ at warehouse $j$ in period $t$ is normal with mean $\mu_j$ and variance $\sigma_j^2$, independent across periods and warehouses. The supplier-to-depot lead time is $D$ periods, the depot-to-warehouse lead time $A$ periods, and holding and backorder costs $h, b$ are equal at all warehouses. Positions $I_j$ are in balance when $\Phi((I_j - A\mu_j)/(\sqrt A\,\sigma_j))$ is the same for all $j$. For system inventory position $s$, with $Y_0$ the system demand over $D$ periods and $Y_j$ the demand at $j$ over the next $A + 1$ periods, the balanced allocation gives each warehouse a share proportional to $\sigma_j$, and $z_j$ is its end-of-period net inventory.

Formalization targets

Goal: Proposition 2 (correctness)

For every tie-breaking rule in its arg min steps, AllocOpt returns values $c^0_n$ that satisfy (7.22) for every $n \in N_0$: some feasible integer allocation attains $c^0_n - f(r^0_n)$, and no feasible integer allocation does better.

Milestones

1. Slope monotonicity (p. 178): $\hat c^m_n \ge \hat c^m_{n-1}$ for $0 < n \le n(m)$.
2. Convexity of $\tilde C_m$ on $[0, \infty)$ (proof of Proposition 2, p. 179).
3. Remark 2 (p. 179): with the inner loop run only while the current slope is $\le 0$, AllocOpt solves (7.22) with $\sum_m r_m \le r^0_n$.
4. Lemma 3 (p. 152): if the positions are in balance and

$$\sum_{j} d_{j,t-1} \ge \max_{i} \Bigl\{ \sum_{j \ne i} d_{j,t+D-1} + d_{i,t+D-1}\Bigl(1 - \frac{\sum_j \sigma_j}{\sigma_i}\Bigr)\Bigr\},$$

then a nonnegative allocation of the arriving $\sum_j d_{j,t-1}$ units restores balance. 5. Net inventory law (pp. 156–157): $z_j$ is normal with mean $(s - (D + A + 1)\sum_i \mu_i)\,\sigma_j / \sum_i \sigma_i$ and variance $(A + 1)\sigma_j^2 + (\sigma_j / \sum_i \sigma_i)^2 D \sum_i \sigma_i^2$. 6. Critical fractile (pp. 157–158): $s$ minimizes $\sum_j E[h (z_j)^+ + b (z_j)^-]$ if and only if $\Phi(z) = b/(b+h)$, where

$$z = \frac{s - (D + A + 1)\sum_i \mu_i}{\bigl[(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2\bigr]^{1/2}}.$$

Significance

The goal certifies an algorithm that the chapter uses as a subroutine three times: in the pool cost (7.14), the subsystem cost (7.15) and the system cost (7.17), and hence in the claim of Section 7.3 that the system-wide cost function can be computed in time $n \log n$ in the number of locations. Because AllocOpt produces the whole vector $(c^0_n)_{n \in N_0}$ in one pass, its correctness gives the nested value functions at every gridpoint of the next echelon, which is what allows the recursion up the echelons. The Eppen–Schrage milestones give the classical quantitative form of risk pooling: the system stock is set by one critical fractile, and the standard deviation term $(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2$ is what the book compares with the single-warehouse and the decentralized systems.

On formalization: the book states Proposition 2 with a two-sentence argument and Remark 2 without proof. The Eppen–Schrage computations are displayed derivations. None of these results has a machine-checked proof on the platform. A verified AllocOpt, stated for an explicit algorithm rather than for an abstract greedy procedure, is reusable for any separable convex integer allocation with a sum constraint.

Difficulty

The usual greedy exchange argument assumes that units are allocated one at a time. AllocOpt allocates in blocks, up to the next gridpoint of the chosen location, and it carries its state across successive targets $r^0_{n-1} \to r^0_n$ without restarting. The proof must therefore show that the state after each outer step is itself an optimal allocation for the current target, and that block moves never step past a breakpoint where the arg min would change. The slopes can be negative, and the equality constraint forces allocation even when every marginal cost is positive. Remark 2 needs an additional argument: under the inequality constraint the loop may stop before $u$ reaches zero, and that point is optimal only because the slopes are nondecreasing.

For the pooling results, the balanced allocation mixes the depot-lead-time demand $Y_0$ of all warehouses with the local demand $Y_j$, and the Gaussian law of $z_j$ rests on the independence of disjoint blocks of periods. The fractile statement requires strict monotonicity of each warehouse's expected cost derivative in $s$, not only a first-order condition.

Formalization scope

• Indices and types. Locations of $M$ are Fin Mbar; gridpoints are integers, values and slopes real numbers; allocations are functions Fin Mbar → ℕ. The standing assumptions of Section 7.4 form the predicate WellFormed: $\bar M \ge 1$, $n(m) \ge 1$ for $m \in M$ (a slope (7.19) needs two gridpoints), gridpoints starting at $0$ and strictly increasing at every location of $M_0$, each $c^m_n$ the value of a function convex on $[0, \infty)$, and $f$ convex on $[0, \infty)$.
• The minimum in (7.22) is stated as attainment plus a lower bound over the finite, nonempty set of feasible integer allocations, never as an unconstrained infimum.
• Ties. The book's arg min fixes no tie-breaking rule. Results are stated for every selection rule that returns a minimizing location.
• Termination. AllocOpt is a total Lean function. The inner loop is given more passes than it can use, so it always exits through its own condition.
• Not stated. The operation count of Proposition 2, $O((1 + \log_2 \bar M)\sum_{m \in M_0} n(m))$, and Proposition 1 and Remark 1 (p. 177) are operation counts with no machine model and are left out.
• Corrections. The first expected-cost display on p. 157 has $+\,b\int_{-\infty}^0 z\,dF_{z_j}(z)$, which is negative. The formalization uses $b\,E[(z_j)^-]$, as in the book's next display.
• Pinnings. Lemma 3 is deterministic: the demands are arbitrary reals, and "in balance following the allocation" means that some $x_j \ge 0$ with $\sum_j x_j = \sum_j d_{j,t-1}$ exists. The critical-fractile milestone is the characterization "minimizer if and only if $\Phi(z) = b/(b+h)$" of the book's "can be found by setting".
• Trivialization ruled out. The allocation problem (7.22) is defined independently of the algorithm, as a minimum over explicit integer allocations, and the $\tilde C_m$ are built from the data by (7.19)–(7.21). Neither (7.22) nor the $\tilde C_m$ are defined as, or required to agree with, what AllocOpt returns.
• Welcome contributions. Lemmas on the invariants of AllocOpt, in particular that after each outer step the allocation $r^*$ is feasible for $r^0_n$ with cost $z$ and all slopes to the left of $n^*(m)$ are at most those to the right. Also Gaussian sum lemmas over finite index sets and a general newsvendor first-order characterization.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005. DOI 10.1007/b138879
• G. D. Eppen and L. Schrage, "Centralized ordering policies in a multi-warehouse system with lead times and random demand", in L. B. Schwarz (ed.), Multi-Level Production/Inventory Control Systems: Theory and Practice, Studies in the Management Sciences, North-Holland, Amsterdam, 1981, pp. 51–67.
• G. D. Eppen, "Effects of centralization on expected costs in a multi-location newsboy problem", Management Science 25(5), 1979, 498–501. DOI 10.1287/mnsc.25.5.498
• B. Fox, "Discrete optimization via marginal analysis", Management Science 13(3), 1966, 210–216. DOI 10.1287/mnsc.13.3.210
• T. Ibaraki and N. Katoh, Resource Allocation Problems: Algorithmic Approaches, MIT Press, 1988.

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

A stocking point that reviews its inventory once per period and must decide how much to order is the basic unit of every service parts supply chain: each warehouse, each repair depot and each forward location in the networks studied later in Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) faces this decision for thousands of items. The practical rule used everywhere is the order-up-to (base-stock) rule: bring the inventory position up to a fixed target level whenever it falls below it, and order nothing otherwise. Chapter 2 of the book justifies this rule for a single item with linear costs, following the dynamic-programming argument of Karlin and Scarf, and the rest of the book takes the rule as given.

Timeline. Arrow, Harris and Marschak posed the periodic-review inventory problem as a dynamic program in 1951 (Econometrica). Bellman, Glicksberg and Gross showed in 1955 that with linear ordering cost and convex expected holding and shortage costs the optimal policy has a critical-number form (Management Science). Karlin and Scarf (1958) extended the analysis to a positive lead time, the setting of the book's Theorems 1–3. Veinott (1965) gave conditions under which a base-stock policy is optimal in multi-product, nonstationary models (Management Science).

Setting

One item is stocked at one location. At the start of each period the inventory position $y$ is observed and a quantity $u \ge 0$ is ordered; with lead time one period it arrives at the start of the next period. Demand in each period is independent of other periods and has a density $g$ on $(0,\infty)$ that is positive and continuous. Unmet demand is backordered. Costs are linear: $c$ per unit ordered, $h$ per unit on hand at the end of a period, $b$ per unit backordered at the end of a period, and future costs are discounted by $\alpha \in (0,1)$. The one-period cost is

$$L(y) = \begin{cases} h\displaystyle\int_0^y (y-x)g(x)\,dx + b\int_y^\infty (x-y)g(x)\,dx, & y > 0,\\[1mm] b\displaystyle\int_0^\infty (x-y)g(x)\,dx, & y \le 0. \end{cases}$$

The book assumes throughout that $b > \frac{1-\alpha}{\alpha}\,c$: the backorder cost outweighs the saving from deferring a purchase.

The $n$-period value functions are $f_1 = L$ and, for $n \ge 2$,

$$f_n(y) = \min_{u \ge 0}\Big\{ c\,u + L(y) + \alpha\int_0^\infty f_{n-1}(y+u-x)\,g(x)\,dx \Big\}.$$

An order $u$ is optimal at $y$ if it attains this minimum over all $u \ge 0$. The order-up-to rule with level $s$ orders $u(y) = \max\{0, s-y\}$. The marginal function of eq. (2.8) is $F_n(w) = c + \alpha\int_0^\infty f_n'(w-x)\,g(x)\,dx$. In Lean these are Model, Model.L, Model.f, Model.IsOptimalOrder, Model.IsOrderUpToOptimal and Model.F in the namespace ServiceParts.BaseStock.

Formalization targets

Goal: Theorem 2 (p. 18) in its $n$-period form

For every horizon $n \ge 2$, either there is a real level $s_n^*$ with

$$u_n^*(y) = \max\{0,\ s_n^* - y\} \ \text{optimal for every } y,$$

or ordering nothing is optimal for every $y$ (level $-\infty$); and there is $N \ge 2$ such that the level is real for all $n \ge N$. No value of $s_n^*$ is fixed: the goal asserts the shape of the optimal policy only.

Milestones, in attack order

1. $L$ is convex (p. 21).
2. Every $f_n$, $n \ge 1$, is convex (p. 19, property (c)).
3. Every $f_n$ is differentiable with $-(c+b) \le f_n' \le h/(1-\alpha)$ (p. 20).
4. Property (b): given an optimal real level $s$ for horizon $n \ge 2$, $f_n' = -c + L'$ below $s$ and $f_n' = L' + \alpha\int_0^\infty f_{n-1}'(\cdot - x)g(x)\,dx$ from $s$ on (p. 19).
5. Given such a level, $F_n(w) \to (1-\alpha)c - b\alpha < 0$ as $w \to -\infty$ (p. 19).
6. Property (a): optimal real levels are nondecreasing in the horizon, $s_n^* \le s_{n+1}^*$ (p. 18).

Significance

The theorem reduces an infinite-dimensional control problem, a choice of order quantity for every possible inventory position, to one number per period. Every later chapter of the book (Palm's theorem for $(s-1,s)$ policies, METRIC-type stock level optimization, allocation in multi-echelon systems) parameterizes policies by such stock levels; this is where the book justifies that parameterization.

The result is classical and proved in many texts. On Prove2Me the mission produces a machine-checked finite-horizon version with a continuous demand density, including the calculus the proof needs: convexity of an expected cost defined by integrals against a density, differentiation under the integral sign in the recursion, and the one-sided behaviour of the value function at the order-up-to level. Existing platform results on base-stock optimality (Veinott's multi-product model, advance demand information) use different models and different arguments; none covers this recursion.

Difficulty

The argument is an induction on $n$ whose hypothesis carries convexity, the derivative formula (b), and bounds on $f_n'$. The delicate step is the existence of a finite root of $F_n$: its limit at $-\infty$ depends on whether the previous level was finite. For $n = 1$ nothing is ordered and the limit is $c - b\alpha$, which the assumption $b > \frac{1-\alpha}{\alpha}c$ does not make negative. The book's base case ("left to the reader") therefore fails when $c > \alpha b$: with $\alpha = \tfrac12$, $c = 1$, $b = \tfrac32$ the two-period problem never orders. The goal is corrected accordingly.

Two properties the book's induction also carries are not usable as printed. Property (d), $f_n' \le f_{n-1}'$, is false: for large $y$, $f_n'(y)$ approaches $h(1 + \alpha + \dots + \alpha^{n-1})$, which increases with $n$. The second-derivative clause of property (c) fails at $y = 0$ whenever $g(0^+) > 0$. A solver cannot follow the printed induction step for step; property (a), which the book derives from (d), is true and is a milestone in its own right.

Formalization scope

• Horizon. The book states Theorem 2 for "the optimal policy" without a horizon. Its proof is an induction on a finite horizon, and the passage $n \to \infty$ is left as a conjecture (p. 21). The goal is the finite-horizon theorem; no infinite-horizon value function is constructed.
• Lead time. The proof sets $\tau = 1$ "to simplify notation"; so does the formalization. Theorem 1 (dependence on the inventory position only) and Theorem 3 (general $\tau$, whose level equation is the conjectured infinite-horizon one) are not stated.
• Level $-\infty$. The goal allows "never order" as the order-up-to rule with level $-\infty$ and adds eventual finiteness; see Difficulty.
• Added hypotheses. $c \ge 0$, $h > 0$ (the book uses $\lim_{w\to\infty} f_n'(w - x) > 0$), $0 < \alpha$ (the book divides by $\alpha$), and a finite mean $\int_0^\infty x\,g(x)\,dx < \infty$ (without it $L$ is infinite). All are fields of Model, together with positivity and continuity of $g$ on $(0,\infty)$, $\int_0^\infty g = 1$, and $b > \frac{1-\alpha}{\alpha}c$.
• Minimum and derivatives. $f_n$ is defined with the infimum over $u \ge 0$ of a nonnegative quantity; optimality is always against every $u' \ge 0$. Statements about $f_n'$ assert differentiability (Differentiable, HasDerivAt) and do not read deriv as evidence of it.
• Levels. The book's $s_n^*$ is "the unique solution of (2.6)"; milestones take any real level at which the order-up-to rule is optimal.

A recursion in which ordering is restricted to order-up-to rules, or in which $f_n$ is defined through $s_n^*$, would make the goal a tautology; here $f_n$ is defined by minimization over all $u \ge 0$ and optimality is checked against all orders.

Needed infrastructure: convexity and differentiation of parametric integrals against a density on $(0,\infty)$, and minimization of a differentiable convex function over a half-line. Both are reusable for the other stochastic inventory missions on the platform. Proofs of individual milestones are welcome independently of the goal.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 2, Section 2.1. https://doi.org/10.1007/b138879
• S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in K. J. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958 (no DOI).
• K. J. Arrow, T. Harris and J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906814
• R. Bellman, I. Glicksberg and O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
• A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206