Eq. (27) — first-step estimate of the augmented Lagrangian

Proved

NonconvexSplitting.ProxADMM.eq27_first_step

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 and Assumption 1 with witnesses $\sigma, \mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \delta, \mathcal Q_3, \gamma$ , and let $(x^t, y^t, z^t)$ be generated by the proximal ADMM with $\mathcal M^* z^0 = \nabla h(x^0)$ . Then, with $y^0$ replaced by $\mathcal M x^0$ ,

L_\beta(x^1, y^1, z^1) - L_\beta(x^0, \mathcal M x^0, z^0) \le \frac12\|x^1 - x^0\|^2_{\frac{2}{\sigma\beta\gamma}\mathcal Q_3 - \delta\mathcal I - \mathcal T_2}.

This replaces (20) at $t = 0$ , where no $x^{-1}$ exists.

Formalization Note The paper "writes $y^0 = \mathcal M x^0$ "; since $y^0$ is not an input of the method, the statement uses $\mathcal M x^0$ directly and places no condition on the sequence's own $y^0$ . The inequality is written additively in EReal.

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. (27) of Li–Pong (p. 10), with `y⁰` replaced by `M x⁰` as the paper writes. -/
theorem eq27_first_step {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)
    (hz0 : ContinuousLinearMap.adjoint M (z 0) = gradient h (x 0)) :
    augLag h P M β (x 1) (y 1) (z 1) ≤
      augLag h P M β (x 0) (M (x 0)) (z 0) +
        ((1 / 2 * wnormSq ((2 / (σ * β * γ)) • Q3 - δ • (1 : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) - T2) (x 1 - x 0) : ℝ) : EReal) := by sorry

end NonconvexSplitting.ProxADMM

Source

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

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