Theorem 4.1 — steepest descent with relative gradient error $\theta$ contracts $J$ by $1-\beta\lambda/L$ per step

Proved

DynSampleSize.Det.theorem_4_1

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexitygradient-methodsinexact-gradientlinear-convergencep2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $J : \mathbb{R}^m \to \mathbb{R}$ be twice continuously differentiable and uniformly convex, satisfying (4.2):

\lambda\|d\|_2^2 \le d^T\nabla^2 J(w)\,d \le L\|d\|_2^2 \qquad\text{for all } w, d,

with constants $0<\lambda<L$ . Let $w_*$ be its minimizer and assume $J(w_*) = 0$ . Let $\theta \in (0,1)$ , let $(g_k)_{k \ge 0}$ be arbitrary vectors (approximations to $\nabla J(w_k)$ ), and let $\{w_k\}$ be generated by iteration (4.1) with the steplength (4.7),

w_{k+1} = w_k - \alpha g_k, \qquad \alpha = \frac{1-\theta}{L}.

Put $\beta = \dfrac{(1-\theta)^2}{2(1+\theta)^2}$ . Then:

(4.9) If at an iteration $k$ the approximate gradient satisfies (4.8), $\|g_k - \nabla J(w_k)\| \le \theta\|g_k\|$ , then

J(w_{k+1}) \le \Bigl(1 - \frac{\beta\lambda}{L}\Bigr) J(w_k).

If moreover (4.8) holds at every iteration, then:

(4.10) $w_k \to w_*$ .
(4.11) For every $\epsilon > 0$ , every iteration count $k$ with

k > \frac{L}{\beta\lambda}\bigl[\log(1/\epsilon) + \log J(w_0)\bigr]

satisfies $J(w_k) < \epsilon = J(w_*) + \epsilon$ ; that is, the number of iterations needed to reach $J(w_j) \le J(w_*) + \epsilon$ is at most $\frac{L}{\beta\lambda}[\log(1/\epsilon) + \log J(w_0)]$ . 4. (4.12) For every $k$ ,

\|g_k\|^2 \le \frac{1}{(1-\theta)^2}\,\frac{2L^2 J(w_0)}{\lambda}\Bigl(1 - \frac{\beta\lambda}{L}\Bigr)^k.

The theorem shows that a gradient approximation whose error is at most a fixed fraction $\theta$ of its own norm preserves the linear convergence rate of steepest descent, at the price of the factor $\beta$ . It motivates the sample-size rule of the stochastic analysis in §4.2.

Formalization Note The space is EuclideanSpace ℝ (Fin m), lam is the paper's $\lambda$ , and assumption (4.2) is HessianBounds J lam L. The minimizer is a point $w_*$ with $J(w_*) \le J(w)$ for all $w$ , and $J(w_*) = 0$ is a hypothesis. (4.11) is stated in the form the proof establishes ((4.18), p. 10): every $k$ beyond the bound is $\epsilon$ -accurate; $\log$ is the natural logarithm. If $J(w_0) = 0$ Lean's convention $\log 0 = 0$ applies, and the statement remains true because then every iterate is optimal.

Preamble

import Mathlib
import Definitions.Def_DynSampleSize_Det_Setting

open Filter Topology

Formal statement

namespace DynSampleSize.Det

theorem theorem_4_1 {m : ℕ} (J : EuclideanSpace ℝ (Fin m) → ℝ) (lam L : ℝ)
    (hJ : HessianBounds J lam L) (wstar : EuclideanSpace ℝ (Fin m))
    (hmin : ∀ w, J wstar ≤ J w) (hJstar : J wstar = 0)
    (θ : ℝ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (g w : ℕ → EuclideanSpace ℝ (Fin m))
    (hw : ∀ k, w (k + 1) = w k - ((1 - θ) / L) • g k) :
    -- (4.9): one step, under (4.8) at that iteration only
    (∀ k, ‖g k - gradient J (w k)‖ ≤ θ * ‖g k‖ →
        J (w (k + 1)) ≤ (1 - beta θ * lam / L) * J (w k)) ∧
    -- (4.10)–(4.12): under (4.8) at every iteration
    ((∀ k, ‖g k - gradient J (w k)‖ ≤ θ * ‖g k‖) →
        Tendsto w atTop (𝓝 wstar) ∧
        (∀ ε : ℝ, 0 < ε → ∀ k : ℕ,
            L / (beta θ * lam) * (Real.log (1 / ε) + Real.log (J (w 0))) < (k : ℝ) →
              J (w k) < ε) ∧
        (∀ k : ℕ, ‖g k‖ ^ 2 ≤
            1 / (1 - θ) ^ 2 * (2 * L ^ 2 * J (w 0) / lam) * (1 - beta θ * lam / L) ^ k)) := by sorry

end DynSampleSize.Det

Source

Byrd, Chin, Nocedal, Wu, Sample size selection in optimization methods for machine learning, Math. Program. (2012), doi:10.1007/s10107-012-0572-5 — authors' version of 18 Oct 2011, p. 8, Theorem 4.1, (4.7)–(4.12); proof pp. 9–10, (4.18)

Human review

Endorsed by Shuze Chen · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 4.1 — steepest descent with relative gradient error θ\thetaθ contracts JJJ by 1−βλ/L1-\beta\lambda/L1−βλ/L per step

Theorem 4.1 — steepest descent with relative gradient error $\theta$ contracts $J$ by $1-\beta\lambda/L$ per step