Prove2Me

Eq. (4) — prox-inequality characterising xˉ=proxg(w)\bar x = \mathrm{prox}_g(w)

Proved
GoldenRatioVI.Explicit.prox_inequality

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

convex-analysisp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-operator

Let E\mathcal E be a finite-dimensional real inner product space and let g:E→(−∞,+∞]g:\mathcal E\to(-\infty,+\infty] be proper, convex and lower semicontinuous. For w,xˉ∈Ew,\bar x\in\mathcal E,

xˉ=prox⁡g(w)  ⟺  ⟨xˉ−w,x−xˉ⟩≥g(xˉ)−g(x)∀x∈E.(4)\bar x = \operatorname{prox}_g(w) \iff \langle \bar x - w, x-\bar x\rangle \ge g(\bar x) - g(x)\quad \forall x\in\mathcal E. \tag{4}

This characteristic property of the proximal operator is used in every convergence proof of the paper; applied to λkg\lambda_k g it yields the inequalities (19)–(20) behind the energy estimate (27).

Formalization Note The right-hand side is written without extended-real subtraction as g(xˉ)≤⟨xˉ−w,x−xˉ⟩+g(x)g(\bar x)\le\langle\bar x-w,x-\bar x\rangle+g(x); it forces xˉ∈dom⁡g\bar x\in\operatorname{dom} g (take x∈dom⁡gx\in\operatorname{dom} g), as the left-hand side does.

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

/-- Eq. (4) of Malitsky (p. 3), the prox-inequality: for a proper convex lsc
`g : E → (−∞, +∞]`, `xbar = prox_g(w)` iff `⟨xbar − w, x − xbar⟩ ≥ g(xbar) − g(x)` for all `x`,
written without `EReal` subtraction as `g(xbar) ≤ ⟨xbar − w, x − xbar⟩ + g(x)`. -/
theorem prox_inequality {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] (g : E → EReal) (hg : IsProperConvexLSC g) (w xbar : E) :
    GoldenRatioVI.Shared.IsProxPoint g w xbar ↔
      ∀ x : E, g xbar ≤ ((inner ℝ (xbar - w) (x - xbar) : ℝ) : EReal) + g x := by sorry

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