Strict decrease of the augmented Lagrangian from a non-stationary start

Proved

NonconvexSplitting.ProxADMM.strict_decrease_after_eq28

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 from a non-stationary $x^0$ with $h(x^0) + P(\mathcal M x^0) < \infty$ and $\mathcal M^* z^0 = \nabla h(x^0)$ . Let $\mathcal R := \delta\mathcal I + \mathcal T_2 - \frac{2}{\sigma\beta}\big(\frac1\gamma\mathcal Q_3 + \frac1{1-\gamma}\mathcal T_1^2\big)$ . Then for every $N > 1$

L_\beta(x^N, y^N, z^N) - L_\beta(x^0, \mathcal M x^0, z^0) \le -\frac12\|x^1 - x^0\|^2_{\mathcal R} < 0 .

Passing to the limit along a convergent subsequence turns this into the strict improvement of Theorem 1(ii).

Formalization Note Stated as two conjuncts: the additive EReal inequality for every $N > 1$ , and $\|x^1 - x^0\|^2_{\mathcal R} > 0$ . As in (27), $y^0$ is replaced by $\mathcal M x^0$ .

Preamble

import Mathlib
import Definitions.Def_NonconvexSplitting_Shared_IsStationary
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

/-- Li–Pong, p. 10, the display after (28): for every `N > 1`,
`L_β(x^N, y^N, z^N) ≤ L_β(x⁰, M x⁰, z⁰) - ½‖x¹ - x⁰‖²_R` and `‖x¹ - x⁰‖²_R > 0`. -/
theorem strict_decrease_after_eq28 {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))
    (hns : ¬ IsStationary h P M (x 0))
    (hfin : ((h (x 0) : ℝ) : EReal) + P (M (x 0)) ≠ ⊤) :
    (∀ N : ℕ, 1 < N →
      augLag h P M β (x N) (y N) (z N) ≤
        augLag h P M β (x 0) (M (x 0)) (z 0) +
          ((-(1 / 2) * wnormSq (δ • (1 : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) + T2 - (2 / (σ * β)) • ((1 / γ) • Q3 + (1 / (1 - γ)) • (T1 * T1))) (x 1 - x 0) : ℝ) : EReal)) ∧
    0 < wnormSq (δ • (1 : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) + T2 - (2 / (σ * β)) • ((1 / γ) • Q3 + (1 / (1 - γ)) • (T1 * T1))) (x 1 - x 0) := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 10, the display after (28)

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