All missions

Fairness in network flows

Many allocation problems ask for a feasible vector whose components are spread as evenly as possible: loads on links, shipments on routes, work assigned to servers. One way to make "evenly" precise is decreasing minimality: the largest component is as small as possible, within this the second largest, and so on. For maximum flows this question goes back to Megiddo, who found the fractional flows that are lexicographically optimal on the edges leaving the source (Megiddo 1974). Integral versions behave differently. Even with integer capacities, the unique fractional optimum can fail to be integral, so the integral problem needs its own theory. Frank and Murota developed that theory for M-convex sets (Frank, Murota 2021). In Fair integral network flows (arXiv:1907.02673v5) they treat integral feasible network flows, where the dec-min problem is harder because the flow polyhedron is not a base polyhedron.

Setting

A digraph $D=(V,A)$ has finitely many nodes and edges. Each edge has a tail and a head, and parallel edges are allowed. An edge enters $Z\subseteq V$ if its head is in $Z$ and its tail is not. For $x\in\mathbb R^A$, $\varrho_x(Z)$ and $\delta_x(Z)$ are the sums of $x$ over the edges entering and leaving $Z$. Bounds are $f:A\to\mathbb Z\cup\{-\infty\}$ and $g:A\to\mathbb Z\cup\{+\infty\}$ with $f\le g$. A demand $m:V\to\mathbb Z$ has $\widetilde m(V)=\sum_v m(v)=0$. An $m$-flow is an $x\in\mathbb R^A$ with $\varrho_x(v)-\delta_x(v)=m(v)$ at every node, and it is $(f,g)$-bounded if $f\le x\le g$. Write $Q=Q(f,g;m)$ for the set of these flows and Q⃛ $=Q\cap\mathbb Z^A$ for its integral members.

For an edge set $F$, a flow $z\in$ Q⃛ is decreasingly minimal on $F$ ($F$-dec-min) if no member of Q⃛ has a lexicographically smaller list of values on $F$ when both lists are sorted in non-increasing order. A box is $T(f^*,g^*)=\{x: f^*\le x\le g^*\}$. It is narrow on $F$ if $f^*(e)$ and $g^*(e)$ are finite with $0\le g^*(e)-f^*(e)\le 1$ for every $e\in F$.

Formalization targets

Goal: Theorem 2.1

Suppose $Q(f,g;m)\neq\emptyset$ and $f,g$ are finite on $F$. Then there are integer-valued $f^*,g^*$ with $f\le f^*\le g^*\le g$ such that, for every $z\in$ Q⃛$(f,g;m)$,

$$z \text{ is } F\text{-dec-min} \iff z\in \text{Q⃛}(f^*,g^*;m),$$

and $0\le g^*(e)-f^*(e)\le 1$ for every $e\in F$.

Milestones

The proof in §§3–5 has three layers, and the milestones follow them.

• Supermodular covering (§3). Theorem 3.1 (TDI of the covering system), Claim 3.3, Theorem 3.2 (min-max formula with an optimal chain) and Theorem 3.4 (chain optimality criteria).
• $L$-upper-minimal flows (§4). Lemmas 4.1 and 4.2 relate saturated edges to covers of $p=\widetilde m-\varrho_{g^-}+\delta_f$. Theorem 4.6 gives the chain criteria (O1)–(O5).
• Reductions and the tightening step (§2.2, §5). The tight-edge and $\beta_F$-capping reductions; Theorem 5.1 (dual optimal chain), Lemma 5.2, Claim 5.4, Lemma 5.5 and Theorem 5.3 (one tightening step that is narrow on $F-F'$).

Significance

Theorem 2.1 reduces fairness to feasibility. The set of fair integral flows is the set of integral points of an ordinary flow polyhedron with tightened bounds. Optimization over fair flows is therefore ordinary flow optimization. A cheapest $F$-dec-min flow, for example, is a minimum-cost $(f^*,g^*)$-bounded flow, solvable by any strongly polynomial min-cost circulation algorithm. The same description gives the structure of the solution set: all fair flows agree on $F$ up to a $\{0,1\}$ choice per edge.

The result is proved in the paper. As far as is known it has not been machine-checked. A formalization would cover the combinatorial core: Hoffman-type feasibility with integrality, the TDI covering theorem for intersecting supermodular functions, complementary slackness in chain form, and the induction on $|F|$. Formalizing the paper also exposed a gap in Theorem 3.4 as printed. It characterizes minimum covers only among sets that already cover $p$, so the milestone carries that hypothesis.

Difficulty

Lexicographic optimality is not a linear objective, and the obvious approach does not work. Minimizing a separable convex function, such as the square sum, does not give dec-min flows: on four edges the sorted vector $(3,3,3,0)$ is decreasingly smaller than $(4,2,2,1)$, yet its square sum is larger. The fractional dec-min flow is unique, but rounding it does not give the integral ones. The difficulty is to tighten bounds without losing any fair flow. One must know, at the current top value $\beta$, exactly which edges are forced to $\beta$ or $\beta-1$ and which can be pushed down. That information comes from a dual object, a chain of node sets, whose existence rests on total dual integrality of a supermodular covering system. Each step needs a chain with the right complementary-slackness behaviour, and then an argument that fixing the edges of $L'$ removes them from the lexicographic comparison.

Formalization scope

Edges are a finite type with tail and head maps, so parallel edges are allowed, and loops are harmless. $\mathbb Z\cup\{-\infty\}$ and $\mathbb Z\cup\{+\infty\}$ are WithBot ℤ and WithTop ℤ. Every comparison with a finite value is written termwise, so no infinite arithmetic decides any case. "$\varrho_g(Z)-\delta_f(Z)<+\infty$" means that every entering edge has finite $g$ and every leaving edge has finite $f$. Decreasing minimality compares the non-increasingly sorted value lists with the strict lexicographic order. An ascending sort would give increasing maximality, which is a different notion. Chains are finite families of distinct sets totally ordered by inclusion. The goal's hypothesis is a real feasible flow, while dec-min is taken among integral flows. The connectivity assumption at the start of §5 is not used.

The goal does not hold vacuously. The bounds $f^*,g^*$ are existentially quantified but must satisfy the iff for every integral feasible flow, and narrowness requires finite values. The sanity files check that (5.1) is satisfiable and that dec-min, which is not square-sum minimality, distinguishes vectors.

A complete development needs integral Hoffman feasibility (open on the platform as CombOpt.MinCostFlow.feasible_flow_iff_cut_condition), LP duality and complementary slackness for the covering programs, and uncrossing for supermodular functions. The digraph, flow and covering definitions are reusable beyond this mission. Contributions are welcome at any layer, in particular Theorem 3.1 and Hoffman's theorem, on which the rest depends.

Selected references

• A. Frank, K. Murota, Fair integral network flows, arXiv:1907.02673v5, 2022; Math. Oper. Res. 2023. https://arxiv.org/abs/1907.02673v5
• A. Frank, K. Murota, Decreasing minimization on M-convex sets: Background and structures, Math. Programming, 2021. https://doi.org/10.1007/s10107-021-01722-2
• A. Frank, Kernel systems of directed graphs, Acta Sci. Math. (Szeged) 41 (1979) 63–76.
• A. Frank, Connections in Combinatorial Optimization, Oxford University Press, 2011 (Theorem 17.1.1).
• A. J. Hoffman, Some recent applications of the theory of linear inequalities to extremal combinatorial analysis, Proc. Symp. Appl. Math. 10 (1960) 113–127.
• N. Megiddo, Optimal flows in networks with multiple sources and sinks, Math. Programming 7 (1974) 97–107. https://doi.org/10.1007/BF01585506

Motivation

Many estimation problems are posed over a manifold and carry a nonsmooth regularizer: sparse principal component analysis over the Stiefel manifold, nonnegative PCA, low-rank semidefinite programs in factored form. They share the composite form

$$\min_{x\in\mathcal M}\ \varphi(x):=f(x)+h(\mathcal Ax),$$

with $f$ smooth, $h$ convex but nonsmooth, $\mathcal A$ linear and $\mathcal M$ an embedded submanifold of $\mathbb R^n$. For smooth objectives on manifolds, first-order methods come with sharp iteration bounds (Boumal, Absil & Cartis, 2019). For the composite problem with a general $\mathcal A$, the available guarantees were weaker: Riemannian proximal gradient methods (Chen et al., 2020) need $\mathcal A=I$ and an inner semismooth Newton solve, and the augmented Lagrangian methods that do handle a general $\mathcal A$ came with only asymptotic convergence.

Deng, Hu, Wu and Wen (arXiv:2404.05121v2, 2024; Mathematics of Operations Research, 2025) give the first oracle-complexity bound for an augmented Lagrangian method on this problem. Their method ManIAL reaches an $\epsilon$-KKT point within $\tilde O(\epsilon^{-3})$ first-order oracle calls with an adaptive inner stopping rule, and within $O(\epsilon^{-3})$ calls with a fixed inner iteration budget.

Timeline (as surveyed in §1.1 of the paper). Smoothing methods based on the Moreau envelope reach $O(\epsilon^{-3})$ iterations for a smoothed stationarity notion. A Riemannian ADMM reaches $O(\epsilon^{-4})$ for a KKT residual. Earlier manifold augmented Lagrangian methods converge without rates. This paper gives the first rates for the augmented Lagrangian framework.

Setting

$\mathcal M\subseteq\mathbb R^n$ is compact, and $T_x\mathcal M$ is its tangent space at $x$. A retraction $R$ maps a tangent vector $u\in T_x\mathcal M$ to a point $R_x(u)\in\mathcal M$; on a compact submanifold it satisfies the retraction bounds $\|R_x(u)-x\|\le\alpha\|u\|$ and $\|R_x(u)-x-u\|\le\beta\|u\|^2$ (2.1). The Riemannian gradient is $\operatorname{grad}\psi(x)=P_{T_x\mathcal M}\nabla\psi(x)$. Assumption 1 requires that $f$ has an $\ell_{\nabla f}$-Lipschitz gradient, that $h:\mathbb R^m\to\mathbb R$ is convex and $\ell_h$-Lipschitz, and that $\varphi$ is bounded below.

A triple $(x,y,z)$ with $x\in\mathcal M$ is an $\epsilon$-KKT point pair (Definition 3.1) if

$$\|P_{T_x\mathcal M}(\nabla f(x)-\mathcal A^*z)\|\le\epsilon,\qquad \operatorname{dist}(-z,\partial h(y))\le\epsilon,\qquad \|\mathcal Ax-y\|\le\epsilon.$$

With the Moreau envelope $M_h^{1/\sigma}(w)=\inf_u\{h(u)+\frac\sigma2\|u-w\|^2\}$, the augmented Lagrangian is $\psi_k(x)=f(x)+M_h^{1/\sigma_k}(\mathcal Ax-z^k/\sigma_k)-\|z^k\|^2/(2\sigma_k)$. It is continuously differentiable. ManIAL (Algorithm 1) starts from $x^0\in\mathcal M$, $y^0$, $z^0=0$ and repeats four steps:

1. Run Riemannian gradient descent (RGD, Algorithm 2) on $\psi_k$ from $x^k$ with stepsize $1/L_k$, where $L_k=\alpha^2(\ell_{\nabla f}+\sigma_k\|\mathcal A\|^2)+2G\beta$ and $G$ bounds $\|\nabla\psi_k\|$ on $\mathcal M$. Option I stops at the first iterate with $\|\operatorname{grad}\psi_k\|\le\epsilon_k$. Option II runs $2^k$ steps and returns the iterate with the smallest gradient.
2. Set $y^{k+1}=\operatorname{prox}_{h/\sigma_k}(\mathcal Ax^{k+1}-z^k/\sigma_k)$.
3. Update the multiplier, $z^{k+1}=z^k-\beta_{k+1}(\mathcal Ax^{k+1}-y^{k+1})$, with a damped step $\beta_{k+1}$ (3.13).
4. Increase the penalty $\sigma_k$.

The certified output is $(x^{K+1},y^{K+1},\bar z^{K+1})$ with $\bar z^{K+1}=z^K-\sigma_K(\mathcal Ax^{K+1}-y^{K+1})$. One first-order oracle call computes $\nabla f$, one prox of $h$ and one retraction.

Formalization targets

Goal: Theorem 3.8 (b corrected)

There are constants $C$, depending only on the data, such that for every $\epsilon\in(0,1]$ some outer index $K$ yields an $\epsilon$-KKT point pair within

$$\text{(a)}\ \ C\epsilon^{-3}\big(1+\log(1/\epsilon)\big)\ \text{calls (Option I, }\sigma_k=b^k,\ \epsilon_k=b^{-k}),\qquad \text{(b)}\ \ C\epsilon^{-3}\ \text{calls (Option II, }\sigma_k=2^{k/3}).$$

The goal also asserts that such runs exist, so its universal statements are not vacuous.

Milestones

• the Moreau envelope facts (Proposition 2.5);
• the RGD rate $\min_{t\le T}\|\operatorname{grad}\psi(x_t)\|\le\sqrt{2L(\psi(x_0)-\psi_{\min})/T}$ (Lemma 3.2);
• the retraction smoothness of $\psi_k$ (Lemma 3.3);
• the inner call counts (Lemma 3.4, corrected);
• the multiplier bound $\|z^k\|\le z_{\max}=\frac{\beta_0\pi^2}6\|\mathcal Ax^0-y^0\|$ (3.31);
• the per-iteration residuals (3.29)–(3.32), sign corrected;
• the uniform gap bound (3.36)–(3.37);
• the outer complexities: Theorem 3.5, with $K\ge\log_b((\ell_h+z_{\max}+1)/\epsilon)$, and Theorem 3.6, corrected.

Significance

Theorem 3.8 is the paper's headline deterministic result: an augmented Lagrangian method for nonsmooth manifold problems with a general linear map $\mathcal A$, with an explicit oracle complexity that matches the best known smoothing rates. Option II removes the logarithmic factor of Option I. The structure of the proof is reusable: an outer analysis that is independent of the subroutine (Theorem 3.5), plus inner counts for any method with a sublinear rate on retraction-smooth functions.

The result is proved in the paper. This mission formalizes it, with four printed slips repaired:

• the Option II penalty, printed $1/2^{k/3}$, must be $2^{k/3}$;
• Lemma 3.4 drops a factor 2 of Lemma 3.2;
• Theorem 3.6's iteration count needs a $\sqrt{2c_2}$ term;
• the sign in (3.30) is reversed.

Each correction is minimal, comes with a counterexample to the printed version, and is declared on the item.

Difficulty

Each step is elementary, but three of them are subtle.

• Lemma 3.3. The descent inequality for $\psi_k$ along the retraction curve combines the Euclidean descent lemma, the second-order retraction bound and the identity $\langle\nabla\psi(x),\eta\rangle=\langle\operatorname{grad}\psi(x),\eta\rangle$ for tangent $\eta$. Its constant depends on a bound $G$ on $\|\nabla\psi_k\|$ over $\mathcal M$, which also fixes the stepsize.
• Bounded multipliers. The damping (3.13) makes $\sum_l\beta_l\|\mathcal Ax^l-y^l\|$ summable for any primal sequence. This is what keeps $z^k$ bounded while $\sigma_k\to\infty$.
• The final count. It sums geometric series of inner counts against the outer iteration count. Absorbing ceilings and small $\epsilon$ into one constant $C$, chosen before $\epsilon$, requires care.

The naive reading of Theorem 3.6, which assumes $c_12^{k/3}\ge c_2$ "without loss of generality", is false. The corrected count carries both $c_1$ and $c_2$.

Formalization scope

• Spaces and maps. Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). $\mathcal A$ is a continuous linear map and $\mathcal A^*$ its adjoint.
• Manifold and retraction. $\mathcal M$ is any compact set with $T_x\mathcal M$ the span of its tangent cone. $R$ is any map that sends tangent vectors to $\mathcal M$ and satisfies (2.1) with $\alpha,\beta>0$. Proposition 2.2 supplies these for every retraction on a compact submanifold, so the paper's setting is a special case.
• Initialization. $y^0$ is arbitrary; the paper's choice $y^0=\mathcal Ax^0$ is the special case in which every multiplier vanishes.
• Prox and envelope. The prox is an argmin predicate, and $M_h^{1/\sigma}$ is a real infimum, which is genuine for Lipschitz $h$.
• KKT condition. $\operatorname{dist}(-z,\partial h(y))\le\epsilon$ is encoded as an attained subgradient.
• Option I is the first hitting time of the stopping test. A run that idles is not allowed.
• Oracle count. The count of outer iterations $0,\dots,K$ is $\sum_{k\le K}(N_k+1)$: the subroutine's gradient evaluations plus one prox each.
• The bound $G$ is the run's own bound on $\|\nabla\psi_k\|$ over $\mathcal M$.
• Logarithms. The logarithm in (3.13) is natural, and $x/0=0$ there changes no iterate.

Not trivial. A universally quantified run statement would be vacuous if no run existed, so existence clauses are part of the goal. The constant $C$ precedes $\epsilon$; with $\epsilon$ first, the goal would be trivial.

Infrastructure. The mission reuses four published definitions: the tangent space, the Riemannian gradient, the prox predicate and the Moreau envelope. Definitions written for this mission that may be reusable elsewhere:

• the retraction-bound and retraction-smoothness predicates;
• the RGD iterate sequence;
• the convex subdifferential of a real function.

The Moreau-envelope calculus of Proposition 2.5 is not in Mathlib. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• K. Deng, J. Hu, J. Wu, Z. Wen, Oracle complexities of augmented Lagrangian methods for nonsmooth manifold optimization, arXiv:2404.05121v2, 2024 (Mathematics of Operations Research, 2025). https://arxiv.org/abs/2404.05121v2
• N. Boumal, P.-A. Absil, C. Cartis, Global rates of convergence for nonconvex optimization on manifolds, IMA Journal of Numerical Analysis 39(1), 2019. https://arxiv.org/abs/1605.08101
• S. Chen, S. Ma, A. M.-C. So, T. Zhang, Proximal gradient method for nonsmooth optimization over the Stiefel manifold, SIAM Journal on Optimization 30(1), 2020. https://arxiv.org/abs/1811.00980
• N. Boumal, An Introduction to Optimization on Smooth Manifolds, Cambridge University Press, 2023. https://www.nicolasboumal.net/book

Motivation

Large service systems such as call centers are staffed by people, and people work at different speeds. The classical many-server heavy-traffic theory, started by Halfin and Whitt (Operations Research, 1981), assumes identical exponential servers; its square-root staffing rule balances quality of service against utilization. Gans et al. documented, on call-center data, that agents' service rates differ markedly. Atar (Annals of Applied Probability 18(4), 2008) modeled the speeds as i.i.d. random rates drawn once at time zero and derived diffusion limits for two routing policies (longest-idle-server-first and fastest-server-first), one policy at a time, by approximating the system with finitely many server pools.

Büke and Qin (arXiv:1905.04198v1, 2019; journal version in Mathematics of Operations Research, 2023) treat the same model without fixing the routing policy. Their device is a measure-valued fairness process that records how cumulative idleness is shared among servers of different speeds. Theorem 5 of the paper shows that the diffusion limit depends on the policy only through the mean of the limiting fairness process.

Setting

The $n$-th system has $n$ servers. Server $k$ works at rate $\tilde\mu^n_k$, where the rates are i.i.d. with law $F$ on $(0,\infty)$, mean $\bar\mu$, variance $\mathrm{var}\,\tilde\mu$ and $\int\mu^2\,dF<\infty$. Customers arrive in a renewal process of rate $\lambda_n$ with interarrival times $u_i/\lambda_n$: $A^n(t)=\sup\{k:\sum_{i\le k}u_i/\lambda_n\le t\}$ with $u_i$ i.i.d., mean $1$, variance $\mathrm{var}\,u$. A customer served by server $k$ needs an exponential time of rate $\tilde\mu^n_k$; a waiting customer abandons at rate $\gamma\ge0$. The routing rule is arbitrary apart from three restrictions: it is non-idling (no server idles while customers wait), non-anticipating (it uses only the past and independent randomization) and non-preemptive.

Write $X^n(t)$ for the number of customers in system, $I^n_k(t)\in\{0,1\}$ for the idleness of server $k$, $\hat X^n(t)=(X^n(t)-n)/\sqrt n$ and $\hat I^n(t)=\sum_kI^n_k(t)/\sqrt n$. The Halfin–Whitt condition (Assumption 1) is $(\lambda_n-n\bar\mu)/\sqrt n\to\hat\lambda$.

The fairness process $\eta^n_t$ is the probability measure on $\mathbb R_+$ that gives to a set $A$ of rates the share of the idleness up to time $t$ that fell on servers with rate in $A$; before any idleness has accumulated it equals a placeholder $\zeta$. Its mean $\langle\!\langle\iota,\eta^n_t\rangle\!\rangle=\int\mu\,d\eta^n_t$ is the average speed of the servers that have been idle. Because $\eta^n$ oscillates wildly right after idleness starts, the paper works with shifted versions $S^n_\varepsilon\eta^n$, equal to $\zeta$ until the scaled cumulative idleness exceeds $\varepsilon$ (at time $\tau^n_\varepsilon$), and calls $\eta$ the limiting fairness process when $S^n_\varepsilon\eta^n\Rightarrow S_\varepsilon\eta$ for every $\varepsilon>0$, in Skorokhod's $J_1$ topology on left-continuous paths (Definition 1). Assumption 3 is a uniform integrability condition on $\eta^n$.

Formalization targets

Goal: Theorem 5

If the scaled initial conditions, the rate fluctuations $\hat\sigma^n=\sum_k(\tilde\mu^n_k-\bar\mu)/\sqrt n$, the noise and the shifted fairness processes converge jointly to $(\xi_0,\tilde\sigma,N,(S_{\varepsilon_k}\eta)_k)$, then $\tilde\sigma\sim N(0,\mathrm{var}\,\tilde\mu)$, $N=\sqrt{\bar\mu(1+\mathrm{var}\,u)}\,W$ for a standard Brownian motion $W$, and $\hat X^n\Rightarrow\xi$ in $D_{\mathbb R}[0,\infty)$, where $\xi$ is the unique solution of

$$\xi(t)=\xi_0+\sqrt{\bar\mu(1+\mathrm{var}\,u)}\,W(t)+(\hat\lambda-\tilde\sigma)t+\langle\!\langle\iota,\eta_t\rangle\!\rangle\int_0^t\xi^-(s)\,ds-\gamma\int_0^t\xi^+(s)\,ds .$$

The diffusion coefficient is corrected: the paper prints $\bar\mu\sqrt{c_a^2+1}$ with $c_a^2=\mathrm{var}\,u/\bar\mu^2$, which disagrees with the Erlang-A limit when all rates are equal and arrivals are Poisson.

Milestones

The milestones follow the proof: the pathwise decomposition (3.2) of $\hat X^n$ (signs corrected); tightness of the maximal scaled idleness (Lemma 1) and its fluid consequences (Corollary 1, Lemma 2); tightness of the shifted fairness processes and of their means (Theorem 2, Corollary 2); a joint Skorokhod representation for countably many tight components (Lemma 4); the martingale limits $\hat M^n_1\Rightarrow\sqrt{\bar\mu}\,W_2$, $\hat M^n_2\to0$; the arrival and rate central limit theorems $\hat A^n\Rightarrow\sqrt{\bar\mu\,\mathrm{var}\,u}\,W_1$, $\hat\sigma^n\Rightarrow N(0,\mathrm{var}\,\tilde\mu)$; and unique pathwise solvability of the limit equation.

Significance

The theorem separates the effect of routing from everything else. For Poisson arrivals and a single rate it reduces to the Garnett–Mandelbaum–Reiman Erlang-A limit; for the two policies Atar analyzed it recovers his limits once their fairness processes are identified (fastest-server-first idles the slowest servers, so $\eta=\delta_{\mu_{\min}}$). A new policy needs only its limiting fairness process to obtain a diffusion approximation, and the coefficient $\langle\!\langle\iota,\eta_t\rangle\!\rangle$ quantifies how much capacity a policy loses to idling fast servers.

No part of the result is formalized. The mission produces a machine-checked statement of the model (pathwise construction of departures from a time-changed Poisson process, non-anticipating routing), of the fairness process and of $J_1$ convergence for left-continuous measure-valued paths, together with a corrected diffusion constant. The Erlang-A special case is an open goal on the platform (ErlangA.Diffusion.theorem_2); this mission does not restate it.

Difficulty

The obvious route, applying the continuous mapping theorem to (3.2), fails because the fairness processes are not tight in any of Skorokhod's four topologies (Remark 1 of the paper): right after idleness starts, $\eta^n_t$ is a point mass on whichever server idled first, so it jumps between distant measures on a vanishing time scale. Convergence is only available for the shifted processes, one $\varepsilon$ at a time, and the limit $\eta$ is defined through infinitely many shifts. Passing to the limit in the product $\langle\!\langle\iota,\eta_t\rangle\!\rangle\int_0^t(\hat X^n)^-$ therefore needs a joint representation of all shifts and the noise on one probability space, a separate argument on the interval where the idleness is below $\varepsilon$, and a Gronwall estimate with a time-dependent coefficient. The joint law of the limit objects matters: with initial conditions correlated with the rates, $\xi_0$ and $\tilde\sigma$ are dependent.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0), servers are Fin n, and all systems live on one probability space (only laws matter). Unit-rate Poisson processes are given by i.i.d. exponential gaps; counts use the public BellWilliams2001.ThresholdPolicy.renewalCount. Non-anticipation is a filtration under which the future potential completions, the future abandonment clock and the future interarrival times are independent of the past; the service martingale property is a theorem, not an assumption. Means of measures are computed in $[0,\infty]$, $\tau^n_\varepsilon$ in $[0,\infty]$, and every convergence in distribution in coupling form (public PuhaWardFluid.Limit.ConvInDist for càdlàg paths, a left-continuous twin for $G_{\mathcal P}[0,\infty)$ with the Lévy–Prokhorov distance). Definition 1 is used along $\varepsilon_k=1/(k+1)$, as the paper does. The hypothesis is the joint convergence of the tuple, with the noise and the rate limit unconstrained; asserting a specific limit for either would make the goal trivial and is excluded. Abandonment rate $\gamma=0$ is allowed.

A complete development needs the renewal functional central limit theorem, a martingale functional central limit theorem for counting-process martingales, Lenglart's inequality, Prokhorov's theorem on product spaces, and Gronwall-type estimates; the $J_1$ machinery for left-continuous paths and the fairness process are reusable for the paper's other results (policy-specific fairness limits, Theorems 3, 4, 6, 7). Proofs of any milestone, and of reusable probabilistic lemmas, are welcome.

Selected references

• B. Büke, W. Qin, Many-Server Queues with Random Service Rates in the Halfin-Whitt Regime: A Measure-Valued Process Approach, arXiv:1905.04198v1, 2019. https://arxiv.org/abs/1905.04198v1
• R. Atar, Central limit theorem for a many-server queue with random service rates, Annals of Applied Probability 18(4):1548–1568, 2008. https://projecteuclid.org/journals/annals-of-applied-probability/volume-18/issue-4
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• O. Garnett, A. Mandelbaum, M. Reiman, Designing a call center with impatient customers, Manufacturing & Service Operations Management 4(3), 2002. https://doi.org/10.1287/msom.4.3.208.7753
• G. Pang, R. Talreja, W. Whitt, Martingale proofs of many-server heavy-traffic limits for Markovian queues, Probability Surveys 4, 2007. https://doi.org/10.1214/06-PS091
• W. Whitt, Stochastic-Process Limits, Springer, 2002. https://doi.org/10.1007/b97479

Chance constraints under distributional ambiguity

A chance constraint asks that a family of safety conditions $A(x)\xi\le b(x)$ hold with probability at least $1-\epsilon$, where $x\in\mathbb R^n$ is a decision and $\xi$ a random vector. Such constraints appear in power-system operation, vehicle routing, scheduling, portfolio selection and facility location (see the applications surveyed in §1 of the paper). The true distribution of $\xi$ is rarely known. A common remedy is to fix a reference distribution $\mathbb P$ (estimated or modelled) and require the constraint under every distribution in a Wasserstein ball around $\mathbb P$. This is the pessimistic, or distributionally robust, chance constraint (P-CC).

Around an empirical reference distribution the feasible region of (P-CC) is nonconvex: Xie (Mathematical Programming, 2019) and Chen, Kuhn, Wiesemann 2018 derived mixed-integer conic representations, and Xie and Ahmed (Operations Research, 2020) showed, as cited in the paper, p.4, that optimizing over it is strongly NP-hard. Shen and Jiang ask which reference distributions make the region convex. This mission formalizes their first main result, for joint chance constraints with uncertainty on the right-hand side.

Timeline:

• 1970 onwards. Prékopa shows that the classical chance constraint $\mathbb P[A\xi\le b(x)]\ge1-\epsilon$ defines a convex set when $\xi$ is log-concave; the result is extended to α-concave distributions (Shapiro, Dentcheva, Ruszczyński, Lectures on Stochastic Programming, 2009, Theorem 4.39 and Corollary 4.41).
• 2018–2019. Xie, and Chen–Kuhn–Wiesemann, reformulate the Wasserstein (P-CC) through a conditional value-at-risk of the distance to the unsafe set.
• 2021–2025. Shen and Jiang show convexity for α-concave references with $\alpha\ge-1$ (arXiv:2111.02486, version 2 of March 2025, published in Operations Research).

Setting

Let $E$ be a finite-dimensional real normed space: the space $\mathbb R^q$ of the uncertain vector $\xi$, with an arbitrary norm $\|\cdot\|$. A safety system has rows $a_1,\dots,a_k$ (continuous linear functionals on $E$) and a right-hand side $b(x)\in\mathbb R^k$ depending affinely on $x\in\mathbb R^n$. With right-hand-side uncertainty the matrix $A$ is constant. The safe event is $\mathcal S(x)=\{\xi: A\xi\le b(x)\}$.

The type-1 Wasserstein distance between Borel probability measures is $d_W(\mathbb Q,\mathbb P)=\inf_\pi\int\|\xi-\xi'\|\,d\pi$, the infimum over couplings $\pi$ of $\mathbb Q$ and $\mathbb P$. For a radius $\delta>0$ the ambiguity set is $\mathcal P=\{\mathbb Q: d_W(\mathbb Q,\mathbb P)\le\delta\}$, taken over all Borel probability measures on $E$. For $\epsilon\in(0,1)$ the feasible region is

$$\mathcal X^p_{\mathrm R}=\Bigl\{x\in\mathbb R^n:\ \inf_{\mathbb Q\in\mathcal P}\mathbb Q\bigl[A\xi\le b(x)\bigr]\ge1-\epsilon\Bigr\}.$$

The generalized mean is $m_\alpha(a,b;\theta)=0$ if $ab=0$, and otherwise $a^\theta b^{1-\theta}$ ($\alpha=0$), $\max\{a,b\}$ ($\alpha=+\infty$), $\min\{a,b\}$ ($\alpha=-\infty$), or $(\theta a^\alpha+(1-\theta)b^\alpha)^{1/\alpha}$. A probability measure $\mathbb P$ is α-concave if $\mathbb P(\theta A+(1-\theta)B)\ge m_\alpha(\mathbb P(A),\mathbb P(B);\theta)$ for all Borel sets $A,B$ and $\theta\in[0,1]$. Log-concave measures (Gaussians, uniform distributions on convex bodies) are the case $\alpha=0$.

Formalization targets

Goal: Theorem 1 (p.8)

If $\mathbb P$ is α-concave with $\alpha\ge-1$, then for every $\delta>0$ and $\epsilon\in(0,1)$,

$$\mathcal X^p_{\mathrm R}\ \text{is convex and closed.}$$

The statement fixes no norm, no number of rows and no particular distribution, and it places no density, support or moment condition on $\mathbb P$.

Milestones, in the order of the paper's proof

• Proposition 1 (p.6): $x\in\mathcal X^p$ iff $\delta/\epsilon+\mathrm{CVaR}_{1-\epsilon}(-d(\zeta,\mathcal S^c(x)))\le0$, for general affine $A(x)$.
• Lemma 1 (p.7): $\mathrm{CVaR}_{1-\epsilon}(X^-)=\mathbb 1\{0\ge\mathrm{VaR}_{1-\epsilon}(X)\}[\mathrm{CVaR}_{1-\epsilon}(X)-\mathbb E[X^+]/\epsilon]$.
• Corollary 1 (p.7): $\mathcal X^p$ through the normalized slack $f(x,\zeta)$, constraints (3)–(4).
• Lemma 2 (p.7, corrected): for $\mathbb P$ absolutely continuous, $d$ and $f$ are atomless.
• Proposition 2 (p.7): $\mathcal X^p=\{x:\ \delta\le\int_0^{\mathrm{VaR}_\epsilon(f)}(\mathbb P[f\ge t]-(1-\epsilon))\,dt,\ \mathbb P[A(x)\zeta\le b(x)]\ge1-\epsilon\}$.
• Proposition 3 (p.8): $x\mapsto\mathbb P[A\xi\le b(x)]$ is α-concave, and $\{x:\mathbb P[A\xi\le b(x)]\ge1-\epsilon\}$ is convex and closed.
• Lemma 3 (p.8): $x\mapsto\mathrm{VaR}_{1-\epsilon}(f(x,\zeta))$ is concave.
• Lemma 4 (p.8): $\psi(x,t)=\mathbb P[f(x,\zeta)\ge t]-(1-\epsilon)$ and $\int_0^y\psi(x,t)\,dt$ are continuous.
• Lemma 7 (p.31, corrected): $\alpha\mapsto m_\alpha(a,b;\theta)$ is nondecreasing, and continuous.
• Lemma 8 (p.35, corrected): $f-c$ is α-concave on $\{f>c\}$ for $\alpha\le1$ or $\alpha=+\infty$.
• Proposition 8 (p.31, corrected): the Borell–Brascamp–Lieb inequality.

Significance

The result. Theorem 1 identifies a broad class of reference distributions, every log-concave one in particular, for which the Wasserstein-robust joint chance constraint with right-hand-side uncertainty is a convex constraint. This contrasts with the NP-hardness around empirical distributions. It allows robust chance-constrained models to be solved by convex methods, and the paper builds a block coordinate ascent algorithm with global convergence on it (§4).

Formalizing it. The result is proved in the paper; no part of it is machine-checked. The proof chains a CVaR reformulation, a layer-cake identity and a Borell–Brascamp–Lieb argument, and the source needs four corrections (Lemmas 2, 7, 8 and Proposition 8; see each milestone). The paper's proof also covers only absolutely continuous references, through Lemma 2, while the theorem is stated, and is true, for every α-concave reference. A complete formal proof must close that gap, for instance by replacing the atomlessness argument with a layer-cake identity valid for any distribution.

Difficulty

The obvious approach writes $\mathcal X^p_{\mathrm R}$ as an intersection over $\mathbb Q\in\mathcal P$ of the sets $\{x:\mathbb Q[A\xi\le b(x)]\ge1-\epsilon\}$. It fails because the ball contains many distributions that are not α-concave (empirical measures among them), whose feasible sets are nonconvex; convexity of the intersection is not inherited term by term. The proof instead reduces the infimum over the ball to a single integral functional of $\mathbb P$, constraint (5). The convexity of its upper level set rests on the Borell–Brascamp–Lieb inequality and on the concavity of a quantile. The continuity needed for closedness, and the passage from midpoint quasi-concavity to quasi-concavity, are delicate when $\mathbb P$ has atoms or lower-dimensional support.

Formalization scope

• $\mathbb R^q$ with a norm is a finite-dimensional real normed space E with its Borel σ-algebra. Rows are continuous linear functionals and $\|a_i\|_*$ is the operator norm.
• The ball is the published WassersteinDRO.StrongDuality.ambiguityBall δ 1 P univ. Its distance takes values in $[0,\infty]$, so the ball imposes no moment condition. The infimum is taken in $[0,\infty]$.
• $\alpha$ is an EReal. The α-concavity of a measure quantifies over all measurable sets and evaluates the Minkowski combination as an outer measure, with no measurability side condition.
• VaR is the lower quantile (sInf) and CVaR is the real infimum over $\gamma$, both of the law of the random variable. Integrals with a possibly negative upper limit are oriented. Distances to a possibly empty set are Metric.infEDist.
• The goal has no density, support, moment, nonzero-row or $k\ge1$ hypothesis. A statement that restricts the ball, fixes the reference to a parametric family, or drops "closed" is not the goal.

Contributions are welcome on any milestone. The generalized mean, α-concave measures and the Borell–Brascamp–Lieb inequality are reusable beyond this mission. The platform's ConvexOptimization.prekopa_leindler is the case $\alpha=0$ of Proposition 8; Theorem 1 needs only the one-dimensional Borell–Brascamp–Lieb inequality.

Selected references

• H. Shen, R. Jiang, Convex Chance-Constrained Programs with Wasserstein Ambiguity, arXiv:2111.02486v2, 2025. https://arxiv.org/abs/2111.02486
• W. Xie, On distributionally robust chance constrained programs with Wasserstein distance, Mathematical Programming, 2019 (cited as [Xie19] in the paper).
• Z. Chen, D. Kuhn, W. Wiesemann, Data-driven chance constrained programs over Wasserstein balls, arXiv:1809.00210, 2018. https://arxiv.org/abs/1809.00210
• W. Xie, S. Ahmed, Bicriteria approximation of chance-constrained covering problems, Operations Research, 2020 (cited as [XA20] in the paper).
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• S. Das Gupta, Brunn–Minkowski inequality and its aftermath, Journal of Multivariate Analysis 10(3), pp. 296–318, 1980 (cited as [Gup80] in the paper).

Motivation

In many sequential decision problems the outcome of a decision arrives late. A recommendation's conversion, a clinical response or a sale is observed hours or weeks after the action, and in the meantime the decision maker has to keep acting. Contextual bandits model the decision side: at each round a learner sees side information, chooses one of $K$ actions and earns a reward that depends on the information and the action. Generalized linear contextual bandits, where the mean reward is a known increasing function $g$ of a linear score, cover logistic and Poisson responses and are standard in online advertising and personalized medicine (Li, Lu, Zhou 2017).

Delays break the usual analysis: the estimator can only use rewards that have arrived, and the learner does not know how many are missing. Earlier work on delayed bandits treated bounded or identically distributed delays, or non-contextual problems (Joulani, György, Szepesvári 2013; and the same authors' NeurIPS 2019 paper on generalized linear contextual bandits with stochastic delays, reference [49] of the paper). Blanchet, Xu, Zhou (2020) allow unbounded, non-identically distributed delays whose tails are dominated by a common envelope, and prove an explicit high-probability regret bound for a delay-adaptive UCB algorithm. That bound, Theorem 1 of the paper, is the goal of this mission.

Setting

Rounds are $t=1,\dots,T$. At round $t$ the learner observes $K$ feature vectors $x_{t,a}\in\mathbb R^d$ with $\|x_{t,a}\|\le1$, drawn afresh each round, chooses an arm $a_t$, and the reward $y_{t,a_t}\in[0,1]$ is generated with conditional mean $g(x_{t,a_t}'\theta^*)$ and conditionally $\hat\sigma$-sub-Gaussian noise. The parameter $\theta^*$ is unknown. The reward of round $t$ is revealed at the end of round $t+D_t$, for a non-negative random delay $D_t$.

At the beginning of round $t$ the complete timestamps are $T_t=\{s\le t-1: s+D_s\le t-1\}$, and the number of missing rewards is $G_t=(t-1)-|T_t|$. With $X_s=x_{s,a_s}$, the design matrices are $V_t=\sum_{s<t}X_sX_s'$ and $W_t=\sum_{s\in T_t}X_sX_s'$.

Assumption 1 asks that the average context covariance have smallest eigenvalue at least $\sigma_0^2$, that $\dot g\ge\kappa>0$ near $\theta^*$, and that $\dot g\le L_g$, $\ddot g\le M_g$. Assumption 2 asks that the delays be independent with a tail envelope $(\xi,\mu,M)$: a distribution $\xi$ on $[0,\infty)$ with mean $\mu$ such that $P(D_t\ge m)\le\xi[m,\infty)$ for all $m\ge M$, and $\xi\{z:z-\mu\ge x\}\le\exp(-x^{1+q}/(2\sigma^2))$. Write $\sigma_G=\sigma\sqrt{2+q}$ and $C_3=2\sigma^2+1$.

DUCB-GLCB (Algorithm 1) plays uniformly random arms for $\tau$ rounds. Afterwards it computes $\hat\theta_t$, a root of $\sum_{s\in T_t}(Y_s-g(X_s'\theta))X_s=0$, sets

$$\beta_t=\frac{\hat\sigma}{\kappa}\sqrt{\frac d2\log\Big(1+\frac{2(t-G_t)}d\Big)+\log\frac1\delta}+\sqrt{G_t},$$

and plays an arm maximizing $x_{t,a}'\hat\theta_t+\beta_t\|x_{t,a}\|_{V_t^{-1}}$. The regret is $R_T=\sum_{t=1}^T\big(\max_a g(x_{t,a}'\theta^*)-g(x_{t,a_t}'\theta^*)\big)$.

Formalization targets

Goal: Theorem 1

For constants $M>0$, $\mu$, $\sigma_0,\hat\sigma,\sigma,\kappa>0$ there is $C>0$ such that, for every $q\ge0$, $1\le d\le T$, $K\ge1$, $\delta\in(0,1)$ and every model satisfying the assumptions, running DUCB-GLCB with $\tau=\lceil C(d+\log(1/\delta))\rceil$ gives

$$P\big(R_T>B_{16}\big)\le5\delta,$$

where $B_{16}$ is the explicit right-hand side of (16): $\tau$ plus $L_g$ times terms of order $\sqrt{(\mu+M)Td\log(T/d)}$, $\sqrt{\sigma_G}(\log T)^{1/4}\sqrt{dT\log(T/d)}$ and $(d\hat\sigma/\kappa)\log(T/(d\delta))\sqrt T$.

Milestones

• Proposition 1-1, 1-2: tail bounds (6), (7) for $G_t$ and $G^*_T=\max_{s\le T}G_s$.
• Proposition 1-3: $\lambda_{\min}(W_t)\ge B$ with probability $1-2\delta$ once $t$ exceeds (8).
• The deterministic steps of the proof: the decomposition (35)–(36), the comparison $v'V_tv\le v'W_tv+G_t\|v\|^2$, the one-step bound (40), the elliptical potential sum (41), the summed bound on p.27 and the regret reduction (42).

Significance

Theorem 1 shows that delays enter the regret only additively. The leading term $d\sqrt T\log T$ is that of the undelayed problem, while the delay parameters $\mu+M$ and $\sigma_G$ appear in lower-order terms. Corollary 1 of the paper derives an expected-regret bound from it, and Proposition 2 sharpens it for bounded and for i.i.d. delays.

The result is proved in the paper and has no machine-checked proof. A formal proof needs a self-normalized concentration bound for the GLM estimator built from an adaptively chosen, delay-filtered subsample, a matrix lower-tail bound for $\lambda_{\min}(W_t)$, and a tail bound for the number of missing rewards. The deterministic linear-algebra steps (the elliptical potential sum in particular) are reusable across linear and generalized linear bandit missions.

Difficulty

The obvious route is to rerun the GLM-UCB analysis on the complete samples. It fails at two places. First, the samples in $T_t$ are selected by the delays, so the confidence ellipsoid lives in the $W_t$-norm, while the algorithm's bonus uses $V_t$; the gap between them is the $\sqrt{G_t}$ term, and $G_t$ is a sum of dependent-looking indicators of unbounded delays. Second, the estimator is only well defined once $W_t$ is well conditioned, which needs a matrix concentration bound with absolute constants and a bound on $G_t$ at the same time.

The confidence step (37) as printed is false: in a linear model with Bernoulli rewards and no delays its failure probability exceeds $2\delta$ at $\delta=1/T$ for large $T$, because the cited self-normalized bound carries a factor $\sqrt2$ missing from the radius. It is not a milestone, and a proof of the goal cannot cite it as printed.

Formalization scope

Vectors are Fin d → ℝ, with the ℓ₂ norm and $\lambda_{\min}$ (the Rayleigh infimum) of a published notation module. Rounds start at $1$. Delays are real, with $s\in T_t$ iff $s+D_s\le t-1$ and $G_t=(t-1)-|T_t|$. The reward is a full table $y_{t,a}$. "Drawn i.i.d." is the freshness of each round's data with respect to everything earlier. The reward model is (2)–(3) per arm conditional on the context, with $g$ non-decreasing. The envelope $\xi$ lives on $[0,\infty)$, which is needed for Proposition 1-1 to hold. The width $\beta_t$ uses $\sqrt{G_t}$ as in Algorithm 1 (the theorem's statement prints $G_t$). The estimator is any measurable function of the complete tuples returning a root of (5) whenever one exists, and $V_t^{-1}$ is Mathlib's total inverse. The constant $C$ is chosen before $q,d,K,T,\delta$ and the model, as printed.

A trivializing encoding is ruled out: $C$ cannot depend on $T$ (so $\tau\ge T$ is impossible), the hypotheses are satisfiable (a verified one-dimensional instance), and the estimator cannot read missing rewards.

Welcome contributions: the elliptical potential bound (41), Proposition 1's tail bounds, the matrix concentration step, and a corrected confidence ellipsoid for the delayed GLM estimator.

Selected references

• J. Blanchet, R. Xu, Z. Zhou, Delay-Adaptive Learning in Generalized Linear Contextual Bandits, arXiv:2003.05174v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2003.05174
• L. Li, Y. Lu, D. Zhou, Provably Optimal Algorithms for Generalized Linear Contextual Bandits, ICML 2017. https://arxiv.org/abs/1703.00048
• P. Joulani, A. György, C. Szepesvári, Online Learning under Delayed Feedback, ICML 2013. https://arxiv.org/abs/1306.0686
• R. Vershynin, Introduction to the Non-Asymptotic Analysis of Random Matrices, 2010. https://arxiv.org/abs/1011.3027

Bayesian simple regret in best arm identification

A clinical trial, an A/B test or a simulation study often ends with one decision: which treatment to adopt. Multi-armed bandit theory calls this best arm identification. When the arm means are fixed, the frequentist simple regret after $T$ pulls decays exponentially at each instance, with a rate that degenerates as the gap closes. A practitioner who has a prior belief about the means needs a different quantity: the Bayesian simple regret, the frequentist simple regret averaged over a prior $H$. Komiyama, Ariu, Kato and Qin (arXiv:2111.09885v3) show that it decays at the polynomial rate $1/T$, and that the leading term comes from instances with gaps at most of order $\sqrt{\log T/T}$.

The closest classical result concerns cumulative regret. Lai (1987), building on Lai and Robbins (1985), describes the Bayesian regret of asymptotically optimal algorithms in terms of the prior's density on the set of close arms. The paper gives the parallel statement for simple regret, with a matching lower bound up to the factor $4.8$ (Theorem 5, not part of this mission).

Setting

There are $K\ge2$ arms with unknown means $\mu=(\mu_1,\dots,\mu_K)\in[0,1]^K$, and a pull of arm $i$ returns a Bernoulli($\mu_i$) reward. Write $\mu^*=\max_i\mu_i$. A forecaster has $T$ pulls and then recommends an arm $J(T)$. The simple regret is $\mathrm R_\mu(T)=\mu^*-\mathbb E_\mu[\mu_{J(T)}]$, and the Bayesian simple regret is $\mathrm R_H(T)=\mathbb E_{\mu\sim H}[\mathrm R_\mu(T)]$.

The prior satisfies Assumption 1: there are conditional densities $h_i(\mu_i\mid\mu_{\setminus i})$ and $h_{ij}(\mu_i,\mu_j\mid\mu_{\setminus ij})$ that are uniformly continuous, with a modulus that does not depend on the conditioning vector. Here $\mu_{\setminus i}$ is the vector of the other means, with law $H_{\setminus i}$.

Two-stage exploration (TSE, Algorithm 1) takes $q\in(0,1)$. It pulls every arm $qT/K$ times, forms confidence bounds $L_i,U_i$ of width $B_{\mathrm{conf}}=\sqrt{K\log T/(qT)}$, and keeps the candidate set $\hat{\mathcal J}^*=\{i:U_i\ge\max_jL_j\}$. A unique candidate is returned at once. Otherwise the remaining budget is shared equally among the candidates, and the candidate with the largest empirical mean is recommended.

Formalization targets

Goal: Theorem 1

With $T'=2qT/K+(1-q)T$ and $\mu^*_{\setminus i}=\max_{j\ne i}\mu_j$,

$$\mathrm R_H(T)\le\frac{C_{\mathrm{opt}}}{T'}+o\Big(\frac1T\Big),\qquad C_{\mathrm{opt}}=\sum_{i}\int\mu^*_{\setminus i}(1-\mu^*_{\setminus i})\,h_i(\mu^*_{\setminus i}\mid\mu_{\setminus i})\,dH_{\setminus i}(\mu_{\setminus i}).$$

Milestones

Lemma 10 (Chernoff and Hoeffding), Lemma 2 ($\mathbb P[\mathcal S]\ge1-2K/T^2$ for the event $\mathcal S$ that all means lie in their intervals), Lemma 3 (three or more candidates contribute $o(1/T)$), Proposition 9 (two-sided Stirling), Lemmas 11 to 13 (sharp expansions of the Bernoulli divergence), Lemma 15 (a two-sided Gaussian approximation, with relative error $o(1)$, of the error of comparing two arms), Lemma 14 (its integral over the gap) and Lemma 4 (two candidates contribute at most $C_{\mathrm{opt}}/T'+o(1/T)$).

Significance

The theorem gives the rate of a natural objective with a constant that depends on the prior only through its density on the set of tied arms. For the uniform prior, $C_{\mathrm{opt}}=(K-1)/(K+1)$. Since $T'\to T$ as $q\to0$, TSE comes within a constant factor of the Bayes-optimal dynamic program, which is too expensive to compute for moderate $K$ and $T$.

No formalization of this result appears on the platform. This mission adds the Bayesian simple regret objective, a two-stage elimination algorithm, sharp second-order bounds for the Bernoulli divergence near the boundary, and a sharp Gaussian comparison for two binomial means. Three statements are printed false and are corrected here with explicit counterexamples: (14) in Lemma 12, and Lemmas 14 and 15, which fail at small means. Lemma 13 is restated in the relative form that its use requires. Each milestone records these differences.

Difficulty

The leading constant is the obstacle. A Chernoff bound on the event $\hat\mu_i\le\hat\mu_j$ gives the right rate, but integrating it against the prior loses a factor of four against Lemma 14 (Remark 4). Lemma 15 must therefore bound the error probability of two binomial means by the Gaussian tail with relative accuracy $1+o(1)$, uniformly in means as small as $T^{-1/6}$ and gaps up to $2B_{\mathrm{conf}}$. At such gaps the target can be super-polynomially small, so an additive normal approximation such as Berry–Esseen does not suffice. Lemma 4 then has to transfer this bound through the prior, for which only uniform continuity is available and whose density may vanish.

Formalization scope

Arms are Fin K with 2 ≤ K, and q ∈ (0, 1). Rewards are a reward tape Fin K → Fin T → Bool with independent entries; since the pulls of TSE are fixed stage by stage, no general bandit protocol is needed. Sample sizes are rounded: $n_1=\lceil qT/K\rceil$, $n_2(s)=\lfloor(T-Kn_1)/s\rfloor$. The final mean is cumulative over both stages. The arg max uses an arbitrary tie-break rule, and every statement holds for all rules uniformly. A prior is RegularPrior H h hh: conditional densities that disintegrate H in lintegral form, with continuity on $[0,1]$ only. $o(1/T)$ in an upper bound is one-sided: for every $\varepsilon>0$, $\le\varepsilon/T$ eventually, and $T_0$ precedes the means in Lemmas 14 and 15, because that uniformity is what lets them be integrated over $H$.

Assumption 1 cannot be made vacuous: the uniform prior satisfies it, and verification files prove that at $K=2$ with $C_{\mathrm{opt}}=1/3$, and prove integrability of every integrand under RegularPrior, so that no Bochner integral defaults to $0$.

A complete development needs tape-probability lemmas, Hoeffding's inequality for the tape, a two-sided Stirling bound, the disintegration argument for the prior, and the binomial sum of Lemma 15. The divergence bounds and Stirling bounds are reusable elsewhere. Alternative proofs of Lemma 14 are welcome.

Selected references

• J. Komiyama, K. Ariu, M. Kato, C. Qin, Rate-optimal Bayesian Simple Regret in Best Arm Identification, arXiv:2111.09885v3, 2023. https://arxiv.org/abs/2111.09885
• T. L. Lai, Adaptive treatment allocation and the multi-armed bandit problem, Annals of Statistics, 1987. https://doi.org/10.1214/aos/1176350495
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• A. Carpentier, A. Locatelli, Tight (lower) bounds for the fixed budget best arm identification bandit problem, COLT, 2016. https://arxiv.org/abs/1605.09004

Why desingularizing functions matter

The Kurdyka–Łojasiewicz (KL) inequality is the regularity condition behind most convergence proofs for first-order methods on nonconvex, nonsmooth problems: proximal gradient, PALM, proximal ADMM and their variants. Near a point $\bar x$, it asks that

$$\varphi'\big(f(x)-f(\bar x)\big)\cdot\operatorname{dist}\big(0,\partial f(x)\big)\ge1$$

for some concave desingularizing function $\varphi$ with $\varphi(0)=0$. Once it holds, a sufficient-decrease argument shows that bounded iterates have finite length and converge to a stationary point, with lengths and rates expressed through $\varphi$ (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014). A smaller $\varphi$ gives a sharper bound. Desingularizing functions are far from unique, so the question "what is the optimal concave desingularizing function?" (question (1) of Wang–Wang) was left open by this literature.

Timeline:

• 1963, 1998: Łojasiewicz proves the gradient inequality for real-analytic functions, and Kurdyka extends it to o-minimal structures.
• 2007: Bolte, Daniilidis and Lewis extend it to nonsmooth subanalytic functions through the limiting subdifferential.
• 2010: Bolte, Daniilidis, Ley and Mazet characterize it for convex functions and give a desingularizing function built from level sets (BDLM 2010).
• 2013–2014: Attouch–Bolte–Svaiter and Bolte–Sabach–Teboulle turn the KL inequality into a general convergence template for descent methods.
• 2021: Wang and Wang introduce the generalized concave KL property and its exact modulus, and prove that the exact modulus is the smallest concave desingularizing function (Proposition 3.9).

Setting

Let $f:\mathbb R^n\to(-\infty,\infty]$ be proper and lower semicontinuous, and write $\partial f$ for its limiting subdifferential and $\operatorname{dist}(0,\partial f(x))\in[0,\infty]$ for the distance from the origin to it, with $\operatorname{dist}(0,\emptyset)=\infty$. Fix $\bar x$ with $\partial f(\bar x)\ne\emptyset$, a neighbourhood $U$ of $\bar x$ and $\eta\in(0,\infty]$, and write $[0<f-f(\bar x)<\eta]$ for the points where $f$ exceeds $f(\bar x)$ by less than $\eta$.

The class $\Phi_\eta$ (Lean PhiClass η ϕ) consists of the functions $\varphi:[0,\eta)\to\mathbb R_+$ that are right-continuous at $0$ with $\varphi(0)=0$ and strictly increasing on $[0,\eta)$. Concave members of $\Phi_\eta$ need not be differentiable, so the paper uses the left derivative $\varphi'_-(t)=\lim_{s\to t^-}(\varphi(s)-\varphi(t))/(s-t)$ (Lean leftDeriv), which exists for concave functions.

The generalized concave KL property of $f$ at $\bar x$ with respect to $U$, $\eta$ and a concave $\varphi\in\Phi_\eta$ is inequality (7) (Lean KLIneq f x̄ U η ϕ):

$$\varphi'_-\big(f(x)-f(\bar x)\big)\cdot\operatorname{dist}\big(0,\partial f(x)\big)\ge1\qquad\text{for all }x\in U\cap[0<f-f(\bar x)<\eta].$$

Such a $\varphi$ is a concave desingularizing function of $f$ at $\bar x$ with respect to $U$ and $\eta$.

The exact modulus (Definition 3.6) is built from

$$h(s)=\sup\Big\{\operatorname{dist}^{-1}\big(0,\partial f(x)\big):\ x\in U\cap[0<f-f(\bar x)<\eta],\ s\le f(x)-f(\bar x)\Big\},\qquad s\in(0,\eta),$$

(Lean hfun) as $\tilde\varphi(t)=\int_0^t h(s)\,ds$ with $\tilde\varphi(0)=0$ (Lean exactModulus). The supremum runs over the sublevel condition $s\le f(x)-f(\bar x)$, not over the level set $s=f(x)-f(\bar x)$ (Remark 3.7(i)); this makes $h$ nonincreasing and $\tilde\varphi$ concave.

Formalization targets

Goal: Proposition 3.9 (corrected)

Assume $f$ has the generalized concave KL property at $\bar x$ with respect to $U$, $\eta$ and a concave $\varphi\in\Phi_\eta$. Then $h<\infty$ on $(0,\eta)$, $\int_0^th<\infty$ on $[0,\eta)$, $\tilde\varphi$ is concave, nondecreasing, right-continuous at $0$ with $\tilde\varphi(0)=0$, satisfies (7), and

$$\tilde\varphi(t)\le\varphi(t),\qquad \tilde\varphi(t)=\inf\big\{\psi(t):\psi\in\Phi_\eta\text{ concave desingularizing}\big\}\qquad(t\in[0,\eta)).$$

Moreover $\tilde\varphi\in\Phi_\eta$ if and only if every level $s\in(0,\eta)$ is reached by some $x\in U\cap\operatorname{dom}\partial f$ with $s\le f(x)-f(\bar x)<\eta$. Under that condition $\tilde\varphi$ is itself the least concave desingularizing function, which is the printed statement.

The printed statement claims $\tilde\varphi\in\Phi_\eta$ unconditionally. This is false. Take $f(x)=|x|$ on $\mathbb R$, $\bar x=0$, $U=(-1,1)$, $\eta=\infty$ and $\varphi(t)=t$. Every assumption holds, but no point of $U$ has $f(x)\ge1$, so $h(s)$ is a supremum over the empty set for $s\ge1$ and $\tilde\varphi(t)=\min(t,1)$ is not strictly increasing. The goal keeps every unconditional clause and replaces the false one by the exact condition.

Milestones, in proof order

1. Lemma 3.1(ii): for concave $\varphi\in\Phi_\eta$, $\varphi'_-$ is nonincreasing and positive on $(0,\eta)$.
2. Proof of Proposition 3.9: $h(s)\le\varphi'_-(s)$ on $(0,\eta)$.
3. Lemma 3.1(i): $\varphi(t)=\lim_{u\to0^+}\int_u^t\varphi'_-=\int_0^t\varphi'_-$.
4. Proof of Proposition 3.9: $h$ is nonincreasing, and positive at every reached level (corrected).
5. Lemma 3.8, for nonnegative $h$: $\int_0^t h$ is concave with $\varphi'_-\ge h$; strictly increasing if $h>0$; $C^1$ if $h$ is continuous.
6. Proof of Proposition 3.9: $\tilde\varphi'_-(f(x)-f(\bar x))\ge h(t)\ge\operatorname{dist}^{-1}(0,\partial f(x))$.

Significance

The result. Proposition 3.9 settles question (1) within the class of concave desingularizing functions: when any exists, the exact modulus is pointwise the smallest, so every length or rate bound written in terms of $\varphi$ is sharpest with $\tilde\varphi$. The paper uses it to sharpen the PALM length bound of Bolte–Sabach–Teboulle (Theorem 4.5) and to show by examples that classical constructions (BDLM, growth conditions, Łojasiewicz exponents) can be strictly suboptimal. Example 3.10 shows that $\tilde\varphi$ can have a kink. Smooth desingularizing functions therefore cannot express the optimum, and this is why the left derivative is needed.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission formalizes it with the conventions made explicit, including the reachability correction. Classical KL vocabulary is already on the platform (limiting subdifferential, $C^1$ desingularizers, the BST finite-length theorem). This mission adds the nonsmooth class $\Phi_\eta$, the left-derivative form of (7) and the exact modulus.

Difficulty

Each step of the printed proof is short, but the real-analysis infrastructure behind it is not in Mathlib as stated.

• The fundamental theorem of calculus through the left derivative of a concave function (Lemma 3.1(i)): left and right derivatives differ on a countable set, and $\varphi$ is only right-continuous at $0$.
• Concavity and the left-derivative bound of $t\mapsto\int_0^th$ for monotone $h$ (Lemma 3.8). At a stationary $\bar x$, $h(0^+)=\infty$ and the integral is improper (Remark 3.7(ii)).
• The infimum identity when the reachability condition fails: then $\tilde\varphi$ is not itself a member of the set over which the infimum is taken.

The natural first idea, that "$h$ is positive because $\operatorname{dist}(0,\partial f(x))>0$ on the band", only works at levels the band reaches. That gap is exactly the correction.

Formalization scope

Points are in EuclideanSpace ℝ (Fin n) and $f$ takes values in EReal. Properness is the published IsProperFn and $\partial f$ the published LimitingSubdiff, both reused. $\eta$ is an ℝ≥0∞ with $0<\eta$, so $\eta=\infty$ is kept. $[0,\eta)$ is Ieta η. $\varphi,\psi:\mathbb R\to\mathbb R$ are constrained only on $[0,\eta)$, and concavity is ConcaveOn ℝ (Ieta η). The left derivative is derivWithin ϕ (Set.Iio t) t, never the two-sided deriv. $\operatorname{dist}$, $\operatorname{dist}^{-1}$ and $h$ are ℝ≥0∞-valued (Metric.infEDist, $\sup\emptyset=0$). $\tilde\varphi$ is the real part of a lintegral over $(0,t]$, and the goal proves that lintegral finite. Inequality (7) is written $\forall v\in\partial f(x),\ 1\le\varphi'_-(f(x)-f(\bar x))\,\|v\|$. $U$ is any neighbourhood of $\bar x$; the paper's $U\subseteq\operatorname{dom}\partial f$ is not required, since points outside $\operatorname{dom}\partial f$ change nothing.

The statement cannot be trivialized through junk values. A real-valued supremum, Metric.infDist, or toReal without the finiteness clause would each make $h$ or $\tilde\varphi$ degenerate; the goal avoids all three. The hypotheses are satisfiable: the $|x|$ instance above meets them all.

Useful infrastructure for this mission includes one-sided derivatives of concave functions and their integrals, lintegral–integral bookkeeping for monotone integrands, and the infimum argument. The first two are reusable for any KL-type analysis with nonsmooth desingularizers. Proofs of the milestones, alternative arguments and general lemmas on concave functions are all welcome.

Selected references

• X. Wang, Z. Wang, The exact modulus of the generalized concave Kurdyka-Łojasiewicz property, arXiv:2008.13257v5, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2008.13257v5
• J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Mathematical Programming 146, 2014. https://doi.org/10.1007/s10107-013-0701-9
• H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Mathematical Programming 137, 2013. https://doi.org/10.1007/s10107-011-0484-9
• J. Bolte, A. Daniilidis, O. Ley, L. Mazet, Characterizations of Łojasiewicz inequalities: subgradient flows, talweg, convexity, Transactions of the AMS 362, 2010. https://doi.org/10.1090/S0002-9947-09-05048-X