A non-stationary start with $\mathcal M^* z^0 = \nabla h(x^0)$ gives $x^1 \neq x^0$

Proved

NonconvexSplitting.ProxADMM.x1_ne_x0

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. Suppose the initial point $x^0$ is not a stationary point of $\min_x h(x) + P(\mathcal M x)$ , that $h(x^0) + P(\mathcal M x^0) < \infty$ , and that $z^0$ satisfies $\mathcal M^* z^0 = \nabla h(x^0)$ . Then

x^1 \ne x^0 .

This is the first step of the proof that a non-stationary start is strictly improved upon.

Preamble

import Mathlib
import Definitions.Def_NonconvexSplitting_Shared_IsStationary
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

/-- Li–Pong, p. 10: from a non-stationary start with `M* z⁰ = ∇h(x⁰)`, the first primal step moves. -/
theorem x1_ne_x0 {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)
    (hz0 : ContinuousLinearMap.adjoint M (z 0) = gradient h (x 0))
    (hns : ¬ IsStationary h P M (x 0))
    (hfin : ((h (x 0) : ℝ) : EReal) + P (M (x 0)) ≠ ⊤) :
    x 1 ≠ x 0 := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 10, first paragraph of the proof of Theorem 1(ii)

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

A non-stationary start with M∗z0=∇h(x0)\mathcal M^* z^0 = \nabla h(x^0)M∗z0=∇h(x0) gives x1≠x0x^1 \neq x^0x1=x0

A non-stationary start with $\mathcal M^* z^0 = \nabla h(x^0)$ gives $x^1 \neq x^0$