Eq. (10) — convergence of $P(y^{t_i+1})$ along a convergent subsequence

Proved

NonconvexSplitting.ProxADMM.eq10_along_subseq

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, and let $(x^t, y^t, z^t)$ be generated by the proximal ADMM. If $(x^{t_i}, y^{t_i}, z^{t_i}) \to (x^*, y^*, z^*)$ along a strictly increasing sequence $t_i$ , then $P(y^*)$ is finite and

\lim_{i\to\infty} P(y^{t_i+1}) = P(y^*).

Together with (9) this is what allows passing to the limit in the inclusion $-z^{t+1} - \beta\mathcal M(x^{t+1}-x^t) \in \partial P(y^{t+1})$ .

Formalization Note The paper's (10) is a limit of real numbers equal to $P(y^*)$ ; the finiteness of $P(y^*)$ , which the limit presupposes, is stated as part of the conclusion. The convergence is 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. (10) of Li–Pong (pp. 9–10): along a convergent subsequence, `P(y^{t_i+1}) → P(y*)`,
and the limit `P(y*)` is finite. -/
theorem eq10_along_subseq {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)
    (s : ℕ → ℕ) (hs : StrictMono s) (xs : EuclideanSpace ℝ (Fin n)) (ys zs : EuclideanSpace ℝ (Fin m))
    (hconv : Tendsto (fun i => (x (s i), y (s i), z (s i))) atTop (𝓝 (xs, ys, zs))) :
    Tendsto (fun i => P (y (s i + 1))) atTop (𝓝 (P ys)) ∧ P ys ≠ ⊤ := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, pp. 9–10, proof that (10) holds along the subsequence (22)

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

Eq. (10) — convergence of P(yti+1)P(y^{t_i+1})P(yti​+1) along a convergent subsequence

Eq. (10) — convergence of $P(y^{t_i+1})$ along a convergent subsequence