Eq. (21) — summed estimate of the augmented Lagrangian

Proved

NonconvexSplitting.ProxADMM.eq21_summed

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

\mathcal R := \delta\mathcal I + \mathcal T_2 - \frac{2}{\sigma\beta}\mathcal H_\gamma, \qquad \mathcal H_\gamma = \frac1\gamma\mathcal Q_3 + \frac{1}{1-\gamma}\mathcal T_1^2 .

Then for all integers $1 \le M_0 < N$

L_\beta(x^N, y^N, z^N) - L_\beta(x^{M_0}, y^{M_0}, z^{M_0}) \le -\frac12\sum_{t=M_0}^{N-2}\|x^{t+1} - x^t\|^2_{\mathcal R} + \frac12\|x^{M_0} - x^{M_0-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}.

(The sum is empty when $N = M_0 + 1$ .)

It shows that the augmented Lagrangian decreases along the iterates up to a single boundary term.

Formalization Note The paper writes the summation start as $M$ ; here it is $M_0$ , since $\mathcal M$ is the linear map. Only the first and last members of the paper's chain are stated, 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. (21) of Li–Pong (p. 9): the summed estimate for the augmented Lagrangian, first and
last members, with `R = δ I + T₂ - (2/(σβ)) H_γ`. The summation start is `M₀` (the paper's `M`). -/
theorem eq21_summed {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)
    (M₀ N : ℕ) (hM₀ : 1 ≤ M₀) (hN : M₀ < N) :
    augLag h P M β (x N) (y N) (z N) ≤
      augLag h P M β (x M₀) (y M₀) (z M₀) +
        ((-(1 / 2) * ∑ t ∈ Finset.Ico M₀ (N - 1),
            wnormSq (δ • (1 : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) + T2 - (2 / (σ * β)) • ((1 / γ) • Q3 + (1 / (1 - γ)) • (T1 * T1))) (x (t + 1) - x t) +
          1 / 2 * wnormSq ((2 / (σ * β * (1 - γ))) • (T1 * T1)) (x M₀ - x (M₀ - 1)) : ℝ) : EReal) := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 9, Eq. (21) and the definition of R after it

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