Lemma 4.1, p. 11 — bounding the dual variable: the dual step is controlled by the primal steps

Proved

NAPPAL.Rate.lemma_4_1

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

augmented-lagrangiandual-variablep2o-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 any admissible steps). Then:

for every $k\ge0$ ,

\|B^\top(p^k-p^{k+1})\|^2\ge\lambda_{\min}(B^\top B)\|p^k-p^{k+1}\|^2;

for every $k\ge1$ ,

B^\top p^k=-\nabla_vG(u^{k-1},v^{k-1})-\nabla H(v^{k-1})+\gamma B^\top[\Theta(u^k)-\Theta(u^{k-1})];

for every $k\ge1$ ,

\|p^k-p^{k+1}\|^2\le\frac{3\gamma^2\|B\|^2(L^0_\Theta)^2}{\lambda_{\min}(B^\top B)}\|u^k-u^{k+1}\|^2+\frac{3(L_G+\gamma\|B\|L^0_\Theta)^2}{\lambda_{\min}(B^\top B)}\|u^{k-1}-u^k\|^2+\frac{3(L_G+L_H)^2}{\lambda_{\min}(B^\top B)}\|v^{k-1}-v^k\|^2.

The dual iterates have no step size of their own; this lemma bounds their movement by the movement of the primal iterates, which is what lets the potential $\Lambda^k$ decrease.

Formalization Note Parts 2 and 3 involve $w^{k-1}$ and are stated for $k\ge1$ . The lemma does not assume the step rule (8); its hypotheses are Assumptions 1–2 and the NAPP-AL relation only, as printed. $B^\top$ is the adjoint of $B$ and $\|B\|$ the operator norm.

Preamble

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

Formal statement

namespace NAPPAL.Rate

theorem lemma_4_1 {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 : ℕ, ‖ContinuousLinearMap.adjoint P.B (p k - p (k + 1))‖ ^ 2 ≥
        NAPPAL.KL.lamMin P * ‖p k - p (k + 1)‖ ^ 2) ∧
    (∀ k : ℕ, 1 ≤ k →
      ContinuousLinearMap.adjoint P.B (p k) =
        -NAPPAL.KL.gradV P (u (k - 1)) (v (k - 1)) - gradient P.H (v (k - 1)) +
          γ • ContinuousLinearMap.adjoint P.B (NAPPAL.KL.Theta P (u k) - NAPPAL.KL.Theta P (u (k - 1)))) ∧
    (∀ k : ℕ, 1 ≤ k →
      ‖p k - p (k + 1)‖ ^ 2 ≤
        3 * γ ^ 2 * ‖P.B‖ ^ 2 * L0 ^ 2 / NAPPAL.KL.lamMin P * ‖u k - u (k + 1)‖ ^ 2 +
          3 * (LG + γ * ‖P.B‖ * L0) ^ 2 / NAPPAL.KL.lamMin P * ‖u (k - 1) - u k‖ ^ 2 +
          3 * (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, p. 11, Lemma 4.1(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