Optimality relations (11) of the proximal ADMM iterates

Proved

NonconvexSplitting.ProxADMM.eq11_optimality

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

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

Assume $h$ is $C^2$ with bounded Hessian, $P$ is proper and lower semicontinuous, $\phi$ is $C^2$ and convex, and $\beta > 0$ . Let $(x^t, y^t, z^t)$ be generated by the proximal ADMM. Then for every $t \ge 0$

\begin{cases} -z^{t+1} - \beta\mathcal M(x^{t+1} - x^t) \in \partial P(y^{t+1}),\\ \nabla h(x^{t+1}) - \mathcal M^* z^{t+1} = -\nabla\phi(x^{t+1}) + \nabla\phi(x^t),\\ \mathcal M x^{t+1} - y^{t+1} = \frac{1}{\beta}(z^t - z^{t+1}), \end{cases}

where $\partial P$ is the limiting subdifferential.

These relations rewrite the first-order optimality conditions of the two subproblems in terms of the updated multiplier; Assumption 1 is not needed.

Preamble

import Mathlib
import Definitions.Def_NonconvexSplitting_Shared_LimitingSubdiff
import Definitions.Def_NonconvexSplitting_Shared_StandingAssumptions
import Definitions.Def_NonconvexSplitting_Shared_IsProxADMMSeq
open NonconvexSplitting.Shared

open Filter Topology
open scoped InnerProductSpace

Formal statement

namespace NonconvexSplitting.ProxADMM

/-- Eq. (11) of Li–Pong (p. 6): the relations satisfied by every proximal ADMM iterate. -/
theorem eq11_optimality {n m : ℕ} (h : EuclideanSpace ℝ (Fin n) → ℝ) (P : EuclideanSpace ℝ (Fin m) → EReal)
    (phi : EuclideanSpace ℝ (Fin n) → ℝ) (M : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)) (β : ℝ)
    (hstd : StandingAssumptions h P phi β)
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (y z : ℕ → EuclideanSpace ℝ (Fin m))
    (hseq : IsProxADMMSeq h P phi M β x y z) (t : ℕ) :
    -(z (t + 1)) - β • M (x (t + 1) - x t) ∈ LimitingSubdiff P (y (t + 1)) ∧
    gradient h (x (t + 1)) - ContinuousLinearMap.adjoint M (z (t + 1)) =
      -(gradient phi (x (t + 1))) + gradient phi (x t) ∧
    M (x (t + 1)) - y (t + 1) = (1 / β) • (z t - z (t + 1)) := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 6, Eq. (11) (derived from (8))

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