.
This work has been supported by the ANR10BLAN 0109 LEDA project.

Abstract
Let be an effective field of characteristic zero. An effective tribe is a subset of which is effectively stable under the algebra operations, restricted division, composition, the implicit function theorem, as well as restricted monomial transformations with arbitrary rational exponents. Given an effective tribe with an effective zero test, we will prove that an effective version of the Weierstrass division theorem holds inside the tribe.
Keywords: Power series, algorithm, Weierstrass preparation, Dalgebraic power series, tribe
There are two main aspects about effective computations with formal power series. On the one hand, we need fast algorithms for the computation of coefficients. There is an important literature on this subject and the asymptotically fastest methods either rely on Newton's method [1] or on relaxed power series evaluation [7].
On the other hand, there is the problem of deciding whether a given power series is zero. This problem is undecidable in general, since we need to check the cancellation of an infinite number of coefficients. Therefore, a related subject is the isolation of sufficiently large classes of power series such that most of the common operations on power series can be carried out inside the class, but such that the class remains sufficiently restricted such that we can design effective zero tests.
In section 2, we first recall the most common operations on formal power series over a field of characteristic zero: the algebra operations, restricted division, composition, the resolution of implicit equations, and so called restricted monomial transformations with arbitrary rational exponents. A subset of which is stable under each of these operations will be called a tribe. We will also specify effective counterparts of these notions.
The main result of this note is presented in section 4: given an effective tribe with an effective zero test, we show that the tribe also satisfies an effective version of the Weierstrass preparation theorem [10], and we give an algorithm for performing Weierstrass division with remainder. Our result can for instance be applied to the tribes of algebraic power series and Dalgebraic power series (see also [4, 5, 9]).
The fact that the collection of all Dalgebraic power series satisfies the Weierstrass preparation theorem was first proved in a more ad hoc way by van den Dries [6]. The notion of a tribe also shares some common properties with the notion of a Weierstrass system, as introduced by Denef and Lipshitz [3] and used in [6]. Our main theorem can be regarded as a simpler, effective and more systematic way to prove that certain types of power series form Weierstrass systems.
The idea behind our main algorithm is very simple: given a series of Weierstrass degree in , we just compute the solutions of the equation in inside a sufficiently large field of gridbased power series. This allows us to compute the polynomial which we know to be the Weierstrass polynomial associated to . Using the stability of the tribe under restricted monomial transformations, we will be able to compute as an element of .
The algorithms rely on our ability to compute with the auxiliary gridbased power series . For this reason, we briefly recall some basic facts about gridbased power series in section 3, as well as the basic techniques which are needed in order to compute with them.
Let be a field of characteristic zero and denote
where we understand that is naturally included in for each . So each element is a power series in a finite number of variables.
We say that is effective if its elements can be represented by concrete data structures and if all field operations can be carried out by algorithms. We say that admits an effective zero test if we also have an algorithm which takes on input and which returns true if and false otherwise.
If is effective, then a power series is said to be computable if we have an effective bound for its dimension (so that ), together with an algorithm which takes on input and produces the coefficient of on output. We will denote the set of computable power series by .
Let be a subset of . We will denote for each and say that is effective if . In this section, we will give definitions of several operations on power series and the corresponding closure properties that may satisfy. From now on, we will always assume that is at least a algebra. It is also useful to assume that is inhabited in the sense that for all . For each , we will denote and . We say that is stable under differentiation if for all (whence ).
The above closure properties admit natural effective analogues. We say that is an effective algebra if is an effective field, if the elements of can be represented by concrete data structures and the algebra operations can be carried out by algorithms. We say that is effectively inhabited if there is an algorithm which takes on input and which computes . We say that is effectively stable under differentiation if there exists an algorithm which takes and on input and which computes .
We say that is stable under restricted division if whenever and are such that . If is effective, then we say that is effectively stable under restricted division if we also have an algorithm which computes as a function of , whenever . Here we do not assume the existence of a test whether (the behaviour of the algorithm being unspecified if ). More generally, given , we say that is stable under restricted division by if whenever , and that is effectively stable under restricted division by if this division can be carried out by algorithm.
Given , we let denote the evaluation of at . Given and with , we define the composition of and to be the unique power series with
We say that a power series domain is stable under composition if for any and with . If we also have an algorithm for the computation of , then we say that is effectively stable under composition.
We notice that stability under composition implies stability under permutations of the . In particular, it suffices that for to be inhabited. Stability under composition also implies stability under the projections with
If is also stable under restricted division by (whence under restricted division by any ), then this means that we may compute the coefficients of the power series expansion of with respect to by induction over :
Similarly, we obtain stability under the differentiation: for any and , we have
Let with and . Assume that the matrix formed by the first columns of the scalar matrix
is invertible. Then the implicit function theorem implies that there exist unique power series , such that the completed vector with satisfies . We say that a power series domain satisfies the implicit function theorem (for implicit functions) if for the above solution of , whenever . We say that effectively satisfies the implicit function theorem if we also have an algorithm to compute as a function of .
We claim that satisfies the implicit function theorem for implicit functions as soon as satisfies the implicit function theorem for one implicit function and is stable under restricted division and composition. We prove this by induction over . For the statement is clear, so assume that . Since is invertible at least one of the must be non zero. Modulo a permutation of rows we may assume that . Applying the implicit function theorem to only, we obtain a function with . Differentiating this relation, we also obtain
for each . Setting , this yields in particular
Now consider the series . For each , we have
In particular,
By the induction hypothesis, we may thus compute series such that for all . Setting , we conclude that and
for all .
Consider an invertible matrix with rational coefficients. Then the transformation
is called a monomial transformation, where is considered as a column vector. For a power series whose support satisfies , we may apply the monomial transformation to as well:
We say that is stable under restricted monomial transformations if for any and invertible matrix with , we have . We say that is effectively stable under restricted monomial transformations if we also have an algorithm to compute as a function of and . Notice that we do not require the existence of a test whether in this case (the behaviour of the algorithm being unspecified whenever ).
If has positive integer coefficients, then we always have and is trivially stable under the monomial transformation whenever is stable under composition.
We say that the algebra with is a local community if is stable under composition, the resolution of implicit equations, and restricted division by . We say that is a tribe if is also stable under restricted monomial transformations. Effective local communities and tribes are defined similarly.
A power series is said to be algebraic if it satisfies a non trivial algebraic equation over the polynomial ring . Setting , this is the case if and only if the module is a vector space of finite dimension. Using this criterion, it is not hard to prove that the set of algebraic power series is a tribe (and actually the smallest tribe for inclusion). Assume that is an effective field. Then an effective algebraic power series can be effectively represented as an effective power series together with an annihilator . It can be shown that is an effective tribe for this representation.
A power series is said to be Dalgebraic if it satisfies a non trivial algebraic differential equation for each , where is a non zero polynomial in variables with coefficients in . We denote by the set of Dalgebraic power series. If is an effective field, then effective Dalgebraic power series may again be represented through an effective power series and differential annihilators of the above form. In [9], one may find more information on how to compute with Dalgebraic power series, and a full proof of the fact that is an effective tribe (the proof being based on earlier techniques from [4, 5]).
In what follows, we will only consider commutative monoids. A monomial monoid is a multiplicative monoid with an asymptotic partial ordering which is compatible with the multiplication (i.e. and ). We denote by the set of infinitesimal elements in and by the set of bounded elements in . We say that has powers if we also have a powering operation such that and for all and .
A monomial monoid is said to be effective if its elements can be represented by effective data structures and if we have algorithms for the multiplication and the asymptotic ordering . Since this implies the existence of an effective equality test. A monomial group is said to be effective if it is an effective monomial monoid with an algorithm for the group inverse. We say that is an effective monomial group with powers if we also have a computable powering operation.
A subset is said to be gridbased if there exist finite sets and such that
If is actually a group which is generated (as a group) by its infinitesimal elements, then we may always take .
If is an effective monomial monoid, then a gridbased subset is said to be effective if the predicate is computable and if finite sets and with (1) are explicitly given.
Let be a field of characteristic zero. Given a formal series with , the set will be called the support of . We say that the formal series is gridbased if its support is gridbased and we denote by the set of such series. A gridbased series is said to be infinitesimal or bounded if resp. , and we denote by resp. the sets of such series.
In [8, Chapter 2] elementary properties of gridbased series are studied at length. We prove there that forms a ring in which all series with are invertible. In particular, if is a totally ordered group, then forms a field. Given a power series and gridbased series , there is also a natural definition for the composition .
Given a gridbased series the maximal elements of for are called dominant monomials for . If has a unique dominant monomial, then we say that is regular, we write for the dominant monomial of , and call the dominant coefficient of . If is totally ordered, then any non zero gridbased series in is regular.
Assume that and are effective. Then a gridbased series is said to be effective if its support is effective and if the map is computable. It can be shown that the set of computable gridbased series forms an effective algebra.
Given an “infinitesimal” indeterminate , the set is a monomial monoid for the asymptotic ordering , and coincides with . Similarly, coincides with the field of Laurent series and with the field of Puiseux series in over . If is algebraically closed, then so is .
Given monomial monoids , one may form the product monomial monoid with for all . Then coincides with the set of power series , whereas coincides with the set of Laurent series .
Given monomial monoids , one may also form the set whose elements are ordered antilexicographically: if there exists an with and for all . The set should naturally be interpreted as (which it is isomorphic to ). The set is a field which contains , and this inclusion is strict if (notice also that ). If is algebraically closed, then is again an algebraically closed field (and again, we have ).
From now on, we will assume that is a monomial group which is generated as a group by its infinitesimal elements. Given a series , a Cartesian representation for is a Laurent series together with monomials such that . Given several series , and Cartesian representations for each of the , we say that these Cartesian representations are compatible if they are of the form for and . In [8, Proposition 3.12] we show that such compatible Cartesian representations always exist.
In [8, Chapter 3], we give constructive proofs of several basic facts about Cartesian representations and based series to be introduced below. These constructive proofs can easily be transformed into algorithms, so we will only state the effective counterparts of the main results. First of all, in order to keep the number of variables in Cartesian representations as low as possible, we may use the following effective variant of [8, Lemma 3.13]:
Lemma
Let be a local community. We will say that is Lbased if admits a Cartesian representation of the form with , and . The set of all such series forms a algebra [8, Proposition 3.14]. If , and are effective, then any gridbased series in is computable. Moreover, we may effectively represent series in by Cartesian representations, and is an effective algebra for this representation.
A Cartesian representation of is said to be faithful if for each dominant monomial of , there exists a dominant monomial of with . We have the following effective counterpart of [8, Proposition 3.19]:
Proposition
Faithful Cartesian representations are a useful technical tool for various computations. They occur for instance in the proof of the following effective counterpart of [8, Proposition 3.20]:
Proposition
Solving power series equations
Assume now that is an effective field with an effective zero test and an algorithm for determining the roots in of polynomials in . Let be an effective local community over and an effective totally ordered monomial group. We notice that a gridbased series in can also be regarded as an ordinary power series in . We are interested in finding all infinitesimal solution of a power series equation
where . The Newton polygon method from [8, Chapter 3] can be generalized in a straightforward way to power series equations instead of polynomial equations and the effective counterpart of [8, Theorem 3.21] becomes:
Theorem
Given with , we may also consider as an element of . Let be the dominant of for this latter representation. The valuation of in is called the Weierstrass degree of . If is algebraically closed, then it can be shown that the number of solutions to the equation in Theorem 4 coincides with the Weierstrass degree, when counting with multiplicities.
Let be an effective field with an effective zero test. We may consider its algebraic closure as an effective field with an effective zero test, when computing non deterministically (we refer to [2] for more details about this technique, which is also called dynamic evaluation).
Let be an effective tribe over with an effective zero test. It is convenient to represent elements of by polynomials , where . The algebraic number is effectively represented using an annihilator and we may always take such that . It is a routine verification that forms again an effective tribe for this representation.
Consider a series , represented as , where is given by an annihilator of degree . Then we notice that we can compute a representation for as a element of . Indeed, whenever for some , then this means that there exists a monomial such that the coefficient of in is a polynomial of non zero degree in . On the other hand, , which means that we can compute an annihilator for of degree . Repeating this reduction a finite number of times, we thus reach the situation in which , so that .
Let still be an effective tribe over with an effective zero test. Given , we recall that is said to have Weierstrass degree in if , but . In that case, the Weierstrass preparation theorem states that there exists unit and a monic polynomial of degree such that . The polynomial is called the Weierstrass polynomial associated to . We claim that and that there exists an algorithm to compute (and therefore the corresponding unit , since is effectively stable under restricted division):
Theorem
Proof. Consider the effective totally ordered monomial group with powers. We have a natural inclusion . Now consider . By theorem 4, we may compute all infinitesimal solutions to the equation in (we recall that there are such solutions, when counting with multiplicities, since is algebraically closed). Now consider
and let be the Weierstrass polynomial associated to . Since also admits the infinitesimal roots when considered as an element of , we have when considering as an element of . It follows that
Assume that has Weierstrass degree in and let . The Weierstrass division theorem states that there exists a quotient and a remainder in with
and . We claim that and once again belong to and that there exists an algorithm to compute them:
Theorem
Proof. Let be the distinct solutions of when considered as an equation in , and let be the multiplicity of each , so that . For each , we compute the polynomials
[1] R.P. Brent and H.T. Kung. Fast algorithms for manipulating formal power series. Journal of the ACM, 25:581–595, 1978.
[2] J. Della Dora, C. Dicrescenzo, and D. Duval. A new method for computing in algebraic number fields. In G. Goos and J. Hartmanis, editors, Eurocal'85 (2), volume 174 of Lect. Notes in Comp. Science, pages 321–326. Springer, 1985.
[3] J. Denef and L. Lipshitz. Ultraproducts and approximation in local rings. Math. Ann., 253:1–28, 1980.
[4] J. Denef and L. Lipshitz. Power series solutions of algebraic differential equations. Math. Ann., 267:213–238, 1984.
[5] J. Denef and L. Lipshitz. Decision problems for differential equations. The Journ. of Symb. Logic, 54(3):941–950, 1989.
[6] L. van den Dries. On the elementary theory of restricted elementary functions. J. Symb. Logic, 53(3):796–808, 1988.
[7] J. van der Hoeven. Relax, but don't be too lazy. JSC, 34:479–542, 2002.
[8] J. van der Hoeven. Transseries and real differential algebra, volume 1888 of Lecture Notes in Mathematics. SpringerVerlag, 2006.
[9] J. van der Hoeven. Computing with Dalgebraic power series. Technical report, HAL, 2014. http://hal.archivesouvertes.fr/.
[10] K. Weierstrass. Mathematische Werke II, Abhandlungen 2, pages 135–142. Mayer und Müller, 1895. Reprinted by Johnson, New York, 1967.