Theorem 9 — rate of the accelerated random method $\mathcal{FG}_\mu$ (Eq. (62)) — goal theorem

Proved

RandomGradFree.Accelerated.accelerated_random_method_rate

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

accelerated-methodsconvex-optimizationp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1random-searchzeroth-order

Let $E$ be a real inner product space of dimension $n \ge 2$ . Let $f : E \to \mathbb R$ be differentiable with $L_1$ -Lipschitz gradient, $L_1 > 0$ , and strongly convex with parameter $\tau \ge 0$ :

f(y) \ge f(x) + \langle \nabla f(x), y - x\rangle + \frac{\tau}{2}\|y-x\|^2, \qquad x, y \in E

( $\tau = 0$ is allowed and means $f$ is convex). Let $x^*$ be a minimizer of $f$ , and write $f^* = f(x^*)$ and $\kappa = \tau/L_1$ . Let $\mu \ge 0$ , and set

\theta_n = \frac{1}{16(n+4)^2L_1}, \qquad h_n = \frac{1}{4(n+4)L_1}.

Consider a run of the accelerated random method $\mathcal{FG}_\mu$ (Eq. (60)) with these $\theta_n, h_n$ , starting point $x_0$ , sequences $(\gamma_k), (\alpha_k)$ with $\gamma_0 > 0$ , $\gamma_0 \ge \tau$ , and i.i.d. standard Gaussian directions. Let $\phi_k = \mathbb E f(x_k)$ , and let $\psi_k = \prod_{i=0}^{k-1}(1-\alpha_i)$ and $C_k$ ( $C_0 = 0$ , $C_k = 1 + \sum_{i=1}^{k-1}\prod_{j=k-i}^{k-1}(1-\alpha_j)$ ) be as in the proof. Then for every $k \ge 0$ ,

\phi_k - f^* \le \psi_k\Big[f(x_0) - f(x^*) + \frac{\gamma_0}{2}\|x_0 - x^*\|^2\Big] + \mu^2 L_1\Big(n + \frac{3(n+8)}{16}C_k\Big),

where

$\psi_k \le \big(1 - \frac{\kappa^{1/2}}{4(n+4)}\big)^k$ ;
$\psi_k \le \big(1 + \frac{k}{8(n+4)}\sqrt{\gamma_0/L_1}\big)^{-2}$ ;
$C_k \le k$ ;
if $\tau > 0$ , then $C_k \le \frac{4(n+4)}{\kappa^{1/2}}$ .

With $\mu$ small this gives the $O(n^2/k^2)$ rate of an accelerated method that uses only function values, and linear convergence with ratio $1 - \kappa^{1/2}/(4(n+4))$ in the strongly convex case.

Formalization Note The paper prints $\theta_n = 1/(16(n+1)^2L_1(f))$ . This statement uses $\theta_n = 1/(16(n+4)^2L_1(f))$ : the proof (pp. 549–550) needs $h_n/(4(n+4)) - h_n^2L_1/2 = \theta_n/2$ , $[\tau\theta_n]^{1/2} = \kappa^{1/2}/(4(n+4))$ and $\theta_n^{1/2} = 1/(4(n+4)L_1^{1/2})$ , all of which hold only with $(n+4)$ ; with the printed value the first step of the proof fails. The paper's $\min\{\cdot,\cdot\}$ bounds are stated as separate conjuncts; the bound $C_k \le 4(n+4)/\kappa^{1/2}$ is guarded by $\tau > 0$ because at $\tau = 0$ the paper's value is $+\infty$ . Convexity, solvability and $\dim E \ge 2$ are the standing assumptions of problem (53) in Section 5. The oracle at $\mu = 0$ is the limiting oracle $g_0$ . $\phi_k$ is the Bochner integral of $f(x_k)$ ; under the hypotheses it is integrable.

Preamble

import Mathlib
import Definitions.Def_RandomGradFree_Accelerated_psi
import Definitions.Def_RandomGradFree_Accelerated_C
import Definitions.Def_RandomGradFree_Accelerated_IsAcceleratedRandomRun

open MeasureTheory ProbabilityTheory

Formal statement

namespace RandomGradFree.Accelerated

theorem accelerated_random_method_rate {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (hdim : 2 ≤ Module.finrank ℝ E)
    (f : E → ℝ) (L₁ : ℝ) (hL₁ : 0 < L₁) (hdiff : Differentiable ℝ f)
    (hgrad : ∀ x y, ‖gradient f x - gradient f y‖ ≤ L₁ * ‖x - y‖)
    (τ : ℝ) (hτ : 0 ≤ τ)
    (hsc : ∀ x y, f y ≥ f x + inner ℝ (gradient f x) (y - x) + τ / 2 * ‖y - x‖ ^ 2)
    (xstar : E) (hopt : ∀ y, f xstar ≤ f y)
    (μ : ℝ) (hμ : 0 ≤ μ)
    (θ : ℝ) (hθ : θ = 1 / (16 * ((Module.finrank ℝ E : ℝ) + 4) ^ 2 * L₁))
    (h : ℝ) (hh : h = 1 / (4 * ((Module.finrank ℝ E : ℝ) + 4) * L₁))
    (x₀ : E) (γ α : ℕ → ℝ)
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (u x v : ℕ → Ω → E) (hrun : IsAcceleratedRandomRun P f μ τ θ h x₀ γ α u x v) (k : ℕ) :
    (∫ ω, f (x k ω) ∂P) - f xstar
        ≤ psi α k * (f x₀ - f xstar + γ 0 / 2 * ‖x₀ - xstar‖ ^ 2)
          + μ ^ 2 * L₁ * ((Module.finrank ℝ E : ℝ)
            + 3 * ((Module.finrank ℝ E : ℝ) + 8) / 16 * C α k) ∧
      psi α k ≤ (1 - Real.sqrt (τ / L₁) / (4 * ((Module.finrank ℝ E : ℝ) + 4))) ^ k ∧
      psi α k ≤ 1 / (1 + k / (8 * ((Module.finrank ℝ E : ℝ) + 4)) * Real.sqrt (γ 0 / L₁)) ^ 2 ∧
      C α k ≤ k ∧
      (0 < τ → C α k ≤ 4 * ((Module.finrank ℝ E : ℝ) + 4) / Real.sqrt (τ / L₁)) := by sorry

end RandomGradFree.Accelerated

Source

Nesterov, Spokoiny, Random Gradient-Free Minimization of Convex Functions, Found. Comput. Math. 17 (2017), p. 549, Theorem 9, Eq. (62) (with ψ_k, C_k from p. 550 and method (60), parameters θ_n, h_n from p. 548; problem (53) pp. 545-546)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $E$ be a finite-dimensional real inner-product space of dimension $n := \dim_{\mathbb R} E$ . $E$ carries its Borel $\sigma$ -algebra and $n \ge 2$ is assumed. The following data and hypotheses are given:

Objective. $f : E \to \mathbb R$ is differentiable everywhere. Its gradient is $L_1$ -Lipschitz for a constant $L_1 > 0$ :

\|\nabla f(x) - \nabla f(y)\| \le L_1 \|x - y\| \quad \text{for all } x, y \in E.

Strong convexity. $\tau \ge 0$ is a real number, and for all $x, y \in E$ :

f(y) \ge f(x) + \langle \nabla f(x),\, y - x\rangle + \tfrac{\tau}{2}\|y - x\|^2.

When $\tau = 0$ this is just the first-order convexity inequality.

Minimizer. $x^\star \in E$ is a global minimizer: $f(x^\star) \le f(y)$ for every $y \in E$ .
Parameters. $\mu \ge 0$ is a real number. The reals $\theta$ and $h$ are fixed to

\theta = \frac{1}{16\,(n+4)^2 L_1}, \qquad h = \frac{1}{4\,(n+4)\,L_1}.

Both are strictly positive because $L_1 > 0$ .

Starting point and sequences. $x_0 \in E$ is a point. $(\gamma_k)_{k \in \mathbb N}$ and $(\alpha_k)_{k \in \mathbb N}$ are arbitrary real sequences. No sign or size condition is imposed on them in this statement itself.
Probability space. $(\Omega, P)$ is a measurable space with a probability measure $P$ .
Random sequences. $u_k, x_k, v_k : \Omega \to E$ for $k \in \mathbb N$ are three sequences of functions. No measurability or integrability of them is assumed in this statement itself.
Run hypothesis. The hypothesis IsAcceleratedRandomRun holds for the tuple $(P, f, \mu, \tau, \theta, h, x_0, \gamma, \alpha, u, x, v)$ . This predicate is defined in an imported file whose code I was not given. Whatever it requires of $u$ , $x$ , $v$ , $\gamma$ and $\alpha$ (for example a recursion, the distribution of random directions, measurability, or conditions on $\gamma$ and $\alpha$ ), this statement assumes exactly that and nothing more. I cannot say what it contains or whether it can be satisfied.
Iteration index. $k \in \mathbb N$ is arbitrary.

The statement also uses two imported functions whose definitions I was not given: $\psi(\alpha, k)$ (psi α k) and $C(\alpha, k)$ (C α k). Both are real numbers that depend only on the sequence $\alpha$ and the index $k$ . Beyond the inequalities below, the statement asserts nothing about them.

Conclusion. All five of the following hold simultaneously:

The expected value of $f$ at the $k$ -th iterate satisfies

\int_\Omega f(x_k(\omega))\,dP(\omega) - f(x^\star) \;\le\; \psi(\alpha,k)\Big(f(x_0) - f(x^\star) + \tfrac{\gamma_0}{2}\|x_0 - x^\star\|^2\Big) + \mu^2 L_1\Big(n + \tfrac{3(n+8)}{16}\,C(\alpha,k)\Big).

A geometric bound:

\psi(\alpha,k) \le \Big(1 - \frac{\sqrt{\tau/L_1}}{4(n+4)}\Big)^{k}.

A polynomial bound:

\psi(\alpha,k) \le \frac{1}{\Big(1 + \dfrac{k}{8(n+4)}\sqrt{\gamma_0/L_1}\Big)^{2}}.

$C(\alpha,k) \le k$ .
If $\tau > 0$ , then

C(\alpha,k) \le \frac{4(n+4)}{\sqrt{\tau/L_1}}.

Degenerate cases.

The integral in (1). It is the Lebesgue integral of $\omega \mapsto f(x_k(\omega))$ . If that function is not integrable (or not measurable), the integral counts as $0$ , and (1) then reads $-f(x^\star) \le$ the right-hand side. Whether IsAcceleratedRandomRun rules this out cannot be seen here.
$k = 0$ . Conjunct (2) becomes $\psi(\alpha,0) \le 1$ , and (3) also becomes $\psi(\alpha,0) \le 1$ . Conjunct (4) becomes $C(\alpha,0) \le 0$ . Conjunct (5) gives the upper bound $4(n+4)/\sqrt{\tau/L_1}$ when $\tau > 0$ .
$\tau = 0$ . Conjunct (2) reduces to $\psi(\alpha,k) \le 1$ , and (5) is vacuous.
Size of $\tau$ . The Lipschitz-gradient hypothesis together with the strong-convexity inequality forces $\tau \le L_1$ on a nonzero space, and $E$ is nonzero because $n \ge 2$ . Hence $\sqrt{\tau/L_1} \le 1$ , and the base in (2) lies between $1 - \tfrac{1}{24}$ and $1$ .
Negative $\gamma_0$ . No sign is imposed on $\gamma_0$ here. If $\gamma_0 < 0$ , the real square root returns $0$ , so (3) becomes $\psi(\alpha,k) \le 1$ . In that case the term $\tfrac{\gamma_0}{2}\|x_0 - x^\star\|^2$ in (1) is non-positive.
$\mu = 0$ . The additive term in (1) vanishes.
Satisfiability. All hypotheses other than IsAcceleratedRandomRun can be satisfied jointly, for example by a quadratic $f$ . Whether the run hypothesis is satisfiable, and hence whether the theorem is vacuous, depends on the unseen definition.

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 9 — rate of the accelerated random method FGμ\mathcal{FG}_\muFGμ​ (Eq. (62)) — goal theorem

Theorem 9 — rate of the accelerated random method $\mathcal{FG}_\mu$ (Eq. (62)) — goal theorem