Valuation bound for coefficients of an integral formal logarithm (source code)

= Valuation bound for coefficients of an integral formal logarithm
{title2=$v_K(c_n)\geq-e\,v_p(n)$}

For an integral one-dimensional <formal group law> over a finite extension of the p-adic field, the inverse of $\partial_YF(T,0)$ has integral coefficients because its constant term is one. Integrating this invariant differential gives $\log_F(T)=T+\sum_{n\geq2}c_nT^n$ with $nc_n$ integral. For $v_K(\pi)=1$ and $e=v_K(p)$ the displayed bound follows. The estimate $v_p(n)\leq(n-1)/(p-1)$ makes the nonlinear part strictly contracting on $\pi^s\mathcal O_K$ for $s>e/(p-1)$, yielding the <deep logarithm subgroup of a formal group>.