Motivation

Stochastic processing networks (Harrison 2000) model manufacturing lines, data switches, call centers and multiclass queueing networks in one framework: jobs wait in buffers, activities process jobs from one or several buffers at once, each activity may need several processors simultaneously, and routing after service may depend on the activity used. A central control question is which dynamic policy keeps such a network stable whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) answer it with maximum pressure policies, a generalization of the back-pressure policy of Tassiulas and Ephremides (1992) for wireless networks. At each decision time the policy picks an extreme allocation maximizing a linear "network pressure" in the current buffer levels; it needs no arrival-rate information. Their main result (Theorem 2) is pathwise stability whenever Harrison's static planning LP has a feasible solution with $\rho\le1$. The proof goes through the fluid model: a deterministic, continuous analogue of the network whose stability implies stability of the stochastic system.

This mission formalizes Theorem 5 of the paper, the strong form of the fluid-level result: under a strict load condition $\rho<1$ and a mild structural assumption, every solution of the maximum pressure fluid model empties in finite time, uniformly over bounded initial states. Fluid stability in this sense (Definition 4) is the property that the standard fluid-limit machinery (Dai 1995) turns into positive Harris recurrence of the stochastic network.

Setting

The network has buffers $0,1,\dots,I$, where Buffer $0$ is the outside world and $\mathcal I=\{1,\dots,I\}$ are the internal buffers, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}\in\{0,1\}$ records whether activity $j$ needs processor $k$, and $B_{ji}\in\{0,1\}$ whether activity $j$ processes buffer $i$.
• An input activity processes only Buffer $0$; a service activity never processes Buffer $0$. Every activity is one or the other. Every processor serves only input activities (an input processor) or only service activities (a service processor).
• $m_j>0$ is the mean processing requirement of activity $j$, $\mu_j=1/m_j$, and $P^j$ is its routing matrix.

The input-output matrix is $R_{ij}=\mu_j\big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\big)$. An allocation is $a\in\mathbb R^J_+$ with $\sum_jA_{kj}a_j\le1$ for every processor and $=1$ for every input processor; $\mathcal A$ is the set of allocations and $\mathcal E$ the set of its extreme points. The network pressure of $a$ at buffer level $z\in\mathbb R^I_+$ is $p(a,z)=z\cdot Ra$.

The static planning LP asks for $x\ge0$ and $\rho$ with $Rx=0$, $\sum_jA_{kj}x_j\le\rho$ for service processors and $=1$ for input processors. Assumption 1 (extreme-allocation-available, EAA) says that for every $z\in\mathbb R^I_+$ some maximizer of $p(\cdot,z)$ over $\mathcal E$ has $z_i>0$ on all its constituent buffers. Assumption 2 says there is $x\ge0$ with $Rx>0$ componentwise.

A fluid model solution is a pair of paths $(\bar Z,\bar T)$, buffer levels $\bar Z(t)\in\mathbb R^I$ and cumulative activity times $\bar T(t)\in\mathbb R^J$, satisfying (14)–(18): $\bar Z(t)=\bar Z(0)-R\bar T(t)$ (written out over buffers), $\bar Z\ge0$, input processors always busy, every processor's busy time at most elapsed time, and $\bar T$ nondecreasing with $\bar T(0)=0$. A time $t>0$ is regular if both paths are differentiable there. Under a maximum pressure policy the solution also satisfies (20): at each regular $t$,

$$R\dot{\bar T}(t)\cdot\bar Z(t)=\max_{a\in\mathcal E}Ra\cdot\bar Z(t).$$

Formalization targets

Goal: Theorem 5

$$\text{Assumptions 1, 2 and an LP solution with } \rho<1\ \Longrightarrow\ \exists\,\delta>0:\ |\bar Z(0)|\le1\Rightarrow \bar Z(t)=0\ \ \forall t\ge\delta,$$

for every solution of (14)–(18) and (20). The constant $\delta$ depends on the network only.

Milestones

1. For an input activity $j$, $R_{ij}=-\mu_jB_{j0}P^j_{0i}\le0$.
2. Assumption 2 yields $\hat x\ge0$ with $R\hat x>0$ that vanishes on input activities and loads no input processor.
3. After scaling $\hat x$, the vector $x^*=\tilde x+\hat x$ is an allocation and $Rx^*\ge\delta e$ for some $\delta>0$.
4. The maximum of $p(\cdot,z)$ over $\mathcal A$ is attained on $\mathcal E$ (p. 201).
5. The identities (22)–(23): $\dot f(t)=2\dot{\bar Z}(t)\cdot\bar Z(t)=-2R\dot{\bar T}(t)\cdot\bar Z(t)$ for $f=\sum_i\bar Z_i^2$.
6. $R\dot{\bar T}(t)\cdot\bar Z(t)\ge Rx^*\cdot\bar Z(t)\ge\delta\sum_i\bar Z_i(t)\ge\delta\|\bar Z(t)\|$.
7. $\dot f(t)\le-2\delta\sqrt{f(t)}$ at regular times.
8. The explicit emptying time: $\bar Z(t)=0$ for $t\ge\|\bar Z(0)\|/\delta$.

Significance

The result. Theorem 4 of the paper gives only weak stability (a fluid model started empty stays empty) under $\rho\le1$, which suffices for pathwise stability. Theorem 5 gives a uniform emptying time under $\rho<1$, the hypothesis that standard arguments (Dai 1995; Dai and Meyn 1995) need to conclude positive Harris recurrence and moment bounds for the stochastic network. The emptying-time bound is explicit and linear in the initial fluid level.

Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The closest formalized result on Prove2Me is ProcessingNetworks.BackPressure.bp_maximal_stability (Dai and Harrison's book, Theorem 9.12), which uses the same Lyapunov idea in a different model: exogenous arrival rates, the planning problem $Rx=\lambda$, no input activities and no Buffer 0. The present mission formalizes the Dai–Lin model with input processors, where the planning LP has $Rx=0$ and the equality constraints (2). The definitions file (network, $\mathcal A$, $\mathcal E$, pressure, fluid model, (20)) is shared in content with the other missions of this series.

Difficulty

Each algebraic step is short; the work is in the analysis. The obvious route reads $\dot f\le-2\delta\sqrt f$ as an ordinary differential inequality and integrates it. That requires the inequality almost everywhere, but it is only available at regular points. So one needs: Lipschitz continuity of $\bar T$ and $\bar Z$ on $[0,\infty)$ from (16)–(18), almost-everywhere differentiability (Rademacher), and a comparison argument for an absolutely continuous function, $\sqrt f=\|\bar Z\|$, whose derivative bound holds only where $f>0$. The step "by (20)" also needs the maximum over $\mathcal E$ to dominate every allocation in $\mathcal A$. That is the vertex property of a bounded polyhedron, which in Lean means compactness of $\mathcal A$ plus a Krein–Milman type argument. The published Dini-derivative extinction criterion ProcessingNetworks.LyapunovCriteria.dini_extinction_criterion (Dai–Harrison Lemma 8.11) is a possible tool for the last step, applied to $\|\bar Z\|$.

Formalization scope

• Indices are 0-based: internal buffers Fin I, buffers $0..I$ as Fin (I+1) with Buffer 0 the index 0 and internal buffer i the index i.succ, activities Fin J, processors Fin K.
• Paths are functions ℝ → (Fin n → ℝ) constrained only at $t\ge0$. Derivatives are deriv, used only at regular points.
• (20) is encoded as IsGreatest of the set of pressures over $\mathcal E$, so the maximum is attained and an empty $\mathcal E$ cannot pass through a junk supremum. $\mathcal E$ is Mathlib's Set.extremePoints.
• The fluid model of the theorem is the predicate "(14)–(18) and (20)". Solutions are not required to be fluid limits.
• The standing assumptions of §2 are one predicate, Network.Standing. Two disclosed additions are needed for the objects to make sense: every input processor has an activity, and $m_j>0$. The row sums of $P^j$ are not imposed.
• The theorem's text cites "the LP (9)–(12)". The proof needs $x\ge0$, so the LP used is (9)–(13), as in Theorems 1, 2 and 4.
• The norm in Definition 4 is Euclidean, as in the proof.
• Assumption 1 is a hypothesis of the goal because the page states it. The fluid-level argument does not use it.
• Ruled out: a vacuous goal. A sorry-free sanity file shows a one-buffer network (one input activity, one service activity) that satisfies every hypothesis of the goal and has a maximum pressure fluid solution. The milestone on the maximum over $\mathcal A$ carries the hypothesis $\mathcal A\neq\emptyset$, because the standing assumptions alone do not imply it.

Contributions of reusable lemmas are welcome, in particular almost-everywhere differentiability of Lipschitz paths on $[0,\infty)$, the vertex property of bounded polyhedra, and extinction of nonnegative absolutely continuous functions with $\dot g\le-\varepsilon$ on $\{g>0\}$.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662

Motivation

The lost-sales inventory problem with lead times is a basic model of operations management. A retailer reviews one product's stock each period and places an order that arrives $L$ periods later. Demand that cannot be met from stock on hand is lost, and the retailer pays a holding cost $h$ per unit left on the shelf and a penalty $p$ per unit of lost demand. The optimal policy depends on the whole pipeline of outstanding orders, so the state space grows with $L$, and the problem is computationally hard for long lead times. Simple base-stock (order-up-to) policies are therefore the standard heuristic, and Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 2009) showed they are asymptotically optimal as the lost-sales penalty grows.

Agrawal and Jia (arXiv:1905.04337) study the learning version, in which the demand distribution is unknown and only sales, not demands, are observed. They give an algorithm whose regret against the best base-stock policy is $\tilde O(L\sqrt T)$, improving the earlier bound of Zhang, Chao and Shi, which grows exponentially in $L$. The improvement rests on one structural fact: started from two different states, the base-stock system accumulates expected costs that differ by an amount linear in $L$ and independent of the horizon. That fact, Lemma 2.5 of the paper, is the goal of this mission.

Setting

Fix a lead time $L\ge 0$ and a base-stock level $x$. A state is a vector $\mathbf s=(s(0),s(1),\dots,s(L))$ of real numbers. Its entry $s(0)$ is the on-hand inventory after the current period's arrival, and $s(1),\dots,s(L)$ are the outstanding orders, $s(L)$ the most recent. Under a base-stock policy with level $x$ the states lie in

$$\mathcal S^x=\Big\{\mathbf s : s(i)\ge 0\ \text{for all } i,\ \sum_{i=0}^{L}s(i)=x\Big\}.$$

In each period $t$ a demand $d_t\ge 0$ is drawn, independently across periods, from a distribution $F$ on $[0,\infty)$. The sales are $y_t=\min\{s_t(0),d_t\}$ and the on-hand inventory is $I_t=s_t(0)$. The policy reorders exactly what was sold, so for $L\ge 1$ the next state is

$$\mathbf s_{t+1}=\big(s_t(0)-y_t+s_t(1),\ s_t(2),\ \dots,\ s_t(L),\ y_t\big),$$

and for $L=0$ the state $(x)$ never changes. The pseudo-cost of period $t$ is $C^x_t=h(s_t(0)-y_t)-p\,y_t$, and the value over horizon $T$ from the start state $\mathbf s$ is

$$V^x_T(\mathbf s)=\mathbb E\Big[\sum_{t=1}^{T}C^x_t\ \Big|\ \mathbf s_1=\mathbf s\Big].$$

Along a demand path, $n^x_T(\mathbf s)=\sum_{t=1}^T y_t$ is the total sales and $m^x_T(\mathbf s)=\sum_{t=1}^T I_t$ the total on-hand inventory.

States are compared by the order of Definition B.1: $\mathbf s'\succeq\mathbf s$ if $\mathbf s'-\mathbf s=\delta$ with $\sum_i\delta_i=0$ and some $0\le k\le L-1$ such that $\delta_i\ge 0$ for $i\le k$ and $\delta_i\le 0$ for $i>k$. Thus $\mathbf s'$ holds the same total, shifted toward the shelf. The state $\hat{\mathbf s}=(x,0,\dots,0)$ dominates every state of $\mathcal S^x$.

Formalization targets

Goal: Lemma 2.5 (p. 8)

For every $x$, every horizon $T$, all costs $h,p\ge 0$, every demand law $F$ and all $\mathbf s,\mathbf s'\in\mathcal S^x$,

$$V^x_T(\mathbf s)-V^x_T(\mathbf s')\le 36\max(h,p)\,L\,x .$$

The constant is the paper's printed one. The proof's last display gives $18(h+p)Lx$, a stronger bound, which is deliberately not the goal.

Milestones (Appendix B and the proof of Lemma 2.5)

All of the following hold for $L\ge 1$, along any single demand path that drives both chains:

1. Lemma B.2 (p. 20). If $\mathbf s'_1\succeq\mathbf s_1$ then for $t\le L+1$ the cumulative sales satisfy $Y'_t-Y_t\le\max_{0\le k\le t-1}(\delta_0+\dots+\delta_k)$.
2. Lemma B.3 (p. 20). If moreover $I'_t\ge I_t$ for $t=1,\dots,L+1$, then $n_T(\mathbf s'_{L+1})=n_T(\mathbf s_{L+1})$ for every $T$.
3. Lemma B.5 (p. 21). At the successive first crossing times $\sigma_i,\tau_i$ of Definition B.4, the state order alternates: $\mathbf s'_{\sigma_i}\succeq\mathbf s_{\sigma_i}$ and $\mathbf s'_{\tau_i}\preceq\mathbf s_{\tau_i}$ whenever these times exist.
4. Lemma B.6 (p. 21). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|n^x_T(\mathbf s')-n^x_T(\mathbf s)|\le 3x$.
5. Lemma B.7 (p. 23). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|m^x_T(\mathbf s)-m^x_T(\mathbf s')|\le 6Lx$.
6. Proof of Lemma 2.5 (p. 9). $\hat{\mathbf s}\succeq\mathbf s$ for every $\mathbf s\in\mathcal S^x$.
7. Proof of Lemma 2.5 (p. 9). $|V^x_T(\mathbf s)-V^x_T(\hat{\mathbf s})|\le 9(h+p)Lx$.

Significance

Lemma 2.5 bounds the dependence of the base-stock chain's finite-horizon cost on its starting state, uniformly in the horizon. In the paper it yields three consequences: the long-run average cost (the loss) of a base-stock policy does not depend on the initial state (Lemma 2.6), the bias of the chain is bounded by $36\max(h,p)Lx$ (Lemma 2.8), and finite-horizon average costs concentrate around the loss (Lemma 2.10). These feed the regret bound of Theorem 1.3. The lemma is also a statement about the base-stock lost-sales system alone, without any learning, so it is of independent interest for coupling arguments on lost-sales chains.

The paper's proof is complete on paper, but nothing in it has a machine-checked proof. Neither the lost-sales base-stock chain with lead times started from an arbitrary pipeline state nor any of the coupling lemmas of Appendix B is formalized elsewhere. This mission produces a checked proof of the goal and of the pathwise comparison lemmas. Theorem 1.3 is not posed: its supporting lemmas rely on limits whose existence the paper settles only by an informal discretization (Remark 4).

Difficulty

The obvious argument couples the two chains on a common demand path and waits until they coalesce. Coalescence is guaranteed only after $L$ consecutive periods of zero demand, an event of probability exponentially small in $L$, so this argument gives a bound exponential in $L$. That is the bound of earlier work.

The linear bound needs a finer pathwise accounting. The two coupled chains do not stay ordered: the one that starts with more inventory on the shelf sells more at first, then runs short and sells less. The order $\succeq$ between the two states alternates along a sequence of times, and the sales gained in one phase must be shown to be lost again in the next, so that the cumulative difference stays bounded by a constant multiple of $x$ for every horizon. Turning this alternation into a bound requires tracking how the pipeline vectors evolve between alternation times, including the boundary cases in which the chains coalesce or the horizon ends inside a phase.

Formalization scope

All declarations live in the namespace LostSalesLearning.ValueGap. A state is a function Fin (L + 1) → ℝ, a demand path is a function ℕ → ℝ≥0, and time is 0-based: traj s d 0 is the paper's $\mathbf s_1$, traj s d t is $\mathbf s_{t+1}$, and $\sum_{t=1}^T$ is a sum over Finset.range T. The demand law $F$ is a probability measure on ℝ≥0, and the demand path has the product law Measure.infinitePi (fun _ => F). The value is the expectation of the summed pseudo-costs, which equals Definition 2.4 by the tower property and is the form used in the paper's proof.

Committed conventions:

• The costs satisfy $h\ge 0$ and $p\ge 0$, the reading of "per unit holding cost and per unit lost sales penalty".
• No assumption is placed on $F$. The paper's assumptions $F(0)>0$ and bounded demand belong to other results.
• The goal holds for every $L\ge 0$; the Appendix B milestones carry $L\ge 1$, as Appendix B does.
• The order $\succeq$ is Definition B.1 verbatim, with the equal-sum clause and the split index $k\le L-1$.
• The pathwise milestones quantify over every demand path and drive both chains with the same path.
• The first crossing times of Definition B.4 are represented by alternationTimes; an absent next crossing is none.

Two trivializing formalizations are ruled out. A comparison of the two values on different or fixed demand paths would be a different statement: the goal compares two expectations under the same law, and each pathwise milestone uses one common path. A Bochner integral of a non-integrable function would be $0$. The integrand here is measurable and bounded by $T(h+p)x$ on $\mathcal S^x$, so the values are genuine expectations.

A complete development needs the elementary dynamics of the chain, including invariance of $\mathcal S^x$ and the shift of trajectories, which is reusable for other lost-sales models. It also needs the alternation times of Definition B.4, and measurability of the trajectory in the demand path. Proofs of individual milestones, alternative proofs of the goal, and sharper constants as separate statements are all welcome.

Selected references

• S. Agrawal and R. Jia, Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management, arXiv:1905.04337v1, 2019. https://arxiv.org/abs/1905.04337
• W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
• H. Zhang, X. Chao and C. Shi, Closing the Gap: A Learning Algorithm for Lost-Sales Inventory Systems with Lead Times, Management Science 66(5), 2020. https://doi.org/10.1287/mnsc.2019.3288
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.

Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.

Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.

Setting

A population consists of $M\ge2$ individuals, each carrying an allelic type. Its description is $\mathbf M=(M_1,\dots,M_M)$, where $M_i$ is the number of allelic types carried by exactly $i$ individuals, so that

$$\sum_{i=1}^{M} iM_i=M. \qquad (7.3)$$

For a real parameter $\nu>0$, the Ewens distribution on descriptions is

$$\pi_M(\mathbf M)=\binom{\nu+M-1}{M}^{-1}\prod_{i=1}^{M}\Big(\frac{\nu}{i}\Big)^{M_i}\frac{1}{M_i!}, \qquad (7.6)$$

where $\binom{x}{k}=x(x-1)\cdots(x-k+1)/k!$ is the binomial coefficient for real $x$. In the infinite alleles model, individuals die at rate $\mu$, each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability $u$; then (7.6) is the equilibrium distribution with $\nu=(M-1)u/(1-u)$ (7.5).

A random sample of size $1\le m\le M$ without replacement is a uniformly random $m$-element subset of the $M$ labelled individuals, each of the $\binom Mm$ subsets being equally likely; the sample has a description in the same sense.

The number $j$ of individuals carrying one given allele performs a random walk on $\{0,\dots,M\}$ with intensities

$$q(j,j-1)=\mu\frac jM\Big(\frac{M-j}{M-1}+\frac{j-1}{M-1}u\Big),\qquad q(j,j+1)=\mu\frac{M-j}{M}\frac{j}{M-1}(1-u). \qquad (7.8)$$

An allele is quasi-fixed when it is the only allele present ($j=M$).

Formalization targets

Goal: consistency under sampling (Theorem 7.1)

If $M\ge2$ and the population description is distributed as $\pi_M$, then a random sample of size $1\le m\le M$ drawn without replacement has description $\mathbf m$ with probability $\pi_m(\mathbf m)$, the same $\nu$ being used for both sizes:

$$\sum_{\mathbf M}\pi_M(\mathbf M)\,P\big(\text{sample has description }\mathbf m\mid\text{population has description }\mathbf M\big)=\pi_m(\mathbf m).$$

Milestones

1. (7.6) is a distribution: $\pi_M(\mathbf M)>0$ and $\sum_{\mathbf M}\pi_M(\mathbf M)=1$ (Exercise 7.1.3).
2. Theorem 7.1 for $m=M-1$, the case the book's proof establishes first.
3. Corollary 7.5, the identity of its proof: the probability that a uniformly chosen individual's allele is carried by exactly $i$ individuals is

$$\sum_{\mathbf M}\frac{iM_i}{M}\pi_M(\mathbf M)=\frac{\nu}{M}\binom{\nu+M-1}{i}^{-1}\binom Mi. \qquad (7.9)$$

4. Theorem 7.9: the probability $Q$ that the walk (7.8) started at $1$ reaches $M$ before $0$ satisfies

$$Q^{-1}=\sum_{i=0}^{M-1}\binom{M-1}{i}^{-1}\binom{\nu+M-1}{i}.$$

Significance

The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on $\nu$. Kelly deduces from it the sufficiency of the number of alleles in a sample for $\nu$ and the heterozygosity $\nu/(\nu+1)$ (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).

Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.

Difficulty

The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between $M-1$ and $M$, a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives $\pi_{M-1}$ and $\pi_M$. Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of $m$-subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.

Formalization scope

• Descriptions of $n$ individuals are integer partitions Nat.Partition n, with $M_i$ the multiplicity of the part $i$; the product in (7.6) runs over $i=1,\dots,n$. The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.
• The population is Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is $\binom Mm^{-1}$ times the number of $m$-subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.
• The goal and Corollary 7.5 quantify over an arbitrary choice of labelling for each population description. They assume $M\ge2$, as required by the chapter's rule that a parent is chosen among the other $M-1$ individuals; the goal also assumes $1\le m\le M$. Because $\pi_M>0$, this forces the conditional sampling law to depend on the population only through its description. Types are natural numbers, so every description is realized and the hypothesis is never vacuous.
• The quasi-fixation probability is defined through the jump chain of (7.8): the limit of the probabilities of reaching $M$ within $n$ jumps without reaching $0$. The theorem assumes $M\ge2$, $\mu>0$, $0<u<1$ and $\nu=(M-1)u/(1-u)$.
• Corollary 7.5 is formalized as the identity of its proof. The identification of the oldest allele's frequency with that of a randomly chosen individual uses allele ages and the reversibility of the labelled process (Theorem 7.2) and is not formalized. Theorem 7.2 itself, whose state space orders the allele labels within each class, and the allele-age results (Corollaries 7.3, 7.4, 7.7, 7.8, Theorem 7.6, Corollary 7.10, Theorem 7.11) are not part of the mission.

Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity $(1-x)^{-\nu}=\prod_j e^{\nu x^j/j}$) are reusable beyond this mission.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 7. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• W. J. Ewens, The sampling theory of selectively neutral alleles, Theoretical Population Biology 3 (1972), 87–112. https://doi.org/10.1016/0040-5809(72)90035-4
• J. F. C. Kingman, The representation of partition structures, Journal of the London Mathematical Society (2) 18 (1978), 374–380. https://doi.org/10.1112/jlms/s2-18.2.374
• M. Kimura and J. F. Crow, The number of alleles that can be maintained in a finite population, Genetics 49 (1964), 725–738. https://doi.org/10.1093/genetics/49.4.725

Motivation

Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.

Setting

There are $T$ periods $t = 1, \dots, T$ and a known lead time $L \ge 0$: an order placed in period $t$ arrives in period $t + L$. Period $t$ has a per-unit holding cost $h_t \ge 0$ and a per-unit backlogging penalty $p_t \ge 0$. Ordering costs are zero ($c_t = 0$), which is the standing assumption of the paper's §4. The initial data are the net inventory $ni_0$ and the pipeline orders $q_{1-L}, \dots, q_0 \ge 0$.

Demands $D_1, \dots, D_T$ are nonnegative random variables on a probability space with a filtration $(\mathcal F_t)$; $\mathcal F_t$ is the information at the beginning of period $t$, and $D_t$ is $\mathcal F_{t+1}$-measurable. A feasible policy $P$ places orders $Q^P_t \ge 0$ that are $\mathcal F_t$-measurable. Write $D_{[s,t]} = \sum_{j=s}^t D_j$ (with $D_j = 0$ for $j \le 0$), $X_t = ni_0 + \sum_{j=1-L}^{t-1} Q_j - D_{[1,t-1]}$ for the inventory position before ordering and $Y_t = X_t + Q_t$ after ordering.

The marginal holding cost of period $t$ is the holding cost that the units ordered in $t$ incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:

$$H^P_t = \sum_{j=t+L}^{T} h_j\,\bigl(Q^P_t - (D_{[t,j]} - X^P_t)^+\bigr)^+, \qquad \Pi^P_t = p_{t+L}\,\bigl(D_{[t,t+L]} - Y^P_t\bigr)^+ .$$

The cost of $P$ is $\mathcal C(P) = \sum_{t=1}^{T-L}(H^P_t + \Pi^P_t)$; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.

A dual-balancing policy $B$ orders nothing after period $T - L$, and in each period $t \le T - L$ orders the quantity that balances the two conditional expected marginal costs:

$$E\bigl[H^B_t \mid \mathcal F_t\bigr] = E\bigl[\Pi^B_t \mid \mathcal F_t\bigr] \quad\text{almost surely.}$$

Formalization targets

Goal: Theorem 4.1

For every dual-balancing policy $B$ and every feasible policy $P$,

$$E[\mathcal C(B)] \;\le\; 2\,E[\mathcal C(P)] .$$

The paper writes $P = OPT$; quantifying over all feasible $P$ is the same statement whenever an optimum exists and needs no existence assumption.

Milestones

1. Lemma 4.1. $E[\mathcal C(B)] = 2\sum_{t=1}^{T-L}E[Z_t]$ with $Z_t = E[H^B_t \mid \mathcal F_t]$.
2. Lemma 4.2. With $\mathcal T_H = \{t : Y^B_t < Y^P_t\}$, $\sum_{t\in\mathcal T_H} H^B_t \le \sum_{t=1}^{T-L} H^P_t$ on every realization.
3. Lemma 4.3. With $\mathcal T_\Pi = \{t : Y^B_t \ge Y^P_t\}$, $\sum_{t\in\mathcal T_\Pi} \Pi^B_t \le \sum_{t=1}^{T-L} \Pi^P_t$ on every realization.

Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals $\sum_{t=1-L}^{0}\Pi_t + H_{(-\infty,0]} + \sum_{t=1}^{T-L}(H_t + \Pi_t)$, which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when $h_T > 0$ and the demands are integrable, so the goal is not about an empty class.

Significance

The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.

Difficulty

The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets $\mathcal T_H$ and $\mathcal T_\Pi$ to be determined by the information of period $t$, so that conditioning on $\mathcal F_t$ commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.

Formalization scope

• Periods are integers (ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods $1, \dots, T$ are read, and the pipeline $q_t$ is substituted for $t \le 0$.
• Ordering costs are $c_t = 0$ and there is no discounting, as in the paper's §4; the reduction of §4.6 from general instances is not formalized. The lead time $L$ is general.
• Information is an arbitrary Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.
• Expected costs are lower Lebesgue integrals in $[0,\infty]$, so an infinite expected cost is never read as $0$.
• The balancing condition carries integrability of $H^B_t$ and $\Pi^B_t$, so a conditional expectation of a non-integrable cost (which Mathlib sets to $0$) cannot satisfy it vacuously. The existence item rules out an empty policy class.
• Lemmas 4.2 and 4.3 are pathwise and do not use the balancing rule. The comparator totals are the marginal totals of Eq. (4), which is the stronger reading.
• Eq. (2) prints $X_{t+L}$ and its restatement on p. 292 prints $p_t$; both are typos, and the formalization uses $X_t$ and $p_{t+L}$.

A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded $\mathcal F_t$-measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.

Selected references

• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. doi:10.1287/moor.1060.0205
• D. C. Heath, P. L. Jackson, Modeling the evolution of demand forecasts with application to safety stock analysis in production/distribution systems, IIE Transactions 26(3):17–30, 1994. doi:10.1080/07408179408966604
• P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000. ISBN 978-0-256-11379-7.

Motivation

The bullwhip effect is the observation that the variability of orders grows as one moves up a supply chain, from the retailer to the wholesaler, the distributor and the factory, even when customer demand is stable. It was documented in industry practice by Lee, Padmanabhan and Whang (Management Science, 1997), who identified demand forecasting as one of its main causes. Amplified order variability raises the safety stock, capacity and transportation costs of every upstream firm, so the question of how large the effect is, and what reduces it, is central to supply chain management.

Chen, Drezner, Ryan and Simchi-Levi (Management Science 46(3), 2000) quantified the effect for a retailer that forecasts with a moving average and follows an order-up-to policy. Their §3 asks whether sharing customer demand information with every stage removes the effect. Theorem 3.1 (the companion mission of this series) shows that it does not; Theorem 3.2, the goal of this mission, gives the lower bound for the chain in which no demand information is shared.

Setting

Time is indexed by the integers $t \in \mathbb Z$. The retailer faces i.i.d. demand

$$D_t = \mu + \epsilon_t,$$

where the error terms $\epsilon_t$ are independent and identically distributed from a symmetric distribution with mean $0$ and variance $\sigma^2 > 0$.

Single-stage policy (§2). With $p \ge 1$ observations, a lead time $L$, a safety factor $z$ and a constant $C_{L,\rho}$, the retailer forms the moving-average estimates

$$\hat D^L_t = L\,\frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat\sigma^L_{et} = C_{L,\rho}\sqrt{\frac{\sum_{i=1}^p e_{t-i}^2}{p}}, \qquad e_t = D_t - \hat D^1_t,$$

raises its inventory position to the order-up-to point $y_t = \hat D^L_t + z\hat\sigma^L_{et}$, and so orders $q_t = y_t - y_{t-1} + D_{t-1}$. Orders may be negative: excess inventory is returned without cost.

Decentralized chain (§3). Stages $k = 1, 2, \dots$ form a serial chain; stage 1 is the retailer, and $L_k$ is the lead time between stages $k$ and $k+1$. No stage sees customer demand except the retailer. Stage $k$ forecasts from the orders it receives,

$$\hat D^{(1)}_t = \frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat D^{(k)}_t = \frac{\sum_{j=0}^{p-1} q^{k-1}_{t-j}}{p} \quad (k \ge 2),$$

uses the order-up-to point $y^k_t = L_k\hat D^{(k)}_t$, and orders

$$q^1_t = y^1_t - y^1_{t-1} + D_{t-1}, \qquad q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t \quad (k \ge 2).$$

Formalization targets

Goal: Theorem 3.2 (Eq. (7))

For every stage $k \ge 1$ and every period $t$,

$$\frac{\operatorname{Var}(q^k_t)}{\operatorname{Var}(D_t)} \;\ge\; \prod_{i=1}^{k}\left(1 + \frac{2L_i}{p} + \frac{2L_i^2}{p^2}\right).$$

The bound is the paper's, with its explicit constants. The paper asserts no tightness for this theorem, and none is claimed.

Milestone: Eq. (6)

For the single-stage policy with any safety factor $z$ and any constant $C_{L,\rho}$,

$$\frac{\operatorname{Var}(q_t)}{\operatorname{Var}(D_t)} \;\ge\; 1 + \frac{2L}{p} + \frac{2L^2}{p^2}.$$

This is the i.i.d. case $\rho = 0$ of the paper's Theorem 2.2. With $z = 0$ and $L = L_1$ the single-stage orders are the stage-1 orders of the chain, so Eq. (6) contains the case $k = 1$ of the goal.

Significance

The result. Theorem 3.2 is half of the paper's comparison between centralized and decentralized information. When demand information is shared, the amplification from the retailer to stage $k$ in the i.i.d. case equals $1 + 2(\sum_{i\le k}L_i)/p + 2(\sum_{i\le k}L_i)^2/p^2$ (Eq. (8)), which grows additively in the lead times. Without sharing, the lower bound (7) is a product over stages and grows multiplicatively. The paper concludes that centralizing demand information "can significantly reduce the bullwhip effect", and that the gap widens as one moves up the chain. Eq. (6) is the single-stage statement that forecasting with a moving average alone already amplifies variability, by a factor depending only on the ratio $L/p$.

Formalizing it. The paper gives no proof of Theorem 3.2; it refers to Ryan (1997, PhD thesis) and to Chen et al. (1998). A machine-checked proof would therefore supply the first self-contained, verified argument for the multiplicative bound. The Gaussian special case of Eq. (6) is already formalized on Prove2Me, in the Snyder–Shen chapter on the bullwhip effect (SupplyChainTheory.bullwhip_signal_processing at $\rho = 0$); that statement assumes Gaussian errors, whereas this mission assumes only symmetry, mean $0$ and variance $\sigma^2$. Neither the multistage bound nor the symmetric-error version of Eq. (6) has a formal proof.

Difficulty

The natural first idea is induction on the stage: treat the orders of stage $k-1$ as the demand of stage $k$ and apply the single-stage bound. That step fails, because the single-stage bound is a statement about i.i.d. demand, and the orders reaching stage $k \ge 2$ are not i.i.d.: they are autocorrelated, and stage $k$'s moving average of those orders interacts with the correlation in a way that can raise or lower the variance. Whether the product bound survives depends on controlling that interaction at every stage. For Eq. (6), the safety-stock term $z\hat\sigma^L_{et}$ is a nonlinear function of the demands, and only symmetry of the errors, not normality, is available to control its interaction with the linear part of the order.

Formalization scope

All objects live in the namespace ChenBullwhip.Decentralized.

• IIDDemand P is the demand model on a probability space $(\Omega, P)$: a constant mu, sigma > 0, and errors eps : ℤ → Ω → ℝ that are measurable, mutually independent (iIndepFun), identically distributed, symmetric (eps t and -eps t have the same law), in $L^2$, with mean $0$ and variance sigma ^ 2. Demand is D t = mu + eps t. Variances are Mathlib's ProbabilityTheory.variance.
• SingleStage defines $\hat D^L_t$, $e_t$, $\hat\sigma^L_{et}$, $y_t$ and $q_t$ of §2; $C_{L,\rho}$ is a free real parameter, as the paper does not fix it.
• Chain defines the forecasts $\hat D^{(k)}_t$ and the orders $q^k_t$ by recursion on the stage, with the convention $q^0_t = D_{t-1}$, so that stage 1 orders $y^1_t - y^1_{t-1} + D_{t-1}$. The recursion $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$ is not printed in the paper; it is the §2.2 order identity applied to a stage whose incoming demand is $q^{k-1}_t$, as the sequence of events on p. 440 describes.

Disclosed hypotheses not on the page: $p \ge 1$ (a moving average needs an observation), $\sigma > 0$ (the paper divides by $\operatorname{Var}(D) = \sigma^2$), and square-integrable errors (Mathlib's variance is $0$ off $L^2$). The paper's model (1) asks $\mu \ge 0$; since $\mu$ affects no variance, no sign condition is imposed. Lead times are natural numbers. The statements hold in every period $t$, with no stationarity hypothesis.

Trivializing formalizations are excluded: the orders are computed from the demands, not posited processes with a given covariance; the variances are genuine because every random variable involved is square integrable; and the ratio's denominator is $\sigma^2 > 0$.

A complete development needs variance and covariance calculus for finite linear combinations of independent $L^2$ variables, and, for Eq. (6), the vanishing of the covariance between an odd and an even function of a symmetric random vector. Both are reusable well beyond this mission. Proofs of either target, and general lemmas on variances of linear filters of i.i.d. sequences, are welcome.

Selected references

• F. Chen, Z. Drezner, J. K. Ryan, D. Simchi-Levi, Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information, Management Science 46(3):436–443, 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• H. L. Lee, V. Padmanabhan, S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546
• J. K. Ryan, Analysis of Inventory Models with Limited Demand Information, Ph.D. dissertation, Department of Industrial Engineering and Management Science, Northwestern University, 1997.
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13 (formalized on Prove2Me as SupplyChainTheory.*).

Motivation

A call center has to decide how many agents to staff. In practice the decision is often posed as a service-level constraint rather than a cost trade-off: use the fewest agents for which the expected waiting cost, or the fraction of customers who wait, stays below a target. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; journal version in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) treat this constraint problem in Section 8 of their paper, alongside the cost-minimization problem of Sections 5–7, and show that a simple square-root staffing rule solves it asymptotically as the arrival rate grows.

The rule matters because it is what practitioners use. Under the classical Erlang-C model, the exact optimum requires evaluating the Erlang-C formula over many staffing levels. The asymptotic rule replaces this with a single equation in the Halfin–Whitt function $P$: when the target is a delay probability $\varepsilon$ (Example 8.5 of the paper), it reduces to staffing $\lambda/\mu + P^{-1}(\varepsilon)\sqrt{\lambda/\mu}$ servers.

Timeline. Erlang's formula for the M/M/N delay probability dates from 1917. Halfin and Whitt (Operations Research 29, 1981) identified the limit $P(x)$ of the delay probability under square-root staffing $N = \lambda/\mu + x\sqrt{\lambda/\mu}$ with integer $N$. Jagers and Van Doorn (Operations Research Letters 5, 1986; SIAM Review 33, 1991) studied the continued Erlang loss and delay functions at non-integer numbers of servers, including their convexity, which is what lets the staffing problem be relaxed to a continuous one. Borst, Mandelbaum and Reiman (2000/2004) used these to prove asymptotic optimality of square-root rules for both the cost and the constraint formulations.

Setting

Customers arrive at rate $\lambda$ to $N$ identical servers, each with service rate $\mu > 0$; $\mu$ is fixed while $\lambda \to \infty$. Stability requires $N > \lambda/\mu$. A customer who waits $t$ time units costs $D_\lambda(t)$, where $D_\lambda(0) = 0$, $D_\lambda$ is strictly increasing on $[0,\infty)$ and $\int_0^\infty D_\lambda(t)e^{-\theta t}\,dt < \infty$ for all $\theta > 0$.

The Erlang-C probability of waiting is

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Big\}^{-1},$$

and the conditional waiting cost is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$. The waiting cost per unit time with $N$ servers is

$$K(N,\lambda) = \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda).$$

Given a target $M_\lambda > 0$, the optimal staffing level is the least integer $N > \lambda/\mu$ with $K(N,\lambda) \le M_\lambda$; call it $N^*_\lambda$.

In the continuous parametrization $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$, define $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, the continuous Erlang-C function $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$, and $K_\lambda(x) = \pi_\lambda(x)G_\lambda(x)$. The Halfin–Whitt function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. A staffing function $x_\lambda > 0$ is judged by the rounding gap

$$T_\lambda(x) = \min\big\{|K(\lfloor N_\lambda(x)\rfloor,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - K(N^*_\lambda,\lambda)|\big\}.$$

It is asymptotically optimal when $T_\lambda(x_\lambda)/M_\lambda \to 0$ as $\lambda\to\infty$.

Formalization targets

Goal: Theorem 8.2 (rationalized regime)

Suppose that for some $\kappa > 0$ and $\gamma \in (0,\infty)$, $G_\lambda(\kappa)/M_\lambda \to \gamma$, i.e. the waiting cost is comparable to the target. Let $y^*_\lambda > 0$ solve $P(y)G_\lambda(y) = M_\lambda$. Then

$$\lim_{\lambda\to\infty}\frac{T_\lambda(y^*_\lambda)}{M_\lambda} = 0.$$

Supporting milestones

• Lemma C.1: $G_\lambda$ is strictly convex and decreasing on $(0,\infty)$.
• Section 3: $\pi_\lambda(x) = \pi(N_\lambda(x),\lambda/\mu)$ when $N_\lambda(x)$ is an integer.
• Lemma 8.1: if $z^*_\lambda > 0$ solves $\hat\pi_\lambda(z)\hat G_\lambda(z) = M_\lambda$ and $K_\lambda(z^*_\lambda)/(\hat\pi_\lambda\hat G_\lambda)(z^*_\lambda) \to 1$, then $T_\lambda(z^*_\lambda)/M_\lambda \to 0$.
• Lemma B.1: $P$ is strictly convex and decreasing on $(0,\infty)$.
• Eq. (17): $\limsup a_\lambda/b = \infty$ implies $\liminf P(a_\lambda)/P(b) = 0$ and $\liminf \pi_\lambda(a_\lambda)/\pi_\lambda(b) = 0$.
• Lemma 4.1 (Halfin–Whitt): for bounded $x_\lambda > 0$, $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$; with $x_\lambda \to x$, $\pi_\lambda(x_\lambda)/P(x)\to 1$.

Further target: Theorem 8.6 (efficiency-driven regime)

If $G_\lambda(\kappa)/M_\lambda \to 0$ for every $\kappa > 0$ and $y^*_\lambda > 0$ solves $G_\lambda(y) = M_\lambda$, then $T_\lambda(y^*_\lambda)/M_\lambda \to 0$.

Significance

The theorem certifies the staffing rule used in workforce-management practice: the excess staffing is determined by one scalar equation involving the Gaussian function $P$ and the scaled waiting cost, and rounding the resulting staffing level misses the constraint by a vanishing fraction of the target. Lemma 8.1 is a reusable framework: any approximation $\hat\pi_\lambda\hat G_\lambda$ that is asymptotically exact at the proposed staffing level yields an asymptotically optimal rule, and the paper instantiates it in three regimes (Theorems 8.2, 8.6, 8.9).

The results are proved on paper. To the best of current knowledge none of them, nor the Halfin–Whitt limit for the continuous Erlang-C extension, has a machine-checked proof. A formalization would produce the first verified heavy-traffic limit of the Erlang-C delay probability, a verified continuous Erlang-C extension with its integer identity, and the convexity facts about $P$ and $G_\lambda$ that many staffing papers cite without proof.

Difficulty

The obvious argument is to quote Halfin and Whitt: the delay probability converges to $P(x)$ under square-root staffing, so $P$ can replace the Erlang-C formula. That limit, as published in 1981, is about integer server counts along sequences with a convergent excess-staffing parameter. The paper needs it for the continuous function $H$ at non-integer server counts and for staffing functions that are merely bounded, and it also needs the identity $H(N,\nu) = \pi(N,\nu)$ at integers and the monotonicity of $\pi_\lambda$ in $x$, both cited from Jagers and Van Doorn rather than proved. None of these is in Mathlib. A second obstacle is that the staffing function $y^*_\lambda$ is defined only implicitly by an equation involving $G_\lambda$, which depends on the arbitrary cost functions $D_\lambda$; nothing a priori prevents it from escaping to infinity, outside the range where the Halfin–Whitt approximation applies. Finally, $T_\lambda$ compares integer-level costs given by the Erlang-C formula with a continuous approximation, so both representations of the delay probability are in play at once.

Formalization scope

The queue itself is not formalized: there is no Markov chain and no waiting-time distribution. Every statement is about the closed-form waiting cost $K(N,\lambda)$ with $\pi$ given by the Erlang-C formula, exactly as the paper's analysis is. Conventions, all in the namespace DimCallCenters.Constraint:

• lam : ℝ is the arrival rate (λ is a Lean keyword); limits are Filter.atTop in lam, with μ fixed. Objects indexed by λ ($M_\lambda$, $N^*_\lambda$, $y^*_\lambda$) are functions of lam constrained only for lam > 0.
• WaitModel packages μ > 0 and $D_\lambda$ with $D_\lambda(0) = 0$, strict monotonicity on $[0,\infty)$, and integrability of $D_\lambda(t)e^{-\theta t}$ on $(0,\infty)$ for θ > 0 (the paper's finiteness of $G$; integrability is required because Lean's integral of a non-integrable function is 0).
• $N^*_\lambda$ is a function Nstar : ℝ → ℕ given with its two defining properties (feasible; below every feasible integer level above λ/μ). $y^*_\lambda$ and $z^*_\lambda$ are any positive solutions of their equations; existence and uniqueness are not hypotheses.
• In $T_\lambda$ the round-down term is dropped when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ (an unstable level where $K$ is undefined). This can only enlarge $T_\lambda$.
• Asymptotic relations are limits of ratios. $\limsup = \infty$ and $\liminf = 0$ are stated with ∃ᶠ ("frequently"), $\limsup < \infty$ as eventual boundedness.
• $P$ is defined through explicit $\phi$, $\Phi$, $h$; the formula also gives $P(0) = 1$, used in Lemma 4.1(2) at $x = 0$.
• No hypothesis $\lim_{N\downarrow\lambda/\mu}G(N,\lambda) = \infty$ is added: it is not needed for the statements here.

A trivializing formalization is ruled out: $T_\lambda$ keeps all of the paper's terms and is never replaced by a smaller quantity, and the hypotheses are jointly satisfiable — $D_\lambda(t) = a\sqrt{\lambda/\mu}\,t$ with $M_\lambda = M\lambda$ satisfies (33) for every $\kappa$ with $\gamma = a/(\mu\kappa M)$.

Infrastructure needed: the continuous Erlang-C function and its integer identity; the Halfin–Whitt limit (a Gaussian approximation of Poisson/gamma tails); calculus facts about the normal hazard rate. These are reusable beyond this mission, notably by the sibling missions on the cost-minimization problem. Example 8.5 (delay-probability target with $D_\lambda = 1_{t>0}$) motivates the rule but violates the strict monotonicity of $D_\lambda$, so it is not an instance of the theorem as stated. Contributions on any milestone, and on Theorem 8.9 (quality-driven regime, which needs Lemma 4.2), are welcome.

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• A. A. Jagers, E. A. Van Doorn, On the Continued Erlang Loss Function, Operations Research Letters 5:43–46, 1986.
• A. A. Jagers, E. A. Van Doorn, Convexity of Functions which are Generalizations of the Erlang Loss Function and the Erlang Delay Function, SIAM Review 33:281–282, 1991.

Motivation

How many agents should a call center staff? Telephone call centers employ millions of people, and staffing is their largest cost, so the question is asked every half hour of every day (Gans, Koole & Mandelbaum, 2003). The classical model is the M/M/N (Erlang-C) queue: calls arrive at rate $\lambda$, service times are exponential with mean $1/\mu$, and $N$ agents serve in parallel. Practitioners use the square-root safety staffing rule $N \approx \lambda/\mu + y\sqrt{\lambda/\mu}$, which Halfin and Whitt (1981) justified in the regime where the probability of waiting stays bounded away from $0$ and $1$.

Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published as Operations Research 52(1), 2004) asked when such a rule is actually optimal: given a staffing cost and a waiting cost, which staffing level minimizes total cost as the arrival rate grows? They identified three regimes according to how the two costs compare. This mission formalizes their third case, the quality-driven regime, in which waiting is so expensive relative to staffing that the optimal number of agents exceeds the offered load by more than any fixed multiple of its square root.

Setting

Fix a service rate $\mu > 0$. For every arrival rate $\lambda > 0$ a waiting-cost function $D_\lambda$ assigns cost $D_\lambda(t)$ to a wait of $t$ time units; it satisfies $D_\lambda(0) = 0$, is strictly increasing, and $t \mapsto D_\lambda(t)e^{-\theta t}$ is integrable on $(0,\infty)$ for every $\theta > 0$. A staffing cost $F$, defined for real $N > 0$, is convex and strictly increasing.

For an integer $N > \lambda/\mu$ the probability of waiting is the Erlang-C formula

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Bigl\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Bigr\}^{-1},\qquad \nu = \lambda/\mu,$$

the expected waiting cost of a delayed customer is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$, and the total cost per unit time is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$. An optimal staffing level $N^*_\lambda$ minimizes $C(\cdot,\lambda)$ over the integers $N > \lambda/\mu$.

Write $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$, and for $x > 0$ put $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$, $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, and $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$, where $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$ extends the Erlang-C formula to real $M$. The normalized cost is $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$, and a surrogate cost is $C[z;\hat F,\hat\pi,\hat G] = \hat F(z) + \hat\pi(z)\hat G(z)$. Rounding is measured by $S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda), C(\lceil N_\lambda(x)\rceil,\lambda)\}$.

Two special functions appear. The Halfin–Whitt delay function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. The Stirling-type approximation is

$$Q_\lambda(x) = \frac{\exp\{N_\lambda(x)[1 - r_\lambda(x) + \log r_\lambda(x)]\}}{\sqrt{2\pi N_\lambda(x)}\,(1-r_\lambda(x))},\qquad r_\lambda(x) = \frac{\lambda/\mu}{N_\lambda(x)}.$$

Asymptotic relations are limits of ratios as $\lambda\to\infty$: $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$, and $a_\lambda \stackrel{\infty}{\ll} b_\lambda$ means $a_\lambda/b_\lambda \to 0$.

Formalization targets

Goal: Theorem 7.1

Assume the regime is quality-driven, display (27): $F_\lambda(\kappa) \stackrel{\infty}{\ll} G_\lambda(\kappa)$ for every $\kappa > 0$. Let $y^*_\lambda$ minimize $F_\lambda(y) + Q_\lambda(y)G_\lambda(y)$ over $y > 0$. Then

$$\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.$$

The statement fixes no constants and no rate; it asserts only that rounding the surrogate optimum loses a vanishing fraction of the excess cost.

Milestones

In attack order: Lemma C.1 ($G_\lambda$ strictly convex decreasing); the identity $H(N,\nu) = \pi(N,\nu)$ at integer $N$ (Section 3, p. 12); Lemma 3.1 and Lemma 3.2; Corollary 3.3 (the asymptotic optimality criterion); Lemma B.1 ($P$ strictly convex decreasing); display (15); Lemma 4.1 (Halfin and Whitt); and the first statement of Lemma 4.2, $\pi_\lambda(x_\lambda) \stackrel{\infty}{\approx} Q_\lambda(x_\lambda)$ whenever $x_\lambda\to\infty$.

Significance

Theorem 7.1 completes the paper's picture of optimal staffing. In the rationalized regime the square-root rule with the Halfin–Whitt function $P$ is optimal; in the efficiency-driven regime staffing barely exceeds the load; in the quality-driven regime the staffing excess outgrows $\sqrt{\lambda/\mu}$ and $P$ must be replaced by the Stirling-type expression $Q_\lambda$. The theorem gives a one-dimensional minimization whose solution is asymptotically optimal, which turns a discrete optimization over $N$ into a smooth problem, and it marks the boundary of validity of square-root staffing.

The result is proved in the paper; it is not formalized anywhere to our knowledge. A complete development formalizes the Section 3 framework (shared with the other regimes of the same paper), the convexity of $G_\lambda$ and of $P$, the Halfin–Whitt limit for the continuous extension $\pi_\lambda$, and the Stirling-type asymptotics of the Erlang-C formula. Each of these is a reusable piece of queueing theory in Lean.

Difficulty

The regime theorem itself is short once the framework is in place; the weight lies in the analytic lemmas. Lemma 4.2 requires uniform asymptotics of $\pi_\lambda$ at a staffing excess $x_\lambda$ that may grow at any rate, from barely faster than a constant to faster than $\sqrt{\lambda}$, where neither the central-limit picture of Halfin and Whitt nor a single Stirling expansion covers all cases. Lemma 4.1 concerns the continuous extension $\pi_\lambda$ at non-integer server counts, whereas Halfin and Whitt's theorem is about integer ones. The natural first idea, that the goal follows from Corollary 3.3 by plugging in Lemma 4.2, does not apply directly: Lemma 4.2 only covers staffing excesses that tend to infinity, and nothing in the definition of the true optimum $x^*_\lambda$ or the surrogate optimum $y^*_\lambda$ says that they do.

Formalization scope

Lean represents $\lambda$ as a positive real, and $\lambda\to\infty$ is the filter atTop on $\mathbb{R}$ with $\mu$ fixed. The standing assumptions on $\mu$ and $D_\lambda$ are the structure WaitModel; $F$ is a function argument with hypotheses ConvexOn and StrictMonoOn on $(0,\infty)$. Staffing levels $N$ are natural numbers. Minimizers ($N^*_\lambda$, $x^*_\lambda$, $z^*_\lambda$, $y^*_\lambda$) are function arguments with minimality hypotheses at every $\lambda > 0$, so every statement holds for every choice among ties. Liminf and limsup relations are stated through Filter.Frequently, avoiding boundedness side conditions.

The queue itself (Poisson arrivals, waiting-time law) is not formalized: the paper's analysis and all its theorems concern the closed-form cost $C(N,\lambda)$ with the Erlang-C formula.

Conventions committed to: (i) the goal adds the hypothesis $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$, which the paper asserts on p. 12 to show the continuous optimum exists but which does not follow from its standing assumptions (it holds exactly when $D_\lambda$ is unbounded); (ii) in $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$, since the cost is undefined at unstable levels; (iii) the integrability of $D_\lambda(t)e^{-\theta t}$ is explicit, because a Lean integral of a non-integrable function is $0$; (iv) $P(0) = 1$, the value of formula (11) at $0$; (v) display (15) is stated for $b > 0$, since the ratio $a_\lambda/b$ is undefined at $b = 0$. The instance $\mu = 1$, $F(N) = cN$, $D_\lambda(t) = a\sqrt{\lambda}\,t$ (Section 9) satisfies every hypothesis of the goal, so the goal is not vacuous; taking $\pi_\lambda$ or $G_\lambda$ at Lean default values is ruled out by these explicit domain conditions.

Only the first statement of Lemma 4.2 is a milestone: the second, $\pi_\lambda(x_\lambda)\approx Q(x_\lambda)$ under $x_\lambda \stackrel{\sup}{\le} \lambda^{1/6}$, fails as printed at $x_\lambda = \lambda^{1/6}$. Contributions on the Erlang-C asymptotics, the normal hazard rate, and Laplace transforms of increasing functions are welcome and reusable beyond this mission.

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000 (the version formalized here; every index and page cited in this mission is the report's).
• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone Call Centers: Tutorial, Review, and Research Prospects, Manufacturing & Service Operations Management 5(2):79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071