Probability

Why time reversal matters

Functional limit theorems describe the behavior of entire time-indexed paths under scaling. In queueing and other stochastic models, a path of departures, workload, or accumulated input may be related to another path by reversing a finite observation window. To carry a limit theorem through that change of viewpoint, one needs to know how reversal acts on the topology of the path space. Ward Whitt's 1980 paper studies composition, reflection, first passage, and time reversal as maps that transfer functional limit theorems to derived processes (Whitt 1980).

The time-reversal result is a precise metric statement. Ordinary reversal preserves the Skorohod $J_1$ distance exactly. A version shifted to begin at the group identity satisfies a bound with constant two. These facts give continuity and, when the random paths satisfy the hypotheses, make reversal available to the continuous mapping theorem. Whitt's introduction explains how deterministic path continuity connects to stochastic-process limits (Whitt 1980, pp. 67–69).

Paths, distances, and reversal

Let $S$ be a complete separable metric group, written additively, with identity $0$ and metric $m$. The metric is translation invariant: moving both points by the same group element leaves their distance unchanged. Let $D$ contain the càdlàg paths $x:[0,1]\to S$, meaning paths that are right continuous and possess left limits. Section 8 additionally requires $x(1)=x(1-)$, so the terminal value agrees with the value approached from earlier times. Let $D_\theta=\{x\in D:x(0)=0\}$. These are the spaces Whitt fixes for time reversal (Whitt 1980, p. 83).

The uniform distance is $\rho(x,y)=\sup_{0\le t\le1}m(x(t),y(t))$. A time change $\lambda\in\Lambda$ is an increasing homeomorphism of $[0,1]$ onto itself; $e(t)=t$ is the identity time change. The $J_1$ distance used in the paper is

$$d(x,y)=\inf_{\lambda\in\Lambda} \max\{\rho(\lambda,e),\rho(x,y\circ\lambda)\}.$$

Two paths may be close when their values can be matched after a small distortion of time. This is the paper's equation (2.1), rather than an unspecified equivalent $J_1$ metric (Whitt 1980, p. 70).

The reverse-time map reads the left limit at the reflected time:

$$R(x)(t)= \begin{cases} x((1-t)-),&0\le t<1,\\ x(0),&t=1, \end{cases} \qquad r(x)(t)=R(x)(t)-x(1).$$

The left limit is essential: the direct value $x(1-t)$ places jumps on the wrong side and generally does not give a right-continuous reverse path. The terminal convention gives $R(x)(0)=x(1)$, so $r(x)(0)=0$. Whitt also uses the reflected time change $(-r)(\lambda)(t)=1-\lambda(1-t)$ in the proof (Whitt 1980, pp. 83–84).

Formalization targets

The goal is Whitt's Theorem 8.1. For every $x,y\in D$,

$$d(Rx,Ry)=d(x,y),\qquad d(rx,ry)\le 2d(x,y).$$

The second inequality also applies when both paths lie in $D_\theta$, since $D_\theta\subseteq D$. The constant is the paper's printed constant, not a parameter to optimize in this mission (Whitt 1980, Theorem 8.1, p. 83).

The milestones record four claims from the theorem's proof: reversal preserves its path spaces and has inverse behavior on its natural domains; reflected time changes stay in $\Lambda$; reversal obeys exact and bounded uniform-distance relations; and reversal interacts with time changes through $(-r)(\lambda)$. Their descriptions reproduce the printed proof sentences. The proof calls the time-change cost a “minimum” once, although equation (2.1) and the displayed calculation use a maximum. The formal target follows equation (2.1) (Whitt 1980, pp. 70, 84).

What the result gives

An isometry preserves every $J_1$ distance, so ordinary reversal preserves convergent and Cauchy sequences in this metric. The bound for $r$ makes shifted reversal Lipschitz and therefore continuous. A functional limit theorem for input paths can then be translated into one for the corresponding reversed paths whenever the path-space hypotheses hold. The result is already proved in Whitt's paper; the open work here is a machine-checked development of its definitions, supporting claims, and metric theorem.

Formalizing the result also creates reusable interfaces for endpoint-constrained càdlàg paths, left-limit reversal, uniform path distance, and reflected time changes. Those interfaces may support later statements about reversed stochastic models. This mission does not assert weak convergence of probability laws or Borel measurability; those would require a separate measurable-space development for $D$.

Mathematical difficulty

The immediate idea $t\mapsto x(1-t)$ does not preserve càdlàg paths at jumps: a right-continuous jump becomes left-continuous. The correction uses left limits, but endpoint behavior then matters. Without $x(1)=x(1-)$, the shifted reverse path need not start at the identity. The $J_1$ assertion also concerns an infimum over all allowed time changes, so a uniform-distance statement alone does not establish the theorem. These are the points at which reflection of the time axis becomes a claim about the precise path-space topology (Whitt 1980, pp. 83–84).

Formalization scope

Lean represents paths as total functions $\mathbb R\to S$; all path conditions, metrics, and equality claims read only $[0,1]$. Càdlàg membership requires right continuity and left limits within the interval, with $x(1)=x(1-)$ included in $D$. Completeness and separability are explicit because the paper calls $S$ a complete separable metric space. The additive metric group is represented by an additive commutative group with an explicit translation-invariance hypothesis. This chooses the commutative reading exemplified by $S=\mathbb R^k$; the paper uses additive notation but does not separately state commutativity.

The paper's $\Lambda$ is encoded by strict increase, continuity, and surjectivity on $[0,1]$, which characterize increasing homeomorphisms there. The paper's $d$ is equation (2.1) on both sides of the goal. Lean uses extended nonnegative distances for $\rho$ and $d$, avoiding the default value a real supremum can assign to an empty or unbounded set. The claims do not become trivial by dropping $D$ membership: it is an explicit hypothesis, and the zero path over $\mathbb R$ satisfies it. A local, sorry-free check confirms that instance. Two easier statements are excluded on purpose: the goal is stated for the $J_1$ distance $d$, not the uniform distance $\rho$, and $R$ reads the left limit $x((1-t)-)$, not the value $x(1-t)$.

The proof's first sentence says the maps are one-to-one and onto. The map $r:D\to D_\theta$ forgets an additive offset and is not injective on all of $D$; the formal milestone expresses involution for $R$ on $D$ and for the restriction of $r$ to $D_\theta$. One identity printed for $r$ with $x\in D_\theta$ also holds for every $x\in D$; the formal milestone uses that broader domain and says so in its item description. Contributions are welcome for the left-limit and time-change infrastructure as well as the four listed statements and the goal.

Selected references

• Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, pp. 67–85. DOI: 10.1287/moor.5.1.67.

Motivation

An airline sells the seats of one flight leg at several fares. Cheap fares are usually booked well before departure and expensive ones close to it, so every early request poses the same question: is the certain revenue of selling a seat now worth more than the chance of selling it later at a higher fare? The policy that answers it is seat inventory control, a core problem of airline revenue management.

For two fare classes the answer is Littlewood's rule (1972): accept a low-fare request as long as the low fare is at least the high fare times the probability that high-fare demand would fill the remaining seats. Belobaba (1987) extended it heuristically to several classes through expected marginal seat revenue (EMSR) protection levels, which are not optimal in general. Wollmer (Operations Research 40(1), 1992) solved the multi-class problem exactly under the assumption that the classes book in order of increasing fare: he showed that an optimal policy is described by one critical value per fare class, computed by a short recursion, and accepts a request precisely when the number of empty seats exceeds the critical value of its class. Brumelle and McGill (Operations Research 41(1), 1993) and later work on nested booking limits reached optimality of static protection levels by other routes.

Setting

There are $c \ge 2$ fare classes, numbered $1, \dots, c$ from the highest fare to the lowest, with fares

$$r_1 > r_2 > \cdots > r_c > 0 .$$

Class $m$ has a random demand $D_m \in \{0, 1, 2, \dots\}$, the number of its future booking requests, with probabilities $P[D_m = i]$, $P[D_m \ge n]$, $P[D_m \le i]$. Seats form one pool, and $n$ denotes the number of empty seats. Lower classes book first: all requests of class $m$ arrive before those of classes $1, \dots, m-1$. The paper assumes $r_2 < r_1 P[D_1 \ge 1]$, so that a class 2 request is refused when one seat remains.

The optimal value $Z_m(n)$ is the expected revenue under an optimal policy when $n$ seats are empty and only classes $1, \dots, m$ may still book. It satisfies $Z_0 \equiv 0$ and

$$Z_m(n) = \mathbb E\Big[\max_{0 \le x \le \min(D_m, n)} \big(r_m x + Z_{m-1}(n-x)\big)\Big],$$

where $x$ is the number of class-$m$ requests accepted. The marginal seat value is $\Delta Z_m(n) = Z_m(n) - Z_m(n-1)$ for $n \ge 1$, and the critical values are

$$k_1 = 0, \qquad k_m = \max\{\, n \ge 1 \mid r_m < \Delta Z_{m-1}(n) \,\} \quad (m > 1). \tag{2}$$

The critical-value rule for class $m$ rejects a class-$m$ request when $n \le k_m$ and accepts it when $n \ge k_m + 1$; it accepts $\min(D_m, (n-k_m)^+)$ of the class's requests.

Formalization targets

Goal: Theorem 2 with the rejection rule of §3

For every class $1 \le m \le c$, $\Delta Z_m(n)$ is nonincreasing in $n \ge 1$. For every class $2 \le m \le c$, the critical value $k_m$ exists, $Z_m(n) = Z_{m-1}(n)$ for $n \le k_m$, the critical-value rule attains the maximum in the recursion for $Z_m(n)$ (and accepting more requests is strictly worse), and for every $j \ge 1$

$$Z_m(k_m+j) = Z_m(k_m) + \sum_{i=0}^{j-1} \Big\{ \Delta Z_{m-1}(k_m+j-i)\,P[D_m \le i] + r_m\,P[D_m \ge i+1] \Big\}. \tag{6}$$

Milestones

1. Eq. (3): $Z_1(n) = r_1\{nP[D_1 \ge n] + \sum_{j=0}^{n-1} jP[D_1 = j]\}$.
2. Eq. (4): $\Delta Z_1(n) = r_1 P[D_1 \ge n]$, nonincreasing in $n$.
3. The note after (2b): if $\Delta Z_{m-1}$ is nonincreasing, then $r_m < \Delta Z_{m-1}(n)$ for $n \le k_m$ and $r_m \ge \Delta Z_{m-1}(n)$ for $n \ge k_m + 1$.
4. The rule of §3: if $\Delta Z_{m-1}$ is nonincreasing, rejecting class $m$ exactly when $n \le k_m$ is optimal, and $Z_m = Z_{m-1}$ on $n \le k_m$.
5. Lemma 1: the case $j = 1$ of (6) for class $\bar m + 1$, and $\Delta Z_{\bar m+1}(k_{\bar m+1}+1) < \Delta Z_{\bar m+1}(k_{\bar m+1})$.
6. The marginal display in the proof of Theorem 1: $\Delta Z_{\bar m+1}(k_{\bar m+1}+j) = \sum_{i<j} \Delta Z_{\bar m}(k_{\bar m+1}+j-i)P[D_{\bar m+1} = i] + r_{\bar m+1}P[D_{\bar m+1} \ge j]$.
7. Theorem 1: (6) for class $\bar m + 1$, and $\Delta Z_{\bar m+1}$ nonincreasing above $k_{\bar m+1}$.

Significance

The theorem reduces a dynamic program over all booking policies to one integer per fare class. The critical values are computed class by class from (2b) and (6), in a number of operations polynomial in the number of seats and classes, and the resulting policy is a nested booking limit that reservation systems can implement directly. The abstract states two further properties derived from it: the critical value decreases with the fare and is zero for the highest class.

The result is proved in the paper; it has no machine-checked proof. A complete formalization would give a verified account of the multi-class seat allocation problem with sequential booking, including the existence of the critical values, which the paper presupposes. The intermediate statements (the concavity-type property of $Z_m$ and the closed form (6)) are reusable for nested-booking-limit results in related models.

Difficulty

The induction of the paper is short, but it relies on one property: $\Delta Z_{m-1}$ must be nonincreasing for the threshold rule to be optimal for class $m$, and the threshold rule must be optimal for $\Delta Z_m$ to inherit the property. These two facts have to be carried together through the induction. The step at the threshold itself ($n = k_m + 1$) behaves differently from the rest: there the marginal value drops strictly, and the argument above the threshold needs the maximality in (2b), not monotonicity alone. The existence of $k_m$ is not argued on the page: it requires bounding the marginal seat value away from $r_m$ for large $n$ without assuming that demands have finite mean. The proofs of Lemma 1 and Theorem 1 also contain index slips ($k_{\bar m}$ printed for $k_{\bar m+1}$) that a formal proof must not reproduce.

Formalization scope

All statements live in the namespace LowerFareFirst.Critical and rest on one definition module, LowerFareFirst.Critical.Model. Classes are natural numbers starting at $1$; fares are a sequence $r : \mathbb N \to \mathbb R$ and demands a sequence of measurable maps $D : \mathbb N \to \Omega \to \mathbb N$ on a probability space $(\Omega, \mu)$, of which only the entries $1, \dots, c$ are constrained. Probabilities are μ.real of events.

Committed conventions:

• $Z_m$ is defined by the dynamic-programming recursion above, which is the reading of the paper's "expected revenue under an optimal policy". It is not the value of the critical-value policy and not defined by (6); either choice would make the goal definitional. Optimality of the rule is stated as attaining the maximum of the recursion for every realized demand.
• "Decreasing" means nonincreasing. The strict reading is false: $\Delta Z_1(n) = r_1 P[D_1 \ge n]$ is constant wherever $P[D_1 = n] = 0$.
• $k_m$ is the greatest element of $\{n \ge 1 \mid r_m < \Delta Z_{m-1}(n)\}$. Its existence is a conclusion of the goal, never a hypothesis; Lemma 1, Theorem 1 and the intermediate milestones take it as a hypothesis, as the page does.
• The standing assumptions of §1 are bundled in one predicate: probability measure, measurable demands, $c \ge 2$, strictly decreasing fares, $r_2 < r_1 P[D_1 \ge 1]$, and $r_c > 0$, an addition to the page: with $r_c \le 0$ and unbounded demand the maximum in (2b) need not exist.
• Independence of the demands is not assumed: the recursion uses only their marginal laws. For independent demands, the paper's setting, $Z_m$ is the optimal expected revenue.
• Where the proofs print $k_{\bar m}$ for $k_{\bar m+1}$, and where §3 says "class $m + 1$" for class $m$, the statements use the corrected index.

A complete development needs elementary facts about expectations of functions of an integer-valued random variable and finite maximization; nothing beyond Mathlib's measure theory. Proofs of any milestone are welcome, as are proofs of the abstract's remarks ($k_m$ nonincreasing in the fare) as separate theorems.

Selected references

• R. D. Wollmer, An Airline Seat Management Model for a Single Leg Route When Lower Fare Classes Book First, Operations Research 40(1), 26–37, 1992. https://doi.org/10.1287/opre.40.1.26
• K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• P. P. Belobaba, Airline Yield Management: An Overview of Seat Inventory Control, Transportation Science 21(2), 63–73, 1987. https://doi.org/10.1287/trsc.21.2.63
• S. L. Brumelle, J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1), 127–137, 1993. https://doi.org/10.1287/opre.41.1.127

Motivation

A binary classifier is learned from a sample of a distribution $P$ on $X \times \{-1, 1\}$, and its quality is measured by its excess classification risk over the Bayes classifier. Without assumptions on $P$ no learning method converges at a uniform rate, so every rate theorem rests on a condition that describes how hard $P$ is. Two such conditions are standard: Tsybakov's noise condition (Tsybakov 2004), which bounds the mass of the region where the label is close to a fair coin flip, and smoothness of the regression function $\eta(x) = P(y = 1 \mid x)$.

Steinwart and Scovel (arXiv:0708.1838v1, the reprint of Ann. Statist. 35 (2007) 575–607) analyse support vector machines with Gaussian RBF kernels. Their rates rest on a new condition, the geometric noise exponent, which measures how much of the weighted measure $|2\eta - 1|\,dP_X$ lies close to the decision boundary. It is tailored to the approximation properties of the Gaussian kernel and is less familiar than the classical conditions. Theorem 2.6 of the paper connects it to them: an envelope condition on $\eta$ near the decision boundary, together with a Tsybakov exponent, yields an explicit geometric noise exponent. This mission formalizes that theorem.

Setting

Let $X \subset \mathbb R^d$ be compact and let $P$ be a distribution on $X \times \{-1, 1\}$ with marginal $P_X$ and regression function $\eta(x) = P(y = 1 \mid x) \in [0, 1]$. The classes of $P$ are $X_{-1} = \{\eta < \tfrac12\}$, $X_1 = \{\eta > \tfrac12\}$ and $X_0 = \{\eta = \tfrac12\}$, all intersected with $X$. The distance to the decision boundary is

$$\tau_x = d(x, X_0 \cup X_1) \text{ on } X_{-1}, \qquad \tau_x = d(x, X_0 \cup X_{-1}) \text{ on } X_1, \qquad \tau_x = 0 \text{ otherwise},$$

with $d(x, A)$ the Euclidean distance of $x$ to $A$ (equation (7), p. 7).

• Tsybakov noise exponent $q \in [0, \infty]$ (Definition 2.2, p. 6): for some $C > 0$ and all sufficiently small $t > 0$, $P_X(|2\eta - 1| \le t) \le C t^q$.
• Geometric noise exponent $\alpha > 0$ (Definition 2.3, p. 7): for some $C > 0$,

$$\int_X |2\eta(x) - 1|\, e^{-\tau_x^2/t}\, P_X(dx) \le C\, t^{\alpha d/2}, \qquad t > 0.$$

• Envelope of order $\gamma > 0$ (Definition 2.5, p. 8): for some $c_\gamma > 0$, $|2\eta(x) - 1| \le c_\gamma \tau_x^\gamma$ for $P_X$-almost all $x \in X$.

In Lean these are TsybakovNoise, GeometricNoise and Envelope, built on Tau, in the namespace FastRatesSVM.GeomNoise.

Formalization targets

Goal: Theorem 2.6 (p. 8)

If $P$ has an envelope of order $\gamma > 0$ and Tsybakov noise exponent $q \in [0, \infty)$, then

$$q \ge 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \frac{(q+1)\gamma}{d}, \qquad 0 \le q < 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \alpha \text{ for all } 0 < \alpha < \frac{(q+1)\gamma}{d}.$$

Both clauses are stated, as one conjunction.

Milestones

1. Display (33), pp. 18–19. Under the Tsybakov bound for all $s > 0$ with constant $C$ and the envelope bound with constant $c_\gamma$, for all $t > 0$ and $\tau \ge 0$:

$$\mathbb E_{P_X}\big(|2\eta - 1|\, e^{-\tau_x^2/t}\big) \le C\tau^{q+1} + \exp\big(-(\tau/c_\gamma)^{2/\gamma} t^{-1}\big).$$

2. The $\tau$-estimate, p. 19. With $\hat a = c_\gamma^{2/\gamma}(q+1)$, for all small $t > 0$ the equation $\tau^{q+1} = \exp(-(\tau/c_\gamma)^{2/\gamma}t^{-1})$ has a positive solution, and every positive solution satisfies $\tau \le (\hat a\gamma/2)^{\gamma/2}\,(t\ln\frac{1}{\hat a t})^{\gamma/2}$.
3. Theorem 2.6, case $0 \le q < 1$.
4. Theorem 2.6, case $q \ge 1$.

Significance

Theorem 2.6 makes the paper's learning rates usable under familiar assumptions. The main rate theorem of the paper (Theorem 2.8) is stated in terms of the geometric noise exponent; through Theorem 2.6 it becomes a rate in terms of a Tsybakov exponent and the order of an envelope, which is a Hölder-type behaviour of $\eta$ at the decision boundary. Example: with $d = 1$, $X = [-1, 1]$, $P_X$ uniform and $\eta(x) = (1 + x)/2$, the distribution has envelope order $1$ and Tsybakov exponent $1$, hence geometric noise exponent $2$.

The result is proved in the paper. As far as known, none of it is machine-checked: none of these noise conditions has a Lean formalization, on Prove2Me or in Mathlib. The mission produces the definitions themselves (the class decomposition, $\tau_x$ and the three noise conditions), which any later formalization of margin-based classification rates can import, and a formal proof of the implication. A companion mission of the same series formalizes the paper's rate theorem, which takes the geometric noise exponent as its hypothesis.

Difficulty

The case $0 \le q < 1$ is elementary once the right splitting level is chosen: the expectation is split at a level $\tau$ of $|2\eta - 1|$, and $\tau$ is then tuned to $t$. Tuning it requires the asymptotics of the solution of a transcendental equation. This yields every exponent below the critical value $(q+1)\gamma/d$, but not the critical value itself: a logarithmic factor is lost.

Reaching the critical exponent when $q \ge 1$ is the substantial step. The paper does it with Hölder's inequality for Lorentz spaces $L_{q,\infty}$ and $L_{q',1}$ and an estimate of a nonincreasing rearrangement (display (32)). Mathlib has neither Lorentz spaces nor nonincreasing rearrangements, so this part either builds that infrastructure or replaces it with a direct layer-cake argument against the distribution function of $|2\eta - 1|$. The obvious approach, the same splitting as for $q < 1$, does not work: it always loses the logarithm.

Formalization scope

• Representation of $P$. $P$ is given by $\mu = P_X$, a probability measure on EuclideanSpace ℝ (Fin d) with $\mu(X^c) = 0$, and a measurable version $\eta$ of the regression function with values in $[0,1]$ everywhere. Every Borel distribution on $X \times \{-1,1\}$ has this form, and the paper defines $\tau_x$ "for some choice of $\eta$".
• Pinned convention $d(x, \emptyset) := 0$. The paper leaves $d(x, \emptyset)$ undefined. Lean's Metric.infDist gives $0$. For Theorem 2.6 both readings give a true statement. Under the reading $\infty$, the companion statements Theorem 2.7 and Lemma 4.1 are false for a version of $\eta$ with an empty class. The convention is chosen for agreement with the companion mission.
• Integrals. All integrals are $[0,\infty]$-valued Lebesgue integrals of nonnegative integrands (lintegral), so a bound can never hold through a junk value of a non-integrable function.
• Added hypotheses. $d \ge 1$, because the exponent $(q+1)\gamma/d$ divides by $d$. In the second clause, $\alpha > 0$: this is the range of Definition 2.3, not a new restriction.
• Display (33). It is stated for every $q \ge 0$, where it holds verbatim, and for $t > 0$ (the page writes $t \ge 0$, but $t^{-1}$ is undefined at $0$). Its hypotheses are the all-$t$ form of (5), which by the remark on p. 6 is equivalent to Definition 2.2 for $q < \infty$ up to the constant, and (10) with its constant named. The page's equality that splits the integral is not stated separately.
• Printed slip. The proof on p. 19 ends "for the case $0 < q < 1$", while the statement covers $q = 0$. The milestone is stated for $0 \le q < 1$; the argument works verbatim at $q = 0$.
• Small $t$. In Definition 2.2, "sufficiently small" is a threshold $t_0 \in (0,1)$. The $\tau$-estimate has its threshold chosen before $t$ and $\tau$, and it also states the existence of a solution, which the page presupposes.
• No trivializing reading. The hypotheses are satisfiable: the example in Significance meets all of them. $\tau_x$ is not identically $0$ there, since it equals $|x|$. So the goal cannot hold vacuously.
• Not formalized. The Lorentz-space step (30) and the rearrangement estimate (32) are not milestones. Contributions of Lorentz quasi-norms or a layer-cake lemma are welcome as supporting theorems.

The source is arXiv:0708.1838v1, the reprint of the Annals article. Its printed page numbers equal the PDF page numbers, and every page cited here is that number.

Selected references

• I. Steinwart, C. Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 575–607, 2007. arXiv reprint: https://arxiv.org/abs/0708.1838 ; DOI: https://doi.org/10.1214/009053606000001226
• A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 135–166, 2004. https://doi.org/10.1214/aos/1079120131

Motivation

The newsvendor problem is the basic single-period inventory model: a decision maker orders $x$ units at unit cost $c$ before a random demand $D$ is observed, sells $\min(D, x)$ units at price $p$, and loses unsold units. Its optimal order is the critical fractile $x^* = F^{-1}(1 - c/p)$ of the demand distribution $F$. Laboratory experiments show that human subjects do not order $x^*$. Schweitzer and Cachon (Management Science 46(3), 2000) gave subjects uniform demand on $[0, 300]$ and found that the average order lay below $x^*$ for a high-margin product and above $x^*$ for a low-margin product: orders are pulled toward the center of the demand range.

Su (Manufacturing & Service Operations Management 10(4), 2008) explains this pattern with a model of bounded rationality: the decision maker does not pick the best order with certainty, but picks better orders more often, through a logit choice rule. This mission formalizes the first results of that paper, the case of uniform demand, where the logit order has an explicit law and the pull toward the center can be proved exactly. The source is the published MSOM 2008 article; all page numbers are its printed pages.

Setting

A decision maker with utility $u$ over an interval $S \subseteq \mathbb R$ and bounded-rationality parameter $\beta > 0$ makes a random choice $Y$ with the logit density

$$\psi(y) = \frac{e^{u(y)/\beta}}{\int_S e^{u(v)/\beta}\,dv}, \qquad y \in S,$$

and $\psi(y) = 0$ off $S$ (eq. (2), p. 571). Large $\beta$ means noisy choices; small $\beta$ concentrates the choice near the maximizer of $u$.

In the newsvendor problem the price $p$ and unit cost $c$ satisfy $0 < c < p$. Demand $D$ has density $f$ and distribution function $F$. The expected profit of ordering $x$ units is

$$\pi(x) = p\,\mathbb E\min(D, x) - c x \qquad \text{(eq. (3), p. 572)},$$

and the optimal solution $x^*$ is its maximizer. The behavioral solution $X^\flat$ is the logit choice with utility $u = \pi$ over the decision domain $S$, the smallest interval containing the support of $f$ (eq. (4), p. 572).

This mission takes uniform demand $D \sim U[a, b]$ with $b > a \ge 0$: $f = 1/(b-a)$ on $[a, b]$ and $S = [a, b]$. The midpoint of the demand range is $m = (a + b)/2$. Two parameters recur:

$$\mu = b - \frac{c}{p}(b - a), \qquad \sigma^2 = \beta\,\frac{b-a}{p}.$$

A truncated normal law on $[a, b]$ with parameters $\mu, \sigma^2$ has density proportional to $e^{-(x-\mu)^2/2\sigma^2}$ on $[a, b]$ and zero elsewhere (eq. (37), p. 586). Write $\phi$ and $\Phi$ for the standard normal density and distribution function.

Formalization targets

Goal: Proposition 3 (p. 577), midpoint bias

$$x^* > m \implies \mathbb E X^\flat < x^*, \qquad x^* < m \implies \mathbb E X^\flat > x^*.$$

The goal is stated for every $\beta > 0$ and every $0 < c < p$, with $x^*$ any maximizer of $\pi$ over $\mathbb R$; it fixes only the sign of the bias, not its size.

Milestones

1. Eq. (5), p. 572. On $[a, b]$, $\pi(x) = Ax^2 + Bx + C$ with $A = -p/(2(b-a))$, $B = pb/(b-a) - c$, $C = -pa^2/(2(b-a))$.
2. The optimum, pp. 572–573. $\pi$ is maximized over $\mathbb R$ exactly at $\mu$, and $F(\mu) = 1 - c/p$, so $x^* = F^{-1}(1 - c/p) = \mu$.
3. Proposition 1, pp. 572–573. The density of $X^\flat$ equals the truncated normal density on $[a,b]$ with parameters $\mu$ and $\sigma^2$.
4. Corollary 1, p. 573.

$$\mathbb E X^\flat = \mu - \sigma\,\frac{\phi((b-\mu)/\sigma) - \phi((a-\mu)/\sigma)}{\Phi((b-\mu)/\sigma) - \Phi((a-\mu)/\sigma)}. \qquad (8)$$

Significance

Proposition 3 gives a single mechanism, noise in the choice of the order, that produces both directions of the bias observed by Schweitzer and Cachon: under uniform demand, a high-profit product ($x^* > m$) is underordered on average and a low-profit product ($x^* < m$) is overordered. Proposition 1 gives the full law of the boundedly rational order, which is what makes the model testable: the paper fits the truncated normal law to experimental order data and estimates $\beta$ (§5). Corollary 1 is the closed-form mean used in that fit and in Proposition 3.

These results are proved in the paper by direct computation; none of them has a machine-checked proof. The mission adds a checked development of the continuous logit choice model on an interval, of the truncated normal law and its mean, and of the uniform-demand newsvendor profit, together with exact statements of what the paper's informal phrases mean (see Formalization scope).

Difficulty

Each step is elementary on paper, but the formal content sits in the integrals. Expected sales $\mathbb E\min(D, x)$ must be computed as a piecewise integral to obtain eq. (5), and the maximizer must be identified over all of $\mathbb R$, not only on $[a, b]$, which needs the profit outside the support as well. Proposition 1 is an identity between two normalized densities, so both normalizing integrals must be shown positive and finite. Corollary 1 requires the mean of a truncated Gaussian in terms of Mathlib's Gaussian density and distribution function, which is not in Mathlib. For Proposition 3, the natural shortcut "the mean of a truncated normal is $\mu$" is false whenever $\mu \ne m$, and it is exactly the asymmetry of the truncation that produces the bias.

Formalization scope

All quantities are real numbers, with the paper's standing assumptions as hypotheses: $b > a \ge 0$, $0 < c < p$ (the page states $p > c$; $c > 0$ is read so that $x^*$ lies inside $(a, b)$), and $\beta > 0$ (eq. (2) divides by $\beta$; $\beta = 0$, perfect rationality, is a limit, not a value of the formula). The decision domain is the closed interval $[a, b]$; the logit density is zero off it, and expectations are integrals over $\mathbb R$. The parameter $\sigma$ is the positive square root of $\beta(b-a)/p$, and $\phi$, $\Phi$ are Mathlib's gaussianPDFReal 0 1 and the distribution function of gaussianReal 0 1.

Corrections and readings relative to the printed text:

• Eq. (5) is stated for $x \in [a, b]$ only; outside it $\pi$ is linear.
• Proposition 1 says the truncated normal has "mean $\mu$ and variance $\sigma^2$"; these are the parameters before truncation (as in eq. (37)), and the statement is the equality of densities. The mean of $X^\flat$ is (8), not $\mu$.
• In Proposition 3, "$f$ constant over $[a, b]$" is read as uniform demand on $[a,b]$, as in its proof. The conclusions are inequalities on $\mathbb E X^\flat$, because the §6 preamble (p. 577) defines "overorders" and "underorders" with the inequalities swapped relative to the proof (p. 586); the formal statement follows the proof.

The optimal solution $x^*$ in the goal is a hypothesis that $x^*$ maximizes $\pi$ over $\mathbb R$, never a variable set to a closed form by fiat; milestone 2 shows the hypothesis is satisfiable and identifies $x^*$. No statement holds vacuously through a junk value: on $[a, b]$ with $a < b$ the logit normalizer is the integral of a continuous positive function over an interval of positive length, and the denominator of (8) is positive because $\sigma > 0$.

Reusable beyond this mission: the logit density on an interval, the truncated normal density, and its mean formula. Proofs of any milestone, and of the mean of a truncated normal law in general, are welcome.

Selected references

• X. Su, Bounded Rationality in Newsvendor Models, Manufacturing & Service Operations Management 10(4):566–589, 2008. https://doi.org/10.1287/msom.1070.0200
• M. E. Schweitzer, G. P. Cachon, Decision Bias in the Newsvendor Problem with a Known Demand Distribution: Experimental Evidence, Management Science 46(3):404–420, 2000. https://doi.org/10.1287/mnsc.46.3.404.12070

Motivation

A service system with several servers can use a larger fraction of its capacity than a single-server system while still giving customers an acceptable wait. The design question is how much unused capacity is needed as the number of servers grows. Ward Whitt's study begins with a factory manager deciding whether to put four machines in one work area. It uses queueing models to connect the number of machines, their utilization, and the delays customers experience. The proposed utilization rule, $(1-\rho)\sqrt{s}=\gamma$, keeps the unused fraction $1-\rho$ proportional to $1/\sqrt{s}$ as the number of servers $s$ changes (Whitt 1992, pp. 708–710).

The paper distinguishes the chance that a customer waits at all from the length of the wait once a delay occurs. That distinction matters when a staffing choice must control a long wait rather than merely the fraction of customers who wait. The exact $M/M/s$ result in §3.1 gives a benchmark for the paper's later approximations to more general arrival and service processes (Whitt 1992, pp. 719–720).

Setting

An $M/M/s$ queue has Poisson arrivals at rate $\lambda$, $s$ identical servers, independent exponential service times, unlimited waiting room, and first-come first-served service. Time is measured so that each server's service rate is one. The server utilization is $\rho=\lambda/s$. We consider $s\geq1$ and $0<\lambda<s$, so the queue has a stationary distribution. Let $p_n$ be the stationary probability that $n$ customers are in the system. Its state process is a birth–death process: arrivals occur at rate $\lambda$ and departures from state $n$ occur at rate $\min(n,s)$.

Let $W$ be an arriving customer's steady-state time in the queue before service begins. An arrival finding fewer than $s$ customers starts service at once. An arrival finding $s+j$ customers waits for $j+1$ service completions while all servers are occupied. In the formal model, the law of $W$ has an atom at zero of mass $\sum_{n<s}p_n$ and, for each $j\geq0$, a gamma component with shape $j+1$, rate $s$, and weight $p_{s+j}$. The arrival-state weights use the Poisson-arrivals-see-time-averages property. This construction represents the FCFS waiting time independently of any claim about its eventual conditional distribution.

For an event $W>0$ of positive probability, $\mathcal L(W\mid W>0)$ denotes the conditional waiting-time law. The paper calls a customer delayed exactly when $W>0$. The scale parameter $\gamma$ is defined by the utilization equation $(1-\rho)\sqrt{s}=\gamma$; because $\rho<1$, this equation makes $\gamma$ positive.

Formalization targets

The supporting target is the §3.1 statement that a delayed customer's waiting time is exponential with rate $s(1-\rho)$, equivalently with mean $1/[s(1-\rho)]$:

$$\mathcal L(W\mid W>0)=\operatorname{Exp}\bigl(s(1-\rho)\bigr).$$

The goal is Proposition 3.1 under the utilization equation. It records both the entire conditional tail and its mean, for every $x\geq0$:

$$\mathbb P(W>x\mid W>0)=e^{-\gamma\sqrt{s}\,x}, \qquad \mathbb E[W\mid W>0]=\frac{1}{\gamma\sqrt{s}}.$$

The goal also asserts $\mathbb P(W>0)>0$, so these conditional quantities are defined. The scan of Proposition 3.1 prints the exponent without $x$ and the mean denominator with $\sqrt2$; the statement here uses the values determined by the preceding exponential-law sentence and by the paragraph following the proposition (Whitt 1992, pp. 719–720).

Significance

The result gives an exact delay distribution for the Markovian multi-server system. With $s$ servers and the utilization equation held fixed, the conditional tail at any positive threshold and the mean wait of a delayed customer both depend on $s$ through $\gamma\sqrt{s}$. Thus the same rule that organizes the probability-of-delay discussion has a definite implication for customers who actually wait. It is also the exact comparison point for the paper's later, explicitly approximate analysis of general $G/G/s$ queues (Whitt 1992, §3.2).

Formalizing this result supplies a reusable representation of the stationary FCFS waiting-time law as a mixture of Erlang distributions, together with a precise connection between birth–death state probabilities and delay. The related platform items QueueingFundamentals.BirthDeath.mmc_steady_state and QueueingFundamentals.BirthDeath.erlang_c_formula state the stationary state probabilities and the probability of delay, respectively; both are open and neither states this waiting-time law. The open QueueingFundamentals.BirthDeath.halfin_whitt concerns the heavy-traffic limit for the $M/M/c$ case, a different target. The current result is known mathematically from Whitt's 1992 paper; this mission asks for its machine-checked proof in the specified model.

Difficulty

The conditional distribution is not immediate from an individual service time. A delayed arrival can encounter any queue length $s+j$, so its waiting time is a gamma law whose shape varies with $j$. The stationary probabilities provide the weights of infinitely many such components. Showing that this whole mixture has one exponential law requires a relation among the stationary tail probabilities and control of the infinite sum. The same mixture must have a well-defined first moment for the conditional mean formula.

Formalization scope

Lean uses a natural number $s\geq1$, a real arrival rate $0<\lambda<s$, and a real sequence $p_n$ satisfying the published QueueingFundamentals.BirthDeath.IsSteadyState predicate with constant birth rate $\lambda$ and death rate $\min(n,s)$. That predicate includes nonnegativity, total mass one, and the global balance equations. Its published definition is imported as a reference. Service rate is exactly one, as fixed in §2.1 of the paper. The conditional waiting-time law is a measure on real time, with a point mass at zero and a countable gamma mixture. The positive-time restriction of this measure expresses conditioning in the milestone; real measure values and an integral express the tail and mean in the goal.

The formal hypotheses spell out positive arrival rate, at least one server, and subcritical utilization. These make the stationary law and the positive exponential rate meaningful. The goal states positive delay probability before dividing by it. The waiting-time law is built from stationary queue lengths and service completions, rather than being defined as exponential; proving that it becomes exponential is the mathematical task. Solvers may develop reusable measure-mixture identities, stationary-tail facts, and gamma or exponential distribution results. The approximation formulas of §3.2 and the paper's numerical tables are outside this mission.

Selected references

• Ward Whitt, Understanding the Efficiency of Multi-Server Service Systems, Management Science 38(5):708–723, 1992. DOI: 10.1287/mnsc.38.5.708.

Motivation

A many-server queue has $N$ identical servers, a stream of arriving customers, and a buffer in which customers wait when every server is busy. It models call centres, hospital wards and server farms, and the regime of practical interest is the Halfin–Whitt or quality-and-efficiency-driven regime, in which the number of servers $N$ grows with the arrival rate $\lambda_N$ so that $\sqrt N(1-\lambda_N/N)\to\beta$: servers are almost fully used, yet only a vanishing fraction of customers waits.

• Halfin and Whitt (1981, Oper. Res. 29) identified the regime and proved a diffusion limit for exponential service times ($GI/M/N$).
• Puhalskii and Reiman (2000, Adv. Appl. Probab. 32) treated phase-type service distributions ($GI/PH/N$).
• Reed (2009, arXiv:0912.2837), the source of this mission, obtained the fluid and diffusion limits of the number in system for the $G/GI/N$ queue with a general service-time distribution, assuming only a finite mean. Its approach rests on a sample-path identity, the system equation (2.8), which writes the number in system of the $N$-server queue through quantities of an infinite-server queue fed by the same arrivals.

This mission formalizes that identity and the proposition that yields it.

Setting

Fix one realisation of the queue (Reed, §2, p. 6).

• There are $N$ servers. At time $0-$ there are $Q_0$ customers; the first $\min(Q_0,N)$ are in service, with residual service times $\tilde\eta_i$, and the other $(Q_0-N)^+$ wait.
• Customers then arrive at times $0\le\tau_1\le\tau_2\le\cdots$ (with $\tau_0=0$); the arrival process is $A(t)=\#\{i\ge1:\tau_i\le t\}$. Arrivals at time $0$ are counted in $A(0)$, so in general $Q(0)\ne Q_0$.
• The $i$-th customer to enter service after time $0-$ has service time $\eta_i$. Service is first come first served, so the first $(Q_0-N)^+$ of these are the initial waiting customers and the $i$-th arrival has service time $\eta_{(Q_0-N)^++i}$.
• $w_i\ge0$ is the waiting time of the $i$-th arrival and $\tilde w_i\ge0$ that of the initial customer $N+i$.
• $F$ is the service-time distribution, with tail $G=1-F$, and $F_0$ the residual service-time distribution, with tail $\bar F_0$; both are carried by $[0,\infty)$.

The number in system is (2.2):

$$Q(t)=\sum_{i=1}^{\min(Q_0,N)}1\{\tilde\eta_i>t\}+\sum_{i=1}^{(Q_0-N)^+}1\{\tilde w_i+\eta_i>t\}+\sum_{i=1}^{A(t)}1\{\tau_i+w_i+\eta_{(Q_0-N)^++i}>t\}.$$

Centring each indicator at its (conditional) mean produces the terms

$$W_0(t)=\sum_{i=1}^{\min(Q_0,N)}\big(1\{\tilde\eta_i>t\}-\bar F_0(t)\big),\qquad A_G(t)=\int_0^tG(t-s)\,dA(s),\qquad I(t)=\min(Q_0,N)\bar F_0(t)+(Q_0-N)^+G(t),$$

and $M_2(t)$, the analogous centred sum (2.5) over the customers who entered service after time $0-$. $A_G(t)$ is the conditional mean number in a $G/GI/\infty$ queue fed by the same arrivals.

A sample path is non-idling if for every $t\ge0$

$$(Q(t)-N)^+=\sum_{i=1}^{(Q_0-N)^+}1\{t<\tilde w_i\}+\sum_{i=1}^{A(t)}1\{\tau_i\le t<\tau_i+w_i\},$$

that is, the customers waiting at time $t$ are exactly those who have arrived and not yet entered service. This holds for every first-come-first-served $N$-server path that never idles a server while a customer waits; the paper uses it at the start of the proof of Proposition 2.1 (p. 8).

Formalization targets

Goal: the system equation (2.8), p. 9

For a non-idling sample path and every $t\ge 0$,

$$Q(t)=I(t)+W_0(t)+M_2(t)+A_G(t)+\int_0^t\big(Q(t-s)-N\big)^+\,dF(s).$$

Milestones

1. The first two equalities of the proof of Proposition 2.1 (p. 8): $\sum_{i\le A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)=\sum_{i\le A(t)}\int_0^\infty 1\{t-(\tau_i+w_i)<s\le t-\tau_i\}\,dF(s)$.
2. The "reverse argument" of the proof (p. 9): $\int_0^t\sum_{i\le(Q_0-N)^+}1\{\tilde w_i>t-s\}\,dF(s)=\sum_{i\le(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big)$.
3. Proposition 2.1 (p. 8): for a non-idling path and $t\ge0$,

$$\sum_{i=1}^{A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)=\int_0^t(Q(t-s)-N)^+\,dF(s)-\sum_{i=1}^{(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big).$$

4. The decomposition (2.7) (p. 7): $Q(t)=I(t)+W_0(t)+M_2(t)+A_G(t)+\sum_{i\le(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big)+\sum_{i\le A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)$.

Significance

The result. Equation (2.8) is the paper's starting point for both of its limit theorems. Writing $Q-N=x+\int_0^t(Q(t-s)-N)^+dF(s)$ with $x=I+W_0+M_2+A_G-N$ shows that the number in system is the image of the infinite-server quantities under the regulator map of the paper's §3, the unique solution of $z(t)=x(t)+\int_0^t(z(t-s)+a)^+dB(s)$. The fluid limit (Theorem 4.1, p. 12) and the diffusion limit (Theorem 5.1, p. 23) then follow from limit theorems for the infinite-server terms and the continuity of that map. Without (2.8), the $N$-server queue has no closed equation in terms of quantities whose limits are known.

Formalizing it. The identity is proved in the paper on pp. 7–9; to our knowledge it has not been machine-checked. This mission produces a sample-path model of the $G/GI/N$ queue (initial customers, arrivals, FCFS service order, waiting times) together with the decomposition of its number in system, reusable for other many-server results stated pathwise. The limit theorems 4.1 and 5.1 themselves are weak-convergence statements in the Skorohod space and are not part of this mission; the regulator map (Proposition 3.1) is the subject of a separate mission of this series.

Difficulty

The decomposition (2.7) is bookkeeping. The content is Proposition 2.1, which converts a sum over customers of tail differences into an integral, against $F$, of the number of waiting customers at earlier times. The step that needs care is the change of viewpoint from "customer $i$'s service time falls in a window of length $w_i$" to "customer $i$ is waiting at time $t-s$", after which the sum over customers must be recognised, at each time $t-s$, as the waiting count of the non-idling identity, with the arrivals counted up to $A(t-s)$ rather than $A(t)$. A second point is the treatment of an atom of $F$ at $0$: the half-open windows $(t-\tau_i-w_i,\,t-\tau_i]$ and the closed integration range $[0,t]$ must match, and $G(x)=1$ for $x<0$ is used whenever a customer is still waiting.

Formalization scope

• Paths are data, not random. A sample path is a structure holding $N$, $Q_0$ and the sequences $\tilde\eta,\eta,\tau,w,\tilde w:\mathbb N\to\mathbb R$, indexed from $1$ as in the paper. The arrival times are primary and $A(t)$ is their counting function; for a counting process with $A(0-)=0$ this is the same data as the paper's $\tau_i=\inf\{t\ge0:A(t)\ge i\}$. The encoding has infinitely many arrivals, finitely many in each bounded interval.
• Distributions are probability measures $\mu$ (for $F$) and $\mu_0$ (for $F_0$) on $\mathbb R$ with no mass on $(-\infty,0)$, and $G(x)=\mu((x,\infty))$ for every real $x$. The paper's i.i.d. assumptions and the mean-$1$ assumption on $F$ are not used by these pathwise identities and are omitted.
• Integrals $\int_0^t\cdot\,dF(s)$ are over the closed interval $[0,t]$, an atom of $F$ at $0$ included; $A_G(t)$, a Stieltjes integral against the counting measure of arrivals, is the finite sum $\sum_{i\le A(t)}G(t-\tau_i)$.
• Non-idling is a hypothesis on the sample path, exactly the identity displayed above. No hypothesis mentions (2.8), Proposition 2.1 or an integral against $F$, and $Q$ is not a free function: it is defined by (2.2). Integrability of $s\mapsto(Q(t-s)-N)^+$ is part of what must be proved, not assumed. The hypotheses are jointly satisfiable, so the goal is not vacuous.
• Needed infrastructure: finite sums, set integrals of indicator functions against a finite measure on $\mathbb R$, and the identity $G(a)-G(b)=\mu((a,b])$. All of it is in Mathlib.

Related platform items: WhittEfficiency.IS.* (the $M/G/\infty$ queue with Poisson arrivals, the infinite-server object behind $A_G$) and PalmQueueing.Palm.swiss_army_formula (a pathwise queueing identity of Palm calculus) are the nearest queueing results; neither is the object of this mission.

Selected references

• J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6), 2009, 2211–2269. arXiv:0912.2837v1. https://arxiv.org/abs/0912.2837 , https://doi.org/10.1214/09-AAP609
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29, 1981, 567–588. https://doi.org/10.1287/opre.29.3.567 (MR629195)
• A. A. Puhalskii and M. I. Reiman, The multiclass GI/PH/N queue in the Halfin–Whitt regime, Adv. Appl. Probab. 32, 2000, 564–595. https://mathscinet.ams.org/mathscinet-getitem?mr=1778580

Motivation

Assembly systems — components purchased from outside, assembled into subassemblies, and those into an end product facing random customer demand — are the standard model of material requirements planning under uncertainty. Rosling's paper (Oper. Res. 37(4), 1989) shows that, under a cost assumption, the optimal policies of such a system are those of an equivalent series system, so that the Clark–Scarf decomposition of serial systems (Clark and Scarf, 1960) applies to assembly systems.

The cost assumption of the main results requires every echelon holding cost to be positive. In §4 Rosling replaces it by a weaker Generalized Assumption (GA), which allows some echelon holding costs to be negative, and then argues with Theorem 4 that GA "covers all cases of practical interest for a long-run analysis". Part (i) of Theorem 4 is the first step of that argument: when GA(i) fails strictly for some item, the model is degenerate, because its minimal cost is $-\infty$. This mission formalizes that statement.

Setting

There are $N \ge 1$ items $1, \dots, N$; item $1$ is the end item. Every item $i \ge 2$ has exactly one immediate successor $s(i)$ with $1 \le s(i) < i$, and $s(1) = 0$, so the items form a tree rooted at the end item. Write $A(i)$ for the set of all successors of $i$, $B(i)$ for the set of all its predecessors, and $P(i)$ for its immediate predecessors. Item $i$ has a lead time $l_i \in \mathbb N$, and its total lead time is $M_0 = 0$, $M_i = l_i + \sum_{k\in A(i)} l_k$; the items are indexed so that $M_{i-1} \le M_i$.

Time runs in periods $t = 1, 2, \dots$. The demands $\xi_1, \xi_2, \dots$ for the end item are independent, identically distributed, nonnegative, with a density and a finite mean $\lambda > 0$. In period $t$ a policy chooses the echelon inventory positions after ordering $Y_{1t}, \dots, Y_{Nt}$ as functions of the demands already observed. The position before ordering is $X_{it} = Y_{i,t-1} - \xi_{t-1}$, and the echelon stock on hand after arrivals is $X^l_{it} = Y_{i,t-l_i} - \sum_{r=t-l_i}^{t-1}\xi_r$; positions referring to periods before $1$ are read off given initial data $x^0$. Problem P asks for a policy satisfying

$$X_{it} \le Y_{it} \le X^l_{kt}\qquad\text{for all } k\in P(i) \text{ and all } i,t \tag{3}$$

that minimizes

$$E\Big\{\sum_{t=1}^\infty \alpha^{t-1}\Big(\sum_{i=1}^N \alpha^{l_i} h_i Y_{it} + \alpha^{l_1}(p+H_1)\int_{Y_{1t}}^\infty(\xi - Y_{1t})\,\varphi_1^{l+1}(\xi)\,d\xi\Big)\Big\} + \text{constant}, \tag{2}$$

where $h_i$ is the echelon holding cost of item $i$, $p$ the backlogging cost, $H_1$ the installation holding cost of the end item, $\alpha$ the discount factor and $\varphi_1^{l+1}$ the density of the demand over $l_1 + 1$ periods.

The quantity of interest is the discounted echelon holding cost of item $i$ and its predecessors,

$$h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}}.$$

GA(i) asks it to be positive for every item.

Formalization targets

Goal: Theorem 4(i), p. 574

If for some item $i$

$$h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}} < 0,$$

then the minimal cost of Problem P is unbounded below: for every real $C$ there is a feasible policy whose cost is a real number less than $C$.

Milestones: the proof of Theorem 4(i), p. 578

1. The one-more-unit policy is feasible. Ordering extra units of every item $k$ of the subsystem $\{i\}\cup B(i)$ in period $M_m - M_k + 1$, where $M_m$ is the greatest total lead time in the subsystem, and holding them forever, preserves (3).
2. The total cost increase. For a non-end item $i$ and a policy of finite cost, $\delta$ extra units change the cost by exactly

$$\delta\,\alpha^{M_m - M_i}\,\frac{\alpha^{l_i}\big(h_i + \sum_{k\in B(i)} h_k\,\alpha^{-(M_{s(k)} - M_{s(i)})}\big)}{1-\alpha}.$$

Significance

Theorem 4(i) explains why the Generalized Assumption is the natural boundary of the theory: a strict violation of GA(i) makes Problem P meaningless, since no policy is optimal and the infimum is $-\infty$. Together with parts (ii) and (iii) of Theorem 4 it reduces every case of interest to systems satisfying GA, for which Rosling's series-system results apply. The quantity in the condition is the natural "net value of stockpiling" of a subsystem, and the same exchange — buy more of a subsystem early and hold it forever — is the basic perturbation behind many optimality arguments for multi-echelon systems.

The result is proved in the paper, in a few lines. To our knowledge neither Theorem 4 nor the assembly model of Problem P has been machine-checked. A formalization adds a precise statement of what "the minimal cost is unbounded below" means for a stochastic infinite-horizon problem with an extended-real cost, and the definitions of the assembly model — product tree, total lead times, echelon positions, history-dependent policies, constraint (3) and objective (2) — which other statements of the same paper need.

Difficulty

The algebra of the cost increase is a geometric series. The work lies elsewhere. First, the one-more-unit policy must be shown feasible for every item of the subsystem in every period, including the boundary items: the successor of $i$, whose constraint loosens, and predecessors with zero lead time. Second, the cost of a policy is an expectation of an infinite discounted sum whose terms have no sign; the cost increase can only be added to a cost that is finite, and the argument needs a feasible policy of finite cost to start from, which the paper takes for granted. Third, for the end item $i = 1$ the extra units also change the expected backlog term of (2), which the printed display omits, so the end item needs a separate bound.

Formalization scope

• Periods start at Lean index $k = 0$ with $k = t - 1$; the discount weight $\alpha^{t-1}$ is $\alpha^k$, and coordinate $j$ of a demand path is $\xi_{j+1}$. Items are natural numbers $1..N$.
• Demand is the product law (Measure.infinitePi) of a probability measure $\nu$ on $\mathbb R$ with $\nu((-\infty,0)) = 0$, $\nu \ll$ Lebesgue, $\nu$ integrable and $\int x\,d\nu > 0$.
• Policies are history-dependent and measurable; feasibility (3) holds almost surely.
• Initial data $x^0_i(s)$, $s \ge 1$, the echelon position of item $i$ at the start of period 1 ordered $s$ periods ago or earlier, are assumed well formed: nonincreasing in $s$, and $x^0_i(s) \le x^0_k(s + l_k)$ for $k \in P(i)$. The paper takes this for granted; it is what makes Problem P feasible.
• Cost is (2) without its policy-independent constant, as an extended real $E[\sum(\alpha^{t-1}c_t)^+] - E[\sum(\alpha^{t-1}c_t)^-]$.
• Added restriction: $0 < \alpha < 1$. The page allows $\alpha = 1$, where the average cost is minimized and is defined only through a limit recipe.
• No sign condition is imposed on $h_i$, $p$ or $H_1$; neither the Assumption nor GA is a hypothesis.

In the extended reals, $\top - \top = \bot$: a policy whose positive and negative cost parts are both infinite gets the value $-\infty$. The goal therefore asks for policies of real cost below every bound; a formalization that only exhibits a policy of cost $\bot$ would be trivially true and is ruled out. Milestone 2 is stated for $i \ge 2$, where the backlog term is unchanged.

Needed infrastructure: lower Lebesgue integrals of discounted sums under the infinite product measure, linearity of the cost under a deterministic perturbation, and the finiteness of the cost of the "never order" policy (whose decisions decrease linearly in the accumulated demand). Contributions of general lemmas on discounted costs of history-dependent policies under infinitePi are welcome and reusable.

Selected references

• K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818