Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 4.4, p. 305 — mirror prox with η = ρ/β on a convex β-smooth f satisfies f((1/t)Σ_{s=1}^t y_{s+1}) − f(x*) ≤ βR²/(ρt)

Open
ConvexOptAlg.MirrorProx.theorem_4_4

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

convergence-rateconvex-optimizationmirror-proxp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1smoothness

Fix an arbitrary norm ∥⋅∥\|\cdot\|∥⋅∥ on a finite-dimensional real space, a compact convex set X\mathcal XX, and a convex open set D\mathcal DD with X⊆D‾\mathcal X\subseteq\overline{\mathcal D}X⊆D and X∩D≠∅\mathcal X\cap\mathcal D\ne\emptysetX∩D=∅. Let Φ\PhiΦ be a mirror map on D\mathcal DD that is ρ\rhoρ-strongly convex on X∩D\mathcal X\cap\mathcal DX∩D with respect to ∥⋅∥\|\cdot\|∥⋅∥, with ρ>0\rho>0ρ>0. Let fff be convex and β\betaβ-smooth on X\mathcal XX with respect to ∥⋅∥\|\cdot\|∥⋅∥, with β>0\beta>0β>0, and let x∗∈Xx^*\in\mathcal Xx∗∈X minimize fff over X\mathcal XX. Run mirror prox with η=ρ/β\eta=\rho/\betaη=ρ/β from x1∈argmin⁡x∈X∩DΦ(x)x_1\in\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}\Phi(x)x1​∈argminx∈X∩D​Φ(x), and let RRR satisfy

Φ(x)−Φ(x1)≤R2for all x∈X∩D,\Phi(x)-\Phi(x_1)\le R^2\qquad\text{for all }x\in\mathcal X\cap\mathcal D,Φ(x)−Φ(x1​)≤R2for all x∈X∩D,

for instance R2=sup⁡x∈X∩DΦ(x)−Φ(x1)R^2=\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)R2=supx∈X∩D​Φ(x)−Φ(x1​). Then for every t≥1t\ge1t≥1,

f(1t∑s=1tys+1)−f(x∗)≤βR2ρt.f\Bigl(\frac1t\sum_{s=1}^t y_{s+1}\Bigr)-f(x^*)\le\frac{\beta R^2}{\rho t}.f(t1​s=1∑t​ys+1​)−f(x∗)≤ρtβR2​.

Mirror prox, introduced by Nemirovski, attains the rate 1/t1/t1/t on smooth functions in non-Euclidean geometries, while mirror descent attains 1/t1/\sqrt t1/t​ on Lipschitz functions (Theorem 4.2). The average is over the intermediate points ys+1y_{s+1}ys+1​, not over the xsx_sxs​.

Formalization Note The existence of the minimizer x∗x^*x∗ is the book's standing assumption (p. 242). The book does not specify x1x_1x1​ in §4.5; it is taken in argmin⁡X∩DΦ\operatorname{argmin}_{\mathcal X\cap\mathcal D}\PhiargminX∩D​Φ as in mirror descent (§4.2, p. 299), which is what makes R2R^2R2 bound DΦ(x,x1)D_\Phi(x,x_1)DΦ​(x,x1​). RRR is any real with Φ−Φ(x1)≤R2\Phi-\Phi(x_1)\le R^2Φ−Φ(x1​)≤R2 on X∩D\mathcal X\cap\mathcal DX∩D; the book's R2=sup⁡R^2=\supR2=sup is the special case where the supremum is finite (when it is +∞+\infty+∞ the book's bound is void). ρ>0\rho>0ρ>0 and β>0\beta>0β>0 are the implicit conditions for η=ρ/β\eta=\rho/\betaη=ρ/β and the division by ρt\rho tρt. The gradient of fff is required relative to X\mathcal XX (HasFDerivWithinAt), matching f:X→Rf:\mathcal X\to\mathbb Rf:X→R; x∗x^*x∗ may lie on the boundary of D\mathcal DD.

Preamble
import Mathlib
import Definitions.Def_ConvexOptAlg_MirrorProx_Defs
Formal statement
namespace ConvexOptAlg.MirrorProx

/-- Theorem 4.4 (Bubeck, arXiv:1405.4980v2, §4.5, p. 305). Fix a norm on a finite-dimensional real
space `E`, a compact convex set `X`, and a convex open set `D` with `X ⊆ closure D` and
`X ∩ D ≠ ∅`. Let `Φ` be a mirror map on `D`, `ρ`-strongly convex on `X ∩ D` w.r.t. `‖·‖`
(`ρ > 0`), and let `f` be convex and `β`-smooth on `X` w.r.t. `‖·‖` (`β > 0`), with a minimizer
`x∗ ∈ X`. Let `(x_t, y_t, y'_t, x'_t)` be a run of mirror prox with `η = ρ/β` started at
`x₁ ∈ argmin_{X ∩ D} Φ`, and let `R` satisfy `Φ(w) − Φ(x₁) ≤ R²` for all `w ∈ X ∩ D` (the
book's `R² = sup_{X ∩ D} Φ − Φ(x₁)` is one such value). Then for every `t ≥ 1`,
`f((1/t) Σ_{s=1}^t y_{s+1}) − f(x∗) ≤ βR²/(ρt)`. -/
theorem theorem_4_4 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (X D : Set E) (hXc : IsCompact X) (hXconv : Convex ℝ X) (hXD : X ⊆ closure D)
    (hXDne : (X ∩ D).Nonempty)
    (Φ : E → ℝ) (Φ' : E → E →L[ℝ] ℝ) (hΦ : IsMirrorMap D Φ Φ')
    (ρ : ℝ) (hρ : 0 < ρ) (hsc : IsStronglyConvexWRT (X ∩ D) Φ Φ' ρ)
    (f : E → ℝ) (f' : E → E →L[ℝ] ℝ) (hf : ConvexOn ℝ X f)
    (β : ℝ) (hβ : 0 < β) (hsm : IsSmoothWRT X f f' β)
    (xstar : E) (hxstar : xstar ∈ X ∧ ∀ w ∈ X, f xstar ≤ f w)
    (x y y' x' : ℕ → E) (hrun : IsMirrorProxRun X D Φ Φ' f' (ρ / β) x y y' x')
    (hx1 : ∀ w ∈ X ∩ D, Φ (x 1) ≤ Φ w)
    (R : ℝ) (hR : ∀ w ∈ X ∩ D, Φ w - Φ (x 1) ≤ R ^ 2)
    (t : ℕ) (ht : 1 ≤ t) :
    f ((1 / (t : ℝ)) • ∑ s ∈ Finset.Icc 1 t, y (s + 1)) - f xstar
      ≤ β * R ^ 2 / (ρ * t) := by sorry

end ConvexOptAlg.MirrorProx
Source
Bubeck, arXiv:1405.4980v2, Theorem 4.4, p. 305 (mirror prox equations, p. 305; proof, pp. 306–307)

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me