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?
 A: 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$.
A: 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}$. 
