The problem of minimizing locally a $C^2$ functional around non-critical points is well-posed

In this paper, we prove the following general result: Let $X$ be a real Hilbert space and $J:X\to {\bf R}$ a $C^1$ functional, with locally Lipschitzian derivative.

Then, for each $x_0\in X$ with $J'(x_0)\neq 0$, there exists $\delta>0$ such that, for every $r\in ]0,\delta[$, the restriction of $J$ to the sphere $\{x\in X : \Vert x-x_0\Vert=r\}$ has a unique global minimum toward which every minimizing sequence strongly converges.