Theorem 2.11 — Polyak's method with $0 < \gamma < 2$ reaches or converges to the level set $M(c)$

Proved

ShorNonsmooth.Fejer.polyak_method_converges

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

fejer-mapp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1polyak-stepsubgradient-method

Let $f$ be a convex function on $E_n$ , $f^* = \inf f(x)$ , and $c \ge f^*$ a level whose set $M(c) = \{x \in E_n : f(x) \le c\}$ is nonempty. For a subgradient selection $g_f$ consider Polyak's method

x_{k+1} = x_k - \frac{\gamma\,[f(x_k) - c]}{\|g_f(x_k)\|^2}\, g_f(x_k), \qquad k = 0, 1, \dots, \qquad (2.32)

which stops once $x_k \in M(c)$ . If $0 < \gamma < 2$ , then for any $x_0 \in E_n$ either $x_{k^*} \in M(c)$ for some $k^*$ , or the limit $\lim_{k \to \infty} x_k$ exists and belongs to $M(c)$ .

The method needs only the level $c$ , not the minimum point; with $c = f^*$ (when attained) it converges to a minimum point of $f$ , and with $c > f^*$ it solves the convex inequality $f(x) \le c$ .

Formalization Note The page prints the label as "Theorem 9.11"; the text on p. 40 ("Theorems 2.11 and 2.14") shows it is Theorem 2.11. The book presupposes a point $y \in M(c)$ , so $M(c) \neq \emptyset$ is assumed (for $c = f^*$ this means the infimum is attained). The subgradient selection is arbitrary and need not be continuous. The step map sets $\varphi_c(x) = x$ on $M(c)$ , as the book does; it also stops when $g_f(x) = 0$ , which under these hypotheses already implies $x \in M(c)$ . The conclusion " $\lim x_k \in M(c)$ " is stated as existence of a limit lying in $M(c)$ .

Preamble

import Mathlib
import Definitions.Def_ShorNonsmooth_Fejer_PolyakMethod

open Filter Topology

Formal statement

namespace ShorNonsmooth.Fejer

/-- Shor (1985), p. 37, Theorem 2.11 (printed "Theorem 9.11", a misprint for 2.11). Let `f` be
convex on `E_n`, `c ≥ f* = inf f` with nonempty level set `M(c) = {x : f(x) ≤ c}`, and let
`{x_k}` be generated by Polyak's method (2.32),
`x_{k+1} = x_k - γ [f(x_k) - c] / ‖g_f(x_k)‖² · g_f(x_k)`, stopped once `x_k ∈ M(c)`, for an
arbitrary subgradient selection `g_f`. If `0 < γ < 2`, then for any `x₀ ∈ E_n` either
`x_{k*} ∈ M(c)` for some `k*`, or `lim_{k→∞} x_k` exists and belongs to `M(c)`. -/
theorem polyak_method_converges {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ConvexOn ℝ Set.univ f) (c : ℝ) (hM : (levelSet f c).Nonempty)
    (γ : ℝ) (hγ0 : 0 < γ) (hγ2 : γ < 2)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hg : ∀ x, ShorNonsmooth.AlmostDiff.IsSubgradient f x (g x))
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (hx : ∀ k, x (k + 1) = polyakStep f g c γ (x k)) :
    (∃ kstar : ℕ, x kstar ∈ levelSet f c) ∨
      ∃ xbar ∈ levelSet f c, Tendsto x atTop (𝓝 xbar) := by sorry

end ShorNonsmooth.Fejer

Source

Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 37, Theorem 2.11 (printed "Theorem 9.11") with formula (2.32)

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 2.11 — Polyak's method with 0<γ<20 < \gamma < 20<γ<2 reaches or converges to the level set M(c)M(c)M(c)

Theorem 2.11 — Polyak's method with $0 < \gamma < 2$ reaches or converges to the level set $M(c)$