Theorem 3.1 (32) — $\mathbb E_u\|g_0(x)\|_^2 \le (n+4)\|\nabla f(x)\|_^2$

Proved

RandomGradFree.Smooth.directional_oracle_second_moment

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

p2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1random-oraclevariance-boundzeroth-order

Let $E$ be a real inner product space of finite dimension $n$ , $u$ a standard Gaussian vector in $E$ , and $f : E \to \mathbb R$ differentiable at $x$ . Let $g_0(x) = f'(x,u)Bu$ be the limiting random oracle of (30). Then

\mathbb E_u\big(\|g_0(x)\|_*^2\big) \le (n+4)\,\|\nabla f(x)\|_*^2 .

This variance bound, of order $n$ rather than the naive $(n+4)^2$ , is what gives the random gradient method $\mathcal{RG}_0$ its linear dependence on the dimension.

Formalization Note $\|g_0(x)\|_* = \|f'(x,u)\,u\|$ with $f'(x,u)$ written as fderiv ℝ f x u; no convexity is assumed, as in part 1 of the theorem.

Preamble

import Mathlib

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Smooth

theorem directional_oracle_second_moment {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (x : E) (hfx : DifferentiableAt ℝ f x) :
    ∫ u, ‖fderiv ℝ f x u • u‖ ^ 2 ∂(stdGaussian E)
      ≤ ((Module.finrank ℝ E : ℝ) + 4) * ‖gradient f x‖ ^ 2 := by sorry

end RandomGradFree.Smooth

Source

Nesterov, Spokoiny, Random Gradient-Free Minimization of Convex Functions, Found. Comput. Math. 17 (2017), p. 537, Theorem 3, part 1, Eq. (32)

Read-back

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

Setting.

$E$ is a finite-dimensional real inner product space with its Borel σ-algebra, and $n = \dim_{\mathbb{R}} E$ .
$\gamma_E$ is the standard Gaussian measure on $E$ (as defined in Mathlib).
$f : E \to \mathbb{R}$ is any function and $x \in E$ .

Hypothesis. $f$ is (Fréchet) differentiable at $x$ . Write $Df(x)$ for its derivative, a linear map $E \to \mathbb{R}$ , and $\nabla f(x)$ for the gradient, the vector with $Df(x)[v] = \langle \nabla f(x), v\rangle$ .

Claim.

\int_E \big\| Df(x)[u]\; u \big\|^2 \, d\gamma_E(u) \;\le\; (n+4)\,\|\nabla f(x)\|^2 .

No other assumption is made on $f$ , such as convexity, smoothness elsewhere, or growth conditions.

Degenerate cases.

Integral convention. The integral is the Lebesgue/Bochner integral. If the integrand were not integrable, the integral would be defined as $0$ and the inequality would hold trivially.
$n = 0$ . Both sides are $0$ .
$\nabla f(x) = 0$ . The claim says the left side is at most $0$ .

Human review

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

View graph

Theorem 3.1 (32) — Eu∥g0(x)∥∗2≤(n+4)∥∇f(x)∥∗2\mathbb E_u\|g_0(x)\|_*^2 \le (n+4)\|\nabla f(x)\|_*^2Eu​∥g0​(x)∥∗2​≤(n+4)∥∇f(x)∥∗2​

Theorem 3.1 (32) — $\mathbb E_u\|g_0(x)\|_^2 \le (n+4)\|\nabla f(x)\|_^2$