Prove2Me

Theorem 3.12 — the level set {f=f∞}\{f = f_\infty\} contains a point with linearly dependent GfG_f

Open
ShorNonsmooth.RAlgorithm.exists_dependent_point_at_limit_level

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

convergencenonsmooth-optimizationp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1piecewise-smoothr-algorithm

Let the assumptions of Theorem 3.11 and condition (3.50) hold: n≥1n \ge 1, f∈Kf \in K with f(x)→+∞f(x) \to +\infty as ∥x∥→∞\|x\| \to \infty, α>1\alpha > 1, and {xk}\{x_k\} a sequence constructed by the r(α)r(\alpha)-algorithm applied to ff with ∥xk+1−xk∥→0\|x_{k+1} - x_k\| \to 0. The values f(xk)f(x_k) are nonincreasing and bounded below, so

f∞=lim⁡k→∞f(xk)>−∞f_\infty = \lim_{k \to \infty} f(x_k) > -\infty

exists. Then the level set U={x:f(x)=f∞}U = \{x : f(x) = f_\infty\} contains a point x∗x^* such that the set of vectors Gf(x∗)G_f(x^*) is linearly dependent.

For a smooth ff (one piece) linear dependence of Gf(x∗)={∇f(x∗)}G_f(x^*) = \{\nabla f(x^*)\} means ∇f(x∗)=0\nabla f(x^*) = 0; in general it is a generalized stationarity condition. The theorem says the monotone values of the rr-algorithm settle at a level containing such a point.

Formalization Note f∞f_\infty is written as inf⁡kf(xk)\inf_k f(x_k), which equals the limit because the values are nonincreasing and bounded below. Linear dependence of the set Gf(x∗)G_f(x^*) is ¬ LinearIndependent of the family indexed by the elements of the set (a set containing 00 is dependent).

Preamble
import Mathlib
import Definitions.Def_ShorNonsmooth_RAlgorithm_RAlgorithm

open scoped InnerProductSpace
open Filter Topology
Formal statement
namespace ShorNonsmooth.RAlgorithm

/-- Shor (1985), p. 84, **Theorem 3.12**. Under the assumptions of Theorem 3.11 and condition
(3.50), let `f_∞ = lim_{k→∞} f(x_k)` (the values `f(x_k)` are nonincreasing and bounded below,
p. 82, so the limit is their infimum). Then the set `U = {x : f(x) = f_∞}` contains a point `x*`
such that the set of vectors `G_f(x*)` is linearly dependent. -/
theorem exists_dependent_point_at_limit_level {n : ℕ} (hn : 0 < n) (P : KRep n)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : P.Forms f)
    (hf_coercive : Tendsto f (cocompact (EuclideanSpace ℝ (Fin n))) atTop)
    (α : ℝ) (hα : 1 < α)
    (x gt g : ℕ → EuclideanSpace ℝ (Fin n))
    (B : ℕ → EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) (h : ℕ → ℝ)
    (hrun : IsRun P f α 0 x gt g B h)
    (hstep : Tendsto (fun k => ‖x (k + 1) - x k‖) atTop (𝓝 0)) :
    ∃ xs : EuclideanSpace ℝ (Fin n), f xs = ⨅ k, f (x k) ∧
      ¬ LinearIndependent ℝ ((↑) : P.Gf xs → EuclideanSpace ℝ (Fin n)) := by sorry

end ShorNonsmooth.RAlgorithm
Source
Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 84, Theorem 3.12 (proof pp. 84–85); f∞f_\infty defined on p. 82
Human review

  • Endorsed by Shuze Chen · Oct 2, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 2, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph