Lemma 4.2, pp. 11–12 — one-step change estimates for the augmented Lagrangian L_γ

Proved

NAPPAL.Rate.lemma_4_2

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

augmented-lagrangiandescent-lemmap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1primal-dual

Let Assumptions 1 and 2 hold and let $\{w^k\}$ be generated by NAPP-AL, with $q^k=p^k+\gamma(\Theta(u^k)+Bv^k)$ and step $\epsilon^k$ . Write $\lambda=\lambda_{\min}(B^\top B)$ and

a_k:=\frac{\beta}{2\epsilon^k}-\frac{L_G+\|q^k\|L_\Omega+\gamma(L^0_\Theta)^2}{2},\qquad b:=\frac{\gamma\lambda-(L_G+L_H)}{2}.

For every $k\ge1$ ,

\mathcal L_\gamma(u^{k+1},v^{k+1},p^k)-\mathcal L_\gamma(u^k,v^k,p^k)\le-a_k\|u^k-u^{k+1}\|^2-b\|v^k-v^{k+1}\|^2+\frac1{2\gamma}\big(\|p^{k-1}-p^k\|^2-\|p^k-p^{k+1}\|^2\big)+\frac1\gamma\|p^k-p^{k+1}\|^2 .

For every $k\ge0$ ,

\mathcal L_\gamma(u^{k+1},v^{k+1},p^{k+1})-\mathcal L_\gamma(u^{k+1},v^{k+1},p^k)=\frac1\gamma\|p^k-p^{k+1}\|^2 .

For every $k\ge1$ ,

\begin{aligned}\mathcal L_\gamma(w^{k+1})-\mathcal L_\gamma(w^k)\le{}&-a_k\|u^k-u^{k+1}\|^2-b\|v^k-v^{k+1}\|^2+\frac1{2\gamma}\big(\|p^{k-1}-p^k\|^2-\|p^k-p^{k+1}\|^2\big)\\&+\frac{6\gamma\|B\|^2(L^0_\Theta)^2}{\lambda}\|u^k-u^{k+1}\|^2+\frac{6(L_G+\gamma\|B\|L^0_\Theta)^2}{\gamma\lambda}\|u^{k-1}-u^k\|^2+\frac{6(L_G+L_H)^2}{\gamma\lambda}\|v^{k-1}-v^k\|^2 .\end{aligned}

These are the descent estimates from which the sufficient decrease of the potential $\Lambda^k$ (Lemma 4.3) is assembled.

Formalization Note Parts 1 and 3 involve $p^{k-1}$ , $u^{k-1}$ , $v^{k-1}$ and are stated for $k\ge1$ . As printed, the lemma does not assume the step rule (8).

Preamble

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

Formal statement

namespace NAPPAL.Rate

theorem lemma_4_2 {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)
    (hA1 : NAPPAL.KL.Assumption1 P LG LH L0 LOmj) (hA2 : NAPPAL.KL.Assumption2 P K β LK γ LG LH)
    (hrun : IsNAPPAL P K γ σ δ ε u v p) :
    (∀ k : ℕ, 1 ≤ k →
      NAPPAL.KL.augLag P γ (u (k + 1), v (k + 1), p k) - NAPPAL.KL.augLag P γ (u k, v k, p k) ≤
        -(β / (2 * ε k) - (LG + ‖qseq P γ u v p k‖ * NAPPAL.KL.LOm LOmj + γ * L0 ^ 2) / 2) *
            ‖u k - u (k + 1)‖ ^ 2 -
          (γ * NAPPAL.KL.lamMin P - (LG + LH)) / 2 * ‖v k - v (k + 1)‖ ^ 2 +
          1 / (2 * γ) * (‖p (k - 1) - p k‖ ^ 2 - ‖p k - p (k + 1)‖ ^ 2) +
          1 / γ * ‖p k - p (k + 1)‖ ^ 2) ∧
    (∀ k : ℕ,
      NAPPAL.KL.augLag P γ (u (k + 1), v (k + 1), p (k + 1)) - NAPPAL.KL.augLag P γ (u (k + 1), v (k + 1), p k) =
        1 / γ * ‖p k - p (k + 1)‖ ^ 2) ∧
    (∀ k : ℕ, 1 ≤ k →
      NAPPAL.KL.augLag P γ (u (k + 1), v (k + 1), p (k + 1)) - NAPPAL.KL.augLag P γ (u k, v k, p k) ≤
        -(β / (2 * ε k) - (LG + ‖qseq P γ u v p k‖ * NAPPAL.KL.LOm LOmj + γ * L0 ^ 2) / 2) *
            ‖u k - u (k + 1)‖ ^ 2 -
          (γ * NAPPAL.KL.lamMin P - (LG + LH)) / 2 * ‖v k - v (k + 1)‖ ^ 2 +
          1 / (2 * γ) * (‖p (k - 1) - p k‖ ^ 2 - ‖p k - p (k + 1)‖ ^ 2) +
          6 * γ * ‖P.B‖ ^ 2 * L0 ^ 2 / NAPPAL.KL.lamMin P * ‖u k - u (k + 1)‖ ^ 2 +
          6 * (LG + γ * ‖P.B‖ * L0) ^ 2 / (γ * NAPPAL.KL.lamMin P) * ‖u (k - 1) - u k‖ ^ 2 +
          6 * (LG + LH) ^ 2 / (γ * NAPPAL.KL.lamMin P) * ‖v (k - 1) - v k‖ ^ 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, pp. 11–12, Lemma 4.2(i)–(iii)

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