Prove2Me

Eq. (31): σ∥zt∥2\sigma\|z^t\|^2 bounded by the gradient and the last primal step

Proved
NonconvexSplitting.ADMMBounded.eq31_dual_bound

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

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

Let h:Rn→Rh : \mathbb{R}^n \to \mathbb{R} be twice continuously differentiable with bounded Hessian, P:Rm→(−∞,+∞]P : \mathbb{R}^m \to (-\infty, +\infty] proper and lower semicontinuous, ϕ:Rn→R\phi : \mathbb{R}^n \to \mathbb{R} twice continuously differentiable and convex, M:Rn→Rm\mathcal M : \mathbb{R}^n \to \mathbb{R}^m linear with adjoint M∗\mathcal M^*, and β>0\beta > 0. Let (xt,yt,zt)t≥0(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 x0,z0x^0, z^0 arbitrary, y0y^0 unconstrained). Suppose Assumption 1 holds with witnesses σ,δ,γ\sigma, \delta, \gamma and Q1,Q2,T1,T2,Q3\mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \mathcal Q_3. For a self-map T\mathcal T write ∥x∥T2:=⟨x,Tx⟩\|x\|^2_{\mathcal T} := \langle x, \mathcal T x\rangle.

Then for every t≥1t \ge 1,

σ∥zt∥2≤1γ∥∇h(xt)∥2+11−γ∥xt−xt−1∥T122.\sigma\|z^t\|^2 \le \frac{1}{\gamma}\|\nabla h(x^t)\|^2 + \frac{1}{1-\gamma}\|x^t - x^{t-1}\|^2_{\mathcal T_1^2}.

It bounds the dual iterates by primal quantities, so that bounds on ∇h(xt)\nabla h(x^t) and on the primal steps transfer to ztz^t.

Formalization Note T12\mathcal T_1^2 is the composition T1∘T1\mathcal T_1 \circ \mathcal T_1, and ∥x∥T122=⟨x,T12x⟩\|x\|^2_{\mathcal T_1^2} = \langle x, \mathcal T_1^2 x\rangle.

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. (31) of Li–Pong (p. 12): for every `t ≥ 1`,
`σ‖z^t‖² ≤ (1/γ)‖∇h(x^t)‖² + (1/(1-γ))‖x^t - x^{t-1}‖²_{T₁²}`. -/
theorem eq31_dual_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) :
    σ * ‖z t‖ ^ 2 ≤
      (1 / γ) * ‖gradient h (x t)‖ ^ 2 +
        (1 / (1 - γ)) * wnormSq (T1 * T1) (x t - x (t - 1)) := by sorry

end NonconvexSplitting.ADMMBounded
Source
Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 12, Eq. (31)
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