Does the implicit function theorem imply Peano existence theorem

Solution 1:

Observe that we have Fréchet-differentiability in the second argument at the point where you want your implicit function. Indeed, the function $T: Y \mapsto (Y', Y(0))$ is linear, and we have $$ \lim_{Y \to 0} \frac{\mathcal H(0, X + Y) - (\mathcal H(0, X) + T(Y))}{\|Y\|_1} = \lim_{Y \to 0} \frac{(0, 0)}{\|Y\|_1} = 0, $$ which is why $d_2 \mathcal H(0, x_0)$ exists and is equal to $T$. Note that $T$ is invertible, since $Y(0)$ determines the integration constant. Furthermore, we can obtain the following modified version of theorem 3.4.10:

Let $X, Y, Z$ be Banach spaces. Let $U \times V \subseteq X \times Y$, $g : U \times V \to Z$ and let $(x, y) \in U \times V$ such that $d_2(x, \cdot)$ exists and $G$ is continuous and $G(x, y) = 0$, and further such that there exists $W \subseteq V$ such that $y \in W$ and $G(z, w) \to G(x, w)$ as $z \to x$ uniformly for $w \in W$. Then there exist $M \subseteq U$ and $N \subseteq W$ such that for each $\xi \in X$, there exists a unique $\eta \in M$ such that $G(\xi, \eta) = 0$ and the thereby defined function is continuous.

In the proof, we replace the mean value theorem in part by the uniform convergence from the assumption, where we choose $N$ small enough such that $\|d_2 L(x, \cdot)\| < 1/4$.

From this theorem, we obtain Peano's existence theorem as in the given proof.

Note also that uniqueness does not follow, since the IFT only gives uniqueness locally around the constant function.