Theorem 4.7 — Strongly Convex SG with Diminishing Step Sizes

Proved

BCN.StronglyConvexDiminishingStep

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

optimizationprobabilitystochastic-gradient

Mathematical statement

Assume $d\ge1$ and $F$ is $c$ -strongly convex on all of $\mathbb R^d$ , with $c>0$ . For differentiable $F$ , this means

F(y)\ge F(x)+\nabla F(x)^\top(y-x)+\frac c2\|y-x\|^2 \quad\text{for all }x,y.

The Lean statement uses StrongConvexOn Set.univ c F. Set $F_{\inf}=F_*$ , where $F_*=\inf_x F(x)$ as defined above, and put $\Delta_0=F(w_0)-F_*$ .

Choose real constants $\beta>1/(c\mu)$ and $\gamma>0$ such that $\beta/(\gamma+1)\le\mu/(LM_G)$ , and let $\alpha_k=\beta/(\gamma+k+1)$ . Define

\nu=\max\left\{\frac{\beta^2LM}{2(\beta c\mu-1)}, (\gamma+1)\Delta_0\right\}.

Then $\Delta_k\le\nu/(\gamma+k+1)$ for every $k\ge0$ . Formalization note: direct source theorem, with every index shifted consistently from the paper's first index $1$ to the local first index $0$ . The strict conditions on $c$ , $\beta$ , and $\gamma$ make the displayed denominators positive.

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. 28 and PDF p. 29, Theorem 4.7, equations (4.20)–(4.22).

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 StronglyConvexDiminishingStep :
  ∀ (d : ℕ), 0 < d → ∀ (P : Objective d) (C : MomentConstants)
    (Ω : Type u) [MeasurableSpace Ω] (prob : Measure Ω) [IsProbabilityMeasure prob]
    (c β γ : ℝ), 0 < c → StrongConvexOn Set.univ c P.F →
    1 / (c * C.μ) < β → 0 < γ → β / (γ + 1) ≤ C.μ / (P.L * C.MG) →
    ∀ R : Run P C prob (fun k ↦ β / (γ + (k : ℝ) + 1)),
      R.lower = optimalValue P → ∀ k,
        expectedGap R k ≤ diminishingGapConstant P C R.w0 c β γ / (γ + (k : ℝ) + 1) := 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. 28 and PDF p. 29, Theorem 4.7, equations (4.20)–(4.22).

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>0$ , 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 $c,\beta,\gamma$ . Put $M_G=M_V+\mu_G^2$ . Its extra assumptions are $c>0$ , $c$ -strong convexity of $f$ on all of $E$ , $\beta>1/(c\mu)$ , $\gamma>0$ , and $\beta/(\gamma+1)\le\mu/(LM_G)$ . It quantifies over every run with steps $\alpha_j=\beta/(\gamma+j+1)$ , where the natural index is regarded as real. 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$ , it 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. The target additionally assumes $b=f_*$ , the total real infimum of the range of $f$ . Put $D=\max\left\{\frac{\beta^2LM}{2(\beta c\mu-1)},(\gamma+1)(f(w_{\mathrm{init}})-f_*)\right\}$ . It asserts $\int_\Omega(f(w_k)-f_*)\,d\mathbb{P}\le D/(\gamma+k+1)$ for every natural $k$ . The first step is $\beta/(\gamma+1)$ , and the conclusion includes $k=0$ with denominator $\gamma+1$ . The assumptions ensure $\beta>0$ , $\beta c\mu-1>0$ , and $\gamma+k+1>0$ for every natural $k$ , so all displayed denominators are positive. Dimension zero is excluded; $M=0$ and $M_V=0$ are allowed. The infimum is total, with value zero for an unbounded-below range; attainment of a minimizer is not a separate hypothesis. An empty region or empty sample type cannot furnish the required run and probability measure. 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