Prove2Me

(4.6) — the optimality gap bounds the squared gradient: J(w)−J(w∗)≥λ2L2∥∇J(w)∥22J(w)-J(w_*) \ge \frac{\lambda}{2L^2}\|\nabla J(w)\|_2^2

Proved
DynSampleSize.Det.eq_4_6

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

convex-optimizationgradient-methodsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let J:Rm→RJ : \mathbb{R}^m \to \mathbb{R} be twice continuously differentiable with Hessian bounds λ∥d∥2≤dT∇2J(w)d≤L∥d∥2\lambda\|d\|^2 \le d^T\nabla^2J(w)d \le L\|d\|^2 for all w,dw, d, where 0<λ<L0<\lambda<L (assumption (4.2)), and let w∗w_* be a minimizer of JJ. Then for every w∈Rmw \in \mathbb{R}^m,

J(w)−J(w∗)  ≥  λ2L2 ∥∇J(w)∥22.J(w) - J(w_*) \;\ge\; \frac{\lambda}{2L^2}\,\|\nabla J(w)\|_2^2 .

Together with (4.5) this shows that J(w)−J(w∗)J(w)-J(w_*) and ∥∇J(w)∥2\|\nabla J(w)\|^2 are equivalent up to constants depending on λ\lambda and LL. In Theorem 4.1 it converts the linear decay of J(wk)J(w_k) into the bound (4.12) on the approximate gradients.

Formalization Note Stated for an arbitrary point ww rather than an iterate wkw_k. The minimizer is a point w∗w_* with J(w∗)≤J(w)J(w_*) \le J(w) for all ww.

Preamble
import Mathlib
import Definitions.Def_DynSampleSize_Det_Setting

open Filter Topology
Formal statement
namespace DynSampleSize.Det

theorem eq_4_6 {m : ℕ} (J : EuclideanSpace ℝ (Fin m) → ℝ) (lam L : ℝ)
    (hJ : HessianBounds J lam L) (wstar : EuclideanSpace ℝ (Fin m))
    (hmin : ∀ w, J wstar ≤ J w) (w : EuclideanSpace ℝ (Fin m)) :
    lam / (2 * L ^ 2) * ‖gradient J w‖ ^ 2 ≤ J w - J wstar := 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, (4.6)
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