Operations Research

Motivation

A data center or cloud platform routes each incoming task to one of $N$ parallel servers. Sending each task to a server with the shortest queue, the join-the-shortest-queue (JSQ) policy, minimizes waiting in a strong sense, but the dispatcher must learn all $N$ queue lengths for every arrival. The power-of-d schemes cut this communication: the dispatcher samples $d$ servers and joins the shortest of them. Mukherjee, Borst, van Leeuwaarden and Whiting ask how large $d=d(N)$ must be for the sampled scheme to perform as well as JSQ as $N\to\infty$. They answer at two scales. At the fluid scale (mission 1 of this series) $d(N)\to\infty$ suffices. At the diffusion scale of the Halfin–Whitt regime, the subject of this mission, $d(N)/(\sqrt N\log N)\to\infty$ suffices, and $d(N)/(\sqrt N\log N)\to 0$ does not.

Timeline:

• Halfin and Whitt (1981) introduced the heavy-traffic regime $(N-\lambda(N))/\sqrt N\to\beta>0$ for many-server systems.
• Eschenfeldt and Gamarnik (2018, arXiv:1502.00999) proved the diffusion limit of ordinary JSQ in this regime, the system (2.4) below.
• Mukherjee, Borst, van Leeuwaarden and Whiting (Stochastic Systems 8(4), 2018; arXiv:1612.00723v2) proved that JSQ(d(N)) has the same diffusion limit when $d(N)/(\sqrt N\log N)\to\infty$ (Theorem 2.4), and that the limit differs when $d(N)/(\sqrt N\log N)\to 0$ (Theorem 2.5).

Setting

There are $N$ servers, each with a buffer of size $b\in\{2,3,\dots\}\cup\{\infty\}$ that counts the task in service. Tasks arrive as a Poisson process of rate $\lambda(N)$, and each needs a unit-mean exponential amount of work, served at unit rate. A task sent to a full server is discarded. Under JSQ(d) the dispatcher samples $d$ servers without replacement ($1\le d\le N$) and sends the task to a server with the shortest queue among them. For $d=N$ this is JSQ.

The state is the occupancy vector $Q=(Q_1,\dots,Q_b)$, where $Q_i$ is the number of servers with at least $i$ tasks. The conventions are $Q_0=N$ and $Q_i=0$ for $i>b$. With the servers ordered by nondecreasing queue length, the $c$-th ordered server has queue length $I(c)=\max\{i\ge0:Q_i\ge N-c+1\}$. An arrival at position $c$ raises $Q_{I(c)+1}$ by one when $I(c)<b$. A departure at position $k$ lowers $Q_{I(k)}$ by one when $I(k)\ge1$. JSQ(d) routes to the smallest position in a uniform $d$-subset of $\{1,\dots,N\}$.

In the Halfin–Whitt regime $(N-\lambda(N))/\sqrt N\to\beta>0$, the diffusion-scaled state is

$$\bar Q_1=-\frac{N-Q_1}{\sqrt N},\qquad \bar Q_i=\frac{Q_i}{\sqrt N}\quad(i\ge2).$$

Here $-\bar Q_1$ is the scaled number of idle servers.

Formalization targets

Goal: Theorem 2.4 (pp. 7–8)

Let $\beta>0$, $b\ge2$ and $k\ge2$. Assume $\bar Q_{k+1}(0)=0$ for large $N$ and $(\bar Q_1(0),\dots,\bar Q_k(0))\Rightarrow\nu$. If $d(N)/(\sqrt N\log N)\to\infty$, then $\bar Q^{d(N)}\Rightarrow\bar Q$ in $D_{\ell_1}[0,\infty)$, where $\bar Q_i\equiv 0$ for $i\ge k+1$ and

$$\begin{aligned}\bar Q_1(t)&=\bar Q_1(0)+\sqrt2W(t)-\beta t+\int_0^t(-\bar Q_1+\bar Q_2)\,ds-U_1(t),\\ \bar Q_2(t)&=\bar Q_2(0)+U_1(t)-\int_0^t(\bar Q_2-\bar Q_3)\,ds,\\ \bar Q_i(t)&=\bar Q_i(0)-\int_0^t(\bar Q_i-\bar Q_{i+1})\,ds,\quad 3\le i\le k.\end{aligned}$$

Here $W$ is a standard Brownian motion and $U_1$ is the nonnegative nondecreasing regulator with $\int_0^\infty\mathbb 1_{[\bar Q_1<0]}\,dU_1=0$. The goal also asserts that this solution is unique.

Milestones

1. Uniqueness clause of Theorem 2.4: (2.4), with the constraint $\bar Q_1\le0$, has at most one solution for every driving path.
2. Theorem 2.4 for $d(N)=N$: the JSQ diffusion limit of [8, Theorem 2], stated along an arbitrary sequence of server counts $N_j\to\infty$.
3. Proposition 5.1 (p. 32): if JSQ has the diffusion limit along every such sequence, then so does JSQ(d(N)) with $d(N)/(\sqrt N\log N)\to\infty$.

The goal follows from 1–3.

Significance

The result. Theorem 2.4 shows that $O(\sqrt N\log N)$ queue-length queries per arrival already achieve diffusion-level optimality: over any finite horizon only $O_P(\sqrt N)$ servers are idle and only $O_P(\sqrt N)$ hold two or more tasks, exactly as under JSQ. With Theorem 2.5 it identifies $\sqrt N\log N$ as the minimal order of $d(N)$. The diffusion limit is also the input for the steady-state analyses of JSQ in this regime (Braverman; Banerjee and Mukherjee).

Formalizing it. The result is proved on paper; nothing in it is machine-checked. A formalization needs:

• a rigorous construction of the many-server JSQ(d) process;
• the stochastic-coupling comparison of §3;
• weak convergence of $\ell_1$-valued processes;
• a reflected integral equation of Skorokhod type.

The Eschenfeldt–Gamarnik limit (milestone 2) is cited by the paper, not proved in it, so its formalization is a separate, substantial contribution.

Difficulty

JSQ(d(N)) cannot be compared with JSQ path by path. The same arrival is routed to different servers under the two schemes, so their occupancy vectors drift apart and do not stay ordered. The obvious generator-based diffusion argument for JSQ(d(N)) itself does not close either. The routing probabilities depend on the whole ordered queue-length profile through $\binom{\cdot}{d}/\binom{N}{d}$-type terms, and these do not reduce to a function of $\bar Q_1,\bar Q_2$ at scale $\sqrt N$ unless $d(N)$ is large enough.

The threshold is sharp: for $d(N)\ll\sqrt N\log N$ the limit is different (Theorem 2.5). Any argument therefore has to use the growth rate quantitatively, controlling at scale $o_P(\sqrt N)$ over a finite horizon how often JSQ(d(N)) fails to make a near-shortest choice. A qualitative fluid-type argument cannot do this. A second difficulty is the limit itself: (2.4) is a reflected equation whose regulator enters two coordinates, so even its well-posedness needs a Skorokhod-type argument with feedback.

Formalization scope

Lean conventions:

• Levels and positions use the paper's index base: Q i is $Q_i$ for $i\ge1$, with Q 0 = N, and positions are $1,\dots,N$. The initial vector Fin k → ℝ lists levels $1,\dots,k$.
• Buffer b : ℕ∞ with 2 ≤ b; ⊤ is an infinite buffer.
• Process construction is by uniformization. A Poisson clock of rate $\lambda+N$ is built from i.i.d. expMeasure (λ + N) interarrival times through the published renewalCount/partialSum. Its i.i.d. marks are arrivals, with probability $\lambda/(\lambda+N)$ and a uniform $d$-subset, or departures at a uniform position. Marks are independent of the clock and of a random initial state. The model is therefore the paper's in law. Sampling is without replacement, so JSQ(N) is JSQ.
• Path space. $D_{\mathbb S}[0,\infty)$ is read as $\ell_1$-valued càdlàg paths, as the proof controls $\ell_1$ distances. Weak convergence to the continuous limit is stated in coupling form: a common probability space with copies of the laws and almost sure uniform convergence in $\ell_1$ on compacts.
• Initial convergence is joint convergence in law of $(\bar Q_1(0),\dots,\bar Q_k(0))$, via bounded continuous test functions. The page's coordinatewise convergence does not determine the limit. The limit's initial value is independent of $W$.
• Solution concept of (2.4) includes $\bar Q_1\le0$, implicit in the paper; without it $U_1\equiv0$ satisfies the complementarity condition and uniqueness fails. $\int\mathbb 1_{[\bar Q_1<0]}dU_1=0$ is a Lebesgue–Stieltjes measure condition. $W$ is Mathlib's IsBrownianReal.
• "Same diffusion limit" in Proposition 5.1 is the paper's reduction: the JSQ result, for all server-count sequences, implies the JSQ(d(N)) result.

Trivializing formalizations are ruled out. The goal asserts the existence of the limit (Brownian motion, initial value and solution), not merely that every limit point solves (2.4). The system hypotheses are satisfiable: the mark law has total mass one, which is checked in Lean. The convergence is of the whole $\ell_1$ path, including the tail above level $k$.

Infrastructure needed and welcome:

• a library for $\ell_1$-valued càdlàg processes;
• the one-sided Skorokhod map with Lipschitz feedback, reusable for many reflected limits;
• the S-coupling of §3, posed as milestones in mission 1 of this series;
• a formal proof of the Eschenfeldt–Gamarnik JSQ limit.

Selected references

• 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(4), 2018. arXiv:1612.00723v2, doi:10.1287/stsy.2018.0016
• P. Eschenfeldt, D. Gamarnik, Join the shortest queue with many servers. The heavy-traffic asymptotics, Mathematics of Operations Research 43(3), 2018. arXiv:1502.00999
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. doi:10.1287/opre.29.3.567
• A. Braverman, Steady-state analysis of the join-the-shortest-queue model in the Halfin–Whitt regime, Mathematics of Operations Research 45(3), 2020. arXiv:1801.05121

Motivation

Algorithms for smooth nonlinear programming, such as augmented Lagrangian, interior point and sequential quadratic programming methods, do not stop at exact Karush–Kuhn–Tucker (KKT) points. They stop at points where the KKT conditions hold approximately. Sequential optimality conditions make this precise: they are properties of sequences $x^k\to x^*$ with approximate multipliers, satisfied at every local minimizer without any constraint qualification, and verified by the iterates of practical methods. To conclude that a limit point is a KKT point, one still needs a condition on the constraints. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) identify, for each of several sequential conditions, the weakest such condition. They call it the weakest strict constraint qualification associated with that condition, and they place each one within the classical hierarchy of constraint qualifications.

This mission concerns the Complementary AKKT condition (CAKKT) of Andreani, Martínez and Svaiter (SIAM J. Optim. 20(6), 2010). CAKKT is strictly stronger than AKKT and is satisfied by the limit points of an augmented Lagrangian method under a weak Łojasiewicz-type hypothesis. The paper's §6.1 compares the associated weakest strict CQ, CAKKT-regularity, with Abadie's constraint qualification, one of the classical conditions of nonlinear programming. The answer is that CAKKT-regularity implies Abadie's CQ, and the converse fails.

Timeline:

• 1967: Abadie introduces the condition $L_\Omega(x^*)=T_\Omega(x^*)$.
• 1969: Guignard weakens it to equality of the polars.
• 1971: Gould and Tolle prove that Guignard's condition is the weakest CQ guaranteeing KKT at local minimizers.
• 2010: Andreani, Martínez and Svaiter introduce CAKKT.
• 2016: Andreani, Martínez, Ramos and Silva characterize the weakest strict CQ for AKKT, the cone continuity property (SIAM J. Optim. 26(1)).
• 2015/2018: the present paper defines CAKKT-regularity and proves Theorems 4.3 and 6.4.

Setting

Let $h_1,\dots,h_m,g_1,\dots,g_p:\mathbb R^n\to\mathbb R$ be continuously differentiable, and let

$$\Omega=\{x\in\mathbb R^n:\ h_i(x)=0\ (i\le m),\ g_j(x)\le 0\ (j\le p)\}.$$

For feasible $x^*$, $J(x^*)=\{j: g_j(x^*)=0\}$ is the set of active inequalities. The polar of a set $K$ is $K^\circ=\{v:\langle v,k\rangle\le 0\ \forall k\in K\}$.

• The tangent cone $T_\Omega(x^*)$ is the set of $d$ for which there are $t_k\downarrow 0$ and $d^k\to d$ with $x^*+t_kd^k\in\Omega$.
• The linearized cone is $L_\Omega(x^*)=\{d:\langle\nabla h_i(x^*),d\rangle=0\ \forall i,\ \langle\nabla g_j(x^*),d\rangle\le 0\ \forall j\in J(x^*)\}$.
• The regular normal cone $\widehat N_\Omega(z)$ is the set of $w$ with $\langle w,y-z\rangle\le o(\|y-z\|)$ for $y\in\Omega$.
• The limiting normal cone $N_\Omega(x^*)$ is the set of limits of $w^k\in\widehat N_\Omega(z^k)$ along $z^k\to x^*$ in $\Omega$.

Abadie's CQ holds at $x^*$ when $L_\Omega(x^*)=T_\Omega(x^*)$.

An objective $f$ satisfies CAKKT at $x^*$ if there are $x^k\to x^*$, $\lambda^k\in\mathbb R^m$ and $\mu^k\in\mathbb R^p_+$ with

$$\nabla f(x^k)+\sum_i\lambda_i^k\nabla h_i(x^k)+\sum_j\mu_j^k\nabla g_j(x^k)\to 0,\qquad \sum_i|\lambda_i^kh_i(x^k)|+\sum_j|\mu_j^kg_j(x^k)|\to 0.$$

For $x\in\mathbb R^n$ and $r\ge 0$, let $K_C(x,r)$ be the set of vectors $\sum_i\lambda_i\nabla h_i(x)+\sum_{j\in J(x^*)}\mu_j\nabla g_j(x)$ with $\mu\ge 0$ and $\sum_i|\lambda_ih_i(x)|+\sum_{j\in J(x^*)}|\mu_jg_j(x)|\le r$. The point $x^*$ is CAKKT-regular if $(x,r)\rightrightarrows K_C(x,r)$ is outer semicontinuous at $(x^*,0)$:

$$\limsup_{(x,r)\to(x^*,0)}K_C(x,r)\subseteq K_C(x^*,0).$$

Formalization targets

Goal: Theorem 6.4

$$x^*\in\Omega\ \text{CAKKT-regular}\quad\Longrightarrow\quad L_\Omega(x^*)=T_\Omega(x^*).$$

Milestones

The inclusion $T_\Omega(x^*)\subseteq L_\Omega(x^*)$ always holds, so the content of the goal is the reverse inclusion. The milestones are the statements the paper's proof uses, in attack order:

1. Lemma 6.1: every $y\in T_\Omega(\bar x)^\circ$ equals $-\nabla F(\bar x)$ for a $C^1$ function $F$ that has a strict global minimum over $\Omega$ at $\bar x$.
2. Lemma 6.2: such a $y$ is the limit of multiplier combinations $\omega^k$ at points $x^k\to\bar x$. The multipliers satisfy $\mu^k_j=c_k\max\{0,g_j(x^k)\}$, and the complementarity residual $r^k$ tends to $0$.
3. $\widehat N_S(z)=T_S(z)^\circ$ for every set $S$.
4. $T_\Omega(x^*)\subseteq L_\Omega(x^*)$.
5. $K_C(x^*,0)=L_\Omega(x^*)^\circ$.
6. Under CAKKT-regularity, $N_\Omega(x^*)\subseteq L_\Omega(x^*)^\circ$.
7. $N_S(z)^\circ\subseteq T_S(z)$ for closed $S$.

Companion: Theorem 4.3

$$x^*\ \text{CAKKT-regular}\iff\big(\forall f\in C^1:\ \text{CAKKT at }x^*\Rightarrow\text{KKT at }x^*\big),$$

with the equivalence of the two formulations (4.12)–(4.13) and (4.14)–(4.15) of CAKKT as a milestone.

Significance

Theorem 6.4 places CAKKT-regularity in the classical hierarchy. Every point at which CAKKT forces KKT for all objectives also satisfies Abadie's CQ, and therefore Guignard's. The paper's Example 6.1 shows that Abadie's CQ does not imply CAKKT-regularity. A convergence theorem for an algorithm that produces CAKKT sequences therefore cannot be stated under Abadie's CQ alone. Together with Theorem 4.3, this fixes exactly what a CAKKT-based method needs from the constraints.

The results are proved in the paper. None of them, and none of the variational-analysis facts they rest on, is formalized on Prove2Me, and Mathlib has no regular or limiting normal cones of nonconvex sets. The work is to formalize the paper's proof together with the parts of Rockafellar–Wets it cites: Theorem 6.11 (gradients of smooth functions as normals), Proposition 6.5, and Theorems 6.26 and 6.28(b). The last is Clarke's theorem that the regular tangent cone of a closed set is the polar of its limiting normal cone. These facts are reusable well beyond this mission.

Difficulty

The inclusion $T_\Omega\subseteq L_\Omega$ is elementary. The reverse inclusion cannot be obtained from CAKKT-regularity at $x^*$ alone, because CAKKT-regularity is a statement about multiplier combinations, which live on the polar side. The argument therefore has to pass through normal cones at points $x^k\ne x^*$ near $x^*$. At such points the active set may differ from $J(x^*)$, and the complementarity residual must be controlled uniformly. Returning from polars to cones requires the passage from the limiting normal cone to the tangent cone (milestone 7). That is a deep fact about closed sets in finite dimension; it is not a formal manipulation of cones. Equality of polars would only give Guignard's CQ.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), indices are Fin m and Fin p, and gradients are Mathlib's gradient. The objects are:

• Constraints. The constraints are a structure Constraints n m p of two index families. Every theorem assumes IsC1 (each $h_i$ and $g_j$ is $C^1$, the paper's standing hypothesis) and feasibility of $x^*$.
• KKT is the multiplier form, with $\mu\ge 0$ and $\mu_j=0$ off $J(x^*)$.
• Cones. The tangent cone uses positive scalars $t_k\to 0$ (Mathlib's tangentConeAt allows negative scalars and is not used). The regular normal cone is empty off the set. The limiting normal cone and outer semicontinuity use the sequential Painlevé–Kuratowski outer limit, and the outer limit in CAKKT-regularity is taken over pairs with $r\ge 0$.
• CAKKT includes $x^k\to x^*$. The page's (4.12)–(4.13) omit it, but p. 1 and (4.14)–(4.15) make it part of the condition.
• Sums over $J(x^*)$ are written over all indices, with the multipliers forced to $0$ off $J(x^*)$.
• Abadie's CQ is the equality of cones of p. 5. The proof's "$T_\Omega(x^*)=L_\Omega(x^*)^\circ$" is a misprint and is not copied.
• Closedness of $\Omega$ is not assumed; it follows from continuity.

The following would trivialize the goal and are excluded:

• a normal cone that is nonempty outside the set;
• the convex normal cone used for the nonconvex $\Omega$;
• KKT without the sign or complementarity conditions;
• for Theorem 4.3, an objective quantified outside the equivalence;
• Abadie's CQ weakened to equality of polars.

A complete development needs Clarke's tangent–normal polarity for closed sets in $\mathbb R^n$, the existence of $C^1$ functions realizing regular normals, and a penalty argument for Lemma 6.2. Proofs of the general variational-analysis milestones (3 and 7) are especially welcome, since they serve any mission on nonconvex constraint sets.

Selected references

• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015 (https://optimization-online.org/wp-content/uploads/2015/11/5197.pdf); Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
• R. Andreani, J. M. Martínez, B. F. Svaiter, A new sequential optimality condition for constrained optimization and algorithmic consequences, SIAM J. Optim. 20(6):3533–3554, 2010. https://doi.org/10.1137/090777189
• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• F. J. Gould, J. W. Tolle, A necessary and sufficient qualification for constrained optimization, SIAM J. Appl. Math. 20(2):164–172, 1971. https://doi.org/10.1137/0120021

Motivation

Many service systems must match jobs to servers whose quality is not known in advance: crowdsourcing platforms routing tasks to worker types, wireless schedulers assigning users to channels, and switches in data networks. The scheduler learns server quality only by trying servers, and every poor assignment lets work pile up. The natural performance measure is therefore not the cumulative reward loss of classical bandits but the queue-regret: the expected excess backlog compared with a genie that knows the best assignment.

Krishnasamy, Sen, Johari and Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach (Operations Research, 2021; arXiv:1604.06377), show that queue-regret has two regimes. In an early stage it grows like the regret of a bandit. In a late stage, once the queue regularly empties, past mistakes are forgotten at every empty instant and the queue-regret decays. This mission formalizes their upper bound for the late stage: a UCB scheduler with forced exploration, Q-UCB, has queue-regret of order $\log^3 t/t$.

Setting

A discrete-time switch has $U$ queues and $K\ge U$ servers. In every slot $t\ge1$, queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ and link $(u,k)$ offers a potential service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$, all independent and i.i.d. over slots. The scheduler picks a matching $\kappa(t)$, an injective assignment of a server $\kappa_u(t)$ to every queue, and queue $u$ evolves as

$$Q_u(t)=\big(Q_u(t-1)+A_u(t)-S_u(t)\big)^+,\qquad S_u(t)=R_{u\kappa_u(t)}(t).$$

The scheduler observes only past schedules and the services offered on scheduled links.

Write $\mu^*_u=\max_k\mu_{uk}$, $k^*_u$ for its maximizer, $\epsilon_u=\mu^*_u-\lambda_u$, and $\Delta=\min_{u,\,k\ne k^*_u}(\mu^*_u-\mu_{uk})$. Assumption 1: each queue has a unique best server and the best servers are distinct, so $k^*$ is the unique optimal matching. Assumption 2: $\epsilon_u>0$ for all $u$. The genie queue $Q^*_u$ always uses $k^*_u$. Assumption 3: the system starts from the stationary law of $Q^*$. The queue-regret is

$$\Psi_u(t)=\mathbb E\big[Q_u(t)-Q^*_u(t)\big].$$

Q-UCB (Algorithm 1) explores in slot $t$ with probability $\min\{1,3K\log^2t/t\}$, scheduling a uniformly random member of a fixed family $\mathcal X$ of $K$ matchings that together cover all $UK$ links. Otherwise it exploits: for each queue it picks the server with the largest index $\hat\mu_{uk}(t)+\sqrt{\log^2t/(2N_{uk}(t))}$, with $\hat\mu_{uk}$ the empirical mean and $N_{uk}$ the number of past assignments of link $(u,k)$, and schedules a matching closest in Hamming distance to these choices. Fix $\beta>1$ and set

$$w(t)=t^{1-1/\beta},\qquad v'_u(t)=\frac{6K}{\epsilon_u}w(t),\qquad v_u(t)=\frac{24}{\epsilon_u^2}\log t+\frac{60K}{\epsilon_u}\frac{v'_u(t)\log^2t}{t}.$$

Formalization targets

Goal: Theorem 5 for Q-UCB (p. 16)

For every $t\ge5800$ with $t\ge\exp\big(4/(\Delta^2(1-1/\beta)^3)\big)$, $w(t)/\log t\ge2/\epsilon_u$ and $v_u(t)+v'_u(t)\le t/2$,

$$\Psi_u(t)\le 6K\frac{v_u(t)\log^2t}{t}+\frac{24.004+UK}{6t^2}.$$

The constants are the paper's, stated exactly.

Milestones (§8.2, pp. 24–34)

• Lemma 10: the number of forced-exploration slots in a window exceeds $5\max(\log t,K(\log^3t_2-\log^3t_1))$ with probability at most $t^{-4}$. Over $[1,t]$ it exceeds $Kw(t)$ with probability at most $t^{-2K}$.
• Lemma 11: with probability at least $1-UK/(6t^3)$, no exploit slot in $(w(t),t]$ schedules a sub-optimal link (event $\mathcal E_1$).
• Lemma 12: pathwise, $Q_u(t)-Q^*_u(t)$ is at most the number of sub-optimal schedules since queue $u$ was last empty, at time $t-B_u(t)$.
• Lemmas 13–17: on $\mathcal E_1\cap\mathcal E_2$, a coarse queue bound $2Kw(t)$ (13), a first bound on the regenerative cycle (14), a maximal inequality for the arrival-minus-service walk (15), a refined polylogarithmic queue bound (16), and the refined cycle bound $B_u(t)\le v_u(t)$ (17), each failing with probability $O(t^{-3})$.

Significance

The theorem shows that a simple learning scheduler loses only $O(K\log^3t/(\epsilon_u^2t))$ in expected backlog in the late stage. Together with the paper's $\Omega(1/t)$ lower bound for consistent policies (Theorem 3), this places the optimal late-stage queue-regret within a polylogarithmic factor. The analysis method has two parts: a high-probability statement that the learner has locked onto the optimal matching, and a regenerative argument that converts it into a bound on queue length. It applies to other learning-in-queues problems in the same way.

All results are proved in the paper (§8.2). None of them has a machine-checked proof. The mission produces a formal model of the learning switch, including the algorithm with arbitrary tie-breaking, the coupled genie and the stationary start, and checks the explicit constants. These constants rely on numerical facts stated in the proofs, for example a positivity check for $x\ge\log5800$ in Lemma 10(b) and the absorption of lower-order terms into $24.004$, which a formal proof must verify.

Difficulty

The obvious argument says that UCB eventually identifies the best server, so the queue behaves like the genie's. This fails for two reasons. First, the regret is an expectation of a queue length, and a queue remembers every early mistake until it next empties. So one must bound the current regenerative cycle, and that bound itself depends on the queue length, which forces the recursion of Lemmas 13, 14, 16 and 17. Second, UCB's standard logarithmic-regret analysis bounds the expected number of sub-optimal pulls. It says nothing about whether a sub-optimal pull happens in a specific late window. Forced exploration at rate $\log^2t/t$ is what makes all indices concentrate at once, and Lemma 11 requires a union bound over every link, slot and sample count with explicit exponents.

Formalization scope

• Probability space. One canonical space: the initial queue vector together with an i.i.d. sequence of slot seeds, namely uniforms for arrivals, links and the explore coin, and a uniform explore index.
  • Arrivals and services are threshold events of the uniforms.
  • $Q(0)$ has the product geometric law $\mathbb P(Q_u(0)=n)=(1-\rho_u)\rho_u^n$ with $\rho_u=\lambda_u(1-\mu^*_u)/((1-\lambda_u)\mu^*_u)$, the stationary law of the genie chain under the printed recursion.
• Indexing and coupling. Queues and servers are Fin U and Fin K, and slots are $t\ge1$. The genie shares arrivals, services and $Q(0)$ with the system. This coupling is implicit in the paper's proofs and does not change $\Psi_u$.
• Algorithm. Q-UCB is formalized for every covering family $\mathcal X$ and every tie-breaking rule, deterministic in the slot and history, for the UCB argmax and the Hamming projection.
  • $N_{uk}(t)$ counts slots $1,\dots,t-1$.
  • An unsampled link has index $+\infty$.
  • $B_u(t)=t$ when queue $u$ never emptied on $[0,t]$.
• Disclosed additions.
  • $K\ge2$ in every statement; $K=1$ is trivial, and the constants fail there.
  • $t,t_1\ge1$ in Lemma 10(a).
  • $\log w(t)\ge(2\log t)^{2/3}$ in Lemma 10(b); the printed statement is false without it, and its proof uses it.
  • Lemmas 14 and 16 take the "arbitrary function" $v_u$ natural-valued.
• Excluded trivializations. Theorem 5 also asserts that $Q_u(t)-Q^*_u(t)$ is integrable, so $\Psi_u(t)$ cannot be a default value of a non-integrable integral. Every probability bound concerns the actual events, and every hypothesis set is satisfiable. For example, with $U=1$, $K=2$, $\lambda=0.5$, $\mu=(0.9,0.1)$, $\beta=2$, the range of Theorem 5 contains $t=\lceil e^{50}\rceil$.
• Out of scope. Theorem 5 and Lemma 11 for Q-ThS (Algorithm 2) are not formalized, and neither is Corollary 6.
• Infrastructure needed and welcome. Chernoff bounds for sums of independent non-identically distributed Bernoulli variables (Lemma 10), Hoeffding's inequality and a maximal suffix-sum bound (Lemmas 14, 15), measurability of the algorithm's trajectory in the seeds, and regenerative-cycle arguments for the reflected random walk. The Chernoff and stationary-queue lemmas are reusable well beyond this mission.

The source is the arXiv v4 preprint; the paper's proofs are in its §8 and §9.

Selected references

• S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021. Preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377 ; https://doi.org/10.1287/opre.2020.1995
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• M. J. Neely, Stochastic Network Optimization with Application to Communication and Queueing Systems, Morgan & Claypool, 2010. https://doi.org/10.2200/S00271ED1V01Y201006CNT007

Motivation

Large data centers and cloud platforms route each incoming job to one of $N$ parallel servers through a single dispatcher. The join-the-shortest-queue (JSQ) policy, which sends each job to a server with the fewest jobs, has strong optimality properties for identical exponential servers, but it needs the queue length of every server at every arrival, which is costly when $N$ is in the thousands. The power-of-$d$ scheme JSQ($d$) polls only $d$ servers chosen at random and joins the shortest among them. For fixed $d\ge2$ it improves dramatically over random routing, which is the supermarket model of Mitzenmacher and of Vvedenskaya, Dobrushin and Karpelevich, but it does not match JSQ.

Mukherjee, Borst, van Leeuwaarden and Whiting (arXiv:1612.00723, Stochastic Systems 2018) ask how fast $d=d(N)$ must grow for JSQ($d(N)$) to behave like JSQ in the large-$N$ limit. This mission concerns their fluid-scale answer: any growth $d(N)\to\infty$ suffices.

Timeline.

• 1996–2001: Vvedenskaya–Dobrushin–Karpelevich and Mitzenmacher derive the fluid limit of JSQ($d$) for fixed $d$ (the supermarket ODE).
• 2015–2018: Eschenfeldt and Gamarnik obtain the Halfin–Whitt diffusion limit of ordinary JSQ (arXiv:1502.00999).
• 2016–2018: Mukherjee et al. prove the first transient fluid limit of ordinary JSQ in $\ell_1$ (their Theorem 4.1). They show that JSQ($d(N)$) has the same fluid limit whenever $d(N)\to\infty$ (Theorem 2.1) and the same diffusion limit whenever $d(N)/(\sqrt N\log N)\to\infty$ (Theorem 2.4, a separate mission).

Setting

There are $N$ identical servers, each with a buffer of size $b\in\{1,2,\dots\}\cup\{\infty\}$ counting the job in service. Jobs arrive as a Poisson process of rate $\lambda(N)$ and need independent unit-mean exponential service. A job sent to a full server is discarded. The occupancy vector is $\mathbf Q(t)=(Q_1(t),Q_2(t),\dots)$, where $Q_i(t)$ is the number of servers with at least $i$ jobs, with the convention $Q_0\equiv N$. If the servers are listed in nondecreasing order of queue length, the $c$-th ordered server holds $I(c)=\max\{i\ge0:Q_i\ge N-c+1\}$ jobs. A dispatch scheme picks an ordered position $c\in\{1,\dots,N\}$ for each arrival, and the arrival raises $Q_{I(c)+1}$ by one (or is discarded if $I(c)=b$).

The schemes are:

• JSQ picks $c=1$;
• JSQ($d$) picks the lowest position among $d$ positions sampled uniformly without replacement, so JSQ($N$) is JSQ;
• MJSQ($n$) picks $c=n+1$;
• CJSQ($n$) is the class of all rules that pick some $c\le n+1$;
• JSQ($n,d$) keeps the JSQ($d$) choice when it is at most $n+1$ and otherwise picks uniformly among the first $n+1$ positions.

Two systems are S-coupled when they share the arrival clock and the departure clock of the $k$-th ordered server for every $k$.

The fluid-scaled state is $\mathbf q(t)=\mathbf Q(t)/N$. It lives in

$$\mathcal S=\Big\{\mathbf q\in[0,1]^b:\ q_i\le q_{i-1}\ (i\ge2),\ \sum_{i\ge1}q_i<\infty\Big\},$$

which carries the $\ell_1$ distance. For $\mathbf q\in\mathcal S$ let $m(\mathbf q)=\min\{i:q_{i+1}<1\}$. The coefficients $p_i(\mathbf q)$ of (4.4) send all incoming work to level $m(\mathbf q)-1$ while the rate $\lambda$ can be absorbed there, and the excess to level $m(\mathbf q)$: if $m(\mathbf q)=0$ then $p_0=1$; otherwise $p_{m-1}=\min\{(1-q_{m+1})/\lambda,1\}$, $p_m=1-p_{m-1}$, and all other $p_i$ vanish.

Formalization targets

Goal: Theorem 2.1

Assume $\lambda(N)/N\to\lambda<1$, $d(N)\to\infty$ and $\mathbf q^{d(N)}(0)\to\mathbf q^\infty$ in $\mathcal S$. Then every subsequence of $\{\mathbf q^{d(N)}(t)\}_{t\ge0}$ has a further subsequence converging weakly (Skorohod $J_1$) to a limit satisfying

$$q_i(t)=q^\infty_i+\lambda\int_0^t p_{i-1}(\mathbf q(s))\,ds-\int_0^t\big(q_i(s)-q_{i+1}(s)\big)\,ds,\qquad i=1,\dots,b. \tag{2.1}$$

The statement fixes no rate for $d(N)$, which is what makes it the right goal.

Milestones

The milestones follow the paper's proof.

• §3, coupling. Proposition 3.1 is a deterministic stack ordering. Proposition 3.2 and Corollary 3.3 sandwich any CJSQ($n$) scheme between JSQ and MJSQ($n$). Proposition 3.5 bounds the $\ell_1$ distance of two S-coupled systems by $2\Delta(t)$, and Proposition 3.6 bounds $\Delta$ for JSQ($d$) against JSQ($n,d$).
• §4.1, JSQ fluid limit. Proposition 4.3 makes the martingales negligible, Lemmas 4.6 and 4.7 characterize compactness and tightness in $\ell_1$, Lemma 4.8 gives level confinement, and Theorem 4.1 is the fluid limit of JSQ itself.
• §4.2. Proposition 4.9 is the reduction "JSQ fluid limit $\Rightarrow$ JSQ($d(N)$) fluid limit".

Significance

The result. Theorem 2.1 shows that on the fluid scale the optimality of JSQ costs nothing beyond $d(N)\to\infty$ queue inquiries per job, far fewer than $N$. In particular the fluid limit is the same as that of JSQ, which is fluid-optimal. The coupling framework of §3 (the class CJSQ($n$), stack orderings, S-coupling) is not tied to JSQ($d$). The paper uses the same tools for the diffusion-scale Theorem 2.4, for batch arrivals and for the interchange of limits, Proposition 2.2.

Formalizing it. Proofs of the paper's results exist; no machine-checked version does. The mission produces:

• a reusable model of many-server systems with ordered-position dispatch;
• a formal stack-ordering and S-coupling toolkit;
• compactness and tightness criteria for $\ell_1$-valued random sequences;
• a complete fluid-limit theorem for a load-balancing policy.

The proof of Theorem 4.1 in the paper is sketched in places (the time-scale separation is argued "analogously" to Hunt and Kurtz), so a formal proof would also settle those steps.

Difficulty

The obvious argument would compare JSQ($d(N)$) directly with JSQ: the two disagree whenever the $d(N)$ sampled servers miss every shortest queue. When a constant fraction of servers is idle this is rare, but when few servers share the minimum queue length the disagreement rate does not vanish, and a direct coupling fails. The paper instead passes through CJSQ($n(N)$) with $n(N)/N\to0$, which is close to JSQ($d(N)$) for a suitable $n(N)$ and sandwiched between JSQ and MJSQ($n(N)$).

The second difficulty is the topology. The sandwich controls tail sums $\sum_{i\ge m}Q_i$, so the fluid limit of JSQ is needed in $\ell_1$, not coordinatewise. With $b=\infty$ the state space is infinite-dimensional, and tightness requires uniform control of tails. Finally, the JSQ fluid limit itself involves a separation of time scales: the drift $p_i(\mathbf q)$ is discontinuous in $\mathbf q$ and arises as an averaged stationary behaviour of a fast process.

Formalization scope

• Occupancy. Occupancy vectors are finitely supported functions ℕ →₀ ℕ with the paper's level index; coordinate $0$ holds $Q_0=N$. The buffer is $b\in\mathbb N_\infty$ with $b\ge1$; both finite and infinite $b$ are covered.
• Construction. Systems are built by uniformization: a Poisson clock of rate $\lambda+N$ with i.i.d. Uniform$[0,1]$ marks. A mark decides arrival versus departure, the departure position, the random $d$-subset (sampling without replacement) and the uniform choice of JSQ($n,d$). S-coupled systems share the clock and the marks.
• Schemes. A scheme maps the event index, the current state and the current mark to a position. CJSQ($n$) rules must be measurable in the mark.
• Fluid states. Fluid states are functions ℕ → ℝ with $q_0=1$. $\mathcal S$ carries the $\ell_1$ distance, computed in $[0,\infty]$.
• Coefficients. $p_{m-1}$ is written as "$1$ if $\lambda\le1-q_{m+1}$, else $(1-q_{m+1})/\lambda$", which equals (4.4) for $\lambda>0$ and never divides by zero.
• Limit equation. A solution of (2.1) must take values in $\mathcal S$, have integrable integrands, and satisfy every equation $i=1,\dots,b$.
• Weak convergence. Weak $J_1$ convergence to a continuous limit is stated in coupling form: copies of the processes on one probability space converge almost surely uniformly on compacts in $\ell_1$. "Any subsequence has a further subsequence" asserts the existence of the limit.
• Initial states. Theorem 2.1 has deterministic initial states with $\ell_1$ convergence and allows $\lambda=0$. Theorem 4.1, Proposition 4.3 and Lemma 4.8 have random initial states converging in probability, and $\lambda>0$.
• Stochastic order. $\le_{st}$ for processes means the existence of an ordered coupling with the right path laws. Proposition 3.6's conditional probability is stated for each value of the integer $A(T)$.
• Correction. Proposition 3.1 as printed quantifies over $m\le b$. For finite $b$ the proof also needs the ordering of the discarded counts, $m=b+1$, and the formal statement orders every level $m\ge1$.

A formalization that states only "every limit point solves (2.1)", or that measures convergence coordinatewise, would be vacuous or weaker: it is ruled out by requiring the limit's existence and $\ell_1$ convergence.

Needed infrastructure. The development needs Poisson clocks and thinning, martingale bounds for counting processes, compactness in $\ell^1$, tightness and Prokhorov's theorem on Polish spaces, and the Skorohod representation. The $\ell_1$ compactness and tightness criteria (Lemmas 4.6, 4.7) and the stack ordering (Proposition 3.1) are reusable on their own. Proofs of any milestone are welcome, as are proofs of Theorem 2.1 that bypass Theorem 4.1.

Selected references

• 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(4), 2018. arXiv:1612.00723v2, https://arxiv.org/abs/1612.00723
• P. Eschenfeldt, D. Gamarnik, Join the Shortest Queue with Many Servers. The Heavy-Traffic Asymptotics, Mathematics of Operations Research 43(3), 2018. https://arxiv.org/abs/1502.00999
• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 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, Problems of Information Transmission 32(1), 1996.
• P. J. Hunt, T. G. Kurtz, Large Loss Networks, Stochastic Processes and their Applications 53(2), 1994. https://doi.org/10.1016/0304-4149(94)90063-9
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

Motivation

In the prophet inequality a gambler observes independent nonnegative random values $V_1,\dots,V_n$ with known laws one at a time and must decide irrevocably, after seeing each one, whether to stop and keep it. Her expected reward is compared with that of a prophet who knows all realizations and earns $\mathbb E(\max_i V_i)$. When the values arrive in a fixed adversarial order the best guarantee is $1/2$ (Krengel, Sucheston and Garling, 1977; Samuel-Cahn, 1984). Prophet inequalities are the stopping-theoretic core of posted-price mechanisms in online auctions, where a guarantee for the gambler translates into a welfare or revenue approximation for sequential pricing.

The prophet secretary problem keeps arbitrary independent laws but lets the values arrive in a uniformly random order, as in the secretary problem.

• 2015: Esfandiari, HajiAghayi, Liaghat and Monemizadeh introduce the problem and give a $1-1/e\approx0.632$ guarantee with $n$ time-dependent thresholds (ESA 2015).
• 2017: Ehsani, Hajiaghayi, Kesselheim and Singla obtain $1-1/e$ with a single threshold, using random tie-breaking (SODA 2018).
• 2018: Azar, Chiplunkar and Kaplan surpass $1-1/e$ by a small margin and give an upper bound of $11/15$ for deterministic distribution-insensitive algorithms (EC 2018).
• 2019: Correa, Saona and Ziliotto break $1-1/e$, proving $0.669$ with blind strategies, and show that no algorithm beats $\sqrt3-1$ (arXiv:1807.07483; Mathematical Programming, doi:10.1007/s10107-020-01544-8). This mission formalizes the $0.669$ guarantee.

Setting

An instance is a list of laws $F_1,\dots,F_n$ of independent nonnegative random variables $V_1,\dots,V_n$, all continuous. A uniformly random permutation $\sigma$ of $[n]=\{1,\dots,n\}$, independent of the values, is the arrival order: at time $j$ the gambler sees $V_{\sigma_j}$.

The time threshold algorithm $\mathrm{TTA}_{\tau_1,\dots,\tau_n}$ stops at the first time $j$ with $V_{\sigma_j}>\tau_j$. Its stopping time is $T=\inf\{j\in[n]:V_{\sigma_j}>\tau_j\}$ and the gambler's reward is $V_{\sigma_T}\mathbf 1_{T<\infty}$, written $V_{\sigma_T}$.

A blind strategy is a nonincreasing function $\alpha:[0,1]\to[0,1]$. Given an instance, draw $u_1,\dots,u_n$ independently and uniformly from $[0,1]$, let $u_{[j]}$ be the $j$-th smallest, and choose thresholds by

$$\mathbb P\big(\max_{i\in[n]}V_i\le\tau_j\big)=\alpha(u_{[j]}).$$

The strategy is called blind because $\alpha$ fixes the levels of the distribution of the maximum at which the gambler stops, independently of the instance and of $n$. The deterministic blind strategy (Definition 3.1) uses $\alpha(j/n)$ in place of $\alpha(u_{[j]})$. A piecewise-constant strategy $\alpha_{\alpha_1,\dots,\alpha_m}(x)=\sum_{j\in[m]}\alpha_j\mathbf 1_{[\frac{j-1}m,\frac jm)}(x)$ uses at most $m$ distinct levels.

Formalization targets

Goal: Theorem 1.1

There is a nonincreasing $\alpha:[0,1]\to[0,1]$ such that, for every $n$ and every continuous instance,

$$\mathbb E(V_{\sigma_T})\;\ge\;0.669\;\mathbb E\big(\max_{i\in[n]}V_i\big),$$

where $T$ is the stopping time of the blind strategy $\alpha$. One $\alpha$ serves every instance.

Milestones, in the order the proof uses them

1. §3, display after Definition 3.1: the blind strategy's value is the limit of the deterministic blind strategy's values on the instance padded with $m$ zeros, as $m\to\infty$.
2. Lemma 3.1: an exact formula for $\mathbb P(V_{\sigma_T}>t)$ for nonincreasing thresholds.
3. Lemma 3.3: $\frac1n\sum_{j\in[k]}(1-\alpha_j)\le\mathbb P(T\le k)\le1-(\prod_{j\le k}\alpha_j)^{1/n}$.
4. Lemma 4.1: $\mathbb P(T\ge k\mid\sigma_k=i)\ge\mathbb P(T>k)\big/\big(1-\frac kn+\frac1n\sum_{l\in[k]}\mathbb P(V_i\le\tau_l)\big)$.
5. Lemma 4.2: a weighted replacement of the union bound $\sum_i\mathbb P(V_i>t)\ge\mathbb P(\max_iV_i>t)$.
6. Lemma 4.3: for $\alpha=\alpha_{\alpha_1,\dots,\alpha_m}$ with $\alpha_m>0$, $\mathbb E(V_{\sigma_T})\ge\min_{j\in[m+1]}f_j(\alpha_1,\dots,\alpha_m)\,\mathbb E(\max_iV_i)$ for explicit functions $f_j$.
7. Corollary 4.4: some $1\ge\alpha_1\ge\dots\ge\alpha_m\ge0$ gives the constant $0.66975$; the paper reports that $m=30$ suffices.

Significance

Theorem 1.1 raised the guarantee for the prophet secretary problem from just above $1-1/e$ to $0.669$, and it separates random-order arrival from adversarial arrival by more than the classical single-threshold analysis. The strategies are distribution-insensitive in a precise sense: the gambler needs only the distribution of the maximum, not the individual laws, and $\alpha$ does not depend on $n$. The milestones are general facts about multi-threshold stopping in random order (Lemmas 3.1, 3.3, 4.1, 4.2) that apply to any nonincreasing thresholds, not only to blind ones.

The result is proved in the paper, with one numerical step: Corollary 4.4 evaluates the bound of Lemma 4.3 at a specific vector $(\alpha_1,\dots,\alpha_{30})$ found by optimization, which the paper does not print. No part of this argument has a machine-checked proof. The formalization would make the reduction from blind to deterministic strategies, the stopping-time estimates and the final numerical certificate explicit and checked. The paper also shows that no blind strategy guarantees more than $0.675$ (Theorem 1.2, outside this mission); any later improvement of the constant leaves this goal, which asserts only $0.669$, intact.

Difficulty

The obvious argument fixes a threshold and bounds the probability that some value exceeds it; with one threshold this cannot beat $1-1/e$, and with time-varying thresholds the events "the gambler has not stopped by time $k$" and "value $i$ arrives at time $k$" are dependent, because the arrival of $i$ at time $k$ removes $i$ from the earlier times. The union bound $\sum_i\mathbb P(V_i>t)\ge\mathbb P(\max_iV_i>t)$ loses exactly the constant one is trying to gain. The analysis must therefore bound the law of the stopping time uniformly over all instances (Lemma 3.3), sharpen the conditional survival probability (Lemma 4.1) and the union bound (Lemma 4.2), and then pass to the limit of large instances. The final constant depends on a numerical optimization over $m=30$ levels, so the closing step is a certified evaluation of an explicit but long expression involving $m$-th roots and logarithms.

Formalization scope

All statements import one definitions file, BlindProphetSec.Blind.Setting.

• Instances: μ : Fin n → Measure ℝ with IsProbabilityMeasure, NullSingletonClass (continuity, the paper's standing assumption of §1.2 and §3) and μ i (Set.Iio 0) = 0 (nonnegativity). Independence is built in: the values are the coordinates of Measure.pi μ. Indices and times are 0-based; the paper's time $j$ is j.val + 1.
• Random order: the average over all $n!$ permutations. A conditional probability $\mathbb P(\cdot\mid\sigma_k=i)$ is written $n\,\mathbb P(\cdot,\ \sigma_k=i)$.
• Expectations are lower Lebesgue integrals in $[0,\infty]$, so $\mathbb E(\max_iV_i)=\infty$ is allowed; the paper's ratios are stated multiplied out, $c\,\mathbb E(\max_iV_i)\le\mathbb E(V_{\sigma_T})$. The reward is $0$ if the gambler never stops.
• Thresholds of blind strategies are encoded through their levels: stop at time $j$ iff $\alpha(u_{[j]})<\mathbb P(\max_iV_i\le V_{\sigma_j})$. For continuous laws this agrees almost surely with $V_{\sigma_j}>\tau_j$ when the level is positive; level $1$ means "never stop", and at level $0$, where the paper's threshold is not unique, the encoding takes the largest threshold.
• Pinned hypotheses: $\mathbb E(\max_iV_i)<\infty$ in the §3 limit display; $t\ge0$ in Lemma 3.1 (the printed identity fails for $t<0$ because the reward is $0$ on $\{T=\infty\}$); $\alpha_1<1$ in Lemma 4.3, so that every term of $f_j$ is the paper's and none is a $0/0$ junk value.
• Generalizations: Lemmas 3.1, 4.1 and 4.2 are stated without continuity, and 4.1, 4.2 without nonnegativity, as printed.

A trivializing formalization is ruled out: the strategy $\alpha$ (and the vector $\alpha_1,\dots,\alpha_m$ of Corollary 4.4) is quantified before $n$ and the instance, the constants $0.669$ and $0.66975$ are exact rationals, and expectations cannot collapse to $0$ through non-integrability.

A complete development needs order statistics of uniform samples, exchangeability arguments for uniformly random permutations, convergence of the padded deterministic strategies, and a certified numerical evaluation of $f_j$. The random-order stopping vocabulary is reusable for other prophet secretary results, including the $\sqrt3-1$ upper bound of the companion mission. Contributions to any milestone, including partial results such as Lemma 3.2 ($\mathbb P(T\ge k\mid\sigma_k=i)\ge\mathbb P(T>k)$), are welcome. The PDF used is the arXiv preprint, version 2 (arXiv:1807.07483v2, 12 March 2019); all labels and pages refer to it.

Selected references

• J. Correa, R. Saona, B. Ziliotto, Prophet Secretary Through Blind Strategies, arXiv:1807.07483v2, 2019; Mathematical Programming, 2021. https://arxiv.org/abs/1807.07483, https://doi.org/10.1007/s10107-020-01544-8
• H. Esfandiari, M. Hajiaghayi, V. Liaghat, M. Monemizadeh, Prophet Secretary, Proceedings of ESA 2015, pp. 496–508.
• S. Ehsani, M. Hajiaghayi, T. Kesselheim, S. Singla, Prophet Secretary for Combinatorial Auctions and Matroids, Proceedings of SODA 2018, pp. 700–714.
• Y. Azar, A. Chiplunkar, H. Kaplan, Prophet Secretary: Surpassing the 1 − 1/e Barrier, Proceedings of EC 2018, pp. 303–318.
• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, The Annals of Probability 12(4), pp. 1213–1216.

Motivation

Stochastic dual dynamic programming (SDDP) and its relatives are the standard algorithms for multistage stochastic programs: hydro-thermal scheduling, energy storage and long-horizon capacity planning are solved with them in industry. They approximate each future cost function from below by a maximum of affine cuts, compute new cuts only at a few randomly chosen nodes of the scenario tree, and use the current approximations to simulate decisions forward. Whether such sampled cutting-plane schemes converge, and in what sense, decides whether their bounds can be trusted.

• Pereira and Pinto (1991) introduced SDDP for multistage stochastic linear programs.
• Chen and Powell (1999) proposed CUPPS, which samples a single scenario per iteration.
• Philpott and Guan (2008) proved almost-sure convergence in finitely many iterations of DOASA and SDDP-type methods for linear stage problems with stagewise independent data, using the finiteness of the set of possible cuts.
• Girardeau, Leclère and Philpott (2015) removed linearity: stage problems are convex with compact feasible sets, the data need not be stagewise independent, and the node selection is any τ-admissible random process. Convergence is then asymptotic, not finite.

This mission formalizes the stochastic part (§3) of the 2015 paper. Mission 1 of the series covers its deterministic part (§2).

Setting

A finite scenario tree has nodes $\mathcal N$, root $0$, parent map $p$, children $r(n)$, leaves $\mathcal L$, and node probabilities $\Phi_n>0$ with $\Phi_0=1$ and $\Phi_n=\sum_{m\in r(n)}\Phi_m$. Every node $m\neq0$ carries a control multifunction $\mathcal U_m:\mathbb R^d\rightrightarrows\mathbb R^p$, a cost $C_m(x,u)\in\mathbb R\cup\{+\infty\}$ and linear dynamics $x_m=f_m(x_{p(m)},u_m)$; every node carries a compact convex stock set $\mathcal X_n$; leaves carry final costs $V_m$. The future cost functions are defined backwards by (20):

$$V_n(x)=\sum_{m\in r(n)}\frac{\Phi_m}{\Phi_n}\min_{u\in\mathcal U_m(x)}\underbrace{C_m(x,u)+V_m\big(f_m(x,u)\big)}_{W_m(x,u)},\qquad x\in\mathcal X_n .$$

Assumptions $(H_2)$ ask for convex, lower semicontinuous, proper costs, convex compact-valued convex multifunctions $\mathcal U_m$, Lipschitz final costs, and an extended relatively complete recourse condition: feasibility and finite cost on a $\delta$-neighbourhood of every $\mathcal X_n$.

The algorithm keeps approximations $V^{k}_n$, starting from $V^{-1}_n\equiv-\infty$. At iteration $k$ it simulates the whole tree with $V^{k-1}$, producing stocks $x^k_n$ and controls $u^k_m$. Cuts $\theta^k_n+\langle\beta^k_n,\cdot-x^k_n\rangle$ are computed at the selected nodes by solving the stage problems (21) at their children and averaging optimal values and Lagrange multipliers with weights $\Phi_m/\Phi_n$. Every approximation is then updated by (22), $V^k_n=\max(V^{k-1}_n,\text{cut})$. The selections $y^k_n\in\{0,1\}$ form a random process. It is τ-admissible (Definition 1) when, inside each block of $\tau$ iterations, cuts are computed backwards along the tree, and when the block indicators $\tilde y^k_n=\max_{\kappa<\tau}y^{k\tau+\kappa}_n$ are i.i.d. in $k$, independent of the past, and equal to $1$ with positive probability.

Formalization targets

Goal: Theorem 3.1

Under $(H_2)$ and a τ-admissible selection process, almost surely, for every non-leaf node $n$ and every node $n$ respectively,

$$\lim_{k\to\infty}\sum_{m\in r(n)}\frac{\Phi_m}{\Phi_n}W_m\big(x^{k\tau}_n,u^{k\tau}_m\big)-V_n\big(x^{k\tau}_n\big)=0,\qquad \lim_{k\to\infty}V_n\big(x^{k\tau}_n\big)-V^{k\tau}_n\big(x^{k\tau}_n\big)=0 .$$

The decisions become optimal for the true problem and the approximations become exact at the visited stocks. Nothing is claimed about exactness elsewhere in the state space.

Milestones

• (26): every new cut is tight at the stock where it is computed.
• Lemma 3.1 (i)–(iii): the $V_n$ are convex and Lipschitz on $\mathcal X_n$; the approximations are lower bounds; finite approximations are uniformly Lipschitz.
• Lemma 3.2: exact approximations at the children make the decisions at a node asymptotically optimal.
• Lemma 5.3: under Definition 1 (i), a node selected inside a block is visited at the stock and with the approximation it had at the start of the block.
• Lemma 5.4: the terms of an i.i.d. sequence selected by a predictable rule are again i.i.d. with the same law.
• (32): exactness along the iterations at which a node is selected.

Significance

The theorem covers in one statement CUPPS (1-admissible), DOASA and SDDP ($(T-1)$-admissible), and many other sampling schemes, for stage problems that are convex rather than linear and for scenario trees without stagewise independence. It shows that the lower bound produced by these methods converges to the optimal value along the simulated trajectories.

The result is proved on paper. It is not formalized anywhere: no proof assistant library contains SDDP-type algorithms for convex stage problems. This mission makes the algorithm, the τ-admissibility notion and the convergence statement precise. Formalizing them corrects slips of the printed statements: the lower-bound property holds on the affine hull of $\mathcal X_n$ only, the boundedness of the cut slopes concerns finite cuts only, and the theorem's two limits concern different node sets. The rest of the work is the formalization of the published proof.

Difficulty

The deterministic argument (mission 1) shows exactness at stage $t$ from exactness at stage $t+1$ along the whole iteration sequence. In the stochastic case a node is updated only at the random iterations at which it is selected, while its stock $x^{k\tau}_n$ moves at every iteration. Exactness along the selected iterations (32) does not transfer to the others: a selection rule that updated a node only when its stock lay in a given region would leave the approximation inexact elsewhere. The proof has to show that the iterations at which the approximation is still $\varepsilon$-inexact are, by independence, selected with positive frequency. This requires the event "$k$ is $\varepsilon$-inexact" to be measurable with respect to the past selections, so the algorithm's choices among multiple minimisers and multipliers must be deterministic (footnote 6). It also requires the optional-skipping Lemma 5.4 and the strong law of large numbers. The first idea of conditioning on the stocks directly fails because the stocks depend on all past selections.

Formalization scope

• Spaces and values. Stocks in EuclideanSpace ℝ (Fin d), controls in EuclideanSpace ℝ (Fin p). Costs and value functions take values in EReal; convexity is epigraph convexity; $V_n=+\infty$ off $\mathcal X_n$; the initial approximation is $-\infty$. Limits are EReal limits, so convergence to $0$ forces the differences to be finite eventually.
• Tree. The platform definition StochasticProg.Multistage.Tree (a finite rooted tree with stages) is referenced; leaves, ascendents and node probabilities are defined on it. Costs are indexed by the child node as in (19a) and (20).
• Standing assumptions, all disclosed in the items: $(H_2)(1)$–$(6)$ clause by clause, with the full ball $B(\delta)$ of $(H_2)(6)$ as printed; $x_0\in\mathcal X_0$; $\Phi$ are node probabilities.
• Algorithm. A run is a predicate on the generated data (stocks, controls, cut values and slopes, approximations). Minimisers, Lagrange multipliers and subgradients are chosen by fixed rules, functions of the stage problem only (footnote 6), so a run is determined by its selection path. Lagrange multipliers of (21b) are encoded by the subgradient inequality of the optimal value of (21) on $\operatorname{Aff}(\mathcal X_n)$, with the multiplier in its direction space. The Lean index is shifted: Vc k is the paper's $V^{k-1}$.
• Selections. $y^k$ are measurable Bool-valued maps on a probability space; Definition 1 (i) holds on every path; (ii) is per node, i.i.d. in $k$ and independent of $\sigma(y^{k'}:k'<k\tau)$, with no independence across nodes.
• Ruling out trivializations. The goal's hypotheses are only $(H_2)$, the choice rules, a run on every sample path, measurable selections and τ-admissibility. The companion statement run_exists shows that runs exist for every selection path, and a sanity check shows $(H_2)$ and τ-admissibility are satisfiable, so the goal is not vacuous. Its conclusion mentions none of the proof's auxiliary objects.
• Infrastructure. The development needs marginal functions of convex problems over convex multifunctions, subdifferentiability of finite convex functions on affine hulls, Lipschitz bounds for maxima of affine functions, and the optional-skipping Lemma 5.4. Lemma 5.4 is a self-contained probability statement and is reusable on its own. Lemma 5.2 of the paper (a Dini-type lemma) is posed in mission 1. Proofs of any milestone, and of auxiliary lemmas on EReal-valued convex functions, are welcome.

Selected references

• P. Girardeau, V. Leclère, A. B. Philpott, On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs, Mathematics of Operations Research 40(1), 2015. https://doi.org/10.1287/moor.2014.0664 (author's version: https://hal.science/hal-01208295v1)
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4), 2008. https://doi.org/10.1016/j.orl.2008.01.013
• Z. L. Chen, W. B. Powell, Convergent cutting-plane and partial-sampling algorithm for multistage stochastic linear programs with recourse, Journal of Optimization Theory and Applications 102(3), pp. 497–524, 1999 (reference [1] of the paper).
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895