I am aware that the implicit and inverse function theorems can be generalized to infinite dimensional cases, but I am having difficulty in applying it to a specific calculation.


Let $C^1\_{\mathbb{R}}[0,1]$ be the space of real-valued $C^1$ functions on the interval $[0,1]$. If we impose the following norm:
$$
\begin{equation}
\lVert f \rVert := \lVert f \rVert\_{\sup}+\lVert f' \rVert\_{\sup}
\end{equation}
$$
for $f \in C^1\_{\mathbb{R}}[0,1]$, it is clear that $C^1\_{\mathbb{R}}[0,1]$ is a Banach space over $\mathbb{R}$.  

Similarly, $C\_{\mathbb{R}}[0,1]$ is the Banach space of real-valued continuous functions on $[0,1]$ with the supremum norm.


Then, we can think of the operator $F:C\_{\mathbb{R}}^1[0,1] \to C\_{\mathbb{R}}[0,1]$ defined by
$$
\begin{equation}
F(f):=\sinh(f)+(f')^2
\end{equation}
$$
How do I show that (or is it indeed true that) $F$ is strongly $C^1$ and the derivative at each point is a linear isomorphism? More generally, how about the case $f \to G(f,f')$ for any smooth function $G : \mathbb{R}^2 \to \mathbb{R}$ whose Jacobian determinant never vanishes?


I appreciate any help.



Showing that a nonlinear operator over function spaces is differentiable and locally invertible?
The derivative of $F$ at $f \in C^1[0,1])$ is by definition the linear operator $F'(f): C^1[0,1] \rightarrow C[0,1]$ given by
$$ F'(f)\dot{f} = \lim\_{t\rightarrow 0} \frac{F(f+t\dot{f}) - F(f)}{t}. $$
Here, you get
$$
F'(f) = (\cosh f)\dot{f} + 2f'\dot{f}'.
$$
To apply the inverse function theorem, you need a linear operator $G(f): C[0,1] \rightarrow C^1[0,1]$ such that $F'(f)G(f)g = g$. In other words, given any $g in C[0,1]$, you need to be able to solve for $\dot{f} \in C^1[0,1]$ so that
$$
(\cosh f)\dot{f} + 2f'\dot{f}' = g.
$$
It's easy to check that if $f = 0$, then this is not possible. $F'(0)$ does have a right inverse, but it is not a bounded linear map from $C[0,1]$ to $C^1[0,1]$. So you cannot invert $F$ near $f = 0$ using the inverse function theorem for Banach spaces. In order to use the inverse function theorem, you need to "regain" the derivative you lost because $F'(f)$ is a first order differential operator.


So you want to restrict to $f$ such that the linear ODE above is a nondegenerate one, i.e., you can write it in the form
$$
\dot{f}' = \dots,
$$
where the right side is continuous on $[0,1]$. Next, you show that, for a given $f$, this ODE always has a solution $\dot{f} \in C^1[0,1]$. You also need to show that the map from $g$ to $\dot{f}$ can be chosen to be a bounded linear map from $C[0,1]$ to $C^1[0,1]$. This is all straightforward using the existence and uniqueness theorem for ODEs.


Offhand, I don't see how to show that $F$ is locally invertible on a neighborhood of $0$ in $C^1[0,1]$. However, you can show that it is locally invertible in a neighborhood of $0$ in $C^k[0,1]$ for $k$ sufficiently large (including $k = \infty$) by using the Nash-Moser inverse function theorem, as mentioned by @DCM.


