Prove2Me

(3.32)–(3.33) — three-point inequalities for the stochastic prox subproblems (3.26) and (3.27)

Proved
NonconvexAG.StochComposite.eq_3_32_3_33

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

accelerated-gradientcomposite-optimizationp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let X\mathcal X be convex with domain KK and prox map P\mathcal P, and run Algorithm 4 along any realization of the oracle samples, with δˉk=Gˉk−∇Ψ(xkmd)\bar\delta_k=\bar G_k-\nabla\Psi(x^{md}_k) (so ∇Ψ(xkmd)+δˉk=Gˉk\nabla\Psi(x^{md}_k)+\bar\delta_k=\bar G_k). Then for every k≥1k\ge1 and every x∈Kx\in K,

⟨∇Ψ(xkmd)+δˉk,xk−x⟩+X(xk)≤X(x)+12λk[∥xk−1−x∥2−∥xk−x∥2−∥xk−xk−1∥2],\langle\nabla\Psi(x^{md}_k)+\bar\delta_k,x_k-x\rangle+\mathcal X(x_k)\le\mathcal X(x)+\frac1{2\lambda_k}\Big[\|x_{k-1}-x\|^2-\|x_k-x\|^2-\|x_k-x_{k-1}\|^2\Big], ⟨∇Ψ(xkmd)+δˉk,xkag−x⟩+X(xkag)≤X(x)+12βk[∥xkmd−x∥2−∥xkag−x∥2−∥xkag−xkmd∥2].\langle\nabla\Psi(x^{md}_k)+\bar\delta_k,x^{ag}_k-x\rangle+\mathcal X(x^{ag}_k)\le\mathcal X(x)+\frac1{2\beta_k}\Big[\|x^{md}_k-x\|^2-\|x^{ag}_k-x\|^2-\|x^{ag}_k-x^{md}_k\|^2\Big].

These are the optimality conditions of the two prox steps (3.26) and (3.27) in three-point form (Lemma 2 of Ghadimi–Lan–Zhang [11]).

Formalization Note The paper says "for any x∈Rnx\in\mathbb R^n"; for x∉Kx\notin K the right-hand side is +∞+\infty and the inequality is trivial, so it is stated for x∈Kx\in K. The statements are pathwise (for every sample point ω\omega); the gradient map ∇Ψ\nabla\Psi enters only through δˉk\bar\delta_k and can be arbitrary.

Preamble
import Mathlib
import Definitions.Def_ConvexOptAlg_SmoothGD_Defs
import Definitions.Def_GhadimiLan_RSG_Model
import Definitions.Def_NonconvexAG_StochComposite_ProxMap
import Definitions.Def_NonconvexAG_StochComposite_RSAG
open MeasureTheory ProbabilityTheory
open scoped InnerProductSpace
Formal statement
namespace NonconvexAG.StochComposite

open GhadimiLan.RSG (E)
open ConvexOptAlg.SmoothGD

/-- (3.32) and (3.33), p. 22: the three-point inequalities for the prox subproblems (3.26) and
(3.27) of Algorithm 4, with `δ̄ₖ = Ḡₖ − ∇Ψ(x^md_k)` (so `∇Ψ(x^md_k) + δ̄ₖ = Ḡₖ`), for every
realization `ω`, every `k ≥ 1` and every `x` in the domain `K` of `𝒳`. -/
theorem eq_3_32_3_33 {n : ℕ} (gΨ : E n → E n) (K : Set (E n)) (X : E n → ℝ)
    (hX : ConvexOn ℝ K X) (P : E n → E n → ℝ → E n) (hP : IsProxMap K X P)
    {Ξ : Type*} (G : E n → Ξ → E n)
    (α β lam : ℕ → ℝ) (m : ℕ → ℕ) (hstep : RSAGStepsizes α β lam m) (x0 : E n)
    {Ω : Type*} (ξ : ℕ → Ω → Ξ) :
    let xk : ℕ → Ω → E n := xSeq G P α β lam m x0 ξ
    let xag : ℕ → Ω → E n := xagSeq G P α β lam m x0 ξ
    let xmd : ℕ → Ω → E n := xmdSeq G P α β lam m x0 ξ
    let δ : ℕ → Ω → E n := deltaBar G gΨ P α β lam m x0 ξ
    ∀ ω : Ω, ∀ k, 1 ≤ k → ∀ x ∈ K,
      inner ℝ (gΨ (xmd k ω) + δ k ω) (xk k ω - x) + X (xk k ω) ≤
          X x + 1 / (2 * lam k) *
            (‖xk (k - 1) ω - x‖ ^ 2 - ‖xk k ω - x‖ ^ 2 - ‖xk k ω - xk (k - 1) ω‖ ^ 2) ∧
        inner ℝ (gΨ (xmd k ω) + δ k ω) (xag k ω - x) + X (xag k ω) ≤
          X x + 1 / (2 * β k) *
            (‖xmd k ω - x‖ ^ 2 - ‖xag k ω - x‖ ^ 2 - ‖xag k ω - xmd k ω‖ ^ 2) := by sorry

end NonconvexAG.StochComposite
Source
Ghadimi & Lan, Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming, arXiv:1310.3787v1, p. 22, (3.32) and (3.33)
Human review

  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 9, 2026

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

View graph