Theorem 4.2 — with $n_k \ge a^k$ , dynamic batch steepest descent satisfies $E[J(w_k)-J(w^*)] \le C\rho^k$

Proved

DynSampleSize.Stoch.theorem_4_2

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

linear-convergencemini-batchp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1sample-sizestochastic-optimization

Let $(Z,P)$ be a probability space of data points, $\ell(w;z)$ a per-sample loss on $\mathbb R^m$ with gradient $\nabla\ell(w;z)$ , and $J(w)=\int\ell(w;z)\,dP(z)$ the expected loss (2.1), under the stochastic model of §4.2 (integrable loss, jointly measurable gradient with finite second moment, and $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$ ). Assume:

$J$ is twice continuously differentiable and uniformly convex: $\lambda\|d\|^2\le d^T\nabla^2J(w)d\le L\|d\|^2$ for all $w,d$ , with $0<\lambda<L$ (4.2); $w^*$ is a minimizer of $J$ ;
there is a constant $\omega$ with $\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1\le\omega$ for all $w$ (4.22);
the sample sizes satisfy $n_k\ge a^k$ for all $k$ , for some $a>1$ .

Let $\{w_k\}$ be generated by the dynamic batch algorithm (4.24), $w_{k+1}=w_k-\frac1L g_k$ , where $g_k$ is the mean of $\nabla\ell(w_k;\cdot)$ over a batch of $n_k$ independent draws from $P$ , drawn independently across iterations, starting from $w_0$ . Then

\mathbb E[J(w_k)-J(w^*)]\;\le\;C\rho^k\qquad\text{for all }k,

where

\rho=\max\{1-\lambda/(4L),\,1/a\}<1\qquad\text{and}\qquad C=\max\{J(w_0)-J(w^*),\,2\omega/\lambda\}.

The statement also asserts that $J(w_k)$ is integrable for every $k$ , so the expectation exists.

Geometric growth of the batch size thus buys linear convergence in expectation, at a rate set by the slower of the deterministic contraction $1-\lambda/(4L)$ and the batch growth $1/a$ .

Formalization Note Draw $i$ of iteration $k$ is $\xi_{k,i}$ , and all draws are independent with law $P$ (Measure.infinitePi over $\mathbb N\times\mathbb N$ ); the paper's sampling without replacement from $N$ points is replaced by its $N\to\infty$ limit, sampling with replacement (p. 5). The loss is a general differentiable $\ell$ ; the paper's linear predictor and convex $l$ are not used by the theorem. λ is written lam.

Preamble

import Mathlib
import Definitions.Def_DynSampleSize_Stoch_UniformConvexity
import Definitions.Def_DynSampleSize_Stoch_Model
import Definitions.Def_DynSampleSize_Stoch_Run

open MeasureTheory

Formal statement

namespace DynSampleSize.Stoch

/-- Theorem 4.2, p. 12: if the sample sizes satisfy `n_k ≥ a^k` for some `a > 1` and (4.22) holds,
the dynamic batch run (4.24) satisfies `E[J(w_k) − J(w*)] ≤ C ρ^k` for all `k`, with
`ρ = max{1 − λ/(4L), 1/a} < 1` and `C = max{J(w₀) − J(w*), 2ω/λ}` (4.28)–(4.29). -/
theorem theorem_4_2 {m : ℕ} {Z : Type*} [MeasurableSpace Z] (P : Measure Z)
    [IsProbabilityMeasure P]
    (ℓ : EuclideanSpace ℝ (Fin m) → Z → ℝ)
    (gradℓ : EuclideanSpace ℝ (Fin m) → Z → EuclideanSpace ℝ (Fin m))
    (hmodel : StochModel P ℓ gradℓ) (lam L : ℝ) (hJ : UniformlyConvex (objective P ℓ) lam L)
    (wstar : EuclideanSpace ℝ (Fin m)) (hwstar : ∀ w, objective P ℓ wstar ≤ objective P ℓ w)
    (ω : ℝ) (hω : ∀ w, vecVar P (gradℓ w) ≤ ω)
    (a : ℝ) (ha : 1 < a) (n : ℕ → ℕ) (hn : ∀ k, a ^ k ≤ (n k : ℝ))
    (w0 : EuclideanSpace ℝ (Fin m)) :
    max (1 - lam / (4 * L)) (1 / a) < 1 ∧
      ∀ k : ℕ,
        Integrable (fun ξ => objective P ℓ (run L gradℓ n w0 ξ k)) (sampleLaw P) ∧
          ∫ ξ, (objective P ℓ (run L gradℓ n w0 ξ k) - objective P ℓ wstar) ∂(sampleLaw P) ≤
            max (objective P ℓ w0 - objective P ℓ wstar) (2 * ω / lam) *
              (max (1 - lam / (4 * L)) (1 / a)) ^ k := by sorry

end DynSampleSize.Stoch

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. 12, Theorem 4.2, (4.28)–(4.29)

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.2 — with nk≥akn_k \ge a^knk​≥ak, dynamic batch steepest descent satisfies E[J(wk)−J(w∗)]≤CρkE[J(w_k)-J(w^*)] \le C\rho^kE[J(wk​)−J(w∗)]≤Cρk

Theorem 4.2 — with $n_k \ge a^k$ , dynamic batch steepest descent satisfies $E[J(w_k)-J(w^*)] \le C\rho^k$