Theorem 3.5 — mirror descent function-value bound (corrected: convex $f$ , Bregman $V$ )

Proved

FirstOrderOpt.Deterministic.mirror_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 normed space and $f$ convex on $X$ . Let $\nu$ be a distance generating function on $X$ with prox-function $V$ , and let $x_t\in X$ be generated by the mirror-descent update (3.2.5), $x_{t+1}=\arg\min_{u\in X}\{\gamma_tg_t(u)+V(x_t,u)\}$ , with $\gamma_t>0$ and $g_t$ a subgradient of $f$ at $x_t$ of dual norm $\|g_t\|_*\le M$ . If $x^*$ is an optimal solution and $\bar x_s^k=\big(\sum_{t=s}^k\gamma_t\big)^{-1}\sum_{t=s}^k\gamma_tx_t$ is the weighted average (3.1.9), then

f(\bar x_s^k)-f(x^*)\le\Big(\sum_{t=s}^k\gamma_t\Big)^{-1}\Big(V(x_s,x^*)+\tfrac12M^2\sum_{t=s}^k\gamma_t^2\Big).

Formalization Note. The retired statement assumed the subgradient inequality only at the iterates, so convexity of $f$ at the averaged point $\bar x$ (Jensen) was unavailable (disproved); $f$ convex on $X$ is the chapter's standing assumption and is now stated. The retired version took $V$ as a free function (with at most nonnegativity and a three-point identity), which admits $V\equiv 0$ ; the corrected version uses FirstOrderOpt.Prox.DistanceGeneratingFunction.V, the prox-function of a distance generating function on $X$ exactly as in §3.2. Closed convexity of $X$ is stated as well.

Preamble

import Mathlib
import Definitions.Def_FirstOrderOpt_Prox_DistanceGeneratingFunction

Formal statement

namespace FirstOrderOpt.Deterministic

open FirstOrderOpt.Prox

/-- Theorem 3.5 (mirror descent function-value bound), Lan p. 61. For `min_{x ∈ X} f(x)` with `X`
closed convex and `f` convex, let `ν` be a distance generating function on `X` with prox-function
`V = ν.V`, and let `x t` be generated by the mirror-descent update (3.2.5)
`x (t+1) = argmin_{u ∈ X} γt·gt(u) + V(x t, u)` with subgradient functionals `g t` of `f` at
`x t` of dual norm at most `M`. If `xstar` is an optimal solution and `x̄ᵏₛ` is the weighted
average (3.1.9), then
`f(x̄ᵏₛ) - f(x*) ≤ (Σ_{t=s}^{k} γt)⁻¹ (V(x s, x*) + (1/2) M² Σ_{t=s}^{k} γt²)`.

Corrected version: the chapter's standing assumptions — `f` convex on `X` (needed for Jensen at
the averaged point `x̄`, which is not an iterate), `X` closed convex, and `V` the Bregman distance
of a distance generating function — are stated; the retired version only assumed the subgradient
inequality at the iterates and took `V` as a free function. -/
theorem mirror_descent_bound_v2 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (X : Set E) (hXconv : Convex ℝ X) (hXclosed : IsClosed X)
    (f : E → ℝ) (hfconv : ConvexOn ℝ X f)
    (ν : DistanceGeneratingFunction X) (M : ℝ) (hM : 0 < M)
    (x : ℕ → E) (g : ℕ → E →L[ℝ] ℝ) (γ : ℕ → ℝ)
    (hx : ∀ t, x t ∈ X) (hγ : ∀ t, 0 < γ t) (hgnorm : ∀ t, ‖g t‖ ≤ M)
    (hsub : ∀ t, ∀ y ∈ X, f (x t) + (g t) (y - x t) ≤ f y)
    (hmin : ∀ t, ∀ y ∈ X, γ t * (g t) (x (t + 1)) + ν.V (x t) (x (t + 1)) ≤
      γ t * (g t) y + ν.V (x t) y)
    (s k : ℕ) (hsk : s ≤ k)
    (xstar : E) (hxstar : xstar ∈ X) (hxstar_opt : ∀ y ∈ X, f xstar ≤ f y)
    (xbar : E)
    (hxbar : xbar = (∑ t ∈ Finset.Icc s k, γ t)⁻¹ • ∑ t ∈ Finset.Icc s k, γ t • x t) :
    f xbar - f xstar ≤ (∑ t ∈ Finset.Icc s k, γ t)⁻¹ *
      (ν.V (x s) xstar + (1 / 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. 61, Theorem 3.5

View graph

Theorem 3.5 — mirror descent function-value bound (corrected: convex fff, Bregman VVV)

Theorem 3.5 — mirror descent function-value bound (corrected: convex $f$ , Bregman $V$ )