Prove2Me

Theorem 3.2 — expected suboptimality Q(β)/k for the Newton-like iteration (corrected constant)

Proved
StochQuasiNewton.SQN.newton_like_expected_suboptimality

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

convergence-ratep2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1quasi-newtonstochastic-optimization

Let F:Rn→RF:\mathbb R^n\to\mathbb R be C2C^2 with λI≺∇2F(w)≺ΛI\lambda I\prec\nabla^2F(w)\prec\Lambda I for all ww (3.4), 0<λ,Λ0<\lambda,\Lambda, and let w∗w^* minimize FF. Let wk,ξk,Hkw^k,\xi^k,H_k be a Newton-like iteration (3.14) started at w1w^1, with μ1I≺Hk≺μ2I\mu_1I\prec H_k\prec\mu_2I, 0<μ1≤μ20<\mu_1\le\mu_2 (3.15), conditionally unbiased stochastic gradients with conditional second moment at most γ2\gamma^2, and step lengths

αk=βk,β>12μ1λ.\alpha^k=\frac\beta k,\qquad\beta>\frac1{2\mu_1\lambda}.

Then for every k≥1k\ge1, F(wk)F(w^k) is integrable and

E[F(wk)−F(w∗)]≤Qc(β)k,Qc(β)=max⁡{Λμ22β2γ22(2μ1λβ−1), Λμ22β2γ2, F(w1)−F(w∗)}.E[F(w^k)-F(w^*)]\le\frac{Q_c(\beta)}k,\qquad Q_c(\beta)=\max\Big\{\frac{\Lambda\mu_2^2\beta^2\gamma^2}{2(2\mu_1\lambda\beta-1)},\ \Lambda\mu_2^2\beta^2\gamma^2,\ F(w^1)-F(w^*)\Big\}.

This is the O(1/k)O(1/k) convergence rate of stochastic Newton-like methods with uniformly bounded preconditioners, of which the SQN method is a special case.

Formalization Note Corrected constant. The paper states the bound with Q(β)=max⁡{Λμ22β2γ2/(2(2μ1λβ−1)), F(w1)−F(w∗)}Q(\beta)=\max\{\Lambda\mu_2^2\beta^2\gamma^2/(2(2\mu_1\lambda\beta-1)),\,F(w^1)-F(w^*)\} (3.17). That version is false: its induction multiplies the hypothesis by 1−2βμ1λ/k1-2\beta\mu_1\lambda/k, which is negative for k<2βμ1λk<2\beta\mu_1\lambda. Counterexample: n=1n=1, F(w)=w2/2+1/2F(w)=w^2/2+1/2 with stochastic gradients w∓1w\mp1 (each with probability 1/21/2), Hk=IH_k=I, w1=0w^1=0, β=2\beta=2; then F(w2)−F(w∗)=2F(w^2)-F(w^*)=2 surely, while Q(2)/2=5/3Q(2)/2=5/3 with γ2=5\gamma^2=5 (strict hypotheses hold with λ=μ1=1−ε\lambda=\mu_1=1-\varepsilon, Λ=μ2=1+ε\Lambda=\mu_2=1+\varepsilon). The middle entry of QcQ_c repairs the early iterations; Qc=QQ_c=Q whenever 2μ1λβ≤3/22\mu_1\lambda\beta\le3/2. Assumption 1(3). The bound γ2\gamma^2 on the second moment is imposed at the iterates, conditionally on the past, which is how the proof uses (3.5); the paper's "for all ww" is unsatisfiable under (3.4). The hypothesis (3.3) on subsampled Hessians is not used by this theorem and is omitted.

Preamble
import Mathlib
import Definitions.Def_StochQuasiNewton_SQN_FiniteSum
import Definitions.Def_StochQuasiNewton_SQN_NewtonLike

open scoped RealInnerProductSpace
open MeasureTheory
Formal statement
namespace StochQuasiNewton.SQN

/-- Theorem 3.2 (corrected constant): for the Newton-like iteration (3.14) on a `C²` objective
`F` with `λ I ≺ ∇²F(w) ≺ Λ I` (3.4) and minimizer `w*`, with `μ₁ I ≺ H_k ≺ μ₂ I`,
`0 < μ₁ ≤ μ₂` (3.15), step lengths `α^k = β/k` with `β > 1/(2 μ₁ λ)`, and the conditions of
`NewtonLikeIteration`, for every `k ≥ 1`, `F(w^k)` is integrable and
`E[F(w^k) − F(w*)] ≤ Q_c(β)/k`, where
`Q_c(β) = max { Λ μ₂² β² γ² / (2(2 μ₁ λ β − 1)), Λ μ₂² β² γ², F(w¹) − F(w*) }`. -/
theorem newton_like_expected_suboptimality {n : ℕ} {Ω Ξ : Type*} [mΩ : MeasurableSpace Ω]
    [MeasurableSpace Ξ] (P : Measure Ω) [IsProbabilityMeasure P] (ℱ : Filtration ℕ mΩ)
    (F : EuclideanSpace ℝ (Fin n) → ℝ) (hF : ContDiff ℝ 2 F) (lam Lam : ℝ) (hlam : 0 < lam)
    (hLam : 0 < Lam)
    (hHess : ∀ w : EuclideanSpace ℝ (Fin n),
      StrictLoewnerBounds lam Lam (fderiv ℝ (gradient F) w))
    (wstar : EuclideanSpace ℝ (Fin n)) (hwstar : IsMinOn F Set.univ wstar)
    (G : EuclideanSpace ℝ (Fin n) → Ξ → EuclideanSpace ℝ (Fin n)) (γ μ₁ μ₂ β : ℝ)
    (hμ₁ : 0 < μ₁) (hμ : μ₁ ≤ μ₂) (hβ : 1 / (2 * μ₁ * lam) < β)
    (w1 : EuclideanSpace ℝ (Fin n)) (w : ℕ → Ω → EuclideanSpace ℝ (Fin n)) (ξ : ℕ → Ω → Ξ)
    (H : ℕ → Ω → Matrix (Fin n) (Fin n) ℝ)
    (hrun : NewtonLikeIteration P ℱ F G γ (fun k => β / k) μ₁ μ₂ w1 w ξ H) :
    ∀ k : ℕ, 1 ≤ k →
      Integrable (fun ω => F (w k ω)) P ∧
        ∫ ω, (F (w k ω) - F wstar) ∂P ≤
          rateConstant Lam lam μ₁ μ₂ β γ (F w1 - F wstar) / k := by sorry

end StochQuasiNewton.SQN
Source
Byrd, Hansen, Nocedal, Singer, A Stochastic Quasi-Newton Method for Large-Scale Optimization, SIAM J. Optim. 26(2) (2016), pp. 1016–1017, Theorem 3.2, Eqs. (3.14)–(3.17)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph