Lemma 4.4 — Expected Descent

Proved

BCN.ExpectedDescent

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

optimizationprobabilitystochastic-gradient

Mathematical statement

Under the common model assumptions, for every $k\ge0$ , both inequalities hold almost surely:

\begin{aligned} \mathbb E[F(w_{k+1})\mid\mathcal F_k]-F(w_k) &\le-\mu\alpha_k q_k+ \frac{\alpha_k^2L}{2}\mathbb E[\|g_k\|^2\mid\mathcal F_k]\\ &\le-\left(\mu-\frac{\alpha_kLM_G}{2}\right)\alpha_k q_k +\frac{\alpha_k^2LM}{2}. \end{aligned}

Formalization note: direct source theorem with full-history conditioning explicit. No upper bound on the positive step size is needed for this lemma.

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. 24 and PDF p. 25, Lemma 4.4, equations (4.10a)–(4.10b).

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 ExpectedDescent :
  ∀ (d : ℕ) (P : Objective d) (C : MomentConstants)
    (Ω : Type u) [MeasurableSpace Ω] (prob : Measure Ω) [IsProbabilityMeasure prob]
    (α : ℕ → ℝ) (R : Run P C prob α) (k : ℕ),
    (∀ᵐ ω ∂prob, prob[loss R (k + 1) | R.history k] ω - loss R k ω ≤
      -(C.μ * α k) * gradSq R k ω + α k ^ 2 * P.L / 2 *
        prob[(fun ω ↦ ‖R.g k ω‖ ^ 2) | R.history k] ω) ∧
    (∀ᵐ ω ∂prob,
      -(C.μ * α k) * gradSq R k ω + α k ^ 2 * P.L / 2 *
        prob[(fun ω ↦ ‖R.g k ω‖ ^ 2) | R.history k] ω ≤
      -(C.μ - α k * P.L * C.MG / 2) * α k * gradSq R k ω +
        α k ^ 2 * P.L * C.M / 2) := 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. 24 and PDF p. 25, Lemma 4.4, equations (4.10a)–(4.10b).

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$ satisfying $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$ , every run with these data, and every natural $k$ . Write $M_G=M_V+\mu_G^2$ . 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$ , $w_{j+1}=w_j-\alpha_jg_j$ almost surely, and $w_j\in U$ almost surely; and $b\le f(x)$ for all $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 further 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 conclusion is the conjunction of two almost-sure assertions: $\mathbb{E}[f(w_{k+1})\mid\mathcal{H}_k]-f(w_k)\le-\mu\alpha_k\|v_k\|^2+\frac{\alpha_k^2L}{2}q_k$ and $-\mu\alpha_k\|v_k\|^2+\frac{\alpha_k^2L}{2}q_k\le-\left(\mu-\frac{\alpha_kLM_G}{2}\right)\alpha_k\|v_k\|^2+\frac{\alpha_k^2LM}{2}$ . Each assertion has its own almost-everywhere quantifier. There is no extra upper bound on the positive steps. The cases $d=0$ , $k=0$ , $M=0$ , and $M_V=0$ are included. An empty region, an empty sample type with a probability-measure requirement, or a step sequence with a nonpositive entry cannot furnish a run; universal assertions over such impossible data are vacuous. Expectations use total Bochner integrals, zero on nonintegrable inputs, and conditional expectations use their total mathematical-library definitions, including zero when required integrability fails. No separate loss-integrability or squared-gradient-integrability field is assumed. Division is total with $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