Lemma 3 — exp-concave functions admit a quadratic lower bound built from the gradient

Proved

LogRegretOCO.ONS.exp_concave_quadratic_lower_bound

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

convex-analysisexp-concavityonline-convex-optimizationp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathcal P\subseteq\mathbb R^n$ have diameter at most $D>0$ , i.e. $\|x-y\|\le D$ for all $x,y\in\mathcal P$ . Let $f:\mathbb R^n\to\mathbb R$ be differentiable at every point of $\mathcal P$ with $\|\nabla f(x)\|\le G$ for all $x\in\mathcal P$ , where $G>0$ , and suppose that $x\mapsto\exp(-\alpha f(x))$ is concave on $\mathcal P$ . Then for every $\beta$ with

0<\beta\le\tfrac12\min\Big\{\frac1{4GD},\,\alpha\Big\}

and all $x,y\in\mathcal P$ ,

f(x)\ \ge\ f(y)+\nabla f(y)^\top(x-y)+\frac\beta2\,(x-y)^\top\nabla f(y)\nabla f(y)^\top(x-y).

The lemma replaces the Hessian in a second-order Taylor bound by the rank-one matrix $\nabla f(y)\nabla f(y)^\top$ ; this is what lets the Online Newton Step work from gradients alone. It gives the per-round inequality (3) of the proof of Theorem 2.

Formalization Note The quadratic term is written as $\beta/2\cdot(\nabla f(y)^\top(x-y))^2$ , which equals $(x-y)^\top\nabla f(y)\nabla f(y)^\top(x-y)$ . The hypotheses $G>0$ , $D>0$ are the non-degeneracy the formula $1/(4GD)$ presupposes (in Lean $1/0=0$ ). The hypothesis $\beta>0$ is added: the paper's proof divides by $\beta$ , and it forces $\alpha>0$ , which is part of the paper's definition of $\alpha$ -exp-concavity. The diameter is used only as the upper bound $\|x-y\|\le D$ , which makes the statement slightly more general. The paper's standing assumptions that $f$ is convex and twice differentiable are not needed (convexity follows from exp-concavity) and are omitted.

Preamble

import Mathlib
open scoped RealInnerProductSpace

Formal statement

namespace LogRegretOCO.ONS

/-- Lemma 3 (Hazan–Agarwal–Kale 2007, p. 177). Let `P` have diameter at most `D`, let `f` be
differentiable at every point of `P` with `‖∇f(x)‖ ≤ G` there, and let `exp(−α f)` be concave on
`P`. Then for every `0 < β ≤ ½ min{1/(4GD), α}` and all `x, y ∈ P`,
`f(x) ≥ f(y) + ∇f(y)ᵀ(x − y) + (β/2) (x − y)ᵀ ∇f(y) ∇f(y)ᵀ (x − y)`.
`0 < G`, `0 < D` are the non-degeneracy the formula `1/(4GD)` presupposes; `0 < β` excludes the
degenerate step size (the proof divides by `β`). -/
theorem exp_concave_quadratic_lower_bound {n : ℕ} (P : Set (EuclideanSpace ℝ (Fin n)))
    (G D α β : ℝ) (hG : 0 < G) (hD : 0 < D)
    (hdiam : ∀ x ∈ P, ∀ y ∈ P, ‖x - y‖ ≤ D)
    (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hdiff : ∀ x ∈ P, DifferentiableAt ℝ f x)
    (hgrad : ∀ x ∈ P, ‖gradient f x‖ ≤ G)
    (hexp : ConcaveOn ℝ P (fun x => Real.exp (-α * f x)))
    (hβ_pos : 0 < β) (hβ : β ≤ (1 / 2) * min (1 / (4 * G * D)) α) :
    ∀ x ∈ P, ∀ y ∈ P,
      f y + ⟪gradient f y, x - y⟫ + (β / 2) * ⟪gradient f y, x - y⟫ ^ 2 ≤ f x := by sorry

end LogRegretOCO.ONS

Source

Hazan, Agarwal, Kale, Logarithmic regret algorithms for online convex optimization, Mach Learn 69 (2007), p. 177, Lemma 3

Read-back

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

Setting. Let $n\in\mathbb{N}$ and let $P\subseteq\mathbb{R}^n$ , where $\mathbb{R}^n$ is Euclidean space. Let $G,D,\alpha,\beta$ be real numbers and let $f:\mathbb{R}^n\to\mathbb{R}$ .

Hypotheses:

$G>0$ and $D>0$ .
For all $x,y\in P$ , $\|x-y\|\le D$ (Euclidean norm).
$f$ is differentiable at every point of $P$ .
For every $x\in P$ , $\|\nabla f(x)\|\le G$ .
The function $x\mapsto e^{-\alpha f(x)}$ is concave on $P$ . As formulated, this concavity hypothesis includes the requirement that $P$ is convex.
$0<\beta\le \tfrac12\min\{\frac{1}{4GD},\alpha\}$ . Since $\min\{\cdot,\alpha\}\le\alpha$ , this forces $\alpha\ge 2\beta>0$ .

Conclusion. For all $x,y\in P$ ,

f(y)+\langle\nabla f(y),\,x-y\rangle+\frac{\beta}{2}\,\langle\nabla f(y),\,x-y\rangle^2\;\le\;f(x).

Here $\langle\cdot,\cdot\rangle$ is the standard inner product and $\nabla f(y)$ is the Euclidean gradient. Because $f$ is differentiable at $y\in P$ , this gradient is the genuine gradient.

Degenerate cases:

$P$ empty: every hypothesis about $P$ holds vacuously and the conclusion is vacuous.
$P$ a single point: only $x=y$ arises, and the inequality reads $f(y)\le f(y)$ .
$n=0$ :
- $P$ is either empty or the single zero point, and the gradient is the zero vector;
- the conclusion reduces to $f(0)\le f(0)$ .
$\alpha$ : it is not assumed positive directly, but the hypotheses on $\beta$ force $\alpha>0$ .
Division: $\frac{1}{4GD}$ is a genuine quotient, since $G,D>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