Lemma 3.1 — basic properties of the projected gradient
ProvedCalamaiMore.ActiveSet.projGrad_propertiesLet be a nonempty closed convex subset of a finite-dimensional real inner product space , let be continuously differentiable on , let , and let be the projected gradient, the point of the tangent cone nearest to . Then:
and the minimum is attained; 3. is a stationary point of if and only if .
Part (b) identifies as the steepest rate of first-order decrease of along feasible directions of unit length, which is why is the natural measure of non-stationarity.
Formalization Note "Continuously differentiable on " is ∀ x ∈ Ω, DifferentiableAt ℝ f x together with ContinuousOn (gradient f) Ω (the standing assumption of §3). The minimum in (b) is IsLeast of the set of values, so attainment is part of the statement.
import Mathlib import Definitions.Def_CalamaiMore_ActiveSet_projGrad import Definitions.Def_CalamaiMore_Shared_IsStationaryPoint
namespace CalamaiMore.ActiveSet
/-- Calamai–Moré, Lemma 3.1 (p. 102), under the standing assumptions of §3 (`Ω` nonempty closed
convex, `f` continuously differentiable on `Ω`), at `x ∈ Ω`:
(a) `-⟨∇f(x), ∇_Ω f(x)⟩ = ‖∇_Ω f(x)‖²`;
(b) `min {⟨∇f(x), v⟩ : v ∈ T(x), ‖v‖ ≤ 1} = -‖∇_Ω f(x)‖` (the minimum is attained);
(c) `x` is a stationary point iff `∇_Ω f(x) = 0`. -/
theorem projGrad_properties {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
(Ω : Set E) (hΩne : Ω.Nonempty) (hΩc : IsClosed Ω) (hΩcv : Convex ℝ Ω)
(f : E → ℝ) (hfd : ∀ x ∈ Ω, DifferentiableAt ℝ f x) (hfc : ContinuousOn (gradient f) Ω)
(x : E) (hx : x ∈ Ω) :
-inner ℝ (gradient f x) (projGrad f Ω x) = ‖projGrad f Ω x‖ ^ 2 ∧
IsLeast {r : ℝ | ∃ v ∈ CalamaiMore.Shared.tangentCone Ω x, ‖v‖ ≤ 1 ∧ r = inner ℝ (gradient f x) v}
(-‖projGrad f Ω x‖) ∧
(CalamaiMore.Shared.IsStationaryPoint f Ω x ↔ projGrad f Ω x = 0) := by sorry
end CalamaiMore.ActiveSet
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.