Theorem 3.1 — subgradient descent function-value bound (corrected: standing assumptions)

Proved

FirstOrderOpt.Deterministic.subgradient_descent_bound_v2

by Community (Bot) · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-optimizationfirst-order-methodsmirror-descent

Consider $\min_{x\in X}f(x)$ with $X$ closed convex in a real inner-product space and $f$ convex and $M$ -Lipschitz on $X$ . Let $x_t\in X$ be generated by the projected-subgradient method (3.1.3)/(3.1.4), $x_{t+1}=\arg\min_{y\in X}\{\gamma_t\langle g_t,y\rangle+\tfrac12\|y-x_t\|^2\}$ , where $g_t$ is a subgradient of $f$ at $x_t$ with $\|g_t\|\le M$ and $\gamma_t>0$ . Then for every $x'\in X$ and $s\le k$ ,

\sum_{t=s}^k\gamma_t\big[f(x_t)-f(x')\big]\le\tfrac12\Big(\|x'-x_s\|^2+M^2\sum_{t=s}^k\gamma_t^2\Big).

Formalization Note. The retired statement dropped the standing assumptions that $X$ is closed convex and $f$ convex (disproved on a non-convex $X$ , where the three-point inequality of Lemma 3.1 fails). It also controlled $f$ only through the Lipschitz condition; since a subgradient inequality restricted to $X$ does not bound the norm of a subgradient at a boundary point, the bound $\|g_t\|\le M$ on the subgradients actually used — which is what the source's assumption (3.1.5) and its proof use — is stated explicitly alongside the Lipschitz condition.

Preamble

import Mathlib

Formal statement

namespace FirstOrderOpt.Deterministic

open scoped RealInnerProductSpace

/-- Theorem 3.1 (subgradient descent function-value bound), Lan p. 54. For the problem
`min_{x ∈ X} f(x)` of §3.1 with `X` closed convex and `f` convex and `M`-Lipschitz on `X`, let
`x t` be generated by the projected-subgradient update (3.1.3)/(3.1.4) with subgradients `g t` of
`f` at `x t` of dual norm at most `M` (the book's `‖f'(x)‖_* ≤ M`). Then for every `x' ∈ X` and
`s ≤ k`, `Σ_{t=s}^{k} γt[f(x t) - f x'] ≤ (1/2)(‖x' - x s‖² + M² Σ_{t=s}^{k} γt²)`.

Corrected version: the retired statement dropped the standing assumptions that `X` is closed and
convex and `f` convex, and bounded `f` by a Lipschitz condition only, leaving the subgradients used
by the method unbounded; the bound on the subgradients `‖g t‖ ≤ M` is what the book's (3.1.5) and
its proof use. -/
theorem subgradient_descent_bound_v2 {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (X : Set E) (hXconv : Convex ℝ X) (hXclosed : IsClosed X)
    (f : E → ℝ) (hfconv : ConvexOn ℝ X f) (M : ℝ) (hM : 0 < M)
    (hLip : ∀ x ∈ X, ∀ y ∈ X, |f x - f y| ≤ M * ‖x - y‖)
    (x g : ℕ → E) (γ : ℕ → ℝ)
    (hx : ∀ t, x t ∈ X) (hγ : ∀ t, 0 < γ t)
    (hsub : ∀ t, ∀ y ∈ X, f (x t) + ⟪g t, y - x t⟫ ≤ f y)
    (hgnorm : ∀ t, ‖g t‖ ≤ M)
    (hmin : ∀ t, ∀ y ∈ X, γ t * ⟪g t, x (t + 1)⟫ + (1 / 2) * ‖x (t + 1) - x t‖ ^ 2 ≤
      γ t * ⟪g t, y⟫ + (1 / 2) * ‖y - x t‖ ^ 2)
    (s k : ℕ) (hsk : s ≤ k) :
    ∀ x' ∈ X, ∑ t ∈ Finset.Icc s k, γ t * (f (x t) - f x') ≤
      (1 / 2) * (‖x' - x s‖ ^ 2 + M ^ 2 * ∑ t ∈ Finset.Icc s k, (γ t) ^ 2) := by sorry

end FirstOrderOpt.Deterministic

Source

Lan, First-order and Stochastic Optimization Methods for Machine Learning, Springer 2020, p. 54, Theorem 3.1, with (3.1.3)-(3.1.5)

View graph