Eq. (18) — the two key estimations produced by the step rule (15)

Proved

GoldenRatioVI.Explicit.step_estimates

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

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

Consider a run of Algorithm 1 (EGRAAL) with parameter $\phi\in(1,\varphi]$ , stepsizes $(\lambda_k)$ , ratios $(\theta_k)$ and iterates $(z^k)$ . For every $k\ge 1$ :

$\lambda_k\le\lambda_{k-1}\big(\frac1\phi+\frac1{\phi^2}\big)$ ;
$\theta_k\le 1+\frac1\phi$ ;

\lambda_k^2\,\|F(z^k)-F(z^{k-1})\|^2 \le \frac{\theta_k\theta_{k-1}}{4}\,\|z^k-z^{k-1}\|^2. \tag{18}

No assumption on $g$ or $F$ is needed: these are consequences of the step rule (15) and the update of $\theta_k$ alone. They replace the global Lipschitz constant in the convergence analysis.

Preamble

import Mathlib
import Definitions.Def_GoldenRatioVI_Explicit_egraalRun

Formal statement

namespace GoldenRatioVI.Explicit

/-- Eq. (18) of Malitsky (p. 5), the two key estimations produced by the step rule (15):
for every `k ≥ 1`, `λ_k ≤ λ_{k−1}(1/ϕ + 1/ϕ²)`, hence `θ_k ≤ 1 + 1/ϕ`, and
`λ_k² ‖F(z^k) − F(z^{k−1})‖² ≤ (θ_k θ_{k−1} / 4) ‖z^k − z^{k−1}‖²`. -/
theorem step_estimates {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] (g : E → EReal) (F : E → E) (ϕ lamBar : ℝ)
    (z zbar : ℕ → E) (lam theta : ℕ → ℝ)
    (hrun : IsEGRAALRun g F ϕ lamBar z zbar lam theta) (k : ℕ) (hk : 1 ≤ k) :
    lam k ≤ lam (k - 1) * (1 / ϕ + 1 / ϕ ^ 2) ∧
    theta k ≤ 1 + 1 / ϕ ∧
    lam k ^ 2 * ‖F (z k) - F (z (k - 1))‖ ^ 2 ≤
      theta k * theta (k - 1) / 4 * ‖z k - z (k - 1)‖ ^ 2 := by sorry

end GoldenRatioVI.Explicit

Source

Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint (Optimization Online 6598, 2018), p. 5, Eq. (18) and the preceding sentence

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