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

Proved

RandomGradFree.Smooth.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 finite 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 the second moments of the random oracles into explicit dimension-dependent constants; the case $p = 6$ produces the factor $(n+6)^3$ in the variance bound (35).

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_moment

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Smooth

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

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

Setting. $E$ is a finite-dimensional real inner product space with its Borel σ-algebra, and $p$ is any real number. Write $n = \dim_{\mathbb{R}} E$ . Write $M_p = \mathrm{moment}(E, p)$ for the imported definition RandomGradFree.Shared.moment. Its body is not included in the code provided, so this read-back cannot unfold it.

Claim. The theorem asserts both of the following:

(a) If $0 \le p \le 2$ , then

M_p \;\le\; n^{p/2}.

(b) If $p \ge 2$ , then

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

Powers are real powers of nonnegative bases. At $p = 2$ both (a) and (b) apply, which gives $n \le M_2 \le n$ together with $M_2 \le 2+n$ . For $p < 0$ the theorem claims nothing.

Degenerate cases.

$n = 0$ ( $E = \{0\}$ $E = {0}$ ). The convention $0^0 = 1$ $0^{0} = 1$ applies.
- At $p = 0$ , part (a) says $M_0 \le 1$ .
- For $0 < p \le 2$ , part (a) says $M_p \le 0$ .
- For $p \ge 2$ , part (b) says $0 \le M_p \le p^{p/2}$ .
$p = 0$ for any $n$ . Part (a) says $M_0 \le 1$ .

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≤2p\le2p≤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\le2$ ), $n^{p/2}\le M_p\le(p+n)^{p/2}$ ( $p\ge2$ )