Prove2Me

Eq. (45): descent inequality for h+qh + q under (44)

Proved
NonconvexSplitting.ProxGrad.eq45_descent_lemma

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

nonconvex-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let h,q:Rn→Rh, q : \mathbb{R}^n \to \mathbb{R} be twice continuously differentiable and ℓ>0\ell > 0, and suppose condition (44) holds: −ℓI⪯∇2h(x)+∇2q(x)⪯ℓI-\ell I \preceq \nabla^2 h(x) + \nabla^2 q(x) \preceq \ell I for all xx. Then for all u,v∈Rnu, v \in \mathbb{R}^n,

(h+q)(v)≤(h+q)(u)+⟨∇h(u)+∇q(u), v−u⟩+ℓ2∥v−u∥2.(h + q)(v) \le (h + q)(u) + \langle \nabla h(u) + \nabla q(u),\, v - u\rangle + \frac{\ell}{2}\|v - u\|^2 .

In the paper this is applied at (u,v)=(xt,xt+1)(u, v) = (x^t, x^{t+1}); it is the first step of the sufficient-decrease estimate (46).

Formalization Note Stated for all pairs (u,v)(u, v), the form the paper's justification ("∇(h+q)\nabla(h+q) is Lipschitz continuous with modulus at most ℓ\ell") yields; convexity of qq is not needed here.

Preamble
import Mathlib
import Definitions.Def_NonconvexSplitting_ProxGrad_HessianSandwich

open scoped InnerProductSpace
Formal statement
namespace NonconvexSplitting.ProxGrad

/-- Eq. (45) of Li–Pong (p. 18), in its two-point form: under (44), `∇(h + q)` is
`ℓ`-Lipschitz, so `(h+q)(v) ≤ (h+q)(u) + ⟪∇h(u) + ∇q(u), v - u⟫ + (ℓ/2)‖v - u‖²`. -/
theorem eq45_descent_lemma {n : ℕ} (h q : EuclideanSpace ℝ (Fin n) → ℝ) (ℓ : ℝ)
    (hh : ContDiff ℝ 2 h) (hq : ContDiff ℝ 2 q) (hℓ : 0 < ℓ) (h44 : HessianSandwich h q ℓ)
    (u v : EuclideanSpace ℝ (Fin n)) :
    h v + q v ≤ h u + q u + ⟪gradient h u + gradient q u, v - u⟫_ℝ + ℓ / 2 * ‖v - u‖ ^ 2 := by sorry

end NonconvexSplitting.ProxGrad
Source
Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 18, Eq. (45)
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