I am trying to prove the strong differentiability version of the Inverse Function Theorem for Banach spaces, but I am not sure if it is true. I am interested in this because it is a kind of punctual version of the theorem. So my main question is:
Is the strong differentiability version of the Inverse Function Theorem true for Banach spaces?
Here is the definition of strong differentiability.
Definition Let $E$ and $E'$ be normed linear spaces, $A \subseteq E$ an open set, $a \in A$ a point and $f: A \to E'$ a function. We say $f$ is strong differentiable at $a$ when there is a continuous linear map $D: E \to E'$ such that $$\lim_{(x,x') \to (a,a)} \frac{f(a+x')-f(a+x) - D(x'-x)}{x'-x} = 0.$$
In this case, $f$ is differentiable at $a$ and $D = Df|_a$, that is, the linear map $D$ is the differential of $f$ at $a$.
Considerer the remainder function $r_a(v) = f(a+v) - f(a) - Df|_a(v)$. In finite dimensional spaces, strong differentiability at $a$ can be shown to be equivalent to this: for every $\varepsilon > 0$, there is a neighborhood of the origin in which the function $r_a$ is Lipschitz with Lipscitz constant $\varepsilon$. I believe this is also true for infinite dimensions, but have not proved it yet.
Inverse Function Theorem (strongly differentiable) Let $E$ and $E'$ be Banach spaces, $A \subseteq E$ an open set, $a \in A$ a point and $f: A \to E'$ a function which is strongly differentiable at $a$ and such that $Df|_a:E \to E'$ is a linear isomorphism. In this case, there is an open neighborhood $V \subseteq A$ of $a$ such that $f|_V: V \to f(V)$ is a homeomorphism, the inverse function $f^{-1}: f(V) \to V$ is strongly differentiable at $f(a)$ and its differentiable at $f(a)$ is $Df^{-1}|_{f(a)} = (Df|_{a})^{-1}$.