Eq. (14) — dual steps bounded by primal steps

Proved

NonconvexSplitting.ProxADMM.eq14_dual_step_bound

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

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

Assume the standing assumptions ( $h$ $C^2$ with bounded Hessian, $P$ proper and lower semicontinuous, $\phi$ $C^2$ and convex, $\beta > 0$ ) and Assumption 1 with witnesses $\sigma, \mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \delta, \mathcal Q_3, \gamma$ . Let $(x^t, y^t, z^t)$ be generated by the proximal ADMM. Then for every $t \ge 1$

\sigma\|z^{t+1} - z^t\|^2 \le \frac{1}{\gamma}\|x^{t+1} - x^t\|^2_{\mathcal Q_3} + \frac{1}{1-\gamma}\|x^t - x^{t-1}\|^2_{\mathcal T_1^2},

where $\|x\|^2_{\mathcal T} = \langle x, \mathcal T x\rangle$ .

It is the step that controls the multiplier updates by the primal updates.

Formalization Note Iterates are indexed from $0$ ; the statement is for $t \ge 1$ and uses $x^{t-1}$ with natural-number subtraction, which is exact since $t \ge 1$ . Only the two ends of the paper's chain of inequalities are stated.

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

/-- Eq. (14) of Li–Pong (p. 8): the change of the dual iterates is controlled by the
changes of the primal iterates. -/
theorem eq14_dual_step_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 + 1) - z t‖ ^ 2 ≤
      (1 / γ) * wnormSq Q3 (x (t + 1) - x t) +
        (1 / (1 - γ)) * wnormSq (T1 * T1) (x t - x (t - 1)) := by sorry

end NonconvexSplitting.ProxADMM

Source

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

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