Theorem 4.10 — Nonconvex SG with Diminishing Step Sizes

Proved

BCN.NonconvexDiminishingStep

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

optimizationprobabilitystochastic-gradient

Mathematical statement

No convexity assumption is made. Let the deterministic positive step sizes satisfy

\sum_{k=0}^{\infty}\alpha_k=\infty, \qquad\sum_{k=0}^{\infty}\alpha_k^2<\infty.

Then the expected weighted partial sums converge to a finite real number, and their step-weighted averages vanish:

\exists S\in\mathbb R,\quad\lim_{K\to\infty}W_K=S, \qquad\lim_{K\to\infty}\frac{W_K}{A_K}=0.

Formalization note: direct source theorem, both conclusions (4.30a)–(4.30b). The existence of a finite limit formalizes the finite expectation limit in (4.30a). It is stronger than merely asserting that each finite partial sum is finite. There is no additional uniform upper bound on all step sizes, no monotonicity requirement, and no assertion that every individual gradient tends to zero. The objective lower bound is required on the open trajectory region.

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. 33 and PDF p. 34, Theorem 4.10, equations (4.30a)–(4.30b); PDF p. 28, step-size condition (4.19).

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 NonconvexDiminishingStep :
  ∀ (d : ℕ) (P : Objective d) (C : MomentConstants)
    (Ω : Type u) [MeasurableSpace Ω] (prob : Measure Ω) [IsProbabilityMeasure prob]
    (α : ℕ → ℝ) (R : Run P C prob α),
    Tendsto (stepSum α) atTop atTop → Summable (fun k ↦ α k ^ 2) →
      (∃ S : ℝ, Tendsto (weightedGradientSum R) atTop (𝓝 S)) ∧
      Tendsto (fun K ↦ weightedGradientSum R K / stepSum α K) atTop (𝓝 0) := 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. 33 and PDF p. 34, Theorem 4.10, equations (4.30a)–(4.30b); PDF p. 28, step-size condition (4.19).

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}$ , every real step sequence $\alpha$ , and every run with these data. 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)$ , $\alpha_j>0$ , the almost-sure update $w_{j+1}=w_j-\alpha_jg_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. For natural $K$ , put $A_K=\sum_{k=0}^{K-1}\alpha_k$ and $W_K=\int_\Omega\sum_{k=0}^{K-1}\alpha_k\|\nabla f(w_k)\|^2\,d\mathbb{P}$ . The target's additional hypotheses are $A_K\to+\infty$ as natural $K\to\infty$ and summability of the real series $\sum_{k=0}^{\infty}\alpha_k^2$ . It concludes both that there exists a real $S$ with $\lim_{K\to\infty}W_K=S$ and that $\lim_{K\to\infty}W_K/A_K=0$ . The existential limit value has no specified formula or uniqueness clause. There is no extra assumption of convexity, failure of convexity, step monotonicity, a particular step formula, or a uniform step-size upper bound. Each step is positive by the run requirements. The finite sums begin at zero; $A_0=W_0=0$ , and the normalized expression at $K=0$ is $0/0=0$ , whereas $A_K>0$ for $K>0$ . The expectations are taken after each finite weighted sum is formed. The dimension $d=0$ , and $M=0$ or $M_V=0$ , are allowed. The regional lower bound $b$ need not equal a global infimum. A nonpositive step, an empty region, or an empty sample type with a probability-measure requirement cannot furnish a run, making universal assertions over such impossible data vacuous. 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