Stochastic Systems

Motivation

A two-stage stochastic linear program chooses a first-stage decision before uncertain coefficients are known and then uses recourse variables to repair the decision after the data are observed. The resulting expected recourse cost is central to existence, stability, and numerical methods: if it can be infinite, an apparently feasible model may still have no meaningful expected objective; if it is differentiable with a continuous gradient, deterministic smooth optimization methods become available on the feasible first-stage domain. Chapter III of Peter Kall's Stochastic Linear Programming develops these properties for fixed recourse. This mission packages two complete results from that development: Theorem 12 on continuous differentiability and Theorem 15 on the exact finiteness criterion under complete recourse.

Theorem 12 is the goal. Theorem 15 is retained as a separate source theorem from the same expected-recourse setting, not as a lemma asserted to prove Theorem 12. Keeping both statements makes the distinction between the general feasible-domain regime and the stronger complete-recourse regime explicit.

Setting

Fix a deterministic matrix (W\in\mathbb R^{m\times p}). A random data point is a triple (d=(A,b,q)), where (A\in\mathbb R^{m\times n}), (b\in\mathbb R^m), and (q\in\mathbb R^p), with arbitrary joint probability law μ. For a first-stage vector (x\in\mathbb R^n), the pointwise recourse value is the extended-real linear-program value

$$Q(x,d)=\inf\{q^\top y:Wy=b-Ax,\ y\ge 0\}.$$

The extended-real convention records an infeasible recourse problem as (+\infty) and an unbounded-below problem as (-\infty). The recourse domain is

$$K=\{x:Q(x,d)<+\infty\text{ for μ-almost every }d\}.$$

Thus (K) requires almost-sure feasibility but does not assume complete recourse and does not exclude a value of (-\infty). The signed extended expectation follows Kall's equation III.(8): it is the integral of the positive part minus the integral of the negative part. A separate real-valued expected-recourse adapter integrates (Q(x,d).\mathrm{toReal}); the target uses that adapter only after explicitly concluding almost-sure finiteness and integrability, so totalization at infinities does not hide a divergent cost.

The shared moment condition is exactly the disjunction from Theorem 10 and Corollary 11: all coordinates of (A,b,q) are square integrable; or (q) is almost surely constant while (A,b) are integrable; or (A,b) are almost surely constant while (q) is integrable; or all three random coefficient ranges are bounded. No independence or finite-support hypothesis is imposed.

Finally, (W) has complete recourse when every right-hand side (z\in\mathbb R^m) admits a nonnegative (y) satisfying (Wy=z). This is stronger than membership of one decision in (K), but it does not by itself prevent an unbounded-below recourse cost.

Formalization targets

Theorem 12: continuous gradient of expected fixed recourse

Assume one of the four moment alternatives, assume the signed expected recourse is strictly above (-\infty) at every (x\in K), and assume the joint law μ is absolutely continuous with respect to Lebesgue measure on the full finite-dimensional coefficient space. Then the pointwise recourse value is finite almost everywhere and its real projection is integrable for each (x\in K). Moreover, there is a continuous field of linear functionals (g(x)) such that

$$g(x)=D Q_\mu(x)\quad\text{within }K,$$

including boundary points of (K). In Lean this is stated by ContinuousOn g K together with HasFDerivWithinAt for the expected-recourse function at every point of (K). It is not weakened to differentiability only on the interior, and it does not add complete recourse.

Theorem 15: finiteness iff almost-sure dual feasibility

Under complete recourse and one of the same four moment alternatives, for an arbitrary fixed (x\in\mathbb R^n),

$$\mathbb E[Q(x,d)]\in\mathbb R \quad\Longleftrightarrow\quad \{z\in\mathbb R^m:W^\top z\le q(d)\}\ne\varnothing \text{ almost surely}.$$

The left side means that the signed extended expectation equals a real number, not merely that a totalized real integral returns a value. The right side requires feasibility of the dual inequalities almost surely; it does not require attainment or optimality. This full equivalence is the mission's supporting milestone.

Significance

Theorem 12 supplies a smooth expected objective on the entire source feasible domain under an absolutely continuous data law. That conclusion is stronger than convexity or local Lipschitz continuity: it provides a continuously varying derivative while retaining boundary points and the random dependence of all coefficient blocks. The explicit finiteness and integrability clauses make clear when the real expected objective faithfully represents the extended-real model.

Theorem 15 separates two different well-posedness questions. Complete recourse guarantees primal feasibility for every residual, while almost-sure feasibility of the dual inequalities is exactly what prevents the expected value from escaping the real line under the stated moment conditions. Omitting either direction would lose the source's characterization.

Both results are established in the 1976 book; the staged Lean theorem declarations contain proof placeholders. Completing them would give machine-checked versions of the source statements using reusable definitions for equality-constrained nonnegative linear-program values, pointwise recourse, expected recourse, complete recourse, the signed expectation, and the four moment regimes.

Difficulty

For differentiability, a pointwise optimal solution or dual vector need not vary continuously when the active basis changes. Absolute continuity removes coefficient configurations lying on relevant exceptional hyperplanes only after a measure-theoretic argument, and the conclusion must hold relative to a possibly closed feasible domain rather than only on an open set. One must also prove finiteness and integrability before using the real-valued expectation; simply differentiating the totalized toReal expression would not establish the source theorem.

For finiteness, complete recourse handles feasibility but not unbounded negative cost. The dual system is random through (q), and the equivalence concerns almost-sure existence of a dual-feasible vector together with a signed extended expectation. Assuming dual feasibility or integrability of the recourse value at the outset would make one direction circular.

Formalization scope

All coefficient spaces use finite Fin indices and real scalars. The law is an arbitrary probability measure on the joint product (A,b,q). The density premise for Theorem 12 is ambient absolute continuity with respect to the product Lebesgue volume; it is not a density on an unspecified lower-dimensional support. Consequently, some constant-coordinate moment branches may be incompatible with that density premise, matching the reviewed ambient interpretation rather than silently changing the measure space.

The feasible domain uses (Q(x,d)<+\infty) almost surely and includes its boundary. The signed expectation preserves positive and negative infinities. Theorem 12 assumes it is above (-\infty) on (K) and concludes the conditions needed for the separate real integral. Theorem 15 adds complete recourse but no density, independence, finite support, pre-assumed dual feasibility, or pre-assumed value integrability. Its decision (x) remains arbitrary.

The mission reuses the platform definitions of LPValue, PointwiseRecourse, ExpectedRecourse, and CompleteRecourse. The book-local Kall1976 namespace contains only the expression-essential data type, feasible domain, signed expectation, moment disjunction, and the two reviewed theorem statements. Contributions may add analytical, measure-theoretic, or linear-programming lemmas needed for proofs, but may not replace the signed expectation by a totalized real value, restrict Theorem 12 to the interior, or weaken Theorem 15 to one implication.

Selected references

• Peter Kall, Stochastic Linear Programming, Springer, 1976, Chapter III: equations (4)-(5), printed p. 41 / PDF47; equation (8), printed p. 44 / PDF50; Theorem 10 and Corollary 11, printed pp. 46-48 / PDF52-54; Theorem 12, printed p. 48 / PDF54; complete recourse, printed p. 51 / PDF57; Theorem 15, printed p. 54 / PDF60. DOI.

Motivation

Same-day and on-demand delivery services (groceries, meals, parcels) must decide how to assign incoming orders to drivers. One option is flexible dispatching: any driver may serve any order in the service region. Another is districting: the region is cut into $m$ districts, one per driver, and each driver serves only the orders from their own district. Districting is easier to run, since drivers learn their territory, routes are short and responsibility is clear, but it gives up the flexibility of pooling. A basic question is when a districting policy loses nothing against the best flexible policy.

Carlsson, Liu, Salari and Yu (Operations Research 72(1), 2024; accepted manuscript SSRN 3915544) answer this in heavy traffic, the regime where the drivers are almost always busy. Their comparison point is the policy $\pi^*$ of Bertsimas and van Ryzin (1993), whose expected delivery time has an explicit leading-order formula in heavy traffic. Their Theorem 6 gives two integral conditions on a partition under which districting matches $\pi^*$ to first order.

Timeline.

• 1959. Beardwood, Halton and Hammersley: the shortest tour through $n$ random points with density $f$ has length $\sim\beta\sqrt n\iint\sqrt{f}$.
• 1991–1993. Bertsimas and van Ryzin: the dynamic traveling repairman and its capacitated, multi-vehicle versions, with heavy-traffic lower bounds and a policy $\pi^*$ that attains the leading-order formula (Theorem 3 of the paper, p. 8).
• 2024. Carlsson, Liu, Salari and Yu: a partition that is equitable for two measures gives a districting policy that is asymptotically optimal in heavy traffic (Theorem 6), together with algorithms to compute such partitions.

Setting

A service region $\mathscr R\subseteq\mathbb R^2$ is compact and convex and contains a depot $x_0$. Orders arrive at rate $\lambda$ at random locations drawn from a demand density $f\ge0$ on $\mathscr R$, Lipschitz, with $\iint_{\mathscr R}f(x)\,dx=1$. There are $m\ge1$ identical vehicles with speed $v>0$ and capacity $q\in\mathbb N_+$, and each order needs an on-site service of mean $\bar s\ge0$. The constant $\beta>0$ comes from the Beardwood–Halton–Hammersley theorem.

The workload factor of the fleet is

$$\rho+\frac{2\lambda\iint_{\mathscr R}\|x-x_0\|f(x)\,dx}{mvq},\qquad \rho=\frac{\lambda\bar s}{m},$$

the long-run fraction of time a vehicle spends in on-site service and in travel to and from the depot. The system is stable when it is below $1$, and heavy traffic is the limit in which it tends to $1$ from below, with only $\lambda$ varying.

Theorem 3 of the paper (Bertsimas and van Ryzin) states that $\pi^*$ achieves

$$T(\pi^*)\sim\frac{\beta^2\lambda(1-\frac1q)^2\left[\iint_{\mathscr R}\sqrt{f(x)}\,dx\right]^2}{2m^2v^2\left(1-\rho-\frac{2\lambda\iint_{\mathscr R}\|x-x_0\|f(x)\,dx}{mvq}\right)^2}$$

in heavy traffic. A policy $\pi$ is asymptotically optimal if $T(\pi)/T(\pi^*)\to1$ in heavy traffic.

A region partitioning policy fixes a partition $\{\mathscr R_1,\dots,\mathscr R_m\}$ of $\mathscr R$ and dedicates one vehicle to each $\mathscr R_i$. District $i$ then receives orders at rate $\lambda_i=\lambda\iint_{\mathscr R_i}f$ with conditional density $f_i=f/\iint_{\mathscr R_i}f$. Its vehicle runs the single-vehicle version of $\pi^*$, so Theorem 3 with $m=1$ gives its delivery time $T_i$. The policy's overall expected delivery time is $T=\sum_i\mathbb P(x\in\mathscr R_i)\,T_i$.

Formalization targets

Goal: Theorem 6 (p. 11)

If for every $i$

$$\iint_{\mathscr R_i}\sqrt{f(x)}\,dx=\frac1m\iint_{\mathscr R}\sqrt{f(x)}\,dx,\qquad \iint_{\mathscr R_i}(\bar svq+2\|x-x_0\|)f(x)\,dx=\frac1m\iint_{\mathscr R}(\bar svq+2\|x-x_0\|)f(x)\,dx,$$

and $T(\pi^*)$ and every $T_i$ obey Theorem 3, then

$$\frac{\sum_{i=1}^m\mathbb P(x\in\mathscr R_i)\,T_i}{T(\pi^*)}\longrightarrow1\quad\text{in heavy traffic.}$$

Milestones

These are the displayed steps of the printed proofs of Theorems 5 and 6 (pp. ec5–ec6):

1. Normalization identities. $\iint_{\mathscr R_i}\sqrt{f_i}=\iint_{\mathscr R_i}\sqrt f/\sqrt{\iint_{\mathscr R_i}f}$ and $\iint_{\mathscr R_i}\|x-x_0\|f_i=\iint_{\mathscr R_i}\|x-x_0\|f/\iint_{\mathscr R_i}f$.
2. Per-district workload identity. Under the second condition, district $i$'s workload factor $\rho_i+2\lambda_i\iint_{\mathscr R_i}\|x-x_0\|f_i/vq$ equals the fleet's for every $\lambda$. The two heavy-traffic limits therefore coincide.
3. Leading-term chain. Under both conditions, the Theorem 3 term of district $i$ (one vehicle, data $\lambda_i,f_i$) equals the fleet's term.
4. Per-district ratio. $T_i/T(\pi^*)\to1$ for every $i$.
5. Total expectation. If $T_i/T(\pi^*)\to1$ for every $i$, then $\sum_i\mathbb P(x\in\mathscr R_i)T_i/T(\pi^*)\to1$.

Significance

The result. Theorem 6 turns a question about stochastic, dynamic routing into a static geometric condition: find a partition that gives every district a $1/m$ share of two measures, $\mu_1=\iint\sqrt f$ (local tour length) and $\mu_2=\iint(\bar svq+2\|x-x_0\|)f$ (service plus round-trip load). The rest of the paper builds on this. It computes such partitions with convex pieces, bounds the loss when the shares are only approximately equal (Proposition 3, the subject of the companion mission), and tests the policy in simulation. The theorem also shows that the arrival rates need not be equal across districts. What has to be equal is the combined load.

Formalizing it. The result has a short pen-and-paper proof, and no machine-checked version exists. The mission records exactly which part of the argument is real analysis (integral identities over a partition, and how heavy-traffic limits pass to ratios) and which part is borrowed from Bertsimas and van Ryzin. It also gives the platform a first districting and continuous-approximation development. Its definitions (workload factor, Theorem 3's leading term, heavy-traffic filter, conditional subregion data) can be reused for other results in the continuous-approximation literature.

Difficulty

The algebra in the proof is simple once Theorem 3 is applied to each district with its own rate $\lambda_i$, density $f_i$ and one vehicle. The obstacle is in the limits. Theorem 3 for district $i$ holds along that district's heavy-traffic limit, where its own workload factor tends to $1$, while asymptotic optimality is measured along the fleet's limit. These are different limits unless the second equitable condition makes the two workload factors equal as functions of $\lambda$. A tempting shortcut is to state the district hypothesis directly with the fleet's quantities, such as $(1/m)\iint_{\mathscr R}\sqrt f$ and the fleet's workload factor. That assumes milestones 2 and 3 and empties the theorem. Division also needs care: $f_i$ and the ratios $T_i/T(\pi^*)$ have denominators that must be shown nonzero from the hypotheses, not assumed.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2) with the Euclidean norm, and integrals are Bochner set integrals for Lebesgue measure. The definition file CarlssonPartition.Equitable.Setting contains:

• the instance $(\mathscr R,x_0,f,m,v,q,\bar s,\beta)$;
• the standing assumptions listed in Setting;
• the workload factor and Theorem 3's leading term, both generic in (vehicle count, rate, region, density);
• $\mathbb P(x\in S)$, $\lambda_i$ and $f_i$;
• partitions;
• the heavy-traffic filter.

Conventions:

• The model is not formalized. The stochastic dynamic routing model (renewal arrivals, TSP batching, queues of tours) has no Mathlib substrate. The paper itself uses it only through Theorem 3 of Bertsimas and van Ryzin. So $T(\pi^*)$ and the $T_i$ are arbitrary real functions of $\lambda$, and Theorem 3 is a hypothesis on them: for the fleet, and for each district with $m=1$ along the district's own limit.
• Heavy traffic is Filter.comap (fun λ => workload) (𝓝[<] 1): the arrival rates along which the workload factor tends to $1$ from below. Every "$\sim$" is a ratio tending to $1$.
• Partitions are read up to null sets: null-measurable pieces, pairwise almost-everywhere disjoint, with union $\mathscr R$.
• Added hypothesis $q\ge2$. At $q=1$ the factor $(1-1/q)^2$ makes Theorem 3's leading term zero, so its ratio hypotheses could not hold and the theorem would be vacuous.
• No positivity of $\iint_{\mathscr R_i}f$ is assumed in the goal, because it follows from the first equitable condition. The milestones that manipulate $f_i$ state it explicitly.
• The Lipschitz condition is kept as a standing assumption of the paper, although only continuity is needed.

Two formalizations would make the goal trivial and are ruled out: defining $T(\pi^*)$ or $T_i$ as the leading-order formula, and writing the district hypothesis with fleet quantities or the fleet's filter. The verification development checks that the heavy-traffic filter is not the bottom filter whenever $\bar s>0$.

Welcome contributions: proofs of the milestones; a general lemma on averaging ratio limits under a probability vector; and finite additivity of set integrals over a.e.-disjoint partitions in the form used here.

Selected references

• J. G. Carlsson, S. Liu, N. Salari, H. Yu, Provably Good Region Partitioning for On-Time Last-Mile Delivery, Operations Research 72(1):91–109, 2024. https://doi.org/10.1287/opre.2021.0588 (accepted manuscript: https://ssrn.com/abstract=3915544)
• D. J. Bertsimas, G. van Ryzin, Stochastic and Dynamic Vehicle Routing in the Euclidean Plane with Multiple Capacitated Vehicles, Operations Research 41(1):60–76, 1993. https://doi.org/10.1287/opre.41.1.60
• D. J. Bertsimas, G. van Ryzin, A Stochastic and Dynamic Vehicle Routing Problem in the Euclidean Plane, Operations Research 39(4):601–615, 1991. https://doi.org/10.1287/opre.39.4.601
• J. Beardwood, J. H. Halton, J. M. Hammersley, The Shortest Path Through Many Points, Mathematical Proceedings of the Cambridge Philosophical Society 55(4):299–327, 1959. https://doi.org/10.1017/S0305004100034095

Why spatial pricing needs a dynamic control

A ride-hailing firm chooses prices while drivers move through a city. A trip from one region uses a driver immediately and returns that driver at another region only after a travel delay. Prices affect which trips are requested, but the actual requests fluctuate. A plan that ignores these fluctuations can run out of available drivers at a busy origin even when its average flows fit the fleet. Chen, Lei, and Jasin study how closely a feasible pricing control can approach a deterministic revenue benchmark in this setting (accepted manuscript, published article).

Their Arc Balancing Control (ABC) responds to realized trips. It groups each directed arc's periods into batches and adjusts the next batch's demand rates according to the previous batch's cumulative surplus or deficit. The paper proves a loss rate for ABC that is smaller than the rate established there for its Static Price Control. The target here is the paper's Theorem 3, with the model and parameters of its authors' accepted manuscript. Its e-companion contains the paper's proofs.

The pricing network and benchmark

The network has $N\ge1$ regions and a horizon of $T\ge1$ periods. Every ordered pair $i\to j$, including $i=j$, is an arc. At most one customer can request an arc's trip in a period. A served trip takes one server from region $i$ for $\tau_{ij}\ge1$ periods, then returns it at $j$. Region $i$ starts with $C_i\ge N$ servers. A control must respect the available server count before it serves each period's realized requests.

The decision is a demand rate $\lambda_{t,ij}\in[0,1]$ rather than its inverse price. The expected revenue from that arc and period is $r_{t,ij}(\lambda_{t,ij})$. The revenue functions are nonnegative and strongly concave, vanish at zero, and have bounded first and second derivatives. The bound on those derivatives is $\Psi_3>0$. The paper's price-side assumptions imply these rate-side conditions; the Lean model states the conditions directly.

The deterministic convex program $\mathrm{DCP}(\zeta)$ chooses rates to maximize the sum of expected revenues. Its flow constraints replace realized trips with their rates, while its cushion requires $\zeta\le\lambda_{t,ij}\le1-\zeta$. Write $J(\zeta)$ for its value and $\lambda^{\zeta,D}$ for an optimal schedule. In the $n$th system, the fleet, horizon, and travel times are multiplied by $n$; each original period's revenue curve is used for $n$ consecutive scaled periods. Thus $T^n=nT$ and $\underline\tau^n=n\min_{i,j}\tau_{ij}$. For a control $\pi$, the per-period benchmark loss is

$$L^\pi(n)=\frac{J(n,0)-\mathbb E^\pi[R^\pi(n)]}{T^n}.$$

ABC uses $\lambda^{n,\zeta,D}$ as its baseline. Its batches have a target sum $b$ of the baseline variance weights $\lambda^{n,\zeta,D}_{t,ij}(1-\lambda^{n,\zeta,D}_{t,ij})$. Within a batch, the control subtracts a weighted share of the preceding batch's realized surplus $\bar\delta^k_{ij}=\sum_{t\in\mathcal T^k_{ij}}(D_{t,ij}-\lambda^{ABC}_{t,ij})$. A rate is projected to $[0,1]$, and an origin with too few available servers is turned off. The finite path law uses the rates posted along each path.

Formalization targets

The principal target is Theorem 3. With $b_n=(\underline\tau^n)^{2/3}$ and

$$\epsilon_n=(\underline\tau^n)^{-1}\left(1+16\sqrt{2(b_n+1)\log T^n}\right),\qquad \zeta_n=2\epsilon_n,$$

there is a constant $\widetilde\Psi_2$, independent of $n$, for which every integer $n\ge1$ satisfies

$$L^{ABC}(n)\le\widetilde\Psi_2\frac{\log(1+n)^{3/2}}{n^{2/3}}.$$

The milestone list follows the source results used in the analysis: Lemma 2 bounds the deterministic cost of a small cushion and gives feasibility; Lemma EC.1 bounds a maximal cumulative Bernoulli deviation; and the two parts of Lemma 4 characterize ABC on a batchwise good event $\mathcal A$ and bound that event's probability. Theorem 3 fixes the complete control and these exact parameters; its constant may depend on the fixed network instance and $\Psi_3$.

What the result establishes

The theorem gives a finite-$n$ loss bound relative to $J(n,0)$, with the stated $n^{-2/3}$ rate and logarithmic factor. In the paper, Lemma 1 shows that $J(n,0)$ bounds the optimal admissible policy's revenue. Theorem 3 therefore bounds ABC's distance from a benchmark that is at least as high as the unknown stochastic optimum. The paper compares this rate with its $n^{-1/2}$ result for Static Price Control and explains the resulting value of adapting prices to realized demand (Theorems 2–3).

The published mathematical result and its manuscript proof are known; the statements in this mission are Lean targets with proofs still to be formalized. A complete development would also make reusable definitions for finite controlled path laws, delayed network flow balance, and cushioned deterministic relaxations. The batch and feedback definitions isolate the paper-specific control from that general infrastructure.

Main difficulty

The deterministic program controls expected flows, while ABC must keep every realized path feasible. An unadjusted baseline can accumulate demand fluctuations over the whole horizon; bounding those fluctuations alone does not describe the effect of ABC's feedback. The control's posted rate in a period depends on earlier realized requests, which changes the distribution of later requests. The manuscript's proof of Lemma 4 bounds a variance proxy from its deterministic baseline when treating the adaptive posted rates; that step needs separate justification in a formal proof. Lemma EC.1, as posed here, covers deterministic Bernoulli rates and does not by itself close that gap. The finite-horizon claim, including small scaling factors for which the cushioned DCP may be infeasible, must still be established.

Formalization scope

Lean represents regions by Fin N, periods by natural numbers $1,\ldots,T$, travel times and server counts by naturals, demand by Boolean paths, and revenue and rates by real numbers. The $\mathrm{DCP}(n,\zeta)$ program uses a real supremum; statements involving positive $\zeta$ assert feasibility, and $J(n,0)$ has the zero schedule as a feasible point. ABC's path law is the product of sequential Bernoulli factors at its own posted rates. Its rate history is built by structural recursion, and the event $\mathcal A$ checks every nonempty batch and all its partial sums.

The accepted manuscript leaves the final incomplete batch unspecified, so the last short batch is merged with its predecessor. The printed ABC box turns an origin off at $C_{t,i}\le N$, while Lemma 4 and its base case require service when $C_{t,i}=N$; the formal control uses $C_{t,i}\ge N$. If the cushioned DCP has no optimum, the baseline is zero. The sample-path part of Lemma 4 adds the hypothesis $\underline\tau\le T$, which the manuscript does not print. Without it the part is false: when the horizon is shorter than every travel time, no server returns, and a single realized trip can leave a region below $N$ servers on the good event. These conventions are recorded with the source discrepancies in the moderation notes. The rate model drops assumptions A1 and A3(i), which concern only the price parametrization, and writes A2, A3(ii), $r\ge0$, and $r(0)=0$ directly. It assumes a twice continuously differentiable extension of revenue to $\mathbb R$. No statement substitutes expected demand for the realized batch surplus or lets the theorem's parameters depend on $n$ by existential choice. Contributions toward the source milestones, the adaptive concentration step, and the reusable model definitions are all within scope.

Selected references

• Q. Chen, Y. Lei, and S. Jasin, Real-Time Spatial-Intertemporal Pricing and Relocation in a Ride-Hailing Network: Near Optimal Heuristics and The Value of Dynamic Pricing, authors' accepted manuscript, LBS Research Online eprint 2845, pp. 7–25 and ec2–ec6; published as Real-Time Spatial–Intertemporal Pricing and Relocation in a Ride-Hailing Network: Near-Optimal Policies and the Value of Dynamic Pricing, Operations Research 72(5):2097–2118, 2024. Manuscript, DOI.

Motivation

Many outpatient clinics offer two ways in: an appointment booked online, and walk-in hours on the day. Some patients have no choice (acute cases arrive as walk-ins), but many can pick either channel, and they pick the one that costs them less: a long appointment delay pushes them into the walk-in room, a crowded walk-in room pushes them to book or to give up. A clinic deciding how to split its daily capacity between the two channels therefore faces a game, not a forecasting problem.

Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science 2023, doi:10.1287/mnsc.2023.4676) model this game and compare three operational levers: the capacity split, how much delay information the booking system reveals, and triage, that is, reserving walk-in hours for acute patients only (as some practices do, e.g. Centre Pediatrics 2021). This mission formalizes the triage comparison, Proposition 6 of the paper: closing walk-in hours to patients who could book pays off exactly when lost demand is cheap relative to overtime.

Setting

Patients. Exogenous walk-ins arrive at rate $\lambda_E$ and are always served on the day, possibly in overtime. Strategic patients arrive as a Poisson process of rate $\lambda>0$. A served patient gains $R>0$.

Capacity. The clinic has total capacity $\mu>0$ per day, split into appointment hours $\mu_S$ and walk-in hours $\mu_W=\mu-\mu_S$, with $\mu_S\in[0,\mu)$.

The appointment queue. Appointments form a single-server queue with deterministic service time $1/\mu_S$. In the observable setting a patient sees the queue: with $k$ patients waiting, the delay is $(k+\tilde u)/\mu_S$, $\tilde u$ uniform on $[0,1]$. A patient schedules when this delay is at most a threshold $\delta$, and scheduling at delay $d$ is worth $u^2_S(d)=R-C_D d$. The fraction of strategic patients who do not schedule is the blocking probability $\pi(\delta,\mu_S)$ of this M/D/1/K−1+p queue, where $K=\lceil\delta\mu_S\rceil$ and $p=\delta\mu_S+1-K$. With $\rho=\lambda/\mu_S$ it has the closed form $\pi(\delta,\mu_S)=1-1/(q_0+\rho)$, where $q_0$ is built from the Poisson weights $\alpha_j=\rho^je^{-\rho}/j!$ by the Brun–Garcia recursion (Online Appendix C, (26)–(27), Corollary C.1). With no appointment hours, $\pi(\delta,0)=1$.

Walking in and balking. A patient who does not schedule walks in with probability proportional to $p_W$ or balks with probability proportional to $p_B$. Walking in is worth $u^2_W(p_W)=R-C_W\,w\big((\lambda_E+p_W\lambda)/\mu_W\big)$, with $w$ convex, strictly increasing and $w(0)=0$; balking is worth $0$. An observable equilibrium $(\delta,p_W,p_B)$ is a solution of conditions (6)–(10): the threshold $\delta$ makes scheduling at least as good as the walk-in/balk mixture up to $\delta$ and worse beyond it, $p_W+p_B=\pi(\delta,\mu_S)$, and patients walk in (balk) only if walking in is worth at least (at most) zero.

Costs. The provider pays $C_L$ per balking patient and $C_O\,o(\cdot)$ for overtime, with $o$ convex and strictly increasing. In the strategic model patients choose freely, and the cost at allocation $\mu_S$ and equilibrium $(\delta,p_W,p_B)$ is

$$Z^s=C_L\,p_B\lambda+C_O\,o\Big(\frac{p_W\lambda+\lambda_E}{\mu_W}\Big). \qquad\text{(Ob.P)}$$

In the triage model strategic patients may only schedule or balk, so they behave with threshold $R/C_D$ and

$$Z^t=C_L\,\pi(R/C_D,\mu_S)\,\lambda+C_O\,o\Big(\frac{\lambda_E}{\mu_W}\Big). \qquad\text{(T.Ob.P)}$$

Let $\underline\mu_W$ solve $R-C_W\,w(\lambda_E/\underline\mu_W)=0$ (15): below these walk-in hours the exogenous walk-ins alone make walking in worthless.

Formalization targets

Goal: Proposition 6

Suppose $\mu>\underline\mu_W$ and set

$$\underline\alpha=\frac{o'(\lambda_E/\mu)}{\mu},\qquad \overline\alpha=\frac{o'(\lambda_E/\underline\mu_W)}{\underline\mu_W}\max\Big\{\frac{\lambda_E}{\lambda\,\pi(R/C_D,\mu-\underline\mu_W)},1\Big\}.$$

Then

$$\frac{C_L}{C_O}\le\underline\alpha\ \Longrightarrow\ \inf Z^t\le\inf Z^s,\qquad \frac{C_L}{C_O}\ge\overline\alpha\ \Longrightarrow\ \inf Z^s\le\inf Z^t,$$

where the infima are over allocations $\mu_S\in[0,\mu)$ and, on the strategic side, over the equilibria at each allocation. The Lean statement says this without infima: every strategic configuration is matched by a triage allocation that costs no more, and every triage allocation is matched by a strategic allocation at which an equilibrium exists and every equilibrium costs no more.

Milestones

1. Proposition C.2 ($\mu_S$-part): $\mu_S\mapsto\pi(\delta,\mu_S)$ is continuous and strictly decreasing on $(0,\infty)$.
2. Proposition 1 (observable setting): an observable equilibrium exists at every allocation.
3. Proposition 2 (1): if $\mu_W\le\underline\mu_W$, every equilibrium is schedule-and-balk, $p_W=0$, $\delta=R/C_D$, $p_B=\pi(R/C_D,\mu_S)$.
4. From the proof of part 1: $\lambda\,(1-\pi(\delta,\mu_S))\le\lambda\,(1-\pi(R/C_D,\mu_S))$ at every equilibrium.
5. From the proof of part 2: if nobody balks, $(\lambda p_W+\lambda_E)/\mu_W\le\lambda_E/\underline\mu_W$.
6. From the proof of part 2: if patients mix between walking in and balking, $(\lambda p_W+\lambda_E)/\mu_W=\lambda_E/\underline\mu_W$.

Significance

Proposition 6 turns a qualitative trade-off into two explicit thresholds on the ratio of the lost-demand cost to the overtime cost. Free choice reduces balking but lets strategic patients crowd the walk-in hours; triage removes that crowding at the price of more balking. The thresholds $\underline\alpha$ and $\overline\alpha$ depend only on the overtime function, the capacity and the blocking probability, so a clinic can evaluate them from its own data. The paper also shows (Remark 4, Appendix D.8) that the same insight holds in the unobservable setting, with capacity playing an additional role; that variant is not part of this mission.

The result is proved in the paper (Online Appendix E.3, pp. 35–37) and has no machine-checked proof. The formalization adds three things. It fixes the equilibrium concept precisely, including the mixture weights and the endpoint conventions. It states the comparison of optimal costs without presupposing that the optima are attained; the paper's proof begins "denote the optimal capacity allocations" without proving existence. And it ties the blocking probability to the paper's closed form, so the monotonicity in $\mu_S$ that the proof invokes becomes a statement about an explicit function rather than about a queue described in words.

Difficulty

The comparison itself is a chain of convexity inequalities at a single allocation. The hard part is the blocking probability. The paper proves that $\pi(\delta,\mu_S)$ decreases in $\mu_S$ by a sample-path argument on the queue, but a formal development has only the closed form, in which $K=\lceil\delta\mu_S\rceil$ jumps at every $\mu_S$ where $\delta\mu_S$ is an integer, $p$ jumps from $1$ to $0$ there, and $\rho=\lambda/\mu_S$ moves continuously. Monotonicity and continuity must be shown across these seams, through alternating sums whose terms cancel heavily. The obvious route, differentiating the closed form for fixed $K$, does not give the sign without a further structural argument on the coefficients $a_j$.

Existence of an equilibrium (milestone 2) is an intermediate-value argument in $\delta$, which in turn needs continuity of $\pi$ in $\delta$ and positivity of $\pi$.

Formalization scope

Everything lives in the namespace OutpatientWalkIn.Triage. The definition Queue contains the closed-form blocking probability blockProb lam δ μS; the definition Setting contains the model, the standing assumptions, the utilities, the equilibrium IsObsEq, the costs obsCost and triageCost, and the thresholds alphaLow, alphaHigh.

Conventions:

• Standing assumptions, hypotheses of every theorem: $\lambda>0$, $\lambda_E\ge0$, $R,C_D,C_W>0$, $C_L,C_O\ge0$, $\mu>0$; $w$ convex and strictly increasing on $[0,\infty)$ with $w(0)=0$ (Assumption 1); $o$ convex and strictly increasing on $[0,\infty)$ (Assumption 2).
• Allocations range over $\mu_S\in[0,\mu)$ on both sides, so that $\mu_W>0$; the paper's $\mu_S=\mu$ leaves the exogenous walk-ins with no walk-in hours.
• $\pi(\delta,0)=1$; the observable setting is defined directly (the paper's $C_G=0$).
• The equilibrium carries the guard $p_W+p_B>0$, which by (8) is $\pi(\delta,\mu_S)>0$ and excludes no equilibrium of the paper.
• Added hypotheses of the goal: $C_O>0$, $\lambda_E>0$, $\underline\mu_W>0$ given by (15), and differentiability of $o$ at $\lambda_E/\mu$ and $\lambda_E/\underline\mu_W$ (where $o'$ is evaluated). Without them Lean's $C_L/0=0$ and the zero derivative of a non-differentiable function would make $\underline\alpha=0$ and turn part 1 into a different claim.
• "Costs less" is "costs no more" (p. 26).

A formalization that compares the two models at one fixed allocation only, that lets the prover choose a cheap equilibrium when several might exist, or that replaces $\pi$ by an arbitrary decreasing function, is not the paper's theorem; the statements here rule these out.

Contributions welcome: properties of the closed-form $\pi$ (positivity, $\pi\le1$, monotonicity and continuity in both arguments), the existence of equilibria, and the convexity estimates of the final comparison. The queue file is reusable for any M/D/1/K model with partial joining.

Selected references

• N. Liu, W. van Jaarsveld, S. Wang, G. Xiao, Managing Outpatient Service with Strategic Walk-ins, SSRN 3558209 (version of 2022-07-05); Management Science, 2023. https://ssrn.com/abstract=3558209, https://doi.org/10.1287/mnsc.2023.4676
• O. Brun, J.-M. Garcia, Analytical solution of finite capacity M/D/1 queues, Journal of Applied Probability 37(4), 2000 (the source of the $a_j$ recursion, cited in the paper's Online Appendix C).
• P. Naor, The regulation of queue size by levying tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200

Motivation

In large server farms and cloud platforms, not every server can process every task. Data locality, licences, hardware and security rules restrict each task type to a subset of servers. Such compatibility constraints are modelled by a bipartite compatibility graph between task types (dispatchers) and servers. Classical mean-field results for load balancing, such as Mitzenmacher's analysis of the power of $d$ choices (Mitzenmacher 2001) and Vvedenskaya, Dobrushin and Karpelevich's supermarket model (1996), assume full flexibility: every task may join every server. Rutten and Mukherjee (arXiv:2008.07562, Math. Oper. Res. 2023) identify graph conditions under which JSQ($d$) on a sparse compatibility graph behaves, in the large-system limit, exactly like the fully flexible system. This holds both on finite time intervals and in steady state.

Related work includes Budhiraja, Mukherjee and Wu (2019), on the supermarket model on graphs whose vertices are servers; Mukherjee, Borst, van Leeuwaarden and Whiting (2018), on the universality of power-of-$d$ schemes; and Bramson (2011) and Cardinaels, Borst and van Leeuwaarden (2019), on the stability of JSQ-type policies under compatibility constraints.

Setting

There are $N$ servers $V_N$ and $M(N)\ge1$ dispatchers $W_N$, with an edge set $E_N\subseteq V_N\times W_N$. Dispatcher $w$ can only send tasks to its neighbourhood $\mathcal N_w=\{v:(v,w)\in E_N\}$.

• Tasks arrive at each dispatcher as independent Poisson streams of rate $\lambda N/M(N)$, with $0<\lambda<1$.
• Each server has its own infinite-buffer queue with unit-mean exponential services.
• Under JSQ($d$), $d\ge2$, an arriving task at $w$ samples $\min(d,|\mathcal N_w|)$ servers of $\mathcal N_w$ uniformly at random, without replacement, and joins a shortest of their queues. Ties are broken uniformly at random.

The state $\Phi(G_N,t)\in\mathbb N^{V_N}$ is the vector of queue lengths. Two statistics of a state $z$ are used:

• the occupancy $q_i(z)=|\{v:z_v\ge i\}|/N$;
• the local empirical distribution $x^w_i(z)=|\{v\in\mathcal N_w:z_v=i\}|/|\mathcal N_w|$.

Occupancies live in $\mathcal Y=\{q\in\ell_1:q_i\in[0,1],\ q_i\ge q_j\text{ for }i<j\}$.

The sequence $\{G_N\}$ is proportionally sparse if for every $\varepsilon>0$

$$\sup_{U\subseteq V_N}\frac1{M(N)}\Big|\Big\{w:\Big|\frac{|\mathcal N_w\cap U|}{|\mathcal N_w|}-\frac{|U|}{N}\Big|\ge\varepsilon\Big\}\Big|\to0 .$$

Put $k_w=\min(d,|\mathcal N_w|)$. The sequence is subcritical if there are probability distributions $\gamma^U_w$ on the sampled sets $U$ with

$$\limsup_{N\to\infty}\max_{v}\frac{N}{M(N)}\sum_w\binom{|\mathcal N_w|}{k_w}^{-1}\sum_{U\subseteq\mathcal N_w,\,|U|=k_w}\gamma^U_w(v)\le1 .$$

This bounds the load that a static randomised routing would put on any server.

The fully flexible mean-field limit is the system of ODEs

$$\frac{dq^*_i}{dt}=\lambda\big((q^*_{i-1})^d-(q^*_i)^d\big)-(q^*_i-q^*_{i+1}),\qquad i\ge1,\quad q^*_0\equiv1,\qquad(3.3)$$

whose fixed point is $q^*_i(\infty)=\lambda^{(d^i-1)/(d-1)}$.

Formalization targets

Goal: Theorem 3.4

Let $\{G_N\}$ be proportionally sparse and connected, and suppose $q^*(0)\in\mathcal Y$ with $\|q(\Phi(G_N,0))-q^*(0)\|_1\to0$. Then, for every $T\ge0$ and $\varepsilon>0$,

$$P\Big(\sup_{t\le T}\|q(\Phi(G_N,t))-q^*(t)\|_1\ge\varepsilon\Big)\to0 .$$

If moreover $\{G_N\}$ is subcritical, then for all large $N$ the chain has a unique stationary distribution $\pi_N$, and $\pi_N(\|q-q^*(\infty)\|_1\ge\varepsilon)\to0$.

Milestones, in the order the proof uses them

• Lemma 4.2: the JSQ($d$) assignment function is Lipschitz.
• Lemma F.1 and Proposition 4.5: on proportionally sparse graphs, local and global empirical distributions agree for almost all dispatchers, uniformly on $[0,T]$.
• Proposition 4.7: under the optimal coupling, the occupancy distance to the fully flexible system is at most twice the number of routing mismatches.
• Theorem 4.3: the process-level limit for Lipschitz policies.
• Lemmas H.2, H.4, H.5 and Theorem 4.8(i): Foster–Lyapunov stability for all large $N$.
• Lemmas 4.9, 4.10 and Theorem 4.8(ii): tightness of the steady states in a weighted $\ell_1$ space.
• Theorem 4.11: exponential global stability of (3.3) in that weighted norm.

Significance

The result. The theorem separates two graph properties.

• Proportional sparsity is an expansion property; it alone makes the transient dynamics universal.
• Subcriticality is a capacity condition; it alone gives stability and tightness of the stationary distributions.

Together they justify using the fully flexible ODE (3.3) and its fixed point for the stationary performance of a constrained system. Companion results (Theorems 3.5 and 3.6, formalized in missions 2 and 3 of this series) show that random graphs with degrees growing only slightly faster than logarithmically satisfy both conditions, so the flexibility needed for full mean-field performance is far smaller than complete flexibility.

Formalizing it. The result is proved on paper but has no machine-checked proof. A formalization would produce the following.

• A reusable model of a continuous-time Markov chain with bounded rates, realised by uniformisation.
• Foster–Lyapunov and petite-set arguments on a countable state space.
• A pathwise coupling bound.
• A tightness criterion in weighted $\ell_1$.
• An interchange-of-limits argument.

The global stability of (3.3) relies on Mitzenmacher's weighted-potential theorem, which is posed separately on the platform (PowerTwoChoices.Limit.theorem_3) and is open.

Difficulty

The obvious argument couples the system on $G_N$ with the fully flexible system server by server. This fails because a task arriving at $w$ can only join $\mathcal N_w$, so the two systems cannot place it at the same server. The paper instead couples the queue lengths chosen and counts mismatches. That bound is only useful if almost every dispatcher sees a local queue-length distribution close to the global one at all times. The set of good dispatchers changes with the state, and controlling it requires a uniform bound over all subsets of servers.

A second gap concerns the goal itself. Theorem 4.3 covers policies that depend only on the local empirical distribution. JSQ($d$) without replacement also depends on $|\mathcal N_w|$ when neighbourhoods are small, so deducing the goal from Theorem 4.3 needs an approximation step that the paper does not spell out.

For the steady state, subcriticality bounds a $\limsup$ only, so stability holds for large $N$ and not for every $N$. Tightness in a fixed $\ell_1$-ball does not suffice: the limit is identified through a stability result that holds in a weighted norm with geometrically growing weights. The tightness has to be proved in that norm, through moment bounds on stationary tails.

Formalization scope

• Graphs. Servers are Fin N, dispatchers Fin (M N) with $M(N)\ge1$, and edges a Finset. Connectivity is a separate hypothesis (Definition 3.1 and §2). Proportional sparsity is the limit condition (3.1). In subcriticality the normaliser is $\binom{|\mathcal N_w|}{k_w}$, and the distributions $\gamma^U_w$ are constrained only for nonempty $U$. Both choices agree with the paper whenever $|\mathcal N_w|\ge d$.
• Dynamics. The process is the uniformised chain with kernel lbKernel, run at the epochs of an independent Poisson clock of rate $(\lambda+1)N$. Statements quantify over every realisation on every probability space, for $N\ge1$. JSQ($d$) samples without replacement; with replacement, Theorem 4.8 is false under Definition 3.3.
• Occupancy. The occupancy is indexed from $0$ with $q_0=1$, and $\ell_1$ distances are l1dist in $[0,\infty]$. "Converges weakly" to a deterministic limit is rendered as convergence in probability. Ergodicity is rendered as existence and uniqueness of a stationary distribution.
• Repairs to the printed text. The printed (3.4) exponent $(d^i-d)/(d-1)$ is corrected to $(d^i-1)/(d-1)$; with the printed value the steady-state claim is false. "For each fixed $N$, ergodic" becomes "for all $N\ge N_0$".
• Ruled out. A rendering in which the hypotheses cannot all hold would make the statements vacuous. Every routing law here sums to one and every clock rate is positive, so neither the process hypotheses nor the ODE hypothesis are vacuous. The conclusion asserts the existence of the stationary distributions it then speaks about.
• Reused definitions. PowerTwoChoices.Limit.SupermarketSystem (the ODE, fixed point and potential) and PowerOfDUniversality.Fluid.FluidSpace (l1dist, supDistL1).
• Generic and reusable. The Markov-chain notions in CountableChain: stationarity, $n$-step kernels, petite sets and uniformisation.

Contributions to any milestone are welcome. Lemma 4.2, Proposition 4.7 and Lemma H.4 are self-contained.

Selected references

• D. Rutten, D. Mukherjee, Load Balancing Under Strict Compatibility Constraints, Math. Oper. Res. (2023); preprint arXiv:2008.07562v2 (cited version). https://arxiv.org/abs/2008.07562
• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Trans. Parallel Distrib. Syst. 12 (2001). https://doi.org/10.1109/71.963420
• N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing system with selection of the shortest of two queues: an asymptotic approach, Probl. Inf. Transm. 32 (1996).
• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of power-of-d load balancing in many-server systems, Stochastic Systems 8 (2018). https://arxiv.org/abs/1612.00723
• M. Bramson, Stability of join the shortest queue networks, Ann. Appl. Probab. 21(4):1568–1625 (2011).
• A. Budhiraja, D. Mukherjee, R. Wu, Supermarket model on graphs, Ann. Appl. Probab. 29(3):1740–1777 (2019).
• E. Cardinaels, S. C. Borst, J. S. H. van Leeuwaarden, Job assignment in large-scale service systems with affinity relations, Queueing Syst. 93:227–268 (2019).
• S. P. Meyn, R. L. Tweedie, Markov Chains and Stochastic Stability, Springer (1993).

Motivation

Outpatient clinics serve two kinds of patients: those who book an appointment and those who walk in on the day. Many providers now run open-access or hybrid schedules, which reserve part of the day for walk-ins. Whether patients book or walk in depends on what they know about the appointment delay. Some clinics publish the next available slot in real time (online booking). Others take requests asynchronously, so patients act on a typical delay. Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science, 2023, doi:10.1287/mnsc.2023.4676) model this choice as a game between strategic patients and a provider who splits capacity between appointment and walk-in hours. This mission formalizes their first comparison result: when capacity is short, showing patients the exact delay is at least as good for the provider as hiding it.

The model extends Naor's observable-queue joining problem (Naor, Econometrica, 1969) to an M/D/1 appointment queue with a continuous delay threshold, and adds a walk-in channel whose waiting cost depends on congestion.

Setting

Demand. Strategic patients arrive as a Poisson process of rate $\lambda>0$ per day. Exogenous walk-ins arrive at rate $\lambda_E\ge0$ and always walk in.

Capacity. The provider has total daily capacity $\mu>0$. It allocates $\mu_S$ to appointment hours and $\mu_W=\mu-\mu_S$ to walk-in hours, with $0\le\mu_S<\mu$. Appointments form a single-server queue with deterministic service time $1/\mu_S$.

Utilities. Service is worth $R>0$. A patient who books with delay $d$ gets $R-C_Dd$, where $C_D>0$. A patient who walks in gets $R-C_W\,w(\rho_W)$, where $C_W>0$ and $\rho_W$ is the walk-in traffic intensity (walk-in arrivals divided by $\mu_W$). Balking is worth $0$. The function $w$ is convex and strictly increasing on $[0,\infty)$ with $w(0)=0$ (Assumption 1).

Provider cost. Each balking patient costs $C_L\ge0$, and overtime costs $C_O\,o(\rho_W)$ with $C_O\ge0$, where $o$ is convex and strictly increasing on $[0,\infty)$ (Assumption 2).

Observable setting. Each patient sees the exact delay $(k+\tilde u)/\mu_S$, where $k$ is the number waiting and $\tilde u$ is uniform on $[0,1]$. A strategy is a triple $(\delta,p_W,p_B)$: book if the delay is at most $\delta$, and otherwise walk in or balk with probabilities $p_W$ and $p_B$. The appointment queue is then the M/D/1/K−1+p queue with $K=\lceil\delta\mu_S\rceil$ and $p=\delta\mu_S+1-K$. Its blocking probability has the closed form

$$\pi(\delta,\mu_S)=1-\frac{1}{q_0+\rho},\qquad \rho=\frac{\lambda}{\mu_S},$$

where $q_0$ is the probability that a departure leaves the system empty, given by Brun–Garcia sums of Poisson weights. An observable equilibrium satisfies conditions (6)–(10): booking is preferred to the walk-in/balk mixture exactly for delays up to $\delta$; $p_W+p_B=\pi(\delta,\mu_S)$; and patients walk in only if walking in is worth at least $0$, and balk only if it is worth at most $0$. The cost is

$$Z^o=C_L\,p_B\lambda+C_O\,o\Big(\frac{p_W\lambda+\lambda_E}{\mu_W}\Big).$$

Unobservable setting. Patients see only the expected M/D/1 delay $\bar d=\lambda_S/(2\mu_S(\mu_S-\lambda_S))$ and choose rates $(\lambda_S,\lambda_W,\lambda_B)$ that sum to $\lambda$. An unobservable equilibrium uses only options of maximal utility among $u^1_S=R-C_D\bar d$, $u^1_W=R-C_Ww((\lambda_W+\lambda_E)/\mu_W)$ and $0$. The cost is

$$Z^u=C_L\lambda_B+C_O\,o\Big(\frac{\lambda_W+\lambda_E}{\mu_W}\Big).$$

Formalization targets

Goal: Theorem 2 (1)

If

$$\mu\le\sqrt{\frac{\lambda C_D}{2R}},$$

then for every allocation $\mu_S$ and every unobservable equilibrium $u$ at $\mu_S$, there is an allocation $\mu'_S$ at which an observable equilibrium exists and every observable equilibrium costs at most $Z^u(u)$. Equivalently, the optimal observable cost is at most the optimal unobservable cost. The paper states "when $\mu$ is sufficiently small"; the threshold is the one its proof establishes.

Milestones

1. (27), §C.1: the closed-form departure law $q_0,\dots,q_K$ is a probability vector that solves the departure-epoch balance equations.
2. Proof of Theorem 2(1): $\lambda/(1+\lambda/\mu_S)\le\lambda[1-\pi(\delta,\mu_S)]\le\lambda$.
3. Proposition C.2 ($\delta$-part): $\pi(\cdot,\mu_S)$ is continuous and strictly decreasing.
4. Proposition 1 (observable setting): an observable equilibrium exists at every allocation.
5. Lemma D.3: an unobservable equilibrium exists at every allocation.
6. Lemma E.5 (1): at a fixed allocation, if $\lambda[1-\pi(\bar d^u,\mu_S)]\ge\lambda^u_S$, the observable setting costs no more.

Significance

The result says that real-time delay information helps a capacity-constrained provider. Patients who see a short queue book instead of balking, so the appointment hours are better used. The second part of Theorem 2 shows that the comparison can reverse when capacity is large, so the information choice depends on the regime. The small-capacity side is the one that applies to clinics without spare capacity.

The formalization also produces reusable queueing content. It gives a machine-checked closed form for the M/D/1/K−1+p queue with fractional buffer (Hassin–Haviv notation): its departure-epoch law, its blocking probability, and the monotonicity and continuity of that probability in the buffer. The paper's proofs are in its Online Appendix: E.3 for Lemma E.5 and Theorem 2, and E.4 for Appendix C. None of these results has a machine-checked proof.

Difficulty

The obvious argument fixes an optimal unobservable allocation and compares both settings there. That argument has three gaps. First, the existence of an optimum of (Un.P) is never proved, so the comparison has to work at every allocation. Second, the same-allocation comparison (Lemma E.5) is a three-by-three case analysis over the equilibrium regimes (schedule-balk, schedule-walk-balk, schedule-walk) of the two settings. One printed case concludes the opposite inequality; under the lemma's hypothesis that case forces equal costs. Third, the closed-form blocking probability is an alternating sum. Its positivity, its bound $q_0\le1$ and its monotonicity across the seams where $\lceil\delta\mu_S\rceil$ jumps are not visible term by term. Existence of the observable equilibrium needs an intermediate-value argument through the continuity of $\pi$ in $\delta$.

Formalization scope

Everything lives in the namespace OutpatientWalkIn.SmallCap, in two definition modules.

• MD1Queue holds the Poisson weights, the $a_j$ recursion (one clause for $j\ge1$), $b_j$, $a'_K$ of (26), the departure law (27), $\alpha'_j$ of (24) and $\pi(\delta,\mu_S)$.
• Setting holds the model, the standing assumptions, both equilibrium notions and both costs.

The conventions are the following.

• Disengagement cost. $C_G$ is not a parameter. The observable ($C_G=0$) and unobservable ($C_G=+\infty$) settings are defined directly, as Lemmas 4 and 6 and Appendices D.3 and D.5 reduce them.
• Standing assumptions. $\lambda>0$, $\lambda_E\ge0$, $R,C_D,C_W>0$, $C_L,C_O\ge0$, $\mu>0$, and Assumptions 1–2 on $[0,\infty)$. The paper leaves the signs other than $R,C_D,C_W>0$ implicit.
• Allocations. $0\le\mu_S<\mu$, so the walk-in intensity never divides by $0$.
• No appointment capacity. $\pi(\delta,0)=1$. In the unobservable setting, $\mu_S=0$ forces $\lambda_S=0$ and drops $u^1_S$ from the comparisons.
• Stability. An unobservable equilibrium must have $\lambda_S<\mu_S$, so the junk value of (18) at $\lambda_S\ge\mu_S$ never enters.
• Mixture weights. The observable equilibrium requires $p_W+p_B>0$, which (8) implies.
• Formula branches. $(1-p)^{-n}$ is written $((1-p)^n)^{-1}$, and the branches $p=1$ and $p<1$ are separate.
• Costs less. It means $\le$ (p. 26).

A trivializing formalization is ruled out on four counts: $\pi$ is the paper's closed form, not an assumed function; the goal quantifies over every unobservable equilibrium and every observable equilibrium at the chosen allocation; no infimum over a possibly empty set appears; and both equilibrium sets are nonempty (milestones 4 and 5).

The infrastructure needed is elementary real analysis and finite sums. Contributions are welcome on the queue lemmas (positivity of $a_j$ and $a'_K$, the bound $q_0\le1$, continuity across seams), which are reusable for any finite-buffer M/D/1 model. The companion mission on the triage model uses the same encoding.

Selected references

• N. Liu, W. van Jaarsveld, S. Wang, G. Xiao, Managing Outpatient Service with Strategic Walk-ins, Management Science, 2023 (SSRN copy of 2022-07-05). https://ssrn.com/abstract=3558209, https://doi.org/10.1287/mnsc.2023.4676
• P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200
• O. Brun, J.-M. Garcia, Analytical Solution of Finite Capacity M/D/1 Queues, Journal of Applied Probability 37(4), 2000. https://doi.org/10.1239/jap/1014843085
• R. Hassin, M. Haviv, To Queue or Not to Queue: Equilibrium Behavior in Queueing Systems, Kluwer, 1997 (2003 ed.). https://doi.org/10.1007/978-1-4615-0359-0

Motivation

A manufacturer that makes several products to stock for price-sensitive customers controls three levers at once: the prices it posts, which shape demand; outsourcing, which clears a large backlog at a cost; and scheduling, which decides which product the single server makes next. Ata and Barjesteh (Operations Research 71(1), 2023) study this multiclass make-to-stock queue in the heavy-traffic regime, where the queue is nearly saturated and the system is approximated by a Brownian control problem. The approximation collapses to a one-dimensional problem in the workload, the total amount of work in the system. Its solution is a two-barrier policy whose state-dependent drift translates back into a dynamic pricing rule, an outsourcing threshold and a scheduling priority (§7 of the paper).

The one-dimensional problem belongs to the family of drift-rate control problems for Brownian motion under a long-run average cost criterion (Ata, Harrison and Shepp, Ann. Appl. Probab. 2005; Rubino and Ata, Oper. Res. 2009). Problems of this kind are solved by a Bellman equation with free boundaries and a verification argument; the present paper adds two-sided singular control (outsourcing at the bottom, idling at the top) to a quadratic drift cost and a piecewise linear state cost.

Setting

There are $K\ge1$ products with mean production times $m_k>0$ and holding, backorder and outsourcing cost rates $h_k,b_k,r_k>0$. A symmetric positive definite matrix $H$ describes the curvature of the revenue rate. Write $a=m'H^{-1}m$ and

$$h^\star=\min_k\frac{h_k}{m_k},\qquad b^\star=\min_k\frac{b_k}{m_k},\qquad \kappa=\min_k\frac{r_k}{m_k}.$$

The drift cost and the effective holding cost are

$$c(x)=\min\{\zeta'H\zeta:\ m'\zeta=x\},\qquad h(w)=h^\star w\ (w\ge0),\quad h(w)=-b^\star w\ (w<0).$$

Let $B$ be a Brownian motion with drift $\mu\ge0$ and variance $\sigma^2>0$, started at $0$, with respect to a filtration $\mathbb F$. An admissible control consists of a progressively measurable drift rate $\theta$ and nondecreasing, right-continuous, adapted processes $L$ (effective outsourcing) and $U$ (idleness) with $L(0)=U(0)=0$. The workload is

$$W(t)=B(t)-\int_0^t\theta(s)\,ds-U(t)+L(t),$$

and admissibility also requires $\mathbb E|W(t)|/t\to0$. The equivalent workload formulation (EWF) is to minimize

$$\limsup_{t\to\infty}\frac1t\,\mathbb E\Big[\int_0^tc(\theta(s))\,ds+\int_0^th(W(s))\,ds+\kappa L(t)\Big]. \tag{29}$$

A barrier policy with barriers $l<u$ keeps $W$ in $[l,u]$, increases $L$ only when $W=l$ and $U$ only when $W=u$.

For $\gamma\ge0$ put $l_\gamma=-\frac1{b^\star}(\gamma+\mu\kappa+\frac a4\kappa^2)$ and $u_\gamma=\gamma/h^\star$. Let $v^-_\gamma$ solve the Riccati equation

$$v'=\frac a{2\sigma^2}(v^2-\kappa^2)-\frac{2\mu}{\sigma^2}(v+\kappa)+\frac{2(h(l_\gamma)-h(w))}{\sigma^2}\ \text{on }[l_\gamma,0],\qquad v(l_\gamma)=-\kappa,$$

and $v^+_\gamma$ solve $v'=\frac a{2\sigma^2}v^2-\frac{2\mu}{\sigma^2}v+\frac{2(h(u_\gamma)-h(w))}{\sigma^2}$ on $[0,u_\gamma]$ with $v(u_\gamma)=0$. The paper's $\gamma^\star$ is the unique $\gamma$ with $v^-_{\gamma}(0)=v^+_{\gamma}(0)$; $v$ pastes $v^-_{\gamma^\star}$ and $v^+_{\gamma^\star}$ at $0$, and the candidate drift is $\theta(w)=\frac a2v(w)$.

Formalization targets

Goal: Theorem 1

For every filtered probability space carrying such a Brownian motion,

$$\lim_{t\to\infty}\frac{J_{\text{cand}}(t)}t=\gamma^\star\quad\text{for every barrier policy at }(l_{\gamma^\star},u_{\gamma^\star})\text{ with drift }\theta(W),\qquad \limsup_{t\to\infty}\frac{J(t)}t\ge\gamma^\star\ \text{for every admissible control},$$

where $J$ is the expected cumulative cost in (29). The constant $\gamma^\star$ is the paper's construction, not a parameter.

Milestones

1. Lemma 1 and Lemma 2: the closed forms $c(x)=x^2/a$ and its conjugate $\varphi(y)=\frac a4y^2$, maximized at $\psi(y)=\frac a2y$.
2. Proposition 2: a barrier policy whose $(\gamma,f)$ solves the ODE (35)–(36) has long-run average cost $\gamma$.
3. Lemma 3: any solution of the Riccati-form Bellman equation (43)–(45) has $\gamma>0$, $l=l_\gamma<0$, $u=u_\gamma>0$.
4. Lemmas 18–20 and Corollary 6: sign and monotonicity of the Riccati solutions.
5. §6.3 well-posedness, Lemma 4(i)–(ii), Corollary 1: uniqueness of $v^\pm_\gamma$, their monotone dependence on $\gamma$, and the unique crossing $\gamma^\star$.
6. Proposition 3 and Corollary 2: $(l_{\gamma^\star},u_{\gamma^\star},\gamma^\star,v)$ is the unique solution of (43)–(45), and $f=\int v$ solves the Bellman equation (37)–(39), uniquely up to a constant.

Significance

The theorem identifies an explicit optimal policy for a two-sided singular drift-control problem: two barriers and a strictly increasing, non-positive drift, all determined by a scalar root $\gamma^\star$ of a monotone equation. In the paper it drives the proposed pricing, outsourcing and scheduling policy (§7) and its asymptotic analysis; the Riccati structure is what makes $\gamma^\star$ computable by line search.

The result is proved in the paper; none of it has been machine-checked. Formalizing it gives a checked verification theorem for an average-cost Brownian control problem with singular controls, and checked statements of the Riccati comparison lemmas on which it rests. Several printed statements of the paper are corrected here (see the scope section), so the formal versions are the first fully precise ones.

Difficulty

The optimality half of Theorem 1 is a verification argument: apply Itô's formula to $f(W(t))$ for an arbitrary admissible control with jumps in $L$ and $U$, use the Bellman inequality pointwise, and control $\mathbb E f(W(t))/t$ with the growth condition (32). Mathlib does not yet have Itô's formula for continuous semimartingales with finite-variation, possibly discontinuous parts, and the candidate's average cost (Proposition 2) needs the same tool plus the fact that a reflected diffusion spends zero time at the barriers.

The deterministic half is not routine either. The obvious reading of the paper, solving each Riccati problem for every $\gamma\ge0$ and passing $\gamma\to\infty$, fails: the solutions blow up in finite time, so $v^\pm_\gamma$ exist only for $\gamma$ in a bounded initial interval, and the crossing argument must be run on that interval. The comparison arguments of Lemmas 18–20 also need second derivatives of solutions whose right-hand side has a kink at $w=0$.

Formalization scope

Time is indexed by $\mathbb R$ and only $t\ge0$ matters. The Brownian motion is defined locally (drift, variance, start at $0$, independence of increments from the filtration). Expected costs are computed in $[0,\infty]$, so a control with infinite cost counts as $+\infty$. The integrals in (34) are Lebesgue–Stieltjes integrals against the paths of $L$ and $U$, jumps included. Derivatives at the barriers are one-sided; $C^1$ and $C^2$ up to the boundary are ContDiffOn on the closed interval. Minima and maxima (in $c$, (37), (40)) are stated as attained.

Standing assumptions added to every statement, all implicit in the paper: $K\ge1$; $m_k,h_k,b_k,r_k>0$; $H$ symmetric positive definite; $\mu\ge0$, $\sigma>0$; $B$ starts at $0$; $L,U$ right-continuous; $\theta$ progressively measurable with locally integrable paths; $l<u$ in the Bellman equations.

Corrected statements. Lemmas 18–20 are printed for solutions on $[0,\infty)$, which do not exist; they are posed on every bounded interval where a solution exists. The §6.3 claim that $v^\pm_\gamma$ exist for every $\gamma\ge0$ is replaced by uniqueness, solvability at $\gamma=0$ and order-connectedness of the solvability sets. Lemma 4's limits as $\gamma\to\infty$ become unboundedness on those sets. Theorem 1's comparison class is every admissible control, which the paper's proof treats, and which contains the stationary Markov policies to which §6 restricts attention.

Not posed. The existence of the reflected diffusion realizing the candidate policy is presupposed by the paper and not claimed: the first half of the goal quantifies over all barrier policies with the given data. The second half is a statement about every admissible control and is not vacuous.

$\gamma^\star$, $v$, $f$ and $\theta$ are built from the Riccati solutions by choice, exactly as the paper constructs them; taking them as hypotheses-constrained parameters, or defining $c$ by its closed form, would trivialize the goal and is ruled out. Contributions are welcome on the Riccati lemmas (pure real analysis, reusable for other drift-control problems), on Itô's formula for semimartingales with finite-variation parts, and on Skorokhod-type existence of reflected diffusions.

Selected references

• B. Ata and N. Barjesteh, An Approximate Analysis of Dynamic Pricing, Outsourcing, and Scheduling Policies for a Multiclass Make-to-Stock Queue in the Heavy Traffic Regime, Operations Research 71(1):341–357, 2023. https://doi.org/10.1287/opre.2022.2361 (accepted manuscript: https://ssrn.com/abstract=3464763)
• B. Ata, J. M. Harrison and L. A. Shepp, Drift rate control of a Brownian processing system, Annals of Applied Probability 15(2):1145–1160, 2005. https://doi.org/10.1214/105051604000000855
• M. Rubino and B. Ata, Dynamic control of a make-to-order, parallel-server system with cancellations, Operations Research 57(1):94–108, 2009. https://doi.org/10.1287/opre.1080.0532
• J. M. Harrison, Brownian Models of Performance and Control, Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139087698