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 \ge 2$ )

Proved

RandomGradFree.Accelerated.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$ and let $M_p = \mathbb E_u\|u\|^p$ be the $p$ -th moment of the norm of a standard Gaussian vector $u$ in $E$ . 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 are used to control the second moment of the random gradient-free oracle, in particular through $M_6 \le (n+6)^3$ .

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Shared_moment

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Accelerated

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

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$ : a finite-dimensional real inner product space with its Borel σ-algebra, of dimension $n = \dim_{\mathbb R} E$ .
$p$ : any real number.
$M_p$ : the real number RandomGradFree.Shared.moment E p. Its definition is not in the code provided, and this read-back does not describe it.

Here $a^{p/2}$ is the real power function.

The theorem asserts two statements together:

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

At $p = 2$ both parts apply, so together they give $M_2 = n$ exactly. For $p < 0$ nothing is asserted.

Degenerate cases, for $n = 0$ (the zero space) under the real-power conventions $0^0 = 1$ and $0^x = 0$ for $x \neq 0$ :

Part 1 gives $M_0 \le 1$ , and $M_p \le 0$ for $0 < p \le 2$ .
Part 2 gives $0 \le M_p \le p^{p/2}$ for $p \ge 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 \ge 2p≥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 \ge 2$ )