Eq. (2) — one projected gradient step: 2∇ᵀ(x − u) ≤ (‖x − u‖² − ‖x' − u‖²)/η + ηG²

Proved

LogRegretOCO.OGD.one_step_inequality

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

gradient-descentonline-convex-optimizationp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1projection

Let $\mathcal P\subseteq\mathbb R^n$ be convex, let $x,g\in\mathbb R^n$ , let $\eta>0$ and $G\in\mathbb R$ with $\|g\|_2\le G$ , and let $z=\Pi_{\mathcal P}(x-\eta g)$ be the Euclidean projection of the gradient step $x-\eta g$ onto $\mathcal P$ . Then for every $u\in\mathcal P$ ,

\|z-u\|_2^2\ \le\ \|x-u\|_2^2+\eta^2\|g\|_2^2-2\eta\, g^\top(x-u),

2\,g^\top(x-u)\ \le\ \frac{\|x-u\|_2^2-\|z-u\|_2^2}{\eta}+\eta\,G^2 .

This is display (2) in the proof of Theorem 1, applied there with $x=x_t$ , $g=\nabla f_t(x_t)$ , $\eta=\eta_{t+1}$ , $z=x_{t+1}$ and $u=x^*$ . It bounds the linearised regret of one round by a telescoping difference of squared distances plus a step-size term, which is Zinkevich's analysis of projected gradient descent.

Formalization Note The paper prints the second line as " $5\nabla_t^\top(x_t-x^*)\le\dots$ "; the $5$ is a typo for $2$ : the line follows from the first one by rearranging, and the proof then sums (2) against (1), which needs the factor $2$ . The Lean states $2$ . The point $x$ is not required to lie in $\mathcal P$ (the inequality holds anyway), and the comparator is any $u\in\mathcal P$ rather than the minimiser $x^*$ . Points are EuclideanSpace ℝ (Fin n).

Preamble

import Mathlib
import Definitions.Def_LogRegretOCO_OGD_Model

Formal statement

namespace LogRegretOCO.OGD

/-- **Eq. (2)** (p. 175): one projected gradient step `z = Π_P(x − η g)` with `η > 0`,
`‖g‖ ≤ G`, measured against any `u ∈ P`:
`‖z − u‖² ≤ ‖x − u‖² + η² ‖g‖² − 2η gᵀ(x − u)` and
`2 gᵀ(x − u) ≤ (‖x − u‖² − ‖z − u‖²)/η + η G²`.
(The paper prints `5∇_t^⊤` in the second line; it is `2∇_t^⊤`.) -/
theorem one_step_inequality {n : ℕ} (P : Set (E n)) (hPc : Convex ℝ P) (x g z u : E n)
    (η G : ℝ) (hη : 0 < η) (hg : ‖g‖ ≤ G) (hz : IsProj P (x - η • g) z) (hu : u ∈ P) :
    ‖z - u‖ ^ 2 ≤ ‖x - u‖ ^ 2 + η ^ 2 * ‖g‖ ^ 2 - 2 * η * inner ℝ g (x - u) ∧
      2 * inner ℝ g (x - u) ≤ (‖x - u‖ ^ 2 - ‖z - u‖ ^ 2) / η + η * G ^ 2 := by sorry

end LogRegretOCO.OGD

Source

Hazan, Agarwal, Kale, Logarithmic regret algorithms for online convex optimization, Mach Learn 69 (2007), p. 175, proof of Theorem 1, Eq. (2)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The inputs are:

a natural number $n$ , with $\mathbb{R}^n$ carrying the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$ ;
a set $P \subseteq \mathbb{R}^n$ , assumed convex;
points $x, g, z, u \in \mathbb{R}^n$ ;
real numbers $\eta$ and $G$ .

The hypotheses are:

$\eta > 0$ .
$\|g\| \le G$ .
$z$ is a projection of $x - \eta g$ onto $P$ . That is, $z \in P$ and $\|z - (x - \eta g)\| \le \|w - (x - \eta g)\|$ for every $w \in P$ . So $z$ is some nearest point of $P$ to $x - \eta g$ , and uniqueness is not assumed.
$u \in P$ .

Nothing requires $x \in P$ , and nothing requires $P$ to be closed.

The theorem asserts that both of the following hold:

\|z - u\|^2 \;\le\; \|x - u\|^2 + \eta^2\|g\|^2 - 2\eta\,\langle g,\, x - u\rangle,

2\,\langle g,\, x - u\rangle \;\le\; \frac{\|x - u\|^2 - \|z - u\|^2}{\eta} + \eta\, G^2 .

The division by $\eta$ is a genuine division, because $\eta > 0$ .

Degenerate cases.

Hypothesis 2 forces $G \ge 0$ .
If $P$ is empty, or $P$ has no nearest point to $x - \eta g$ , hypothesis 3 cannot hold and the statement is vacuous for those data.
If $n = 0$ , all vectors are $0$ . The inequalities become $0 \le 0$ and $0 \le \eta G^2$ , and the second holds because $G \ge 0$ .
If $g = 0$ , the first inequality says $\|z - u\|^2 \le \|x - u\|^2$ , where $z$ is a nearest point of $P$ to $x$ .
If $P = \{u\}$ is a single point, then $z = u$ and the left side of the first inequality is $0$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph