All missions

Motivation

In a many-server queue with $n$ servers, the Halfin–Whitt (quality-and-efficiency-driven) regime lets $n\to\infty$ while the arrival rate approaches capacity at rate $\sqrt n$. In this regime the centred and scaled number of customers in each service phase of a $G/Ph/n+GI$ queue (general arrivals, phase-type service, general patience) converges to a $d$-dimensional diffusion with a piecewise-linear drift (Dai, He and Tezcan, Ann. Appl. Probab. 2010). This diffusion is exponentially ergodic with a unique invariant measure $\mu$ (Dieker and Gao, Ann. Appl. Probab. 2013), but for $d\ge2$ no explicit formula for $\mu$ is known.

Since $\mu$ is not explicit, its averages $\mu(h)$ are estimated by simulation, for example by the time average of $h$ along one long trajectory. The second main result of Jin, Pang, Xu and Xu (arXiv:2209.07361) is a central limit theorem for these time averages. It gives the $\sqrt t$ rate of convergence, for every starting point, and identifies the limiting variance through the solution of a Stein (Poisson) equation.

Setting

A model consists of $d\ge1$, a patience rate $\alpha>0$, $\beta\in\mathbb R$, a probability vector $p\in\mathbb R^d$, service rates $v_k>0$, a sub-stochastic matrix $P$ with $P_{ii}=0$ and $I-P$ invertible, and a $d\times d$ matrix $\sigma$. Put $R=(I-P')\mathrm{diag}(v)$ and $e=(1,\dots,1)'$. The phase distribution has mean one, $e'R^{-1}p=1$, and $\sigma\sigma'$ is uniformly elliptic: $\xi'\sigma\sigma'\xi\ge c|\xi|^2$ for some $c>0$. The drift is

$$g(x)=-\beta p-Rx+(R-\alpha I)p\,(e'x)^+ ,$$

and the limiting diffusion solves, for a standard Brownian motion $B$,

$$X^x_t=x+\int_0^tg(X^x_s)\,ds+\sigma B_t .$$

Its semigroup is $P_th(x)=\mathbb Eh(X^x_t)$ and $\mu$ is its invariant probability measure. For bounded measurable $h$, the empirical average is $\mathcal E^x_t(h)=\frac1t\int_0^th(X^x_s)\,ds$. The Stein solution is

$$f(x)=-\int_0^\infty\big(P_th(x)-\mu(h)\big)\,dt ,$$

which solves $\mathcal Af=h-\mu(h)$ for the generator $\mathcal Af=\langle\nabla f,g\rangle+\frac12\langle\sigma\sigma',\nabla^2f\rangle_{HS}$. Here $\|h\|_\infty$ is the essential supremum of $|h|$.

Formalization targets

Goal: Theorem 1.3

There is $C>0$ such that for every bounded measurable $h$, $f$ is differentiable, $\mu(|\sigma'\nabla f|^2)\le C\|h\|_\infty^2$, and for every $x$

$$\sqrt t\,\big[\mathcal E^x_t(h)-\mu(h)\big]\Rightarrow\mathcal N\big(0,\mu(|\sigma'\nabla f|^2)\big)\qquad(t\to\infty).$$

Milestones (§3 of the paper)

• Lemma 3.2: the integral defining $f$ converges, $f$ solves (3.1) in integrated form, and $f(x)=\int_0^\infty e^{-\lambda t}P_t[\lambda f-h+\mu(h)](x)\,dt$ for every $\lambda>0$.
• Lemma 3.4: moment bounds $\mathbb E|X^x_t|^m\le e^{Ct}(|x|^m+1)$, uniform over a family of mollified diffusions $X^{\varepsilon}$, and $\mathbb E|X^{\varepsilon,x}_t-X^x_t|^m\to0$.
• Proposition 3.7: the weighted occupation time of $e'X^x$ in $[-\epsilon,\epsilon]$ has mean at most $C\epsilon e^{ct}(1+|x|)(1+t)$.
• Lemma 3.5: the Jacobians of the mollified diffusions converge almost surely, simultaneously for all $0\le s\le t$, to the Jacobian $J^x$ of $X^x$.
• Lemma 3.6: $L^m$ bounds $C|u|^mt^{-m/2}e^{mC_{op}t}$ on the weights $\mathcal I^x_u(t)=\frac1t\int_0^t\langle\sigma^{-1}J^x_ru,dB_r\rangle$, and their convergence as $\varepsilon\to0$.
• Lemma 3.3: $\nabla_u\mathbb E\psi(X^x_t)=\mathbb E[\psi(X^x_t)\mathcal I^x_u(t)]$ for $C^1$ functions $\psi$ with bounded gradient.
• Proposition 3.1: $|f(x)|,|\nabla f(x)|\le C\|h\|_\infty(1+|x|^2)$.

Significance

The theorem gives the rate $\sqrt t$ and the asymptotic variance of the standard ergodic-average estimator of $\mu(h)$, which yields asymptotic confidence intervals for steady-state performance measures of the queue approximated by the diffusion. The function $h$ need only be bounded and measurable, so indicator functions are included, for example the probability that the total queue $e'X$ exceeds a level. The same variance governs the moderate deviation principle (Theorem 1.4 of the paper), which is a planned follow-up.

The result is proved in the source paper. None of it is formalized. Formalizing it requires Lean infrastructure that does not exist yet and is reusable beyond queueing: Stein/Poisson equations for non-smooth drifts, a Bismut–Elworthy–Li formula, derivative flows of diffusions, and a continuous-time martingale CLT.

Difficulty

The obvious argument applies Itô's formula to the Stein solution $f(X_t)$: the time average becomes a martingale plus a boundary term, and a martingale CLT finishes the proof. That argument needs $f\in C^1$ with polynomial growth of $\nabla f$. For bounded measurable $h$, classical regularity results for Stein equations do not apply, and the drift $g$ is not differentiable on the hyperplane $e'x=0$, so the diffusion cannot be differentiated in its starting point directly. The central difficulty is Proposition 3.1, a gradient bound for $f$ when neither $h$ nor $g$ is differentiable.

Formalization scope

• The state space is EuclideanSpace ℝ (Fin d) with the Euclidean norm. Matrices act through Matrix.toEuclideanCLM, whose norm is the operator norm.
• Time is ℝ≥0. Brownian motion is the published predicate EthierKurtz.IsStandardBrownian. The diffusion is the pathwise solution of the integral equation above, for every $\omega$.
• Statements take $(\Omega,\mathbb P,B,X)$ and an invariant probability measure $\mu$ as hypotheses. Both exist, and the conclusions depend only on the law.
• $\sigma$ is a general uniformly elliptic matrix. The paper's explicit formula for $\sigma\sigma'$ (p. 3) is one instance, and Remark 1.1 says the results use only ellipticity.
• "$f$ is the solution to (3.1)" means the function (3.2). Its differentiability is part of the conclusions, because in Lean the gradient of a non-differentiable function is $0$ and the variance could otherwise vanish silently.
• Weak convergence is convergence of $\mathbb E\varphi(Y_t)$ for every bounded continuous $\varphi$ (§1.4), along real $t\to\infty$. Expectations of powers are lower Lebesgue integrals.
• The constant $C$ in the goal and in Proposition 3.1 is uniform in $h$.
• The Jacobians $J_{s,t}$ are propagators of the linearized equation, not the paper's $\exp\int_s^t\nabla g\,dr$, which fails to solve the equation when the matrices do not commute ($d\ge2$).
• Itô integrals are characterized as $L^2$ limits of dyadic left-point Riemann sums.
• Lemma 3.4 states a model-dependent rate $C$ in place of $C_m=2m^2\tilde C_{op}$, because the explicit rate fails in large dimension.

Restricting $h$ to smooth or Lipschitz functions, starting $X$ in $\mu$, taking $d=1$ or a diagonal $\sigma$, or dropping the differentiability of $f$ each makes the statement weaker or trivial, and none of them is the theorem.

Welcome contributions include a general Itô integral and Itô formula for additive-noise diffusions, a martingale CLT in continuous time, exponential ergodicity of this diffusion (Lemma A.1 of the paper, posed in the companion mission on the Euler–Maruyama scheme), and any of the milestones.

Selected references

• X. Jin, G. Pang, L. Xu, X. Xu, An Approximation to the Invariant Measure of the Limiting Diffusion of G/Ph/n+GI Queues in the Halfin–Whitt Regime and Related Asymptotics, arXiv:2209.07361v1, 2022. https://arxiv.org/abs/2209.07361
• J. G. Dai, S. He, T. Tezcan, Many-server diffusion limits for G/Ph/n+GI queues, Ann. Appl. Probab. 20(5), 2010. https://doi.org/10.1214/09-AAP674
• A. B. Dieker, X. Gao, Positive recurrence of piecewise Ornstein–Uhlenbeck processes and common quadratic Lyapunov functions, Ann. Appl. Probab. 23(4), 2013. https://doi.org/10.1214/12-AAP870
• X. Fang, Q.-M. Shao, L. Xu, Multivariate approximations in Wasserstein distance by Stein's method and Bismut's formula, Probab. Theory Relat. Fields 174, 2019. https://doi.org/10.1007/s00440-018-0874-5

Motivation

A retailer often knows more about her own demand than the supplier who produces for her. When the supplier must commit to a production quantity before demand is realized, what the retailer tells him shapes how much he produces, and therefore how much demand she can serve. Information design (Bayesian persuasion, Kamenica and Gentzkow, 2011) asks how a sender should commit in advance to a randomized disclosure rule to steer a receiver's action.

O. Candogan and H. Gurkan, The Value of Information Design in Supply Chain Management (SSRN 4378997; Management Science, 2024, DOI 10.1287/mnsc.2023.03004) solve this problem for a supplier facing a newsvendor problem with uniform demand. Their Theorem 1 identifies the retailer's optimal policy: full disclosure, no disclosure, or an explicit two-message partial disclosure, according to thresholds on the critical ratio. Their Theorem 2, the goal of this mission, quantifies how much the optimal policy is worth compared with the two naive policies a practitioner would use by default, and how this gain moves with the retailer's prior and the supplier's cost structure.

Setting

The state is $\omega\in\{0,1\}$ with prior $p_0=\mathbb P(\omega=0)$. Demand is $D_0\sim U[a_0,b_0]$ in state $0$ and $D_1\sim U[a_1,b_1]$ in state $1$, with nested supports $a_0\le a_1<b_1\le b_0$.

Supplier. At belief $p=\mathbb P(\omega=0)$ the supplier chooses $Q\ge0$ to minimize the expected newsvendor cost

$$S_\xi(p,Q)=p\,\mathbb E\big[\xi(D_0-Q)^++(1-\xi)(Q-D_0)^+\big]+(1-p)\,\mathbb E\big[\xi(D_1-Q)^++(1-\xi)(Q-D_1)^+\big],$$

where $\xi=C_s/(C_s+C_e)\in(0,1)$ is the critical ratio of the unit shortage cost $C_s$ to the total unit cost $C_s+C_e$.

Retailer. The retailer learns $\omega$ and sends a message $m$ from a finite set $\mathcal M$ according to a committed policy $\pi(m\mid\omega)$. Message $m$ has probability $\mathbb P(m)=p_0\pi(m\mid0)+(1-p_0)\pi(m\mid1)$ and induces the posterior $p_m=p_0\pi(m\mid0)/\mathbb P(m)$. The supplier best-responds with an optimal quantity $Q^*(p_m)$, and the retailer pays her expected shortage

$$R(p,Q)=p\,\mathbb E[(D_0-Q)^+]+(1-p)\,\mathbb E[(D_1-Q)^+].$$

Her optimal expected cost $V_\xi(p_0)$ is the infimum of $\sum_m\mathbb P(m)\,R(p_m,Q^*(p_m))$ over all finite message sets, all policies and all best responses of the supplier.

Naive policies. Under no disclosure the supplier keeps the prior, and the retailer pays $K(p_0)=R(p_0,Q^*_{p_0})$. Under full disclosure he learns $\omega$, and she pays $K_F(p_0)=(1-p_0)K(0)+p_0K(1)$. The values of information are

$$VI_{ND}(\xi,p_0)=K(p_0)-V_\xi(p_0),\qquad VI_{FD}(\xi,p_0)=K_F(p_0)-V_\xi(p_0).$$

Thresholds. $\underline\tau(p)=p(a_1-a_0)/(b_0-a_0)$, $\hat p=\xi(b_0-a_0)/(a_1-a_0)$, $p_0^*=\sqrt{\hat p}$ and $\xi^*=1-\tfrac12(a_1-a_0)/(b_0-b_1+a_1-a_0)$.

Formalization targets

Goal: Theorem 2 (p. 13)

In the partial-disclosure regime $\xi\in(0,\underline\tau(p_0)]$, with $a_0<a_1$:

$$VI_{ND}\ \text{is unimodal in } p_0 \text{ with peak } p_0^*=\sqrt{\xi(b_0-a_0)/(a_1-a_0)}\ \text{and decreasing in } \xi;$$ $$VI_{FD}\ \text{is decreasing in } p_0 \text{ and unimodal in } \xi \text{ with peak } \xi^*.$$

For fixed $\xi$ the regime is $p_0\in[\hat p,1]$; for fixed $p_0$ it is $\xi\in(0,\underline\tau(p_0)]$.

Milestones

1. Proposition 1 (p. 8): the supplier's optimal quantity is unique and given in closed form.
2. (B.2) (p. 25): $V_\xi(p_0)=\kappa(p_0)$, the lower convex envelope of $K$ on $[0,1]$.
3. (B.5) (p. 28): $K$ in closed form for $\xi\le(a_1-a_0)/(b_0-a_0)$.
4. Lemma 1 (p. 25): $\kappa$ in closed form in the three regimes of $\xi$.
5. The four derivative displays (p. 30): $\partial VI_{ND}/\partial\xi$, $\partial VI_{ND}/\partial p_0$, $\partial VI_{FD}/\partial\xi$, $\partial VI_{FD}/\partial p_0$ in the regime.

Significance

The result. Theorem 2 tells a retailer when designing information is worth the effort. Against no disclosure, the gain is largest at the intermediate prior $p_0^*$ and shrinks as shortages become relatively more expensive for the supplier. Against full disclosure, the gain shrinks as the prior probability of the wide-support state $\omega=0$ grows and peaks at the intermediate critical ratio $\xi^*$. These comparative statics are what the paper's managerial discussion (pp. 13–14, Figures 4–5) rests on.

Formalizing it. The result is proved in the paper (Online Appendix B, pp. 24–30), by citing Kamenica–Gentzkow for the reduction to the convex envelope and by explicit calculus. No part of it is machine-checked. A complete formalization would contain a self-contained proof of the concavification reduction for a two-state sender–receiver game with finite message sets, the newsvendor quantile of a uniform mixture, and an exact convex-envelope computation, each reusable beyond this paper.

Difficulty

The derivative formulas are routine once $K$ and $\kappa$ are known in closed form. The work lies upstream. The optimal cost is an infimum over all finite policies and all best responses, and turning it into $\kappa(p_0)$ requires the Kamenica–Gentzkow argument: Jensen's inequality over Bayes-plausible posterior distributions for the lower bound, and a two-point splitting for attainment. $\kappa$ itself is a supremum over all convex minorants, and identifying it requires showing that $K$ is convex below $\hat p$ and concave above, and that the chord from $(\hat p,K(\hat p))$ to $(1,K(1))$ is supporting. Finally, $K$ is defined through an argmin, so its closed form needs the uniqueness of the newsvendor quantile. A solver who differentiates the closed forms of p. 28 directly proves only the last step.

Formalization scope

All objects live in the namespace SCInfoDesign.ValueInfo. The supports are bundled in a structure Params. The critical ratio $\xi$ is an explicit argument of every object, because Theorem 2 varies it.

Conventions.

• Uniform expectations are interval integrals divided by the interval length.
• The supplier's cost is the paper's cost (2) divided by $C_s+C_e$, which has the same minimizers.
• Message sets are finite (Fin n).
• A zero-probability message gets the junk posterior $0$ and weight $0$.
• $K$ uses the largest optimal quantity, which is the unique one here.
• $\kappa$ is the published BiconvexProg.BranchBound.convexEnvelope on $[0,1]$.
• The value of information is the difference, not its absolute value; the difference is nonnegative.
• "Unimodal with peak $x^*$" means strictly increasing up to $x^*$ and strictly decreasing from $x^*$, on the regime.
• The $\xi$-claims are stated for $p_0<1$: at $p_0=1$ both values are identically $0$.

Added hypotheses. These are the paper's implicit standing assumptions: $a_0<b_0$ and $a_1<b_1$, nonnegative demand ($0\le a_0$, $0\le a_1$), and $0<\xi<1$. The goal and the derivative displays also assume $a_0<a_1$: otherwise the regime is empty and $\hat p$ is $0/0$.

Ruled out. The optimal cost is not the cost of the paper's policy $\Gamma^*$, and the supplier's response is an argmin of (2), not the closed form of Proposition 1. Theorem 2 is therefore a statement about the game, not about a formula.

Infrastructure. A complete development needs the concavification theorem for finite policies (milestone 2, reusable for every two-state persuasion model), the uniform-mixture newsvendor quantile (milestone 1), the exact computation of a convex envelope (milestone 4) and one-variable calculus. Contributions of any milestone, of general lemmas on convex envelopes on an interval, or of the Kamenica–Gentzkow reduction in general form are welcome. The proofs of the paper are in its Online Appendix.

Selected references

• O. Candogan, H. Gurkan, The Value of Information Design in Supply Chain Management, Management Science, 2024 (read as SSRN 4378997). https://ssrn.com/abstract=4378997 , https://doi.org/10.1287/mnsc.2023.03004
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6), 2015. https://doi.org/10.1287/opre.2015.1422

Motivation

A retailer who sees her own demand before her supplier does can decide how much of that knowledge to pass upstream. Sharing everything is not obviously best: the supplier uses the information to set his production quantity for his own benefit, and the retailer bears a cost when he under-produces. Candogan and Gurkan (SSRN 4378997; published in Management Science, 2024, doi:10.1287/mnsc.2023.03004) treat this as a Bayesian persuasion (information design) problem in the sense of Kamenica and Gentzkow (AER 2011): the retailer commits in advance to a signalling policy, and the supplier best-responds to the posterior belief that each signal induces. The paper characterizes the retailer's optimal policy in closed form for uniform demand. This mission covers its first main result, the case where one demand support is nested inside the other.

The question links the supply-chain literature on information sharing between firms, where sharing is usually all-or-nothing, with the persuasion literature, where optimal signals are typically partial.

Setting

The state is $\omega\in\{0,1\}$, with prior $p_0=\mathbb P(\omega=0)\in[0,1]$. Demand is $D_\omega$, where $D_0$ is uniform on $[a_0,b_0]$ and $D_1$ is uniform on $[a_1,b_1]$. The supports are nested: $0\le a_0\le a_1<b_1\le b_0$ and $a_0<b_0$.

A disclosure policy $\Gamma=(\pi,\mathcal M)$ is a finite message space $\mathcal M$ and conditional probabilities $\pi(m\mid\omega)$. After message $m$ the supplier holds the posterior

$$p=\frac{\pi(m\mid\omega=0)\,p_0}{\pi(m\mid\omega=0)\,p_0+\pi(m\mid\omega=1)(1-p_0)}.$$

Full disclosure sends message $m_i$ exactly in state $i$; no disclosure sends the same message in both states.

At belief $p$ the supplier solves the newsvendor problem

$$\min_{Q\ge 0}\; p\,\mathbb E\big[\xi(D_0-Q)^+ + (1-\xi)(Q-D_0)^+\big] + (1-p)\,\mathbb E\big[\xi(D_1-Q)^+ + (1-\xi)(Q-D_1)^+\big],$$

where $\xi=C_s/(C_s+C_e)\in(0,1)$ is his critical ratio (shortage cost $C_s$, excess cost $C_e$). A best-response profile $Q^*$ picks an optimal quantity $Q^*_p$ for every belief $p\in[0,1]$. The retailer pays the expected shortage $p\,\mathbb E(D_0-Q^*_p)^+ + (1-p)\,\mathbb E(D_1-Q^*_p)^+$ at the induced posterior. Her design problem (3) minimizes the expectation of this cost over the random posterior, jointly over policies $\Gamma$ and best-response profiles $Q^*$. The function $K(p)$ of (B.1) is her cost when both parties hold belief $p$.

The thresholds are

$$\xi_h=\frac{a_1-a_0}{b_0-a_0-b_1+a_1},\qquad \underline\tau(p)=\frac{p(a_1-a_0)}{b_0-a_0},\qquad \bar\tau(p)=1-\frac{p(b_0-b_1)}{b_0-a_0}.$$

Formalization targets

Goal: Theorem 1 (p. 9)

For every prior $p_0\in[0,1]$:

$$\xi\in[\xi_h,1)\Rightarrow\text{full disclosure is optimal};\qquad \xi\in[\underline\tau(p_0),\xi_h]\Rightarrow\text{no disclosure is optimal};$$ $$\xi\in(0,\underline\tau(p_0)]\Rightarrow\Gamma^*\text{ is optimal},\quad \pi^*(m_1\mid\omega=0)=\frac{1-p_0}{p_0}\,\frac{\xi(b_0-a_0)}{(a_1-a_0)-\xi(b_0-a_0)},\ \ \pi^*(m_1\mid\omega=1)=1.$$

Milestones

1. Proposition 1 (p. 8): the supplier's optimal quantity $Q^*_p$ is unique and has an explicit three-piece form in $(p,\xi)$.
2. (B.2) (p. 25): the optimal value of (3) is $\kappa(p_0)$, where $\kappa$ is the lower convex envelope of $K$ on $[0,1]$.
3. (B.5) (p. 28): $K$ in closed form when $\xi\le(a_1-a_0)/(b_0-a_0)$.
4. Lemma 1 (p. 25): $\kappa$ in the three regimes of $\xi$.
5. The $\Gamma^*$ display (p. 26): under $\Gamma^*$, message $m_0$ has probability $(p_0-\hat p)/(1-\hat p)$ and induces posterior $1$, and, when $p_0<1$ (so that $m_1$ has positive probability), $m_1$ induces $\hat p=\xi(b_0-a_0)/(a_1-a_0)$.

Significance

The result shows that the optimal amount of disclosure depends on the critical ratio. When $\xi$ is high the retailer reveals everything; in an intermediate band she reveals nothing; when $\xi$ is low she uses a two-message policy that always reveals the narrow-support state ($\omega=1$ always sends $m_1$) but pools part of the wide-support state with it. Corollaries 1–4 of the paper read the thresholds off this theorem (independence of the prior for large $\xi$, full disclosure when $a_0=a_1$, never full disclosure when $b_0=b_1$), and Theorem 2 of the paper, on the value of information design relative to full and no disclosure, is built on Lemma 1 and (B.5).

The paper proves the result in its Online Appendix, citing Kamenica and Gentzkow for the reduction to a convex envelope. None of it has been machine-checked. A formalization would make the persuasion reduction explicit for finite message spaces and best-response profiles, and would check the case analysis of the envelope, where the paper prints one overlapping-indicator slip (Lemma 1, case 3).

Difficulty

The obvious argument is to compare the three named policies and pick the cheapest. That is not a proof: optimality is over every policy on every finite message space, and it is only the convex-envelope reduction that cuts the comparison down to splittings of the prior into posteriors. The reduction itself requires showing that the attainable expected costs are exactly the convex combinations of values of $K$ at Bayes-plausible posteriors. The envelope computation then needs the shape of $K$: the supplier's quantity is piecewise defined, so $K$ is a piecewise rational function of $p$ whose convexity changes across the boundaries $\underline\tau(p)=\xi$ and $\bar\tau(p)=\xi$. In the low-$\xi$ regime $K$ is neither convex nor concave on $[0,1]$, so its greatest convex minorant is a genuine mixture of $K$ itself and a line segment, whose junction point $\hat p$ has to be located exactly.

Formalization scope

States are Fin 2; a policy on a finite type $M$ is a map $\pi : \mathrm{Fin}\,2\to M\to\mathbb R$ with nonnegative entries and rows summing to $1$. The paper does not bound $\mathcal M$; finite message spaces are a convention, and binary spaces already attain the optimum. Uniform expectations are interval integrals divided by the length. The supplier's cost is normalized by $C_s+C_e$ and parameterized by $\xi$, which leaves its minimizers unchanged. A message of probability zero is given posterior $0$ and weight $0$.

The supplier's response is defined as an argmin of (2), never by the closed form of Proposition 1, and optimality quantifies over all finite policies and all best-response profiles, never over the three named policies; a formalization that hard-codes either would make the goal a statement about a formula. $K$ is evaluated at the largest optimal quantity, which is the unique one under the mission's hypotheses. The envelope $\kappa$ is the published definition BiconvexProg.BranchBound.convexEnvelope (greatest convex minorant) on $[0,1]$.

Standing hypotheses, stated in every theorem: $a_0<b_0$, $a_1<b_1$, $0<\xi<1$, $p_0\in[0,1]$, and nesting $a_0\le a_1$, $b_1\le b_0$. The hypotheses $0\le a_0$, $0\le a_1$ are added: demand is nonnegative, and without them the constraint $Q\ge0$ can bind. Equal supports are allowed; the threshold $\xi_h$ is then $0/0=0$ in Lean and the goal remains true. Lemma 1's third case is formalized as the piecewise function its two indicators intend.

A complete development needs: the convex-envelope (concavification) theorem for finite-support distributions on $[0,1]$, the newsvendor quantile characterization for a mixture of uniforms, and calculus for piecewise rational functions. The first two are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• O. Candogan, H. Gurkan, The Value of Information Design in Supply Chain Management, Management Science, 2024. SSRN preprint: https://ssrn.com/abstract=4378997; DOI: https://doi.org/10.1287/mnsc.2023.03004
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6), 2015. https://doi.org/10.1287/opre.2015.1422

Why self-preferencing is a regulatory question

Large retail platforms such as Amazon both host independent sellers and sell their own products in competition with them. The platform also controls the search ranking, the order in which products are shown to a consumer. The European Commission and the US Federal Trade Commission have examined whether platforms rank their own products ahead of rivals' (self-preferencing), and proposals of search neutrality would oblige a platform to rank products by relevance alone. The intuitive case for such a rule is that it protects consumers and third-party sellers.

T. Zou and B. Zhou, Self-Preferencing and Search Neutrality in Online Retail Platforms (Management Science, DOI 10.1287/mnsc.2022.01795), study this intuition in a duopoly model with consumer search and find that it can fail: when consumers see prices before searching, a platform free to steer consumers forces the third-party seller to cut its price to attract search, and neutrality removes that pressure. This mission formalizes their §4.2, which isolates the role of the commission rate $r$ the platform charges the third-party seller, at equal popularity of the two products.

Setting

A platform sells its own product $F$ and hosts a third-party seller of product $T$; production costs are zero. A unit mass of consumers has unit demand. A consumer of type $k\in\{f,t\}$ values a product at $1$ if it matches her taste and at $0$ otherwise. A type-$f$ consumer is matched by $F$ with probability $\rho_H$ and by $T$ with probability $\rho_L$; for a type-$t$ consumer the roles are swapped. Throughout, $0<\rho_L<\rho_H<1$. In this mission the two types have equal mass, $\alpha=1/2$.

Sellers set prices $p_F,p_T\in[0,1]$. The platform keeps a fraction $r$ of the third-party seller's revenue, so the profits are

$$\pi_F=p_FD_F+r\,p_TD_T,\qquad \pi_T=(1-r)\,p_TD_T,$$

where $D_j$ is the demand for product $j$.

For each consumer type the platform shows one product first: the prominent product. A consumer sees both prices before searching, learns whether the prominent product matches for free, and pays a search cost $c$, uniform on $[0,1]$, to inspect the other product. Optimal search yields the per-type demands (1)–(2) of the paper and a consumer surplus equal to the expected payoff of optimal search, averaged over types and over $c$.

Under search neutrality the ranking is fixed: $F$ is prominent for type $f$ and $T$ for type $t$. An equilibrium with neutrality is a pair of prices from which neither seller gains by a unilateral change. Without neutrality, the sellers set prices first and the platform then chooses, at whatever prices it sees, the ranking that maximizes its own profit from each consumer. An equilibrium is a pair of prices together with an optimal ranking rule $\sigma$, mapping prices to rankings, such that neither seller gains by changing its price, given that the ranking will respond.

Formalization targets

Goal: Proposition 5

At $\alpha=1/2$:

1. If $\rho_L/\rho_H<r<1$, search neutrality does not affect the outcome: every equilibrium without neutrality has the same prices, ranking, profits and consumer surplus as every equilibrium with neutrality.
2. If $0\le r<\rho_L/\rho_H$, every pair of equilibria satisfies

$$CS^{S}<CS^{NS},\qquad \pi_T^{NS}<\pi_T^{S}.$$

3. There is $\bar\rho<1$ such that, for $\bar\rho<\rho_L<\rho_H<1$ and every $r<\rho_L/\rho_H$, also $\pi_F^{NS}<\pi_F^{S}$.

Milestones

• Lemma 1 (p. 25): with neutrality the unique equilibrium is $p_F=p_T=1$, with $\pi_F=\rho_H(1+r)/2$ and $\pi_T=\rho_H(1-r)/2$.
• Proposition 4(1) (p. 24): without neutrality and with $r>\rho_L/\rho_H$, every equilibrium ranks neutrally and has $p_F=p_T=1$.
• The fixed-ranking game (Appendix, pp. 42–43): with $F$ prominent for all, the equilibrium is an explicit interior pair when $r<3-2/(\rho_H\rho_L)$ and $(1,\tfrac12)$ otherwise.
• Proposition 4(2) (p. 24): without neutrality and with $r<\rho_L/\rho_H$, every equilibrium makes $F$ prominent for all and has $p_F>p_T$; the prices are monotone in $r,\rho_H,\rho_L$ on the region $r\le 3-2/(\rho_H\rho_L)$ and equal $(1,\tfrac12)$ beyond it.
• The surplus display (Appendix, pp. 43–44): consumer surplus without neutrality as an explicit quadratic in the prices.

Significance

The result separates two regimes of a single policy question. With a high commission the platform already earns most of the revenue of product $T$ and has no incentive to steer; neutrality is then moot. With a low commission the platform steers every consumer to $F$; the third-party seller responds by pricing below $F$ to make search worthwhile, and consumers benefit from this competition. Imposing neutrality removes it, prices rise to $1$, and consumer surplus falls to zero, while the third-party seller gains. For high match probabilities the platform gains as well, which makes neutrality a commitment device a platform might accept voluntarily. Proposition 5 is the equal-popularity version of the paper's main short-term finding (Proposition 3, under a low commission), now valid for every commission rate.

The paper proves Proposition 5, Proposition 4 and Lemma 1 in an online appendix that is not part of the manuscript used here; the manuscript's own Appendix contains only the equilibrium derivations for the game with a fixed ranking. None of these results is machine-checked. A formalization would produce the first verified treatment of a pricing game with an endogenous, profit-maximizing ranking stage and of a consumer-surplus integral over search costs; the definitions are reusable for the companion mission on the low-commission regime and for other prominence models.

Difficulty

The demands are piecewise quadratic with a kink where the two prices cross, so profits are not concave on $[0,1]^2$, and first-order conditions only locate candidates. The central difficulty is the ranking stage. A seller's deviation can change the platform's ranking: the third-party seller may raise its price to make prominence for type $t$ worthwhile to the platform, and the platform as a seller may cut its price to undercut. Checking an equilibrium therefore requires comparing profits across ranking regimes at every deviation price, not only inside the regime of the candidate. The uniqueness claims require excluding equilibria in every regime, including those supported by an unusual tie-break of the ranking rule. The comparison of platform profits in part 3 compares the explicit interior prices of Proposition 4(2), a rational function of $(\rho_H,\rho_L,r)$, with $\rho_H(1+r)/2$; the paper gives no explicit threshold $\bar\rho$.

Formalization scope

• Parameters: $0<\rho_L<\rho_H<1$ and $0\le r<1$. The paper calls $r$ a percentage commission without stating its range; $r<1$ is needed because at $r=1$ the third-party seller's profit is identically zero and Lemma 1's uniqueness fails. Prices range over $[0,1]$ (p. 8).
• The equilibrium without neutrality is subgame perfect: the ranking rule must be optimal for the platform, type by type, at every price pair, and deviations are evaluated at the ranking chosen at the deviated prices. A ranking that is arbitrary, or optimal only at the equilibrium prices, would allow spurious equilibria and is ruled out by the definitions. Ties in the ranking may be broken arbitrarily, and statements about "every equilibrium" hold for every tie-break.
• "The equilibrium" is read as "every equilibrium"; existence is a separate conjunct of the milestones, so the comparisons of Proposition 5 are not vacuous.
• At the boundary $r=\rho_L/\rho_H$ the platform is indifferent for type-$t$ consumers at prices $(1,1)$, and two different equilibria exist depending on the tie-break. Statements about every equilibrium are made for $r>\rho_L/\rho_H$, and at the boundary only existence is claimed.
• Consumer surplus is defined from the search model as $\int_0^1$ over the search cost of the optimal-search payoff. It is not defined by the paper's closed-form display, which is a milestone.
• "Reduces" and "improves" in Proposition 5 and "increase/decrease" in Proposition 4(2) are read strictly. "Sufficiently large" is read as one threshold $\bar\rho<1$ independent of $r$.
• Definitions needed: two finite types, the demands (1)–(2), profits, ranking rules and their optimality, both equilibrium notions, and the surplus integral, all in SearchNeutrality.Commission.Model; the closed-form prices and surplus in SearchNeutrality.Commission.ClosedForms. These duplicate, with the same names, the definitions of the companion mission SearchNeutrality.ShortTerm.
• Contributions welcome: proofs of the milestones in any order, reusable lemmas on the per-type ranking comparison, and an explicit admissible $\bar\rho$.

Selected references

• T. Zou, B. Zhou, Self-Preferencing and Search Neutrality in Online Retail Platforms, Management Science (authors' manuscript), 2024. https://doi.org/10.1287/mnsc.2022.01795
• M. Armstrong, J. Vickers, J. Zhou, Prominence and consumer search, RAND Journal of Economics 40(2), 2009. https://doi.org/10.1111/j.1756-2171.2009.00067.x
• M. Armstrong, J. Zhou, Paying for prominence, Economic Journal 121(556), 2011. https://doi.org/10.1111/j.1468-0297.2011.02469.x

Motivation

Large data centers and cloud platforms route a stream of incoming tasks to many server pools, each pool able to serve several tasks at once. A dispatcher that sends each task to the least loaded pool (join-the-shortest-queue, JSQ) balances the load best, but it needs the exact number of tasks at every pool, which is costly to maintain at scale. A threshold dispatching rule needs much less information: it only needs to know which pools hold fewer than $\ell_n$ tasks, or fewer than $\ell_n+\Delta$ tasks. For constant arrival rates and exponential service it has the same fluid and diffusion limits as JSQ when $\Delta = 1$ and the threshold equals $\lfloor\rho\rfloor$, where $\rho$ is the offered load per pool (Goldsztajn, Borst, van Leeuwaarden, Mukherjee and Whiting, INFORMS Journal on Computing 34(1), 2022, reference [15] of arXiv:2012.10142v3).

The difficulty is that the right threshold depends on $\rho$, which the dispatcher does not know. Goldsztajn, Borst and van Leeuwaarden (arXiv:2012.10142v3) let the dispatcher learn it online. This mission concerns their second main result: with Coxian service times, which are dense among all service-time distributions, and the basic learning scheme, the threshold settles at the optimal value and the load becomes nearly balanced, almost surely in the many-server limit. (The first main result, for exponential service with a time-varying arrival rate and a refined learning scheme, is the subject of a companion mission.)

Setting

There are $n$ server pools. Tasks arrive as a Poisson process of rate $n\lambda$, $\lambda \ge 0$. A task passes through at most $r \ge 1$ phases: it starts in phase $1$, phase $m$ lasts an exponential time of rate $\mu_m > 0$, and after phase $m$ the task moves to phase $m+1$ with probability $p_m$ or leaves with probability $1-p_m$, with $p_r = 0$ and $p_m\in(0,1)$ for $m\ne r$. The mean service time $1/\mu$ follows from these data, and $\rho := \lambda/\mu$.

A pool has profile $\nu\in\mathbb N^r$ if it holds $\nu(m)$ tasks in phase $m$. The occupancy state $s_n(\nu)$ is the fraction of pools with profile $\nu$, a point of $S = \{s\in[0,1]^{\mathbb N^r} : \sum_\nu s(\nu) = 1\}$, and $q_n(i) = \sum_{\nu(1)+\dots+\nu(r)\ge i} s_n(\nu)$ is the fraction of pools with at least $i$ tasks.

Dispatching. With threshold $\ell_n$ and $h_n = \ell_n+\Delta$ for an integer $\Delta\ge1$, an arriving task goes to a uniformly random pool with fewer than $\ell_n$ tasks if there is one; otherwise to a uniformly random pool with fewer than $h_n$ tasks if there is one; otherwise to a uniformly random pool.

Basic learning. $\ell_n(t) = \lfloor u_n(t)\rfloor_\Delta$, where $u_n = \sum_{i\ge1}q_n(i)$ is the number of tasks divided by $n$ and $\lfloor x\rfloor_\Delta = \max\{k\Delta : k\Delta\le x,\ k\in\mathbb Z\}$.

All systems, for every $n$, are built on one probability space from independent unit-rate Poisson processes $\mathcal N_{(\nu,i,j)}$, i.i.d. uniform selection variables $U_j$ and random initial states $s_n(0)$, through the equations (21a)–(21b) of §6.1.1. Initial states converge, $s_n(0)\to s(0)$, and $q_n(0,B+1)=0$ for a fixed $B$.

Formalization targets

Goal: Theorem 3

If $\rho\notin\{i\Delta : i\in\mathbb N\}$, there are constants $\sigma,\eta,c>0$, independent of the horizon $T$, such that almost surely

$$\lim_{n\to\infty}\sup_{t\in[\sigma,T]}|\ell_n(t)-\lfloor\rho\rfloor_\Delta| = 0,\qquad \lim_{n\to\infty}\sup_{t\in[\sigma,T]}|1-q_n(t,i)| = 0\ \ (i\le\lfloor\rho\rfloor_\Delta),$$ $$\limsup_{n\to\infty}\sup_{t\in[\sigma,T]}\sum_{i>\lfloor\rho\rfloor_\Delta+\Delta} q_n(t,i)\,e^{\eta(t-\sigma)}\le c .$$

The constants are left unspecified, as in the paper; what is fixed is the shape: the threshold equals $\lfloor\rho\rfloor_\Delta$ after time $\sigma$, the first $\lfloor\rho\rfloor_\Delta$ columns are asymptotically full, and the excess mass decays exponentially.

Milestones

In the order the proof uses them: well-posedness of the coupled construction (§6.1.1); relative compactness of the occupancy and counting processes (Proposition 14); a uniform bound on occupancy and threshold over $[0,T]$ (Lemma 15); the set $\Omega_T$ of nice sample paths (Proposition 16); the almost-sure law of large numbers $u_n\to u$ for the total mass, with $u$ the infinite-server fluid function built from the residual-service survival functions $G_m$ (Proposition 17); and differential inequalities for the limits of the mass processes $x, y, z$ while the threshold is $\lfloor\rho\rfloor_\Delta$ (Proposition 18).

Significance

Theorem 3 says that a dispatcher that knows nothing about the load except the current number of tasks reaches the threshold JSQ-like balancing needs, and then balances the load: with $\Delta=1$, the fraction of pools with fewer than $\lfloor\rho\rfloor$ tasks vanishes and the fraction with more than $\lceil\rho\rceil$ tasks is $O(e^{-\eta(t-\sigma)})$, where $\eta=\min_m(1-p_m)\mu_m$ is a lower bound on the service hazard rate. Because Coxian laws are dense among service-time distributions, the result is evidence that threshold-based learning works beyond exponential service. Proposition 17 is also a statement of independent interest: the fluid law of large numbers for an infinite-server system with Coxian service, known to hold weakly, holds almost surely under this coupling.

The results are proved in the paper (arXiv:2012.10142v3, 2024). No part of them is formalized. The mission produces a machine-checked model of the coupled many-server construction with phase-type service, which no Lean library has, and a complete formal proof of the paper's almost-sure fluid-limit argument.

Difficulty

The statements are almost sure and pathwise, about one coupled sequence of jump processes with a countable state space $\mathbb N^r$, so weak-convergence arguments do not suffice. The natural first idea, to read off Theorem 3 from Proposition 17 alone, settles only (8a): $u_n\to u$ and $u(t)\to\rho$ force $\ell_n=\lfloor\rho\rfloor_\Delta$ eventually, but they say nothing about how the mass is distributed across the pools. Statements (8b) and (8c) require tracking the column masses $x_n, y_n, z_n$ through subsequential fluid limits that are only known to be Lipschitz, with dispatching decisions that depend discontinuously on the state. The phases complicate this: a pool's departure rate depends on the phases of its tasks, which the column picture ignores, and only the lower bound $\eta$ on the hazard rate controls the decay. The hypothesis $\rho\notin\Delta\mathbb N$ cannot be dropped: when $\rho$ is a multiple of $\Delta$, the threshold can oscillate between $\rho-\Delta$ and $\rho$.

Formalization scope

• Phases and profiles. Phases are Fin r; profiles are Fin r → ℕ; a fixed enumeration $\nu_i$ of $\mathbb N^r$ is a parameter. $q(i)$ is computed as $1-\sum_{\Sigma(\nu)<i}s(\nu)$, equal to (1) on $S$.
• Residual service. $G_m(t) = (e^{tQ}\mathbf 1)_m$ with the Coxian sub-generator $Q$ ($Q_{mm}=-\mu_m$, $Q_{m,m+1}=p_m\mu_m$).
• The construction is a structure: primitives (the published BesbesZeevi.Parametric.PoissonProcess for every driving process, their mutual independence, i.i.d. uniforms, independent initial conditions with $n\,s_n(0,\nu)\in\mathbb N$), plus processes that almost surely solve (21a)–(21b) for every $n\ge1$ and all $t\ge0$, are càdlàg, $S$-valued and have finitely many tasks. Left limits are Function.leftLim; $\nu-e_1$ and $\nu+e_m-e_{m+1}$ are guarded, never truncated. The dispatching indicators $r_{ij}$ are defined for all $i\ge0$, and the endpoints of $J_i(s,j)$ are corrected so that the intervals partition $[0,1)$ as the text states.
• $\Omega_T$ is a predicate collecting exactly the properties of Propositions 14 and 16; relative compactness with respect to $\varrho$ is rendered as subsequential coordinatewise uniform convergence on $[0,T]$.
• Theorem 3 quantifies $\exists\,\sigma,\eta,c>0$ before $\forall T$; with $T$ fixed first, (8c) would hold trivially with $c$ depending on $T$, because the occupancy vanishes beyond a column $B_T$. The tail sum in (8c) is taken in $[0,\infty]$, so it cannot be satisfied through a non-summable family, and $\eta$ must be positive.
• Needed infrastructure: functional strong laws for Poisson processes, Arzelà–Ascoli-type compactness in the uniform topology on càdlàg paths, a pathwise forward-induction construction of jump processes, and matrix-exponential facts for phase-type laws. The last three are reusable well beyond this mission. Contributions to any milestone, or to these supporting lemmas, are welcome.

Selected references

• D. Goldsztajn, S. C. Borst, J. S. H. van Leeuwaarden, Learning and balancing unknown loads in large-scale systems, arXiv:2012.10142v3, 2024. https://arxiv.org/abs/2012.10142v3
• D. Goldsztajn, S. C. Borst, J. S. H. van Leeuwaarden, D. Mukherjee, P. A. Whiting, Self-learning threshold-based load balancing, INFORMS Journal on Computing 34(1), pp. 39–54, 2022 (reference [15] of the paper above).
• M. Bramson, State space collapse with application to heavy traffic limits for multiclass queueing networks, Queueing Systems 30, 1998 (the compactness technique of Appendix A). https://doi.org/10.1023/A:1019108120366

Motivation

The reflected random walk $X_{n+1}=[X_n+U_{n+1}]^+$ is the waiting-time sequence of the single-server queue (Lindley's recursion). Additive functionals $\sum_{i\le n}X_i^p$ measure accumulated congestion. For $p=1$ this is the total waiting time, the area under the workload curve.

Existing general results on sample-path large deviations for additive functionals of Markov chains (in the Donsker–Varadhan line) assume the function to be bounded. They therefore do not cover the cumulative waiting time of a single-server queue. For $f(x)=x^p$ the relevant rare events are not produced by a small, uniform tilt of the whole trajectory but by a few busy periods of exceptional size, and the speed is sublinear.

Bazhba, Blanchet, Rhee and Zwart (arXiv:2003.14381, Mathematics of Operations Research, 2025) prove that the scaled partial-sum process satisfies a large deviation principle at the sublinear speed $n^{1/(1+p)}$. They also identify the rate function through a variational problem over paths of bounded variation.

Related work on large deviations of the area under a busy period either treats queue-length functionals (Blanchet–Glynn–Meyn, 2013) or assumes a moment generating function that is finite everywhere (Duffy–Meyn, 2014). Neither obtains a sample-path result. The present paper assumes only that the moment generating function of the increment is finite near the origin. It relies on the sample-path large deviations for light-tailed random walk trajectories of Borovkov and Mogulskii (II, III) and of Vysotsky (ALEA, 2021), and on the authors' earlier work in the $M_1'$ topology (Bazhba et al., 2020).

Setting

Let $U_1,U_2,\dots$ be i.i.d. copies of a real random variable $U$ with $\mu=\mathbf E(U)<0$. Let $\theta_+$ and $\theta_-$ be the supremum and infimum of $\{\theta:\mathbf E(e^{\theta U})<\infty\}$. The paper assumes:

1. $-\infty\le\theta_-<0<\theta_+\le\infty$ (Assumption 2.1);
2. $\log\mathbf P(U\ge n)/n\to-\theta_+$ and $\log\mathbf P(-U\ge n)/n\to\theta_-$ (Assumption 2.2);
3. $\mathbf P(U>0)>0$ (Assumption 2.3).

The chain is $X_0=0$, $X_{n+1}=[X_n+U_{n+1}]^+$. Fix $p>0$ and let $\alpha=1/(1+p)$. The object of study is

$$\bar Y_n(t)=\frac1n\sum_{i=1}^{\lfloor nt\rfloor}X_i^p,\qquad t\in[0,1].$$

The busy periods are delimited by the return times $T_0=0$, $T_i=\inf\{k>T_{i-1}:X_k=0\}$. The busy-period areas are $W_j=\sum_{i=T_{j-1}+1}^{T_j}X_i^p$, and the long-run mean of $X^p$ is $\lambda=\mathbf E(W_1)/\mathbf E(T_1)$.

$\bar Y_n$ lives in the Skorokhod space $\mathbb D[0,1]$ of càdlàg paths. This space carries the $M_1'$ metric $d_{M_1'}$ (Definitions 2.1–2.2). It compares parametrizations of the extended completed graph, which joins each jump by a vertical segment and also joins $0$ to $\xi(0)$ at the origin ($\xi(0-)=0$).

The rate function involves the variational problem

$$\mathcal B^*_y=\inf_{\xi\in B_y}I_y(\xi).$$

Here $B_y$ is the set of paths $\xi$ of bounded variation on compacts with $\xi(0)=y$ whose reflected area $\int_0^{\mathcal T(\xi)}\Psi(\xi)(s)^p\,ds$ up to the first return time $\mathcal T(\xi)$ of $\Psi(\xi)$ to zero is at least $1$. $\Psi(\xi)(t)=\xi(t)-\inf_{s\le t}(\xi(s)\wedge0)$ is the reflection map. The cost is

$$I_y(\xi)=\int_0^{\mathcal T(\xi)}\Lambda^*(\dot\xi^{(a)}(s))\,ds+\theta_+\xi^{(u)}(\mathcal T(\xi))+\theta_-\xi^{(d)}(\mathcal T(\xi)),$$

where $\Lambda^*$ is the Legendre transform of $\log\mathbf Ee^{\theta U}$ and $\xi^{(a)},\xi^{(u)},\xi^{(d)}$ are the absolutely continuous, upward singular and downward singular parts of $\xi$.

Formalization targets

Goal: Theorem 2.1

$\bar Y_n$ satisfies the large deviation principle in $(\mathbb D[0,1],\mathcal T_{M_1'})$ with speed $n^\alpha$ and rate function

$$I_Y(\zeta)=\begin{cases}\mathcal B^*_0\sum_{t:\zeta(t)\neq\zeta(t-)}(\zeta(t)-\zeta(t-))^\alpha & \zeta\in\mathbb D^{(\lambda)}[0,1],\\ \infty&\text{otherwise,}\end{cases}$$

where $\mathbb D^{(\lambda)}[0,1]$ is the set of paths $\lambda t+\zeta(t)$ with $\zeta$ a non-decreasing pure jump path, $\zeta(0)\ge0$.

Busy-period tails

• Theorem 2.2: $\lim_{t\to\infty}t^{-\alpha}\log\mathbf P(W_1\ge t)=-\mathcal B^*_0$.
• Theorem 2.3: $\lim_{n\to\infty}n^{-\alpha}\log\mathbf P(V_n\ge nb)=-\mathcal B^*_0b^\alpha$ for the last, incomplete busy period.

Milestones

1. The variational problem. Lemma 4.1 ($\mathcal B^*_y=0$ beyond $\bar y=(|\mu|(p+1))^\alpha$, and the restriction to absolutely continuous paths). Proposition 4.1 (monotonicity, Lipschitz continuity, $\mathcal B^*_y\in(0,\infty)$ on $[0,\bar y)$). Lemma 4.4 (finite horizon). Lemma 4.5 (uniform $M_1'$ continuity of the area on level sets).
2. Busy-period estimates. Lemma 4.6, Proposition 4.2, and Proposition 4.3(ii) ($\mathcal B^*_0=\mathcal B^*_\pi$).
3. The decomposition. Lemma 3.1 (LDP for the last busy period), Lemmas 3.2–3.3 (finite-dimensional LDP), Lemma 3.7 (LDP for completed busy periods in $M_1'$), and Lemma 3.8 (exponential equivalence).

Significance

The result. The theorem gives the full large deviation behaviour of $\sum X_i^p$, not only its one-dimensional tail. It identifies the mechanism of rare events: one or a few busy periods of area of order $n$, each contributing $\mathcal B^*_0$ times its area to the power $\alpha$. In the rate function, a busy period in progress at the end of the horizon is indistinguishable from a completed one; the paper's Theorem 2.3 and Proposition 4.3 make this precise. By contraction the theorem yields tail asymptotics for any $M_1'$-continuous functional of the cumulative cost process.

The formalization. The result is proved on paper. No part of it has been machine-checked, and the platform has no Skorokhod $M_1'$ metric and no large deviation principle at a sublinear speed. A complete development would supply the first formal $M_1'$ metric on $\mathbb D[0,T]$ and a sample-path LDP for a heavy-tailed regime. It would also provide a formal treatment of variational problems over paths of bounded variation with singular parts.

Difficulty

The obvious route is the contraction principle applied to the sample-path LDP for the scaled random walk $\bar K_n$, followed by the map that sends the walk to the area under its reflection up to its first return to zero. That map is not continuous: the first passage time is discontinuous in every Skorokhod topology. The paper replaces the random horizon by a large fixed horizon $T$, but then must show that the variational problems over $[0,T]$ and over $[0,\mathcal T(\xi)]$ have the same value (Lemma 4.4). It must also prove uniform continuity of the area functional on level sets of the rate function (Lemma 4.5).

A second difficulty is the class of admissible paths. Because $\theta_\pm$ may be finite, optimal paths could a priori contain jumps or singular parts. Lemma 4.1 rules this out. Finally, the passage from the finite-dimensional LDP to the $M_1'$ topology requires the busy period in progress at time $n$ to be handled separately. The mere existence of the limit in Theorem 2.3 relies on a time-reversal argument and on the decay rate of the stationary distribution.

Formalization scope

• Increments. A sequence U : ℕ → Ω → ℝ, measurable, independent and identically distributed, with U i the paper's $U_{i+1}$. Moments are lower Lebesgue integrals in $[0,\infty]$, never Mathlib's mgf. $\theta_\pm\in[-\infty,\infty]$.
• Logarithms and limits. All logarithms are ENNReal.log with $\log0=-\infty$; liminf and limsup are taken in EReal. Probabilities of possibly non-measurable events are outer measures.
• Path space. $\mathbb D[0,T]$ consists of functions $\mathbb R\to\mathbb R$, càdlàg on $[0,T]$ and constant outside. $\xi(0-)=0$. Parametrizations are on $[0,T]$, and "nondecreasing" uses the reflexive closure of the printed strict order. $d_{M_1'}$ takes values in $[0,\infty]$.
• Rate function ingredients. Costs, $\mathcal B^*_y$, $\mathcal B^*_\pi$, $\mathcal V^{T*}_y$, $\beta$ and all rate functions take values in $[0,\infty]$, with $\theta_+\cdot0=0$ when $\theta_+=\infty$. The exit time $\mathcal T(\xi)$ lies in $[0,\infty]$; the return times $T_i$ lie in $\mathbb N\cup\{\infty\}$. The cost of a bounded-variation path is the infimum over its representations $\xi(0)+\int g+\sigma_u-\sigma_d$ with singular non-decreasing $\sigma_u,\sigma_d$; this infimum is attained at the Hahn–Jordan decomposition. The downward singular cost is nonnegative (the sign on p. 22 is a typo).
• The goal. It is stated with $T=1$, as in the paper's proof. The LDP is given by bounds for open and closed sets, which is equivalent to (2.2).
• Ruling out trivial readings. $B_y$ and $V^T_y$ range over all paths, with jumps and singular parts, and $\mathcal B^*_0$ and $\lambda$ are defined from the data, not assumed. Restricting either problem to absolutely continuous paths would make Lemma 4.1(ii) a tautology. Taking $\theta_\pm$ infinite, $p=1$, or the $J_1$ topology would change the theorem.
• Infrastructure. A complete development needs sample-path LDPs for random walks in $M_1'$ (the cited Results B.1–B.3), the Dawson–Gärtner projective limit theorem, Lebesgue decompositions of BV functions, and regenerative structure of the reflected random walk. The $M_1'$ metric, the LDP vocabulary at general speed and the bounded-variation cost are reusable beyond this mission.

Contributions to any milestone, and formalizations of the cited Results B.1–B.3, are welcome.

Selected references

• M. Bazhba, J. Blanchet, C.-H. Rhee, B. Zwart, Sample-path large deviations for unbounded additive functionals of the reflected random walk, Mathematics of Operations Research, 2025; arXiv:2003.14381v3. https://arxiv.org/abs/2003.14381
• M. Bazhba, J. Blanchet, C.-H. Rhee, B. Zwart, Sample path large deviations for Lévy processes and random walks with Weibull increments, Annals of Applied Probability 30(6), 2020. https://doi.org/10.1214/20-AAP1570
• J. Blanchet, P. Glynn, S. Meyn, Large deviations for the empirical mean of an M/M/1 queue, Queueing Systems 73(4), 2013. https://doi.org/10.1007/s11134-013-9349-7
• A. A. Borovkov, A. A. Mogulskii, Large deviation principles for random walk trajectories. II, Theory of Probability and its Applications 57(1), 2013. https://doi.org/10.1137/S0040585X97985765
• A. A. Borovkov, A. A. Mogulskii, Large deviation principles for random walk trajectories. III, Theory of Probability and its Applications 58(1), 2014. https://doi.org/10.1137/S0040585X97986370
• K. R. Duffy, S. P. Meyn, Large deviation asymptotics for busy periods, Stochastic Systems 4(1), 2014. https://doi.org/10.1214/13-SSY098
• V. Vysotsky, Contraction principle for trajectories of random walks and Cramér's theorem for kernel-weighted sums, ALEA. Latin American Journal of Probability and Mathematical Statistics 18(2):1103–1125, 2021.
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, Springer, 2010 (corrected reprint of the 2nd ed.). https://doi.org/10.1007/978-3-642-03311-7
• W. Whitt, Stochastic-Process Limits, Springer, 2002. https://doi.org/10.1007/b97479