Prove2Me

Eq. (13): M∗zt+1=∇h(xt+1)+∇ϕ(xt+1)−∇ϕ(xt)\mathcal M^* z^{t+1} = \nabla h(x^{t+1}) + \nabla\phi(x^{t+1}) - \nabla\phi(x^t)

Proved
NonconvexSplitting.ADMMBounded.eq13_dual_identity

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

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

Let h:Rn→Rh : \mathbb{R}^n \to \mathbb{R} be twice continuously differentiable with bounded Hessian, P:Rm→(−∞,+∞]P : \mathbb{R}^m \to (-\infty, +\infty] proper and lower semicontinuous, ϕ:Rn→R\phi : \mathbb{R}^n \to \mathbb{R} twice continuously differentiable and convex, M:Rn→Rm\mathcal M : \mathbb{R}^n \to \mathbb{R}^m linear with adjoint M∗\mathcal M^*, and β>0\beta > 0. Let (xt,yt,zt)t≥0(x^t, y^t, z^t)_{t \ge 0} be a sequence generated by the proximal ADMM with penalty β\beta and proximal function ϕ\phi (initial points x0,z0x^0, z^0 arbitrary, y0y^0 unconstrained).

Then for every t≥0t \ge 0,

M∗zt+1=∇h(xt+1)+∇ϕ(xt+1)−∇ϕ(xt).\mathcal M^* z^{t+1} = \nabla h(x^{t+1}) + \nabla\phi(x^{t+1}) - \nabla\phi(x^t).

This identity expresses the dual iterate through the primal iterates. It is the starting point of the estimates on the dual variable used in the boundedness proof, in particular Eq. (31).

Formalization Note Assumption 1 is not assumed. The adjoint M∗\mathcal M^* is Mathlib's ContinuousLinearMap.adjoint, and ∇\nabla is gradient.

Preamble
import Mathlib
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.ADMMBounded

/-- Eq. (13) of Li–Pong (p. 8): along the proximal ADMM, for every `t`,
`M* z^{t+1} = ∇h(x^{t+1}) + ∇φ(x^{t+1}) - ∇φ(x^t)`. -/
theorem eq13_dual_identity {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 : ℕ) :
    ContinuousLinearMap.adjoint M (z (t + 1)) =
      gradient h (x (t + 1)) + gradient phi (x (t + 1)) - gradient phi (x t) := by sorry

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