All missions

Motivation

Multistage stochastic programs model decisions taken over time while uncertain data are revealed: generation scheduling in hydro-thermal power systems, capacity expansion, unit commitment, portfolio management. When the uncertainty is represented by a finite scenario tree, the problem becomes one very large deterministic program, and decomposition algorithms solve it stage by stage. For linear problems the standard methods are nested Benders decomposition and its sampling variant, stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto (1991). Both rely on the convexity of the value functions, which they approximate from below by linear cuts.

Many applications need integer decisions (on/off status of generators, investment choices), and integer variables destroy convexity. Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observed that when the state variables passed between stages are binary, exact convex polyhedral representations still exist on the binary points. They proposed stochastic nested decomposition (SND) and its stage-wise independent special case SDDiP, and identified three properties of cuts (valid, tight, finite) under which the algorithms converge. This mission formalizes that convergence theorem, Theorem 2 of the paper.

Timeline. Birge (1985) gave nested decomposition for multistage linear programs; Pereira and Pinto (1991) introduced SDDP. Philpott and Guan (2008) proved almost sure finite convergence of SDDP-type methods for linear problems, and Girardeau, Leclère and Philpott (2015) extended convergence to convex problems. Zou, Ahmed and Sun (2019) proved finite convergence with probability one for mixed integer problems with binary states and abstract valid, tight and finite cuts, and showed that their Lagrangian cuts have the first two properties.

Setting

Let $\mathcal T$ be a scenario tree with stages $1,\dots,T$, root $1$, parent map $a(n)$ and children $\mathcal C(n)$. The nodes of the last stage are the scenarios. Node probabilities satisfy $p_n>0$, $p_1=1$, and $p_n=\sum_{m\in\mathcal C(n)}p_m$ before the last stage, and $q_{nm}=p_m/p_n$. Each node has a linear cost $f_n(x_n,y_n)$ and a nonempty compact mixed integer polyhedral set $X_n$ (assumption (A1)). The state $x_n\in\{0,1\}^d$ is binary, the local variables $y_n$ are general, and the root's parent state $\bar x_0$ is fixed. The problem in local-copy form (2.1) is

$$\min\sum_{n\in\mathcal T}p_nf_n(x_n,y_n)\quad\text{s.t.}\quad(z_n,x_n,y_n)\in X_n,\ z_n=x_{a(n)},\ x_n\in\{0,1\}^d .$$

Its value functions satisfy the recursion (2.3): $Q_n(x_{a(n)})=\min\{f_n(x_n,y_n)+\mathcal Q_n(x_n)\}$ over the nodal feasible set, with the expected cost-to-go function $\mathcal Q_n(x)=\sum_{m\in\mathcal C(n)}q_{nm}Q_m(x)$.

The SND algorithm keeps an under-approximation $\psi^i_n$ of each $\mathcal Q_n$: the maximum of a lower bound $L_n$ and the aggregated cuts $\sum_{m\in\mathcal C(n)}q_{nm}(v^\ell_m+(\pi^\ell_m)^\top x)$ collected so far (3.2). Each iteration $i$ samples $M$ scenarios with replacement. In the forward step it solves the nodal problems $P^i_n(x^i_{a(n)},\psi^i_n)$ from the root down, which yields the forward tree solution $\{(x^i_n,y^i_n)\}$ of (3.6). In the backward step, at every sampled node it generates one cut per child at the state $x^i_n$ and adds their aggregate to $\psi_n$. Cuts are valid if $Q_m(x)\ge v^i_m+(\pi^i_m)^\top x$ on $\{0,1\}^d$ (3.4). They are tight if they equal the value $\underline Q^i_m(x^i_n,\psi^{i+1}_m)$ of the child's updated nodal problem at $x^i_n$ (3.5). They are finite if only finitely many distinct cuts occur. Assumption (A3) requires the nodal solver to return the same optimal solution whenever it is given the same problem.

Formalization targets

Goal: Theorem 2 (p. 474)

With sampling with replacement, valid, tight and finite cuts, and a solver satisfying (A3), the following holds with probability one:

$$\exists\, i_0\ \ \forall i\ge i_0:\quad \{(x^i_n,y^i_n)\}_{n\in\mathcal T}\ \text{is an optimal solution of (2.1)}.$$

Milestones, in the order the proof uses them

1. Valid cuts give under-approximations, $\psi^i_n\le\mathcal Q_n$ and $\underline Q^i_n\le Q_n$ (proof of Claim 1, p. 475).
2. Claim 1: if $\psi^i_n(x^i_n)=\mathcal Q_n(x^i_n)$ for all $n$, the forward solution is optimal for (2.1) (p. 475).
3. With finitely many possible cuts, the approximations $\{\psi^i_n\}$ change only in finitely many iterations (pp. 474–475).
4. (3.8a)–(3.8f): a sampled node whose children are exact becomes exact after its backward step (p. 476).
5. Under sampling with replacement, every scenario is sampled in infinitely many iterations, almost surely (p. 476).
6. Claim 2: almost surely, no infinite block of unchanged approximations has a non-optimal forward solution (p. 475).

Significance

Theorem 2 separates the convergence of nested decomposition from the choice of cuts. Any cut family with the three properties yields an exact algorithm for multistage stochastic integer programs with binary states. The paper verifies the properties for integer optimality cuts and, through its Theorem 3, shows that Lagrangian cuts from the local-copy reformulation are valid and tight. The convergence of SDDiP, the variant used in computations, follows from the same theorem, and binary expansion of general integer states extends the reach to mixed integer state spaces.

The result is proved in the paper; no machine-checked proof exists. A formal development would turn its informal points into checked statements: that the minima are attained, that the DP recursion is equivalent to the extensive form, and that the finiteness of cuts is global. It would also supply a reusable framework (scenario trees with node probabilities, cut-based approximations, sampled runs) for the convergence theory of SDDP-type methods.

Difficulty

No single step is deep; the difficulty is the interaction of the pieces. A tempting argument says the approximations stop changing, so the algorithm stops at an optimum. But a stalled run need not be optimal: if a node at which $\psi_n$ is inexact is never sampled again, nothing changes and the forward solution stays suboptimal. The proof must therefore combine three things: the deterministic finiteness of changes, an almost sure statement about sampling, and the exactness chain (3.8). That chain depends on tightness with respect to the updated approximation of the child, and it fails if tightness refers to the approximation from before the backward step. The equivalence between optimality for the DP recursion and for the extensive form (2.1), used without proof in Claim 1, also requires a backward induction over the tree.

Formalization scope

The tree is the platform definition StochasticProg.Multistage.Tree H, with stage $t$ of the paper equal to stage = t − 1. Binary vectors are Fin d → Bool, embedded in $\mathbb R^d$. The copy variable $z_n$ is eliminated through $z_n=x_{a(n)}$. Minima are written as infima over sets that the standing assumptions make nonempty, bounded below and attained. Lean iterations are numbered from $0$, and the run is infinite (stopping criteria and bounds play no role).

Readings of informal words. "Optimal solution of (2.1)" means a feasible tree solution of least cost $\sum_np_nf_n$ among all feasible tree solutions. "After a finite number of iterations" means from some iteration on, in every iteration (∀ᶠ i in atTop). "With probability one" refers to a probability space carrying independent draws, $M\ge1$ per iteration, each with law $\{p_n:n\in S_T\}$. "Finite" cuts means one finite set for the whole run, as the proof uses it, not a different finite set per iteration. (A3) means the solver is a function of the node, the parent state and the approximation, and returns an optimal solution.

Added hypotheses, which the paper uses without stating them: $p_n>0$; every nodal problem is feasible for every binary parent state, which replaces (A2) (not used by Theorem 2); and the lower bounds under-estimate, $L_n\le\mathcal Q_n$, which is Algorithm 1's "initial under-approximation".

Trivializing formalizations are ruled out: tightness refers to the child's approximation after its own update, optimality is for the true extensive form and not relative to $\psi$, and the probability statement is over independent sampling, not over a fixed sample sequence assumed to visit every scenario.

Contributions welcome: the attainment lemmas for nodal minima, the DP/extensive-form equivalence on trees, and the second Borel–Cantelli argument for repeated sampling. All of these are reusable for other SDDP-type convergence results.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36 (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40 (2015) 130–145. https://doi.org/10.1287/moor.2014.0664
• J. R. Birge, Decomposition and partitioning methods for multistage stochastic linear programs, Oper. Res. 33 (1985) 989–1007. https://doi.org/10.1287/opre.33.5.989

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.