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

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

is lower semicontinuous on $\Omega$: for every sequence $\{x_k\} \subseteq \Omega$ converging to $x \in \Omega$, $\|\nabla_\Omega f(x)\| \le \liminf_k \|\nabla_\Omega f(x_k)\|$.

The projected gradient itself need not be continuous, since the tangent cone jumps when the point reaches a new face of $\Omega$; lower semicontinuity of its norm is what survives, and it is what shows that the limit of a sequence with $\|\nabla_\Omega f(x_k)\| \to 0$ is stationary.

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