Lemma 4.3, p. 15 — sufficient decrease of the potential: Λ^{k+1} − Λ^k ≤ −c_3‖w^k − w^{k+1}‖²

Proved

NAPPAL.Rate.lemma_4_3

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

augmented-lagrangianlyapunovp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1sufficient-decrease

Let Assumptions 1 and 2 hold, set $\delta_k$ as in (8), and let $\{w^k\}$ be generated by NAPP-AL. With $c_2=\frac{7(L_G+L_H)^2}{\gamma\lambda_{\min}(B^\top B)}$ , put

c_4:=\frac{\gamma\lambda_{\min}(B^\top B)-(L_G+L_H)}{2}-c_2,\qquad c_3:=\min\Big\{\frac12,\ c_4,\ \frac1{3\gamma}\Big\}.

Then $c_4>0$ , and for every $k\ge1$ the potential $\Lambda^k$ of (18) satisfies

\Lambda^{k+1}-\Lambda^k\le-c_3\|w^k-w^{k+1}\|^2 .\tag{19}

The potential $\Lambda^k$ is therefore non-increasing, and the squared step lengths are summable once $\Lambda^k$ is bounded below; this is the engine of Theorem 4.1 and Proposition 4.1.

Formalization Note The positivity $c_4>0$ is part of the printed statement (" $(>0)$ ") and is kept as a conjunct. $\Lambda^k$ involves $w^{k-1}$ , so (19) is stated for $k\ge1$ . $\|w^k-w^{k+1}\|$ is the Euclidean norm of the stacked difference.

Preamble

import Mathlib
import Definitions.Def_NAPPAL_Rate_Setting
open Filter Topology
open scoped InnerProductSpace

Formal statement

namespace NAPPAL.Rate

theorem lemma_4_3 {n d m : ℕ} (P : NAPPAL.KL.Problem n d m) (LG LH L0 LK β γ σ : ℝ) (LOmj : Fin m → ℝ)
    (K : NAPPAL.KL.E n → ℝ) (δ ε : ℕ → ℝ) (u : ℕ → NAPPAL.KL.E n) (v : ℕ → NAPPAL.KL.E d) (p : ℕ → NAPPAL.KL.E m)
    (hrun : RunHyp P LG LH L0 LOmj K β LK γ σ δ ε u v p) :
    0 < NAPPAL.KL.c4 P LG LH γ ∧
    ∀ k : ℕ, 1 ≤ k →
      NAPPAL.KL.Lam P LG LH L0 γ u v p (k + 1) - NAPPAL.KL.Lam P LG LH L0 γ u v p k ≤
        -NAPPAL.KL.c3 P LG LH γ * NAPPAL.KL.wdist (u k, v k, p k) (u (k + 1), v (k + 1), p (k + 1)) ^ 2 := by sorry

end NAPPAL.Rate

Source

Zhu, Zhao, Zhang, A First-Order Primal-Dual Method for Nonconvex Constrained Optimization Based on the Augmented Lagrangian, arXiv:2007.12219v1, p. 15, Lemma 4.3, (19)

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph