existence and uniqueness of solutions for ODEs in formal power series?

I came across this question and it looked like something that is likely to have been looked into, but I couldn't find a reference.

Let $k$ be some (algebraically closed, if needed) field. There is a formal differentiation in the ring of formal power series $k[[x]]$. Let $F(x,y) \in k[[x,y]]$ be a formal series which is algebraic over $x$ and $y$. Consider a differential equation: $$y'=F(x,y)$$ where $y$ belongs to the maximal ideal of $k[[x]]$, so $F(x,y)$ is well-defined. What is known about solutions of such ODEs?

Is it true that there exists a formal series $y \in k[[x]]$ that satisfies the equation? Is it true that it is unique?

-

Yes. No algebraicity assumption is necessary. Rewrite the desired condition as

$$y = \int_0^x F(x, y) \, dx = \sum_{n, m \ge 0} f_{n, m} \int_0^x x^n y^m \, dx = L(x, y).$$

We compute that

$$L(x, y_0) - L(x, y_1) = \sum_{n, m \ge 0} f_{n, m} \int_0^x x^n (y_0^n - y_1^m) \, dx$$

hence that if $x^k | y_0 - y_1$ then $x^{k+1} | L(x, y_0) - L(x, y_1)$. It follows that the operation $y \mapsto L(x, y)$ on $x k[[x]]$ is Lipschitz with respect to the $x$-adic metric with Lipschitz constant less than $1$ (the exact constant depends on how you're defining the $x$-adic metric), hence has a unique fixed point by the Banach fixed point theorem. (This is a formal version of the standard proof of Picard-Lindelöf.) Moreover, this fixed point has coefficients in the field generated by $f_{n, m}$.

-
is there a standard reference for this in the formal setting? –  Dima Sustretov Feb 13 at 23:33
This solution is way too complicated. It's much easier: the way we teach students to find a power series solution. Just plug in and equate similar terms to get a "chain-like" linear system in the coefficients of $y$: each coefficient is uniquely found in terms of the previous ones. (And you assume $y_0=0$.) Or, if you prefer, keep differentiating the equation and substituting $x=0$: you'll get $y^{(n)}$ in terms of the previous derivatives. Since the series are formal, it's even easier as there's no convergence issue. –  Alex Degtyarev Feb 13 at 23:39
@Alex: there's nothing particularly complicated about the Banach fixed point theorem. –  Qiaochu Yuan Feb 14 at 1:56
Of course there's nothing complicated about the contraction principle. But when it is used to solve a triangular system, students start hating mathematics. –  Alex Degtyarev Feb 14 at 5:15

This is a very simple fact which is verified by hands. You just plug a formal power series for $y$, and see that all coefficients can be uniquely determined. (Condition that $y$ belongs to the maxial ideal is just a fancy way to state that the constant term of $y$ is zero, that is "$y(0)=0$"). It is included in many old books on analytic functions and differential equations. For example H. Cartan, Théorie élémentaire des fonctions analytiques d'une ou plusieurs variables complexes. (There is an English, Russian and German translations). G. Valiron, Fonctions analytiques. This is a part of the standard proof of existence of analytic solutions. If in addition the series for $F$ converges, then so does the series for $y$.

-