Frank-Wolfe Beyond 1/t Convergence
Sebastian Pokutta
math.OC
Apr 30, 2026 · v3
TL;DR
The principal convergence arguments (O(1/t) rate, LDS-based o(1/t) theorems, Hölder-error-bound rates) are formally verified in Lean 4, largely via agentic auto-formalization.
Abstract
We consider smooth convex minimization over compact convex sets, i.e., $\min_{x \in C} f(x)$ with the (vanilla) Frank-Wolfe algorithm. Well-known lower bounds establish a worst-case $Ω(1/t)$ primal-gap barrier in the general smooth convex case, and faster convergence usually requires favorable function properties such as Hölder error bounds or strong convexity. We present a new Local Dual Sharpness (LDS) condition, essentially a property of the feasible region and its LMO, under which the Frank-Wolfe algorithm converges in $o(1/t)$ for any smooth convex function, ruling out an $Ω(1/t)$ lower bound under LDS. The condition is a generalization (and localization) of uniform convexity of sets and it is satisfied by any uniformly convex set. To our knowledge, this is the first unconditional $o(1/t)$ convergence result for uniformly convex sets. Combining LDS with stronger function properties, e.g., a local variant of Hölder error bounds, allows us to quantify the actual rates.
Problem
The vanilla Frank–Wolfe algorithm for smooth convex minimization over compact convex sets has a worst-case Ω(1/t) primal-gap lower bound. Faster rates usually require strong properties of the objective, such as strong convexity or Hölder error bounds.
Approach
The paper introduces a Local Dual Sharpness (LDS) condition on the feasible region and its fixed LMO selector around a reference set such as the minimizer set. LDS generalizes and localizes uniform convexity of sets. The paper proves o(1/t) convergence under LDS for short steps, exact line search, and the open-loop step-size, and obtains quantitative rates when LDS is combined with a local Hölder error bound. The principal arguments are machine-checked in Lean 4; much of the formalization was produced with an agentic auto-formalization framework and then independently checked.
Results
Under LDS, Frank–Wolfe achieves f(x_t)−f* = o(1/t) for any smooth convex objective, without extra growth assumptions. This gives the first unconditional o(1/t) result for uniformly convex sets. Under an additional local Hölder error bound of order r, the rate is O(t^{-rq/(rq-2)}), and a stadium-shaped example illustrates the behavior numerically.
