Lemma 1 — Gaussian moment bounds $M_p \le n^{p/2}$ ( $p\in[0,2]$ ), $n^{p/2}\le M_p\le (p+n)^{p/2}$ ( $p\ge2$ )

Proved

RandomGradFree.Nonsmooth.gaussian_moment_bound

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

gaussian-momentsgaussian-smoothingp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $E$ be a real inner product space of dimension $n$ , $u$ a standard Gaussian vector in $E$ , and $M_p = \mathbb E_u\|u\|^p$ . Then:

for $p \in [0,2]$ ,

M_p \le n^{p/2};

for $p \ge 2$ ,

n^{p/2} \le M_p \le (p+n)^{p/2}.

These bounds turn every moment of the Gaussian direction that appears in the variance of the gradient-free oracles into an explicit function of the dimension; $p = 1$ gives the approximation error of Gaussian smoothing and $p = 4$ the second moment of the oracle.

Formalization Note Powers are real powers (Real.rpow) and $n$ is Module.finrank ℝ E; no lower bound on $n$ is assumed (at $n = 0$ all bounds hold).

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_moment

Formal statement

namespace RandomGradFree.Nonsmooth

theorem gaussian_moment_bound (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (p : ℝ) :
    (0 ≤ p → p ≤ 2 → RandomGradFree.Shared.moment E p ≤ (Module.finrank ℝ E : ℝ) ^ (p / 2)) ∧
    (2 ≤ p → (Module.finrank ℝ E : ℝ) ^ (p / 2) ≤ RandomGradFree.Shared.moment E p ∧
      RandomGradFree.Shared.moment E p ≤ (p + Module.finrank ℝ E) ^ (p / 2)) := by sorry

end RandomGradFree.Nonsmooth

Source

Nesterov, Spokoiny, Random Gradient-Free Minimization of Convex Functions, Found. Comput. Math. 17 (2017), p. 534, Lemma 1, Eqs. (16)-(17)

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.
$n = \dim_{\mathbb{R}} E$ , viewed as a real number.
$p$ is any real number.

The statement concerns a quantity $M_p = \mathrm{moment}(E, p)$ , a real number. It is defined in a separate shared definition that is not included in this declaration's code, so its meaning cannot be expanded here. The statement asserts both of the following:

If $0 \le p \le 2$ , then

M_p \le n^{p/2}.

If $p \ge 2$ , then

n^{p/2} \le M_p \le (p+n)^{p/2}.

Powers are real powers of nonnegative reals.

Degenerate cases:

$p < 0$ : both implications are vacuous, so nothing is asserted.
$p = 2$ : both parts apply, giving $M_2 \le n$ and $n \le M_2 \le n+2$ . Hence $M_2 = n$ exactly.
$p = 0$ : $n^0 = 1$ (including $0^0 = 1$ ), so the claim is $M_0 \le 1$ .
$n = 0$ ( $E = \{0\}$ ), $0 < p \le 2$ : $0^{p/2} = 0$ , so the claim is $M_p \le 0$ .
$n = 0$ , $p \ge 2$ : the claim is $0 \le M_p \le p^{p/2}$ .

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

Lemma 1 — Gaussian moment bounds Mp≤np/2M_p \le n^{p/2}Mp​≤np/2 (p∈[0,2]p\in[0,2]p∈[0,2]), np/2≤Mp≤(p+n)p/2n^{p/2}\le M_p\le (p+n)^{p/2}np/2≤Mp​≤(p+n)p/2 (p≥2p\ge2p≥2)

Lemma 1 — Gaussian moment bounds $M_p \le n^{p/2}$ ( $p\in[0,2]$ ), $n^{p/2}\le M_p\le (p+n)^{p/2}$ ( $p\ge2$ )