Second Derivative Test in Banach Spaces According to $[$Exercise $12.8$, $1]$ we have the following version of the Second Derivative Test:
Theorem. Let $E=(E,\|\cdot \|)$ be a Banach space, let $D$ be a subset of $E$ and suppose $f: D \rightarrow \mathbb{R}$ is $2$ times continuously differentiable at a point $x \in D$. If $f'(x)=0$ and the bilinear form $f''(x)$ is positive definite that is $[f''(x)(v)](v)>0$ for every nonzero $v \in E$, then $f$ attains a local mininum at $x \in D$ that is there exists an $\varepsilon>0$ such that if $\|y-x\|<\varepsilon$, then $f(x)<f(y)$.
Here, the differentiability is in the Fréchet sense, where $f'(x):E \rightarrow \mathbb{R}$ denote the first Fréchet derivative of $f$ at $x$ and $f''(x)$ stands the second Fréchet derivative of $f$ at $x$ so that for each $v \in E$, $f''(x)v \in \mathcal{L}(E, \mathbb{R})$ . Moreover, $f$ be $2$ times continuously differentiable in $x$ means that the function $y \mapsto f'(y)$ is continuously differentiable in $x$ that is $y \mapsto f'(y)$ is differentiable at each point in a neighborhood of $x$ and $y \mapsto f'(y)$ is continuous at $x$.
Question. The theorem above is true? If is true, how to prove?
I've seen similar results $($for instance in $[2])$. However, in general such results require that the domain $D$ of the functional be either open/convex $($for instance, a open ball in $E)$. In this case, we have that the domain of the functional is just a subset of $E$. So I seriously doubt whether such a result remains valid in this subset context. In $[1]$ the author gives a hint to prove the theorem: use the Mean Value Theorem $([$Theorem $12.7$, $1])$ twice to show that $f(y)-f(x)>0$ for all $y \in E$ in a sufficiently small ball around $x$. But even then I still haven't been able to prove such a result. Is it possible to prove it this way?
$[1]$ Baggett, L. Functional analysis. A primer. Marcel Dekker, Inc., New York, $1992$.
$[2]$ Deimling, K., Nonlinear functional analysis. Springer-Verlag, Berlin, $1985$.
 A: The theorem is not true.
Here is a counterexample: Take $E=l^2$, $D=E$, and
$$
f(x) = \sum_k \frac1k x_k^2 -x_k^3.
$$
Then
$$
f'(x)v = \sum_k (\frac2k x_k -3x_k^2)v_k,
$$
$$
f''(x)(v,v) = \sum_k (\frac2k  -6x_k)v_k^2,
$$
hence $f(0)=0$, $f'(0)=0$ and $f''(0)(v,v)>0$ for all $v\ne 0$. One can check that these derivatives are Frechet derivatives and continuous.
Define $y_n := \frac 2n e_n$, where $e_n$ is the standard unit vector.
Then $y_n \to 0$, $f(y_n) = -4/n^3$, and $x=0$ is not a local minimum of $f$.
The problem is that $f''(0)(e_n,e_n) = \frac2n$, which gets arbitrarily small. A sufficient condition would be the existence of $\delta>0$ such that
$$
f''(x)(v,v) \ge \delta \|v\|^2 \quad\forall v.
$$
In finite-dimensional spaces this follows from the $f''(x)(v,v)>0$ for all $v\ne0$ due to compactness of the unit ball.
A: daw gave a nice answer/counterexample.
I want to add a more geometric interpretation.
There is a version of Morse Lemma in the Hilbert setting, which asserts that  if $x_0$ is a non-degenerate critical point of $f\in C^3(E,\mathbb R)$ i.e.  $f''(x_0)$ induces an
isomorphism $v\in E\mapsto f''(x_0)(v,\cdot)\in E^*$  with the dual of $E$ then  up to a smooth change of coordinates defined in a neighbourhood of $x_0$, $f$  takes the form
$$f(v) = f(x_0) + \frac 1 2 \vert\vert P_+ v \vert\vert^2 - \frac 1 2 \vert\vert P_- v \vert \vert^2$$
where $P_+, P_- : E\to E$ are orthogonal projectors to the positive/negative eigenspace of $f''(x_0)$.
Therefore $f$ becomes locally a quadratic functional.
From this we see that if $f''(x_0)$ is also positive definite (and $x_0$ is non-degenerate as above) then $P_- =0$ thus locally $f(v) = f(x_0) + \frac 1 2 \vert\vert P_+ v \vert\vert^2$
and we have a minimum at $x_0$.
However positive definiteness is not enough to have non-degeneracy if $E$ is infinite dimensional.
A sufficient condition that can be added is to require that  $\vert \vert f''(x_0)(v,\cdot)\vert \vert\geq C \vert \vert v \vert \vert$ for some $C>0$
this indeed implies that $v\mapsto f''(x_0)(v,\cdot):E\to E^*$ has closed range and now positive definiteness is enough to conclude that is also invertible (continuously).
This can be found in
Palais, Morse theory on Hilbert manifolds,  Topology, Vol.2  pp. 299-340. 1963.
