Prove2Me

Lemma 2 — bounded iterates keep (λk)(\lambda_k) and (θk)(\theta_k) bounded and separated from 0

Proved
GoldenRatioVI.Explicit.steps_bounded_below

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

golden-ratio-algorithmp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1step-size

Let E\mathcal E be a finite-dimensional real inner product space, let gg satisfy (C2), and let FF be Lipschitz on every bounded subset of dom⁡g\operatorname{dom} g. Consider a run of Algorithm 1 with stepsizes (λk)(\lambda_k), ratios (θk)(\theta_k) and iterates (zk)(z^k). If (zk)(z^k) is bounded, then there are constants 0<c≤C0<c\le C and 0<c′≤C′0<c'\le C' with

c≤λk≤Candc′≤θk≤C′for all k≥0.c\le\lambda_k\le C \quad\text{and}\quad c'\le\theta_k\le C'\qquad\text{for all } k\ge0.

The lemma shows that the adaptive stepsizes, which approximate an inverse local Lipschitz constant of FF, do not degenerate along bounded runs; this is what turns the energy inequality (27) into convergence.

Formalization Note The paper's Lemma 2 carries no explicit hypothesis; it is stated under the standing assumptions of §2.1 ("for our purposes, the locally Lipschitz-continuity of FF is sufficient") and (C2). The Lipschitz hypothesis is the one-constant-per-bounded-subset-of-dom⁡g\operatorname{dom} g form used in the proof; it coincides with local Lipschitz continuity when dom⁡g\operatorname{dom} g is closed.

Preamble
import Mathlib
import Definitions.Def_GoldenRatioVI_Explicit_viProblem
import Definitions.Def_GoldenRatioVI_Explicit_egraalRun
Formal statement
namespace GoldenRatioVI.Explicit

/-- Lemma 2 of Malitsky (p. 6): if the sequence `(z^k)` generated by Algorithm 1 is bounded,
then both `(λ_k)` and `(θ_k)` are bounded and separated from `0`. Standing assumptions of §2.1:
`g` satisfies (C2) and `F` is Lipschitz on bounded subsets of `dom g`. -/
theorem steps_bounded_below {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] (g : E → EReal) (F : E → E) (ϕ lamBar : ℝ)
    (z zbar : ℕ → E) (lam theta : ℕ → ℝ)
    (hg : IsProperConvexLSC g) (hL : IsLipschitzOnBoundedDom g F)
    (hrun : IsEGRAALRun g F ϕ lamBar z zbar lam theta)
    (hz : Bornology.IsBounded (Set.range z)) :
    (∃ C : ℝ, ∀ k, lam k ≤ C) ∧ (∃ c : ℝ, 0 < c ∧ ∀ k, c ≤ lam k) ∧
    (∃ C : ℝ, ∀ k, theta k ≤ C) ∧ (∃ c : ℝ, 0 < c ∧ ∀ k, c ≤ theta k) := by sorry

end GoldenRatioVI.Explicit
Source
Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint (Optimization Online 6598, 2018), p. 6, Lemma 2
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