Theorem 1 — cluster points of the proximal ADMM are stationary and improve on a non-stationary start

Proved

NonconvexSplitting.ProxADMM.theorem1

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

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

Let $h : \mathbb{R}^n \to \mathbb{R}$ be twice continuously differentiable with bounded Hessian, $P : \mathbb{R}^m \to (-\infty, +\infty]$ proper and lower semicontinuous, $\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ linear, $\phi : \mathbb{R}^n \to \mathbb{R}$ twice continuously differentiable and convex, and $\beta > 0$ . Suppose Assumption 1 holds with witnesses $\sigma, \mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \delta, \mathcal Q_3, \gamma$ , and let $(x^t, y^t, z^t)$ be any sequence generated by the proximal ADMM

y^{t+1} \in \operatorname{Arg\,min}_y L_\beta(x^t, y, z^t),\quad x^{t+1} \in \operatorname{Arg\,min}_x \{L_\beta(x, y^{t+1}, z^t) + D_\phi(x, x^t)\},\quad z^{t+1} = z^t - \beta(\mathcal M x^{t+1} - y^{t+1}).

(Global subsequential convergence) If $(x^*, y^*, z^*)$ is a cluster point of $\{(x^t, y^t, z^t)\}$ , then

\lim_{t\to\infty}\|y^{t+1} - y^t\|^2 + \|x^{t+1} - x^t\|^2 + \|z^{t+1} - z^t\|^2 = 0,

$\nabla h(x^*) = \mathcal M^* z^*$ , $-z^* \in \partial P(y^*)$ , $y^* = \mathcal M x^*$ , and $x^*$ is a stationary point of $\min_x h(x) + P(\mathcal M x)$ . 2. (Strict improvement in objective values) If $x^0$ is not stationary, $h(x^0) + P(\mathcal M x^0) < \infty$ and $\mathcal M^* z^0 = \nabla h(x^0)$ , then every cluster point $(x^*, y^*, z^*)$ satisfies

h(x^*) + P(\mathcal M x^*) < h(x^0) + P(\mathcal M x^0).

The theorem makes no claim that a cluster point exists; boundedness of the sequence is the subject of Theorem 2.

Formalization Note A cluster point is the limit of $(x^{t_i}, y^{t_i}, z^{t_i})$ along some strictly increasing $t_i$ . Objective values are compared in EReal. Both parts are one statement, a conjunction.

Preamble

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

open Filter Topology
open scoped InnerProductSpace

Formal statement

namespace NonconvexSplitting.ProxADMM

/-- Theorem 1 of Li–Pong (p. 7): (i) global subsequential convergence of the proximal ADMM and
(ii) strict improvement of the objective from a non-stationary start. -/
theorem theorem1 {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 β)
    (σ δ γ : ℝ) (Q1 Q2 T1 T2 Q3 : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hA : Assumption1 h phi M β σ Q1 Q2 T1 T2 δ Q3 γ)
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (y z : ℕ → EuclideanSpace ℝ (Fin m))
    (hseq : IsProxADMMSeq h P phi M β x y z) :
    -- (i) global subsequential convergence
    (∀ (s : ℕ → ℕ) (xs : EuclideanSpace ℝ (Fin n)) (ys zs : EuclideanSpace ℝ (Fin m)), StrictMono s →
      Tendsto (fun i => (x (s i), y (s i), z (s i))) atTop (𝓝 (xs, ys, zs)) →
      Tendsto (fun t => ‖y (t + 1) - y t‖ ^ 2 + ‖x (t + 1) - x t‖ ^ 2 + ‖z (t + 1) - z t‖ ^ 2)
      atTop (𝓝 0) ∧
      (gradient h xs = ContinuousLinearMap.adjoint M zs ∧ -zs ∈ LimitingSubdiff P ys ∧ ys = M xs) ∧
      IsStationary h P M xs) ∧
    -- (ii) strict improvement in objective values
    (ContinuousLinearMap.adjoint M (z 0) = gradient h (x 0) →
      ¬ IsStationary h P M (x 0) →
      ((h (x 0) : ℝ) : EReal) + P (M (x 0)) ≠ ⊤ →
      ∀ (s : ℕ → ℕ) (xs : EuclideanSpace ℝ (Fin n)) (ys zs : EuclideanSpace ℝ (Fin m)), StrictMono s →
        Tendsto (fun i => (x (s i), y (s i), z (s i))) atTop (𝓝 (xs, ys, zs)) →
        ((h xs : ℝ) : EReal) + P (M xs) < ((h (x 0) : ℝ) : EReal) + P (M (x 0))) := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 7, Theorem 1

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