(9) and (10) imply (12) and stationarity of the cluster point

Proved

NonconvexSplitting.ProxADMM.stationary_of_eq9_eq10

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, and let $(x^{t_i}, y^{t_i}, z^{t_i}) \to (x^*, y^*, z^*)$ along a strictly increasing sequence $t_i$ . Suppose

\lim_{t\to\infty} \|y^{t+1} - y^t\|^2 + \|x^{t+1} - x^t\|^2 + \|z^{t+1} - z^t\|^2 = 0 \qquad (9)

and $\lim_{i\to\infty} P(y^{t_i+1}) = P(y^*)$ with $P(y^*)$ finite (10). Then

\nabla h(x^*) = \mathcal M^* z^*, \qquad -z^* \in \partial P(y^*), \qquad y^* = \mathcal M x^*, \qquad (12)

and $x^*$ is a stationary point of $\min_x h(x) + P(\mathcal M x)$ .

Assumption 1 is not needed for this step; it is used to establish (9) and (10).

Formalization Note The paper writes (10) as a limit of the real numbers $P(y^{t_i+1})$ equal to $P(y^*)$ ; the finiteness $P(y^*) < \infty$ is stated explicitly, because a limit $+\infty$ in EReal would not place $y^*$ in the domain of $P$ , where the limiting subdifferential is defined.

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
open NonconvexSplitting.Shared

open Filter Topology
open scoped InnerProductSpace

Formal statement

namespace NonconvexSplitting.ProxADMM

/-- Li–Pong, p. 6: if (9) holds and (10) holds along a convergent subsequence, then (12) holds and
`xs` is a stationary point of (1). Assumption 1 is not used. -/
theorem stationary_of_eq9_eq10 {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)
    (s : ℕ → ℕ) (hs : StrictMono s) (xs : EuclideanSpace ℝ (Fin n)) (ys zs : EuclideanSpace ℝ (Fin m))
    (hconv : Tendsto (fun i => (x (s i), y (s i), z (s i))) atTop (𝓝 (xs, ys, zs)))
    (h9 : Tendsto (fun t => ‖y (t + 1) - y t‖ ^ 2 + ‖x (t + 1) - x t‖ ^ 2 + ‖z (t + 1) - z t‖ ^ 2)
      atTop (𝓝 0))
    (h10 : Tendsto (fun i => P (y (s i + 1))) atTop (𝓝 (P ys))) (h10fin : P ys ≠ ⊤) :
    (gradient h xs = ContinuousLinearMap.adjoint M zs ∧ -zs ∈ LimitingSubdiff P ys ∧ ys = M xs) ∧
    IsStationary h P M xs := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, pp. 6–7, the claim before Theorem 1 with Eqs. (9), (10), (12)

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