Theorem 4.2 (35) — second moments of $g_\mu$ and $\hat g_\mu$ for $f\in C^{1,1}$

Proved

RandomGradFree.Smooth.oracle_second_moment

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

lipschitz-gradientp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1random-oraclevariance-boundzeroth-order

Let $E$ be a real inner product space of finite dimension $n$ , $u$ a standard Gaussian vector in $E$ , and $f : E \to \mathbb R$ convex, differentiable, with $L_1$ -Lipschitz gradient. Let $\mu > 0$ and $x \in E$ , and let $g_\mu(x)$ , $\hat g_\mu(x)$ be the oracles of (30). Then

\begin{aligned} \mathbb E_u\big(\|g_\mu(x)\|_*^2\big) &\le \frac{\mu^2}{2}L_1^2(n+6)^3 + 2(n+4)\|\nabla f(x)\|_*^2,\\ \mathbb E_u\big(\|\hat g_\mu(x)\|_*^2\big) &\le \frac{\mu^2}{8}L_1^2(n+6)^3 + 2(n+4)\|\nabla f(x)\|_*^2. \end{aligned}

The first inequality is the variance bound used in the complexity analysis of the random gradient method $\mathcal{RG}_\mu$ (Theorem 8).

Formalization Note The convexity hypothesis of Theorem 4's preamble is kept, as in the paper's statement. $\|g_\mu(x)\|_* = \|B^{-1}g_\mu(x)\|$ . Both second moments are genuine integrals: for $f \in C^{1,1}$ the finite differences are bounded by $\|\nabla f(x)\|\|u\| + \frac{\mu}{2}L_1\|u\|^2$ .

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_oracle
import Definitions.Def_RandomGradFree_Smooth_symOracle

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Smooth

theorem oracle_second_moment {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (hf : ConvexOn ℝ Set.univ f)
    (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)
        ≤ μ ^ 2 / 2 * L₁ ^ 2 * ((Module.finrank ℝ E : ℝ) + 6) ^ 3
          + 2 * ((Module.finrank ℝ E : ℝ) + 4) * ‖gradient f x‖ ^ 2 ∧
      ∫ u, ‖symOracle f μ x u‖ ^ 2 ∂(stdGaussian E)
        ≤ μ ^ 2 / 8 * L₁ ^ 2 * ((Module.finrank ℝ E : ℝ) + 6) ^ 3
          + 2 * ((Module.finrank ℝ E : ℝ) + 4) * ‖gradient f x‖ ^ 2 := by sorry

end RandomGradFree.Smooth

Source

Nesterov, Spokoiny, Random Gradient-Free Minimization of Convex Functions, Found. Comput. Math. 17 (2017), p. 538, Theorem 4, part 2, Eq. (35)

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, $n = \dim_{\mathbb{R}} E$ , and $\gamma_E$ is the standard Gaussian measure on $E$ .
$f : E \to \mathbb{R}$ , and $L_1$ , $\mu$ are real numbers.

Hypotheses.

$f$ is convex on all of $E$ .
$L_1 \ge 0$ .
$f$ is differentiable everywhere, with gradient $\nabla f$ .
The gradient is $L_1$ -Lipschitz: $\|\nabla f(x) - \nabla f(y)\| \le L_1 \|x - y\|$ for all $x, y$ .
$\mu > 0$ .
$x \in E$ is arbitrary.

Claim. Both of the following hold:

\int_E \big\|\mathrm{oracle}_{f,\mu}(x,u)\big\|^2\, d\gamma_E(u) \;\le\; \frac{\mu^2}{2}\,L_1^2\,(n+6)^3 \;+\; 2(n+4)\,\|\nabla f(x)\|^2,

\int_E \Big\|\frac{f(x+\mu u)-f(x-\mu u)}{2\mu}\,u\Big\|^2\, d\gamma_E(u) \;\le\; \frac{\mu^2}{8}\,L_1^2\,(n+6)^3 \;+\; 2(n+4)\,\|\nabla f(x)\|^2 .

In the first inequality, $\mathrm{oracle}$ is the imported definition RandomGradFree.Shared.oracle. Its body is not included in the code provided, so this read-back cannot unfold it. In the second inequality, the integrand is the symmetric oracle written out explicitly.

Degenerate cases.

Integral convention. If either integrand were not integrable, its integral would be defined as $0$ . That inequality would then hold trivially, since both right-hand sides are $\ge 0$ .
$L_1 = 0$ . This is allowed. It forces $\nabla f$ to be constant, so $f$ is affine, and the $\mu$ -terms vanish.
$n = 0$ . The right-hand sides become $\frac{\mu^2}{2}\cdot 216\,L_1^2$ and $\frac{\mu^2}{8}\cdot 216\,L_1^2$ , because $\nabla f(x) = 0$ . The left side of the symmetric bound is $0$ .
$\mu = 0$ . This is excluded by the hypothesis $\mu > 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 4.2 (35) — second moments of gμg_\mugμ​ and g^μ\hat g_\mug^​μ​ for f∈C1,1f\in C^{1,1}f∈C1,1

Theorem 4.2 (35) — second moments of $g_\mu$ and $\hat g_\mu$ for $f\in C^{1,1}$