Prove2Me

P(xti+1)→P(x∗)P(x^{t_i+1}) \to P(x^*) along a convergent subsequence

Proved
NonconvexSplitting.ProxGrad.P_tendsto_along_subseq

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

nonconvex-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-gradient

Assume the hypotheses of Theorem 4: the standing assumptions on hh and PP; qq twice continuously differentiable and convex; ℓ>0\ell > 0 with −ℓI⪯∇2h(x)+∇2q(x)⪯ℓI-\ell I \preceq \nabla^2 h(x) + \nabla^2 q(x) \preceq \ell I for all xx; step size β∈(0,1/ℓ)\beta \in (0, 1/\ell); and (xt)(x^t) generated by (43). If xti→x∗x^{t_i} \to x^* along a strictly increasing sequence of indices tit_i, then

lim⁡i→∞P(xti+1)=P(x∗).\lim_{i \to \infty} P(x^{t_i + 1}) = P(x^*) .

Together with (47), this gives the function-value convergence xti+1→Px∗x^{t_i+1} \xrightarrow{P} x^* required by the definition of the limiting subdifferential.

Formalization Note The limit is taken in EReal.

Preamble
import Mathlib
import Definitions.Def_NonconvexSplitting_ProxGrad_StandingAssumptions
import Definitions.Def_NonconvexSplitting_ProxGrad_HessianSandwich
import Definitions.Def_NonconvexSplitting_ProxGrad_IsProxGradSeq

open Filter Topology
Formal statement
namespace NonconvexSplitting.ProxGrad

/-- Li–Pong (p. 19): under the hypotheses of Theorem 4, if `x^{t_i} → x*` along a strictly
increasing `t_i`, then `P(x^{t_i + 1}) → P(x*)` (in `EReal`). -/
theorem P_tendsto_along_subseq {n : ℕ} (h q : EuclideanSpace ℝ (Fin n) → ℝ) (P : EuclideanSpace ℝ (Fin n) → EReal) (ℓ β : ℝ)
    (x : ℕ → EuclideanSpace ℝ (Fin n))
    (hSA : StandingAssumptions h P) (hq : ContDiff ℝ 2 q) (hq_convex : ConvexOn ℝ Set.univ q)
    (hℓ : 0 < ℓ) (h44 : HessianSandwich h q ℓ) (hβ : 0 < β)
    (hβℓ : β < 1 / ℓ) (hx : IsProxGradSeq h P β x)
    (xs : EuclideanSpace ℝ (Fin n)) (φ : ℕ → ℕ) (hφ : StrictMono φ)
    (hlim : Tendsto (x ∘ φ) atTop (𝓝 xs)) :
    Tendsto (fun i => P (x (φ i + 1))) atTop (𝓝 (P xs)) := by sorry

end NonconvexSplitting.ProxGrad
Source
Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 19, first paragraph of the page
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