The OR Formalization Drive

Motivation

Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of $(x,y)$ over $y$ produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.

Timeline:

• 1917: Suslin shows that projections of Borel sets need not be Borel and introduces analytic sets; Lusin proves that analytic sets are universally measurable.
• 1941–1949: Jankov and von Neumann independently prove that an analytic subset of a product admits a selector measurable with respect to the σ-algebra generated by analytic sets.
• 1974: Blackwell, Freedman and Orkin use analytic sets to construct ε-optimal policies in Borel dynamic programming.
• 1978: Bertsekas and Shreve give the treatment used here (§7.6–7.7), including the selection theorem for lower semianalytic functions, Proposition 7.50.

Setting

A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is $\mathscr B_X$. The Baire space is $\mathscr N=\mathbb N^{\mathbb N}$ with the product topology. A set $A\subseteq X$ is analytic if it is empty or the image of $\mathscr N$ under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when $X$ is uncountable.

Three σ-algebras on $X$ are in play. The analytic σ-algebra $\mathscr A_X$ is generated by the analytic sets (Definition 7.19). The universal σ-algebra is $\mathscr U_X=\bigcap_{p}\mathscr B_X(p)$, the intersection over all probability measures $p$ on $(X,\mathscr B_X)$ of the $p$-completions of $\mathscr B_X$ (Definition 7.18). For a function $f$ from $D\subseteq X$ into a Borel space $Y$, $f$ is analytically measurable if $D\in\mathscr A_X$ and $f^{-1}(B)\in\mathscr A_X$ for every $B\in\mathscr B_Y$, and universally measurable if the same holds with $\mathscr U_X$ (Definition 7.20).

Let $R^*=[-\infty,\infty]$. A function $f:D\to R^*$ is lower semianalytic if $D$ is analytic and $\{x\in D\mid f(x)<c\}$ is analytic for every real $c$ (Definition 7.21). For $D\subseteq X\times Y$ write $D_x=\{y\mid (x,y)\in D\}$, $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and define the partial infimum

$$f^*(x)=\inf_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

A selector is a function $\varphi:\mathrm{proj}_X(D)\to Y$ whose graph $\mathrm{Gr}(\varphi)$ lies in $D$.

Formalization targets

Goal: Proposition 7.50

Let $X,Y$ be Borel spaces, $D\subseteq X\times Y$ analytic, and $f:D\to R^*$ lower semianalytic.

(a) For every $\varepsilon>0$ there is an analytically measurable selector $\varphi$ with

$$f[x,\varphi(x)]\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

(b) The set $I$ of points where the infimum is attained is universally measurable, and for every $\varepsilon>0$ there is a universally measurable selector $\varphi$ with $f[x,\varphi(x)]=f^*(x)$ on $I$ and the bounds of (a) off $I$.

The goal fixes no constant beyond the book's $\varepsilon$ and $-1/\varepsilon$.

Milestones

In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 ($\mathscr A_X\subseteq\mathscr U_X$), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:

$$A\subseteq X\times Y\text{ analytic}\ \Longrightarrow\ \exists\,\varphi:\mathrm{proj}_X(A)\to Y\ \text{analytically measurable},\ \mathrm{Gr}(\varphi)\subseteq A.$$

Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).

Significance

Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion $J^*_K=T^K(J_0)$ and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.

All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.

Difficulty

The obvious route to a selector is to choose, for each $x$, a minimizing or near-minimizing $y$. The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set $\{x\mid f^*(x)<c\}$ is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of $A$ by $\mathscr N$, and an argument that the resulting map is measurable with respect to $\mathscr A_X$, which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.

Formalization scope

• A Borel space is a type with a topology satisfying the class IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On $X\times Y$ the product σ-algebra is used; it coincides with $\mathscr B_{X\times Y}$ for separable metrizable spaces (Proposition 7.13).
• Analytic sets are Mathlib's MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).
• $R^*$ is EReal. The book uses $\infty-\infty=\infty$, and Mathlib's EReal uses $\bot+\top=\bot$. No statement of this mission adds infinities of opposite sign; $f^*(x)+\varepsilon$ adds a real number.
• Functions on $D$ and on $\mathrm{proj}_X(D)$ are functions on subtypes. The graph condition $\mathrm{Gr}(\varphi)\subseteq D$ is part of every selector statement.
• Universally measurable means NullMeasurableSet E p for every probability measure p.
• "Analytically measurable" refers to the σ-algebra generated by analytic sets. Replacing it by the power set, dropping the graph condition, or dropping the $-1/\varepsilon$ case would make the selection theorems a consequence of the axiom of choice. The statements rule all three out.

Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on $P(X)$, the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, §7.6–7.7. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Annals of Probability 2 (1974) 926–941. https://doi.org/10.1214/aop/1176996558
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer 1995, §18 (Jankov–von Neumann uniformization), §29 (measurability of analytic sets). https://doi.org/10.1007/978-1-4612-4190-4
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979) 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

A stochastic approximation algorithm is a recursion

$$x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$$

in $\mathbb R^d$, where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$.

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (together with a boundedness condition on the iterates), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$. A probabilistic step then verifies A1 for concrete noise models. Proposition 4.2 does this for martingale difference noise with bounded $q$-th moments, at the price of step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$. This mission formalizes the second verification, Proposition 4.4: when the noise is subgaussian, A1 holds almost surely under the much weaker requirement that $\sum_ne^{-c/\gamma_n}<\infty$ for every $c>0$, which allows step sizes decaying only slightly faster than $1/\log n$. The notes attribute the result to Duflo (1997), see also Kushner and Yin (1997) and Benaïm and Hirsch (1996).

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and let

$$m(t)=\sup\{k\ge0:\ t\ge\tau_k\}$$

be the index of the step that contains time $t\ge0$. For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$, so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$.

Assumption A1 asks that for every $T>0$

$$\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,$$

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$, where

$$\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\bar U(s)\,ds\Big\|.$$

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub-$\sigma$-algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$-measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$. The noise is subgaussian if there is a number $\Gamma>0$ such that for all $n$ and all $\theta\in\mathbb R^d$

$$E\big(\exp\langle\theta,U_{n+1}\rangle\,\big|\,\mathcal F_n\big)\le\exp\Big(\frac\Gamma2\|\theta\|^2\Big).$$

Bounded noise, $\|U_n\|\le\sqrt\Gamma$, is an example.

Formalization targets

Goal: Proposition 4.4

For a Robbins–Monro algorithm with subgaussian noise and a deterministic step sequence such that

$$\sum_ne^{-c/\gamma_n}<\infty\qquad\text{for each }c>0,$$

with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$.

Milestones

1. The exponential supermartingale. For every $\theta\in\mathbb R^d$,

$$Z_n(\theta)=\exp\Big[\sum_{i=1}^n\langle\theta,\gamma_iU_i\rangle-\frac\Gamma2\sum_{i=1}^n\gamma_i^2\|\theta\|^2\Big]$$

is a supermartingale. 2. Directional maximal tail bound. For every unit vector $e$, $\alpha>0$, $n$ and $T>0$,

$$P\Big(\sup_{n<k\le m(\tau_n+T)}\Big\langle e,\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\rangle\ge\alpha\Big)\le\exp\Big(\frac{-\alpha^2}{2\Gamma\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2}\Big).$$

3. Eq. (18). There are $C,C'>0$ depending only on $d$ and $\Gamma$ with

$$P(\Delta(t,T)\ge\alpha)\le C\exp\Big(\frac{-\alpha^2}{C'\int_t^{t+T}\bar\gamma(s)\,ds}\Big)\qquad(t\ge0,\ T>0,\ \alpha>0).$$

4. Block comparison. $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$.

Significance

Proposition 4.4 is the sufficient condition for the ODE method when the noise has Gaussian-type tails. Its step-size condition holds whenever $\gamma_n\log n\to0$, so it admits steps that decrease far more slowly than the $\sum\gamma_n^2<\infty$ of the classical $L^2$ theory; slowly decreasing steps are what practitioners use to keep algorithms responsive. Combined with Proposition 4.1 it shows that the interpolated process of such an algorithm, with bounded iterates, is almost surely an asymptotic pseudotrajectory of the flow of $F$, and the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would add reusable pieces: an exponential supermartingale and maximal inequality for vector-valued martingale differences with a conditional subgaussian bound (Mathlib's conditional subgaussian notion is scalar), a Borel–Cantelli argument along the grid $kT$, and the continuous-time bookkeeping of $\bar U$, $\bar\gamma$ and $\Delta$ shared with the other missions of this series.

Difficulty

The moment method of Proposition 4.2 does not reach this regime: any fixed polynomial moment of the window sums decays only polynomially in the window's step sizes, and under $\sum e^{-c/\gamma_n}<\infty$ alone polynomial bounds are not summable over windows. Exponential tail bounds are needed, and they must be maximal (uniform over the window) and must hold for the norm of a vector, not only for a scalar. The continuous-time deviation $\Delta(t,T)$ involves partial steps at both ends of $[t,t+h]$, so the bound must be stated in terms of $\int_t^{t+T}\bar\gamma$ rather than a sum over whole steps, with constants that do not depend on $t$, $T$ or $\alpha$. Finally, A1 quantifies over all $T>0$: the almost-sure statement must hold on a single event of full probability for every $T$.

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d) (the paper writes $\mathbb R^m$); time is real. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$, and their values at $0$ are unused, as the paper indexes them from $1$. The filtration is a Mathlib Filtration ℕ; $U_{n+1}$ is $\mathcal F_{n+1}$-strongly measurable and integrable, and $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. The subgaussian condition requires $\exp\langle\theta,U_{n+1}\rangle$ to be integrable for every $\theta$ and $n$. The summand $e^{-c/\gamma_n}$ is taken to be $0$ when $\gamma_n=0$, its limiting value. The suprema in A1 and $\Delta$ are taken in $[0,\infty]$; the supremum over an empty range of $k$ is $0$. In Eq. (18) the constants are chosen before the probability space, the algorithm and $t,T,\alpha$.

The following readings are excluded and are not acceptable formalizations: a subgaussian condition that holds vacuously because the exponential is not integrable (Lean's conditional expectation of a non-integrable function is $0$); a summability condition made trivial or false by the convention $c/0=0$; and the conclusion "for each $T$, A1 holds almost surely" in place of "almost surely, A1 holds for all $T$". The second sentence of Proposition 4.4 (the asymptotic pseudotrajectory conclusion) is outside this mission.

All hypotheses are satisfiable: $U=0$, $x=0$, $F=0$, $\Gamma=1$ and $\gamma_n=1/n$ satisfy every one of them.

Contributions welcome: a maximal inequality for nonnegative supermartingales in the form needed here, vector subgaussian tail bounds for martingale transforms with deterministic weights (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997.
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586

Why staffing large call centers is a mathematical question

A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.

The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.

The Erlang-C cost model

Customers arrive at rate $\lambda>0$ and receive exponential service at rate $\mu>0$ per server. The service rate $\mu$ is fixed as $\lambda$ grows. For an integer number of servers $N>\lambda/\mu$, the Erlang-C delay probability $\pi(N,\lambda/\mu)$ is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate $N\mu-\lambda$. Let $D_\lambda(t)$ be the cost of a wait of length $t$. It is strictly increasing on $t\ge0$, satisfies $D_\lambda(0)=0$, and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is

$$G(N,\lambda)=(N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt.$$

The staffing cost $F(N)$ is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real $N>0$. Total cost per unit of time at a stable integer level is

$$C(N,\lambda)=F(N)+\lambda\pi(N,\lambda/\mu)G(N,\lambda).$$

Write $N^*_\lambda$ for any minimizing stable integer level. Ties are permitted. For a positive real offset $x$, define $N_\lambda(x)=\lambda/\mu+x\sqrt{\lambda/\mu}$, $F_\lambda(x)=F(N_\lambda(x))-F(\lambda/\mu)$, and $G_\lambda(x)=\lambda G(N_\lambda(x),\lambda)$. The report extends Erlang-C continuously to $\pi_\lambda(x)$ and writes the incremental continuous objective as $C_\lambda(x)=F_\lambda(x)+\pi_\lambda(x)G_\lambda(x)$. These definitions and the integer-extension identity are from Section 3, printed pages 11–12.

Formalization targets

The report defines the efficiency-driven regime by

$$\text{for every }\kappa>0,\qquad \lim_{\lambda\to\infty}\frac{F_\lambda(\kappa)}{G_\lambda(\kappa)}=+\infty.$$

For each $\lambda>0$, choose $y^*_\lambda>0$ to minimize $F_\lambda(y)+G_\lambda(y)$ over $y>0$. Let $S_\lambda(y)$ be the smaller cost of the stable integer levels immediately below and above $N_\lambda(y)$; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is

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

The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.

What the result gives

The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline $F(\lambda/\mu)$, which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.

The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.

Where the difficulty lies

The simple objective replaces the delay probability $\pi_\lambda(y)$ by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with $\lambda$. Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when $N_\lambda(y)$ is just above $\lambda/\mu$, its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.

Formalization scope and conventions

Lean represents $\lambda$, $\mu$, offsets, and costs as real numbers; arrival-rate limits use the real filter at $+\infty$. Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of $D_\lambda$ on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for $G$ and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on $F$ are convexity and strict increase on positive real staffing levels; $F$ does not depend on $\lambda$.

The report asserts that $G(N,\lambda)$ diverges as $N$ decreases to $\lambda/\mu$, although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.

All formulas are total Lean functions. Their values at $\lambda\le0$, unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of $S_\lambda$ ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.

The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.

Selected references

• Sem Borst, Avi Mandelbaum, and Martin I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000. Report PDF. Theorem 6.1, printed p. 19; Corollary 3.3, printed p. 14; Lemma 4.1, printed p. 15; Lemma C.1, printed p. 40.

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

Motivation

Impulse control models an agent who acts on a random system through discrete interventions, each with a fixed cost: inventory replenishment, cash management, exchange-rate interventions by a central bank. With two agents whose objectives conflict, the problem becomes a nonzero-sum stochastic differential game with impulse controls. Before the work of Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; preprint arXiv:1605.00039), such games had no general verification theorem and few explicit equilibria; the paper supplies both. Its main application, formalized in this mission, is a game between two central banks with different targets for an exchange rate, a two-player version of the exchange-rate control models of Bertola, Runggaldier and Yasuda and of Cadenillas and Zapatero (references [10], [12] of the paper). The paper proves that this game has an explicit one-parameter family of Nash equilibria of threshold type, with closed-form payoffs.

Setting

The state is a real process. Without interventions it is $x+\sigma W_s$, where $W$ is a standard real Brownian motion and $\sigma>0$. Player 1 may shift it up by impulses $\delta\in Z_1=[0,\infty[$, player 2 down by impulses $\delta\in Z_2=]-\infty,0]$:

$$X_s=x+\sigma W_s+\sum_{k:\tau_{1,k}\le s}\delta_{1,k}+\sum_{k:\tau_{2,k}\le s}\delta_{2,k}.$$

Player 1 earns the running payoff $f_1(X_s)=X_s-s_1$, player 2 earns $f_2(X_s)=s_2-X_s$, with $s_1<s_2$. An impulse $\delta$ costs its author $c+\lambda|\delta|$ and pays the opponent $\tilde c+\tilde\lambda|\delta|$. Payoffs are discounted at rate $\rho>0$. The standing assumptions are $c\ge\tilde c\ge0$, $\lambda\ge\tilde\lambda\ge0$, $(c,\lambda)\ne(\tilde c,\tilde\lambda)$ and $1-\lambda\rho>0$.

A strategy of player $i$ is a pair $\varphi_i=(\mathcal C_i,\xi_i)$: an open continuation region $\mathcal C_i\subseteq\mathbb R$ and a continuous impulse map $\xi_i:\mathbb R\to Z_i$. Player $i$ intervenes when the state leaves $\mathcal C_i$, applying the impulse $\xi_i(\text{state})$; player 1 has priority when both want to act. This rule defines the controlled process $X^{x;\varphi_1,\varphi_2}$ and the interventions $(\tau_{i,k},\delta_{i,k})$ inductively. Player $i$'s payoff is

$$J^i(x;\varphi_1,\varphi_2)=\mathbb E_x\Big[\int_0^\infty e^{-\rho s}f_i(X_s)\,ds-\sum_{k}e^{-\rho\tau_{i,k}}(c+\lambda|\delta_{i,k}|)+\sum_{k}e^{-\rho\tau_{j,k}}(\tilde c+\tilde\lambda|\delta_{j,k}|)\Big].$$

A pair is $x$-admissible, $(\varphi_1,\varphi_2)\in\Phi_x$, when these random variables are integrable, $\sup_t|X_t|$ has all moments, and neither player's interventions accumulate in finite time. A Nash equilibrium is an admissible pair from which no player gains by deviating to any strategy that keeps the pair admissible.

The explicit objects are $\theta=\sqrt{2\rho/\sigma^2}$, $\eta=(1-\lambda\rho)/\rho$ and

$$F(y)=2y+\theta c-\eta\log\frac{\eta+y}{\eta-y},\qquad 0<y<\eta .$$

From the zero $\xi$ of $F$ and a free parameter $\tilde s\in\mathbb R$, the formulas (4.20)–(4.21) give thresholds $\bar x_1<\bar x_2$, targets $x_1^*,x_2^*\in]\bar x_1,\bar x_2[$, coefficients $A_{ij}$, the functions $\varphi_i(y)=A_{i1}e^{\theta y}+A_{i2}e^{-\theta y}\pm(y-s_i)/\rho$ and the piecewise candidates $\tilde V_1,\tilde V_2$ of (4.6). These are linear outside $]\bar x_1,\bar x_2[$ and equal $\varphi_i$ inside.

Formalization targets

Goal: Proposition 4.7

For every $\tilde s\in\mathbb R$ and every initial state $x\in\mathbb R$, the threshold strategies

$$\varphi_1^*=\big(]\bar x_1,+\infty[,\ y\mapsto\max(x_1^*-y,0)\big),\qquad \varphi_2^*=\big(]-\infty,\bar x_2[,\ y\mapsto\min(x_2^*-y,0)\big)$$

form an $x$-admissible Nash equilibrium, and

$$J^1(x;\varphi_1^*,\varphi_2^*)=\tilde V_1(x),\qquad J^2(x;\varphi_1^*,\varphi_2^*)=\tilde V_2(x).$$

Milestones

1. (4.17). $F$ has a unique zero $\xi\in(0,\eta)$.
2. Proposition 4.2. For every $\tilde s$, the explicit 8-uple (4.20) satisfies the order conditions (4.7) and the optimality and pasting conditions (4.8)–(4.9). Moreover, $\varphi_2''$ changes sign exactly once in $]x_2^*,\bar x_2[$.
3. Lemma 4.6. The impulses (4.23) maximise $\delta\mapsto\tilde V_i(x+\delta)-c-\lambda|\delta|$, and the intervention operators satisfy (4.24): $\{\mathcal M_1\tilde V_1-\tilde V_1<0\}=]\bar x_1,\infty[$ and $\{\mathcal M_2\tilde V_2-\tilde V_2<0\}=]-\infty,\bar x_2[$.
4. Condition (v). The equilibrium pair is $x$-admissible for every $x$. This includes the integrability (4.26) of the discounted intervention costs.

Milestones 1–3 are deterministic real analysis; milestone 4 and the goal are probabilistic.

Significance

The result gives explicit equilibria, with explicit thresholds and payoffs, for a nonzero-sum stochastic game with impulse controls. Such games rarely have closed-form solutions. The equilibria form a continuum indexed by $\tilde s$: equilibrium payoffs are not unique, and every equilibrium in the family is a translate of a fixed interval policy. The explicit formulas also support the comparative statics of Section 4.4, where the continuation region widens as the fixed cost grows.

Proposition 4.7 is proved in the paper by applying its verification theorem (Theorem 3.3) to $\tilde V_1,\tilde V_2$. The admissibility estimate (4.26) is written out only for initial states $x\in\{x_1^*,x_2^*\}$; the general case is said to be similar. As far as is known, none of these results has a machine-checked proof. A formal proof would check every regularity, pasting and admissibility condition. It would also yield a reusable pathwise construction of impulse-controlled Brownian motion.

Difficulty

The deterministic milestones need careful algebra with nested logarithms and square roots. Proving Lemma 4.6 requires the global shape of $\tilde V_i(y)\pm\lambda y$, which needs the sign pattern of $\varphi_2''$ from Proposition 4.2, not only local conditions at the thresholds.

The goal is harder. The Nash inequality must hold against every admissible deviation: any open continuation region and any continuous impulse map, not only threshold strategies. Comparing payoffs therefore needs a verification argument, namely Itô's formula for a function that is $C^2$ only piecewise and $C^1$ across the thresholds, applied along a process with an unbounded number of jumps, plus a localisation that uses the moment condition (2.8). Admissibility needs a renewal-type bound on the discounted number of interventions, built from i.i.d. exit times of Brownian motion from an interval.

Formalization scope

The Lean development lives in the namespace ImpulseGames.LinearGame.

• The constants and standing assumptions are a structure Model with the proposition Model.Standing. The added hypothesis $c>0$ appears in every statement that uses $\xi$: with $c=0$, which the standing assumptions allow, $F$ has no zero in $(0,\eta)$ and the family (4.20) does not exist.
• The zero $\xi$ is a parameter, constrained by $\xi\in(0,\eta)$ and $F(\xi)=0$. Milestone 1 shows that exactly one such $\xi$ exists.
• The Brownian motion is Mathlib's IsBrownianReal W P on a probability space, with time in $\mathbb R_{\ge0}$. Definition 2.2 is formalized pathwise: exit times $\inf\{s>\tilde\tau_{k-1}:\tilde X^{k-1}_s\notin\mathcal C_i\}$ in $[0,\infty]$ with $\inf\emptyset=\infty$, the tie rule favouring player 1, and $e^{-\rho\cdot\infty}=0$ for the tail of each impulse control. No SDE or stochastic integral appears in any statement; the uncontrolled dynamics are $\zeta+\sigma(W_s-W_t)$.
• Payoffs are Bochner expectations. $\Phi_x$ requires every random variable of (2.7) to be integrable, so no deviation can obtain the default value $0$ of a non-integrable expectation. The moment condition (2.8) is stated with an extended-real supremum, and (2.9) is read almost surely.
• The Nash condition quantifies over all strategies of Definition 2.1. A formalization that restricts deviations to threshold strategies would be a different, weaker theorem and is excluded. Likewise, the equilibrium payoffs $\tilde V_i$ are the explicit formulas (4.6), never defined as "the equilibrium value".

Two slips of the page are corrected. First, the paper's impulse maps $\xi_i^*(y)=x_i^*-y$ are not $Z_i$-valued on all of $\mathbb R$; they are replaced by $\max(x_1^*-y,0)$ and $\min(x_2^*-y,0)$, which agree with them wherever each player acts. Second, in Lemma 4.6 the maximiser (4.23) is not unique when $\lambda=\tilde\lambda$, in the opponent's intervention region (all impulses tie there). The statement asserts maximality everywhere and uniqueness outside that region.

A complete development needs: elementary real analysis for milestones 1–3; a pathwise theory of piecewise-defined processes; an Itô formula for Brownian motion with $C^1$, piecewise-$C^2$ functions; and exit-time estimates for Brownian motion. The last two are reusable well beyond this mission. Proofs of the deterministic milestones are welcome independently of the stochastic part.

Selected references

• R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-sum stochastic differential games with impulse controls: a verification theorem with applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0989 (accepted manuscript: arXiv:1605.00039v4, https://arxiv.org/abs/1605.00039)
• G. Bertola, W. J. Runggaldier, K. Yasuda, On classical and restricted impulse stochastic control for the exchange rate, Applied Mathematics and Optimization 74(2), 423–454, 2016.
• A. Cadenillas, F. Zapatero, Classical and impulse stochastic control of the exchange rate using interest rates and reserves, Mathematical Finance 10(2), 141–156, 2000.
• B. Øksendal, A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer, 2007.

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.