Eq. (32): lower estimate of the merit value at $t = 1$

Proved

NonconvexSplitting.ADMMBounded.eq32_lower_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$ . 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 .

Let $\mu \in (0, 1)$ satisfy $(1-\mu)\beta > \zeta/(2\gamma)$ , and set $c := \frac{1-\mu}{\zeta} - \frac{1}{2\beta\gamma}$ (so $c > 0$ ).

Then for every $t \ge 1$ ,

L_\beta(x^1, y^1, z^1) + \frac12\|x^1 - x^0\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2} \ge \mu h(x^t) + (1-\mu)h_0 + \frac{c}{\sigma}\|\nabla h(x^t)\|^2 + P(y^t) + \frac{\beta}{2}\Bigl\|\mathcal M x^t - y^t - \frac{z^t}{\beta}\Bigr\|^2 + \frac12\|x^t - x^{t-1}\|^2_{\frac{1}{\sigma\beta(1-\gamma)}\mathcal T_1^2}.

Every term on the right is controlled by the constant on the left; under either set of coercivity hypotheses of Theorem 2 this yields bounds on the iterates.

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. 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. The quantity $z^t/\beta$ is written $(1/\beta)\,z^t$ .

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. (32) of Li–Pong (p. 12): under Assumption 1 and condition (29) (with `h₀` any lower
bound of `h(x) - (1/(σζ))‖∇h(x)‖²`), for `μ ∈ (0,1)` with `(1-μ)β > ζ/(2γ)` and
`c = (1-μ)/ζ - 1/(2βγ)`, for every `t ≥ 1` the value at `t = 1` of the merit sequence of (30)
dominates
`μ h(x^t) + (1-μ) h₀ + (c/σ)‖∇h(x^t)‖² + P(y^t) + (β/2)‖M x^t - y^t - z^t/β‖²
  + ½‖x^t - x^{t-1}‖²_{(1/(σβ(1-γ)))T₁²}`, written additively in `EReal`. -/
theorem eq32_lower_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 γ)
    (ζ h₀ : ℝ) (hζ : 0 < ζ ∧ ζ < 2 * β * γ)
    (h29 : ∀ x, h₀ ≤ h x - 1 / (σ * ζ) * ‖gradient h x‖ ^ 2)
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (y z : ℕ → EuclideanSpace ℝ (Fin m))
    (hseq : IsProxADMMSeq h P phi M β x y z)
    (μ : ℝ) (hμ : 0 < μ ∧ μ < 1) (hμβ : ζ / (2 * γ) < (1 - μ) * β)
    (t : ℕ) (ht : 1 ≤ t) :
    ((μ * h (x t) + (1 - μ) * h₀ +
          ((1 - μ) / ζ - 1 / (2 * β * γ)) / σ * ‖gradient h (x t)‖ ^ 2 : ℝ) : EReal) +
        P (y t) +
        ((β / 2 * ‖M (x t) - y t - (1 / β) • z t‖ ^ 2 +
          1 / 2 * wnormSq ((1 / (σ * β * (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. 12, Eq. (32) and the sentence after it (definition of c and μ)

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. (32): lower estimate of the merit value at t=1t = 1t=1

Eq. (32): lower estimate of the merit value at $t = 1$