Eq. (2.33) — a Polyak step strictly decreases the distance to every point of
ProvedShorNonsmooth.Fejer.polyak_step_dist_sq_lefejer-mapp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1polyak-stepsubgradient-method
Let be convex on , , , and . Let , let be a subgradient of at , and set
Then for every
This is the Fejér inequality behind every result of the section: it says that Polyak's step is an -Fejér map, and it quantifies the decrease.
Formalization Note The step is written out with the single subgradient ; the hypotheses force (a zero subgradient would make a minimum point, hence ), so the division is genuine.
Preamble
import Mathlib import Definitions.Def_ShorNonsmooth_Fejer_PolyakMethod open Filter Topology
Formal statement
namespace ShorNonsmooth.Fejer
/-- Shor (1985), p. 37, inequality (2.33) (proof of Theorem 2.11). Let `f` be convex on `E_n`,
`M(c) = {x : f(x) ≤ c}`, `0 < γ < 2`, and let `g_k` be a subgradient of `f` at `x_k ∉ M(c)`.
Then for every `y ∈ M(c)` the Polyak step `x_{k+1} = x_k - γ [f(x_k) - c] / ‖g_k‖² · g_k`
satisfies
`‖x_{k+1} - y‖² ≤ ‖x_k - y‖² - γ(2 - γ) [f(x_k) - c]² / ‖g_k‖² < ‖x_k - y‖²`. -/
theorem polyak_step_dist_sq_le {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
(hf : ConvexOn ℝ Set.univ f) (c γ : ℝ) (hγ0 : 0 < γ) (hγ2 : γ < 2)
(xk gk y : EuclideanSpace ℝ (Fin n)) (hgk : ShorNonsmooth.AlmostDiff.IsSubgradient f xk gk)
(hxk : xk ∉ levelSet f c) (hy : y ∈ levelSet f c) :
‖xk - (γ * (f xk - c) / ‖gk‖ ^ 2) • gk - y‖ ^ 2 ≤
‖xk - y‖ ^ 2 - γ * (2 - γ) * (f xk - c) ^ 2 / ‖gk‖ ^ 2 ∧
‖xk - y‖ ^ 2 - γ * (2 - γ) * (f xk - c) ^ 2 / ‖gk‖ ^ 2 < ‖xk - y‖ ^ 2 := by sorry
end ShorNonsmooth.Fejer
Source
Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 37, inequality (2.33) (proof of Theorem 2.11)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.