Lemma 5 — $\mathbb E_u\|g_\mu(x)\|_^2 \le 4(n+4)\|\nabla f_\mu(x)\|_^2 + 3\mu^2L_1^2(f)(n+4)^3$ (Eq. (37))

Proved

RandomGradFree.Accelerated.oracle_second_moment_smoothing

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

gaussian-smoothingp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1random-oraclezeroth-order

Let $E$ be a real inner product space of dimension $n$ , and let $f : E \to \mathbb R$ be differentiable with $L_1$ -Lipschitz gradient (no convexity is assumed). Let $\mu > 0$ and let $u$ be a standard Gaussian vector in $E$ . Then for every $x \in E$ the random gradient-free oracle $B^{-1}g_\mu(x) = \frac{f(x+\mu u)-f(x)}{\mu}u$ satisfies

\mathbb E_u\big(\|g_\mu(x)\|_*^2\big) \le 4(n+4)\,\|\nabla f_\mu(x)\|_*^2 + 3\mu^2 L_1^2 (n+4)^3 .

Unlike the bound in terms of $\nabla f(x)$ , this form has the gradient of the smoothed function on the right, which is what the analysis of the accelerated method needs.

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_smoothing
import Definitions.Def_RandomGradFree_Shared_oracle

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Accelerated

theorem oracle_second_moment_smoothing {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (L₁ : ℝ) (hL₁ : 0 ≤ L₁) (hdiff : Differentiable ℝ f)
    (hgrad : ∀ x y, ‖gradient f x - gradient f y‖ ≤ L₁ * ‖x - y‖)
    (μ : ℝ) (hμ : 0 < μ) (x : E) :
    ∫ u, ‖RandomGradFree.Shared.oracle f μ x u‖ ^ 2 ∂(stdGaussian E)
      ≤ 4 * ((Module.finrank ℝ E : ℝ) + 4) * ‖gradient (RandomGradFree.Shared.smoothing f μ) x‖ ^ 2
        + 3 * μ ^ 2 * L₁ ^ 2 * ((Module.finrank ℝ E : ℝ) + 4) ^ 3 := by sorry

end RandomGradFree.Accelerated

Source

Nesterov, Spokoiny, Random Gradient-Free Minimization of Convex Functions, Found. Comput. Math. 17 (2017), p. 539, Lemma 5, Eq. (37)

Read-back

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

Setting:

$E$ : a finite-dimensional real inner product space with its Borel σ-algebra, of dimension $n$ , carrying the standard Gaussian probability measure $\mathcal N_E$ (Mathlib's stdGaussian).
$f : E \to \mathbb R$ : differentiable everywhere, with $L_1$ -Lipschitz gradient for some real $L_1 \ge 0$ .
$\mu > 0$ : a real number, strictly positive.
$x \in E$ : any point.
$g_\mu(x, u) \in E$ : RandomGradFree.Shared.oracle f μ x u.
$f_\mu$ : RandomGradFree.Shared.smoothing f μ.

The definitions of $g_\mu$ and $f_\mu$ are not in the code provided, and this read-back does not describe them.

The theorem asserts

\int_E \|g_\mu(x,u)\|^2 \, d\mathcal N_E(u) \;\le\; 4\,(n+4)\,\|\nabla f_\mu(x)\|^2 \;+\; 3\,\mu^2 L_1^2\,(n+4)^3 .

Here $\nabla f_\mu(x)$ is the gradient of $f_\mu$ at $x$ . By the gradient convention, it would be $0$ if $f_\mu$ were not differentiable at $x$ ; this statement does not itself assert that differentiability. The integral is a Bochner integral of a nonnegative function, assigned the value $0$ if the function is not integrable.

Degenerate cases:

$n = 0$ : the right-hand side is $4\cdot 4\cdot\|\nabla f_\mu(x)\|^2 + 3\cdot 64\,\mu^2 L_1^2$ , while the left-hand side is $0$ because $E = \{0\}$ .
$L_1 = 0$ : only the first term remains.
$\mu = 0$ is excluded by hypothesis.

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

Lemma 5 — Eu∥gμ(x)∥∗2≤4(n+4)∥∇fμ(x)∥∗2+3μ2L12(f)(n+4)3\mathbb E_u\|g_\mu(x)\|_*^2 \le 4(n+4)\|\nabla f_\mu(x)\|_*^2 + 3\mu^2L_1^2(f)(n+4)^3Eu​∥gμ​(x)∥∗2​≤4(n+4)∥∇fμ​(x)∥∗2​+3μ2L12​(f)(n+4)3 (Eq. (37))

Lemma 5 — $\mathbb E_u\|g_\mu(x)\|_^2 \le 4(n+4)\|\nabla f_\mu(x)\|_^2 + 3\mu^2L_1^2(f)(n+4)^3$ (Eq. (37))