Theorem 3.13 — the $r(\alpha)$ -algorithm converges to an isolated local minimum

Open

ShorNonsmooth.RAlgorithm.converges_to_isolated_local_min

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

convergencelocal-minimumnonsmooth-optimizationp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1r-algorithm

Let $n \ge 1$ , let $f \in K$ satisfy (3.50), let $\alpha > 1$ , and let $\{x_k\}_{k=0}^\infty$ be a sequence generated by the $r(\alpha)$ -algorithm applied to $f$ satisfying (3.52), $\|x_{k+1} - x_k\| \to 0$ (the assumptions of Theorem 3.12).

Let $x^*$ be an isolated local minimum point of $f$ and let the starting point $x_0$ be such that the set

S = \{x \in E_n : f(x^*) \le f(x) \le f(x_0)\}

has a connected component containing both $x^*$ and $x_0$ . Suppose that this component contains no point $z \neq x^*$ whose set $G_f(z)$ is linearly dependent. Then

\lim_{k \to \infty} x_k = x^* .

This is the section's convergence theorem: under a nondegeneracy condition on the region the iterates can visit, the $r$ -algorithm with exact directional minimization converges to the local minimum in that region.

Formalization Note "Isolated local minimum point" is read as a local minimum point having a neighbourhood that contains no other local minimum point. The connected component is connectedComponentIn S x₀, required to contain $x^*$ . The book states this theorem as a corollary of Theorem 3.11 without proof.

Preamble

import Mathlib
import Definitions.Def_ShorNonsmooth_RAlgorithm_RAlgorithm

open scoped InnerProductSpace
open Filter Topology

Formal statement

namespace ShorNonsmooth.RAlgorithm

/-- Shor (1985), p. 85, **Theorem 3.13**. Let `x*` be an isolated local minimum point of `f ∈ K`
(a local minimum having a neighbourhood that contains no other local minimum point) and let `x₀`
be a starting point such that the set `S = {x ∈ E_n : f(x*) ≤ f(x) ≤ f(x₀)}` has a connected
component containing `x*` and `x₀`. Suppose that this component contains, except for `x*`, no
point `z` with linearly dependent `G_f(z)`. Then, under the assumptions of Theorem 3.12
(those of Theorem 3.11 and (3.50)), the sequence `{x_k}` generated by the `r(α)`-algorithm
converges to `x*`. -/
theorem converges_to_isolated_local_min {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)) (hxs_min : IsLocalMin f xs)
    (hxs_isolated : ∃ V ∈ 𝓝 xs, ∀ y ∈ V, IsLocalMin f y → y = xs)
    (hxs_comp : xs ∈ connectedComponentIn {y | f xs ≤ f y ∧ f y ≤ f (x 0)} (x 0))
    (hindep : ∀ z ∈ connectedComponentIn {y | f xs ≤ f y ∧ f y ≤ f (x 0)} (x 0), z ≠ xs →
      LinearIndependent ℝ ((↑) : P.Gf z → EuclideanSpace ℝ (Fin n))) :
    Tendsto x atTop (𝓝 xs) := by sorry

end ShorNonsmooth.RAlgorithm

Source

Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 85, Theorem 3.13

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

Theorem 3.13 — the r(α)r(\alpha)r(α)-algorithm converges to an isolated local minimum

Theorem 3.13 — the $r(\alpha)$ -algorithm converges to an isolated local minimum