Section 2, Eq. (21) — $\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)$ for $\mu > 0$

Proved

RandomGradFree.Accelerated.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, let $f : E \to \mathbb R$ be differentiable with $L_1$ -Lipschitz gradient, and let $\mu > 0$ . Then the Gaussian approximation $f_\mu$ is differentiable at every $x \in E$ , and its gradient is the expectation of the random gradient-free oracle:

\nabla f_\mu(x) = \frac{1}{\kappa}\int_E \frac{f(x+\mu u) - f(x)}{\mu}\, e^{-\frac12\|u\|^2}\, Bu\,du = \mathbb E_u\big(g_\mu(x)\big).

Thus $g_\mu(x)$ is an unbiased estimate of $\nabla f_\mu(x)$ ; this is the identity used when the expectation over $u_k$ is taken in the proof of Theorem 9.

Formalization Note The statement is HasGradientAt of $f_\mu$ at $x$ with gradient the Bochner integral of the ( $B^{-1}$ -applied) oracle against stdGaussian E. The paper states differentiability for any positive $\mu$ ; the $C^{1,1}$ hypothesis of this mission guarantees the integrals exist.

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_smoothing
import Definitions.Def_RandomGradFree_Shared_oracle

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Accelerated

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

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$ : a finite-dimensional real inner product space with its Borel σ-algebra, carrying the standard Gaussian probability measure $\mathcal N_E$ .
$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 μ.

Neither definition is in the code provided, and this read-back does not describe them.

The theorem asserts that $f_\mu$ is differentiable at $x$ and its gradient there is the $E$ -valued Gaussian average of the oracle:

\nabla f_\mu(x) \;=\; \int_E g_\mu(x,u)\, d\mathcal N_E(u).

Degenerate cases:

The integral is a Bochner integral. If $u \mapsto g_\mu(x,u)$ were not integrable, it would be assigned the value $0$ , and the claim would then read " $f_\mu$ has gradient $0$ at $x$ ".
$n = 0$ makes the claim trivial.
$\mu = 0$ is excluded.

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)=Eu gμ(x)\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)∇fμ​(x)=Eu​gμ​(x) for μ>0\mu > 0μ>0

Section 2, Eq. (21) — $\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)$ for $\mu > 0$