Operations Research

Motivation

Many-server queues are the basic model of call centres and hospital wards, and the Halfin–Whitt regime (the number of servers $n$ grows while the traffic intensity approaches one at rate $n^{-1/2}$) is where such systems operate efficiently and with short delays. In this regime the centred and scaled queue process of a $G/Ph/n+GI$ queue (general arrivals, phase-type service, $n$ servers, generally distributed patience) converges to a $d$-dimensional diffusion, $d$ being the number of service phases (Dai, He and Tezcan, Ann. Appl. Probab. 2010). For $GI/Ph/n+M$ queues the stationary distribution of the queue converges to the invariant measure $\mu$ of that diffusion (Dai, Dieker and Gao, Queueing Systems 2014). So $\mu$ is the object one would like to compute.

With exponential service the diffusion is one-dimensional and $\mu$ is explicit. With phase-type service it is multidimensional with a piecewise-linear drift; Dieker and Gao (Ann. Appl. Probab. 2013) proved that it is exponentially ergodic with a unique $\mu$, but no closed form is known, and the characterization of multidimensional piecewise-linear diffusions was left open in Browne and Whitt (1995). Jin, Pang, Xu and Xu (arXiv:2209.07361) approximate $\mu$ by the invariant measure of the Euler–Maruyama discretization and give an explicit error rate in the Wasserstein-1 distance.

Setting

Fix $d\ge1$, a patience rate $\alpha>0$, a slack $\beta\in\mathbb R$, a probability vector $p\in\mathbb R^d$, service rates $v_1,\dots,v_d>0$ and a sub-stochastic phase-transition matrix $P$ with $P_{ii}=0$ and $I-P$ invertible. Let $R=(I-P')\,\mathrm{diag}(v)$, $e=(1,\dots,1)'$, and assume the phase-type distribution has mean one, $e'R^{-1}p=1$. The drift is the piecewise-linear map

$$g(x)=-\beta p-Rx+(R-\alpha I)p\,(e'x)^+,\qquad y^+=\max\{0,y\}.$$

Let $\sigma$ be a $d\times d$ matrix with $\xi'\sigma\sigma'\xi\ge c\,\xi'\xi$ for some $c>0$ (in the queueing model $\sigma\sigma'$ has an explicit formula in terms of the arrival variability $c_a^2$, $p$, $P$, $v$; only the ellipticity is used). The limiting diffusion is

$$X_t=x+\int_0^t g(X_s)\,ds+\sigma B_t,$$

with $B$ a standard $d$-dimensional Brownian motion; $P_t(x,\cdot)$ is the law of $X_t$ started at $x$, and $\mu$ is a probability measure with $\int P_t(x,\cdot)\,\mu(dx)=\mu$ for all $t\ge0$.

The Euler–Maruyama chain with step $\eta>0$ is

$$\tilde X^\eta_{k+1}=\tilde X^\eta_k+g(\tilde X^\eta_k)\,\eta+\sqrt\eta\,\sigma\xi_{k+1},\qquad k\in\mathbb N_0,$$

with independent standard Gaussian $\xi_k$; its one-step kernel is $\tilde P_\eta(x,\cdot)=\mathcal N(x+\eta g(x),\eta\sigma\sigma')$, and $\tilde\mu_\eta$ denotes an invariant probability measure of it. The Wasserstein-1 distance is taken in its dual form

$$d_W(\mu_1,\mu_2)=\sup_{h\in\mathrm{Lip}(1)}\Big|\int h\,d\mu_1-\int h\,d\mu_2\Big|,$$

where $\mathrm{Lip}(1)$ is the set of $h$ with $|h(x)-h(y)|\le|x-y|$.

Formalization targets

Goal: Theorem 1.2(i)

There is $\eta_0>0$ such that for every $\varsigma\in(0,1)$ there is $C_\varsigma>0$, depending on $\varsigma$ but not on $\eta$, such that for every $\eta\in(0,\eta_0]$ the chain has a unique invariant probability measure $\tilde\mu_\eta$ and

$$d_W(\mu,\tilde\mu_\eta)\le C_\varsigma\,\eta^{\frac{1-\varsigma}{2}}.$$

The constants are left unspecified, so the goal survives any improvement of them.

Milestones

In the order the proof uses them:

1. (A.4)–(A.7): a $C^2$ Lyapunov function $V$ with $\hat c_1|y|^2\le V(y)\le\hat C|y|^2+\hat C'$, $|\nabla V(y)|\le C(1+|y|)$ and $\mathcal AV\le-c_1V+\breve c_1$, where $\mathcal A$ is the generator.
2. Lemma A.1: moment bounds $\mathbb EV^\ell(X^x_t)\le e^{-c_1t}V^\ell(x)+\breve c_\ell(1-e^{-c_1t})/c_1$, and exponential ergodicity of the diffusion in $d_W$ and in weighted total variation.
3. Lemma A.2: $\tilde P_\eta f$ is Lipschitz for bounded measurable $f$ (strong Feller), and the chain is irreducible.
4. Lemma A.3: the one-step error $\mathbb E|X^x_\eta-\tilde X^{\eta,x}_1|^{2\ell}\le\tilde C_\ell(1+V^\ell(x))\eta^{3\ell}$.
5. Lemma A.4: the drift condition $\tilde P_\eta V^\ell\le(e^{-c_1\eta}+\tilde C_\ell\eta^{3/2})V^\ell+\check K_\ell$ for the chain.
6. Proposition 2.1: existence, uniqueness and exponential ergodicity of $\tilde\mu_\eta$, and $\tilde\mu_\eta(|\cdot|^\ell)\le C$ uniformly in $\eta$.
7. Lemma 2.2: for the solution $f$ of the Stein equation $\mathcal Af=h-\mu(h)$ with $h\in\mathrm{Lip}_0(1)$, the polynomial bounds on $f,\nabla f,\nabla^2f$ and the local $(1-\varsigma)$-Hölder bound on $\nabla^2 f$.
8. (2.7)–(2.8): the second-order Taylor remainder in Stein's argument is $O(\eta^{(3-\varsigma)/2})$.

Significance

The theorem gives a computable approximation of the stationary distribution of the diffusion limit, with an explicit rate. Combined with the convergence of the scaled queue's stationary distribution to $\mu$ at rate $n^{(\varsigma-1)/2}$ for $M/Ph/n+M$ queues (Braverman and Dai), it yields an approximation of the steady state of the queue itself, by simulating the chain for $O(n\log n)$ steps (Remark 2.3 of the paper). Proposition 2.1 also shows that the explicit Euler scheme does not blow up for this non-gradient, non-differentiable drift, which is not automatic: the Euler scheme of an ergodic SDE may blow up.

The result is proved in the paper; nothing here is open mathematically, though Lemma 2.2 is imported from Gurvich's regularity theory rather than proved there. To our knowledge none of it is formalized. A formalization provides the first machine-checked Wasserstein bound between the invariant measures of a multidimensional diffusion and its discretization, and on the way the Lyapunov and Harris-type ergodicity theory of Euler–Maruyama chains.

Difficulty

Standard error analyses of Euler schemes for invariant measures assume a gradient drift, strong dissipativity, or several bounded derivatives; none holds here. The drift is not differentiable on the hyperplane $\{e'x=0\}$ and is dissipative only in the Lyapunov sense of Dieker and Gao, so contraction-based couplings do not apply. The Stein argument instead needs second derivatives of the Stein solution $f$ that are Hölder continuous with polynomially growing constants; this is where the loss $\eta^{-\varsigma/2}$ comes from, and it rests on elliptic regularity for an operator with only Lipschitz coefficients. The ergodicity of the chain must also hold with constants uniform in $\eta$, which the classical Lyapunov criteria do not give directly.

Formalization scope

• The state space is EuclideanSpace ℝ (Fin d), so $|\cdot|$ is the Euclidean norm; matrices act by the usual product, and $\|A\|_{\mathrm{op}}=\sup_{|u|=1}|Au|$.
• $\sigma$ is a general uniformly elliptic matrix, not the paper's explicit covariance; the general case contains the paper's.
• Brownian motion is the published EthierKurtz.IsStandardBrownian (time ℝ≥0). The diffusion is a pathwise integral equation with continuous paths, so no Itô integral is needed. The transition function $P_t$ is characterized by: on every probability space, every solution from $x$ has law $P_t(x,\cdot)$ at time $t$. $\mu$ is a hypothesis (an invariant probability measure of $P_t$), never assumed smooth or with moments.
• The chain's kernel is the image of stdGaussian under $z\mapsto x+\eta g(x)+\sqrt\eta\,\sigma z$; $k\in\mathbb N_0$ starts at $0$.
• $d_W$, $\|\cdot\|_{\mathrm{TV}}$ and $\|\cdot\|_{\mathrm{TV},V}$ take values in $[0,\infty]$ and equal $+\infty$ unless the needed first moment (or $\int(1+V)$) is finite; so a bound on $d_W$ cannot hold because an integral of a non-integrable test function defaults to $0$. All moment bounds are lower Lebesgue integrals.
• "For any small enough $\varsigma$" is read as every $\varsigma\in(0,1)$; the step threshold $\eta_0$ is chosen before $\varsigma$, and $C_\varsigma$ before $\eta$.
• The Stein solution is $f=-\int_0^\infty(P_th-\mu(h))\,dt$ (the paper's (3.2)); Lemma 2.2 concludes that it is $C^2$ and solves $\mathcal Af=h-\mu(h)$, so its derivatives are never junk.
• Lemma A.2's gradient bound is stated in Lipschitz form, since $\tilde P_\eta f$ need not be differentiable where $g$ is not.

Trivializing encodings are excluded: the existence and uniqueness of $\tilde\mu_\eta$ is a conclusion, not a hypothesis, and the distance is infinite rather than zero when moments fail.

A complete development needs Brownian motion with Gaussian increments, a pathwise SDE solution theory for Lipschitz drift, Itô's formula (or Dynkin's formula) for $C^2$ functions of additive-noise diffusions, Harris-type ergodic theorems for Feller chains and diffusions, and elliptic regularity for the Stein equation. The Harris theorems and Wasserstein machinery are reusable well beyond this mission. Contributions to any milestone, and to general infrastructure for Euler–Maruyama chains, are welcome.

Selected references

• X. H. 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
• A. B. Dieker, X. Gao, Positive recurrence of piecewise Ornstein–Uhlenbeck processes and common quadratic Lyapunov functions, Annals of Applied Probability 23(4): 1291–1317, 2013.
• J. G. Dai, S. He, T. Tezcan, Many-server diffusion limits for G/Ph/n+GI queues, Annals of Applied Probability 20(5): 1854–1890, 2010.
• J. G. Dai, A. B. Dieker, X. Gao, Validity of heavy-traffic steady-state approximations in many-server queues with abandonment, Queueing Systems 78(1): 1–29, 2014.
• S. Browne, W. Whitt, Piecewise-linear diffusion processes, in J. Dshalalow (ed.), Advances in Queueing: Theory, Methods, and Open Problems, 463–480, 1995.
• I. Gurvich, Diffusion models and steady-state approximations for exponentially ergodic Markovian queues, Annals of Applied Probability 24(6): 2527–2559, 2014.
• A. Braverman, J. G. Dai, Stein's method for steady-state diffusion approximations of M/Ph/n+M systems, Annals of Applied Probability 27(1): 550–581, 2017.
• M. Hairer, J. C. Mattingly, Spectral gaps in Wasserstein distances and the 2D stochastic Navier–Stokes equations, Annals of Probability 36(6): 2050–2091, 2008.

Bibliographic data as in the reference list of arXiv:2209.07361v1, pp. 35–37.

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

Randomized load balancing assigns arriving jobs to one of several parallel servers using only partial information about queue lengths. The best-known example is the power-of-choice rule: sample $\ell$ of the $N$ queues and join the shortest. Such rules are used in large server farms because the dispatcher communicates with only a few servers per job. The case of exponential service times and power-of-choice routing in this regime was treated by Banerjee, Budhiraja and Estevez.

Atar and Ichiba (arXiv:2409.15121) study a fixed number $N$ of critically loaded queues in the diffusion (heavy-traffic) regime. Each queue has its own dedicated arrival stream. A thinner load-balancing stream is routed by rank: a job joins the queue whose current length has rank $r$ with probability $p_r$. Because ties in queue length are frequent, the natural limit is not a stochastic differential equation but a stochastic differential inclusion in which the drift is only known to lie in a set. Rank-based diffusions, where the drift of a particle depends on its rank among all particles, are studied independently in stochastic portfolio theory and interacting particle systems (for example Banner, Fernholz and Karatzas and Ichiba, Karatzas and Shkolnikov). This paper connects them to queueing.

Setting

There are $N$ servers, indexed by $[N]=\{1,\dots,N\}$. For $x\in\mathbb R^N$ the rank of coordinate $i$ is $\mathrm{rank}(i;x)=\#\{j:x_j<x_i\}+\#\{j\le i:x_j=x_i\}$, so ties go to the smaller index. For a permutation $\pi$ of $[N]$ write $b_\pi=(b_{\pi(1)},\dots,b_{\pi(N)})$. The order-compatible permutations of $x$ are $\mathfrak P(x)=\{\pi: x_i<x_j\Rightarrow\pi(i)<\pi(j)\}$.

The queueing model. A sequence of systems is indexed by $n$. In the $n$-th system:

• queue $i$ receives a Poisson stream $E^n_i$ of rate $\lambda^n_i$;
• a Poisson load-balancing stream $A^n_0$ of rate $\lambda^n_0$ is routed by i.i.d. marks $\theta_k$ with $P(\theta_k=r)=p_r$, where $p_1\ge\dots\ge p_N$;
• the $k$-th load-balancing job joins the queue whose rank, just before the arrival, equals $\theta_k$;
• server $i$ has i.i.d. service times with mean $1/\mu^n_i$ and squared coefficient of variation $(\sigma^{ser}_i)^2$.

The queue lengths $X^n$ and busy times $T^n$ satisfy the usual balance equations. The scaling is:

• $n^{-1/2}(\lambda^n_i-n\lambda_i)\to\hat\lambda_i$, $n^{-1/2}\lambda^n_0\to\lambda_0>0$ and $n^{-1/2}(\mu^n_i-n\mu_i)\to\hat\mu_i$;
• critical load $\lambda_i=\mu_i$;
• initial residual service times are $o(n^{-1/2})$;
• (IC₀): $\hat X^n(0-)=n^{-1/2}X^n(0-)$ converges in law to a law $\mu_0$ on $\mathbb R^N_+$.

The diffusion-scaled processes are $\hat X^n_i(t)=n^{-1/2}X^n_i(t)$ and $\hat L^n_i(t)=n^{-1/2}\mu^n_i(t-T^n_i(t))$, the scaled queue length and scaled cumulative idle time.

The limit equations. Given $b,m\in\mathbb R^N$ and $\sigma\in(0,\infty)^N$, the reflected rank-based SDE (SDER) is

$$X_i(t)=X_i(0)+\sigma_iB_i(t)+m_it+\int_0^t b_{\mathrm{rank}(i;X(s))}\,ds+L_i(t)\ge0,\qquad \int_0^\infty X_i\,dL_i=0 .$$

Here $L_i$ is continuous, nondecreasing, starts at $0$, and increases only when $X_i=0$. The inclusion (SDIR) replaces the drift by a progressively measurable $\beta(t)\in\mathrm{conv}\{b_\pi:\pi\in\mathfrak P(X(t))\}$ for a.e. $t$. A weak solution is a filtered probability space satisfying the usual conditions, carrying an $N$-dimensional Brownian motion $B$ and adapted processes satisfying the equation almost surely.

Formalization targets

Goal: Theorem 2.3(i)

Define the limit data from the queue:

$$b_r=\lambda_0p_r,\qquad m_i=\hat\lambda_i-\hat\mu_i,\qquad \sigma_i=\big(\lambda_i+\mu_i(\sigma^{ser}_i)^2\big)^{1/2}.$$

Under (IC₀), there is a weak solution $(X,L,B)$ of (SDER), which is also a weak solution of (SDIR) with $\beta(t)=b_{\mathrm{rank}(\cdot;X(t))}$, with $X(0)\sim\mu_0$ and

$$(\hat X^n,\hat L^n)\Rightarrow(X,L)\quad\text{in } D(\mathbb R_+,\mathbb R^N)\times C(\mathbb R_+,\mathbb R^N).$$

The goal is stated in existence form. The paper's phrase "the solution" relies on uniqueness in law, which it obtains from pathwise uniqueness through a cited Yamada–Watanabe-type argument (Remark 2.1).

Milestones

The milestones are the results the paper's proof uses, in order:

• the monotonicity inequality (3.2) for the drift sets when $b$ is nonincreasing;
• pathwise uniqueness for (SDI) and (SDIR) (Proposition 3.1);
• solutions of (SDE)/(SDER) solve (SDI)/(SDIR) (Remark 3.2);
• Skorokhod's lemma (Lemma 4.2);
• the martingale property of the routing compensator (Lemma 4.3);
• the reflection representation, the functional central limit theorem for the primitives, and C-tightness (Lemma 4.4(i)–(iii));
• tightness, identification of subsequential limits, and convergence to (SDIR) (Proposition 4.1(i)–(iii));
• the Lebesgue-null collision set (5.15), which turns (SDIR) into (SDER).

Significance

The theorem identifies the heavy-traffic limit of rank-based randomized routing for every routing vector $p$ with $p_1\ge\dots\ge p_N$, including both versions of power-of-$\ell$-choices. The limit is a reflected rank-based diffusion: routing enters only through the drift $b=\lambda_0p$, which depends on the queues' ranks. Along the way, the paper proves pathwise uniqueness for a class of rank-based differential inclusions, a result of independent interest for rank-based diffusions with arbitrary tie behaviour.

The results are proved on paper. No part of them is machine-checked. A formalization would produce:

• a reusable definition layer: weak solutions of reflected SDEs and SDIs, C-tightness, Poisson processes, and a queueing model with general service times;
• checked proofs of Skorokhod's lemma in its complementarity form and of the drift-set monotonicity;
• a precise record of where the argument relies on cited results: Remark 2.1, a renewal FCLT, Tanaka's formula, and a measurable-selection argument from Atar, Budhiraja and Ramanan (Probab. Theory Related Fields 142, 2008), and Yamada and Watanabe with Kurtz for uniqueness in law.

Difficulty

The obvious route is to write the limit as an SDE with drift $b_{\mathrm{rank}(i;X)}$ and pass to the limit. That route fails because $x\mapsto b_{\mathrm{rank}(\cdot;x)}$ is discontinuous exactly on the ties $\{x_i=x_j\}$. Limits of the queueing drift there are only constrained to a convex hull of permuted vectors. The paper therefore works with the inclusion (SDIR) and needs three things:

• Uniqueness for a discontinuous, set-valued drift. This rests on a monotonicity property of $\mathrm{conv}\{b_\pi:\pi\in\mathfrak P(x)\}$ derived from the rearrangement inequality.
• A progressively measurable selection of the a.e. derivative of the limiting compensator.
• A local-time estimate showing that two coordinates of the limit spend zero Lebesgue time together, so the inclusion collapses to the equation.

The queueing side brings its own difficulty. The routing depends on the rank at left limits $X^n(s-)$, so the compensator of the routed stream is a random time change, and it must be shown to be a martingale for the system's history.

Formalization scope

Conventions committed to:

• servers and ranks are Fin N, so the paper's index $i$ is Lean's $i-1$;
• paths are maps $\mathbb R\to\mathbb R^N$ evaluated at $t\ge0$, and filtrations are indexed by $\mathbb R_{\ge0}$;
• norms are $\ell^1$, through the referenced BellWilliams2001.ThresholdPolicy.Paths; this is equivalent to the paper's Euclidean norm;
• all systems live on one probability space; the model equations hold almost surely, while sample-path properties hold for every $\omega$;
• routing is the finite sum over arrival epochs with the rank at left limits, and the marks may depend on $n$;
• the potential service process uses the paper's index base $0$ (initial residual time included);
• the constants $b,m,\sigma$ are computed from the model, never free;
• the integrals $\int X_i\,dL_i$ and $\int x\,dz$ are lintegrals against Stieltjes measures, with $z(0-)=0$;
• the usual conditions take the Karatzas–Shreve form;
• C-tightness is the Jacod–Shiryaev VI.3.26 criterion;
• weak convergence to continuous limits is in Skorokhod-coupling form (CouplingConverges);
• limit spaces are Ω' : Type.

The goal is not trivialized by a vacuous model. The structure LoadBalancingSequence imposes only the paper's assumptions, and the limit is required to be a genuine weak solution, with an $\mathbb F$-Brownian motion, adaptedness, progressive measurability and the a.e.-$t$ inclusion. A statement for a fixed $n$, for $N=2$ only, for exponential service, for power-of-choice only, or with free $b,m,\sigma$ would be a different theorem.

A complete development needs:

• Poisson and renewal functional central limit theorems;
• martingale methods for counting processes;
• the one-dimensional Skorokhod map;
• the Skorokhod representation theorem;
• Itô and Tanaka formulas for continuous semimartingales;
• Yamada–Watanabe-type uniqueness in law.

The rank, drift-set, reflection and C-tightness definitions are reusable beyond this mission. Contributions to any milestone are welcome, including a sharper version of Proposition 4.1(iii) asserting uniqueness in law.

Selected references

• R. Atar and T. Ichiba, Rank-Based Stochastic Differential Inclusions and Diffusion Limits for a Load Balancing Model, arXiv preprint, 2024. https://arxiv.org/abs/2409.15121
• S. Banerjee, A. Budhiraja and B. Estevez, Load balancing in parallel queues and rank-based diffusions, arXiv preprint, 2023. https://arxiv.org/abs/2302.10317
• A. D. Banner, R. Fernholz and I. Karatzas, Atlas models of equity markets, Ann. Appl. Probab. 15, 2005. https://doi.org/10.1214/105051605000000449
• T. Ichiba, I. Karatzas and M. Shkolnikov, Strong solutions of stochastic equations with rank-based coefficients, Probab. Theory Related Fields 156, 2013. https://doi.org/10.1007/s00440-012-0426-3
• T. Yamada and S. Watanabe, On the uniqueness of solutions of stochastic differential equations, J. Math. Kyoto Univ. 11, 1971. https://doi.org/10.1215/kjm/1250523691
• T. G. Kurtz, Weak and strong solutions of general stochastic models, Electron. Commun. Probab. 19, 2014. https://doi.org/10.1214/ECP.v19-2833
• J. Jacod and A. N. Shiryaev, Limit Theorems for Stochastic Processes, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-662-05265-5

Motivation

Many operational risk questions ask for a small probability $p_u=P(L(X)\ge u)$: the chance that the cost $L$ of a decision, evaluated at a random scenario $X\in\mathbb R^d$, exceeds a large threshold $u$. Examples are large delays in project networks or vehicle routing, large portfolio credit losses, and failures in engineered systems. Plain Monte Carlo needs on the order of $p_u^{-1}$ samples to estimate $p_u$ to fixed relative accuracy, which is prohibitive when $p_u$ is $10^{-6}$ or smaller. Importance sampling (IS) draws samples from a different distribution and reweights them by a likelihood ratio, but classical efficient IS schemes are built for one model at a time: they need the distribution of $X$ and the structure of $L$ (e.g. linearity or convexity) to solve for a good sampling distribution.

Deo and Murthy (arXiv:2102.07060v3, published in Operations Research, 2025) propose a self-structuring sampler that needs neither: it applies a fixed multiplicative stretching to ordinary samples of $X$ and uses only black-box evaluations of $L$. Their main result is that this sampler is asymptotically optimal in the standard sense of logarithmic efficiency (Asmussen and Glynn 2007, Ch. 6) over a nonparametric class of light- and Weibull-type-tailed distributions and nonconvex losses.

Setting

Write $\mathbb R^d_+=\{x:x\ge0\}$ and $\mathbb R^d_{++}=\{x:x>0\}$ (componentwise), and $\|x\|=\max_i|x_i|$. The random vector $X=(X_1,\dots,X_d)$ has density $f_X$. Its marginal cumulative hazards are $\Lambda_i(x)=-\log P(X_i>x)$, $\Lambda(x)=(\Lambda_1(x_1),\dots,\Lambda_d(x_d))$, and $Y=\Lambda(X)$ is the standardized vector. Let $q_i=\Lambda_i^{\leftarrow}$ be the left-continuous inverse, $q(y)=(q_1(y_1),\dots,q_d(y_d))$, $\hat q(t)=q(t\mathbf 1)/\|q(t\mathbf 1)\|$ and $\Lambda_{\min}(u)=\min_i\Lambda_i(u)$.

The standing assumptions are:

• Assumption 2.1 on the loss: risk sets $\{x\in\operatorname{supp}X: L(x)\ge u\}$ lie in $\mathbb R^d_+$ for large $u$, and $L(nx_n)/n^\rho\to L^*(x)$ for every $x_n\to x$ in $\mathbb R^d_+$, with $\rho>0$ and $L^*>0$ somewhere on $\mathbb R^d_+$.
• Assumption 3.1 on the marginals: each $\Lambda_i$ is continuous, eventually strictly increasing, and regularly varying with index $\alpha_i>0$ ($\Lambda_i(sx)/\Lambda_i(s)\to x^{\alpha_i}$).
• Assumption 3.2 on the dependence: $Y$ has density $p(y)e^{-\varphi(y)}$ with $n^{-1}\varphi(ny_n)\to I(y)$ and $n^{-\varepsilon}\log p(ny_n)\to0$ along every $y_n\to y\ne0$ in $\mathbb R^d_+$.
• Assumption 5.1: each $\Lambda_i$ is eventually convex or concave.
• The limit $q^*=\lim_{t\to\infty}\hat q(t)$ exists.

The sampler (Algorithm 1) fixes a hyper-parameter $l=l(u)$ and maps a sample $x$ to $T(x)=x\,(u/l)^{\kappa(x)}$, with either exponent

$$\kappa^{(1)}(x)=\frac1\rho\frac{\log(1+|x|)}{\|\log(1+|x|)\|_\infty}\qquad\text{or}\qquad \kappa^{(2)}(x)=\frac{\log(1+|x|)}{\log l}.$$

With $J$ the closed-form Jacobian of Table 1 and $Z=T(X)$, the single-sample estimator is

$$\zeta(u)=\frac{J(X)f_X(Z)}{f_X(X)}\,\mathbb I\big(L(Z)\ge u\big),\qquad M_{2,u}=E[\zeta(u)^2].$$

Formalization targets

Goal: Theorem 5.1 (logarithmic efficiency)

Under Assumptions 2.1, 3.1, 3.2, 5.1, existence of $q^*$, $L^*(q^*x)>0$ for some $x\in\mathbb R^d_+$, and any slowly varying $l(u)\to\infty$, for either exponent,

$$M_{2,u}<\infty\ \text{for large }u,\qquad \lim_{u\to\infty}\frac{\log M_{2,u}}{\log p_u^2}=1.$$

The goal fixes neither the exponent, nor the hyper-parameter $l$, nor the loss or the distribution beyond the stated assumptions.

Milestones

The milestones follow the paper's proof chain (Appendix A.3 for $\kappa^{(1)}$, Appendix E for $\kappa^{(2)}$):

1. Proposition 2.1: $\zeta(u)$ is unbiased and $T$ is invertible.
2. Lemma 3.1: the coordinates of $Y$ are standard exponential.
3. Theorem 3.1: $\{Y/t\}$ satisfies a large deviations principle with rate $I$.
4. Lemma 3.2: $I$ is continuous and homogeneous, and $\inf_{y_i>c}I=c$.
5. Lemma A.1: the rare event in standardized coordinates.
6. Theorem 4.1: the tail asymptotic

$$\log p_u=-\Lambda_{\min}(u^{1/\rho})\big[I^*+o(1)\big],\qquad I^*=\inf\{I(y):L^*(q^*y^{1/\alpha})\ge1,\ y\ge0\}.$$

7. Lemmas A.4 and A.5: bounds on $T^{-1}$, and $\psi_u=\Lambda\circ T^{-1}\circ q$ is $o(t(u))$ on compacts.
8. Lemma A.6: $M_{2,u}$ as a Laplace-type functional of $Y_u=Y/t(u)$.
9. Lemma A.7: the density exponent $a_u\ge I+o(1)$.
10. Lemma A.9: the rare set stays a fixed distance from the origin.
11. Display (85): the $\kappa^{(2)}$ bound on $T^{-1}$.

Significance

Theorem 4.1 gives the exponential decay rate of $p_u$ for a broad class of nonconvex losses (piecewise affine and quadratic functions, values of mixed integer programs, neural-network feature maps) under nonparametric, copula-style dependence. Previously such asymptotics were known only for specific losses and distribution families. Theorem 5.1 shows that one simple, model-oblivious transformation attains the best possible exponential rate for the second moment, so the relative error grows more slowly than any power $p_u^{-\varepsilon}$. This supports using the sampler for value-at-risk, conditional value-at-risk and chance-constrained optimization.

The results are proved in the paper's appendices (Appendices A, D.1 and E). None of them has a machine-checked proof. Formalizing them would require regular variation and Potter bounds, a tail large deviations principle in $\mathbb R^d$, and a Varadhan-type integral lemma along a real speed. These are general tools that are missing from Mathlib and are reusable well beyond this paper.

Difficulty

The obvious argument is to bound $M_{2,u}$ by computing the likelihood ratio on the rare set. This fails because the rare set, after standardization, is described only asymptotically: $L_u(x)=u^{-1}L(q(t(u)x))$ converges to $f_{LD}(x)=L^*(q^*x^{1/\alpha})$ only continuously on $\mathbb R^d_{++}$, not uniformly. The exponent of the likelihood ratio involves the density of $Y$ at two different scales ($t(u)p$ and $\psi_u(t(u)p)$) and the hazard rates at points pulled back by $T^{-1}$. A lower bound on it must hold uniformly enough to apply a Varadhan-type lemma with a varying family of functions, while the transformed sample stays inside a region where the asymptotic density assumptions apply. The upper and lower large-deviations bounds also rely on homogeneity of $I$ and $f_{LD}$, which hold only for the heaviest-tailed coordinates of $q^*$.

Formalization scope

Points of $\mathbb R^d$ are Fin d → ℝ with the sup norm, and components are 0-based. $X$ is modelled by its law $\mu$ together with a density $f_X$. $M_{2,u}$ is a lower Lebesgue integral and $p_u=\mu\{L\ge u\}$; both are extended nonnegative reals, so neither $+\infty$ nor $0$ is collapsed to a junk value. Logarithms of probabilities in large-deviations statements are taken in EReal, where $\log0=-\infty$. $I^*$ is an EReal infimum, equal to $+\infty$ over an empty set. Regular variation is the real-variable limit with an eventually positive denominator, and reuses the published definition HeavyTailNV.Tail.IsRegularlyVarying. The Jacobian is Table 1's closed form. Statements that evaluate $q$ at $t(u)p$ take $p\in\mathbb R^d_{++}$.

The following hypotheses are added relative to the printed statements, each disclosed on its item:

• $l(u)\to\infty$ in Theorem 5.1 and Lemma A.7 (the paper states it in §2.2 and uses it in Lemma A.5 and Appendix D.1).
• "$L^*(q^*x)$ not identically zero" is read as positivity somewhere.
• Measurability of $L$.
• $0<l\le u$, and $l>1$ for $\kappa^{(2)}$, together with an IS support condition in Proposition 2.1 and Lemma A.6. Proposition 2.1 is false as printed without them.
• $p(ny_n)>0$ eventually inside (13).
• $d\ge1$ where junk values at $d=0$ would otherwise matter.
• In Theorem 4.1, continuity of the rate $I$ on $\mathbb R^d_+\setminus\{0\}$, which the theorem's hypothesis "the tail LDP in Theorem 3.1" carries through Lemma 3.2(a) and which the proof uses.

The following printed statements are corrected:

• Lemma A.6 is stated without its spurious factor $t(u)^{2d}$.
• Lemma A.9 is restricted to points with $q(t(u)p)\in\operatorname{supp}X$. As printed it fails when $L$ is large off the support.
• Lemma 3.2's "$I(0)=0$" becomes a limit at $0$, since (13) does not determine $I(0)$.
• Theorem 3.1 is stated with real speed $t$, which implies the printed sequence form.

Lemmas A.8 and A.10 and Corollary A.1 are not posed. Their uniform claims over all of $\mathbb R^d_+$ depend on pointwise versions of the hazard rates and on the values of $L$ off the support and off $\mathbb R^d_+$, which the hypotheses do not control; Corollary A.1 fails as printed when $X$ has negative components.

A trivializing formalization is ruled out explicitly. The goal is the limit (23) for the estimator $\zeta(u)$ of §5.2 with Table 1's Jacobian, for every admissible $l$ and both exponents. It is not the bound $M_{2,u}\ge p_u^2$, not a statement about an unspecified IS density, and not a statement for one fixed $l$. The finiteness conjunct prevents Lean's $\log 0=0$ convention from satisfying it.

Contributions are welcome at every level. The general tools (Potter bounds, the tail LDP, a Varadhan lemma for continuously converging functions) are useful as separate developments.

Selected references

• A. Deo, K. Murthy, Achieving Efficiency in Black-Box Simulation of Distribution Tails with Self-Structuring Importance Samplers, Operations Research, 2025; preprint arXiv:2102.07060v3, 2023. https://arxiv.org/abs/2102.07060
• S. Asmussen, P. W. Glynn, Stochastic Simulation: Algorithms and Analysis, Springer, 2007. https://doi.org/10.1007/978-0-387-69033-9
• L. de Haan, A. Ferreira, Extreme Value Theory: An Introduction, Springer, 2006. https://doi.org/10.1007/0-387-34471-3
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4

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