By a theorem of Mattuck [*Abelian Varieties over $p$-Adic Ground Fields*, Annals of Mathematics, Second Series, Vol. 62, No. 1 (Jul., 1955), pp. 92-119], for an Abelian variety $A$ of dimension $g$ over a $p$-adic local field $K$ with ring of integers $O_K$, there is an exact sequence $0 \to O_K^g \to A(K) \to \{\mathrm{finite}\} \to 0$.

Is there an analogue of this theorem for Abelian varieties over $\mathbf{F}_q(\!(t)\!)$ (e.g. with $O_K^g$ replaced by a pro-$p$-group)? The only thing I found is a remark in [Milne, *Arithmetic Duality Theorems*, Remark I.3.6, bottom of p. 45]. For elliptic curves, there is Proposition 10.2.26 (Filtration of $E(K)$) in [Liu, *Algebraic Geometry and
Arithmetic Curves*, 2nd ed.].

Commutative formal groups], but it introduces a lot of notation and is therefore difficult to read. $\endgroup$