The Exact Time-Uniform Rate Frontier for Stochastic Gradient Descent on Smooth Convex Objectives
Ruijie Li, Kang Chen, Tianyu Wang
math.OC
Sep 8, 2026 · v1
cs.LG stat.ML
TL;DR
The main time-uniform SGD convergence frontier results are formalized and kernel-checked in Lean 4, with a public GitHub repository and AI-assisted translation.
Abstract
We study the time-uniform convergence of the raw iterate of standard stochastic gradient descent (SGD) for unconstrained smooth convex objectives. We prove that, under standard noise assumptions, the time-uniform convergence rate gets arbitrarily close to $\sqrt{\log n / n}$ but never reaches it. More specifically, we prove that for every positive, eventually nondecreasing sequence $h$ satisfying $h(n) = o(\sqrt{n})$, a bound of order $h(n)/\sqrt{n}$, holding simultaneously for all $n$ with probability at least $1-α$ and uniformly over the problem class, is achievable if and only if \[ \sum_{j = 1}^{\infty} \frac{1}{h(2^j)^2} < \infty. \] The constructive sufficiency result follows from a dyadic horizon-free schedule together with an additive conditional-restart inequality. The necessity counterpart applies to every deterministic nonnegative schedule and holds even for a one-dimensional analytic smooth convex objective with Gaussian noise.
Problem
The paper asks which time-uniform high-probability convergence rates h(n)/sqrt(n) the raw iterate of standard SGD can achieve on smooth convex objectives with norm-sub-Gaussian noise. The schedule must be deterministic and horizon-free, and the bound must hold simultaneously for all n.
Approach
For sufficiency, the authors build a dyadic epoch-based stepsize schedule with a constant step inside each epoch and combine it with an additive conditional-restart inequality. For necessity, they use fixed-horizon lower bounds on a one-dimensional analytic convex objective with Gaussian noise; this argument applies to every deterministic nonnegative schedule. The targeted results were translated into Lean 4 with AI assistance, checked by the Lean kernel, and audited for theorem correspondence and unintended axioms.
Results
A profile h is achievable if and only if the sum over j of 1/h(2^j)^2 is finite. Achievable rates therefore approach sqrt(log n / n) arbitrarily closely but never reach it. The Lean 4 formalization is released on GitHub together with integrity audits.
