Lemma 3.3 — $\|\nabla_\Omega f(\cdot)\|$ is lower semicontinuous on $\Omega$

Proved

CalamaiMore.Convergence.projGrad_norm_lsc

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1projected-gradientsemicontinuity

Let $\Omega$ be a nonempty closed convex subset of a finite-dimensional real inner product space $E$ and let $f : E \to \mathbb R$ be continuously differentiable on $\Omega$ . Then the map

x \mapsto \|\nabla_\Omega f(x)\|

is lower semicontinuous on $\Omega$ : if $x_k \to x$ with all $x_k, x \in \Omega$ , then $\|\nabla_\Omega f(x)\| \le \liminf_{k} \|\nabla_\Omega f(x_k)\|$ .

The map need not be continuous: $\nabla_\Omega f$ can be bounded away from zero near a stationary point. Lower semicontinuity is what transfers $\|\nabla_\Omega f(x_k)\| \to 0$ to stationarity of limit points.

Formalization Note Lower semicontinuity on $\Omega$ is Mathlib's LowerSemicontinuousOn, i.e. relative to $\Omega$ .

Preamble

import Mathlib
import Definitions.Def_CalamaiMore_Convergence_projGrad

Formal statement

namespace CalamaiMore.Convergence

/-- Calamai–Moré, Lemma 3.3 (p. 104): `x ↦ ‖∇_Ω f(x)‖` is lower semicontinuous on `Ω`. -/
theorem projGrad_norm_lsc {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) Ω) :
    LowerSemicontinuousOn (fun y => ‖projGrad f Ω y‖) Ω := by sorry

end CalamaiMore.Convergence

Source

Calamai & Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), p. 104, Lemma 3.3

Human review

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

View graph

Lemma 3.3 — ∥∇Ωf(⋅)∥\|\nabla_\Omega f(\cdot)\|∥∇Ω​f(⋅)∥ is lower semicontinuous on Ω\OmegaΩ

Lemma 3.3 — $\|\nabla_\Omega f(\cdot)\|$ is lower semicontinuous on $\Omega$