All missions

Motivation

Stochastic gradient methods return a single random point, and a practitioner who runs one rarely knows how far that point is from the true optimum. A central limit theorem (CLT) for the iterates answers this: it says that the suitably rescaled error is asymptotically Gaussian with an explicit covariance, which is the basis of confidence regions for the optimal solution. For the classical Robbins–Monro scheme with diminishing steps such results are classical (for example Polyak and Juditsky, SIAM J. Control Optim. 1992, for averaged iterates). Modern practice, however, uses variance reduction by mini-batches whose size grows along the run, together with constant step lengths and Nesterov acceleration. Lei and Shanbhag (arXiv:2006.07769v3, 2024; Math. Oper. Res. 2025) prove CLTs for these schemes. This mission formalizes their CLT for the accelerated method with geometrically increasing batch sizes (Theorem 2).

Setting

The problem is $\min_{x\in\mathbb R^m} f(x)$ with $f(x)=\mathbb E[F(x,\xi)]$. Assumption 1: $f$ is continuously differentiable, its gradient is $L$-Lipschitz, and $f$ is $\eta$-strongly convex, $(\nabla f(x)-\nabla f(x'))^T(x-x')\ge\eta\|x-x'\|^2$. Its unique minimizer is $x^*$.

The exact gradient is unavailable. At iteration $k$ the method averages $N_k$ sampled gradients; the gradient noise $w_{k,N_k}$ is the difference between this average and $\nabla f(x_k)$. With $\mathcal F_k$ the history before round $k$, it satisfies (5):

$$\mathbb E[w_{k,N_k}\mid\mathcal F_k]=0,\qquad \mathbb E[\|w_{k,N_k}\|^2\mid\mathcal F_k]\le \nu^2/N_k .$$

Algorithm 2 (variance-reduced accelerated SGD) starts at $x_0=y_0$ and iterates

$$y_{k+1}=x_k-\alpha(\nabla f(x_k)+w_{k,N_k}),\qquad x_{k+1}=y_{k+1}+\beta(y_{k+1}-y_k).$$

Assumption 2 has two parts. (i) The gradient has a Hessian $H$ at $x^*$ with a quadratic remainder, $\|\nabla f(x)-H(x-x^*)\|\le R_D\|x-x^*\|^2$. (ii) The rescaled noise has an asymptotic covariance $S_0$, conditionally and unconditionally, $N_k\mathbb E[w_kw_k^T\mid\mathcal F_k]\to S_0$ and $N_k\mathbb E[w_kw_k^T]\to S_0$, and $\|\sqrt{N_k}w_k\|^2$ is uniformly integrable. For a real square matrix $P$, $\rho(P)$ is the spectral radius, the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 2

Take $\alpha\in(0,1/L]$, $\gamma=\sqrt{\alpha\eta}$, $\beta=\frac{1-\gamma}{1+\gamma}$, $N_k=\lceil\rho_2^{-(k+1)}\rceil$ with $\rho_2\in(1-\gamma,1)$, and

$$P_2=\rho_2^{-1/2}\begin{pmatrix}(1+\beta)(I_m-\alpha H)&-\beta(I_m-\alpha H)\\ I_m&0_m\end{pmatrix}.$$

Then $\rho(P_2)<1$ and

$$\alpha^{-1}\rho_2^{-k/2}\begin{pmatrix}y_k-x^*\\ y_{k-1}-x^*\end{pmatrix}\xrightarrow{d}N(0,\Sigma_2),\qquad \Sigma_2=\sum_{t=0}^{\infty}P_2^t\begin{pmatrix}S_0&0\\0&0\end{pmatrix}(P_2^t)^T .$$

The statement holds for every dimension $m$, every admissible $\alpha$ and every $\rho_2$ above the deterministic rate $1-\gamma$; no constant is hard-coded.

Milestones

In proof order:

1. the Hessian $H$ is symmetric with spectrum in $[\eta,L]$ (proof of Theorem 1, p.17);
2. display (46): $\rho(H_2)=\max_i\sqrt{\beta(1-\alpha\lambda_i)}\le 1-\gamma<\rho_2<\rho_2^{1/2}$ (p.20);
3. Lemma 2, the bound (11) on $\mathbb E[f(y_k)-f^*]$ for arbitrary batch sizes (p.8);
4. Proposition 2, the geometric rate (22) and $\mathbb E\|x_k-x^*\|^2\le c\rho_2^k$ (p.12);
5. Lemma 10, Gelfand's formula and $\|P^k\|\le c(\iota)(\rho(P)+\iota)^k$ (p.38);
6. Lemma 6, a multivariate martingale CLT for triangular arrays (p.14);
7. Lemma 7, the CLT for the linear recursion $e_{k+1}=Pe_k-\alpha\rho^{-(k+1)/2}Gw_{k,N_k}+\zeta_{k+1}$ (p.16), in a corrected form.

Significance

Theorem 2 identifies the exact asymptotic law of the accelerated iterates under growing batches: the error decays like $\rho_2^{k/2}$ and, after rescaling, is Gaussian with covariance $\Sigma_2$, the solution of a discrete Lyapunov equation. With the CLT for the non-accelerated method (Theorem 1 of the paper) it supports the confidence-region constructions of §5 of the paper, and it quantifies how acceleration changes the limiting covariance: through $P_2$, a $2m\times 2m$ matrix with complex eigenvalues, rather than through $I-\alpha H$.

The paper proves the result. Nothing in it is machine-checked, and parts of the underlying theory are not in Mathlib: there is no multivariate martingale CLT for triangular arrays (Mathlib has convergence in distribution and the one-dimensional central limit theorem for i.i.d. sums, and the platform has one-dimensional martingale CLTs only), and no stability theory for random linear recursions. Formalizing Lemma 6 and Lemma 7 produces reusable tools for any stochastic approximation scheme whose error obeys a linear recursion with martingale noise. The mission also corrects Lemma 7: as printed it allows remainders $\zeta_k\to0$ in probability whose accumulated effect does not vanish, and the corrected version adds $\sup_k\mathbb E\|\zeta_k\|<\infty$, which Theorem 2's remainder satisfies.

Difficulty

Three steps are hard. First, the noise has a covariance that only stabilizes asymptotically, so Lemma 7 must apply a martingale-array CLT whose rows are weighted by powers $P^{k-1-t}$ of a non-normal matrix. Controlling these weights needs Gelfand's formula rather than a norm bound: $\|P_2\|$ can exceed $1$ even though $\rho(P_2)<1$. Second, for $P_2$ the eigenvalue computation (46) goes through a $2\times 2$ characteristic equation per eigenvalue of $H$ with nonpositive discriminant; the spectral radius is attained by complex eigenvalues, so arguments over real spectra do not apply. Third, the nonlinear remainder $\alpha\rho_2^{-(k+1)/2}D(x_k)(x_k-x^*)$ must be shown negligible. That uses the mean-square rate of Proposition 2, which rests on an estimate-sequence analysis of the accelerated method with noise (Lemma 2), not on a contraction argument; the natural first idea, a one-step contraction of $\|x_k-x^*\|$, fails for the momentum iteration.

Formalization scope

• $\mathbb R^m$ is EuclideanSpace ℝ (Fin m), $\mathbb R^{2m}$ is EuclideanSpace ℝ (Fin m ⊕ Fin m) with the first summand as the first block, block matrices are built with Matrix.fromBlocks, and $\nabla f$ is Mathlib's gradient.
• The noise is abstract: any $\mathcal F_{k+1}$-measurable, square-integrable $w_k$ with (5). The paper's sampled noise (3) is an instance, and the paper uses nothing else about it.
• $\rho$ is the spectral radius over $\mathbb C$, valued in $[0,\infty]$. Convergence in distribution is TendstoInDistribution and $N(0,\Sigma)$ is multivariateGaussian 0 Σ. Every series $\sum_t P^tC(P^t)^T$ is accompanied by a summability claim, since an unsummable tsum is $0$.
• Expectations of nonnegative quantities are lower Lebesgue integrals. Condition (31) is written with $\forall\varepsilon\,\exists R$ rather than a real supremum, which would be $0$ on an unbounded family.
• At $k=0$ the term $y_{k-1}$ reads $y_0$, which does not affect the limit.
• The step $\beta=(1-\gamma)/(1+\gamma)$ may be $0$ (when $\alpha\eta=1$), and the statements cover that case.

Infrastructure that a complete development needs and that is reusable beyond this mission: the multivariate martingale CLT for triangular arrays (Lemma 6), Gelfand-type bounds for real matrices (Lemma 10, with Mathlib's Banach-algebra Gelfand formula as the starting point), the CLT for linear recursions (Lemma 7), and the noisy estimate-sequence bound for Nesterov's method (Lemma 2). Contributions to any milestone are welcome, as are alternative proofs of the milestones' statements.

Selected references

• J. Lei, U. V. Shanbhag, Variance-Reduced Accelerated First-order Methods: Central Limit Theorems and Confidence Statements, arXiv:2006.07769v3, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2006.07769
• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM Journal on Control and Optimization 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Many stocked goods can be thrown out and restarted: a water reservoir that becomes contaminated, a product line that is replaced, perishable stock that is discarded. In each case a manager decides each period how much to order and also whether to reset, that is, discard the whole stock and start again from empty. Lee, Mintz, Aswani, Shen and Yang (arXiv:2209.03571, later in Manufacturing & Service Operations Management, 2025) study this decision. Reset control for local water storage was introduced and studied numerically by Mintz, Shen and Aswani (IEEE CDC 2017, cited by the paper as Mintz et al. 2017), whose dynamic programming equations (Proposition 1 of the paper) are the starting point here. The main theorem of Lee et al. says when the optimal policy has a simple threshold form.

Classical inventory theory has an answer for the problem without resets. Scarf (1959) showed that an $(s,S)$ policy is optimal when the cost-to-go is $K$-convex: order up to $S$ when the stock falls below $s$, otherwise do nothing. The reset option breaks this argument. The value function becomes a minimum of a convex no-reset cost and a concave reset cost, which is neither convex nor $K$-convex.

Setting

The stock $x\in[0,c_{\max}]$ is reviewed every period, and $t$ counts the periods since the last reset. In each period the manager chooses a reset flag $r\in\{0,1\}$ and an order $u\ge0$.

• A reset discards the stock at the expected cost $R(x,t)$ and returns the system to $(\zeta,0)=(0,0)$. A reset is forced at age $t=k$.
• An order $u$ is feasible if $0\le u\le c_{\max}-\xi$, where $\xi$ is the stock after the reset decision.
• The expected stage cost is $c\,u+K\cdot\mathbf 1\{u>0\}+H(\xi+u,t)$.
• The demand $w$ has density $f$, and unmet demand is lost: $x'=(\xi+u-w)^+$.
• The discount factor is $\gamma\in[0,1)$.

With $J_0=J(0,0)$, the value function solves the dynamic programming equations (22):

$$J(x,t)=\min\Big\{J_0+R(x,t),\ \min_{0\le u\le c_{\max}-x}\ c\,u+K\mathbf 1\{u>0\}+H(x+u,t)+\gamma\,\mathbb E\,J\big((x+u-w)^+,t+1\big)\Big\}$$

for $t<k$, $J(x,k)=J_0+R(x,k)$, and $J_0$ is the minimal order value from $(0,0)$.

The assumptions are as follows.

• A2: $|\partial_xH(\cdot,t)|\le\kappa_t$ and $\partial_{xx}H(\cdot,t)\ge m_t>0$.
• A3: $R(\cdot,t)$ is concave and non-decreasing, with $|\partial_xR|\le\eta_t$ and $\partial_xR$ Lipschitz.
• A5: $f$ vanishes on $(-\infty,0)$, is $L$-Lipschitz on $[0,\infty)$ and bounded by $P$ there.

The four-threshold policy (23) with thresholds $0\le\sigma_t\le s_t\le\Sigma_t\le+\infty$, level $S_t$ and reset order $\varphi$ acts as follows:

• on $[0,\sigma_t)$, reset and order $\varphi$;
• on $[\sigma_t,s_t)$, order up to $S_t$;
• on $[s_t,\Sigma_t)$, do nothing;
• from $\Sigma_t$ on, reset and order $\varphi$.

Formalization targets

Goal: Theorem 1 (p.21)

Suppose

$$0\le\gamma\le\min_t\gamma_t,\qquad \gamma_{k-1}=\frac{m_{k-1}}{(Lc_{\max}+P)\eta_k},\qquad \gamma_t=\frac{m_t}{(Lc_{\max}+P)(\eta_{t+1}+c+\kappa_{t+1})+m_{t+1}} .$$

Then, for every solution $J$ of (22) and every age $t<k$, the policy (23) attains the minimum in (22) at every stock level, and $J(\cdot,t)$ has the four-piece form (28). Each piece has a continuous derivative bounded by

$$M_t=\eta_t+c+\kappa_t+\frac{m_t}{Lc_{\max}+P},$$

which is Lipschitz for the reset and order-up-to pieces, and for the do-nothing piece when $\partial_xH(\cdot,t)$ is.

Milestones

The milestones are the paper's own chain, in proof order:

• Lemma 2: the Lipschitz constant of a convolution with a density that may jump at $0$.
• Proposition 2: under Assumption T (piecewise $C^1$, derivative $\le M_{t+1}$), $z\mapsto\mathbb E\,J((z-w)^+,t+1)$ has a derivative bounded by $M_{t+1}$ and $(Lc_{\max}+P)M_{t+1}$-Lipschitz.
• Lemma 1: a function with derivative at least $M$, plus $\lambda$ times an $L$-Lipschitz function, is non-decreasing for $\lambda L\le M$.
• Proposition 3: $G(z,t)=cz+H(z,t)+\gamma\,\mathbb E J((z-w)^+,t+1)$ is convex on $[0,c_{\max}]$ when $\gamma(Lc_{\max}+P)M_{t+1}\le m_t$.
• Proposition 4: the $(s,S)$ lemma for a continuous convex function on the closed interval $[0,c_{\max}]$.
• Proposition 5: the four-stage structure of an optimal policy.
• Proposition 6: the form (28) and the derivative bound $M_t$.

Significance

The theorem reduces a two-dimensional control (reset and order) on a continuous state to four numbers per age. This is what makes the bisection-type computation of the paper's §4 possible, and it gives managers an interpretable rule for water storage and retail product lines. It also shows a way around the failure of $K$-convexity: a small discount factor lets strong convexity of the stage cost absorb the curvature that discounting passes back.

The result is proved in the paper; nothing in this mission is open mathematically. No part of it has been machine-checked before. The remaining work is the formalization: the differentiation under the integral sign for piecewise $C^1$ integrands, the convolution estimates, the closed-interval $(s,S)$ lemma, the case analysis of Proposition 5 (Figure 6, p.35) and the backward induction carrying the constants $M_t$. One clause of the paper is false as printed and is corrected here: "each piece has a Lipschitz derivative" fails when $\partial_{xx}H$ is unbounded, which Assumption 2 allows. The formal statements keep the continuous derivative and the bound $M_t$ unconditionally, keep the Lipschitz claim unconditionally for the reset and order-up-to pieces, and assert it for the do-nothing piece when $\partial_xH(\cdot,t)$ is Lipschitz.

Difficulty

The obvious argument is Scarf's: show that $J(\cdot,t+1)$ is $K$-convex and conclude $(s,S)$ optimality. It fails at the first step. The reset branch $J_0+R(x,t)$ is concave, so its minimum with the no-reset branch has kinks pointing the wrong way, and no convexity notion survives the induction. The paper instead carries smoothness: piecewise $C^1$ with an explicit derivative bound. It recovers convexity of $G$ only after taking the expectation, which needs the demand density's Lipschitz constant and sup norm. Keeping track of the constants through the induction is the point of (29). A second difficulty is the region bookkeeping. The no-reset set is an interval $[\sigma_t,\sigma'_t]$, and the order threshold must be placed relative to it. In one sub-case the paper's own choice $s_t=s'_t$ overlaps the reset region and has to be adjusted.

Formalization scope

• States and orders. States are real numbers in $[0,c_{\max}]$. The dynamic programming equations are a hypothesis on $J:\mathbb R\times\mathbb N\to\mathbb R$, with every minimum stated as attained (IsLeast). "Optimal" means attaining the minimum in (22). Proposition 1, which links (22) to the stochastic control problem, is cited by the paper and not formalized.
• Costs and demand. Costs enter through $c,K,H,R$. Expectations are Lebesgue integrals against the density $f$, which is a probability density (the published FDivToolkit.IsDensity).
• Derivatives. All derivatives are taken within $[0,c_{\max}]$, one-sided at the ends, as the paper's retail example requires, and are named explicitly so that no junk value of deriv enters.
• Thresholds and bounds. Thresholds are extended reals and existential, with $+\infty$ allowed. The discount bounds are written multiplicatively, which avoids division by zero.
• Assumption T. It is used without its Lipschitz requirement, which the proofs never need.
• Ruled out. The DP hypothesis is not vacuous: a verification file builds an instance satisfying every hypothesis of Theorem 1 together with a solution of (22).

The development needs Mathlib's one-dimensional calculus (HasDerivWithinAt, convexity from a monotone derivative), parametric integrals, and convolution bounds. Lemma 2, Lemma 1 and Proposition 4 are reusable beyond this mission, for any $(s,S)$ argument on a bounded interval or any smoothing-by-convolution estimate. Contributions to any milestone are welcome, and Proposition 2 is the analytic core.

Selected references

• Y. Lee, Y. Mintz, A. Aswani, Z.-J. M. Shen, C. Yang, Optimal Policy for Inventory Management with Periodic and Controlled Resets, arXiv:2209.03571v1, 2022; Manufacturing & Service Operations Management, 2025. https://arxiv.org/abs/2209.03571
• Y. Mintz, Z. Shen, A. Aswani, Local water storage control for the developing world, 2017 IEEE 56th Conference on Decision and Control (CDC), 5074–5079, 2017 (as cited by the paper).
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, Technical report, Stanford University, 1959 (as cited by the paper).
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, Athena Scientific, 1995 (Lemma 4.2.1).

Why restless bandits, and why this assumption

A restless bandit couples $N$ identical Markov decision processes through a budget: at every time step exactly $\alpha N$ of the $N$ arms must be pulled, and every arm changes state whether it is pulled or not. The model, introduced by Whittle (1988), describes scheduling of machines or patients, sensor management, queueing control and recommendation. Computing an optimal policy is PSPACE-hard (Papadimitriou and Tsitsiklis, 1999), so the research question is asymptotic optimality: a policy whose average reward approaches the optimum as $N\to\infty$.

Timeline of the assumptions under which asymptotic optimality was known, as surveyed in §2 of the paper:

• Whittle index, Weber and Weiss (1990): asymptotically optimal in continuous time under indexability, a unichain condition on the $N$-armed system under every policy, and the global attractor property (GAP) of a fluid limit.
• LP-priority policies, Verloop (2016): indexability removed; the unichain condition and GAP remain.
• Follow-the-virtual-advice (FTVA), Hong, Xie, Chen, Wang (2023): discrete time, GAP replaced by a synchronization assumption (SA), with an $O(1/\sqrt N)$ gap.
• This paper, Hong, Xie, Chen, Wang, arXiv:2402.05689v4: only that the optimal single-armed policy induces an aperiodic unichain, with an $O(1/\sqrt N)$ gap. Neither GAP nor SA is assumed; Appendix B.2 of the paper shows that aperiodicity cannot simply be dropped.

The model

The single-armed MDP is $(\mathbb S,\mathbb A,P,r)$ with a finite state space $\mathbb S$, actions $\mathbb A=\{0,1\}$ (1 = pull), transition probabilities $P(s,a,s')$ and rewards $r(s,a)$. Let $r_{\max}=\max_{s,a}|r(s,a)|$, $0<\alpha<1$ with $\alpha N$ an integer, and $\beta=\min\{\alpha,1-\alpha\}$.

A policy for the $N$-armed problem chooses, from the whole history, a random action vector that pulls exactly $\alpha N$ arms; given the actions, the arms move independently. Its liminf average reward is

$$R^-(\pi,S_0)=\liminf_{T\to\infty}\frac1{NT}\sum_{t<T}\sum_{i\in[N]}\mathbb E\,r\big(S_t(i),A_t(i)\big),$$

and the optimal reward $R^*(N,S_0)$ is its supremum over all policies.

The LP relaxation maximizes $\sum_{s,a}r(s,a)y(s,a)$ over stationary state-action distributions $y$ with $\sum_s y(s,1)=\alpha$; its value is $R^{\mathrm{rel}}$. An optimal $y^*$ defines the optimal single-armed policy $\bar\pi^*(a\mid s)=y^*(s,a)/(y^*(s,0)+y^*(s,1))$ (and $1/2$ if the denominator is $0$), the matrix $P_{\bar\pi^*}$ and its stationary distribution $\mu^*(s)=y^*(s,0)+y^*(s,1)$. Assumption 1 asks that $P_{\bar\pi^*}$ have a single recurrent class, which is aperiodic.

For $D\subseteq[N]$, $x(D,s)$ is the number of arms of $D$ in state $s$ divided by $N$, and $m(D)=|D|/N$. A focus-set policy samples an ideal action $\hat A_t(i)\sim\bar\pi^*(\cdot\mid S_t(i))$ for every arm, picks a focus set $D_t$, and lets as many arms of $D_t$ follow their ideal actions as the budget allows. The set-expansion policy chooses $D_t$ of largest size among the sets with nonnegative slack

$$\delta(x,D)=\beta(1-m(D))-\tfrac12\|x(D)-m(D)\mu^*\|_1,$$

growing $D_{t-1}$ when its slack is positive and shrinking it otherwise. The constant of the main bound involves

$$W=\sum_{k\ge0}(P_{\bar\pi^*}-\Xi)^k(P_{\bar\pi^*}^\top-\Xi^\top)^k,$$

where $\Xi$ has every row equal to $\mu^*$, and its largest eigenvalue $\lambda_W$.

Formalization targets

Goal: Theorem 1 with its explicit constant

$$R^*(N,S_0)-R^-(\pi,S_0)\le\frac{256\,r_{\max}\,\lambda_W^2\,|\mathbb S|^2}{\beta^2\sqrt N}$$

for every $N\ge1$ with $\alpha N\in\mathbb N$ and every initial state vector $S_0$. Theorem 1 states $C_{\mathrm{SE}}/\sqrt N$ and gives $C_{\mathrm{SE}}$ in its proof (p.18).

Milestones, in proof order

• $W$ converges, is positive definite, and $W\succeq I$ (Lemma 11).
• Pseudo-contraction $\|vP_{\bar\pi^*}-\mu^*\|_W\le(1-\frac1{2\lambda_W})\|v-\mu^*\|_W$ (Lemma 1).
• $h_W(x,D)=\|x(D)-m(D)\mu^*\|_W$ satisfies drift, distance domination and Lipschitz bounds (Lemma 2).
• $L_1$ non-expansiveness and one-step concentration (Lemmas 12, 13).
• The set-expansion policy satisfies majority conformity, almost non-shrinking and sufficient coverage (Lemmas 3, 4, 5).
• The meta-theorem: these three conditions give an $O(1/\sqrt N)$ gap with explicit constants (Theorem 5).
• $R^{\mathrm{rel}}\ge R^*(N,S_0)$ (Lemma 10), and $R^{\mathrm{rel}}-R^-(\pi,S_0)\le 256\,r_{\max}\lambda_W^2|\mathbb S|^2/(\beta^2\sqrt N)$ (closing display of the proof of Theorem 1).

What the result gives

The theorem gives the first asymptotic optimality guarantee for average-reward restless bandits under an assumption that can be checked on the single-armed LP solution alone. The $O(1/\sqrt N)$ rate holds for every finite $N$ and every initial state, not only in the limit, and the constant depends only on the problem data and on the mixing of $P_{\bar\pi^*}$ through $\lambda_W$. The meta-theorem (Theorem 5) is a reusable tool: any focus-set policy satisfying its three conditions inherits the same rate, which is how the paper also treats its ID policy.

The result is proved in the paper, which appeared in Mathematics of Operations Research (2025). No machine-checked proof of it, or of any of its milestones, is known. The formalization would check the full chain: the Lyapunov-equation matrix of a finite aperiodic unichain, concentration of empirical state counts, the bivariate drift argument without a stationary distribution, and the LP upper bound for history-dependent policies.

Where the difficulty lies

The obvious first idea is a Lyapunov argument on the whole system state $X_t([N])$. It fails because the budget prevents all arms from following $\bar\pi^*$, so the full state need not drift towards $\mu^*$: this is where GAP or SA were used before. The paper's way around it is a Lyapunov function $h(x,D)$ indexed by a moving subset; the difficulty moves to controlling how $D_t$ changes. Lemma 4, which shows that the focus set almost never shrinks, needs a combinatorial construction of a large admissible subset after the slack turns negative. The meta-theorem must turn a drift inequality for $h(X_t,D_t)+L_h(1-m(D_t))$ into a long-run average bound without assuming that the focus-set chain has a unique stationary distribution (Appendix D). Lemma 10 needs the occupation-measure argument over all history-dependent policies with a liminf objective.

Formalization scope

Arms are Fin N; $k=\alpha N$ is a natural number with (k : ℝ) = α * N. Laws on finite sets are real probability vectors; the history law of a policy and the law of the focus-set chain $(X_t,D_{t-1})$ are defined recursively in $t$. $R^-$ is a Filter.liminf of Cesàro averages, $R^*$ a supremum over history-dependent randomized policies, and $R^{\mathrm{rel}}$ a supremum of the LP objective over its feasible set. $W$ is a tsum of real matrices and $\lambda_W$ its maximal Rayleigh quotient. Aperiodic unichain constrains recurrent states only, reusing the published Reaches and IsRecurrentState. The set-expansion policy is any focus-set process whose update obeys Algorithm 2's lines 2–5 and whose rectifier obeys Algorithm 1's (4)–(5), which contains Algorithm 2's uniform tie-breaking.

A tsum that does not converge is 0 in Lean, which would make $\lambda_W=0$ and the bound trivially $0$: every statement using $W$ assumes Assumption 1, under which the series converges (Lemma 11). $R^*$ is not a junk supremum: the policy class is nonempty and every $R^-$ lies in $[-r_{\max},r_{\max}]$ (proved in the sanity checks).

Reusable beyond this mission: the history-dependent policy class and $R^-$ for weakly coupled MDPs, the matrix $W$ of a finite aperiodic unichain and its contraction, and the LP relaxation bound. Contributions are welcome on any milestone, and on general Mathlib facts they need: convergence of $P^k$ for finite aperiodic unichains, and Cauchy–Schwarz bounds for sums of independent bounded vectors.

Selected references

• Y. Hong, Q. Xie, Y. Chen, W. Wang, Unichain and Aperiodicity are Sufficient for Asymptotic Optimality of Average-Reward Restless Bandits, arXiv:2402.05689v4, 2026; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2402.05689
• P. Whittle, Restless bandits: activity allocation in a changing world, Journal of Applied Probability 25A, 1988. https://doi.org/10.2307/3214163
• R. R. Weber, G. Weiss, On an index policy for restless bandits, Journal of Applied Probability 27(3), 1990. https://doi.org/10.2307/3214547
• C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queuing network control, Mathematics of Operations Research 24(2), 1999. https://doi.org/10.1287/moor.24.2.293
• I. M. Verloop, Asymptotically optimal priority policies for indexable and nonindexable restless bandits, Annals of Applied Probability 26(4), 2016. https://doi.org/10.1214/15-AAP1137
• Y. Hong, Q. Xie, Y. Chen, W. Wang, Restless bandits with average reward: breaking the uniform global attractor assumption, NeurIPS 2023. https://arxiv.org/abs/2306.00196
• M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

MaxWeight is the standard scheduling rule for switched queueing networks, used to model input-queued switches, wireless networks and data centers. In each time unit it picks, among the feasible service vectors $\sigma\in\mathcal S$, one that maximizes $\sum_j Q_j\sigma_j$, where $Q_j$ is the length of queue $j$. For single-hop networks, where every job leaves after one service, Tassiulas and Ephremides showed that MaxWeight is maximally stable: the queue process is positive recurrent whenever the load lies in the interior of the capacity region (Tassiulas–Ephremides 1992). Whether the same holds for multihop networks, where served jobs move on to other queues, was open.

Bramson, D'Auria and Walton (arXiv:1909.10825, Math. Oper. Res. 2021) answer it negatively. They give an explicit two-component network in which the load is subcritical but the MaxWeight queue process is transient. Their paper describes this as the first proof of transience of MaxWeight under subcritical arrival rates (p.2). The same paper shows that a weighted MaxWeight policy is maximally stable (Theorem 2), which this mission does not formalize.

Timeline:

• 1992: Tassiulas and Ephremides prove that MaxWeight (back-pressure) is maximally stable for single-hop networks and, with back-pressure weights, for multihop routing.
• 1991–1992: Lu–Kumar and Rybko–Stolyar give subcritical networks that are unstable under priority disciplines. The present proof uses the same cycle argument.
• 2021: Bramson, D'Auria and Walton prove Theorem 1, that plain MaxWeight is transient on the network of Figure 1.

Setting

The network has $2J+2$ queues in two components $\mathcal A=\{\mathcal A_0,\dots,\mathcal A_J\}$ and $\mathcal B=\{\mathcal B_0,\dots,\mathcal B_J\}$. Time is discrete and jobs are unit sized. In each time unit, each of the $2J$ externally fed queues $\mathcal A_j,\mathcal B_j$ ($j\ge1$) receives one external arrival with probability $a/J$, independently of the other queues and of the past. A job served at $\mathcal A_j$ ($j\ge1$) moves to $\mathcal B_0$, a job served at $\mathcal B_j$ moves to $\mathcal A_0$, and jobs served at $\mathcal A_0$ or $\mathcal B_0$ leave. The traffic intensity is $\rho_{\mathcal A_0}=\rho_{\mathcal B_0}=a$ and $\rho_{\mathcal A_j}=\rho_{\mathcal B_j}=a/J$.

For $\nu\in\mathbb N$, a schedule $\sigma\in\mathbb Z_+^{2J+2}$ is feasible when

$$\sigma_{\mathcal A_0}+\frac1\nu\sum_{j=1}^J\sigma_{\mathcal A_j}\le1,\qquad \sigma_{\mathcal B_0}+\frac1\nu\sum_{j=1}^J\sigma_{\mathcal B_j}\le1 .$$

So in each time unit each component serves either up to $\nu$ jobs from its externally fed queues or one job from its internal queue. The subcritical region $\mathcal C$ is the interior of the convex hull of $\mathcal S$. Under MaxWeight, the schedule $\sigma(t)$ of time unit $t$ maximizes $\sum_jQ_j(t-1)\sigma_j$ over $\mathcal S$, with ties broken arbitrarily or at random. Each queue serves $\sigma_j\wedge Q_j(t-1)$ jobs, and the served jobs and the new arrivals then join their queues. The queue lengths $Q(t)\in\mathbb Z_+^{2J+2}$ form a countable-state Markov chain, and $Q^\Sigma_{\mathcal A}$, $Q^\Sigma_{\mathcal B}$ denote the component totals.

Formalization targets

Goal: Theorem 1

Assume $r_{\boldsymbol\rho}:=a(1+1/\nu)<1$ (4) and

$$1<\nu<J,\qquad \frac{J}{2J-\nu}<a<1-\frac{(J+\nu)(J+\nu^2)}{\nu(J^2+J+\nu^2)} . \tag{5}$$

Then

$$\boldsymbol\rho\in\mathcal C\quad\text{and every state of the MaxWeight queue process is transient,}$$

for every tie rule. One admissible choice is $a=7/12$, $\nu=6$, $J=30$.

Milestones

1. Lemma 1 and display (16): uniform concentration of the arrival counts over all windows of $[0,T]$, and $\mathbb P(G_M)\ge1-e^{-\eta T}$.
2. Lemmas 2–7: pathwise statements for MaxWeight trajectories with arrivals in $G_M$, started in $\mathcal I_M$ ($M$ jobs at a balanced $\mathcal B$, few at $\mathcal A$). They cover the emptying time $U$ of $\mathcal B$, the feed into $\mathcal A_0$, the starvation of $\mathcal A_1,\dots,\mathcal A_J$, their balance, the emptiness of $\mathcal B$ on $[U,V]$, and the time $V$ and the mass $Q^\Sigma_{\mathcal A}(V)$.
3. Proposition 1: at time $V$ the mirror image of $\mathcal I_M$ holds with $M'=\gamma M$, $\gamma>1$, and the total never drops below $\tfrac12\tfrac{a}{a+\nu}M$ before $V$.
4. The iteration bound of the proof of Theorem 1: from $\mathcal I_M$ the total falls below $\tfrac12\tfrac{a}{a+\nu}M$ with probability at most $\sum_k e^{-\eta\gamma^kT}$.
5. $\boldsymbol\rho\in\mathcal C$ under (4), and a corrected closing step: every state leads to the empty state, and the empty state leads into $\mathcal I_M$ for arbitrarily large $M$.

Significance

The theorem shows that MaxWeight, the default throughput-optimal policy for single-hop switched networks, is not maximally stable once jobs are routed through several queues. A stability guarantee for multihop networks therefore needs a modified policy, such as the weighted MaxWeight of Theorem 2 of the same paper or back-pressure. The example is explicit and holds for an open set of parameters, so the instability is not an artifact of a boundary case.

The result is proved on paper. No machine-checked proof of it is known. A formalization would contribute a Lean model of discrete-time switched networks under MaxWeight with arbitrary tie rules, the large-deviation estimate for Bernoulli counts over all windows, a complete pathwise cycle analysis in the style of Lu–Kumar and Rybko–Stolyar, and a transience proof for a chain that is not irreducible. The printed proof ends with "since all states communicate", which is false: a state with two jobs at $\mathcal A_1$ and nothing else has no predecessor. The mission replaces that step with a milestone that is true.

Difficulty

The obvious argument is a drift argument: since $\boldsymbol\rho\in\mathcal C$, one looks for a Lyapunov function whose drift is negative. No such function exists here. The work grows only over a full cycle, in which component $\mathcal B$ drains into $\mathcal A_0$ while MaxWeight keeps serving $\mathcal A_0$ (one job per unit) instead of the externally fed queues $\mathcal A_j$ (up to $\nu$ per unit), and then the roles of $\mathcal A$ and $\mathcal B$ swap. Proving this requires tracking several queue groups simultaneously over $[0,U]$, $[U\wedge\varepsilon\kappa_2M,V)$ and $[U,V]$, with constants that depend only on $a,J,\nu,\gamma$, chosen before $\varepsilon$, and with $M$ large depending on $\varepsilon$. The probabilistic step then iterates the cycle with the strong Markov property at the stopping time $V$, using the $\mathcal A\leftrightarrow\mathcal B$ symmetry. The final step from "never empties with positive probability" to "every state is transient" needs a communication argument, because the chain is not irreducible.

Formalization scope

• State space $\mathbb Z_+^{2J+2}$ as functions on $\{0,\dots,J\}\sqcup\{0,\dots,J\}$; the left copy is $\mathcal A$, index $0$ is the internal queue. Schedule constraint (3) multiplied by $\nu$ over $\mathbb N$.
• One time unit: serve $\sigma_j\wedge Q_j$ with $\sigma$ a MaxWeight schedule for the current state (the maximum is over all of $\mathcal S$, not capped by $Q$), route, then add arrivals. Arrivals are independent Bernoulli$(a/J)$ at each of the $2J$ external queues.
• Tie rules: every state-dependent distribution on schedules supported on the maximizers. Deterministic rules are the point-mass case. All statements hold for every tie rule.
• Transience: the published countable-chain definitions (MatrixAnalytic_Stability_Chain, referenced), with IsTransientChain meaning that no state is recurrent. Fixing one tie rule, assuming irreducibility, or proving only that some state is transient would each give a weaker theorem.
• Lemmas 2–7 and Proposition 1 are stated for every MaxWeight sample path whose arrivals satisfy (15). $U$ and $V$ are integer first-hitting times capped at $\lceil T\rceil$, so $Q(U)$ and $Q(V)$ are defined.
• $\mathcal C$ is the interior of the convex hull of $\mathcal S$ in $\mathbb R^{2J+2}$.

Contributions of any milestone are welcome. Lemma 1 and the kernel/communication facts can be reused for other discrete-time queueing models.

Selected references

• M. Bramson, B. D'Auria, N. Walton, Stability and Instability of the MaxWeight Policy, arXiv:1909.10825v2, 2021; Math. Oper. Res. 46(4), 2021. https://arxiv.org/abs/1909.10825
• L. Tassiulas, A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Trans. Automatic Control 37(12), 1992. https://doi.org/10.1109/9.182479
• S. H. Lu, P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Trans. Automatic Control 36(12), 1991. https://doi.org/10.1109/9.106159
• A. N. Rybko, A. L. Stolyar, Ergodicity of stochastic processes describing the operation of open queueing networks, Problems of Information Transmission 28(3), 1992.
• M. Bramson, Stability of Queueing Networks, Lecture Notes in Mathematics 1950, Springer, 2008. https://doi.org/10.1007/978-3-540-68896-9

Online decisions with an imperfect forecast

Many revenue management, online advertising and online linear programming problems share one form. Requests arrive one at a time, each must be answered at once, and every answer uses up part of a fixed budget. Algorithms of this kind are usually analyzed in one of two regimes: requests drawn i.i.d. from one law, or requests chosen by an adversary. For an adversary, no algorithm has sublinear regret against the offline optimum. Real demand lies between the two, since it is nonstationary, but forecasts are available.

Jiang, Li and Zhang (arXiv:2012.06961v3) measure the quality of a forecast by a Wasserstein budget and show that regret is governed by that budget. The earlier nonstationarity measure of Besbes, Gur and Zeevi (arXiv:1307.5449) was built on a variation functional and applies to unconstrained problems. Balseiro, Lu and Mirrokni (arXiv:2011.10124) consider total variation distance. The mission's target is Theorem 3 of the paper, the upper bound. The matching lower bound, Theorem 2 there, is not in scope.

Setting

Let $\mathcal X\subset\mathbb R^k$ be compact and convex with $0\in\mathcal X$. For each type $\theta\in\Theta$ there is a concave reward $f(x;\theta)$ and convex consumptions $g_i(x;\theta)$, $i=1,\dots,m$. Over $T$ periods a type $\theta_t$ is drawn independently from an unknown law $\mathcal P_t$ and revealed. The decision maker then picks $x_t\in\mathcal X$, subject to a total budget $c\ge0$. The types are compared by what they do:

$$\rho(\theta,\theta')=\sup_{x\in\mathcal X}\|(f(x;\theta),g(x;\theta))-(f(x;\theta'),g(x;\theta'))\|_\infty .$$

The Wasserstein distance $\mathcal W(\mathcal Q_1,\mathcal Q_2)$ is the infimum of $\int\rho\,d\pi$ over couplings $\pi$ of $\mathcal Q_1,\mathcal Q_2$, and the deviation budget of the truth from a prior $\hat{\mathcal P}$ is $\sum_t\mathcal W(\mathcal P_t,\hat{\mathcal P}_t)$.

Write $h(p;\theta)=\max_{x\in\mathcal X}\{f(x;\theta)-p^\top g(x;\theta)\}$ and $\hat L(p)=p^\top c+\sum_t\hat{\mathcal P}_t h(p;\theta)$. A fluid plan is a price $\hat p^*\ge0$ with a measurable maximizer $\hat x(\theta)$ of the Lagrangian at $\hat p^*$, such that the per-period consumptions $\hat\gamma_t=\hat{\mathcal P}_t\,g(\hat x(\theta);\theta)$ fit the budget and are complementary to $\hat p^*$. The algorithm IGD($\hat\gamma$) keeps a price $p_t$ with $p_1=0$. It computes the maximizer $\tilde x_t$ of the Lagrangian at $p_t$, takes $x_t=\tilde x_t$ if the remaining budget allows it and $x_t=0$ otherwise, and updates $p_{t+1}=(p_t+\tfrac1{\sqrt T}(g(\tilde x_t;\theta_t)-\hat\gamma_t))\vee0$. Regret compares $R_T(\pi)=\sum_t f(x_t;\theta_t)$ with the offline optimum $R^*_T$ of the program that knows $\theta_1,\dots,\theta_T$.

Formalization targets

Goal: Theorem 3

For all $T\ge1$, $c\ge0$ and all priors, $\hat L$ has a minimizer, every minimizer extends to a fluid plan, a measurable tie-break rule exists, and for every plan, every rule and every $\mathcal P$ with $\sum_t\mathcal W(\mathcal P_t,\hat{\mathcal P}_t)\le W_T$,

$$\mathbb E[R^*_T-R_T(\pi)]\le\Bigl(\frac m2+mq(q+1)\Bigr)\sqrt T+qm+2(q+1)(m+1)W_T\le C\max\{\sqrt T,W_T\},$$

with $C$ depending only on $m$ and on the reward-to-consumption ratio $q$ of Assumption 1.

Milestones

In the order of the proof: existence of the plan and of the tie-break rule; integrability of the regret; Lemma 1 and the dual bound $\mathbb E[R^*_T]\le L(p)$; the reward gap of virtual actions and the regret decomposition; Lemma 3, which is the Wasserstein Lipschitz bound on $L_{\mathcal Q}$; the bound on $\hat p^*$; Lemmas 5 and 4; the one-step dual inequalities; and displays (32) and (33).

Significance

The bound separates two costs: $\sqrt T$ is the price of randomness, and $W_T$ is the price of a wrong forecast. With Theorem 2 of the paper the rate is optimal, and the algorithm needs no knowledge of $W_T$. So the same run is valid for every law in the ball around the prior.

On the formal side, the theorem is proved in the paper, and to our knowledge it has no machine-checked proof; a search of the platform found none. A complete development gives a primal-dual online allocation analysis, reusable for other budget-constrained online problems, and a Wasserstein estimate for dual functions on a general metric space. The formal statement also records two corrections to the source. The first adds $f(0;\theta)\ge0$, which the printed proofs use tacitly. The second requires a complementary tie-break in (10): with a free choice among maximizers the regret can be linear. Each comes with a counterexample in the items. The paper does not prove the existence of a complementary plan, and this mission does ask for it.

Difficulty

Most of the regret bound is direct once its objects exist, but three steps are not. The obvious reading of (10), any maximizer at $\hat p^*$, fails at ties. Showing that a complementary maximizer exists for every minimizer of $\hat L$, measurably in $\theta$, is the hardest item. It needs a directional derivative of an integral of maxima, and convexity to turn a mixture of maximizers back into a single action. The measure theory is also real: $\Theta$ is not assumed complete, so an optimal coupling need not exist, and the offline value is a parametric maximum whose measurability must be proved. Finally, the independence of $p_t$ and $\theta_t$ has to be extracted from the structure of the run.

Formalization scope

$\mathcal X$ is a subset of Fin k → ℝ, and Model carries $f,g$, which are typed on all of $\mathbb R^k$ with every hypothesis on $\mathcal X$. $\Theta$ is a MetricSpace with BorelSpace, and DistEqRho says its distance is $\rho$. Separability of $\Theta$ and measurability of $f,g$ in $\theta$ are lemmas to prove, not hypotheses. The product law Measure.pi encodes independence. $\mathcal W$ is valued in ℝ≥0∞ and uses the published WassersteinDRO.StrongDuality.couplings. $R^*_T$, $R^{UB}_T$ and $h$ are real sSups over nonempty bounded sets. The run is a recursion on a natural number with price … 0 equal to $p_1$, and it reads the profile at index $t$ only, so it cannot anticipate. A tie-break rule is any jointly measurable selection, and the bound holds for all of them.

The goal states integrability explicitly, because a Bochner integral of a non-integrable function is $0$, and clause (a) of the goal makes the statement non-vacuous. The policy is the actual run of Algorithm 1, and the constants are fixed before the instance, so neither can trivialize the bound.

A complete development needs measurable selection for compact-valued maps, Danskin-type derivatives, and Fubini on Measure.pi. Selection and the Wasserstein estimate are reusable beyond this mission. Contributions to any milestone, or more general lemmas that imply one, are welcome.

Selected references

• J. Jiang, X. Li, J. Zhang, Online Stochastic Optimization with Wasserstein Based Non-stationarity, arXiv:2012.06961v3, 2022; later published as Online Stochastic Optimization with Wasserstein-Based Nonstationarity, Management Science, 2025. https://arxiv.org/abs/2012.06961
• O. Besbes, Y. Gur, A. Zeevi, Non-stationary Stochastic Optimization, Operations Research 63(5), 2015. https://arxiv.org/abs/1307.5449
• S. Balseiro, H. Lu, V. Mirrokni, The Best of Many Worlds: Dual Mirror Descent for Online Allocation Problems, 2020. https://arxiv.org/abs/2011.10124
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999

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