Is evaluation of formal power series compatible with composition over nonarchimedean complete fields? In algebraic number theory, one may want to consider a $p$-adic local field and consider the $p$-adic logarithm and $p$-adic exponential function on it. These form inverse homomorphism between a sufficiently higher unit group (multiplicative) and a sufficiently high power of the valuation rings' maximal ideal (additive). Usually, care is put into determining where precisely the power series defining the logarithm/exponential converge in order to determine an appropriate domain and codomain for these isomorphisms. However, the fact that $\exp$ and $\log$ are inverse at all is usually claimed to merely be a formal consequence of this identity holding for power series (e.g. in Neukirch's Algebraic Number Theory, Katok's p-adic Analysis Compared with Real and many others). If some further justification is made, it is a callback to the following lemma (e.g. in Gouvea's $p$-adic Numbers or Cassels' Local Fields):
Lemma: If $(b_{nm})_{n,m\in\mathbb{N}}$ is a double sequence in a nonarchimedean complete field $K$, such  that $b_{nm}\rightarrow0$ as $\max(n,m)\rightarrow\infty$, then the double series $\sum_{n\ge0}\sum_{m\ge0}b_{nm}$ and $\sum_{m\ge0}\sum_{n\ge0}b_{nm}$ both exist in $K$ and are equal.
So, the principle underlying this should be answered by the
Question: If $K$ is a nonarchimedean complete field, $P,Q\in K[[X]]$ are formal power series, such that $Q(0)=0$, and $x\in K$, such that the series $Q(x)$ converges in $K$ and the series $P(Q(x))$ converges in $K$, then does the series $(P\circ Q)(x)$, where $P\circ Q\in K[[X]]$ is the formal composite of the power series, converge in $K$ with value $(P\circ Q)(x)=P(Q(x))$?
Let's write $P=\sum_{i\ge0}a_iX^i$ and $Q=\sum_{j\ge1}b_jX^j$. The formal composite works out to be
$$P\circ Q=\sum_{k\ge0}\left(\sum_{i\ge0}a_i\sum_{\substack{j_1+\dotsc+j_i=k\\j_1,\dotsc,j_i\ge1}}b_{j_1}\cdot\dotsc\cdot b_{j_n}\right)X^k.$$ Note that the sum in brackets is a finite sum, since the terms for $i>k$ vanish, but the number of summands is not bounded as $k\rightarrow\infty$. Now, first note that $Q(x)^i=\left(\sum_{j\ge1}b_jx^j\right)^i=\sum_{k\ge0}\left(\sum_{\substack{j_1+\dotsc+j_i=k\\j_1,\dotsc,j_i\ge1}}b_{j_1}\cdot\dotsc\cdot b_{j_i}\right)x^k$. This identity is clear if it were an identity of formal power series, but to justify it as an identity of series in $K$, one also needs the above lemma to justify some rearrangements. Nonetheless, this holds true unconditionally for products of series in a nonarchimedean complete field (see Corollary 2.11 here). Then, we obtain
$$P(Q(x))=\sum_{i\ge0}a_iQ(x)^i=\sum_{i\ge0}\sum_{k\ge0}a_i\sum_{\substack{j_1+\dotsc+j_i=k\\j_1,\dotsc,j_i\ge1}}b_{j_1}\cdot\dotsc\cdot b_{j_i}x^k.$$
This is almost the series $(P\circ Q)(x)$, except we would have to interchange the summations $\sum_{i\ge0}$ and $\sum_{k\ge0}$. If the lemma were to apply in this situation, life would be great and the result would follow. However, I cannot establish the hypothesis that $a_i\sum_{\substack{j_1+\dotsc+j_i=k\\j_1,\dotsc,j_i\ge1}}b_{j_1}\cdot\dotsc\cdot b_{j_i}x^k\rightarrow0$ as $\max(i,k)\rightarrow\infty$.
 A: This is not true in full generality.  For a silly example, suppose $|a_i|$ grows extremely fast, and take $Q(X)=X^2-X$. Then $Q(1)=0$ so $P(Q(1))$ converges.  However, it is easy to see that if you choose $|a_i|$ to grow fast enough then the norms of the coefficients of $P\circ Q$ will still grow fast such that $(P\circ Q)(x)$ cannot converge for any $x\neq 0$ (you just need to choose $|a_k|$ to be large enough so that $\sum_{i\ge0}a_i\sum_{\substack{j_1+\dotsc+j_i=k\\j_1,\dotsc,j_i\ge1}}b_{j_1}\cdot\dotsc\cdot b_{j_n}$ is dominated by the $i=k$ term).
Here, then, is a correct statement.  Suppose $r$ is such that the sequence $|b_j|r^j$ is bounded (in particular, this implies $Q(x)$ converges for all $|x|<r$).  Let $R=\sup_j(|b_j|r^j)$ (this is what you would "formally" expect $|Q(x)|$ to be for $|x|=r$ if there was not any fortuitous cancellation that made it smaller).  Suppose that the sequence $|a_i|R^i$ is also bounded (in particular, this implies $P(Q(x))$ converges for all $|x|<r$).  Then for any $x$ such that $|x|<r$, $(P\circ Q)(x)$ converges to $P(Q(x))$.
(I suspect this can be improved to include the case $|x|=r$ if $|b_j|r^j\to 0$ and $|a_i|R^i\to 0$ so $P(x)$ and $Q(P(x))$ converge for $|x|=r$, but do not quite see how to make the argument work in that case.)
To prove this, as you have observed, it suffices to show that $$c_{ik}=a_i\sum_{\substack{j_1+\dotsc+j_i=k\\j_1,\dotsc,j_i\ge1}}b_{j_1}\cdot\dotsc\cdot b_{j_i}x^k$$ goes to $0$ as $\max(i,k)\to\infty$.  Since $|b_j|\leq R/r^j$ for all $j$, we have $|c_{ik}|\leq |a_i|R^i|x|^k/r^k$.  Since $|x|<r$, $|x|^k/r^k\to 0$ as $k\to\infty$.  Since $|a_i|R^i$ is bounded, this means $c_{ik}\to 0$ as $k\to \infty$ uniformly in $i$.  Since $c_{ik}=0$ for $i>k$, this implies $c_{ik}\to 0$ as $\max(i,k)\to\infty$, as desired.
A: Here is a slight improvement on the estimations.
Proposition: Let $K$ be a nonarchimedean complete field and $P=\sum_{i\ge0}a_iX^i,Q=\sum_{j\ge1}b_jX^j\in K[[x]]$. If $0\le r$ is such that $|b_j|r^j\rightarrow0$ as $j\rightarrow\infty$, so in particular $R=\max_{j\ge1}|b_j|r^j$ exists, and furthermore $|a_i|R^i\rightarrow0$ as $i\rightarrow\infty$, then $P\circ Q$ converges at all $x\in K$, such that $|x|\le r$, with value $(P\circ Q)(x)=P(Q(x))$.
Remark: The hypotheses of the proposition are weaker than that $r$ be smaller than the convergence radius of $Q$ (resp. that $R$ be smaller than the convergence radius of $P$), but stronger than that $r$ be smaller than or equal to the convergence radius of $Q$ (resp. that $R$ be smaller than or equal to the convergence radius of $P$). If $r\in|K|$ (resp. $R\in|K|$), the condition is precisely equivalent to $Q$ converging on the closed disk of radius $r$ (resp. $P$ converging on the closed disk of radius $R$).
Proof: Let $x\in K$, such that $|x|\le r$. Note that $0\le|b_jx^j|=|b_j||x|^j\le |b_j|r^j\rightarrow0$ as $j\rightarrow\infty$, hence $b_jx^j\rightarrow0$ as $j\rightarrow\infty$. In particular, $Q(x)$ converges. Furthermore, $|b_jx^j|\le|b_j|r^j\le R$ for all $j\ge1$. By the nonarchimedean triangle inequality, $|Q(x)|\le R$, so $P(Q(x))$ converges*. Since $|a_i|R^i\rightarrow0$ as $i\rightarrow\infty$, $S=\max_{i\ge0}|a_i|R^i$ exists. If $R=0$, then $Q=0$ or $r=0$ and the theorem is trivial in either case, so we may assume $R>0$. If $S=0$, then $P=0$ and the theorem is trivial again, so we may assume $S>0$. As established in the question, it suffices to show that $$c_{ik}=a_i\sum_{\substack{j_1+\dotsc+j_i=k\\j_1,\dotsc,j_i\ge1}}b_{j_1}\cdot\dotsc\cdot b_{j_i}x^k\rightarrow0\qquad\text{as }\max(i,k)\rightarrow\infty.$$
Let $\varepsilon>0$ be arbitrary.  Choose $I\ge0$, such that $|a_i|R^i<\varepsilon$ for $i\ge I$, and $J\ge1$, such that $|b_jx^j|<\varepsilon R/S$ for $j\ge J$. Let $i,k\ge0$, such that $\max(i,k)\ge IJ$. If $i\ge I$, then the previous estimate shows $|c_{ik}|\le|a_i|R^i|x|^k/r^k\le|a_i|R^i<\varepsilon$. If $i<I$, then $\max(i,k)\ge IJ\ge I>i$ forces $k=\max(i,k)\ge IJ$. If $j_1,\dotsc,j_i\ge1$ are such that $j_1+\dotsc+j_i=k$, then we can find an $1\le a\le i$, such that $j_a\ge k/i>k/I\ge IJ/I=J$. It follows that $|b_{j_1}x^{j_1}\cdot\dotsc\cdot b_{j_i}x^{j_i}|\le R^{i-1}|b_{j_a}x^{j_a}|< R^i\varepsilon/S$. The nonarchimedean triangle inequality then implies $|c_{ik}|<|a_i|R^i\varepsilon/S\le\varepsilon$. The claim follows.$\square$
*This would technically already follow from the following estimates.
