Showing that a nonlinear operator over function spaces is differentiable and locally invertible? 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.
 A: If $F(f) = G(f,f')$ for some $G\in C^\infty(\mathbb{R}^2)$ then I think you can establish that
$$
F'(f)u = (\partial_1 G)(f,f')u + (\partial_2 G)(f,f')u'
$$
holds in much the same way as if you were dealing with functions of real variables. Writing $D:C^1 \to C$ for differentiation and $I:C^1\to C$ for the inclusion map,
$$
F'(f) = (\partial_1 G)(f,f')I + (\partial_2 G)(f,f')D
$$
is:

*

*Fredholm if $(\partial_2 G)(f,f')$ is everywhere nonzero; and

*Compact if $(\partial_2 G)(f,f')$ is everywhere zero

In the second case, $F'(f)$ can't be an isomorphism.
For the example you give (i.e. $G(x,y) = \sinh(x)+y^2$), $F'(0)$ is the inclusion of $C^1$ into $C$, which can't be an isomorphism for the simpler reason that not all continuous functions are $C^1$.
A: 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.
