Theorem 2 — $\nabla f_\mu(x) \in \partial_\epsilon f(x)$ with $\epsilon = \mu L_0(f) n^{1/2}$ , $\mu \ge 0$

Proved

RandomGradFree.Nonsmooth.gradient_smoothing_mem_epsSubdiff

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

convexitygaussian-smoothingp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1subdifferential

Let $E$ be a real inner product space of dimension $n$ , let $f : E \to \mathbb R$ be convex and Lipschitz continuous with constant $L_0 \ge 0$ , and let $\mu \ge 0$ . Put $\epsilon = \mu L_0 n^{1/2}$ . For $\mu > 0$ let $\nabla f_\mu(x)$ be the gradient of the Gaussian smoothing $f_\mu$ ; for $\mu = 0$ let $\nabla f_0(x) = \mathbb E_u[f'(x,u)\,u]$ be the limiting vector of Eq. (24), where $f'(x,u) = \lim_{\alpha \downarrow 0} (f(x+\alpha u) - f(x))/\alpha$ is the directional derivative. Then for every $x \in E$ the vector $\nabla f_\mu(x)$ is an $\epsilon$ -subgradient of $f$ at $x$ :

f(y) \ge f(x) - \epsilon + \langle \nabla f_\mu(x), y - x\rangle \qquad \text{for all } y \in E .

Thus the expected output of the random oracle is an approximate subgradient of the original nonsmooth function, with an error that vanishes linearly in $\mu$ .

Formalization Note The $\epsilon$ -subdifferential (p. 532) is written out as the inequality above. For $\mu > 0$ the vector is Mathlib's gradient of $f_\mu$ (which is differentiable, Eq. (21)); for $\mu = 0$ it is $\nabla f_0(x)$ of Eq. (24), written as the Gaussian expectation of the shared oracle at $\mu = 0$ , $f'(x,u)\,u$ (Eq. (30), item 3). At $\mu = 0$ the statement is $\nabla f_0(x) \in \partial f(x)$ , Eq. (31).

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_smoothing
import Definitions.Def_RandomGradFree_Shared_oracle

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Nonsmooth

theorem gradient_smoothing_mem_epsSubdiff {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (hf : ConvexOn ℝ Set.univ f)
    (L₀ : ℝ) (hL₀ : 0 ≤ L₀) (hLip : ∀ x y, |f x - f y| ≤ L₀ * ‖x - y‖)
    (μ : ℝ) (hμ : 0 ≤ μ) (x : E) :
    ∀ y : E, f y ≥ f x - μ * L₀ * Real.sqrt (Module.finrank ℝ E)
      + inner ℝ (if μ = 0 then ∫ u, RandomGradFree.Shared.oracle f 0 x u ∂(stdGaussian E)
          else gradient (RandomGradFree.Shared.smoothing f μ) x) (y - x) := by sorry

end RandomGradFree.Nonsmooth

Source

Nesterov, Spokoiny, Random Gradient-Free Minimization of Convex Functions, Found. Comput. Math. 17 (2017), p. 535, Theorem 2

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 $\sigma$ -algebra. Write:

$n = \dim_{\mathbb{R}} E$ ;
$\gamma_E$ for Mathlib's standard Gaussian probability measure on $E$ ;
$\langle\cdot,\cdot\rangle$ for the inner product.

Two functions come from imported files whose code was not supplied, so their meaning cannot be unfolded here:

$f_\mu = \mathrm{smoothing}(f,\mu) : E \to \mathbb{R}$ ;
$\mathrm{oracle}(f, 0, x, u)$ , a value in $E$ that depends on $f$ , the number $0$ , a point $x$ and a variable $u$ . It must lie in $E$ because it is integrated to give a vector that enters the inner product.

Hypotheses.

$f : E \to \mathbb{R}$ is convex on all of $E$ .
$L_0$ is a real number with $L_0 \ge 0$ .
For all $x, y \in E$ : $|f(x) - f(y)| \le L_0 \|x - y\|$ . That is, $f$ is $L_0$ -Lipschitz.
$\mu$ is a real number with $\mu \ge 0$ .
$x$ is a fixed point of $E$ .

No integrability or differentiability hypothesis is made.

The vector $g$ . Define

g = \begin{cases} \displaystyle\int_E \mathrm{oracle}(f,0,x,u)\, d\gamma_E(u) & \text{if } \mu = 0,\\[2mm] \nabla f_\mu(x) & \text{if } \mu > 0. \end{cases}

Two conventions matter here:

The integral is a Bochner integral. If $u \mapsto \mathrm{oracle}(f,0,x,u)$ is not $\gamma_E$ -integrable, the integral is defined to be $0$ .
$\nabla f_\mu(x)$ is Mathlib's gradient. If $f_\mu$ is not differentiable at $x$ , the gradient is defined to be $0$ .

Conclusion. For every $y \in E$ ,

f(y) \ \ge\ f(x) - \mu L_0 \sqrt{n} + \langle g,\ y - x\rangle.

Degenerate cases.

Junk-value zeros. If the relevant integral fails to exist ( $\mu = 0$ ), or $f_\mu$ is not differentiable at $x$ ( $\mu > 0$ ), then $g = 0$ . The statement then asserts $f(y) \ge f(x) - \mu L_0 \sqrt{n}$ for all $y$ .
$\mu = 0$ . The correction term vanishes, and the claim is $f(y) \ge f(x) + \langle g, y - x\rangle$ , with $g$ the oracle integral (or $0$ if it does not exist).
$L_0 = 0$ . The Lipschitz hypothesis forces $f$ to be constant. The claim becomes $0 \ge \langle g, y - x\rangle$ for all $y$ .
$n = 0$ . $E$ has only the point $0$ , so $y = x = 0$ and $\sqrt{0} = 0$ . The claim reduces to $f(0) \ge f(0)$ , which holds trivially.
No vacuous case. The hypotheses can always be satisfied, for example by a constant $f$ with any $L_0 \ge 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 2 — ∇fμ(x)∈∂ϵf(x)\nabla f_\mu(x) \in \partial_\epsilon f(x)∇fμ​(x)∈∂ϵ​f(x) with ϵ=μL0(f)n1/2\epsilon = \mu L_0(f) n^{1/2}ϵ=μL0​(f)n1/2, μ≥0\mu \ge 0μ≥0

Theorem 2 — $\nabla f_\mu(x) \in \partial_\epsilon f(x)$ with $\epsilon = \mu L_0(f) n^{1/2}$ , $\mu \ge 0$