Prove2Me

(4.17) — under (4.8) at every iteration, J(wk)≤(1−βλ/L)kJ(w0)J(w_k) \le (1-\beta\lambda/L)^k J(w_0)

Proved
DynSampleSize.Det.eq_4_17

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

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

Let J:Rm→RJ : \mathbb{R}^m \to \mathbb{R} satisfy assumption (4.2) with constants 0<λ<L0<\lambda<L, and let w∗w_* be its minimizer, normalized so that J(w∗)=0J(w_*) = 0. Let θ∈(0,1)\theta \in (0,1), let (gk)(g_k) be arbitrary vectors and let wk+1=wk−1−θLgkw_{k+1} = w_k - \frac{1-\theta}{L} g_k (iteration (4.1) with steplength (4.7)). If the relative-error condition (4.8), ∥gj−∇J(wj)∥≤θ∥gj∥\|g_j - \nabla J(w_j)\| \le \theta\|g_j\|, holds at every iteration j<kj < k, then

J(wk)  ≤  (1−βλL)kJ(w0),β=(1−θ)22(1+θ)2.J(w_k) \;\le\; \Bigl(1 - \frac{\beta\lambda}{L}\Bigr)^{k} J(w_0), \qquad \beta = \frac{(1-\theta)^2}{2(1+\theta)^2}.

This is the linear convergence of the function values, from which (4.10), (4.11) and (4.12) of Theorem 4.1 follow.

Formalization Note The paper assumes (4.8) "at every iteration"; the Lean statement assumes it only for the iterations j<kj < k that precede wkw_k, which is a slightly stronger statement implied by the same proof.

Preamble
import Mathlib
import Definitions.Def_DynSampleSize_Det_Setting

open Filter Topology
Formal statement
namespace DynSampleSize.Det

theorem eq_4_17 {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) (k : ℕ)
    (h48 : ∀ j < k, ‖g j - gradient J (w j)‖ ≤ θ * ‖g j‖) :
    J (w k) ≤ (1 - beta θ * lam / L) ^ k * J (w 0) := 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. 9, (4.17)
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