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

Proved

RandomGradFree.Nonsmooth.smoothing_hasGradient

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

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

Let $f : E \to \mathbb R$ be Lipschitz continuous with constant $L_0 \ge 0$ and let $\mu > 0$ . Then the Gaussian smoothing $f_\mu$ is differentiable at every $x \in E$ , and its gradient is the expectation of the finite-difference oracle:

\nabla f_\mu(x) = \mathbb E_u\!\left[\frac{f(x+\mu u) - f(x)}{\mu}\, u\right].

In other words, the random oracle $g_\mu(x)$ is an unbiased estimator of $\nabla f_\mu(x)$ ; this is the identity that turns the random search method into a stochastic gradient method for $f_\mu$ .

Formalization Note "Differentiable with this gradient" is Mathlib's HasGradientAt, with the gradient taken with respect to the inner product of $E$ (the paper's $\langle B\cdot,\cdot\rangle$ , so the paper's $B^{-1}\nabla f_\mu(x)$ ). The paper assumes only that $f$ has directional derivatives and differentiates under the integral sign; Lipschitz continuity is assumed here, which justifies that step and is the setting of Theorem 6.

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_smoothing
import Definitions.Def_RandomGradFree_Nonsmooth_oracle

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Nonsmooth

theorem smoothing_hasGradient {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (L₀ : ℝ) (hL₀ : 0 ≤ L₀) (hLip : ∀ x y, |f x - f y| ≤ L₀ * ‖x - y‖)
    (μ : ℝ) (hμ : 0 < μ) (x : E) :
    HasGradientAt (RandomGradFree.Shared.smoothing f μ) (∫ u, oracle f μ x u ∂(stdGaussian E)) x := by sorry

end RandomGradFree.Nonsmooth

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

The setting is:

$E$ is a finite-dimensional real inner product space with its Borel σ-algebra.
$\gamma_E$ is the standard Gaussian measure on $E$ .
$f : E \to \mathbb{R}$ is any function (convexity is not assumed) satisfying, for a real $L_0 \ge 0$ , $|f(x)-f(y)| \le L_0\|x-y\|$ for all $x, y$ .
$\mu > 0$ (strictly) is a real number and $x \in E$ is a point.

The statement asserts that $f_\mu = \mathrm{smoothing}(f,\mu)$ is (Fréchet) differentiable at $x$ and that its gradient there is

\nabla f_\mu(x) \;=\; \int_E \frac{f(x+\mu u) - f(x)}{\mu}\, u \;\, d\gamma_E(u) ,

with the integral taken as a vector-valued (Bochner) integral in $E$ . The gradient is the vector representing the derivative through the inner product. The function $f_\mu$ is defined in a separate shared definition not included in this declaration's code, so its formula cannot be expanded here.

The statement does not separately assert that the integrand is integrable. By convention, the integral of a non-integrable function is the zero vector. In that case the claim would read $\nabla f_\mu(x) = 0$ .

Degenerate cases:

$E = \{0\}$ : the integrand is $0$ , so the claim is that $f_\mu$ has gradient $0$ at $x$ . On the one-point space this holds for any function.
$L_0 = 0$ : $f$ is constant, the integrand is identically $0$ , and the claim is that $f_\mu$ has gradient $0$ at $x$ .

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$