Theorem 2: the proximal ADMM sequence is bounded under coercivity

Proved

NonconvexSplitting.ADMMBounded.theorem2

by mikedeng1 · Sep 29, 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, $\phi : \mathbb{R}^n \to \mathbb{R}$ twice continuously differentiable and convex, $\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ linear with adjoint $\mathcal M^*$ , and $\beta > 0$ . Let $(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 $x^0, z^0$ arbitrary, $y^0$ unconstrained). Suppose Assumption 1 holds with witnesses $\sigma, \delta, \gamma$ and $\mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \mathcal Q_3$ . For a self-map $\mathcal T$ write $\|x\|^2_{\mathcal T} := \langle x, \mathcal T x\rangle$ . Suppose moreover that condition (29) holds with the same $\sigma$ and $\gamma$ : there are $\zeta$ with $0 < \zeta < 2\beta\gamma$ and $h_0 \in \mathbb{R}$ such that

h(x) - \frac{1}{\sigma\zeta}\|\nabla h(x)\|^2 \ge h_0 \qquad \text{for all } x .

Suppose that either

$\mathcal M$ is invertible and $\liminf_{\|y\| \to \infty} P(y) = \infty$ ; or
$\liminf_{\|x\| \to \infty} h(x) = \infty$ and $\inf_y P(y) > -\infty$ .

Then the sequence $\{(x^t, y^t, z^t)\}$ is bounded: there is $R$ with

\|x^t\| \le R, \quad \|y^t\| \le R, \quad \|z^t\| \le R \qquad \text{for all } t \ge 0 .

Boundedness guarantees that the sequence has a cluster point, which is the hypothesis under which the convergence results for the proximal ADMM (stationarity of cluster points, and whole-sequence convergence under the Kurdyka–Łojasiewicz property) apply.

Formalization Note The paper defines $h_0$ as the infimum $\inf_x\{h(x) - \frac{1}{\sigma\zeta}\|\nabla h(x)\|^2\}$ and requires it to be $> -\infty$ ; here $h_0$ is any real lower bound. The infimum is finite exactly when a real lower bound exists, and the proof uses $h_0$ only as a lower bound, so the two readings give the same result. "Invertible" is bijectivity of $\mathcal M$ as a map $\mathbb{R}^n \to \mathbb{R}^m$ (the dimensions are kept separate). $\liminf_{\|y\|\to\infty} P(y) = \infty$ is encoded as: for every $r \in \mathbb{R}$ there is $R$ with $P(y) > r$ whenever $\|y\| > R$ ; likewise for $h$ . $\inf_y P(y) > -\infty$ is: some real $c$ satisfies $c \le P(y)$ for all $y$ . The two cases are one disjunctive hypothesis of a single statement. The bound covers all three blocks and all $t \ge 0$ ; $y^0$ is a single (arbitrary) point and does not affect boundedness.

Preamble

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

/-- Theorem 2 of Li–Pong (p. 11): boundedness of the proximal ADMM sequence.
Under the standing assumptions, Assumption 1 and condition (29) (with the same `σ`, `γ`),
if either (i) `M` is invertible and `P` is coercive, or (ii) `h` is coercive and `P` is
bounded below, then every proximal ADMM sequence `(x^t, y^t, z^t)` is bounded. -/
theorem theorem2 {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 γ)
    (ζ h₀ : ℝ) (hζ : 0 < ζ ∧ ζ < 2 * β * γ)
    (h29 : ∀ x, h₀ ≤ h x - 1 / (σ * ζ) * ‖gradient h x‖ ^ 2)
    (hcase :
      (Function.Bijective M ∧
          ∀ r : ℝ, ∃ R : ℝ, ∀ w : EuclideanSpace ℝ (Fin m), R < ‖w‖ → (r : EReal) < P w) ∨
        ((∀ r : ℝ, ∃ R : ℝ, ∀ v : EuclideanSpace ℝ (Fin n), R < ‖v‖ → r < h v) ∧
          ∃ c : ℝ, ∀ w : EuclideanSpace ℝ (Fin m), (c : EReal) ≤ P w))
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (y z : ℕ → EuclideanSpace ℝ (Fin m))
    (hseq : IsProxADMMSeq h P phi M β x y z) :
    ∃ R : ℝ, ∀ t : ℕ, ‖x t‖ ≤ R ∧ ‖y t‖ ≤ R ∧ ‖z t‖ ≤ R := by sorry

end NonconvexSplitting.ADMMBounded

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 11, Theorem 2 (with condition (29))

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