Probability

Motivation

Many service systems do not receive random, memoryless traffic: customers are given appointments. Outpatient clinics, airport runways, container terminals and delivery slots all schedule arrivals on a regular grid, and the actual arrival deviates from the appointment by a random lateness or earliness. A queue fed by such scheduled traffic is a basic model for these systems, going back to Winsten (1959) and Mercer (1960, 1973), and Chen and Zhao (1997) used it with deterministic service times to model aircraft landings, proving stability under bounded perturbations.

Classical queueing theory says that a single-server queue fed by stationary traffic is stable when the mean work brought per unit time is below the service rate, and unstable when it is above (Loynes 1962). The boundary case, critical loading, is unstable for renewal traffic with non-degenerate interarrival times: the workload grows like $\sqrt t$. Araman and Glynn ask what happens at critical loading when the traffic is scheduled and every customer brings the same amount of work, and show that the answer depends only on the right tail of the arrival perturbations.

Timeline. Winsten (1959) and Mercer (1960, 1973) analysed queues with scheduled arrivals and obtained waiting-time distributions in implicit form. Loynes (1962) proved the stability dichotomy for stationary input. Kingman (1962) showed that the heavy-traffic limit of the S/G/1 queue coincides with that of D/G/1 when perturbations are positive with finite mean. Chen and Zhao (1997) studied the S/D/1 queue with bounded perturbations. Araman and Glynn (2012) obtained a fractional-Brownian functional limit for scheduled traffic with infinite-mean perturbations, and Araman, Chen, Glynn and Xia (2022) showed that S/D/1 queues with Pareto-like perturbations behave unlike D/D/1 and G/D/1 queues. The present note (arXiv 2022; Operations Research technical note, 2025) settles stability at critical loading.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathbb P)$ and a scheduling interval $h>0$. Customer $j\in\mathbb Z$ is scheduled at time $jh$. Its perturbation $\xi_j$ is a real random variable, and the $\xi_j$ are independent and identically distributed with $\mathbb E|\xi_0|<\infty$. A uniform shift $U$, uniform on $[0,1]$ and independent of $\xi=(\xi_j)_{j\in\mathbb Z}$, makes the arrival process stationary. Customer $j$ arrives at

$$A_j = jh + hU + \xi_j ,$$

and for $t\ge0$ the arrival count is $N(t)=\#\{j : A_j\in(0,t]\}$, so $N(0)=0$.

A single server works at unit rate and every customer brings exactly $h$ units of work (the S/D/1 queue; "D" for deterministic service $V_j=h$). Since one customer is scheduled per $h$ time units, the queue is critically loaded. The system is empty at time $0$, and the workload at time $t\ge0$ is

$$W(t)=\sup_{0\le s\le t}\Big(h\big(N(t)-N(s)\big)-(t-s)\Big).$$

The proof runs in reversed time. With reversed arrival times $R_j = jh+Uh-\xi_j$, let

$$\Lambda(s)=h\cdot\#\{j: R_j\in(0,s]\},\qquad M(t)=\sup_{0\le s\le t}\big(\Lambda(s)-s\big).$$

Write $\xi_0^+=\max(\xi_0,0)$. "$\xi_0^+$ is a bounded random variable" means that $\xi_0\le c$ almost surely for some constant $c$.

Formalization targets

Goal: Theorem 1

$$\exists\,W(\infty)\ \text{finite-valued with}\ W(t)\Rightarrow W(\infty)\ (t\to\infty)\quad\Longleftrightarrow\quad \exists c,\ \ \xi_0\le c\ \text{a.s.}$$

The statement makes no assumption beyond the standing model. In particular the left tail of $\xi_0$ is arbitrary (only $\mathbb E\xi_0^-<\infty$).

The steps of the published proof (milestones)

1. Loynes representation: $W(t)\overset{\mathcal D}{=}M(t)$ for each $t\ge0$.
2. Early customers: $\beta_1(s)\le\Gamma_1$ for all $s$ and $\mathbb E\Gamma_1<\infty$.
3. Upper decomposition: $\#\{j : R_j\in(0,s]\}\le\beta_1(s)+\lfloor s/h\rfloor+1+\beta_2(s)$.
4. Late customers under bounded perturbations: if every $\xi_j\le c$, then $\beta_2(s)\le\lfloor c/h\rfloor+1$.
5. Sufficiency: if $\xi_0^+$ is bounded, then $\sup_{s\ge0}(\Lambda(s)-s)<\infty$ a.s.
6. $Y_n<\infty$ for all $n$ and $\Gamma_2<\infty$, a.s.
7. Lower decomposition: $n+\tilde Y_n\le\Lambda(nh)/h+Y_n+\Gamma_2$.
8. Ergodic recurrence: $\frac1n\sum_{j\le n}I(Y_j\le l)\to\mathbb P(Y_0\le l)$ a.s.
9. If $\xi_0^+$ is unbounded, then $\mathbb P(\tilde Y_0>r)>0$ for every $r$.
10. If $\xi_0^+$ is unbounded and $\mathbb P(Y_0\le l)>0$, then $Y_n\le l$ and $\tilde Y_n>r$ for infinitely many $n$, a.s.
11. Necessity: if $\xi_0^+$ is unbounded, then $\sup_{s\ge0}(\Lambda(s)-s)=\infty$ a.s.

Here $\beta_1,\beta_2$ count reversed arrivals in $(0,s]$ of customers $j\le-1$ and $j\ge\lfloor s/h\rfloor+1$; $\Gamma_1,\Gamma_2,Y_n,\tilde Y_n$ are the counts $\sum_{j\ge1}I(-\xi_{-j}>(j-1)h)$, $\sum_{j\ge1}I(\xi_j\ge(j-1)h)$, $\sum_{j\ge1}I(-\xi_{n+1-j}>(j-2)h)$ and $\sum_{j\ge1}I(\xi^+_{n+j}\ge(j+2)h)$.

Significance

The result. Theorem 1 shows that, unlike renewal traffic, scheduled traffic can keep a critically loaded queue stable, and it identifies exactly when: only late arrivals (the right tail of $\xi_0$) can destabilise the queue, while arbitrarily early arrivals cannot. For appointment systems this says that a server whose capacity exactly matches the schedule has a finite stationary backlog precisely when lateness is bounded, so tardiness, not earliness, determines whether waiting times stay bounded. It complements Corollary 1 of the same note, a diffusion limit $t^{-1/2}W(t)\Rightarrow\sigma X(1)$ for random service times at critical loading.

Formalizing it. The theorem is proved in the paper, but its proof contains several misprints: an identity that omits a term and has an infinite summand, a bound with a wrong constant, a sign error in $Y$, a false inequality $\beta_2(s)\ge\tilde Y_{k(s)}$, and a conditional Borel–Cantelli step applied to non-adapted events. The milestones of this mission state the corrected inequalities, each checked by hand on small instances. A machine-checked proof would settle the argument. No part of it is formalized anywhere at present.

Difficulty

The forward workload $W(t)$ is not monotone in $t$, so its convergence cannot be read off from its paths; the proof needs the time reversal to a monotone running maximum $M(t)$, and the reversal of a perturbed lattice requires its stationarity under the uniform shift. In the unstable direction the obvious first idea is to show that $\Lambda(s)-s$ is large for a fixed large $s$. That fails: for each fixed $s$ the overshoot is a tight random variable. Large values occur only along random times at which many customers just after $s$ are very late while few customers just before $s$ are very early, and producing infinitely many such times needs an ergodic or Borel–Cantelli argument over a dependent stationary sequence. Mathlib has no pointwise ergodic theorem and no conditional Borel–Cantelli lemma, so this step needs new infrastructure.

Formalization scope

All declarations live in the namespace ScheduledQueue.Stability. The standing model is a bundle ScheduledInput P ξ U (measurable, i.i.d. via iIndepFun and IdentDistrib, Integrable (ξ 0), HasLaw U uniform on $[0,1]$, and independence of U from the whole sequence). Customers are indexed by ℤ, time by ℝ, and $t\to\infty$ is the atTop filter on ℝ. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is a probability measure on $\mathbb R$.

Conventions that differ from the printed page:

• the workload is $\sup_{0\le s\le t}(h(N(t)-N(s))-(t-s))$; the printed $\sum_{i=N(s)}^{N(t)}V_i$ counts customer $N(s)$ and would give $W(0)=h\ne0$, contradicting the theorem's hypothesis $W(0)=0$;
• $N$ counts arrivals in half-open intervals $(0,t]$ (the printed closed intervals are not additive; both agree a.s. at fixed times);
• the proof's displays are corrected: the upper decomposition (the page's identity omits $j=0$ and its $\beta_4$ is infinite, and "$M(t)\le\max\beta_1+\max\beta_2$" mixes units), the $\beta_2$ bound ($\lfloor c/h\rfloor+1$ instead of the printed, false $(\lfloor c\rfloor+1)/h$), the sign and range of $Y_n$, and the lower decomposition (the printed $\beta_2(s)\ge\tilde Y_{k(s)}$ is false);
• the Borel–Cantelli milestone states the conclusion ("infinitely many $n$") rather than the stopping times $\tau_i$.

Every count used inside a pointwise inequality is an extended natural number (Set.encard), so that statements such as "$\Gamma_2<\infty$ a.s." are not satisfied by the junk value $0$ of an infinite Set.ncard. The goal's limit is a probability measure on $\mathbb R$, not on the extended reals, because there "$W(t)\Rightarrow\infty$" would also count as convergence. "Bounded" means bounded almost surely, not pointwise. Measurability of $W(t)$ is part of the conclusion of the "if" direction, not a hypothesis.

A complete development needs the stationarity and time reversal of the perturbed lattice point process, tail-sum bounds $\sum_j\mathbb P(X>(j-1)h)\le\mathbb EX/h+1$, a pointwise ergodic theorem for i.i.d. shifts (or a Lévy-type Borel–Cantelli argument), and measurability of suprema over intervals. The ergodic theorem and the reversal lemma are reusable well beyond this mission. Proofs of individual milestones, in any order, are welcome.

Selected references

• V. F. Araman and P. W. Glynn, Stability of a Queue Fed by Scheduled Traffic at Critical Loading, arXiv preprint, 2022; Operations Research (technical note), 2025. https://arxiv.org/abs/2212.04164v1
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781
• H. Chen and Y. J. Zhao, A new queueing model for aircraft landing process, AIAA, 1997. https://doi.org/10.2514/6.1997-3737
• V. F. Araman, H. Chen, P. W. Glynn and L. Xia, On a single server queue fed by scheduled traffic with Pareto perturbations, Queueing Systems 100, 61–91, 2022.
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society, Series B 24(2), 383–392, 1962. http://www.jstor.org/stable/2984229
• A. Mercer, Queues with scheduled arrivals: a correction, simplification and extension, Journal of the Royal Statistical Society, Series B 35(1), 104–116, 1973.
• J. L. Doob, Stochastic Processes, Wiley, 1953.

Why a fluid limit for matching markets

Two-sided platforms (ride hailing, delivery, freelancing, logistics) collect demand and supply requests over a matching cycle and then clear them with an optimization problem. When such a platform runs an experiment, treated and control units compete for the same supply, so the outcome of one unit depends on the treatment of others. Interference bias of this kind is the subject of Bright, Delarue and Lobel, Reducing Marketplace Interference Bias Via Shadow Prices (arXiv:2205.02274v4; Management Science, 2025). Their analysis of estimators, including the shadow-price estimator built from linear-programming duals, is carried out in a deterministic fluid limit. Theorem 1 of the paper justifies that step: as the market becomes dense, the expected matching value per unit of density converges to the optimal value of a deterministic linear program with the arrival rates as inputs.

The same kind of statement, the expected value of a random linear program converging to the value of the program at the mean data, is also used in network revenue management and in stochastic matching, where fluid linear programs serve as benchmarks.

Setting

Network. There are $n_d$ demand types and $n_s$ supply types. A directed network has one demand node $u^d_i$ per demand type (a sink), one supply node $u^s_j$ per supply type (a source) and a finite set $\mathcal U_*$ of intermediate nodes. Every arc $(u,w)$ carries a value $v_{u,w}\in\mathbb R$ and a capacity $k_{u,w}\ge 0$.

Matching program. For a density $\tau$, demand vector $d$ and supply vector $s$, $\Phi_\tau(d,s)$ is the maximum of $\sum_{(u,w)} v_{u,w}x_{u,w}$ over flows $x$ with inflow at most $d_i$ at $u^d_i$, outflow at most $s_j$ at $u^s_j$, flow balance at every intermediate node and $0\le x_{u,w}\le\tau k_{u,w}$ (display (2), p. 7). Write $\Phi:=\Phi_1$. Without intermediate nodes this is a capacitated bipartite transportation problem.

Random counts. Demand units of type $i$ arrive at rate $\lambda_i\ge 0$ and supply units of type $j$ at rate $\pi_j\ge 0$. At density $\tau$ the numbers of units collected in one cycle are independent Poisson counts

$$D^{\tau,\lambda}_i\sim\mathrm{Poisson}(\lambda_i\tau),\qquad S^\tau_j\sim\mathrm{Poisson}(\pi_j\tau).$$

Treatment effect. If a treatment changes the demand rates from $\lambda$ to $\lambda+\beta$ (with $\lambda+\beta\ge 0$), the global treatment effect at density $\tau$ is $\Delta^\tau=\frac1\tau\mathbb E[\Phi_\tau(D^{\tau,\lambda+\beta},S^\tau)-\Phi_\tau(D^{\tau,\lambda},S^\tau)]$ (Definition 1, p. 8).

Formalization targets

Goal: Theorem 1, display (7), p. 12

$$\lim_{\tau\to\infty}\mathbb E\Big[\frac1\tau\,\Phi_\tau\big(D^{\tau,\lambda},S^\tau\big)\Big]=\Phi(\lambda,\pi),$$

for every network, every $\lambda\ge 0$ and every $\pi\ge 0$, along integer densities $\tau$. No rate of convergence and no constant is fixed.

Milestones

1. Lemma 1 (p. 37), scaling. For integer $d,s\ge 0$ and $\tau>0$, $\frac1\tau\Phi_\tau(d,s)=\Phi(\frac1\tau d,\frac1\tau s)$, and $x$ is optimal on the right if and only if $\tau x$ is optimal on the left.
2. Poisson tail bound (proof of Lemma 2, p. 38). For $V\sim\mathrm{Poisson}(\lambda_0)$, $\mathbb P(V\ge t)\le e^{-t}$ for every $t\ge 7\lambda_0$ (Janson, Łuczak and Ruciński 2000, Corollary 2.4).
3. Lemma 2 (p. 38). If $X_n\sim\mathrm{Poisson}(\lambda n)$ for $n\ge 1$, then $Z=\sup_{n\ge1}X_n/n$ has finite mean, whatever the joint law of the $X_n$.

Companion: Corollary 1, display (8), p. 13

$$\lim_{\tau\to\infty}\Delta^\tau=\Phi(\lambda+\beta,\pi)-\Phi(\lambda,\pi).$$

Significance

Theorem 1 is the bridge between the paper's stochastic model and its deterministic analysis. Corollary 1 follows from it and identifies the estimand $\Delta=\Phi(\lambda+\beta,\pi)-\Phi(\lambda,\pi)$. Every fluid-limit result of the paper is stated about this deterministic quantity: that the RCT estimator overestimates the treatment effect (Theorem 2), and that in a symmetric experiment the shadow-price estimator is no more biased than the RCT estimator (Theorem 4). Without Theorem 1 those results describe a linear program, not the experiment.

The result is proved in the paper (Appendix C.1, pp. 37–39). As far as a search of the Prove2Me catalogue shows, it has not been formalized: the catalogue has fluid limits of queueing networks and several Poisson concentration bounds, but no law of large numbers for the value of a random network-flow program. A formal development would provide a reusable definition of the capacitated network-flow program with supply and demand bounds, its scaling identity, and an integrability tool for suprema of scaled Poisson counts. The two other missions of this series, on the shadow-price estimator in the fluid limit and in finite samples, use the same network program.

Difficulty

The obvious argument is: $\frac1\tau D^\tau\to\lambda$ and $\frac1\tau S^\tau\to\pi$, $\Phi$ is continuous, so the expectations converge. Each step needs care.

• The counts at different densities are defined only through their laws. A pathwise limit needs a coupling of the counts across $\tau$, which is not part of the statement.
• Continuity of $\Phi$ in its right-hand side, including at data where some $\lambda_i$ or $\pi_j$ is zero, is a statement about the value function of a parametric linear program. Mathlib has no theory of LP value functions.
• Passing the limit inside the expectation needs a dominating function. The paper builds one from the supremum of scaled Poisson counts (Lemma 2), whose integrability rests on the Poisson tail bound. That bound is not in Mathlib either.

Formalization scope

Representation.

• Demand types are Fin nd and supply types Fin ns; Lean index $i$ is the paper's type $i+1$.
• A network is a structure with arc type E and intermediate-node type I. Each arc's tail is a supply or intermediate node and its head is a demand or intermediate node, which builds in the source/sink structure. Values are real and capacities nonnegative.
• $\Phi_\tau(d,s)$ is the supremum of the objective over the feasible set of (2). For nonnegative data this set contains $0$ and lies in the box $[0,\tau k]$, so the supremum is a maximum.

Probability.

• The count law at density $\tau$ is the product of independent Poisson laws on $\mathbb N^{n_d}\times\mathbb N^{n_s}$. Independence across types and between demand and supply is the paper's reading of a Poisson process per type; it is used by the proofs but not written out.
• Expectations are Bochner integrals. The integrand of the goal is bounded by $\sum|v_{u,w}|k_{u,w}$, and every function on the countable count space is measurable, so the expectation is genuine and not the junk value $0$.
• The limit is taken along integer $\tau\to\infty$, as on p. 12.
• In Lemma 2, $\max_{n\ge1}$ is read as a supremum in $[0,\infty]$, and "finite mean" as a finite lower Lebesgue integral.

Ruled out. A trivializing formalization is excluded: the expectation is taken against the Poisson laws with means $\lambda_i\tau$ and $\pi_j\tau$, with the factor $1/\tau$ inside the expectation, not against point masses at the rates or in the rescaled form $\mathbb E[\Phi(\frac1\tau D^\tau,\frac1\tau S^\tau)]$. No hypothesis beyond $\lambda,\pi\ge 0$ is imposed.

Not stated.

• The second sentence of Theorem 1, the almost-sure convergence of optimal primal and dual solutions. It assumes unique optima only inside its proof and needs a coupling across $\tau$ that the paper does not construct.
• Lemma 1's "$z^*=\tau x^*$" presupposes unique optima. It is stated as the equivalence "$x$ is optimal for $\Phi(\frac1\tau d,\frac1\tau s)$ if and only if $\tau x$ is optimal for $\Phi_\tau(d,s)$".

The statements follow arXiv:2205.02274v4. Its printed slips are corrected as disclosed in each item's Formalization Note.

Infrastructure needed.

• Monotonicity and continuity of the value of a capacitated linear program in its right-hand side.
• The Poisson Chernoff bound.
• Convergence in probability of scaled Poisson counts.

The network-program definition and the Poisson tail bound are reusable beyond this mission. Contributions toward any of these are welcome.

Selected references

• I. Bright, A. Delarue, I. Lobel, Reducing Marketplace Interference Bias Via Shadow Prices, arXiv preprint, v4, 2024; Management Science, 2025. https://arxiv.org/abs/2205.02274v4
• S. Janson, T. Łuczak, A. Ruciński, Random Graphs, Wiley, 2000, Corollary 2.4. https://doi.org/10.1002/9781118032718

Motivation

Two-sided platforms (ride hailing, delivery, freight, cloud capacity) test product changes with user-split experiments: each arriving demand unit is assigned to treatment with probability $\rho$ and to control otherwise. Treated and control units then compete for the same supply, so the outcome of one group depends on the size of the other. This interference biases the standard estimator that compares the value earned by the two groups and rescales by $\rho$ and $1-\rho$ (Blake and Coey, 2014; Johari, Li, Liskovich and Weintraub, 2022).

Bright, Delarue and Lobel (arXiv:2205.02274v4, 2024; Management Science 2025) model each matching cycle as a linear program and propose a shadow-price estimator that weights the observed demand counts by the marginal values of demand in the experiment's matching problem. This mission formalizes their finite-sample result, Theorem 6: at every market size, the shadow-price estimator is unbiased for the slope of the expected value function at the experiment state. The fluid-limit comparison with the standard estimator (Theorem 4) and the fluid limit of the matching value (Theorem 1) are the subjects of the other two missions of this series.

Setting

A matching network has one sink node $u^d_i$ for each of $n_d$ demand types, one source node $u^s_j$ for each of $n_s$ supply types, a finite set of intermediate nodes, and arcs that leave a supply or intermediate node and enter a demand or intermediate node. Arc $(u,w)$ has a value $v_{u,w}\in\mathbb R$ and a capacity $k_{u,w}\ge0$. For a density $\tau>0$, demand $d$ and supply $s$, the matching value $\Phi_\tau(d,s)$ is the optimal value of the linear program (2): maximize $\sum v_{u,w}x_{u,w}$ subject to inflow at $u^d_i$ at most $d_i$, outflow at $u^s_j$ at most $s_j$, flow balance at intermediate nodes, and $0\le x_{u,w}\le\tau k_{u,w}$. Write $\Phi=\Phi_1$ and $e_i$ for the $i$-th unit vector.

Rates are a control demand rate $\lambda\ge0$, a treatment effect $\beta$ with $\lambda+\beta\ge0$, and a supply rate $\pi\ge0$. In the partial-treatment market with treated fraction $\eta\in[0,1]$, the demand counts $D^{\tau,\lambda+\eta\beta}_i\sim\mathrm{Poisson}((\lambda_i+\eta\beta_i)\tau)$ and supply counts $S^{\tau,\pi}_j\sim\mathrm{Poisson}(\pi_j\tau)$ are independent. The finite-sample partial-treatment value function is

$$\Psi_\tau(\eta)=\mathbb E\Big[\tfrac1\tau\,\Phi_\tau\big(D^{\tau,\lambda+\eta\beta},S^{\tau,\pi}\big)\Big],$$

and the global treatment effect is $\Delta^\tau=\Psi_\tau(1)-\Psi_\tau(0)$.

In the experiment with treatment fraction $\rho\in(0,1)$, the platform observes independent control counts $D^{\tau,\mathrm{control}}_i\sim\mathrm{Poisson}((1-\rho)\lambda_i\tau)$, treatment counts $D^{\tau,\mathrm{treatment}}_i\sim\mathrm{Poisson}(\rho(\lambda_i+\beta_i)\tau)$ and supply counts, and solves the matching problem at $D^{\tau,\mathrm{experiment}}=D^{\tau,\mathrm{control}}+D^{\tau,\mathrm{treatment}}$. The negative-demand subgradient is $a^-_i=\Phi_\tau(d,s)-\Phi_\tau(d-e_i,s)$ and the positive one $a^+_i=\Phi_\tau(d+e_i,s)-\Phi_\tau(d,s)$. The shadow-price estimator is

$$\hat\Delta^\tau_{SP}=\frac1\tau\,A^{\tau,\mathrm{experiment},-}\cdot\Big(\frac1\rho D^{\tau,\mathrm{treatment}}-\frac1{1-\rho}D^{\tau,\mathrm{control}}\Big),$$

with $A^{\tau,\mathrm{experiment},-}$ the vector $a^-$ at $(D^{\tau,\mathrm{experiment}},S^\tau)$.

Formalization targets

Goal: Theorem 6 (p. 24)

For every network, all rates as above, every $\rho\in(0,1)$ and every $\tau>0$, $\Psi_\tau$ is differentiable at $\rho$ and

$$\mathbb E\big[\hat\Delta^\tau_{SP}\big]=\Psi_\tau'(\rho).$$

Milestones

1. Lemma 1 (p. 37): $\frac1\tau\Phi_\tau(d,s)=\Phi(\frac1\tau d,\frac1\tau s)$ for integer $d,s$, and optimal flows correspond by the factor $\tau$.
2. Theorem 7 (p. 24): with integer $d,s$ and integer scaled capacities, $\Phi_\tau(d\pm\varepsilon,s)$ is linear in $\varepsilon\ge0$ on $\sum_i\varepsilon_i\le1$, with slopes $a^+$ and $a^-$.
3. Lemma 3 (p. 51): for $D\sim\mathrm{Poisson}(\lambda)$ and $g$ of linear growth, $\frac{\partial}{\partial\lambda}\mathbb E[g(x,D)]=\mathbb E[g(x,D+1)-g(x,D)]$.
4. Lemma 4 (p. 52): $\frac{\partial}{\partial\lambda_i}\mathbb E[\Phi(D,S)]=\mathbb E[A^+_i]$ for Poisson demand and supply.
5. (32) (p. 54): given the total demand, the expected treatment and control counts of type $i$ are the total times $\rho(\lambda_i+\beta_i)/(\lambda_i+\rho\beta_i)$ and $(1-\rho)\lambda_i/(\lambda_i+\rho\beta_i)$.
6. Lemma 5 (p. 53): $\mathbb E[Df(D)]=\lambda\,\mathbb E[f(D+1)]$ for $D\sim\mathrm{Poisson}(\lambda)$.

Companion: Corollary 2 (p. 24)

If $|\Psi_\tau''|\le M$ on $[0,1]$, then $|\mathbb E[\hat\Delta^\tau_{SP}]-\Delta^\tau|\le M/2$.

Significance

Theorem 6 says the shadow-price estimator measures, in expectation, the derivative of the value function at the experiment state, for every finite market and for every network, with no uniqueness assumption on optimal dual solutions. It is what licenses the estimator outside the fluid limit, where the matching problem is frequently degenerate. Corollary 2 turns it into an explicit bias bound in terms of the curvature of $\Psi_\tau$, and the same identity integrated over a uniformly random $\rho$ gives an unbiased estimator of $\Delta^\tau$ (Theorem 8 of the paper, not part of this mission).

The paper proves Theorem 6 in Appendix C.4.4; none of the statements has been machine-checked. The formalization adds a precise account of the junk cases a proof on paper passes over (infeasible programs at zero demand, the choice of subgradient), a Lean development of Poisson derivative identities that does not exist in Mathlib, and a network-flow LP layer shared with the two sibling missions. Theorem 7 is a discrete-concavity statement about network-flow values that is of independent interest.

Difficulty

The two sides of (14) are expectations under different laws: the right-hand side differentiates an expectation over the total demand in its Poisson means, while the left-hand side is an expectation over the separately observed treatment and control counts of a quantity that depends on both. Differentiating needs control of an infinite Poisson series uniformly in the mean, and differentiability in $\eta$ is a joint statement about all $n_d$ means at once. Computing the left-hand side with the law of the total demand alone loses exactly the information the estimator uses. The finite-sample matching problem is often degenerate, so its optimal duals are not unique; the paper notes that the particular selection $a=a^-$ is what makes Theorem 6 hold (p. 25), so no argument that treats the duals as interchangeable can work. Theorem 7 is a discrete-concavity statement about network-flow values that needs integrality of the data, and is the hardest combinatorial statement of the mission.

Formalization scope

Demand types are Fin nd and supply types Fin ns (Lean index $i$ is the paper's type $i+1$). A network is a structure with arcs carrying their endpoints by type, values and nonnegative capacities. $\Phi_\tau(d,s)$ is the supremum of the objective over the feasible set; for nonnegative arguments the set contains $x=0$ and lies in the box $[0,\tau k]$, so it is a maximum. Poisson vectors are products (Measure.pi) of Mathlib's poissonMeasure, and the experiment law is the product of the control, treatment and supply laws; independence across all counts is the paper's standing reading of one Poisson process per type. Derivatives are HasDerivAt, so every differentiability claim is part of a conclusion. Statements follow arXiv:2205.02274v4; its printed slips are corrected as disclosed in each item: (16) carries $d_i\ge1$ wherever $\varepsilon_i>0$, Lemma 1's uniqueness presupposition becomes a correspondence of optimal sets, Lemma 4 is stated for arbitrary capacities so that it covers $\Phi_\tau$, and (32) drops the redundant conditioning on supply.

Standing hypotheses are $\lambda\ge0$, $\lambda+\beta\ge0$, $\pi\ge0$, $0<\rho<1$, $\tau>0$; Assumptions 1–3 of the paper are not hypotheses of Theorem 6, because its proof uses none of them, and no integrality of capacities is assumed outside Theorem 7. The estimator is (18) applied to $\Phi_\tau$ and its expectation is taken under the separate laws of control and treatment counts; it is not defined as a derivative, and its expectation is not computed from the law of the total demand. At zero demand, the infeasible value of $\Phi_\tau(d-e_i,s)$ is multiplied by a vanishing count, so it never affects the estimator.

Useful infrastructure beyond this mission: derivatives of Poisson expectations in the mean, the binomial conditional law of a Poisson split, and value-function facts for capacitated network-flow LPs. Contributions to any milestone are welcome; Lemmas 3 and 5 and (32) are pure probability and independent of the LP layer.

Selected references

• I. Bright, A. Delarue, I. Lobel, Reducing Marketplace Interference Bias Via Shadow Prices, arXiv:2205.02274v4, 2024; Management Science, 2025. https://arxiv.org/abs/2205.02274v4
• T. Blake, D. Coey, Why Marketplace Experimentation Is Harder than it Seems: The Role of Test-Control Interference, ACM EC, 2014. https://doi.org/10.1145/2600057.2602837
• R. Johari, H. Li, I. Liskovich, G. Y. Weintraub, Experimental Design in Two-Sided Platforms: An Analysis of Bias, Management Science 68(10), 2022. https://doi.org/10.1287/mnsc.2021.4247

Motivation

Global sensitivity analysis asks how much of the uncertainty in the output $Y$ of a model, a simulator or a learned predictor is attributable to an input $X$. A standard way to answer is to compare the law of $Y$ with its law after $X$ is revealed, and to average that discrepancy over $X$. Variance-based indices (Sobol' 1993; Wagner 1995) compare conditional and unconditional means. Density-based and distribution-based indices compare whole distributions. Rényi's postulates for measures of dependence ask, among other things, that such an index vanish exactly under independence (zero-independence) and reach its maximum exactly when $Y$ is a function of $X$ (max-functionality, Postulate E). Variance-based indices fail the first postulate, because the conditional mean can be constant while the conditional law moves.

Borgonovo, Figalli, Plischke and Savaré (Management Science, 2025) propose indices in which the discrepancy is an optimal transport cost. The squared 2-Wasserstein case is the numerator of the Wasserstein correlation coefficient of Wiesel (2022), whose Theorem 2.2 gives max-functionality for that coefficient. The paper extends max-functionality to general continuous costs, through a strict-convexity property of the transport cost on Dirac masses (Lemma 4). This mission formalizes that result, Theorem 5, together with the zero-independence property, Proposition 3.

Setting

Let $(\Omega,\mathcal B,P)$ be a probability space and $\mathsf X$, $\mathsf Y$ Polish spaces with their Borel $\sigma$-algebras. The input $X:\Omega\to\mathsf X$ and the output $Y:\Omega\to\mathsf Y$ are measurable, with laws $\mu$ and $\nu$.

A cost is a continuous function $k:\mathsf Y\times\mathsf Y\to[0,+\infty]$ with $k(y,y')=0$ if and only if $y=y'$. It need not be symmetric, a metric, or finite. For probability measures $\nu,\nu'$ on $\mathsf Y$, a coupling is a probability measure $\pi$ on $\mathsf Y\times\mathsf Y$ with marginals $\nu$ and $\nu'$, and the optimal transport cost is

$$K(\nu,\nu')=\inf_{\pi\in\Pi(\nu,\nu')}\iint k(y,y')\,d\pi(y,y').$$

For a sub-$\sigma$-algebra $\mathcal F$ of the Borel sets of $\mathsf X$, a version of the conditional distribution of $Y$ given $(X,\mathcal F)$ is a Markov kernel $x\mapsto\nu^{\mathcal F}_x$ that is $\mathcal F$-measurable in $x$ and satisfies $P(X\in A,\,Y\in B)=\int_A\nu^{\mathcal F}_x(B)\,d\mu(x)$ for $A\in\mathcal F$ and Borel $B$. The OT-based sensitivity measure of Definition 1 is

$$\xi^K(Y,X\mid\mathcal F)=\int_{\mathsf X}K(\nu,\nu^{\mathcal F}_x)\,d\mu(x),$$

written $\xi^K(Y,X)$ when $\mathcal F$ is the full Borel $\sigma$-algebra. The candidate maximum is

$$\mathbb M^K[Y]=\mathbb E[k(Y,Y')]=\iint k(y,y')\,d\nu(y)\,d\nu(y'),$$

with $Y'$ an independent copy of $Y$; for $k(y,y')=\|y-y'\|_2^2$ it equals twice the total variance of $Y$.

Formalization targets

Goal: Theorem 5 (max-functionality)

If $\mathbb M^K[Y]<+\infty$, then for every sub-$\sigma$-algebra $\mathcal F$ and every version of the conditional distribution,

$$\xi^K(Y,X\mid\mathcal F)\le\mathbb M^K[Y],$$

and

$$\xi^K(Y,X\mid\mathcal F)=\mathbb M^K[Y]\iff Y=f(X)\ P\text{-a.s. for some }\mathcal F\text{-measurable }f:\mathsf X\to\mathsf Y.$$

Milestones

The steps of the paper's proof, in order:

1. (57): $K(\nu,\nu')\le\iint k\,d\nu\,d\nu'$.
2. $K(\nu,\delta_{y'})=\int k(y,y')\,d\nu(y)$.
3. Lemma 4: for $y_1\ne y_2$ in $\operatorname{supp}\nu$ and $t\in(0,1)$,

$$K\big(\nu,(1-t)\delta_{y_1}+t\delta_{y_2}\big)<(1-t)K(\nu,\delta_{y_1})+tK(\nu,\delta_{y_2}).$$

4. (62): the disintegration $\int K(\nu,\delta_y)\,d\nu(y)=\int_{\mathsf X}\int K(\nu,\delta_y)\,d\nu^{\mathcal F}_x(y)\,d\mu(x)$.
5. The bound $K(\nu,\nu')\le\int K(\nu,\delta_y)\,d\nu'(y)$.
6. (63): at the maximum, that bound is an equality for $\mu$-a.e. $x$.
7. (65): Jensen's inequality for $K(\nu,\cdot)$ over the representation (64) of a mixture.

Companion: Proposition 3 (zero-independence)

$$\xi^K(Y,X)=0\iff X\text{ and }Y\text{ are independent}.$$

Significance

The result. Together, Proposition 3 and Theorem 5 place $\xi^K$ on a scale from $0$ (no information about $Y$ in $X$) to $\mathbb M^K[Y]$ (complete information), so the ratio $\xi^K(Y,X\mid\mathcal F)/\mathbb M^K[Y]$ is a normalized measure of association. This normalization is what lets practitioners rank inputs of a simulator or features of a model on a common scale. The result covers all continuous costs vanishing exactly on the diagonal, including the powers of a metric that give the Wasserstein indices, and arbitrary sub-$\sigma$-algebras $\mathcal F$, which model partial information about $X$ (for example the information carried by a function $g(X)$).

Formalizing it. The theorem is proved in the paper; the work here is to formalize the known proof. As far as is known, no machine-checked version of this result or of Wiesel's Wasserstein-correlation theorem exists. Along the way the development needs facts about optimal transport with extended-real costs that are not in Mathlib: the product-coupling bound, the transport cost to a Dirac mass, convexity and lower semicontinuity of $K(\nu,\cdot)$, and cyclical monotonicity of optimal plans.

Difficulty

The inequality and the "functional dependence ⇒ equality" direction are direct computations with the product coupling and with Dirac conditional laws. The converse is the hard direction. Equality of the integrals gives only the pointwise equality (63) almost everywhere, and the step from there to "$\nu^{\mathcal F}_x$ is a Dirac mass" needs strict convexity of $K(\nu,\cdot)$. Strict convexity fails for general measures: $K(\nu,\cdot)$ is affine along many segments. It holds only between Dirac masses at distinct points of $\operatorname{supp}\nu$ (Lemma 4), and even there it fails when the costs involved are infinite. A non-Dirac conditional law is not a two-point mixture, so the strict inequality must be carried over to general measures with an integrand that takes values in $[0,+\infty]$. The last step, building an $\mathcal F$-measurable $f$ from the conditional laws, is measure-theoretic bookkeeping that is easy to get wrong.

Formalization scope

• Spaces and values. $\mathsf X$ and $\mathsf Y$ are Polish with their Borel $\sigma$-algebras; the paper's supports in $\mathbb R^{n_X}$, $\mathbb R^{n_Y}$ are such spaces. All of $k$, $K$, $\mathbb M^K$ and $\xi^K$ take values in $[0,+\infty]$ (ℝ≥0∞), so $+\infty$ is allowed as on the page, and integrals are lower Lebesgue integrals.
• Transport cost. $K$ is the published definition RWPI.SqrtLasso.transportCost. Its first argument is the marginal $\nu$, and the cost is evaluated as $k(y,y')$ with $y\sim\nu$.
• Conditional laws. The conditional distribution is not a chosen object. Any Markov kernel satisfying the defining property IsCondDistrib is admissible, and every theorem quantifies over all versions and over all sub-$\sigma$-algebras $\mathcal F$.
• Ruled-out encodings. The goal must not fix $\mathcal F$ to the Borel $\sigma$-algebra or fix a version of the kernel. Its conclusion must not be replaced by "$\nu^{\mathcal F}_x$ is a Dirac mass for $\mu$-a.e. $x$", which is an intermediate step of the proof, not the theorem.
• Disclosed correction. Lemma 4 carries the extra hypotheses $K(\nu,\delta_{y_1}),K(\nu,\delta_{y_2})<+\infty$. As printed, both sides of (19) can be $+\infty$ under the lemma's assumptions. Theorem 5 is stated as printed.
• Not posed. The cyclical monotonicity of optimal plans, cited from Villani (2008, Ch. 5), and the existence of optimal plans used in Proposition 3 are standard optimal-transport facts. They are not milestones but are welcome as supporting lemmas.

Selected references

• E. Borgonovo, A. Figalli, E. Plischke, G. Savaré, Global Sensitivity Analysis via Optimal Transport, Management Science, 2025 (authors' manuscript of 7 March 2024 used here). https://doi.org/10.1287/mnsc.2023.01796
• J. Wiesel, Measuring Association with Wasserstein Distances, Bernoulli 28(4):2816–2832, 2022. https://doi.org/10.3150/21-BEJ1438
• C. Villani, Optimal Transport: Old and New, Springer, 2008. https://doi.org/10.1007/978-3-540-71050-9
• A. Rényi, On Measures of Dependence, Acta Mathematica Academiae Scientiarum Hungaricae 10:441–451, 1959. https://doi.org/10.1007/BF02024507
• I. M. Sobol', Sensitivity Estimates for Nonlinear Mathematical Models, Mathematical Modelling and Computational Experiments 1:407–414, 1993.
• H. M. Wagner, Global Sensitivity Analysis, Operations Research 43(6):948–969, 1995. https://doi.org/10.1287/opre.43.6.948

Motivation

Thompson sampling (TS) is the standard randomized heuristic for the Bayesian multi-armed bandit: at each decision it samples a parameter vector from the current posterior and pulls the arm that would be best if the sample were true. It ignores the remaining horizon. Min, Maglaras and Moallemi (arXiv:1902.04251, Management Science, 2025) obtain horizon-aware generalizations of TS from the information relaxation duality of Brown, Smith and Sun (Oper. Res. 2010). Each penalty function yields an upper bound on the Bayes-optimal value and an IRS policy. Such a policy samples a whole future outcome and plays the first action of the penalized clairvoyant optimum. With the zero-information penalty it is exactly TS.

Two of these policies, IRS.FH and IRS.V-Zero, are designed to interpolate between TS and the myopic rule. When one period remains they pull the arm with the highest predictive mean (Remark 5 of the paper). This mission formalizes the other end, Proposition 1: when many periods remain, they randomize exactly as Thompson sampling does. The paper presents this as the sense in which IRS policies "behave like TS during the initial decision epochs" and shift smoothly from exploration to exploitation without a tuning parameter.

Setting

There are $K \ge 1$ arms $\mathcal A = \{1,\dots,K\}$. Arm $a$ has an unknown parameter $\theta_a$. Given $\theta_a$, its rewards $R_{a,1}, R_{a,2}, \dots$ are i.i.d. with law $\mathcal R_a(\theta_a)$. The prior of $\theta_a$ is $\mathcal P_a(y_a)$, a member of a conjugate family indexed by a belief $y_a$. A Bayesian update $\mathcal U_a$ maps $(y_a, r)$ to the posterior belief after a reward $r$. The arms are independent. Throughout, rewards are integrable: $\mathbb E_{y_a}|R_{a,1}| < \infty$ for every belief (display (3)).

• The conditional mean reward is $\mu_a(\theta_a) = \mathbb E[R_{a,n} \mid \theta_a]$, and the predictive mean is $\bar\mu_a(y_a) = \mathbb E_{y_a}[\mu_a(\theta_a)]$.
• The outcome $\omega = (\theta, (R_{a,n})_{a,n})$ has law $\mathcal I(y)$.
• The posterior predictive mean after the first $n$ rewards of arm $a$ is $\hat\mu_{a,n}(\omega; y_a) = \mathbb E_{y_a}[\mu_a(\theta_a) \mid R_{a,1},\dots,R_{a,n}]$.

At remaining horizon $T$ and belief $y$, the three policies act as follows:

1. TS samples $\tilde\theta \sim \mathcal P(y)$ and plays $A^{TS}(y) = \operatorname{argmax}_a \mu_a(\tilde\theta_a)$.
2. IRS.FH samples $\tilde\omega \sim \mathcal I(y)$ and plays $A^{IRS.FH}(T,y) = \operatorname{argmax}_a \hat\mu_{a,T-1}(\tilde\omega)$, the arm with the best posterior mean after $T-1$ sampled rewards of every arm.
3. IRS.V-Zero samples $\tilde\omega \sim \mathcal I(y)$ and solves the allocation problem

$$\max_{n \in \mathcal N_T} \sum_{a=1}^K \sum_{i=1}^{n_a} \hat\mu_{a,i-1}(\tilde\omega), \qquad \mathcal N_T = \Big\{n \in \mathbb N_0^K : \sum_a n_a = T\Big\}.$$

It then plays the arm $A^{IRS.V\text{-}Zero}(T,y) = \operatorname{argmax}_a \tilde n^*_a$ to which the optimal allocation $\tilde n^*$ assigns the most pulls.

Each action is a random variable driven by the policy's own sample.

Formalization targets

Goal: Proposition 1 (p. 25)

Assume $\mu_i(\theta_i) \ne \mu_j(\theta_j)$ almost surely under $\mathcal P(y)$, for all $i \ne j$. Then for every arm $a$,

$$\lim_{T\to\infty} \mathbb P[A^{IRS.FH}(T,y) = a] = \mathbb P[A^{TS}(y) = a], \qquad \lim_{T\to\infty} \mathbb P[A^{IRS.V\text{-}Zero}(T,y) = a] = \mathbb P[A^{TS}(y) = a].$$

This holds for every choice of the tie-breaking rules in the argmaxes and in the allocation problem.

Milestones

1. Proposition 4 (p. 53): $\mu_a(\theta_a)$ and $\max_a \mu_a(\theta_a)$ are integrable under the prior.
2. Proposition 5 (p. 54): $\hat\mu_{a,n}$ and the sample mean $\frac1n\sum_{i\le n} R_{a,i}$ converge almost surely to $\mu_a(\theta_a)$.
3. Display (109) (p. 54): if a sequence of vectors converges to a vector with distinct entries, every argmax rule eventually selects the argmax of the limit.
4. The allocation argument (113)–(123) (pp. 54–56): if the payoff rows converge to distinct limits, then for large $T$ every optimal allocation gives its largest share only to the arm with the largest limit.
5. Display (55) alone: the IRS.FH half of the goal.

Significance

Proposition 1 identifies the long-horizon behaviour of the two IRS policies with that of Thompson sampling. Together with Remark 5 it pins down both ends of the horizon. It explains why their simulated regret curves track TS early and the myopic policy late (§5 of the paper). It also shows that the design choice "play the arm with the largest allocation" in IRS.V-Zero is the one that recovers TS. Other selection rules, such as any arm with a positive allocation, need not.

The paper gives a complete proof in Appendix D.1–D.2. A machine-checked version adds three things. It fixes the probabilistic model of a conjugate Bayesian bandit with infinite reward sequences in Lean, which the companion missions on the same paper also need. It makes the role of tie-breaking explicit. And it repairs a step of the printed proof: the bound $n^\circ(A^\circ_T) \ge \lfloor T/2 \rfloor$ in §D.2 holds only for two arms, and the general case needs $\lceil T/K \rceil$ and a threshold growing with $K$. No formalization of this result is known on Prove2Me or in Mathlib.

Difficulty

The IRS.FH half reduces to almost-sure convergence of posterior means, which is a martingale argument (Lévy's upward theorem). That argument needs $\mu_a(\theta_a)$ to be measurable with respect to the limit $\sigma$-algebra of the reward sequence, a fact supplied by the strong law of large numbers. Building the outcome law, a mixture over $\theta$ of infinite product measures, and identifying the conjugate update with conditional expectation are where the measure theory lies.

The IRS.V-Zero half does not follow from convergence of the posterior means alone. The selected arm is a function of an optimal allocation of a combinatorial problem whose size grows with $T$. The naive expectation that the arm with the best limit receives "most" pulls has to be proved by an exchange argument that handles the finitely many early terms, where the posterior means can still be badly ordered. The printed version of this argument is correct only for $K = 2$.

Formalization scope

• Arms are Fin K with NeZero K; the reward sequence of an arm is ℕ → ℝ, 0-based.
• One parameter type and one belief type serve all arms; reward laws and priors are Markov kernels.
• Conjugacy is stated as Bayes' rule on rectangles for every belief. The update is assumed jointly measurable, and the standing integrability (3) is assumed for every belief.
• The outcome law $\mathcal I(y)$ is a product over arms of mixtures $\int \delta_\theta \otimes \mathcal R_a(\theta)^{\otimes \mathbb N}\, \mathcal P_a(y_a)(d\theta)$.
• $\hat\mu_{a,n}$ is the pathwise conjugate version $\bar\mu_a(y_{a,n})$ of the conditional expectation (10), defined at every outcome so that it can sit inside an argmax.
• $\mathbb P[A = a]$ is the mass of $\{a\}$ under the pushforward of the policy's sampling law. All tie-breaking rules are required to be measurable; otherwise the pushforward would be the zero measure.
• The assumption of the proposition is required almost surely under the prior, not as injectivity of $\mu$.
• A formalization in which the selectors were non-measurable, the outcome law degenerate, or the distinctness hypothesis unsatisfiable would make the goal vacuous. The definitions rule out the first two, and a deterministic two-arm instance shows the hypotheses are satisfiable.

The development needs Lévy's upward theorem (MeasureTheory.tendsto_ae_condExp in Mathlib) and the strong law of large numbers (ProbabilityTheory.strong_law_ae). It also needs a lemma identifying iterated conjugate updates with the posterior given finitely many rewards, and the measurability of $\theta \mapsto \mathcal R_a(\theta)^{\otimes\mathbb N}$. These last two are reusable for any Bayesian bandit or sequential-estimation development. Contributions of the two deterministic milestones are self-contained and welcome first.

Selected references

• S. Min, C. Maglaras, C. C. Moallemi, Thompson Sampling with Information Relaxation Penalties, Management Science, 2025; preprint arXiv:1902.04251v2, 2021. https://arxiv.org/abs/1902.04251
• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research 58(4), 2010. https://doi.org/10.1287/opre.1090.0796
• W. R. Thompson, On the Likelihood that One Unknown Probability Exceeds Another in View of the Evidence of Two Samples, Biometrika 25(3/4), 1933. https://doi.org/10.2307/2332286
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4), 2014. https://doi.org/10.1287/moor.2014.0650

Motivation

Multi-server queues model call centres, hospital wards, cloud server pools and any system in which $n$ identical servers work through one first-come-first-served (FCFS) line. Capacity planning for such systems needs bounds on the steady-state queue length and on the probability of delay (the chance that an arriving job finds every server busy) that are explicit, hold for every $n$, and stay informative as the load approaches capacity.

For a single server, Kingman's bound (Kingman 1962, ref. [89] of the paper) gives exactly this: the mean wait is at most a multiple of $1/(1-\rho)$ that depends only on the first two moments of the inter-arrival and service times. For $n$ servers with general distributions (the GI/GI/n queue), no comparable explicit bound was known.

Timeline.

• 1962: Kingman's single-server bound.
• 1981: Halfin and Whitt identify the heavy-traffic regime $\sqrt n(1-\rho)\to\beta$ in which the probability of delay is nondegenerate (Halfin and Whitt 1981).
• 2013: Gamarnik and Goldberg prove (for the GI/G/n queue) that the steady-state number waiting is stochastically dominated by the supremum of a process built from independent renewal processes (Gamarnik and Goldberg 2013). Their bound is not explicit and needs more than two service moments.
• 2017–2025: Li and Goldberg derive explicit bounds with $1/(1-\rho)$ scaling under $\mathbb E[A^2]<\infty$ and $\mathbb E[S^{2+\epsilon}]<\infty$ (arXiv:1706.04628, Mathematics of Operations Research 2025).

Setting

A GI/GI/n queue has $n\ge1$ identical servers and one FCFS line. Jobs arrive with i.i.d. inter-arrival times distributed as a nonnegative random variable $A$. Each job needs an i.i.d. service time distributed as a nonnegative random variable $S$, independent of the arrivals. An arriving job starts service at the first server to become free, in order of arrival.

Write $\mu_A=1/\mathbb E[A]$ and $\mu_S=1/\mathbb E[S]$ for the arrival and service rates, and $\rho=\mu_A/(n\mu_S)$ for the traffic intensity. The moment index is

$$r^*=\sup\{r:\mathbb E[S^r]<\infty\},$$

which may be $+\infty$. Normalised moments are $\mathbb E[(A\mu_A)^2]$ and $\mathbb E[(S\mu_S)^r]$.

$Q(t)$ is the number of jobs in the system (in service and waiting) at time $t$. "$Q(\infty)$ exists" means that, whatever the initial condition, $Q(t)$ converges in distribution as $t\to\infty$ to a random variable $Q(\infty)$. The steady-state number waiting is $L(\infty)=\max(0,Q(\infty)-n)$, and the steady-state probability of delay is $\mathbb P(Q(\infty)\ge n)$.

The milestones also use equilibrium renewal processes. For a nonnegative $X$ with finite mean, its equilibrium law $R(X)$ satisfies $\mathbb P(R>y)=\frac1{\mathbb E[X]}\int_y^\infty\mathbb P(X>z)\,dz$. An equilibrium renewal process with renewals distributed as $X$ has its first renewal interval distributed as $R(X)$ and the later ones distributed as $X$.

$A_e(t)$ counts the renewals in $[0,t]$ of such a process for $A$. $N_{e,1}(t),\dots,N_{e,n}(t)$ count those of $n$ independent such processes for $S$, also independent of $A_e$.

Formalization targets

Goal: Theorem 2 (pp. 9–10)

Assume

• $\mathbb E[A^2]<\infty$;
• $r^*>2.5$;
• $\mu_A<n\mu_S$;
• $Q(\infty)$ exists.

Then for all $x>0$ and all $r\in[2.5,r^*)$,

$$\mathbb P\Big(L(\infty)\ge\frac x{1-\rho}\Big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^6)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)x^{-\frac r2}+1.1\,e^{-.0225\,\mathbb E[(A\mu_A)^2]^{-1}x},$$ $$\mathbb P\big(Q(\infty)\ge n\big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^7)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)\big(n(1-\rho)^2\big)^{-\frac r2}+1.1\,e^{-.0028\,\mathbb E[(A\mu_A)^2]^{-1}n(1-\rho)^2}.$$

The paper states the infimum over $r$. With $r$ universally quantified the statement is equivalent, because the exponential term does not depend on $r$.

Milestones

They follow the paper's proof, in attack order:

• Lemma 1, the Gamarnik–Goldberg comparison $\mathbb P(L(\infty)\ge x)\le\mathbb P(\sup_{t\ge0}(A_e(t)-\sum_{i=1}^nN_{e,i}(t))\ge x)$;
• Lemma 2, which splits that supremum into an arrival part and a service part;
• Lemmas 8, 9 and 10, which reduce the arrival part to Kingman's bound with an explicit exponent;
• Lemma 3, the exponential bound for the arrival part;
• Lemma 4 and Theorem 10, conditional bounds from central moments of the pooled process $\sum_iN_{e,i}(t)$;
• Lemmas 5 and 6, those central-moment bounds;
• the explicit bound for $r\in(2.5,r^*)$ displayed on p. 28;
• Lemma 14, a transient comparison for a queue started with all servers busy;
• Lemma 7 and Corollary 5, comparisons with fewer servers that make the bound informative at the level $Q(\infty)\ge n$.

Significance

The result. The bounds hold for every $n$ and every load with $\rho<1$, and they depend on the distributions only through a few normalised moments. In the Halfin–Whitt regime, $n(1-\rho)^2$ stays bounded away from zero, so the delay bound stays informative. As $\rho\to1$ with $n$ fixed, the queue tail decays at the Kingman scale $1/(1-\rho)$. These are the first such bounds for general GI/GI/n queues; earlier explicit results needed Poisson arrivals or exponential service. The paper derives from Theorem 2 bounds at a fixed $r$ (Corollaries 1–2), a refinement beyond $1/(1-\rho)$ scaling when $n(1-\rho)^2$ is large (Corollary 3), and optimised bounds under growth conditions on $\mathbb E[(S\mu_S)^r]$ (Theorem 3).

Formalization. The theorem is proved in the paper, partly in a supplemental appendix, and none of it is formalized; there are no machine-checked results for multi-server queues with general distributions anywhere. A complete development would add to the platform the first FCFS multi-server queue with general distributions, its steady state, equilibrium renewal processes, and the Gamarnik–Goldberg comparison chain. Each is reusable for later work on many-server queues.

Difficulty

The obvious route is to compare the $n$-server queue with a single-server one, or to apply a heavy-traffic limit. The first loses a factor of $n$; the second gives limits but no bounds at a fixed $n$.

The paper's route needs two hard ingredients:

• Comparison with renewal processes. The stochastic comparison of Lemmas 1 and 14 is a theorem about the sample-path dynamics of FCFS service, not a calculation.
• Uniform moment bounds. Explicit control of $\mathbb E|\sum_{i=1}^nN_{e,i}(t)-nt|^r$ at the scale $(nt)^{r/2}$, uniformly in $n$ and $t$, is required. Classical renewal moment bounds are either asymptotic in $t$ or lose the dependence on $n$.

For the probability of delay, Lemma 1 at level $0$ gives only the trivial bound $1$. A second comparison across server counts (Lemma 7) is needed.

Formalization scope

Laws. $A$ and $S$ are represented by their laws $\mu_A,\mu_S$: probability measures on $\mathbb R$ carried by $[0,\infty)$, integrable, with positive mean. Positivity of the means is implicit in the paper, which needs $\mu_X=1/\mathbb E[X]$ finite; it is stated explicitly. $\mathbb E[(X\mu_X)^r]$ is a real integral and is used only where it is finite: $r<r^*$ for $S$, and $r=2$ with $\mathbb E[A^2]<\infty$ for $A$. $r^*$ is an extended real.

The queue.

• The queue is the Kiefer–Wolfowitz workload recursion, driven by an initial condition and i.i.d. pairs of inter-arrival and service times.
• An initial condition gives the first-arrival time and the residual service time at each server. No job waits at time $0$.
• "$Q(\infty)$ exists with law $\pi$" quantifies over every initial law of that kind, independent of the inputs. This class is narrower than the paper's, so the hypothesis is weaker and the stated theorem is stronger. The paper's proof uses only such initial conditions (Lemma 7 through Lemma 14).
• $L(\infty)$ is the truncated difference $\max(0,Q(\infty)-n)$.

Renewal processes.

• Counts are natural numbers, computed pathwise from the renewal intervals.
• Bounding families are arbitrary probability spaces carrying mutually independent intervals with the prescribed laws.
• Suprema of processes are taken in the extended reals.

Ruled out. None of the following trivializing formalizations is used:

• a steady-state hypothesis that no queue satisfies, or one restricted to an initial-condition class that drops what Lemma 7 needs;
• a real-valued supremum or infimum, which collapses to $0$ on unbounded families;
• a Bochner moment of a non-integrable function, which is $0$ in Lean.

The infimum over $r$ is stated as a universal quantifier.

Needed infrastructure. Equilibrium distributions and renewal counting processes, moment and maximal inequalities for sums of independent renewal processes, Kingman's exponential martingale bound, and the sample-path comparison of FCFS multi-server queues. Contributions on any of these are welcome: the renewal and random-walk results (Lemmas 5, 6, 8–10) are independent of queueing.

Selected references

• Y. Li and D. A. Goldberg, Simple and explicit bounds for multi-server queues with 1/(1−ρ) scaling, Mathematics of Operations Research, 2025; arXiv:1706.04628v3. https://arxiv.org/abs/1706.04628
• D. Gamarnik and D. A. Goldberg, Steady-state GI/G/n queue in the Halfin–Whitt regime, Annals of Applied Probability 23(6), 2382–2419, 2013. https://doi.org/10.1214/12-AAP905
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24, 383–392, 1962 (ref. [89] of Li–Goldberg).
• J. F. C. Kingman, A martingale inequality in the theory of queues, Mathematical Proceedings of the Cambridge Philosophical Society 60(2), 359–361, 1964 (ref. [90] of Li–Goldberg; the source of Lemma 9).