Theorem 4.8 — Nonconvex SG with Fixed Step Size

Proved

BCN.NonconvexFixedStep

by Minghui · Sep 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

optimizationprobabilitystochastic-gradient

Mathematical statement

Choose $0<a\le\mu/(LM_G)$ and $\alpha_k=a$ for every $k\ge0$ . No convexity assumption is made. For every integer $K\ge1$ ,

G_K\le\frac{KaLM}{\mu}+ \frac{2(F(w_0)-F_{\inf})}{\mu a},

\frac{G_K}{K}\le\frac{aLM}{\mu}+ \frac{2(F(w_0)-F_{\inf})}{K\mu a}.

The right-hand side of the second inequality tends to $aLM/\mu$ as $K\to\infty$ . Formalization note: direct source theorem, both bounds (4.28a)–(4.28b), with explicit convergence of the second bound. The conclusion is about average squared gradients; it does not assert an individual-iterate limit.

Source: Léon Bottou, Frank E. Curtis, Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning, arXiv:1606.04838v3, https://arxiv.org/abs/1606.04838v3; Section 4, PDF p. 32, Theorem 4.8, equations (4.27)–(4.28).

Notation and probability model

Let $d\in\mathbb N$ and $F:\mathbb R^d\to\mathbb R$ have an actual gradient $\nabla F$ at every point, with $\|\nabla F(x)-\nabla F(y)\|\le L\|x-y\|$ for all $x,y$ , where $L>0$ . On a probability space $(\Omega,\mathcal A,\mathbb P)$ , let $(\mathcal F_k)_{k\ge0}$ be an increasing family of sub- $\sigma$ -algebras of $\mathcal A$ . The initial vector $w_0$ is deterministic. The iterate $w_k$ is strongly $\mathcal F_k$ -measurable, and the sampled direction $g_k$ is strongly $\mathcal F_{k+1}$ -measurable with $\mathbb E\|g_k\|^2<\infty$ . For deterministic real step sizes $\alpha_k>0$ , the algorithm is

w_{k+1}=w_k-\alpha_k g_k\quad\text{almost surely}.

An open set $U\subseteq\mathbb R^d$ contains every iterate almost surely, and a real number $F_{\inf}$ satisfies $F(x)\ge F_{\inf}$ for all $x\in U$ . Put $m_k=\mathbb E[g_k\mid\mathcal F_k]$ . Fix real constants $0<\mu\le\mu_G$ , $M\ge0$ , $M_V\ge0$ , and $M_G=M_V+\mu_G^2$ . The source's first- and second-moment assumptions are, almost surely for every $k$ ,

\nabla F(w_k)^\top m_k\ge\mu\|\nabla F(w_k)\|^2, \qquad\|m_k\|\le\mu_G\|\nabla F(w_k)\|,

\mathbb E[\|g_k\|^2\mid\mathcal F_k]-\|m_k\|^2 \le M+M_V\|\nabla F(w_k)\|^2.

Write $q_k=\|\nabla F(w_k)\|^2$ , $A_K=\sum_{k=0}^{K-1}\alpha_k$ , $W_K=\mathbb E[\sum_{k=0}^{K-1}\alpha_k q_k]$ , and $G_K=\mathbb E[\sum_{k=0}^{K-1}q_k]$ ; empty sums are zero. Define $F_*:=\inf_{x\in\mathbb R^d}F(x)$ using the actual objective's range (Lean's real-valued sInf), and $\Delta_k=\mathbb E[F(w_k)-F_*]$ when stating the strongly convex targets. Those targets require $d\ge1$ , positive strong-convexity modulus, and $F_{\inf}=F_*$ . The other targets permit $d=0$ and use the trajectory-region lower bound $F_{\inf}$ , without assuming a global minimizer.

Formalization note: these are source assumptions with explicit filtration, measurability, and finite-second-moment conventions for genuine Bochner and conditional expectations. The deterministic initialization and square-integrable directions imply finite iterate second moments; objective and gradient moments must be justified from smoothness in the proofs. The model assumes no expected descent inequality, no gradient-gap inequality, and no convergence conclusion. Local index $0$ is paper index $1$ throughout. Full-history conditioning follows Algorithm 4.1, PDF p. 22, footnote 4; the model assumptions are Assumptions 4.1 and 4.3, PDF p. 23 and PDF p. 24, equations (4.6)–(4.9), in Section 4 of Bottou–Curtis–Nocedal, Optimization Methods for Large-Scale Machine Learning: https://arxiv.org/abs/1606.04838v3.

Preamble

import Definitions.Def_BCN_SG_Model
open MeasureTheory Filter
open scoped Topology
universe u

Formal statement

namespace BCN
theorem NonconvexFixedStep :
  ∀ (d : ℕ) (P : Objective d) (C : MomentConstants)
    (Ω : Type u) [MeasurableSpace Ω] (prob : Measure Ω) [IsProbabilityMeasure prob]
    (a : ℝ), 0 < a → a ≤ C.μ / (P.L * C.MG) →
    ∀ R : Run P C prob (fun _ ↦ a),
      (∀ K : ℕ, 0 < K →
        gradientSum R K ≤ (K : ℝ) * a * P.L * C.M / C.μ +
          2 * (P.F R.w0 - R.lower) / (C.μ * a)) ∧
      (∀ K : ℕ, 0 < K →
        gradientSum R K / (K : ℝ) ≤ a * P.L * C.M / C.μ +
          2 * (P.F R.w0 - R.lower) / ((K : ℝ) * C.μ * a)) ∧
      Tendsto (fun K : ℕ ↦ a * P.L * C.M / C.μ +
        2 * (P.F R.w0 - R.lower) / ((K : ℝ) * C.μ * a)) atTop
        (𝓝 (a * P.L * C.M / C.μ)) := by sorry
end BCN

Source

Léon Bottou, Frank E. Curtis, Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning, arXiv:1606.04838v3, https://arxiv.org/abs/1606.04838v3; Section 4, PDF p. 32, Theorem 4.8, equations (4.27)–(4.28).

Read-back

What the Lean code literally says, in plain math · gpt-6

This declaration is an unproved theorem target. It quantifies universally over every natural $d$ , the Euclidean space $E=\mathbb{R}^d$ , every objective $f:E\to\mathbb{R}$ with a gradient at every point and a real $L>0$ satisfying $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$ , every real $\mu,\mu_G,M,M_V$ with $0<\mu\le\mu_G$ , $M\ge0$ , and $M_V\ge0$ , every sample type $\Omega$ in its arbitrary universe with a measurable-space structure and probability measure $\mathbb{P}$ , and every real $a$ . Put $M_G=M_V+\mu_G^2$ . It assumes $a>0$ and $a\le\mu/(LM_G)$ and quantifies over every run with constant steps $\alpha_j=a$ . A run supplies an increasing filtration $(\mathcal{H}_j)$ of sub- $\sigma$ -algebras of the ambient measurable space, functions $w_j,g_j:\Omega\to E$ , a deterministic vector $w_{\mathrm{init}}$ , an open set $U$ , and a real $b$ . It requires $w_0(\omega)=w_{\mathrm{init}}$ for every $\omega$ ; for every natural $j$ , strong $\mathcal{H}_j$ -measurability of $w_j$ , strong $\mathcal{H}_{j+1}$ -measurability of $g_j$ , $g_j\in L^2(\mathbb{P};E)$ , positive steps, the almost-sure update $w_{j+1}=w_j-ag_j$ , and almost-sure membership $w_j\in U$ ; and $b\le f(x)$ for every $x\in U$ . Put $v_j=\nabla f(w_j)$ , $m_j=\mathbb{E}[g_j\mid\mathcal{H}_j]$ , and $q_j=\mathbb{E}[\|g_j\|^2\mid\mathcal{H}_j]$ . For every $j$ , the run requires almost surely $\mu\|v_j\|^2\le\langle v_j,m_j\rangle$ , $\|m_j\|\le\mu_G\|v_j\|$ , and $q_j-\|m_j\|^2\le M+M_V\|v_j\|^2$ . Almost-sure requirements are separate at each index. Neither convexity nor failure of convexity is required. Define $G_K=\int_\Omega\sum_{k=0}^{K-1}\|\nabla f(w_k)\|^2\,d\mathbb{P}$ for natural $K$ . The target asserts three conclusions in conjunction: for every natural $K>0$ , $G_K\le\frac{KaLM}{\mu}+\frac{2(f(w_{\mathrm{init}})-b)}{\mu a}$ ; for every natural $K>0$ , $G_K/K\le\frac{aLM}{\mu}+\frac{2(f(w_{\mathrm{init}})-b)}{K\mu a}$ ; and $\lim_{K\to\infty}\left(\frac{aLM}{\mu}+\frac{2(f(w_{\mathrm{init}})-b)}{K\mu a}\right)=\frac{aLM}{\mu}$ . Natural indices in real expressions are coerced to real numbers. The limit concerns the explicit right-hand-side sequence. The run's bound $b$ is only required on its open region and need not equal a global infimum. The sum ranges from zero through $K-1$ and has value zero at $K=0$ . The finite-horizon inequalities are restricted to $K>0$ , where their denominators are positive. The sequence whose limit is asserted is also defined at $K=0$ and has value $aLM/\mu$ there by total division. The cases $d=0$ , $M=0$ , and $M_V=0$ are allowed. An empty region or empty sample type cannot furnish the required data. Expectations use total Bochner integrals, zero on nonintegrable inputs; conditional expectations use total mathematical-library definitions, including zero when required integrability fails. No separate loss-integrability or squared-gradient-integrability field is assumed. Real division has $x/0=0$ .

Human review

Endorsed by Shuze Chen · Sep 26, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph