Lemma 3 — exp-concave functions lie above a gradient paraboloid

Proved

LogRegretOCO.FTAL.exp_concave_approx_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 $P \subseteq \mathbb{R}^n$ be convex with $\|x - y\| \le D$ for all $x, y \in P$ , where $D > 0$ . Let $f$ be a real function, differentiable at every point of $P$ , with $\|\nabla f(x)\| \le G$ for $x \in P$ ( $G > 0$ ), and such that $x \mapsto \exp(-\alpha f(x))$ is concave on $P$ for some $\alpha > 0$ . Then for every $\beta$ with $0 < \beta \le \tfrac12 \min\{\tfrac{1}{4GD}, \alpha\}$ ,

f(x) \ge f(y) + \nabla f(y)^\top (x - y) + \frac{\beta}{2} (x - y)^\top \nabla f(y) \nabla f(y)^\top (x - y) \qquad \text{for all } x, y \in P.

The lemma says that an exp-concave function with bounded gradients is bounded below, on the whole decision set, by a rank-one quadratic that touches it at $y$ . This is what lets Follow the Approximate Leader replace each cost by its quadratic model without increasing the regret.

Formalization Note The quadratic term is written as $\frac{\beta}{2}\langle \nabla f(y), x - y\rangle^2$ , which equals $\frac{\beta}{2}(x-y)^\top \nabla f(y)\nabla f(y)^\top(x-y)$ . The paper states $\beta \le \frac12\min\{\cdot\}$ ; the hypothesis $\beta > 0$ is added because the proof divides by $\beta$ (at $\beta = 0$ the claim would be the tangent inequality for a convex function). $G > 0$ and $D > 0$ make $1/(4GD)$ meaningful (in Lean $1/0 = 0$ ). $f$ is a function on all of $\mathbb{R}^n$ , differentiable at the points of $P$ ; the diameter is used only as an upper bound.

Preamble

import Mathlib

Formal statement

namespace LogRegretOCO.FTAL
theorem exp_concave_approx_lower_bound {n : ℕ} (P : Set (EuclideanSpace ℝ (Fin n)))
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (D G α β : ℝ)
    (hPconv : Convex ℝ P) (hD : 0 < D) (hG : 0 < G) (hα : 0 < α)
    (hdiam : ∀ x ∈ P, ∀ y ∈ P, ‖x - y‖ ≤ D)
    (hdiff : ∀ x ∈ P, DifferentiableAt ℝ f x)
    (hgrad : ∀ x ∈ P, ‖gradient f x‖ ≤ G)
    (hexp : ConcaveOn ℝ P (fun x => Real.exp (-α * f x)))
    (hβ0 : 0 < β) (hβ : β ≤ 1 / 2 * min (1 / (4 * G * D)) α) :
    ∀ x ∈ P, ∀ y ∈ P,
      f y + inner ℝ (gradient f y) (x - y) + β / 2 * (inner ℝ (gradient f y) (x - y)) ^ 2
        ≤ f x := by sorry
end LogRegretOCO.FTAL

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 $\mathbb{R}^n$ carry its Euclidean norm and inner product. The theorem concerns a set $P \subseteq \mathbb{R}^n$ , a function $f : \mathbb{R}^n \to \mathbb{R}$ , and real numbers $D, G, \alpha, \beta$ .

Hypotheses.

$P$ is convex.
$D > 0$ , $G > 0$ and $\alpha > 0$ .
$\|x - y\| \le D$ for all $x, y \in P$ .
$f$ is differentiable at every point of $P$ . This is differentiability as a function on all of $\mathbb{R}^n$ , at those points.
$\|\nabla f(x)\| \le G$ for every $x \in P$ .
The function $x \mapsto e^{-\alpha f(x)}$ is concave on $P$ .
The parameter $\beta$ satisfies

0 < \beta \le \tfrac12 \min\!\Big(\frac{1}{4GD},\, \alpha\Big).

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).

Nothing requires $P$ to be closed, bounded beyond the diameter condition, or nonempty.

Degenerate cases.

$P = \emptyset$ . The conclusion holds vacuously.
$P$ is a single point. Then $x = y$ , and the conclusion reads $f(x) \le f(x)$ .
$n = 0$ . $P$ is empty or a single point, and the gradient is $0$ . The conclusion is again trivial.
Division by zero. It cannot occur, because $G > 0$ and $D > 0$ .
Gradient convention. Differentiability is assumed on $P$ , so the gradient values in the conclusion are never the default zero value used at non-differentiable points.

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