Remark 4(1) — Theorem 3 when $L_\beta$ is a KL function

Proved

NonconvexSplitting.ADMMKL.remark4_kl_convergence

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

admmkurdyka-lojasiewicznonconvex-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $h:\mathbb R^n\to\mathbb R$ be twice continuously differentiable with bounded Hessian, $P:\mathbb R^m\to(-\infty,+\infty]$ proper and closed, $\mathcal M:\mathbb R^n\to\mathbb R^m$ linear and $\beta>0$ , with augmented Lagrangian $L_\beta(x,y,z)=h(x)+P(y)-\langle z,\mathcal Mx-y\rangle+\frac\beta2\|\mathcal Mx-y\|^2$ . Suppose Assumption 1 holds with $\mathcal T_1=0$ (hence $\phi=0$ ), with witnesses $\sigma,\mathcal Q_1,\mathcal Q_2,\delta,\mathcal Q_3,\gamma$ , and let $(x^t,y^t,z^t)_{t\ge0}$ be generated by the ADMM

y^{t+1}\in\operatorname*{Arg\,min}_y L_\beta(x^t,y,z^t),\qquad x^{t+1}\in\operatorname*{Arg\,min}_x L_\beta(x,y^{t+1},z^t),\qquad z^{t+1}=z^t-\beta(\mathcal Mx^{t+1}-y^{t+1}).

Suppose that $L_\beta$ , as a function of $(x,y,z)$ on $\mathbb R^n\times\mathbb R^m\times\mathbb R^m$ , is a KL function, and that $(x^t,y^t,z^t)$ has a cluster point $(x^*,y^*,z^*)$ . Then $(x^t,y^t,z^t)\to(x^*,y^*,z^*)$ , $x^*$ is a stationary point of $\min_x h(x)+P(\mathcal Mx)$ , and

\sum_{t=0}^{\infty}\|x^{t+1}-x^t\|<\infty .

This is the analytic core of Theorem 3: the semi-algebraic hypothesis is used only to guarantee the KL property of $L_\beta$ .

Formalization Note The ADMM is the relation IsProxADMMSeq with $\phi = 0$ (the Bregman term vanishes); Assumption 1 is instantiated with $\phi = 0$ and $\mathcal T_1 = 0$ , and $\mathcal T_2$ is left as a parameter (Assumption 1 forces $0 \preceq \mathcal T_2 \preceq \mathcal T_1 = 0$ ). Values of $L_\beta$ and $P$ live in EReal; iterates are indexed from $0$ , and $y^0$ is not constrained. Finite length is Summable (fun t => ‖x (t+1) - x t‖); summability does not depend on the first term, so this is the paper's (34) summed from $t=1$ .

Preamble

import Mathlib
import Definitions.Def_NonconvexSplitting_Shared_StandingAssumptions
import Definitions.Def_NonconvexSplitting_Shared_Assumption1
import Definitions.Def_NonconvexSplitting_Shared_IsProxADMMSeq
import Definitions.Def_NonconvexSplitting_Shared_LimitingSubdiff
import Definitions.Def_NonconvexSplitting_Shared_IsStationary
import Definitions.Def_NonconvexSplitting_ADMMKL_AugLagProd
import Definitions.Def_NonconvexSplitting_ADMMKL_KLProperty
open NonconvexSplitting.Shared

open Filter Topology
open scoped InnerProductSpace

Formal statement

namespace NonconvexSplitting.ADMMKL

/-- Remark 4(1) of Li–Pong (p. 16): the conclusion of Theorem 3 holds when the semi-algebraicity
of `h` and `P` is replaced by the assumption that the augmented Lagrangian `L_β` (a function of
the triple `(x, y, z)`) is a KL function: the ADMM sequence converges to its cluster point
`(x*, y*, z*)`, `x*` is stationary, and `∑ ‖x^{t+1} - x^t‖ < ∞`. -/
theorem remark4_kl_convergence {n m : ℕ} (h : EuclideanSpace ℝ (Fin n) → ℝ) (P : EuclideanSpace ℝ (Fin m) → EReal)
    (M : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)) (β : ℝ)
    (hstd : StandingAssumptions h P (fun _ => 0) β)
    (σ δ γ : ℝ) (Q1 Q2 T2 Q3 : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hA : Assumption1 h (fun _ => 0) M β σ Q1 Q2 0 T2 δ Q3 γ)
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (y z : ℕ → EuclideanSpace ℝ (Fin m))
    (hseq : IsProxADMMSeq h P (fun _ => 0) M β x y z)
    (hKL : IsKLFunction (augLagX h P M β))
    (xs : EuclideanSpace ℝ (Fin n)) (ys zs : EuclideanSpace ℝ (Fin m))
    (hclu : ∃ s : ℕ → ℕ, StrictMono s ∧
      Tendsto (fun i => (x (s i), y (s i), z (s i))) atTop (𝓝 (xs, ys, zs))) :
    Tendsto x atTop (𝓝 xs) ∧ Tendsto y atTop (𝓝 ys) ∧ Tendsto z atTop (𝓝 zs) ∧
      IsStationary h P M xs ∧ Summable (fun t => ‖x (t + 1) - x t‖) := by sorry

end NonconvexSplitting.ADMMKL

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 16, Remark 4(1)

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

Remark 4(1) — Theorem 3 when LβL_\betaLβ​ is a KL function

Remark 4(1) — Theorem 3 when $L_\beta$ is a KL function