> <\body> <\hide-preamble> >>>>> >>>> >>> \; |||<\author-note> Chen and Fang were partially supported by National Key R&D Programs of China (number 2023YFA1009401), the NSFC grants (number 12271511), and the Strategic Priority Research Program of the Chinese Academy of Sciences (number XDB05102). All authors were also supported by the International Partnership Program of Chinese Academy of Sciences (Grant number 167GJHZ2023001FN). |<\author-affiliation> KLMM, Academy of Mathematics and Systems Science Chinese Academy of Sciences,\ Beijing 100190, China |>>||<\author-affiliation> KLMM, Academy of Mathematics and Systems Science Chinese Academy of Sciences,\ Beijing 100190, China |>>||<\author-affiliation> LIX, CNRS, Institut Polytechnique de Paris Bâtiment Alan Turing, CS35003 1, rue Honoré d'Estienne d'Orves 91120 Palaiseau, France |<\author-note> van der Hoeven has been supported by an ERC-2023-ADG grant for the ODELIX project (number 101142171). |>>|>|<\doc-note> > Consider formal power series ,\,f\\|]>> that are defined as the solutions of asystem of polynomial differential equations together with a sufficient number of initial conditions. Given \,\,F|]>>, several algorithms have been proposed in order to test whether ,\,f|)>=0>. In this paper, we present such an algorithm for the case where ,\,f> are so-called transseries instead of power series. ||> Standard mathematical notation exists for many special functions such as , , , , , >, >, But how to decide whether an expression like -\*\> actually represents the zero function? One popular approach is to rely on differential algebra , by defining as a symbolic solution of the equation =f>. However, this only allows one to define up to a multiplicative constant, which is insufficient to conclude that =\*\>. Another approach is to define as the unique solution of =f> with =1>>. This can be made more precise by restricting our attention to D-algebraic power series. Let > be an effective field. We say that \|]>> is if it satisfies an equation ,\,f>|)>=0> for some differential polynomial ,\,F>|]>\\>>. In that case, is actually uniquely determined by and a sufficient number of initial conditions. Given D-algebraic series ,\,f> and a differential polynomial in ,\,F>>, the test problem>> now consists of deciding whether ,\,f|)>=0>. Many solutions have been proposed for this problem and we refer to for a brief overview of existing approaches. However, one problem with ordinary power series is that they do not form a field. So-called are a far reaching generalization of power series, by closing off |]>> under exponentiation, logarithms, and infinite summation. An example of a transseries at infinity (\>) is <\equation> \+|x>+|x>+\>+3*\+++>+>+>+\. The transseries with real coefficients form a field > that is closed under differentiation, composition and the resolution of many differential equations. A transseries is again said to be if ,\,f>|)>=0> for some \,\,F>|]>\\>. For example, the transseries() is D-algebraic. Given D-algebraic transseries ,\,f> and a differential polynomial in ,\,F>>, our main result is an algorithm for deciding whether ,\,f|)>=0>. In fact, we reduce this problem to the case , but at the same time generalize it to the case where the coefficients of and the differential polynomial with |)>=0> are taken in an effective differential subfield of > for which we already have a zero-test. Asubstantial part of the paper is devoted to recalling required theoretical results about transseries from. From an effective point of view, computations with transseries are most conveniently carried out with respect to a so-called =,\,\|)>>. This allows one to consider general transseries as power series in> with real exponents, and whose coefficients can recursively be expanded with respect to the transbasis ,\,\|)>>. For instance, for \>, the transseries -\|)>> is a series in > with coefficients in|]>|]>>. Along with our survey, we present a precise framework, much in the vein of. Having carried out the necessary preparations, our main algorithm turns out to be a natural extension of the zero-test from for formal power series. Using a theorem from, we were also able to further sharpen the bound on the required expansion order. As an illustration of our algorithm, we will first define the Lambert function as the unique transseries solution to a suitable asymptotic differential equation and then verify that it satisfies the equation *\>=x>. Let > be a totally ordered abelian group. A subset \> is said to be if there exist |\,\,\|\>\\>\\\\\\0|}>> and \\> with <\equation*> S\\*\+\+\*\+\\*\+\+i*\+\\i,\,i\\|}>. Given a field >, consider a formal power series \\>f>*z>> with >\\> and such that the support \\\f>\0|}>> is grid-based. Then we call a (with coefficients in > and exponents in >) and we denote the set of such series by >|]>|]>> or simply by>|]>|]>>. In2.2> it is shown that >|]>|]>> forms a field. It actually forms a valued field for the valuation >|]>|]>\\|}>>> defined by \min supp f> (and \+\>). If \>|]>|]>> is non-zero, then we call >> the of . If > is an ordered field, then so is >|]>|]>>, bysetting 0\f>\0>. In that case, we will write >|]>|]>>> for the subset of strictly positive elements. <\example> We have >|)>\\>|]>|]>> with +\*\>. <\example> If 1/z> is a \Pformal infinitely large variable\Q, then we define >\z>> and >|]>|]>\\>|]>|]>>. Given variables ,\,z> and =,\,\|)>\\>, let >\z>*\*z>>. We totally order > anti-lexicographically via <\equation*> |\\\|\>\|\\\|\>\=\\\\\|)>\\\=\>\\\\=\|)> and define the field of grid-based series in ,\,z> by >;\;z>|]>|]>\\>|]>|]>>. We note that >;\;z>|]>|]>\\>|]>|]> \ >|]>|]>> and this inclusion is strict as soon as1>>: , \>z>*z\\>|]>|]>>|]>|]>\\>;z>|]>|]>>. Note also that +z|)>>\\>;z>|]>|]>> with *+>. We will sometimes consider series ,\,\>f,\,\>*z>*\*z>> in >;\;z>|]>|]>> jointly with respect to all variables ,\,z> and write \\\|}>> for its valuation. On other occasions, we expand \\>f>*z>> as a series in > with coefficients >\\>;\;z>|]>|]>> and write >\\\|}>> for its valuation in >. Given \>|]>|]>>, we will use the following traditional asymptotic notation: <\equation*> |||>|>|g>|>|\v>>|>|>|g>|>|\v>>|||g>|>|=v>>|||g>|>|\v.>>>>> For elements ,\\\\|}>> in the value group (or infinity), we also write =O|)>> if |\|>\n*|\|>>> for some integer 1> and =o|)>> if |\|>\|\|>> for all integers 1>. The following asymptotic relations will also be useful: <\eqnarray*> g>|>|=O|)>>>|g>|>|=o|)>.>>>> Any grid-based series \>|]>|]>> admits a unique <\equation*> f=f>+f>+f>, where >\\0>f>*z>>, >\f>, and >\\0>f>*z>>. We define >|]>|]>>\\>|]>|]>\f=f>|}>> and >|]>|]>>\\>|]>|]>\f=f>|}>>.\ A field > is said to be if we have algorithms for the field operations and zero testing. An ordered field is effective if we also have an algorithm for the ordering. Assume that > is effective and that > is an effective ordered subfield of >. We recursively define a with coefficients in > and exponents in > as an algorithm that takes no input and that either produces zero or a pair |)>\f>> with \> and \>, as well as another lazy power series >>. The pair |)>> actually represents a term >> and we will use this latter notation in the sequel. Writing *z>\f>>, *z>\>|)>>>, *z>\>|)>>|)>>>, >, where the sequence stops whenever >|)>\|)>>> produces zero, we allow coefficients > to be zero, but we require that ,\,\,\|}>> is a grid-based subsetof>. We may thus regard as a grid-based series *z>+c*z>+c*z>+\\\>|]>|]>>. Conversely, a series \>|]>|]>> is said to be if it can be computed as a lazy power series. We write >|]>|]>> for the set of such series. In fact, >|]>|]>> forms a field and the lazy approach allows us to implement the ring operations in an elegant way as follows: given |)>\\\> and non-zero \>|]>|]>> with >=a*z>> and >=b*z>>, we set <\eqnarray*> g|)>>,g|)>>|)>>|>|b|)>*z>,f>\g>|)>>|\=\>>|>,f>\g|)>>|\\\>>|>,f\g>|)>>|\\\>>>>>>>|>|)>*f|)>>,>|)>*f|)>>|)>>|>|+\>,>|)>*f>|)>>>|>,>|)>>|>|+\>,>|)>*g>+f>*g|)>>>>> We also take 0\f>, *f>, etc. Assuming that \0>, we invert as follows <\eqnarray*> |)>>,|)>>|)>>|||)>.>>>> Since any non-zero \>|]>|]>> can be written as >*> with \>>, \>, and \>|]>|]>> with \0>, we may thus compute > as *z>*>. The lazy approach is very convenient as long as we only need a modest number of terms. For high order expansions, the relaxed (or online) approach is more efficient. Assume now that > is an effective field and that > is an effective ordered subfield of>. In the case of iterated series in >;\;z>|]>|]>=\>|]>|]>>, the lazy approach raises the problem of infinite cancellations: assume that we wish to subtract <\equation> -z>-> using the lazy approach. Then the successive terms of the result are *z>, *z>, *z>, >. Due to this infinite cancellation, we never reach the first term > of the result. In order to circumvent this difficulty, assume that we are given an effective subfield> of >;\;z>|]>|]>> such that \>\\\|}>\>. We will call > an if for any \\>;\;z>|]>|]>> with k\n>>, when regarding \>f>*z>> as a series in >;\;z>|]>|]>>|]>|]>>, we have >\> for all \>> and >|]>|]>>. In the example() we may then take \\,z|)>>, after which expansion with respect to > yields <\equation*> -z>->=>->|)>+||)>>+||)>>+\ and the coefficients >->>, |)>>>, |)>>>, > are all in >. In particular, we may detect the infinite cancellation in the first term using the zero test in >. In this paper, we adopted the framework of grid-based series in order to use some of the results from . However, the results from this book and the present paper can be adapted to so called . We say that a subset of > is if is either finite or ,\,\|}>> with \\\\> and \> \=+\>. It was shown by Levi-Civita that the set >|]>|]>> of series \\>f>*z>> with steady support forms a field. An example of such a steady series that is not grid-based is =1>z>. The field of is simply >;\;z>|]>|]>\\>|]>|]> \ >|]>|]>>. In fact, the framework of steady series would have been slightly better for the present paper, since it is the most natural setting for lazy power series expansions. Furthermore, we have seen that a series in >|]>|]> \ >|]>|]>> is not necessarily grid-based, so extra efforts are sometimes required to prove this, whenever this indeed is the case. Even more generally, Hahn showed that the set >|]>|]>> of series \\>f>*z>> with well-ordered support also forms a field. In this setting, we naturally have >|]>|]>=\>|]>|]> \ >|]>|]>>. An example of a well-ordered series that is not steady is z+z+z+\>, which is a natural solution of the equation =z+f|)>>. However, this kind of series is more problematic from an algorithmic point of view, since the order type of the support of \f/> is >. In particular, expressions like -f> give rise to infinite cancellations as in(), but with no easy fix; see also. Let be a formal variable that we think of as being infinitely large. Given \\>, let >\log\|\\>\log> denote the >-fold iterated logarithm. A is a tuple =,\,\|)>>> with the following properties: <\description> =log> x> for some \\>. \exp \>;\;\>|]>|]>>>> for ,n>. \\\log \>. In , we understand that >;\;\>|]>|]>>>> consists of the multiplicative group of formal exponentials >> with \\>;\;\>|]>|]>>> and \0>. Accordingly, in , we have written > for the series > with =\>>. We may always insert further iterated logarithms into > whenever needed. More precisely, the tuple |^>\,\,\,\|)>> with \log+1> x> is again a transbasis. In the extension >;\>;\;\>|]>|]>>>> , can be strengthened to <\with> <\equation> 1\log \\\\log \. <\example> The tuple =,\,\,\|)>\,\+x+x>|)>> forms a transbasis, since >, =\> with \>;x>|]>|]>>>>, and +x+x\\>;x>;x>|]>|]>>>>. <\remark> Let 1> be a positive integer. Then <\equation*> exp |1-x>=\+\+x>*\>>\\>;\+x+\+x|)>*\>|]>|]>, where +x+\+x>|)>> is a transbasis. If is large, then the expression +\+x> becomes very large, which is not convenient. There are various other types of transbasis, for which |1-x>> may directly be included in the transbasis instead of +x+\+x>>. In this paper, we will ignore such \Poptimizations\Q and refer to4.4> for more details on alternative definitions. A is an element of >;\;\>|]>|]>> for some transbasis =,\,\|)>>>.It turns out that the grid-based transseries form a field > (modulo natural when varying >). This is not directly obvious from our, which depends on the underlying transbasis >. Usually, one first defines the field of transseries > in a more conceptual manner and then proves that any transseries can be expanded with respect to a transbasis: see4 and Section4.4>. However, in this paper, we will always manipulate transseries via transbasis, so our more computational \Pdefinition\Q will be more direct and convenient. Grid-based transseries were first considered by Écalle in. For constructions of fields of transseries with well-ordered support, we refer toA> or. Consider a transbasis =,\,\|)>> with =log> x>. Then we have the natural derivation \x*log x*\*log> x*|\ x>> on >|]>|]>>, with f=-\\>\*f>*\>> for all \>|]>|]>>. This derivation extends by induction on to \\>;\;\>|]>|]>>: assuming that we defined > on >;\;\>|]>|]>>, we can in particular compute \/\\\ log \\\>;\;\>|]>|]>>. Now given \\>f>*\>\\>;\;\>|]>|]>>|]>|]>>, we take <\equation*> \ f\\\> f>-\* \|\>*f>|)>*\>\\>;\;\>|]>|]>>|]>|]>. If \>;\;\>|]>|]>>, then it can be shown that f\\>;\;\>|]>|]>>. This is due to the fact that, for a suitable notion of infinite summation, we have <\equation> \ f=-\\>f>** \|\>+\+\* \|\>|)>*\>*\*\>, with f\supp f+supp \|\>+\+supp \|\>>. 2.4 and5.1>.>> Assuming that > x,log-1> x,\,x> all belong to >, it follows that > is also closed under the usual differentiation with respect to . In addition, for ,n>>, we have the derivation \/\ \|)>*\> with \=\>. Given \>, it is shown in5.1> that <\equation> f\g\g\1\\ f\\ g. Applying this to Equation, we get <\equation> \|\>\\\ \|\>. Given \>;\;\>|]>|]>>, the formula() implies f|)>=v f|)>\v>, since /\ \|)>=0>. For any \>, it follows that f|)>\v>. If has dominant monomial >*\*\>> with \0>, this also yields f|)>\0>, whence f\1>. For all \>>, we thus obtain <\equation> f\1\ f|)>\1. Let > be an effective ordered subfield of> and let \>;\;\>|]>|]>> be an ambient field. We call > a if ,\,log \\> and > is effectively closed under >. Differentiation can be implemented in a lazy manner: given a non-zero \>;\;\>|]>|]>> with >=a*\>> (when regarded as a lazy series in >), we maytake <\equation*> f|)>>, f|)>>|)>= a-\*a|)>*\>,\ f>|)>, where a=0> if and a> can be expanded recursively as /\ \|)>*\ a> with respect to > if 1>. We already noted that |^>\,\,\,\|)>> is a transbasis for \log \>. Moreover, |^>\>|)>> is again a differential ambient field for \\*\>. Indeed, \\>\|^>> and the lazy algorithms for the field operations allow us to compute the iterated coefficients of any transseries in the field generated by \\> >. For the rest of this paper, let > be an effective ordered subfield of >, let =,\,\|)>> beatransbasis, and let \>;\;\>|]>|]>>\\\\>;\;\>|]>|]>> be adifferential ambient field. We denote by > the field of grid-based transseries. Consider a linear differential operator *\+\+L\\|]>> with \0>. We define \min |)>,\,v|)>|)>> and \|)>>*\+\+|)>>\\|]>>. Given \\> and >\\>*\*\>>, we write \>>> for the unique differential operator in |]>> with \>>=L>*f|)>> for all \>, and we let \>>\\>*L\>>>. We also denote by >> or >> the integer such that \>>=\>>|)>*\+\+\>>|)>>>*\>>> and \>>|)>>>\0>. <\theorem> <\enumerate-alpha> All transseries solutions of the equation in > are actually in |]>>. If \|]>> is a solution of with dominant monomial |)>*\>>, then we have \>>. Conversely, any \\> and \>> give rise to such a solution. Given \|]>>, all solutions of in > are actually in |]>>. Moreover, there exists a unique solution to in |]>> with the property that, for any \\> and \>>, the coefficient of |)>*\>> in vanishes. <\proof> The statements are rephrasings of 7.17> and its corollaries. In(), the unique solution is called the of and we denote it by L g>. The operator :\|]>\\|]>> is linear and even preserves infinite summation7.4>. Given |]>>, let \\\L g\\|}>>. We say that > is if :\\\> for every |]>>> and if we have an algorithm to compute >. In order to make > effectively linearly closed, we need to consider sequences of extensions \> f|)>> by distinguished solutions of linear differential equations. The main difficulty concerns the design of azero-test on such an extension > f|)>>. In this subsection, we will start by showing how to expand distinguished solutions with respect to >, assuming that \\>;\;\>|]>|]>>> is effectively linearly closed. So consider a linear differential operator \+\+L\|]>> with \0>. Note that we regard as an operator in > instead of >, for convenience. We define \min |)>,\,v|)>|)>>, where > stands for the valuation with respect to>.\ Now let |]>>. If , then g=0>, so assume that 0> and let >\\*\>> be the first term of its expansion in >. In order to compute the expansion of g> in >, we may assume without loss of generality that =0> and decompose with |]>=|]>> and |]>>> with \0>. We may now expand g> in a lazy manner as follows: <\equation> g|)>>, g|)>>|)>\*\>,L>-T*\>|)>|)>|)>,|\\H\>> \|\>>.> Here we note that \>>>\|]>>, whence \> using our assumption that > is effectively linearly closed. We extend the classical notion of indicial polynomials to linear differential operators with transseries coefficients. Let \+\+L\|]>> with \0> still be a linear differential operator in >. We define the of by \|)>>*+\+|)>>\>. (If , then =\|)>>, but this does not hold in general.) <\proposition> Let \\> and \+\+L\|]>> with \0>. If >\0>, then > must be a root of the indicial polynomial >.\ <\proof> First note that \>>=\>*L\>>> can be obtained from by substituting -\> for>. In particular, \>>>=\|)>>. Then writing \>>=*\+\++o\>>|)>>|)>>, we have =\|)>>. Applying to > gives \/\\\ \/\=1> for ,>. Therefore, \>>=\>**\+\+\>*+o\>>|)>>|)>>. Then rewrite \>>\>=>*\+\+>>> in >. Applying to > yields \/\\\ \/\> and thus >=\>*+o\>>|)>>|)>>. Hence once >\0>, we must have >*=\>*\|)>=0>. \ Combining Theorem and Proposition, if > and > are two distinct solutions to in |]>>, then -f|)>>> must be a root of the indicial polynomial >. Consider a differential polynomial \> F|]>> of order and total degree in,\ F>>. We may also write ,\,i\\>P,\,i>*F>*\* F|)>>> with ,\,i>\\>>. We define =min,\,i\\> v,\,i>|)>> and =,\,i\\>,\,i>|)>>*F>*\* F|)>>>. We may also decompose >+\+P>>, where >> regroups all homogeneous terms of total degree in ,\ F>, for ,d>. Given \\>, we write>> and \>> for the unique differential polynomial in > F|]>> with >=P+f|)>>> and \>=P*f|)>> for all \>, respectively. From(), we get <\equation> \\1\P>=P+o. In other words, if \1>, then >-P|)>\v>, so in particular >>=D>. If >> is homogeneous of degree and \0>, then one also has <\equation> v\>|)>=v+d*v|)>. For details about these elementary definitions and properties, see . The equation <\equation> P=0,f\1 is said to be if =v>|)>\v>|)>>. More generally, if \\>, then <\equation> P=0,f\\> is said to be if \>>=0,\1> is quasi-linear8.5>. If \1> and() is quasi-linear, then so is the equation >|)>=0,\1>, by(). Consequently, if \\>> and() is quasi-linear, then so is >|)>=0,\\>>. <\example> Let =>>|)>>, \\|)>>, and <\equation*> P\>+->+>|)>*\ F+>|)>*F+ F|x>+F\> F|]>. The equation =0>, 1> is quasi-linear, since =v>|)>=\v>|)>=>. Assume that() has a solution \> and let \|]>> be such that |)>>>. Then the solution is said to be if>=0> for all \\> with >\0>. <\theorem> Any quasi-linear differential equation )> has a unique distinguished solution in |^>=\|^>>;\;|^>>|]>|]>>, where |^>=|^>,\,|^>|)>= \,\,log \,\,\,\|)>>. The uniqueness persists when replacing |^>> by an even larger transbasis. <\proof> This is a rephrasing of 8.21>. <\remark> With the above notation, given another solution > of() in|^>>, the difference \-f> satisfies the quasi-linear equation |)>=0,\\\>>. Then |)>>\0>> since otherwise |)>=P|)>\L \\0>. By Proposition, the valuation |)>> must be a root of the indicial polynomial of, when regarding as an operator in >. This remark even goes through for complex solutions \|^>|]>> of(). Consider a normalized quasi-linear differential equation(), where > F|]>> and=0>. Assume that > and > have been extended such that the distinguished solution of() lies in >. The aim of this subsection is to compute the expansion \>f>*\>> of with respect to >. We first decompose , where > F|]>> and > F|]>> is such that \min,\,i> v,\,i>|)>\0>. It is readily checked that \\>;\;\>|]>|]>> is the distinguished solution of the equation |)>=0,\\1>. We will assume that we already know how to compute this solution > and that \>. As in Section, we will also assume that > is effectively linearly closed. Now consider \P>> and decompose it as \L F-g-R>, where |]>>, > with \0> and > F|]>> with >|)>\0> and \0>. Note that we now write and with respect to > instead of >, which does not change their valuation with respect to >. We already saw in Section how to compute >. This allows us to lazily compute =f-f> using the formula <\equation*> =L|)>|)>. The dependency of the right-hand side on > is legit in the lazy expansion paradigm, aslong as the coefficient of >> in |)>|)>> only depends on coefficients of >> in > with \\>. By construction, this is the case here. <\example> Following from Example, let us compute the expansion of the distinguished solution to the quasi-linear equation =0>, 1>. Decomposing >, we have *\ F+F+x*F*\ F+F>. The distinguished solution of =0,f\1>> is =0>>, so =P>=P> and \0>. We now write <\equation*> =*\++\|)>*\ F+|)>*F+F*\ F+F with respect to > and decompose it as =L F-g-R>, where +1>, *\> and -*\|)>*\ F+x*\*F-F*\ F-F>.\ Then we compute using |)>>, where =g+R>. By, we have =v|)>>. Combining |)>\v>, we have =v=2> and >=g>=\*\> with =1-x>. Decompose +> with =\+1> and =0>. Then we have \\> \=-1|)> \=x>. Therefore, <\equation*> \|)>>, \|)>>|)>=,L|~>|)>|)>,||~>\R|\>>.> Hence the first term of is >. Repeating this process, we obtain <\equation*> |~>|)>>, |~>|)>>|)>=|2>-x|)>*\,L|~>|~>|)>|)>,||~>|~>\|~>>|\>>,> <\equation*> |~>|~>|)>>, |~>|~>|)>>|)>=|3>-|2>+x|)>*\,L|~>|~>|~>|)>|)>,||~>|~>|~>\|~>|~>>|\>>,> which leads to the expansion <\equation*> U=x*\+|2>-x|)>*\+|3>-|2>+x|)>*\+\. We first recall the basic notion of Newton degree and several related properties. Consider the extension <\equation*> |~>=|~>,\,|~>|)>= \,\,log \,\,\,\|)> of > with new logarithms. Let <\equation*> |~>\\|~>>;\;|~>>|]>|]> with derivations |~>> with |~> |~>=|~>> for ,n+s>. Then any \> F|]>> can be rewritten as an element \|~>|~>> F|]>>, which also corresponds to the -fold upward shifting from8.2.3>; see also293>. By and its subsequent remark, there exist a unique polynomial \> and integer \\> such that >=Q\|~> F|)>>> for all sufficiently large . We call =Q\ F|)>>> the for . For a general monomial >> , the of the asymptotic differential equation <\equation> P=0,f\\> is defined to be the largest possible degree of \>>>> for all \ \ >such that \\>. In fact, the equation is quasi-linear if and only if its Newton degree is one. The following theorem shows that Newton degree plays a crucial role in determining a lower bound on the number of the solutions to in |]>>. <\theorem> If the asymptotic algebraic differential equation is of Newton degree , then)> has at least solutions in |~>|]>> when counting with multiplicities, provided that is sufficiently large. Note that we can always assume that >=1> in the equation by replacing with\>>.> In the sequel, we will therefore only consider the equation <\equation> P=0,f\1. We may then use the following simpler criterion for the existence of solutions: <\theorem> Let \> F|]>> be such that |)>>=0>. Then the asymptotic differential equation has a solution in |~>|]>>, provided that is sufficiently large. To show Theorem, it is sufficient to prove the following lemma. <\lemma> Let \> F|]>>. Then |)>>=0> if and only if the Newton degree of the equation is non-zero. <\proof> If |)>>\0>, then() implies that() cannot have any solutions in |]>>. Theorem then implies that the Newton degree of() must vanish. Conversely, assume that |)>>=0> and let \|~>|~>> F|]>> be -fold upward shifting of as above. Let > and|~>> stand for the dominant monomials of and >, respectively. Since =\*|~>> for some invertible > with \\>, one may verify that /|~>\\>. Since |)>>=0>, we have >\\*\>>> for some \0>. Consequently, >=P>\|~>*\/2>>, whence >|)>>=0>. Taking sufficiently large such that >\\*|~> F|)>>>, it follows that >=deg N\0>. At first sight, it may seem that the mere resolution of quasi-linear differential equations is far off from solving general algebraic differential equations. But in fact, it is key the to the resolution of more general equations, due to the following consequence of8.7>>: <\theorem> Let > be a differential subfield of > for the derivation /\ x:f\f>, in which any equation =\*f> or =\/\> with \> has a non-zero solution in >. Assume also that every quasi-linear differential equation with coefficients in > has a solution in >. Then any root in > of a differential polynomial in > F|]>> must be in >. The equations =\*f> and =\/\> have >> and +c> as their general solutions, so in order to apply the theorem, it is important that we know how to compute exponentials and logarithms of elements in > and >>, respectively, while extending> if necessary. For this, we will use the same technique as in, but we actually only need to compute exponentials and logarithms up to constant factors. Moreover, due to the second condition in the theorem, we will assume that we know how to solve quasi-linear equations. Given \> with =c*\>*\*\>*|)>> with 0> and \1>, we have <\equation*> log \=-\*log \-\-\*log \+log c+log |)>. We have seen at the end of Section how to extend > with > if \0>, after which *log \-\-\*log \\>. If 1>, then this may require the extension of the constant field > with , but we may always assume if we just wish to integrate/\>. Finally, the function log |)>> is the distinguished (and actually unique) solution of the quasi-linear differential equation =\/|)>,g\1>. Let \>. As long as \log \> for some , we may write =-\*log \+|~>> and continue with |~>> in the role of >. This leads to a decomposition <\equation*> \=-\*log \-\-\*log \+\, where ,\,\\>, \>, and either and \log \>, or k\n> and \\\log \>, or and \\>. If \\>\0>, then similar arguments as in Section show that |^>\,\,\,\>|\|>>,\,\,\|)>> is again a transbasis and |^>\>|\|>>|)>>|)>> a differential ambient field that contains >|\|>>>. After this extension (if necessary), wehave <\equation*> \>=\>>*>|\|>>|)>1>*\>*\*\>*\>>. If >=0>, then this may require the extension of the constant field > with >>>, but we may assume >=0> if we just wish to compute a non-zero solution of=\*f>. We have >>=1+g>, where is the distinguished (and actually unique) solution of the quasi-linear equation =\>*,g\1>. <\example> Following Example, we will expand >> with =\*U+\-x\\|)>>. First decompose > as =-x+\>+\>>, where >=\> and >=\*U>. Then extend the transbasis > to ,\>>|)>>. For >>>, consider the distinguished solution of the quasi-linear equation =0>, 1>, where <\equation*> \\\**\ U|)>*-*\ F\> F|]>. Then >>-1=V=1+x*\+(x\x)*\+-*x+x|)>*\+\> and >=\*\>*>. Consider the admissible ranking > on > F> with F\\> F> whenever j>. The of a differential polynomial \> F|]>\\> is the highest variable F> occurring in when regarding as a polynomial in F,\>. We will denote it by >. Considering as a polynomial in >, the leading coefficient > is called the of and = P/\ \>> its ; we also define \I*S>. If has degree in >, then the pair ,d|)>> is called the of and such pairs are ordered lexicographically. We understand that -\> for polynomials \>. Given ,\,Q\\> F|]>\\>, we say that is with respect to ,\,Q>> if there exists an such that \\\> \>> or =\=\>> and > P\deg> Q>. The process of provides us with a relation of the form <\eqnarray*> >>*\*I>>*S>>*\*S>>*P>|| Q+\+\*Q+R,>>>> where ,\,\,\,\,\\\>, ,\,\\\> F|]>|]>>, \> F|]>> and where is reduced with respect to ,\,Q>. We will denote ,\,Q|)>>. we are given a grid-based transseries \> such that 1> and a differential polynomial \> F|]>>. Let \\|]>> be such that F=|)>>>. Note that we have \0> if \0>. We first present a criterion for the existence of a root of that is sufficiently close to . <\with|color|black> <\proposition> Let \> F|]>\\> and \> be such that \0> and 1>. Let \0>. If |)>\v|)>+\>, then has a root> in \|)>>;\;|)>>;\>;\;\>|]>|]>> with -f|)>\\>, for some \>. <\proof> Let \v|)>-|)>+\|)>\0> and |)>\-\/2>>>. We have |)>=v|)>>|)>> and |)>=v|)>>|)>>. Using(), we now get >|)>\v>|)>\v>. Hence |)>>=0>, so has a root > in \|)>>;\;|)>>;\>;\;\>|]>|]>> with \1> and \>, by Theorem. Then =f+\*\-\/2>> is as required. Now assume that =0,f\1> is quasi-linear and let be a solution of it. Let > be the indicial polynomial of >, considered as an operator with respect to >. We define > to be the largest root of > in >. If no such root exists, then we set \v>. Let us show now that there always exists a threshold \v> in > such that for any \> and any > in \|)>>;\;|)>>;\>;\;\>|]>|]>> with |)>=0> and -f|)>\\>, we have =f>. The smallest such > will be denoted by > and we call it the of at .\ <\proposition> Let \> F|]>\\> such that =0,f\1> is quasi-linear. Assume that \> is a solution of this equation. Then <\equation*> \\max,Z|)>. <\proof> Consider a root \\ \|)>>;\;|)>>;\>;\;\>|]>|]>> of with \1> and \f>. Then Remark implies that -f|)>> is a root of >. Consequently \max,Z|)>>. Consider a quasi-linear differential equation =0,f\1> with > F|]>> and assume that its distinguished solution belongs to >. Given ||Q,\,Q|\>|\>\> F|]>>, we will now present an algorithm to check whether ,\,Q> simultaneously vanish at . By induction, we suppose that azero test on \>;\;\>|]>|]>\|)>> F|)>> has been given. In particular, one can test whether the coefficients of with respect to > are zero and thus compute the valuation of in >. <\named-specified-algorithm|ZeroTest,\,Q|)>>> : ,\,Q\> F|]>\>, ordered by non-decreasing Ritt rank if =\=Q=0> and otherwise <|named-specified-algorithm> <\listing> If Q\> then return If |)>> then return ,Q,\,Q|)>> If |)>> then return ,Q,\,Q|)>> If J\,\,Q,P|}>,J rem Q\0> then return ,\,Q|)>> Let \max,v|)>,Z,v|)>,v|)>|)>> Return the result of the test |)>\\+v|)>> <\proof> In steps 2, 3, and 4, the Ritt rank of the first argument of > always strictly decreases; this proves the termination of the algorithm. Furthermore, if one of the tests in steps 2, 3, or 4 succeeds, then the algorithm is clearly correct. In step 1, note that we assumed that \0> as an element of > F|]>>. So if \>, then =Q\0>. Assume now that we reach step 5. By construction, this means that \0> and for all ,\,Q,P|}>>. In particular, Ritt reduction of by yields arelation <\eqnarray*> *S*P>||*Q+\+U*\ Q,>>>> where \> and ,\,U\\> F|]>>. If |)>\\+v|)>>, then we clearly have \0>, so assume that |)>\\+v|)>>. Applying Proposition, we obtain a grid-based transseries \\ \|)>>;\;|)>>;\>;\;\>|]>|]>> such that |)>=0> and -f|)>\\>, for some \>. Using(), it follows that <\equation> v>|)>=v|)>\\, <\equation> v|)>|)>=v|)>\\v|)>|)>=v|)>\\. Now implies >=\> and thus >=Z\\>. From, we in particular get |)>\0> and |)>\0>. Hence evaluating at > yields |)>=0>. Applying Proposition to >, we obtain >\\>. Since -f|)>\\>, we conclude that =f>. From =0>, Ritt reduction of by also yields =0> for all ,\,Q|}>>. <\theorem> Let \>;\;\>|]>|]>\\> be a differential ambient field (which comes with azero test, by assumption). Let > F|]>\> be a differential polynomial. If =0,f\1> is a quasi-linear equation with a distinguished solution >;\;\>|]>|]>>, then > f|)>\>;\;\>|]>|]>> is again a differential ambient field. <\proof> Our zero test on > f|]>> trivially extends to the quotient field > f|)>> since afraction vanishes if and only if its numerator does. We may use the algorithms from Sections, , and to compute expansions of elements in > f|)>>. function> Following from Examples, and, consider the distinguished transseries solution =U> of=0>, 1> and let <\equation*> W\log x\U+log x-log log x. We will use to show that > satisfies <\equation*> W*\>=x, i.e., > is a real branch of the function> at infinity. To this end, it is enough to verify that\ <\equation> *U+\-x|)>*\*U+\-x>=\>. In Example, we computed *U+\-x>=\*\>*>. Then the equality is equivalent to =0>, where\ <\equation*> Q\|)>*-1\> F|]>. Now we apply algorithm to >, and over >. Since =S=U+1-x*\>, we have |)>=v|)>=0> and thus the algorithm proceeds to step4. Ritt reduction yields <\eqnarray*> || \>||*I*\ Q+\*P Q+\*P.>>>> Since is a root of , we obtain rem Q=0>, leading the algorithm to step 5. Writing ,V> F=\**\ U|)>*F-x*\ F=\* U|)>*F-\ F>, we have ,V>|)>=0>, ,V>=N>>, and thus ,V>=0>. Hence, we take \1>. Since F=I*F>, we only need to test whether |)>\1> in the final step 6: <\equation*> Q=+O|)>|)>*+O*\|)>|)>-1=O*\|)>. As a result, we finally obtain that is a root of and thus show that is arealbranch of the Lambert function. <\bibliography|bib|tm-plain|> <\bib-list|27> M.Aschenbrenner, L.vanden DriesJ.vander Hoeven. . 195Annals of Mathematics studies. Princeton University Press, 2017. F.Boulier. . , University of Lille I, 1994. R.M.Corless, G.H.Gonnet, D.E.G.Hare, D.J.JeffreyD.E.Knuth. On the Lambert function. , 5(4):329\U359, 1996. B.I.DahnP.Göring. Notes on exponential-logarithmic terms. , 127:45\U50, 1986. J.DenefL.Lipshitz. Power series solutions of algebraic differential equations. , 267:213\U238, 1984. J.DenefL.Lipshitz. Decision problems for differential equations. , 54(3):941\U950, 1989. J.Écalle. . Hermann, collection: Actualités mathématiques, 1992. K.O.GeddesG.H.Gonnet. A new algorithm for computing symbolic limits using hierarchical series. , 358, 490\U495. Springer, 1988. J.vander Hoeven. Outils effectifs en asymptotique et applications. LIX/RR/94/09, LIX, École polytechnique, France, 1994. J.vander Hoeven. . , École polytechnique, Palaiseau, France, 1997. J.vander Hoeven. Complex transseries solutions to algebraic differential equations. 2001-34, Univ. d'Orsay, 2001. J.vander Hoeven. A new zero-test for formal power series. Teo Mora, , 117\U122. Lille, France, July 2002. J.vander Hoeven. Relax, but don't be too lazy. , 34:479\U542, 2002. J.vander Hoeven. , 1888. Springer-Verlag, 2006. J.vander Hoeven. Computing with D-algebraic power series. , 30(1):17\U49, 2019. J.vander Hoeven. . Scypress, 2020. J.vander HoevenJ.R.Shackell. Complexity bounds for zero-test algorithms. , 41:1004\U1020, 2006. E.L.Ince. . Longmans, Green and Co., 1926. Reprinted by Dover in 1944 and 1956. A.G.Khovanskii. , 88. AMS, Providence RI, 1991. E.R.Kolchin. . Academic Press, New York, 1973. T.Levi-Civita. Sugli infiniti ed infinitesimi attuali quali elimenti analitici. , 7:1765\U1815, 1893. A.Péladan-Germa. . , Gage, École Polytechnique, Palaiseau, France, 1997. D.Richardson, B.Salvy, J.ShackellJ.vander Hoeven. Expansions of exp-log functions. , 309\U313. Zürich, Switzerland, July 1996. R.H.Risch. Algebraic properties of elementary functions in analysis. , 4(101):743\U759, 1975. J.F.Ritt. . Amer. Math. Soc., New York, 1950. J.Shackell. A differential-equations approach to functional equivalence. , 7\U10. Portland, Oregon, ACM, New York, 1989. ACM Press. J.Shackell. Zero equivalence in function fields defined by differential equations. , 336(1):151\U172, 1993. <\initial> <\collection> <\attachments> <\collection> <\associate|bib-bibliography> <\db-entry|+byKiFsUoTc7rBN|book|TeXmacs:vdH:book> <|db-entry> > <\db-entry|+qYhUkmR1lNMNv8K|book|Ritt50> <|db-entry> > <\db-entry|+qYhUkmR1lNMNv3I|book|Kol73> <|db-entry> > <\db-entry|+qYhUkmR1lNMNuvt|phdthesis|Boul94> <|db-entry> > <\db-entry|+qYhUkmR1lNMNv8I|article|Ris75> <|db-entry> > <\db-entry|+qYhUkmR1lNMNuy5|article|DL84> <|db-entry> L. > <\db-entry|+qYhUkmR1lNMNuy6|article|DL89> <|db-entry> L. > <\db-entry|+6WngoxZOt05dLD|book|Khov91> <|db-entry> > <\db-entry|+6WngoxZOt05dLI|inproceedings|Sh89> <|db-entry> > <\db-entry|+6WngoxZOt05dLJ|article|Sh93> <|db-entry> > <\db-entry|+qYhUkmR1lNMNv7D|phdthesis|Pel:phd> <|db-entry> > <\db-entry|+qYhUkmR1lNMNvCY|article|vdH:zerotest> <|db-entry> J. R. > <\db-entry|+qYhUkmR1lNMNvEF|article|vdH:dalg> <|db-entry> > <\db-entry|+qYhUkmR1lNMNvCb|inproceedings|vdH:issac02> <|db-entry> > > <\db-entry|+qYhUkmR1lNMNuxu|article|DG86> <|db-entry> P. > <\db-entry|+qYhUkmR1lNMNv07|inproceedings|GeGo88> <|db-entry> G. H. > <\db-entry|+qYhUkmR1lNMNuyd|book|Ec92> <|db-entry> > <\db-entry|+qYhUkmR1lNMNvCq|book|vdH:ln> <|db-entry> > <\db-entry|+qYhUkmR1lNMNvCS|techreport|vdH:osc> <|db-entry> > <\db-entry|+qYhUkmR1lNMNvEe|book|vdH:mt> <|db-entry> L. van den J. van der > <\db-entry|+haC4GcdToVz5G6|inproceedings|vdH:issac96> <|db-entry> B. J. J. van der > <\db-entry|+qYhUkmR1lNMNvCC|phdthesis|vdH:phd> <|db-entry> > <\db-entry|+UxLEI9PJlFl3Ur|article|vdH:relax> <|db-entry> > <\db-entry|+qYhUkmR1lNMNv45|article|LC1893> <|db-entry> > <\db-entry|+qYhUkmR1lNMNvBw|techreport|vdH:94a> <|db-entry> > <\db-entry|+qYhUkmR1lNMNv2K|book|Ince26> <|db-entry> > <\db-entry|+uqELzhk132jYmJ0|article|CGHJK1996> <|db-entry> G. H. D. E. G. D. J. D. E. > function> > <\references> <\collection> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > <\auxiliary> <\collection> <\associate|bib> TeXmacs:vdH:book Ritt50 Kol73 Boul94 Ris75 DL84 DL89 Khov91 Sh89 Sh93 Pel:phd vdH:zerotest vdH:dalg vdH:issac02 DG86 GeGo88 Ec92 vdH:ln vdH:ln vdH:osc vdH:mt vdH:issac96 vdH:phd vdH:dalg vdH:osc vdH:ln vdH:relax vdH:ln LC1893 vdH:94a vdH:ln vdH:ln Ec92 vdH:mt DG86 vdH:phd vdH:ln vdH:ln vdH:ln vdH:ln Ince26 vdH:ln vdH:ln vdH:ln vdH:ln vdH:mt vdH:ln vdH:osc vdH:ln vdH:issac96 CGHJK1996 <\associate|toc> |math-font-series||1Introduction> |.>>>>|> |math-font-series||2Generalized power series> |.>>>>|> |2.1Grid-based series |.>>>>|> > |2.2Iterated series |.>>>>|> > |2.3Asymptotic relations and the canonical decomposition of a series |.>>>>|> > |2.4Computable series |.>>>>|> > |2.5Computable iterated series |.>>>>|> > |2.6Beyond grid-based series |.>>>>|> > |math-font-series||3Transseries> |.>>>>|> |3.1Transbases |.>>>>|> > |3.2Grid-based transseries |.>>>>|> > |3.3Differentiation of transseries |.>>>>|> > |3.4Computable transseries |.>>>>|> > |math-font-series||4Linear differential equations> |.>>>>|> |4.1Linear differential equations over transseries |.>>>>|> > |4.2Computing distinguished solutions |.>>>>|> > |4.3Indicial polynomials |.>>>>|> > |math-font-series||5Quasi-linear differential equations> |.>>>>|> |5.1Differential equations over transseries |.>>>>|> > |5.2Quasi-linear differential equations |.>>>>|> > |5.3Computing distinguished solutions |.>>>>|> > |math-font-series||6General algebraic differential equations> |.>>>>|> |6.1Existence of solutions |.>>>>|> > |6.2From general equations to quasi-linear equations |.>>>>|> > |6.2.1Computing logarithms |.>>>>|> > |6.2.2Computing exponentials |.>>>>|> > |math-font-series||7The new algorithm for zero testing> |.>>>>|> |7.1Ritt reduction |.>>>>|> > |7.2Root separation bounds |.>>>>|> > |7.3The main algorithm |.>>>>|> > |7.4A worked example: the Lambert |W> function |.>>>>|> > |math-font-series||Bibliography> |.>>>>|>