Prove2Me

p. 156 — ∥xb−xa∥≤∑s=ab−1∥xs+1−xs∥≤C∑s=ab−1ρs\|x^{b} - x^{a}\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s

Proved
NumStochOpt.Nonstationary.lemma_p156_step_bound

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

p2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1projectionstochastic-optimizationsubgradient-method

Let X⊆RnX \subseteq \mathbb R^n be a convex compact set, ρs≥0\rho_s \ge 0, and let gs∈Rng_s \in \mathbb R^n satisfy ∥gs∥≤C\|g_s\| \le C for all ss. Let (xs)(x^s) satisfy the projected subgradient recursion (6.41)

xs+1=πX[xs−ρsgs],s=0,1,…x^{s+1} = \pi_X[x^s - \rho_s g_s], \qquad s = 0, 1, \dots

If a≤ba \le b and xa∈Xx^a \in X, then

∥xb−xa∥  ≤  ∑s=ab−1∥xs+1−xs∥  ≤  C∑s=ab−1ρs.\|x^b - x^a\| \;\le\; \sum_{s=a}^{b-1} \|x^{s+1} - x^s\| \;\le\; C \sum_{s=a}^{b-1} \rho_s .

In the proof of Theorem 6.3 this bounds the distance travelled between the index sks_k of a subsequence and the exit time τk\tau_k, which converts the decrease of VV into a decrease proportional to ε\varepsilon.

Formalization Note The book writes "where CC is a constant"; the proof yields CC = the constant of hypothesis (d) of Theorem 6.3, ∥gs∥≤C\|g_s\| \le C. The hypothesis xa∈Xx^a \in X holds for every a≥1a \ge 1 (all iterates after the first are projections onto XX); in the book a=ska = s_k is large. ρs≥0\rho_s \ge 0 is the step-size convention of the chapter, not printed in Theorem 6.3.

Preamble
import Mathlib
import Definitions.Def_NumStochOpt_QuasiFejer_ProjectionMethod
Formal statement
namespace NumStochOpt.Nonstationary

/-- Proof of Theorem 6.3, p. 156 (unnumbered display): "in view of the properties of `π_X`",
`‖x^τ - x^a‖ ≤ ∑_{s=a}^{τ-1} ‖x^{s+1} - x^s‖ ≤ C ∑_{s=a}^{τ-1} ρ_s` along the iteration (6.41)
`x^{s+1} = π_X[x^s - ρ_s g_s]`, where `C` is the bound of hypothesis (d), `‖g_s‖ ≤ C`, and
`x^a ∈ X` (which holds for every `a ≥ 1`). -/
theorem lemma_p156_step_bound {n : ℕ}
    (X : Set (EuclideanSpace ℝ (Fin n))) (hXconv : Convex ℝ X) (hXcpt : IsCompact X)
    (x g : ℕ → EuclideanSpace ℝ (Fin n)) (ρ : ℕ → ℝ) (C : ℝ)
    (hrec : ∀ s, x (s + 1) = NumStochOpt.QuasiFejer.projX X (x s - ρ s • g s))
    (hρnn : ∀ s, 0 ≤ ρ s) (hbound : ∀ s, ‖g s‖ ≤ C)
    (a b : ℕ) (hab : a ≤ b) (hxa : x a ∈ X) :
    ‖x b - x a‖ ≤ ∑ s ∈ Finset.Ico a b, ‖x (s + 1) - x s‖ ∧
      ∑ s ∈ Finset.Ico a b, ‖x (s + 1) - x s‖ ≤ C * ∑ s ∈ Finset.Ico a b, ρ s := by sorry

end NumStochOpt.Nonstationary
Source
Yu. Ermoliev, "Stochastic Quasigradient Methods", in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer 1988, Ch. 6, p. 156, proof of Theorem 6.3, unnumbered display
Human review

  • Endorsed by Shuze Chen · Oct 5, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 5, 2026

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

View graph