The Morse Lemma on Banach Spaces

Let be a map of an open subset U of a Banach space E. Let be a critical point of <!-- MATH $f(d{f_p} = 0)$ --> . If E is a conjugate space <!-- MATH $(E = {F^ \ast })$ --> we define what it means for p to be nondegenerate. In this case there is a diffeomorphism of a neighborhood of p with a neighborhood of <!-- MATH $0 \in E,\gamma (p) = 0$ --> with <!-- MATH \begin{displaymath} f \circ {\gamma ^{ - 1}}(x) = \frac{1}{2}{d^2}{f_p}(x,x) + f(p). \end{displaymath} -->