Operations Research

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

Motivation

In distributed optimization a network of $m$ agents minimizes a sum of private functions while each agent talks only to its neighbours. Applications include federated and decentralized learning, sensor networks and multi-robot systems, where the data cannot be pooled at one site. Many of these networks are directed (communication links are one-way, for instance because transmission powers differ) and time-varying (links come and go). On such networks no doubly stochastic mixing matrix is available in general, and plain averaging drifts toward a weighted average instead of the true one. The push-sum protocol corrects this drift by carrying an auxiliary weight $\phi_i$ at every agent (Kempe, Dobra & Gehrke 2003; Nedić & Olshevsky 2015).

Y. Sun, A. Daneshmand and G. Scutari (arXiv:1905.02637v2) analyse SONATA, a gradient-tracking method in which each agent solves a strongly convex surrogate of its local problem instead of taking a gradient step, for composite problems (a convex, possibly nonsmooth regulariser $G$ and a convex constraint set). They prove linear convergence on undirected graphs (their Theorem 3.9, the companion mission of this series) and, in Section 4, for a push-sum version over time-varying digraphs (Theorem 4.5). This mission formalizes the second result.

Timeline. Gradient tracking with push-sum over time-varying digraphs appears in NEXT/SONATA (Di Lorenzo & Scutari 2016; Scutari & Sun 2019), where convergence was proved without rates for nonconvex problems. Linear rates for smooth unconstrained strongly convex problems over time-varying digraphs were obtained for Push-DIGing (Nedić, Olshevsky & Shi 2017). Sun, Daneshmand and Scutari (2019, revised 2020) extend the linear rate to the composite, constrained setting with surrogates, and require only the average $F$, not every $f_i$, to be strongly convex.

Setting

Problem (P). Agent $i\in[m]$ holds $f_i:\mathbb R^d\to\mathbb R$; the agents solve

$$\min_{x\in\mathcal K}U(x)\triangleq F(x)+G(x),\qquad F=\frac1m\sum_{i=1}^mf_i .$$

Assumption A: $\mathcal K$ is nonempty, closed and convex; each $f_i$ is twice differentiable on an open set $\mathcal O\supseteq\mathcal K$ and convex; $\mu I\preceq\nabla^2F(x)\preceq LI$ on $\mathcal K$ with $\mu>0$; $G$ is convex on $\mathcal K$. $x^\star$ is the solution and $U^\star=U(x^\star)$.

Surrogates (Assumption C). Each agent has $\tilde f_i(x;z)$, $C^2$ on $\mathcal O\times\mathcal O$, with $\nabla\tilde f_i(x;x)=\nabla f_i(x)$, $\nabla\tilde f_i(\cdot;x)$ $\tilde L_i$-Lipschitz and $\tilde f_i(\cdot;x)$ $\tilde\mu_i$-strongly convex on $\mathcal K$. Constants $D^\ell_i\le D^u_i$ satisfy $D^\ell_iI\preceq\nabla^2\tilde f_i(x;y)-\nabla^2F(x)\preceq D^u_iI$ on $\mathcal K\times\mathcal K$ (15); $\tilde\mu_{\rm mn}=\min_i\tilde\mu_i$, $D^\ell_{\rm mn}=\min_iD^\ell_i$.

Network (Assumption B′). At time $\nu$ the digraph $\mathcal G^\nu$ has edge set $\mathcal E^\nu$; $(i,j)\in\mathcal E^\nu$ is a link from $i$ to $j$. There is an integer $B>0$ such that the union of the edge sets over every window $[\nu B,(\nu+1)B-1]$ is strongly connected.

Weights (Assumption E). $C^\nu=(c^\nu_{ij})$ is column stochastic, $c^\nu_{ii}\ge c_\ell>0$, $c^\nu_{ij}\ge c_\ell$ if $(j,i)\in\mathcal E^\nu$ and $c^\nu_{ij}=0$ for other $j\ne i$.

Algorithm 3. From $x_i^0\in\mathcal K$, $y_i^0=\nabla f_i(x_i^0)$, $\phi_i^0=1$, each agent computes

$$\hat x_i^\nu\in\operatorname*{argmin}_{x_i\in\mathcal K}\ \tilde f_i(x_i;x_i^\nu)+(y_i^\nu-\nabla f_i(x_i^\nu))^\top(x_i-x_i^\nu)+G(x_i),\qquad x_i^{\nu+1/2}=x_i^\nu+\alpha(\hat x_i^\nu-x_i^\nu),$$

then $\phi_i^{\nu+1}=\sum_jc^\nu_{ij}\phi_j^\nu$, $x_i^{\nu+1}=\frac1{\phi_i^{\nu+1}}\sum_jc^\nu_{ij}\phi_j^\nu x_j^{\nu+1/2}$ and $y_i^{\nu+1}=\frac1{\phi_i^{\nu+1}}\sum_jc^\nu_{ij}(\phi_j^\nu y_j^\nu+\nabla f_j(x_j^{\nu+1})-\nabla f_j(x_j^\nu))$.

The analysis uses the weighted gap $p_\phi^\nu=\sum_i\phi_i^\nu(U(x_i^\nu)-U^\star)$, the tracking error $\delta_i^\nu=\nabla F(x_i^\nu)-y_i^\nu$, and the consensus errors $x^\nu_{\phi,\perp}$, $y^\nu_{\phi,\perp}$ measured against the $\phi$-weighted averages.

Formalization targets

Goal: Theorem 4.5

If $\tilde\mu_{\rm mn}\ge D^\ell_{\rm mn}$, there is $\bar\alpha\in(0,1]$ such that for every $\alpha\in(0,\bar\alpha)$, every run and every agent $i$,

$$\exists\,C,\ z\in[0,1):\qquad|U(x_i^\nu)-U^\star|\le C\,z^\nu\quad\forall\nu .$$

The goal is qualitative: neither $\bar\alpha$ nor the rate is fixed, so it survives any improvement of the constants.

Milestones

In attack order: the weighted tracking identity (74) and its consequence $\bar y^\nu_\phi=\overline{\nabla f}^\nu$; the bounds $\phi_{lb}\le\phi_i^\nu\le\phi_{ub}$ (p. 29); the per-agent descent inequality (Lemma I.1); the lower bound on the weighted step length (Lemma I.2); the tracking-error bound $\|\delta^\nu\|^2\le8L^2_{\rm mx}\|x^\nu_{\phi,\perp}\|^2+2\|y^\nu_{\phi,\perp}\|^2$ (Lemma I.3); the contraction $p_\phi^{\nu+1}\le\sigma(\alpha)p_\phi^\nu+\eta(\alpha)\phi_{ub}(\cdots)$ (Proposition 4.1); the bound of $\|d^\nu\|^2$ by $p_\phi^\nu$ and $\|y^\nu_{\phi,\perp}\|^2$ (Proposition 4.3).

Significance

Theorem 4.5 gives a linear rate for distributed composite and constrained optimization over time-varying directed networks. Two features matter: the individual $f_i$ need not be strongly convex, and the surrogates cover proximal-gradient steps, DANE-type local solves and mirror-descent steps under one analysis. The rate depends on the surrogate-mismatch constants $D_i$, which is the mechanism by which the paper shows that local computation helps when the $f_i$ are similar.

The result is proved in the paper; the proof of Theorem 4.5 refers to the undirected argument, and several of its supporting statements (Propositions 4.1 and 4.3) have their proofs omitted or relegated to the supplement, with consensus estimates quoted from Scutari & Sun (2019). To our knowledge none of it is machine-checked. A formalization produces a checked proof of the directed result together with reusable statements about push-sum weights over $B$-strongly connected digraphs.

Difficulty

The obvious argument is to repeat the undirected proof with weighted averages. Two steps fail. First, the $\phi$-weighted average is not the minimiser of $\sum_i\|x_i-c\|^2$, so consensus errors measured against it lose a constant (the 8 in Lemma I.3 instead of 4), and every passage between weighted and unweighted sums needs the bounds $\phi_{lb}\le\phi_i^\nu\le\phi_{ub}$, which rest on a product-of-matrices argument over windows of length $(m-1)B$. Second, the matrices change with $\nu$, so there is no single contraction factor; geometric decay of the consensus errors holds only over windows, and the coupling between the optimality gap, the consensus errors and the step lengths must be closed by a small-gain argument whose constants are uniform over the run. The step-size threshold must not depend on the starting point.

Formalization scope

Points are EuclideanSpace ℝ (Fin d); stacked vectors are Fin m → ℝ^d with the Euclidean norm $\|v\|^2=\sum_i\|v_i\|^2$, never Lean's sup norm. The Hessian is the derivative of the gradient, and Loewner bounds are quadratic-form inequalities. Time is 0-based. A run is a relational predicate: $\hat x_i^\nu$ is some minimizer of the subproblem, whose existence the paper takes for granted; $x^\star$ is assumed to exist. The divisions by $\phi_i^{\nu+1}$ appear as in the paper and are genuine, since Assumption E keeps the weights positive. $f_i$ is convex on $\mathcal K$ and locally convex on $\mathcal O$ (positive semidefinite Hessian; $\mathcal O$ need not be convex), $\tilde\mu_i>0$, and $D^\ell_i,D^u_i$ are parameters: the statements hold for every valid choice. The graph sequence, $B$, $c_\ell$ and the matrices $C^\nu$ come before $\bar\alpha$; the starting point and the run come after $\alpha$. The bounds on $\phi$ are stated for $m\ge2$ (the printed $\phi_{ub}$ is $0$ at $m=1$), and positivity of $\sigma(\alpha)$ is claimed only when $D_{\rm mx}>0$ or $\alpha<1$.

The following do not count as a formalization of the goal: an unsatisfiable run predicate (a sorry-free verification file exhibits a run satisfying every hypothesis), a $\bar\alpha$ chosen after the run, the $\phi$ bounds or a contraction factor assumed in place of Assumptions B′ and E, and dropping the $1/\phi_i^{\nu+1}$ normalisation.

Not posed: the explicit rate (Theorem III.1), the complexity corollaries, and the consensus estimates Lemma 4.2 and Proposition 4.4, whose constants $c_0,\rho_B$ come from Scutari & Sun (2019) (as printed, $c_0$ is negative). A complete development needs Taylor expansions with integral remainder along segments, first-order optimality for composite problems on convex sets, and products of column-stochastic matrices over strongly connected windows; the last is reusable for any push-sum method. Contributions to any milestone, and to the missing consensus estimates as auxiliary lemmas, are welcome.

Selected references

• Y. Sun, A. Daneshmand, G. Scutari, Distributed Optimization Based on Gradient-tracking Revisited: Enhancing Convergence Rate via Surrogation, arXiv:1905.02637v2, 2020; SIAM J. Optim. 32(2), 2022. https://arxiv.org/abs/1905.02637v2
• G. Scutari, Y. Sun, Distributed nonconvex constrained optimization over time-varying digraphs, Math. Program. 176, 2019. https://doi.org/10.1007/s10107-018-01357-w
• P. Di Lorenzo, G. Scutari, NEXT: In-Network Nonconvex Optimization, IEEE Trans. Signal Inf. Process. Netw. 2(2), 2016. https://doi.org/10.1109/TSIPN.2016.2524588
• A. Nedić, A. Olshevsky, W. Shi, Achieving Geometric Convergence for Distributed Optimization over Time-Varying Graphs, SIAM J. Optim. 27(4), 2017. https://doi.org/10.1137/16M1084316
• A. Nedić, A. Olshevsky, Distributed optimization over time-varying directed graphs, IEEE Trans. Autom. Control 60(3), 2015. https://doi.org/10.1109/TAC.2014.2364096
• D. Kempe, A. Dobra, J. Gehrke, Gossip-based computation of aggregate information, FOCS 2003. https://doi.org/10.1109/SFCS.2003.1238221

Motivation

Hotel rooms, rental cars, cloud servers, operating rooms and rental equipment are reusable resources: a customer occupies capacity for a fixed service time, and the capacity returns to the firm afterwards. Many of these settings also allow advance reservation, where a request made today is for a service that starts later. Lei and Jasin study dynamic pricing in this setting. Prices are posted period by period, demand is non-stationary, and the firm wants revenue close to the best achievable while never booking more units than it owns.

Classical network revenue management, where capacity is sold once and never returns, has an extensive asymptotic theory. In that literature, controls that re-solve or adjust a fluid (deterministic) plan are known to lose a vanishing fraction of the optimal revenue as demand and capacity grow (Gallego and van Ryzin 1997; Jasin 2014). Reusable resources break the standard argument, because each sale removes capacity for a window of time and not for the rest of the horizon. Lei and Jasin give the first control for reusable resources with non-stationary arrivals, deterministic service times and advance reservation whose average loss is $o(\theta^{-1/2})$ in the scale parameter $\theta$ (Lei and Jasin, Operations Research 2020).

Setting

A firm manages $I$ resource types with integer capacities $C_i \ge 1$ and sells $K \ge 1$ service types over periods $t = 1, \dots, T$. At most one request arrives per period. A type-$k$ request made at the beginning of period $t$ uses $a_{ik} \in \{0,1\}$ units of resource $i$ during periods $t+\ell_k, \dots, t+\ell_k+n_k-1$. Here $n_k$ is the service time and $\ell_k$ the reservation lead time.

In each period the firm chooses a demand-rate vector $\lambda^t \in \Omega_\lambda = [0,\lambda_U]^K$, which is equivalent to choosing prices. A type-$k$ request then arrives with probability $\lambda^t_k$, independently of the past given $\lambda^t$, and the expected revenue rate is $r^t(\lambda^t)$. The deterministic relaxation DET-H maximizes $\sum_{t=1}^T r^t(\lambda^t)$ over $\lambda^t \in \Omega_\lambda$, subject to

$$\sum_{k=1}^K \sum_{s \,:\, s+\ell_k \le t \le s+\ell_k+n_k-1} a_{ik}\lambda^s_k \le C_i \qquad \text{for every resource } i \text{ and period } t \le T.$$

Its optimal value $J^D_H$ bounds the optimal expected revenue, and the average loss of a control $\pi$ is $\mathcal{L}(\pi) = (J^D_H - \mathbf{E}[R^\pi])/T$. Let $\lambda^D$ be an optimal solution of DET-H. The quantity $\underline{n}_k$ is the smallest number of periods with $\lambda^{t,D}_k > 0$ inside any service cycle of type $k$ that carries positive demand.

The control DPC-B$(m,\epsilon)$ splits the horizon, for each type $k$, into adjacent batches $\mathcal{T}_k^b$, each with $m_k$ positive-rate periods. In period $t$ it posts

$$\lambda^t_k = \mathrm{Proj}_{[0,\lambda_U]}\Bigl[\lambda^{t,D}_k - \Bigl(\frac{\epsilon_k}{\underline{n}_k} + \frac{1}{m_k}\sum_{s \in \mathcal{T}_k^{\beta_k(t)-1}} (D^s_k - \lambda^s_k)\Bigr)\mathbf{1}\{\lambda^{t,D}_k > 0\}\Bigr],$$

where $\beta_k(t)$ is the batch containing $t$. The rate is set to $0$ when fewer than $a_{ik}$ units of some resource $i$ are free at the service start $t+\ell_k$. The buffer $\epsilon_k$ protects capacity, and the batch term corrects for the demand surprises of the previous batch.

Formalization targets

Goal: Theorem 3, display (8)

There is a constant $M_3>0$, depending only on $K$, the curvature constant $\Psi$ of Assumption A5 and a bound $R$ on $|r^t|$, such that for every instance, every valid batch partition with $m_k \le \underline{n}_k$ and every $\epsilon_k$ in the stated range,

$$\mathcal{L}(\text{DPC-B}(m,\epsilon)) \le M_3 \sum_{k=1}^K \Bigl[\frac{\epsilon_k}{\underline{n}_k} + \frac{1}{m_k} + \frac{T}{m_k}\exp\Bigl\{-\frac{(\min_j\epsilon_j-1)^2}{256K^2\min\{\max_i C_i, m_k\}}\Bigr\}\Bigr].$$

The constant is uniform in $T$, $C$, $n_k$, $\ell_k$, $m_k$ and $\epsilon_k$, which is what makes the bound informative.

Milestones

1. Lemma EC.3: on the good event $\mathcal{G}(\epsilon,m,\delta)$, the free capacity satisfies $C^t \succeq e$ and the corrected rates stay inside $(0,\lambda_U)$.
2. (EC.22): on $\mathcal{G}$, the posted rate equals the unprojected corrected rate.
3. Lemma EC.4, as proved in (EC.23): $\mathbf{P}(\bar{\mathcal{G}}) \le \sum_k \frac{4T}{m_k}\exp\{\min\{\max_i C_i, m_k\}\gamma_k^2 - \frac{\min_j\epsilon_j-1}{8K}\gamma_k\}$ for all $\gamma_k \in (0,1]$.
4. $\mathbf{E}[(\sum_{s\in\mathcal{T}_k^b}\Delta^s_k)^2] \le m_k$ for every batch.
5. $\mathbf{E}([\nabla r^t(\lambda^{t,D})]^\top(\eta^t_\delta\odot\eta^t_e)) = 0$.

A companion item states Lemma 2 in this setting: stretching $\lambda^D$ in time solves DET-H for the $\theta$-th system of display (7).

Significance

Along the scaling (7), Theorem 3 with $m_k \approx \underline{n}_k^{2/3}$ gives an average loss of $O(\theta^{-2/3}\log^{1/2}\theta)$. The non-adaptive control DPC of the same paper achieves $O(\theta^{-1/2}\log^{1/2}\theta)$ (its Theorem 1). The result shows that batch-level feedback improves on the square-root barrier for reusable resources, and it does so with heterogeneous service times and advance reservation, which cover car rental and hotel bookings.

Theorem 3 and its lemmas are proved in the paper's e-companion. No machine-checked proof of them, and no formal model of reusable-resource revenue management, is known. The mission produces a Lean model of the setting: capacity windows with lead times, the availability table $\tilde C(t,s)$, an adapted control on finite sample paths, and its exact path law. On top of that model it states the paper's main bound in full. Several printed steps need repair (see the scope section), so a formal proof would also settle the exact constants.

Difficulty

The obvious route bounds each period's loss by a Taylor expansion around $\lambda^{t,D}$ and controls the deviations by a martingale inequality. That route needs the control to coincide with the unprojected corrected rate for the whole horizon, that is, no capacity shortfall and no clipping. Capacity is a moving window of overlapping services with different lengths and lead times, so a shortfall at one period depends on requests made up to $n_k+\ell_k$ periods earlier, in other batches and other types. The batch correction makes the rates depend on past errors, so the errors are martingale differences, not independent variables. The concentration bound must hold uniformly over batches whose number grows with $T$, with a variance proxy $\min\{\max_i C_i, m_k\}$ that is not the batch length. The early periods, before any service of type $k$ has completed, need a separate threshold (the two cases of (EC.17)).

Formalization scope

All objects are defined in the namespace ReusablePricing.DPCB. The conventions are fixed as follows.

• Periods are $1,\dots,T$. A sample path is a function Fin T → Option (Fin K), recording no request or one request of a type in each period. Expectations are finite sums against the exact path law: the product over periods of the one-period law, whose probabilities are the rates posted given the past. The demand law is never left as a hypothesis.
• Decisions are rates. A turn-off is rate $0$. Prices and A1–A3 do not appear. The bound $R$ on $|r^t|$ over $\Omega_\lambda$ replaces the proofs' $r^u$. $K\lambda_U \le 1$ is assumed, as implied by at most one request per period.
• Capacity windows are empty for $t \le \ell_k$. $C^t = \tilde C(t,t)$, and $\tilde C$ is defined by its defining sentence on p. 18, not by the update rule of Step 2a, whose indices do not match its own explanation. Admission is tested for services starting within the horizon.
• $\underline{n}$ in (EC.17) is $\min_k\underline{n}_k$. The events of (EC.16) are read over the batches $\mathcal{T}_k^b$. Statements "on $\mathcal{G}$" are made on paths of positive probability.
• Lemma EC.4 is stated with the $8K$ that its proof establishes, not the printed $4K$.
• Goal statements carry every standing hypothesis of Section 6: optimality of $\lambda^D$, the convention $\lambda^{t,D}_k\in\{0\}\cup(0,\lambda_U)$, A4, A5, and the existence of a demand-carrying cycle for every type, which $\underline{n}_k$ presupposes. The sanity check exhibits instances, with and without lead time, where all hypotheses of Theorem 3 hold and the $\epsilon$-range is nonempty.

The constant $M_3$ is quantified before the instance, after only $K$, $\Psi$ and $R$. Choosing it after the instance would make the bound trivial, because the loss never exceeds $2R$.

A complete development needs Freedman- or Doob-type inequalities for bounded martingale differences on finite path spaces, second-order Taylor bounds for $C^2$ functions on boxes in $\mathbb{R}^K$, and window-counting lemmas for capacity. The first two are reusable well beyond this mission. Contributions of any of the milestones, of general martingale tools for finite adapted processes, or of a proof of the companion Lemma 2 are welcome.

Selected references

• Y. Lei and S. Jasin, Real-Time Dynamic Pricing for Revenue Management with Reusable Resources, Advance Reservation, and Deterministic Service Time Requirements, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1906 (author manuscript: SSRN 2816718, https://ssrn.com/abstract=2816718)
• G. Gallego and G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24
• S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1276