Prove2Me

Stepsize rule (15): λk≤ρλk−1\lambda_k\le\rho\lambda_{k-1} and θk≤1+1/φ\theta_k\le1+1/\varphi

Proved
GoldenRatioVI.step_le_rho_and_theta_le

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

convex-optimizationmonotone-operatorsproximal-methodsvariational-inequalities

Let φ∈(1,ϕ]\varphi\in(1,\phi], λ0>0\lambda_0>0, λˉ>0\bar\lambda>0, and let (zk),(zˉk),(λk),(θk)(z^k),(\bar z^k),(\lambda_k),(\theta_k) be generated by Algorithm 1 (EGRAAL) from any z0,z1∈Ez^0,z^1\in\mathcal E, for some gg with domain DD and some FF. Then for every k≥1k\ge1,

λk≤λk−1(1φ+1φ2)andθk−1−1φ≤0.\lambda_k\le\lambda_{k-1}\Big(\frac1\varphi+\frac1{\varphi^2}\Big)\qquad\text{and}\qquad \theta_k-1-\frac1\varphi\le0 .

The bound θk≤1+1/φ\theta_k\le1+1/\varphi is what makes the coefficient of ∥zk+1−zˉk∥2\|z^{k+1}-\bar z^k\|^2 in (25) nonpositive.

Differences from the source:

  • generalization: the standing assumptions of §2.1: (C1)–(C3) and F locally Lipschitz → only the run and φ ∈ (1, ϕ], λ₀ > 0, λ̄ > 0; no (C1)–(C3) or Lipschitz assumption; reason: the estimate is a consequence of the rule (15) alone; the paper's setting is a special case
  • encoding: g : E → (−∞, +∞] proper convex lsc → a set D with real values g : E → ℝ; D nonempty, ConvexOn ℝ D g, and the extension by +∞ off D lower semicontinuous (IsProperConvexLsc); reason: every proper convex lsc g is of this form (D = dom g) and conversely; same instances
  • generalization: F : dom g → E; inputs z⁰, z¹ at which F is evaluated in (15), (17) → F : E → E, with monotonicity (and local Lipschitz continuity, where assumed) imposed on D only and values off D unconstrained; z 0, z 1 ∈ E arbitrary; reason: specializes to the paper by taking z⁰, z¹ ∈ dom g and any extension of F off dom g; for k ≥ 2 the iterates lie in dom g
  • encoding: convention 0/0 = +∞ in (15) → egraalStep omits the middle entry of the minimum when F(z^k) = F(z^{k−1}); reason: the middle entry is then a/0 with a ≥ 0, i.e. +∞, and drops out of the minimum; same stepsizes
  • encoding: z^{k+1} = prox_{λ_k g}(z̄^k − λ_k F(z^k)) with prox a function → IsProx D (λ_k g) (z̄^k − λ_k F(z^k)) (z^{k+1}): z^{k+1} ∈ D minimizes λ_k g(x) + ½‖x − w‖² over D; reason: under (C2) in finite dimension the minimizer exists and is unique, so the predicate determines the same iterates
  • reading: index k unspecified (the algorithm runs for k ≥ 1) → every k ≥ 1; reason: every term is defined for k ≥ 1 (λ_{k−1}, θ_{k−1}, z^{k−1}); the paper uses the estimate for k ≥ 1
Preamble
import Mathlib
import Definitions.Def_GoldenRatioVI_IsEGRAALRun
Formal statement
namespace GoldenRatioVI

/-- **First consequence of the stepsize rule (15): `λ_k ≤ ρλ_{k−1}` and `θ_k ≤ 1 + 1/φ`.**
Malitsky, *Golden Ratio Algorithms for Variational Inequalities*, preprint (2018), §2.1, p. 5 (unnumbered): "Condition (15) leads to two key estimations. First, one has
λk ≤ λk−1(1/φ + 1/φ²), which in turn implies θk − 1 − 1/φ ≤ 0."

For a run of Algorithm 1 with `1 < phi ≤ ϕ`, `lam0 > 0`, `lbar > 0`, and every `k ≥ 1`:
`lam k ≤ lam (k−1) (1/φ + 1/φ²)` and `theta k − 1 − 1/φ ≤ 0`.

**Formalization Note.** `ϕ` is Mathlib's `Real.goldenRatio`; the parameter `φ` is `phi`. -/
theorem step_le_rho_and_theta_le {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] {D : Set E} {g : E → ℝ} {F : E → E} {phi lam0 lbar : ℝ}
    {z zbar : ℕ → E} {lam theta : ℕ → ℝ}
    (hphi : 1 < phi) (hphiG : phi ≤ Real.goldenRatio) (hlam0 : 0 < lam0) (hlbar : 0 < lbar)
    (hrun : IsEGRAALRun D g F phi lam0 lbar z zbar lam theta) (k : ℕ) (hk : 1 ≤ k) :
    lam k ≤ lam (k - 1) * (1 / phi + 1 / phi ^ 2) ∧ theta k - 1 - 1 / phi ≤ 0 := by sorry

end GoldenRatioVI
Source
Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint (2018), §2.1, p. 5 (unnumbered, after Algorithm 1)

View graph