Operations Research

Motivation

A retailer with a large catalogue but a limited display (a web page, a shelf, a search result) must decide which assortment of products to show each arriving customer. Customers choose among the displayed products or leave without buying, and the retailer does not know their preferences in advance; it learns them only from the purchases it observes. This is the MNL-Bandit problem of Agrawal, Avadhanula, Goyal and Zeevi (arXiv:1706.03880v2; Operations Research 67(5), 2019), in which customer choices follow the multinomial logit model, the workhorse of revenue management and marketing.

The same paper gives an epoch-based upper-confidence-bound policy whose regret is at most of order $\sqrt{NT\log NT}$ (its Theorem 1). This mission formalizes the matching lower bound, the paper's Theorem 2: under a constraint that at most $K$ products be displayed, no policy can have regret smaller than order $\sqrt{NT/K}$ on every instance. Lower bounds of this kind are what certify that an algorithm is near-optimal rather than merely good.

Timeline. The square-root lower bound for $N$-armed bandits goes back to Auer, Cesa-Bianchi, Freund and Schapire (2002), presented in the survey of Bubeck and Cesa-Bianchi (arXiv:1204.5721, 2012). Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013) minimized regret under MNL choice with explore-then-exploit policies, obtaining $O(N^2\log^2T)$ and $O(N\log T)$ bounds for instances whose best and second-best assortments are well separated. Agrawal et al. (2017–2019) proved the instance-independent $\Omega(\sqrt{NT/K})$ lower bound formalized here; Chen and Wang (2017) later obtained $\Omega(\sqrt{NT})$ when $K<N/4$.

Setting

There are $n$ products. An instance consists of a no-purchase weight $v_0>0$, attraction parameters $v_1,\dots,v_n$ with $0\le v_i\le v_0$, and revenues $r_i\in[0,1]$. At each period $t=1,\dots,T$ the seller offers an assortment $S_t\subseteq\{1,\dots,n\}$ and observes a choice $c_t\in S_t\cup\{0\}$, where $0$ means no purchase. Under the multinomial logit (MNL) model,

$$p_i(S)=\frac{v_i}{v_0+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

and choices are independent across periods given the offered sets. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i/(v_0+\sum_{j\in S}v_j)$.

A policy chooses $S_t$ from the past assortments and choices, possibly at random. It satisfies the $K$-cardinality constraint if $|S_t|\le K$ always. Its regret over $T$ periods is

$$\mathrm{Reg}_\pi(T,v)=\mathbb E_\pi\Big(\sum_{t=1}^{T}R(S^*,v)-R(S_t,v)\Big),$$

where $S^*$ maximizes $R(\cdot,v)$ over assortments of at most $K$ products.

A randomized instance is a probability distribution over instances with common known revenues and a common no-purchase weight; the regret against it is averaged over the hidden attraction parameters, the choices and the policy's randomization.

Formalization targets

Goal: Theorem 2 (p. 14)

There is an absolute constant $C>0$ such that for all $n\ge2$, $1\le K\le n$ and $T\ge n$ there is a finitely supported randomized instance, chosen before the policy, such that every policy $\pi$ respecting the $K$-cardinality constraint satisfies

$$\mathbb E_{v}\big[\mathrm{Reg}_\pi(T,v)\big]\ge C\sqrt{\frac{nT}{K}} .$$

The constant is not fixed; any positive value suffices.

Milestones

The paper proves Theorem 2 in two cases.

1. Lemma E.1 (p. 57): the Bernoulli divergence bound $\mathrm{kl}(\alpha,\alpha+\epsilon)\le 4\epsilon^2/\alpha$ in the direction used by Lemma E.2.
2. Lemma E.2 (p. 57): for a guessing algorithm on $N\ge12$ coins and $t\le N\alpha/(60\epsilon^2)$, at least $N/3$ hiding places $j$ of the biased coin have $\mathcal P_j(a_t=j)\le 1/2$.
3. Lemma 5.1 (p. 15): on the Bernoulli instance $I_{\mathrm{MAB}}$ with $\epsilon=\frac1{100}\sqrt{N\alpha/T}$, every online algorithm has expected regret at least $\epsilon T/6$.
4. Lemma E.4 (p. 60): one period of MNL feedback on the instance $\hat I_{\mathrm{MNL}}$, where $\epsilon=\sqrt{1/(32T)}$, has divergence at most $4\epsilon^2$.
5. Lemma E.5 (p. 61): over $T$ periods the two choice laws of that instance have divergence at most $4T\epsilon^2$.

Items 1–3 serve the case $K<n$, which the paper reduces to a multi-armed bandit through the instance $I_{\mathrm{MNL}}$ of Definition 5.2 ($NK$ products in $N$ groups of $K$, one hidden group with larger attraction). Items 4–5 serve the case $K=n$ through the two-point instance $\hat I_{\mathrm{MNL}}$ of Definition E.1.

Significance

The theorem shows that the $\sqrt{T}$ growth of regret in assortment learning cannot be improved, and that the dependence on the number of products is polynomial: when the display size $K$ is fixed, the UCB policy of the same paper is optimal up to logarithmic factors (Remark 4). It separates what learning under the MNL model costs from what the combinatorics of the assortment adds, and the reduction it uses, simulating an assortment algorithm inside a bandit algorithm, is reusable for other choice-model bandits.

The result is proved in the paper, with its proof in Appendix E. To our knowledge neither the theorem nor its lemmas have been machine-checked. A formal proof has to repair several printed slips: Lemma 5.1's hypotheses do not exclude $\alpha$ close to $1$, where the bound fails; the proof of Lemma E.2 uses a form of Pinsker's inequality with a wrong constant; Lemma E.1 states one direction of the divergence and computes the other; and the constants of the $K=N$ case do not match. The formal statements here carry the corrected hypotheses, each disclosed in its note.

Difficulty

The obvious argument fails at the reduction. The bandit lower bound is a statement about algorithms that pull one arm per round, while an assortment policy offers $K$ products at once and sees a choice among them. Transferring the bound requires simulating MNL feedback from Bernoulli coins (Algorithm 2 of the paper), whose loop has a random length, and then relating the regret of the simulated assortment algorithm over a random number of calls to the bandit regret over $T$ pulls. The paper does this in expectation, and the constants have to be tracked through the random horizon.

A second difficulty is that the lower bound must hold for every policy, including randomized ones, against a single randomized instance fixed in advance. Bounding the regret of each deterministic policy separately is not enough unless the instance does not depend on the policy, which the statement requires. The change-of-measure steps (Lemmas E.2 and E.5) need a chain rule for the divergence between laws of adaptively generated histories.

Formalization scope

Products, periods and arms are 0-based (Fin n); a choice is Option (Fin n) with none the no-purchase alternative. Histories have finite length $T$, laws of histories are explicit products of policy weights and MNL (or Bernoulli) probabilities, and every expectation is a finite sum, so no measurability or integrability side conditions arise. The no-purchase weight $v_0$ is explicit (Definition 5.2 has $v_0=K$). $R(S^*,v)$ is a maximum over the finite, nonempty family $\{S:|S|\le K\}$.

Policies are behavioural: at every history they give a probability vector over assortments, which by Kuhn's theorem covers the paper's admissible policies with external randomization. The randomized instance is a finite list of instances with nonnegative weights summing to one; every support point has the same revenues and no-purchase weight, which are known to the seller. The quantifiers are in the paper's order: the constant first, then $n,K,T$, then the randomized instance, then every policy. A formalization with the policy quantified before the instance, with $C=0$ allowed, with varying known revenues across hidden support points, or with only deterministic policies, would be weaker and is ruled out.

Hypotheses added to the printed statements: $n\ge2$ and $K\ge1$ in Theorem 2 (the claim fails for $n=1$ and $K=0$); $0<\alpha$, $0<\epsilon$, $\alpha+\epsilon\le3/4$ in Lemma E.1; $0<\alpha$, $0<\epsilon$, $2\alpha+\epsilon\le1$ in Lemma E.2; $0<\alpha$, $2\alpha+\epsilon\le1$, $T\ge1$ in Lemma 5.1. Lemmas E.4 and E.5 use Definition E.1's $\epsilon=\sqrt{1/(32T)}$, with $T\ge1$ and $n\ge2$ so the instance is defined. Lemma E.5 is stated, as in its proof, for deterministic policies.

The development reuses three published definitions: the MNL revenue ChoiceCDLP.MNL.mnlObjective, the Bernoulli divergence RegretBandits.Stochastic.klBern, and the discrete Kullback–Leibler divergence FoundationsRL.GeneralDM.klDivDiscrete (valued in $[0,\infty]$). Proved platform results useful to solvers include Pinsker's inequality (BanditAlgorithm.pinsker_inequality_total_variation), the Bernoulli bound $d(p,q)\le(q-p)^2/(p(2-p-q))$ (BanditAlgorithm.bernoulli_relative_entropy_le_sq_div_of_add_le_one) and a divergence decomposition for bandits. A chain rule for the divergence of finite adaptive histories, and a formal version of the simulation of Algorithm 2, would be reusable beyond this mission; both are welcome as supporting lemmas.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880 — DOI https://doi.org/10.1287/opre.2018.1832
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
• X. Chen, Y. Wang, A Note on a Tight Lower Bound for MNL-Bandit Assortment Selection Models, arXiv:1709.06109, 2017. https://arxiv.org/abs/1709.06109

Motivation

The (s, S) policy is the standard control rule for a single item reviewed periodically: when the inventory position reaches or drops below a reorder level $s$, order enough to bring it up to the order-up-to level $S$. Under a fixed ordering cost and fairly general holding and shortage costs, some (s, S) policy minimizes the long-run average cost among all policies (Veinott 1966). That makes computing the best (s, S) pair a routine subproblem in inventory software, in multi-echelon heuristics, and in textbooks.

Before 1991 the available methods searched a box of candidate pairs. Veinott and Wagner (1965) bounded the optimal $s$ and $S$ and compared policies within the bounds. Later methods (Johnson, Management Science 15, 1968; Bell, SIAM J. Applied Mathematics 18, 1970; Federgruen and Zipkin 1984) used policy iteration or partial enumeration. Zheng and Federgruen (1991) gave an exact search that walks a monotone staircase path through the $(s,S)$ grid, and showed it costs about as much as evaluating a single policy. The procedure is the one presented in standard inventory texts such as Zipkin's Foundations of Inventory Management (2000).

Setting

One-period demands $D$ are i.i.d. and integer valued, with $p_j=\Pr\{D=j\}$, $j\ge0$, and $p_0<1$. An order costs $K>0$. $G(y)$ is the one-period expected cost when a period starts at inventory position $y\in\mathbb Z$. The paper assumes only:

• $-G$ is unimodal: for some integer $m$, $G$ is nonincreasing on $y\le m$ and nondecreasing on $y\ge m$;
• $\lim_{|y|\to\infty}G(y)>\min_yG(y)+K$.

Write $y_1^*$ and $y_2^*$ for the smallest and largest minimizers of $G$. The renewal density $m$ and renewal function $M$ are

$$m(0)=(1-p_0)^{-1},\quad m(j)=\sum_{l=0}^{j}p_l\,m(j-l)\ (j\ge1),\qquad M(0)=0,\quad M(j)=M(j-1)+m(j-1).$$

For integers $s<S$, the long-run average cost of the (s, S) policy is

$$c(s,S)=\frac{K+\sum_{j=0}^{S-s-1}m(j)\,G(S-j)}{M(S-s)}.$$

A pair $(s,S)$ is an optimal policy if $c(s,S)\le c(s',S')$ for all integers $s'<S'$. The optimal cost $c^*$ is the value of any optimal policy. For fixed $S$, $s$ is an optimal reorder level if $c(s,S)\le c(s',S)$ for all $s'<S$.

The algorithm (§3, p. 659) starts at any minimizer $y^*$ of $G$.

• Step 0. Decrease $s$ from $y^*$ until $c(s,y^*)\le G(s)$. Set $S^0:=y^*$, $c^0:=c(s,S^0)$ and $S:=y^*+1$.
• Step 1. While $G(S)\le c^0$: if $c(s,S)<c^0$, set $S^0:=S$, increase $s$ while $c(s,S^0)\le G(s+1)$, and set $c^0:=c(s,S^0)$. In either case, $S:=S+1$.

Formalization targets

Goal: Theorem 1(a)

For every demand law with $p_0<1$, every $K>0$, every $G$ satisfying the two assumptions, and every minimizer $y^*$ of $G$, the algorithm terminates. On termination, with final values $s,S^0,c^0$,

$$c(s,S^0)\le c(s',S')\ \text{ for all integers } s'<S',\qquad c^0=c(s,S^0)=c^*.$$

Milestones

The milestones are the results the paper's justification of the algorithm (p. 659) rests on, in the order it uses them:

1. the weighted-average identity (6), $c(s-1,S)=\alpha_nc(s,S)+(1-\alpha_n)G(s)$ with $\alpha_n=M(n)/M(n+1)$ and $n=S-s$, and Lemma 0 on the comparisons it implies;
2. Lemma 1(a): a reorder level $s^0<y_1^*$ with $G(s^0)\ge c(s^0,S)\ge G(s^0+1)$ (condition (7)) is optimal for $S$;
3. Corollary 1, the stopping rule of Step 0;
4. Lemma 2(a)–(c), the bounds $y_2^*\le S^*$ and $S^*\le\bar S^*=\max\{y\ge y_2^*:G(y)\le c^*\}$, which give the stopping rule of Step 1;
5. Lemma 3(a), the single-comparison test for improvement, and Corollary 2(b) with Lemma 3(b), which justify the inner loop.

Significance

The result. Theorem 1(a) makes the exact optimum of the (s, S) problem as cheap to compute as the cost of one policy, for any $G$ with $-G$ unimodal. No convexity is needed, and lead times, random lead times of the Zipkin type, and linear purchase costs are allowed. Its bounds (Lemma 2) and the monotone staircase structure of the search also underlie later work on continuous review, discounting and approximation.

Formalizing it. The theorem is proved on paper. As far as we know, none of the results in this mission has a machine-checked proof: the platform's Veinott–Wagner items concern a different (discounted, convex) model. Formalizing it produces a verified correctness proof of a widely implemented algorithm, and checks the paper's lemmas at their edge cases. Two of the printed statements need repair: Lemma 1(b) and Lemma 3(a) (see the scope section).

Difficulty

Optimality is claimed over all pairs $s'<S'$, an infinite set, but the algorithm visits only a monotone path. The proof therefore has to show that every pair it skips is no better. For a fixed $S$, the skipped reorder levels are handled by the unimodality of $c(\cdot,S)$ (Lemma 1). The skipped order-up-to levels are handled by the one-comparison test of Lemma 3(a), and those above the stopping point by the bound of Lemma 2(b). An argument from joint convexity or joint unimodality of $c$ in $(s,S)$ is not available. The paper uses no structure of $c$ beyond what Lemmas 0–3 state, and these hold only under the side conditions written in them.

Lemma 2(b)'s printed proof leaves the class of (s, S) policies (it uses a randomized order-up-to level). The limit at $-\infty$ may be finite, so $\min_{s<S}c(s,S)$ need not be attained for every $S$. Lattice demands, for which $m$ vanishes somewhere, create ties between adjacent reorder levels. Each of these breaks a naive transcription of the paper's argument.

Formalization scope

• Levels $s,S,y$ are integers. Demand values are natural numbers, and the demand law is the published VeinottWagnerSS.RenewalCost.DemandDist with the extra hypothesis $p_0<1$. All costs are real.
• The cost is the ratio above. Equation (1) on p. 655 is misprinted as $M(S-s)K+\sum\cdots$, and the ratio is the form fixed by (3) and (5). The Lean value $c(s,S)$ for $s\ge S$ is a junk $0$, so every quantifier over reorder levels carries $s<S$.
• $m$ is defined by the solved recursion $m(j)=(1-p_0)^{-1}\sum_{l=1}^{j}p_l\,m(j-l)$ (p. 660), and $M(j)=\sum_{i<j}m(i)$.
• The growth assumption is encoded as: $G$ has a minimizer $y_0$ and $G(y)>G(y_0)+K$ for all but finitely many $y$. Under unimodality this is equivalent to the page's limit condition. It is not strengthened to $G\to+\infty$.
• Optimality is among (s, S) policies. That an (s, S) policy is optimal among all policies is Veinott (1966) and is neither stated nor used. $c^*$, $c^*(S)$, $y_i^*$, $\bar S^*$, $\bar S_c$ and $s'$ are never real infima: they are the cost of a given optimal pair, $\exists$-statements, or binders characterised as least or greatest elements.
• The algorithm is a step function on the state $(s,S,S^0,c^0,\text{phase})$ that keeps the paper's order of tests and its weak and strict inequalities. The run with $n$ steps returns an output only if the algorithm has terminated.
• Ruled out as trivializing: comparing only with the pairs the algorithm visits or with a bounded box; assuming termination, or a budget that returns the current state; assuming $G\to+\infty$; leaving $c(s,S)$ unguarded for $s\ge S$.
• Repaired statements. Lemma 3(a) is stated with condition (7) at $S^0$ as an extra hypothesis. With $s^0$ merely optimal it fails when $m$ has a zero: for $p=(1/5,0,1/5,3/5)$, $m(1)=0$ and adjacent reorder levels tie. The algorithm always has (7). Lemma 1(b), "an optimal reorder level satisfying (7) exists for every $S$", is false when $\lim_{y\to-\infty}G(y)$ is finite. An example is $D\equiv2$, $K=1$, $G(0)=5$, $G(y)=10-0.1\cdot2^{-|y|}$ ($y\neq0$), $S=1$, where no optimal reorder level exists. It is not posed here, and the goal does not depend on it.
• Not formalized: Theorem 1(b)–(c), the operation counts, which depend on a bookkeeping model described in words; Corollary 3, which the paper notes is not needed for the algorithm; and the variant for a general starting level $S_0$.
• Welcome contributions: general facts about the discrete renewal density ($m\ge0$, $M>0$), the identity (6), and lemmas on $c(\cdot,S)$ that are reusable for related (s, S) and (r, Q) work.

Selected references

• Y.-S. Zheng and A. Federgruen, Finding Optimal (s, S) Policies Is About As Simple As Evaluating a Single Policy, Operations Research 39(4):654–665, 1991. https://doi.org/10.1287/opre.39.4.654
• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM J. Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• A. Federgruen and P. Zipkin, An Efficient Algorithm for Computing Optimal (s, S) Policies, Operations Research 32(6):1268–1285, 1984. https://doi.org/10.1287/opre.32.6.1268
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Why arrival averages and time averages agree

Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.

Before 1982 the property had been proved under strong extra structure:

• Strauch (1970) proved an instantaneous version, at a fixed time point, which does not by itself give limit theorems.
• Wolff (1970) proved a limit theorem for a stationary observed process, using particular properties of its interaction with the Poisson stream.
• Stidham (1972) proved a limit theorem for regenerative processes, under restrictions on how regeneration points relate to the arrivals.
• Wolff (1982), the source of this mission, proved the limit theorem with no stationarity, regeneration or ergodicity at all. The only link assumed between system and arrivals is that the system does not anticipate future arrivals. The proof uses Watanabe's (1964) martingale characterization of the Poisson process.
• Melamed and Whitt (1990) recast the result as one instance of a general "arrivals see time averages" (ASTA) principle for arbitrary point processes.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. On it live a process $N=\{N(t),t\ge0\}$, the state of a system, with values in an arbitrary measurable space, and a Poisson process $A=\{A(t),t\ge0\}$ at rate $\lambda>0$, counting customer arrivals in $(0,t]$. The interaction between $A$ and $N$ is unspecified: arrivals may change the state.

Fix a set $B$ of states with $\{N(t)\in B\}\in\mathcal F$ for every $t\ge0$, and define

$$U(t)=\mathbf 1\{N(t)\in B\},\qquad V(t)=t^{-1}\int_0^tU(s)\,ds,\qquad Y(t)=\int_0^tU(s)\,dA(s),\qquad Z(t)=\frac{Y(t)}{A(t)}.$$

$V(t)$ is the fraction of time in $[0,t]$ that $N$ is in $B$. $Y(t)$ is the number of arrivals up to $t$ who find $N$ in $B$, and $Z(t)$ is the fraction of arrivals who do.

The paths of $U$ are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. $U$ is assumed jointly measurable in $(\omega,t)\in\Omega\times[0,\infty)$. The single structural assumption is the Lack of Anticipation Assumption (LAA):

for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ and $\{U(s),0\le s\le t\}$ are independent.

The paper's proof of (6) uses this independence for every event of $\mathcal F_t$, the σ-field generated by $\{A(s),U(s);0\le s\le t\}$. The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to $\mathcal F_t$: for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ is independent of $\mathcal F_t$. This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of $A$ and from the past of $U$ is not independence from their joint past.

Formalization targets

Goal: Theorem 1 (p. 225)

Under lack of anticipation (with respect to $\mathcal F_t$, see above), for every random variable $V(\infty)$,

$$V(t)\to V(\infty)\ \text{w.p. 1}\quad\Longleftrightarrow\quad Z(t)\to V(\infty)\ \text{w.p. 1},\qquad t\to\infty.$$

The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.

Milestones

The proof in §2 passes through the following statements, which form the milestone list:

1. (2), (3): $E\{Y(t)\}=\lambda tE\{V(t)\}=\lambda E\{\int_0^tU(s)\,ds\}$.
2. (6): $E\{Y(t+h)-Y(t)\mid\mathcal F_t\}=\lambda E\{\int_t^{t+h}U(s)\,ds\mid\mathcal F_t\}$.
3. Lemma 1: $R(t)=Y(t)-\lambda tV(t)$ is a martingale.
4. (7): the second-moment bound $E\{R^2(t)\}\le\lambda t+2\lambda^2t^2$.
5. (10): the grid strong law $R(nh)/n\to0$ w.p. 1.
6. (11): the pathwise interpolation bound between grid points.
7. Lemma 2: $R(t)/t\to0$ w.p. 1.
8. The strong law $A(t)/t\to\lambda$ for the Poisson process.

Companion: Theorem 2 (p. 228)

For a Poisson process with bounded, integrable rate $\lambda(t)$ and $\Lambda(t)/t\to\bar\lambda\in(0,\infty)$, where $\Lambda(t)=\int_0^t\lambda(s)\,ds$, the same equivalence holds with $V(t)$ replaced by the rate-weighted average $\bar V(t)=\Lambda(t)^{-1}\int_0^tU(s)\lambda(s)\,ds$. Display (12), $E\{Y(t)\}=\int_0^tE\{U(s)\}\lambda(s)\,ds$, is its analogue of (3).

Significance

Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).

The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:

• the strong law for the Poisson process;
• a strong law for square-integrable martingale differences;
• Stieltjes integration against a counting path.

Difficulty

The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of $A$ are independent of the past of $U$. The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.

On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, $U(t)=\mathbf 1\{A \text{ jumps at } t\}$ satisfies LAA with $V\equiv0$ but $Z\equiv1$. The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.

Formalization scope

• Time and paths. Time is $\mathbb R$, and every hypothesis concerns $t\ge0$ only. Processes are maps $\mathbb R\to\Omega\to(\cdot)$. A Poisson process with intensity function $\lambda(\cdot)$ is a counting process $A:\mathbb R\to\Omega\to\mathbb N$ with $A(0)=0$, every path non-decreasing and right-continuous, Poisson-distributed increments with mean $\int_s^t\lambda$, and independent increments over any finite increasing sequence of times. The constant-rate case is Theorem 1's setting.
• The averages. $Y(t)$ is encoded as $\sum_{k=1}^{A(t)}U(T_k)$ over the arrival epochs $T_k=\inf\{s\ge0:A(s)\ge k\}$, which is the Lebesgue–Stieltjes integral $\int_{(0,t]}U\,dA$ with multiplicities. $Z(t)=0$ when $A(t)=0$, and $V(0)=0$; limits do not see these values.
• The standing hypotheses. These are carried as binders of the goal: measurability of $\{N(t)\in B\}$ for $t\ge0$, path regularity w.p. 1 (left continuity at $t>0$, right limits at $t\ge0$), joint measurability on $\Omega\times[0,\infty)$, and lack of anticipation as independence of the σ-field of future increments of $A$ from $\mathcal F_t$. The milestones (2), (3), (7) and (11) need less: (2) and (3) are stated under the printed LAA, and (7) and (11) under no independence assumption at all.
• The limit and the expectations. $V(\infty)$ is an arbitrary function $\Omega\to\mathbb R$, shared by both sides of the equivalence. Expectations in the milestones come with integrability conclusions, or are lower integrals in $[0,\infty]$, so that no identity holds through Lean's junk value $0$ for non-integrable functions.
• Ruled out. A formalization in which $V(\infty)$ is quantified separately on each side, which loses "to the same limit". A goal that assumes Lemma 2, (3) or the strong law $A(t)/t\to\lambda$ as a hypothesis. A definition of $Y$ that counts distinct jump times and not arrivals.

Welcome contributions:

• a reusable Poisson-process library: the strong law, square moments, independence of increments from a past σ-field;
• a martingale strong law of Feller's type;
• Stieltjes sums against counting paths.

All of these are useful well beyond this mission.

Selected references

• R. W. Wolff, Poisson Arrivals See Time Averages, Operations Research 30(2):223–231, 1982. https://doi.org/10.1287/opre.30.2.223
• S. Watanabe, On discontinuous additive functionals and Lévy measures of a Markov process, Japanese Journal of Mathematics 34:53–70, 1964. https://doi.org/10.4099/jjm1924.34.0_53
• B. Melamed and W. Whitt, On arrivals that see time averages, Operations Research 38(1):156–172, 1990. https://doi.org/10.1287/opre.38.1.156
• P. Brémaud and J. Jacod, Processus ponctuels et martingales: résultats récents sur la modélisation et le filtrage, Advances in Applied Probability 9(2):362–416, 1977. https://doi.org/10.2307/1426091
• S. Stidham, Regenerative processes in the theory of queues, with applications to the alternating-priority queue, Advances in Applied Probability 4(3):542–577, 1972.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

Many iterative algorithms update only part of a vector at a time. In a parallel implementation, one processor may read a value written several rounds earlier by another processor. Random observations also perturb each update. John N. Tsitsiklis's 1994 paper gives conditions under which such an asynchronous stochastic iteration still converges. The paper develops the result to analyze Q-learning, where state-action values are revised from sampled costs and successor states. Its general theorem also applies to iterative fixed-point calculations beyond that application.

The central issue is that a processor can choose which component to update after seeing the past, and its input can be stale. A convergence theorem that presumes a fixed update schedule or current data would miss both features. The paper's Assumptions 1–3 describe when delays, sampling noise, and random step sizes remain compatible with almost-sure convergence. Assumption 5 gives a weighted maximum norm contraction for the iteration map. Theorem 3 combines these conditions into the target of this mission.

Setting

Fix a positive integer $n$ and write $x(t)\in\mathbb R^n$ for the vector after round $t\ge0$. Let $F:\mathbb R^n\to\mathbb R^n$ be the map whose fixed point the iteration seeks. For component $i$, the step size $\alpha_i(t)$ lies in $[0,1]$, the noise is $w_i(t)$, and $\tau^i_j(t)\le t$ is the time from which component $j$ was read. Thus $x^i(t)$ has coordinates $x_j(\tau^i_j(t))$. With $\alpha_i(t)=0$ when component $i$ is idle, all rounds obey the single update equation

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr).$$

All quantities live on a probability space with law $\mathsf P$. The increasing filtration $\mathcal F(t)$ represents information available when the step sizes and delays are selected, before the round's noise is observed. Assumption 1 says every timestamp $\tau^i_j(t)$ tends to infinity almost surely: no fixed old value remains in use forever. Assumption 2 makes the initial state, chosen step sizes, delays, and noise measurable at the specified times; the noise has conditional mean zero, and its conditional second moment is bounded by a deterministic affine function of the largest squared iterate seen so far. Assumption 3 requires, for each component, divergent total step size and a square-summable step-size sequence, with a deterministic bound on all squared partial sums.

For a vector $v$ with strictly positive coordinates, the weighted maximum norm is $\|z\|_v=\max_i |z_i|/v_i$. Assumption 5 provides $x^*\in\mathbb R^n$ and $\beta\in[0,1)$ such that $\|F(x)-x^*\|_v\le\beta\|x-x^*\|_v$ for every $x$. Assumption 6, used in the boundedness milestone, requires the related growth bound $\|F(x)\|_v\le\beta\|x\|_v+D$ for some real $D$. The weighted norm permits different component scales.

Formalization targets

Boundedness under a weighted growth bound

Theorem 1 is the main intermediate target. Under Assumptions 1, 2, 3, and 6, it asserts

$$\mathsf P\!\left(\exists M\in\mathbb R\;\forall t,i,\ |x_i(t)|\le M\right)=1.$$

The bound $M$ may depend on the sample path. Lemmas 1–3 of the paper are milestones in its analysis: a scalar noisy recursion converges, its tails become uniformly small, and the pathwise bounds in the contradiction step hold.

Almost-sure convergence under a weighted contraction

The goal is Theorem 3, under Assumptions 1, 2, 3, and 5:

$$\mathsf P\!\left(\lim_{t\to\infty}x(t)=x^*\right)=1.$$

This theorem does not assume bounded iterates or Assumption 6 separately. Its proof uses Theorem 1 after deriving the needed growth bound from the contraction condition. Lemma 8 is the remaining milestone, comparing the coordinate iterates to an auxiliary deterministic recursion and a noise tail.

Significance

The result gives a fixed-point convergence guarantee when coordinates update at different times, delays can vary, and update choices can depend on past observations. In the paper's Q-learning application, these features describe exploratory sampling and possible parallel computation with old state-action values. For discounted problems, the associated Q-learning map contracts in the maximum norm, so Theorem 3 supplies the convergence step once the stochastic assumptions are checked (Tsitsiklis 1994, §7).

The mathematical results were proved in 1994; this mission asks for machine-checked proofs of their formal statements. Its reusable output would include a model of asynchronous noisy iteration, a scalar martingale-noise convergence lemma with random conditional variance bounds, and a precise interface between weighted contractions and pathwise convergence. The goal and milestone theorem files are currently statements with proof holes, while the definition file compiles without one.

Difficulty

A coordinate's next value depends on a vector assembled from observations at several earlier times. A direct estimate against the current error therefore does not close: the stale coordinates can reflect larger past errors. The noise condition is also tied to the largest iterate seen so far, so a deterministic global variance bound is unavailable before boundedness has been established. These two dependencies make the ordinary synchronous contraction argument insufficient. The scalar noise result and the pathwise comparison lemmas isolate the conditions needed for the boundedness and convergence statements.

Formalization scope

Vectors are functions Fin n → ℝ, with $n>0$; the source labels coordinates $1,\ldots,n$, while Fin n starts at zero. Function order is componentwise. The model sets $\alpha_i(t)=0$ on idle rounds and uses the paper's unified update equation. It does not store the sets of update times separately. The delay values on idle rounds are left arbitrary because they do not affect the update; the source chooses the current time there. All step sizes lie in $[0,1]$, and all delays are at most the current time, on every sample path.

The probability law is a probability measure. The filtration consists of increasing sub-σ-algebras. The iterate sequence is explicitly assumed adapted in the main theorems, matching the paper's use of $x(t)$ and its running maximum as $\mathcal F(t)$-measurable random variables. Conditional moment assumptions use integral inequalities over measurable sets, allowing generalized conditional expectations when the noise need not have a finite unconditional second moment. The conditional upper bound is required nonnegative almost surely, as the original inequality entails. Divergence and square summability use partial sums, so a non-summable series cannot receive a default value.

The maximum norm is the finite supremum of coordinate absolute values, and the weighted norm divides by the strictly positive coordinates of $v$. Almost-sure boundedness means a path-dependent finite bound on every coordinate and time. Pathwise Lemmas 3 and 8 are stated on a retained sample path, with the auxiliary quantities and hypotheses established at their locations in the paper; Lemma 8 uses the proof's translated and rescaled coordinates. These conventions rule out an empty coordinate type, junk integrals, and a vacuous boundedness claim. Contributions to the stated lemmas, their probabilistic infrastructure, and the final convergence proof are within scope.

Selected references

• John N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. DOI: 10.1023/A:1022689125041.

Motivation

Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating $x \leftarrow x + \alpha\,(F(x) - x + w)$ with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).

Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping $F$: a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.

Setting

A mapping $F:\mathbb R^n\to\mathbb R^n$ with components $F_1,\dots,F_n$ is given, and the goal is to solve $F(x)=x$. Time is discrete, $t=0,1,2,\dots$. The iterate $x(t)\in\mathbb R^n$ evolves by

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr),\qquad x^i(t)=\bigl(x_1(\tau^i_1(t)),\dots,x_n(\tau^i_n(t))\bigr),$$

where $\alpha_i(t)\in[0,1]$ is a stepsize ($\alpha_i(t)=0$ when component $i$ is not updated), $w_i(t)$ is noise, and $0\le\tau^i_j(t)\le t$ are delays: the update of component $i$ may read component $j$ as it was at an earlier time. All quantities are random variables on a probability space $(\Omega,\mathcal F,P)$ with an increasing sequence of σ-fields $\{\mathcal F(t)\}$, the history up to the choice of the stepsizes at time $t$.

Vector inequalities are componentwise and $e$ is the vector of ones. The paper's assumptions are:

• Assumption 1: every delay index $\tau^i_j(t)$ tends to infinity, with probability 1.
• Assumption 2: $x(0)$, $\alpha_i(t)$, $\tau^i_j(t)$ are $\mathcal F(t)$-measurable and $w_i(t)$ is $\mathcal F(t+1)$-measurable; $E[w_i(t)\mid\mathcal F(t)]=0$; and $E[w_i^2(t)\mid\mathcal F(t)]\le A+B\max_j\max_{\tau\le t}|x_j(\tau)|^2$ for deterministic constants $A,B$.
• Assumption 3: $\sum_t\alpha_i(t)=\infty$ and $\sum_t\alpha_i^2(t)\le C$ with probability 1, for a deterministic $C$.
• Assumption 4: $F$ is monotone ($x\le y\Rightarrow F(x)\le F(y)$), continuous, has a unique fixed point $x^*$, and $F(x)-re\le F(x-re)\le F(x+re)\le F(x)+re$ for all $x$ and all $r>0$.

In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.

Formalization targets

Goal: Theorem 2 (p. 189)

Under Assumptions 1–4, if $x(t)$ is bounded with probability 1, then

$$\lim_{t\to\infty}x(t)=x^*\qquad\text{with probability 1.}$$

Boundedness is a hypothesis, not a conclusion: for monotone $F$ it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.

Milestones

1. Lemma 1 (p. 190): for a scalar recursion $W(t+1)=(1-\alpha(t))W(t)+\alpha(t)w(t)$ with martingale-difference noise whose conditional variance is bounded by an a.s. bounded $B(t)$, and stepsizes with $\sum\alpha=\infty$, $\sum\alpha^2\le C$, $W(t)\to0$ with probability 1.
2. Lemma 4 (p. 193): the sequences $U^{k+1}=(U^k+F(U^k))/2$, $U^0=x^*+re$, and $L^{k+1}=(L^k+F(L^k))/2$, $L^0=x^*-re$, satisfy $F(U^k)\le U^{k+1}\le U^k$ and $F(L^k)\ge L^{k+1}\ge L^k$.
3. Lemma 5 (p. 193): $U^k\to x^*$ and $L^k\to x^*$.
4. Lemma 6 (p. 194): on a sample path where $L^k\le x(t)\le U^k$ from time $t_k$ on and all delays exceed $t_k$ from time $t'_k$ on, $x_i(t)\le X_i(t)+W_i(t;t'_k)$, where $X_i$ relaxes from $U^k_i$ towards $F_i(U^k)$ and $W_i(t;t'_k)$ accumulates the noise from $t'_k$.
5. Lemma 7 (p. 195): under the choices of $\delta_k$ and $t''_k$ made on pp. 194–195, $x_i(t)\le U^{k+1}_i$ for all $t\ge t''_k$.

Significance

Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.

The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.

Difficulty

The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes $U^k,L^k$ to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.

Formalization scope

• Components are Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. $re$ is r • 1.
• The update is stated in the paper's unified form for every $t$, with $\alpha_i(t)=0$ off the update times; the update sets $T^i$ are not represented. The paper sets $\tau^i_j(t)=t$ off $T^i$; the formalization leaves $\tau^i_j(t)$ free there, which is more general. $\alpha_i(t)\in[0,1]$ and $\tau^i_j(t)\le t$ hold on every sample path.
• Conditional expectations are generalized, written with set integrals (CondMeanZero, CondSqLe): $\int_S w\,dP=0$ for every $\mathcal F(t)$-set $S$ on which $w$ is integrable, and $\int_S w^2\,dP\le\int_S g^+\,dP$ in $[0,\infty]$. Mathlib's condExp is not used: it is $0$ for non-integrable functions and would make the noise assumptions vacuous.
• Series conditions use partial sums (divergence to $+\infty$; every partial sum at most $C$), never tsum, which is $0$ for non-summable sequences. The constants $A,B,C$ are chosen before the almost-sure quantifier; the bound on $x(t)$ is chosen after it.
• The paper treats $x(t)$ as determined by $\mathcal F(t)$ and uses this implicitly; Theorem 2 assumes it explicitly (Adapted).
• Lemma 1 leaves $W(0)$ unconstrained, as on the page. Lemmas 4 and 5 hold for every $r>0$. Lemmas 6 and 7 are pathwise: they fix one sample path and take the induction's objects ($k$, $t_k$, $t'_k$, $t''_k$, $X$, $\delta_k$) as given with exactly the properties the paper has established for them; they are not existential statements about these times.
• A trivializing formalization (junk conditional expectations, tsum for the series, a deterministic bound on $x(t)$, or a second unrelated $x^*$) is ruled out by the choices above.

Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version $W(t;t_0)$), and lemmas on monotone maps satisfying (7).

Selected references

• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994) 185–202. https://doi.org/10.1023/A:1022689125041
• C. J. C. H. Watkins and P. Dayan, Q-learning, Machine Learning 8 (1992) 279–292. https://doi.org/10.1007/BF00992698
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994) 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://hdl.handle.net/1721.1/3719
• B. T. Poljak and Ya. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automation and Remote Control 34 (1973) 377–397.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

An assembly system must coordinate the production of components that meet at a common downstream item. A shortage of any required component can delay the finished product, while producing a component too early incurs holding cost. In Rosling's 1989 study, the central question is whether optimal decisions for such a tree can be understood using the simpler theory of a pure series inventory system. The paper proves an equivalence when the initial inventory positions are in a condition it calls long-run balance. That equivalence gives a precise route from an assembly network to serial inventory control without discarding its lead times or its discounted costs.

Setting

There are items $1,\ldots,N$ in a tree rooted at end item $1$. Every item $i>1$ has one immediate successor $s(i)<i$; one unit of each component is needed for an end unit. Let $l_i$ be the production or delivery lead time of item $i$. The total lead time $M_i$ is the sum of lead times on the path from $i$ to the end item, with $M_0=0$, and the equivalent lead time is $L_i=M_i-M_{i-1}$. Items are indexed so that $M_i$ is nondecreasing. These definitions and indexing conditions are in §§1–2 of the paper.

At the beginning of each period $t$, outstanding orders arrive, the controller chooses the post-order echelon position $Y_{it}$, and then demand $\xi_t$ for the end item occurs. The pre-order position is $X_{it}$, while $X^l_{kt}$ is the position of predecessor $k$ from orders old enough to arrive after its lead time. A decision is feasible when $X_{it}\le Y_{it}\le X^l_{kt}$ for every immediate predecessor $k$ of $i$. Decisions depend only on demands already observed. The demands are independent and identically distributed, nonnegative, and have a density and a finite positive mean.

The discounted Problem P charges echelon holding cost $h_i$ for item $i$ and a shortage coefficient $p+H_1$ for the end item. Its discount factor is $\alpha$. The objective is the expectation of the sum over periods of the holding charges and the expected end-item shortfall over $l_1+1$ demands, with a constant independent of the policy. The paper's Assumption requires every $h_i>0$ and $\sum_i h_i\alpha^{-M_{s(i)}}<p+H_1$. The system is in long-run balance in period $t$ when positions of adjacent items, compared at the same age relative to total lead time, satisfy equation (5):

$$X^{M_i-\mu}_{it}\le X^{M_{i+1}-\mu}_{i+1,t} \quad(1\le i<N,\ 0\le\mu<M_i).$$

Formalization targets

Equivalent series optimal policies

The equivalent series system has successor $i-1$, lead time $L_i$, the same demand law and shortage coefficient, and holding coefficient $h_i\alpha^{l_i-L_i}$. Theorem 2 states that its optimal policies and those of the assembly system agree when the assembly system is initially in long-run balance. In the formal statement, the first inclusion is unconditional; the reverse inclusion is conditional on Problem P attaining an optimum:

$$\operatorname{Opt}(P)\subseteq\operatorname{Opt}(P_{\mathrm{series}}), \qquad \operatorname{Opt}(P)\ne\varnothing \Longrightarrow \operatorname{Opt}(P_{\mathrm{series}})\subseteq\operatorname{Opt}(P).$$

The target includes Lemmas 1 and 2, Theorem 1, Corollary 1, and the cost identity displayed in the proof of Theorem 2. Lemma 1 limits excess production, Lemma 2 gives a production lower bound, Theorem 1 describes when long-run balance is reached and preserved, and Corollary 1 uses the adjacent series position in that result. Each is stated at the strength given on pp. 568–569 of the paper.

Significance

Theorem 2 identifies the same policy choices in a tree assembly problem and a series problem whose stages have modified lead times and holding coefficients. It makes the serial interpretation exact for initially balanced systems and supports the paper's later discussion of series-system calculations. The statement is an equivalence of optimal policies, rather than just an equality of numerical values, so both the feasible-policy comparison and the cost comparison matter.

The theorem and its supporting results are proved in the 1989 paper; they have not been machine-checked in this development. A complete formalization would supply a reusable account of finite-history inventory policies, random demand histories, echelon positions, and extended-real discounted objectives. The published serial model SupplyChainTheory_multiechelon represents a different stage-indexed system; the assembly tree, its initial pipeline, and Problem P still need their own definitions. The paper's order-up-to Corollary 2 relies on an extension of earlier serial results and is outside this target.

Difficulty

The first natural comparison is to replace the tree's predecessor constraints with adjacent-item constraints. Those feasible sets are not equal for arbitrary states: positions at different total lead times can cross, and initial orders placed before period 1 affect the earliest periods. Long-run balance controls the necessary position comparisons, but equation (5) is empty for an item with $M_i=0$. The printed proof also uses a middle inequality outside the range covered by equation (5) when an equivalent lead time vanishes. A faithful statement must account for these boundary cases without defining the series problem through the assembly problem's optimal policies.

Formalization scope

Items use the paper's indices $1,\ldots,N$, with $N\ge1$ and $s(1)=0$. Lean period $k$ is paper period $t=k+1$; the policy sees exactly $k$ earlier demands. The common demand law $\nu$ is a probability measure on the reals, concentrated on nonnegative values, absolutely continuous with respect to Lebesgue measure, integrable, and of positive mean. The law of demand over $l_1+1$ periods is the pushforward of a finite product law under summation. Feasibility and the optimal-policy bounds are almost-sure statements, so changes on null histories do not alter them. Pathwise balance results quantify over one nonnegative demand path.

Initial positions include the orders placed before period 1. Their ages are monotone and obey the predecessor constraints inherited from that past. In addition to the paper's initial long-run balance, a separate boundary condition carries the missing comparison when $M_i=0$. Discounting is restricted to $0<\alpha<1$: at $\alpha=1$ the paper specifies average cost through a separate limiting prescription. The formal cost lies in the extended reals and is computed from its positive and negative parts; under the Assumption, feasible policies have a finite negative part. The policy-independent constant of equation (2) is omitted from both systems. “Optimal” means feasible and no more costly than every feasible policy, never a default value of an empty infimum.

The series system is built as a second instance of the same model, using the paper's successor, lead-time, and holding-coefficient transformations. Its cost and constraint (3) are then computed by the shared definitions. Contributions toward the lead-time identities, almost-sure policy comparisons, finite-time balance theorem, and extended-real cost identity are all part of the scope.

Selected references

• Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. DOI: 10.1287/opre.37.4.565.

Motivation

Spare-parts provisioning for repairable ("recoverable") items is a classical inventory problem: aircraft components fail, are sent to repair, and a stock of spares covers the units in the repair pipeline. Sherbrooke's METRIC model (Sherbrooke 1968), developed at RAND for the U.S. Air Force, measures the performance of a stock level by the expected number of backorders, the average number of unfilled demands outstanding at a random time. Every allocation computed by METRIC is driven by this quantity, and in particular by how it depends on the mean demand of each item.

For a new item that mean is not known. Air Force practice at the time produced a single engineering estimate of mean demand and computed backorders from it as if it were exact. In the section Demand Prediction (pp. 138–139) Sherbrooke argues that this practice is biased in one direction: under Poisson demand and any positive spare stock, the point estimate always understates expected backorders whenever the true mean is genuinely uncertain. This is his reason why a Bayesian treatment of demand is "of fundamental importance for all items, not merely low-demand items". The mission formalizes that claim and the computation behind it.

Setting

Fix one item. Its spare stock $s \in \{0, 1, 2, \dots\}$ is stock on hand plus on order plus in repair, minus backorders; under one-for-one replenishment it is constant. Let the number of units in resupply at a random time be Poisson distributed with mean $\lambda > 0$:

$$p(x \mid \lambda) = e^{-\lambda}\frac{\lambda^x}{x!}, \qquad x = 0, 1, 2, \dots$$

The expected backorders at spare stock $s$ are, by the paper's eq. (2),

$$B(s \mid \lambda) = \sum_{x=s+1}^{\infty} (x - s)\, p(x \mid \lambda).$$

In eq. (2) the mean is $\lambda T$ (customer rate times mean resupply time); on p. 138 it is the mean demand over a unit time interval. Only the mean enters, so it is written as one parameter $\lambda$. In Lean this is SherbrookeMetric.PointEstimate.backorders s lam, built on the published Poisson probabilities ServiceParts.StockLevels.poissonPmf.

Uncertain mean demand. The true mean takes the values $\lambda_k > 0$, $k \in K$ ($K$ finite), with probabilities $w_k \ge 0$, $\sum_k w_k = 1$. The point estimate is the mean of this distribution, $\bar\lambda = \sum_k w_k \lambda_k$, and the expected backorders accounting for the uncertainty are $\sum_k w_k B(s \mid \lambda_k)$. The paper's example (p. 138) takes $\lambda \in \{0.5, 1.5\}$ with probability $0.5$ each, so $\bar\lambda = 1$; its procedure (p. 139) discretizes a gamma prior to five to ten values.

Formalization targets

Goal: the point estimate understates backorders (pp. 138–139)

If two distinct values $\lambda_k \ne \lambda_{k'}$ both carry positive probability, then for every spare stock $s \ge 1$

$$B(s \mid \bar\lambda) < \sum_k w_k\, B(s \mid \lambda_k),$$

and for $s = 0$ the two sides are equal for every prior. The goal fixes no constants and no particular prior.

Milestones

1. Eq. (10), p. 139: for $\lambda > 0$, $B(s \mid \cdot)$ is twice differentiable at $\lambda$ with

$$\frac{\partial^2 B(s \mid \lambda)}{\partial\lambda^2} = \frac{e^{-\lambda}\lambda^{s-1}}{(s-1)!} > 0 \quad (s \ge 1),$$

and second derivative $0$ for $s = 0$. 2. Strict convexity, p. 139: for $s \ge 1$, $\lambda \mapsto B(s \mid \lambda)$ is strictly convex on $(0, \infty)$. 3. The worked example, p. 138 (off the goal's path): $B(2 \mid 1) = 3e^{-1} - 1 \approx 0.1036$ and $0.5\,B(2 \mid 0.5) + 0.5\,B(2 \mid 1.5) \approx 0.1486$.

Significance

The result. Expected backorders are the objective METRIC minimizes, item by item, subject to a budget. If the objective is evaluated at a point estimate, every item with uncertain demand looks better stocked than it is, and since the size of the error varies by item, the marginal comparisons that drive the allocation are distorted. The inequality is the quantitative statement behind the paper's recommendation to compute backorders as a posterior mixture over possible mean demands. It also says that an underestimate of demand costs more than an overestimate of the same size when backorders are the objective. For $s = 0$ the bias vanishes because $B(0 \mid \lambda) = \lambda$ is linear.

Formalizing it. The paper proves the statement in one line ("it is easy to show") by differentiating twice. No machine-checked version exists. A formal proof needs termwise differentiation of the Poisson backorder series, a closed form for its second derivative, and the passage from a positive second derivative to strict convexity and then to a strict finite Jensen inequality under a nondegenerate prior. The resulting facts about $\lambda \mapsto B(s \mid \lambda)$ are reusable in any Poisson inventory model (base-stock, $(s-1, s)$ policies, METRIC and VARI-METRIC). Convexity of $B$ in the stock level $s$, the paper's eq. (3), is a different statement; it is already posed on the platform as ServiceParts.StockLevels.backorder_differences (compound Poisson demand) and is not repeated here. The definition of the Poisson probabilities is the published ServiceParts.StockLevels.Basic (Muckstadt 2005).

Difficulty

Each step is classical, but none is a one-liner in Lean. The series $B(s \mid \lambda)$ is an infinite sum whose terms depend on $\lambda$ both through $e^{-\lambda}$ and through $\lambda^x$, so differentiating it twice under the summation sign requires a uniform summability bound for the derivative series on a neighbourhood of $\lambda$. The tempting shortcut of reasoning with deriv alone fails: deriv returns $0$ at points of non-differentiability, so a formula for deriv (deriv B) says nothing about smoothness, and the milestone is stated with HasDerivAt for this reason. The strict inequality further needs strict convexity, not just convexity, and a hypothesis that the prior is not concentrated on one value: with a one-point prior both sides coincide.

Formalization scope

• $B(s \mid \lambda)$ is a real-valued tsum over $x \in \mathbb N$ of $(x - s)\,p(x \mid \lambda)$ for $x > s$ and $0$ otherwise. The family is summable for every real $\lambda$; no statement relies on the tsum junk value.
• Spare stock is a natural number; mean demand is real. Convexity and the second-derivative formula are stated for $\lambda > 0$, the paper's "for any positive $\lambda$".
• Explicit readings of the paper's phrases: "backorders computed from a point estimate" is $B(s \mid \bar\lambda)$ with $\bar\lambda$ the prior mean (the paper assumes "the initial estimate is the mean of the true mean demand distribution"); "the correct value" is the prior expectation $\sum_k w_k B(s \mid \lambda_k)$; "mean demand can assume more than one value" means two distinct values each of positive probability; "positive spare stock" means $s \ge 1$; "understate" is strict.
• The prior is a finite distribution with positive support points. This covers the paper's two-point example and its five-to-ten-point discretization of a gamma prior; a general prior on $(0, \infty)$ would need integrability hypotheses and is not part of the mission.
• The printed value $B^*(2) = 0.1485$ is a rounding slip; the exact value is $0.14864\ldots$, and the worked example states $0.1486$.
• A formalization that fixes $s$, uses $\le$ in place of $<$, drops the nondegeneracy hypothesis (making the strict statement false), or states the second derivative with deriv alone (vacuous at non-differentiable points) does not meet the target.
• Not formalized: the remark that the understatement "is also true for probability distributions like the negative binomial, though difficult to prove analytically" (unproved on the page), the gamma prior and Bayes updating (a procedure), and the comment that the resulting allocation "will produce inferior results" (not a mathematical statement).
• Contributions welcome: termwise differentiation lemmas for Poisson-weighted series, the closed form $B(s \mid \lambda) = \lambda - s + \sum_{x<s}(s - x)p(x \mid \lambda)$, and a strict finite Jensen inequality in the form used here.

Selected references

• 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
• 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
• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005. https://doi.org/10.1007/0-387-27288-8

Why marginal allocation needs a convex hull

Service organizations keep repairable spare parts at a depot and at operating bases. Stock has a purchase or holding cost, while insufficient stock leaves backorders. Craig Sherbrooke's METRIC study describes how to evaluate such a system and distribute additional units among item types. Its fifth computational stage compares the reduction in expected backorders from the next unit with the cost of that unit. The comparison is delicate because the backorder function after optimizing the depot–base split can fail to be convex as a function of total item stock, even though a fixed depot-stock version is convex. Sherbrooke therefore introduces a convex extension before applying marginal analysis (Sherbrooke 1968, pp. 134–135).

This mission isolates the theorem in the paper's Appendix. It concerns abstract item functions with the properties needed for the allocation rule, so the result can be studied independently of the queueing assumptions and the FORTRAN procedure that produced those functions in METRIC. The paper supplies a proof of the Appendix theorem; the mission seeks a machine-checked formalization of its precise mathematical content (Sherbrooke 1968, pp. 140–141).

Setting: stock levels, costs, and the lower boundary

There is a finite collection of items indexed by $i$. A decision assigns each item a stock level $m_i\in\mathbb N$, where $0$ is permitted. Item $i$ has a unit cost $c_i$ and a real-valued function $\Xi_i(m)$ representing the backorder contribution associated with stock level $m$. In the METRIC application, $\Xi_i$ is obtained after choosing the best allocation of $m$ units between depot and bases. The Appendix theorem uses only that $\Xi_i$ is nonincreasing and has a finite lower bound. “Decreasing” is read weakly: the paper's justification says that adding a unit “cannot exceed” the backorders at the previous level (Sherbrooke 1968, p. 136).

For a function $g:\mathbb N\to\mathbb R$, write $\Delta g(m)=g(m+1)-g(m)$. The function is discretely convex when $\Delta g(m+1)\ge\Delta g(m)$ at every level. The lower convex hull $H_i$, written $\Xi_i'$ in the paper, is the greatest discretely convex function at or below $\Xi_i$. It follows the lower boundary of the convex hull of the points $(m,\Xi_i(m))$; a point above that boundary is lowered, while a contact point keeps its original value (Sherbrooke 1968, pp. 135–136, 140). The existing ServiceParts.StockLevels.Basic definition supplies $\Delta$ and $\Delta^2$ for real stock-level functions; this mission reuses it.

The original objective is the separable sum

$$J(m)=\sum_i\bigl(c_i m_i+\Xi_i(m_i)\bigr).$$

For each item, conditions (12) select the first level $\bar m_i$ where adding another unit no longer lowers the convexified cost:

$$c_i+H_i(\bar m_i+1)-H_i(\bar m_i)\ge0,\qquad \bar m_i>0\Longrightarrow c_i+H_i(\bar m_i)-H_i(\bar m_i-1)<0.$$

The second condition is automatic at $\bar m_i=0$, following the paper's convention $H_i(-1)=+\infty$ (Sherbrooke 1968, p. 140, Eqs. (11)–(12)).

Formalization targets

The Appendix goal is that each item's conditions (12) have exactly one solution and that the vector formed from those solutions minimizes the original, possibly nonconvex objective:

$$\forall i\;\exists!\bar m_i\in\mathbb N\text{ satisfying (12)}, \qquad J(\bar m)\le J(m)\quad\text{for every }m\in\mathbb N^I.$$

The milestone list follows the Appendix's claims: the lower boundary is a convex minorant; its marginal changes approach zero; (12) has a solution and that solution is unique; it minimizes the convexified single-item cost; and the selected level is a contact point where $H_i(\bar m_i)=\Xi_i(\bar m_i)$. The final comparison is with $J$, not just with the objective formed from $H_i$ (Sherbrooke 1968, pp. 140–141).

What the result establishes

The theorem licenses the paper's marginal allocation rule even when an item's original backorder function has nonconvex points. The rule can use a convex lower boundary to identify a level, yet the resulting allocation is optimal for the original function. Without the contact-point conclusion, optimality of the modified objective alone would not give that guarantee. The theorem is stated for any finite number of independent items with the listed properties, so it is reusable beyond the specific depot–base model (Sherbrooke 1968, pp. 134–136, 140–141).

The paper proves the result informally. This mission's definitions and theorem statements compile locally as open Lean goals; they do not yet constitute a machine-checked proof. A related published Prove2Me result, ServiceParts.Allocation.allocOpt_correct, proves correctness of an allocation algorithm for piecewise-linear functions assumed convex. It does not address the convexification or contact claim here. The platform's posed ServiceParts.StockLevels.optimal_stock_criterion and greedy_fill_rate_optimal concern other marginal criteria and likewise do not settle this Appendix theorem. A successful development would provide reusable Lean infrastructure for lower convex envelopes of integer sequences, their forward differences, and separable finite allocations.

Difficulty

A one-step marginal comparison on the raw $\Xi_i$ is insufficient when its forward differences can fall and then rise: an apparent local stopping point need not minimize the full sequence. Replacing $\Xi_i$ by a convex minorant restores ordered marginal changes, but a minimizer of a smaller function need not minimize the original function. The central burden is therefore the exact relation between the lower boundary and the original points at a level selected by the strict condition in (12). Ties in the objective add a second precision issue: the selected level is unique under the rule even when the objective has more than one minimizer (Sherbrooke 1968, pp. 135, 140–141).

Formalization scope and conventions

Stock levels are natural numbers, item contributions and costs are real, and the item type is finite; the empty item type is allowed, making both the sum and the coordinatewise statement trivial. The functions $\Xi_i$ are nonincreasing and bounded below, as in the Appendix. The lower hull is a pointwise real supremum over all discretely convex minorants. Its defining family is nonempty and bounded at each point under the lower-bound hypothesis, which every hull theorem carries. The hull is therefore fixed by the input function rather than supplied as an arbitrary minorant. The goal compares every vector in $\mathbb N^I$, without a budget restriction. The formalization does not use a default value for $H_i(-1)$: the predecessor condition applies only to positive stock levels.

The paper prints $c_i\ge0$ with at least one positive cost. Its existence assertion fails when a particular $c_i=0$: for $\Xi_i(m)=1/(m+1)$, a bounded, decreasing, convex sequence, the first inequality of (12) never holds. The goal and existence milestone therefore require $c_i>0$ for every present item. The paper's phrase “unique optimizing” is interpreted as uniqueness of the stock vector determined by (12), together with its optimality. It cannot assert uniqueness among all minimizers: with $c=1$, $\Xi(0)=1$, and $\Xi(m)=0$ for $m\ge1$, levels $0$ and $1$ tie. The proof's own wording identifies (12) as the unique selection rule (Sherbrooke 1968, p. 140).

The formalization contains separate definitions for discrete convexity, the greatest lower hull, conditions (12), and objective (11). It welcomes proofs and general lemmas about convex integer sequences and finite separable sums. The METRIC computation, empirical Air Force data, equations (7)–(9), and the discussion of Lagrangian versus combinatorial solutions are context rather than goals of this mission. A definition that simply sets $H_i=\Xi_i$, or a conclusion that minimizes only the hull objective, would omit the theorem's content.

Selected references

• Craig C. Sherbrooke, METRIC: A Multi-Echelon Technique for Recoverable Item Control, Operations Research 16(1), 122–141, 1968. DOI: 10.1287/opre.16.1.122.