Eq. (30): the merit sequence stays below its value at $t = 1$

Proved

NonconvexSplitting.ADMMBounded.eq30_merit_bound

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$ .

Then for every $t \ge 1$ ,

L_\beta(x^t, y^t, z^t) + \frac12\|x^t - x^{t-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2} \le L_\beta(x^1, y^1, z^1) + \frac12\|x^1 - x^0\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}.

The quantity on the left is non-increasing in $t$ ; this bound gives a uniform upper estimate along the whole sequence, from which the boundedness of the iterates is extracted.

Formalization Note The augmented Lagrangian $L_\beta$ takes values in $(-\infty, +\infty]$ , so the inequality is stated in EReal in additive form (the real terms moved to the side where they are added), which avoids extended-real subtraction.

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

/-- Eq. (30) of Li–Pong (p. 11): for every `t ≥ 1`,
`L_β(x^t, y^t, z^t) + ½‖x^t - x^{t-1}‖²_{(2/(σβ(1-γ)))T₁²}` is at most its value at `t = 1`,
written additively in `EReal`. -/
theorem eq30_merit_bound {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)
    (t : ℕ) (ht : 1 ≤ t) :
    augLag h P M β (x t) (y t) (z t) +
        ((1 / 2 * wnormSq ((2 / (σ * β * (1 - γ))) • (T1 * T1)) (x t - x (t - 1)) : ℝ) : EReal) ≤
      augLag h P M β (x 1) (y 1) (z 1) +
        ((1 / 2 * wnormSq ((2 / (σ * β * (1 - γ))) • (T1 * T1)) (x 1 - x 0) : ℝ) : EReal) := by sorry

end NonconvexSplitting.ADMMBounded

Source

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

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

Eq. (30): the merit sequence stays below its value at t=1t = 1t=1

Eq. (30): the merit sequence stays below its value at $t = 1$