Section 2, Eq. (21) — $\nabla f_\mu(x) = \mathbb E_u \frac{f(x+\mu u)-f(x)}{\mu}Bu$

Proved

RandomGradFree.Smooth.smoothing_hasGradient

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

gaussian-smoothingp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1zeroth-order

Let $E$ be a finite-dimensional real inner product space, $f : E \to \mathbb R$ differentiable with $L_1$ -Lipschitz gradient, and $\mu > 0$ . Then the Gaussian approximation $f_\mu$ is differentiable at every $x \in E$ , and its gradient is the expected finite-difference oracle:

\nabla f_\mu(x) = \mathbb E_u\!\left[\frac{f(x+\mu u) - f(x)}{\mu}\, u\right] = \frac1\kappa\int_E \frac{f(x+\mu u)-f(x)}{\mu}\, e^{-\frac12\|u\|^2}\, u\, du .

This identity says that the random oracle $g_\mu$ is an unbiased estimator of $\nabla f_\mu$ , so the random gradient method is a stochastic gradient method for $f_\mu$ .

Formalization Note The paper's formula has $Bu$ (a dual vector); after identifying $E^*$ with $E$ via the inner product this is the vector $u$ . The paper asks only that $f$ be continuous enough to differentiate under the integral and leaves integrability implicit; here $f \in C^{1,1}$ (the setting of Theorem 8) guarantees it.

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_smoothing
import Definitions.Def_RandomGradFree_Shared_oracle

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Smooth

theorem smoothing_hasGradient {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) :
    HasGradientAt (RandomGradFree.Shared.smoothing f μ) (∫ u, RandomGradFree.Shared.oracle f μ x u ∂(stdGaussian E)) x := by sorry

end RandomGradFree.Smooth

Source

Nesterov, Spokoiny, Random Gradient-Free Minimization of Convex Functions, Found. Comput. Math. 17 (2017), pp. 534-535, Section 2, Eq. (21)

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 $\gamma_E$ is the standard Gaussian measure on $E$ .

Hypotheses.

$f : E \to \mathbb{R}$ is differentiable everywhere.
Its gradient is $L_1$ -Lipschitz, with $L_1 \ge 0$ : $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x-y\|$ for all $x, y$ .
$\mu > 0$ .
$x \in E$ is arbitrary.

Convexity of $f$ is not assumed.

Claim. Let $f_\mu = \mathrm{smoothing}(f,\mu) : E \to \mathbb{R}$ and $\mathrm{oracle}_{f,\mu}$ be the imported definitions RandomGradFree.Shared.smoothing and RandomGradFree.Shared.oracle. Their bodies are not included in the code provided, so this read-back cannot unfold them. The theorem asserts that $f_\mu$ is Fréchet differentiable at $x$ with gradient equal to the $E$ -valued Bochner integral

\nabla f_\mu(x) \;=\; \int_E \mathrm{oracle}_{f,\mu}(x,u)\, d\gamma_E(u).

Degenerate cases.

Integral convention. If $u \mapsto \mathrm{oracle}_{f,\mu}(x,u)$ were not Bochner-integrable, the integral would be defined as $0$ . The claim would then say that $f_\mu$ has gradient $0$ at $x$ .
$L_1 = 0$ . This is allowed and forces $f$ to be affine.
$\mu = 0$ . This is excluded.
$E = \{0\}$ . The claim reduces to the right-hand side being the zero vector, which holds automatically.

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

Section 2, Eq. (21) — ∇fμ(x)=Euf(x+μu)−f(x)μBu\nabla f_\mu(x) = \mathbb E_u \frac{f(x+\mu u)-f(x)}{\mu}Bu∇fμ​(x)=Eu​μf(x+μu)−f(x)​Bu

Section 2, Eq. (21) — $\nabla f_\mu(x) = \mathbb E_u \frac{f(x+\mu u)-f(x)}{\mu}Bu$