Theorem 2.16 — with the Camerini–Fratta–Maffioli coefficient, $-s_k$ makes a smaller angle with $x^* - x_k$

Proved

ShorNonsmooth.Fejer.cfm_angle_ge

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

conjugate-subgradientp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1subgradient-method

Let $f$ be convex on $E_n$ with a minimum point $x^*$ and $f^* = f(x^*)$ , and let $\{x_k\}$ , $\{s_k\}$ be generated by the procedure (2.38) with $0 < \gamma_k \le 1$ and the coefficients

\beta_k = \begin{cases} -\alpha_k \dfrac{(s_{k-1}, g_f(x_k))}{\|s_{k-1}\|^2} & \text{if } (s_{k-1}, g_f(x_k)) < 0,\\[4pt] 0 & \text{otherwise,}\end{cases} \qquad 0 \le \alpha_k \le 2,

for any subgradient selection $g_f$ . Then for every $k$ with $s_k \neq 0$ and $g_f(x_k) \neq 0$

\frac{(x_k - x^*,\, s_k)}{\|s_k\|} \ge \frac{(x_k - x^*,\, g_f(x_k))}{\|g_f(x_k)\|} . \qquad (2.39)

The direction $-s_k$ therefore forms an angle with the direction from $x_k$ towards the minimum that is no larger than that of the negative subgradient.

Formalization Note These $\beta_k$ are nonnegative, so the conditions of Theorem 2.15 hold. The book divides by $\|s_k\|$ and $\|g_f(x_k)\|$ ; the inequality is stated at the indices where both are nonzero.

Preamble

import Mathlib
import Definitions.Def_ShorNonsmooth_Fejer_PolyakMethod

open Filter Topology

Formal statement

namespace ShorNonsmooth.Fejer

/-- Shor (1985), p. 41, Theorem 2.16, inequality (2.39). Under the conditions of Theorem 2.15
(`f` convex with minimum point `x*`, `f* = f(x*)`, procedure (2.38) with `0 < γ_k ≤ 1`), let
`β_k = -α_k (s_{k-1}, g_f(x_k)) / ‖s_{k-1}‖²` if `(s_{k-1}, g_f(x_k)) < 0` and `β_k = 0`
otherwise, with `0 ≤ α_k ≤ 2`. Then
`(x_k - x*, s_k) / ‖s_k‖ ≥ (x_k - x*, g_f(x_k)) / ‖g_f(x_k)‖`
for every `k` at which `s_k ≠ 0` and `g_f(x_k) ≠ 0` (the book divides by both norms). -/
theorem cfm_angle_ge {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ConvexOn ℝ Set.univ f) (xstar : EuclideanSpace ℝ (Fin n))
    (hmin : ∀ y, f xstar ≤ f y)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hg : ∀ x, ShorNonsmooth.AlmostDiff.IsSubgradient f x (g x))
    (γ α : ℕ → ℝ) (hγ : ∀ k, 0 < γ k ∧ γ k ≤ 1) (hα : ∀ k, 0 ≤ α k ∧ α k ≤ 2)
    (x s : ℕ → EuclideanSpace ℝ (Fin n)) (hs0 : s 0 = g (x 0))
    (hx : ∀ k, x (k + 1) = x k - cfmStepsize f (f xstar) (γ k) (x k) (s k) • s k)
    (hs : ∀ k, s (k + 1) = g (x (k + 1)) + cfmBeta (α (k + 1)) (s k) (g (x (k + 1))) • s k) :
    ∀ k, s k ≠ 0 → g (x k) ≠ 0 →
      inner ℝ (x k - xstar) (s k) / ‖s k‖ ≥ inner ℝ (x k - xstar) (g (x k)) / ‖g (x k)‖ := by sorry

end ShorNonsmooth.Fejer

Source

Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 41, Theorem 2.16, inequality (2.39)

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.16 — with the Camerini–Fratta–Maffioli coefficient, −sk-s_k−sk​ makes a smaller angle with x∗−xkx^* - x_kx∗−xk​

Theorem 2.16 — with the Camerini–Fratta–Maffioli coefficient, $-s_k$ makes a smaller angle with $x^* - x_k$