> <\body> ||<\author-address> de Mathématiques ( 425) Université Paris-Sud 91405 Orsay Cedex France >|> <\abstract> It is well known that the operation of integration may lead to divergent formal expansions like \>=\>*(\z>+\2*z>+2*\3*z>+6*\4*z>+\)> as soon as one leaves the area of formal power series for the area of formal transseries. On the other hand, from the analytic point of view, the operation of integration is usually ``regularizing'', in the sense that it improves convergence rather than destroying it. For this reason, it is natural to consider so called ``integral transseries'' which are similar to usual transseries except that we are allowed to recursively keep integrals in the expansions. Integral transseries come with a natural notion of ``combinatorial convergence'', which is preserved under the usual operations on transseries, as well as integration. In this paper, we lay the formal foundations for this calculus. \>>\>>> A natural way to solve a differential equation like f=\>+f> for large 1> is to rewrite it in integral form f= \>+ f> and recursively replace the left-hand side by the right-hand side. This yields a convergent expansion for as an ``integral transseries'' f=\>+ \>+2* \>* \>+\.> More generally such infinite sums can occur recursively in the exponents. The aim of this paper is to develop a systematic calculus for integral transseries. We will work in the context of complex grid-based transseries, which is briefly recalled in section . An ``integral transseries'' is an infinite linear combination of ``integral transmonomials'', which are finite expressions formed from certain ``elementary monomials'' \ using multiplication and integration. The elementary monomials are exponentials of integrals of ``simpler'' integral transseries. The representation of a complex transseries by an integral transseries is far from being unique, which provides a lot of flexibility for the computation with integral transseries. A major aim of the theory is to lift the usual operations on complex transseries, such as differentiation, truncation, division, , to their representations by integral transseries. Moreover, we want these operations to preserve ``combinatorial convergence''. For instance, even though the transseries represented by in () is not convergent, the expansion is said to be combinatorially convergent as an integral transseries. Indeed, the main reason of being for integral transseries is that they allow us to maintain a formal notion of convergence during our computations, there where the represented transseries themselves are divergent. Before introducing integral transseries in their full generality, we first introduce the simpler notion of integral series in sections , and . A first technical difficulty is to impose suitable conditions on the supports of integral series. Since we work in the grid-based context, we need a suitable analogue of the grid-based finiteness property. This involves two ingredients: finite generation (regular language specifications in section ) and an asymptotic descent condition (the cycle condition in section), which states roughly speaking that later terms in the expansion are smaller and smaller from an asymptotic point of view. Moreover, because integral monomials represent series and not merely monomials, we need this descent condition to be sufficiently uniform. This motivates the introduction of the span of an integral series in section and frameworks in section . These notions allow to obtain quick and rough bounds for the support of the transseries represented by an integral series or monomial. In order to lift computations with classical complex transseries to integral transseries, the key step is a mechanism for rewriting integral transseries in a form with a clear asymptotically dominant part. For instance, in order to compute a fraction <\equation*> \>)-4* \>> it is necessary to first expand the denominator in such a way that it can be inverted. Using integration by parts, one has <\eqnarray*> \>)>||>|\>+>|\>+>|\>*>|\>+>|\>>>| \>>||>|\>+>|2*\>+ >|\>- >|2*\>>>>> whence <\eqnarray*> \>)-4* \>>||>|2*\>*1+\>>|>|||\>>*>|\>+|\>>>|\>-|\>> >|\>+|\>> >|\>>>>> Now > admits a natural ``integral transseries'' inverse +\+\>. A more systematic procedure for obtaining expansions like () and () will be the object of sections and . In section , we prepare this material by introducing the integral transseries analogue of transbases and differentiation. Putting all techniques together, we finally construct the field of integral transseries in section . Integral transseries can be seen as a natural generalization of Écalle's arborified moulds . One advantage of the approach in this paper is that a systematic calculus for integral transseries avoids the process of ``arborification''. Even though the latter technique also has a large degree of generality, our technique works in a context as general as that of complex transseries, for which a satisfactory theory of accelero-summation is not even known yet (but under development). Furthermore, with more work, we think that our technique may be generalized so as to include other types of operators, like infinite summation, and parameterized transseries. Unfortunately, we also have to pay the price of a certain technicity in sections and. It remains an interesting question how far the ideas in this paper may be further simplified. A few ideas in this direction will be mentioned in the conclusion. We plan to further develop the topic of integral transseries and its link with the theory of accelero-summation in a forthcoming paper. The field of complex grid-based transseries has been constructed and studied in . Below we will quickly present a classical variant of the construction. We first endow > with the following total ordering: <\equation*> x+y*\\x+y*\\x\x\(x=x\y\y). This gives > the structure of a totally ordered >-vector space, although the ordering is not compatible with the multiplication. <\remark> In fact, it is possible to consider more general orderings on > and vary the orderings during the construction . However, in this paper, we will assume the above ordering, for simplicity. Now consider the totally ordered monomial groups > and corresponding fields =\>>, which are inductively defined by <\eqnarray*> >||>|>||*z)\exp \>>>>> We call <\equation*> \=\\\\\ the field of purely exponential complex transseries. Setting <\equation*> \=\\\\\, we have =\>>, because of the grid-based property. For each \>, let \log=\\log>> denote the field obtained from > when replacing by z=log |n\> log z>. We call <\equation*> \=\\\\log\\\log\\ the field of complex transseries. Setting <\equation*> \=\\\\log\\\log\\, we again have =\>>, because of the grid-based property. <\remark> In the above construction, we essentially close the field >>> under exponentiation and next under logarithm. In , we proceed exactly the other way around. We recursively define a strong derivation on >, by setting <\equation*> (\)=f*\ for monomials \\> and extending by strong linearity. Next, we set <\equation*> (f\log)=*log z>*f\log for \\log>. It is classical to verify that > is a strong derivation which satisfies <\equation> f\g\g\1\f\g. For all \>>, the logarithmic derivative of is denoted by >=f/f>. Using general strongly linear algebra, it follows from () that > admits a distinguished strong right inverse >, f)=0> for all . More specifically, one has <\equation> \=>>+\>|(\>)>+\>-\\'>|(\>)>+\*\ for all transmonomials \\\{1}>. It can also be checked that \{1}>> and [z]>> are stable under integration for all (and similarly for \ \{1}>> and [z]>>). In particular, we have <\equation*> \=exp \> in the inductive construction of >. In this paper, the flatness relations >>, >>, >> and >> are defined in an >-expo-linear way: <\eqnarray*> \\>|>|\\\>:\\\\>:\>\\>>>|\\>|>|\\\>:\\\\>:\>\\>>>|\\>|>|\\\\>>|\\>|>||\>>\\>>>> For instance, \*z>\\> and )*z>\\>. A subset > of > is said to be if \\\\\\\\\\> for all ,\\\>. We denote by >>> the set of all flat subsets. We have ,{1}\>>> and >>> is stable under arbitrary intersections. <\remark> The above definitions can be generalized to the case of more general strong algebras >>, where > is a partially ordered monomial group which admits powers in a totally ordered ring with 0>. In that case, we set <\eqnarray*> \\>|>|\\R>:\\\R>:\>\\>>>|\\>|>|\\R>:\\\R>:\>\\>>>>> The definitions remain valid if > is only a partially ordered monomial monoid which can be embedded into a partially ordered group. Given \\>, we define the flattened dominance and neglection relations >>>, >>>, >>>> and >>>> by <\eqnarray*> \>\>|>|\\\:\\\*\>>|\>\>|>|\\\:\\\*\>>|\>>\>|>|\\\:\\\*\>>|\>>\>|>|\\\:\\\*\>>>> We also define the derived relations >>>, >>>, >>>> and >>>> by <\eqnarray*> \>\>|>|\>\\>\>>|\>\>|>|-\\>\>>|\>>\>|>|\>>\\>>\>>|\>>\>|>|-\\>>\>>>> Notice that \>\\\/\\\> and \>>\\\/\\\> The differentiation > and the distinguished integration > on > satisfy <\eqnarray*> >|>>>>|>>|\>|>>>>|>>>> for all \\\{1}> (the first relation is easily checked and the second one follows from relation follows from ()). We say that > and > are . <\remark> In , the flatness relations were defined in a >-expo-linear way using <\eqnarray*> \\>|>|\log \>>|\\>|>|\log \>>>> Equivalently, we may define them using <\eqnarray*> \\>|>|>\\>>>|\\>|>|>\\>>>>> When replacing >> and >> by the relations >>> and >>> defined by <\eqnarray*> >g>|>|\\\>:\\\\>:\*f\\*g>>|>g>|>|\\\>:\\\\>:\*f\\*g>>>> it is also possible to recover the >-expo-linear case. Classically, a transbasis is a tuple =(\,\,\)> of transseries with \\\\> and such that <\description> =exp z> for some \>. \\;\;\>> for all 1>. The integer is called the of the transbasis and > is said to be a transbasis if . We recall that the flatness relations >> and >> were defined in an >-expo-linear way, whence ;\;\>=\>;\;\>>>. We denote by >> the set of power products >*\*\>> with ,\,\\\>. The of a transseries \> is the highest such that \\exp>. In this paper, it will be convenient to consider a variant of the concept of transbases. Given \>, consider the differentiation <\equation*> \= z)>*\. A of level is a tuple =(\,\,\)> of transseries with \ \\\\> and such that <\description> \|\>\\;\;\>> for all . We will sometimes denote =exp z>. We notice that ;\;\>> is stable under > for all {1,\,l}> and it has been proved in that [\];\;\>> is stable under 1>>. In what follows, all transbasis will be considered to be differential. The following incomplete transbasis theorem is proved in a similar way as the usual theorem for non-differential transbases : <\theorem> Let > be a transbasis of level and \> a transseries of level >. Then there exists a transbasis |~>> of level (l,l)> such that \|~>>>>. Let be a constant field, > a monomial set and let ]]> be a strong -module of formal power series. Consider a set > and a strong -module ]]> which admits > as a strong basis. We will call elements of > monomials, even though we do not necessarily have an ordering >> on >. Assume that we have a strongly linear mapping <\equation*> :C[[\]]\C[[\]], such that |^>> is regular for all \\>. Then we call ]]> a and we say that > for each C[[\]]>. \ We denote by >> the equivalence relation on ]]> defined by g\=>. If > and > are monoids and > preserves multiplication, then we call ]]> a representation algebra. <\example> Given a set > and a mapping :\\C[[\]]> such that |^>> is regular for all \\>, let ]]> be the set of all mappings \C> such that >*|^>)\\>> is a summable family in ]]>. A family \(C[[\]])> is said to be summable if >*|^>))\\\\>> is a summable family in ]]>, in which case we set <\equation*> F:\\F>f>. The strong summation is well-defined, since F>f>*|^>> is summable for all \\> and |^>\0>. The mapping > extends to ]]> by strong linearity, giving ]]> the structure of a representation module. Any other representation module with the same > and > on > can be embedded into ]]>. <\example> Let >> be the strong -algebra of grid-based series over a monomial group >. Let |^>,\,|^>> be infinitesimal monomials in > and consider the formal group =\>*\*\>>. We have a natural multiplicative mapping :\\\;\>*\*\>\|^>>*\*|^>>>, which extends to >> according to the previous example. This gives >> the structure of a representation algebra. An C>> is called a of >. If > is generated by its infinitesimal elements, then each series in >> admits a Cartesian representation for a suitable >. <\example> Let ]]>>> be a representation module with representation mapping :C[[\]]\C[[\]]>. A is a mapping :\\(\)> with \\supp |^>> for all \\>. Given C[[\]]>, we set f=\supp f> \>, so that f\supp >. A family )I>\C[[\]]> to be >-summable if I:\\ f}> is finite for all \\>. The subset ]]>> of ]]> of all such that >*\)\supp f>> is >-summable is a representation module for the >-summability relation. We have ]]>=C[[\]]> for the trivial support function with \=supp |^>> for all\\>. Let ]]>>> be a representation module with representation mapping :C[[\]]\C[[\]]> and a support function as in example . Given \C[[\]]> and \\>, we denote <\equation*> >=\\>>*\. A strongly linear operator >:C[[\]]\C[[\]]> is said to be a truncation operator >, if <\description> >\T>=T>>. For all C[[\]]>, we have T> f\\>. For all C[[\]]>, we have > f|^>=>>. Two truncation operators >> and >> are said to be compatible if they commute. In that case, \\>=T>\T>> is again a truncation operator. Let > be a set of subsets of >, which is closed under complements and finite intersections. Then we say that ]]> is >-truncation-closed> if for each \>, there exists a truncation operator >:C[[\]]\C[[\]]> for each \>, and \\>=T>\T>=T>\T>> for all ,\\>. In what follows, given ,\\\>, we will sometimes use the notations > \)={\\\:\\\}>, >> \)={\\\:\\>\}>, <\example> In the case of Cartesian representations from example , we may simply take <\eqnarray*> >:C>>|>|>>>||>||\>>>>>> for all subsets > of >, where <\equation*> |\>={\\\:|^>\\}. Let ]]> be a strong differential -algebra for the derivation >. Assume that > admits a regular and distinguished right inverse >>. Let > be a monomial group together with a multiplicative mapping :\\C[[\]]> such that |^>> is regular for all \\>. In what follows, we will assume that |^>\\> for \\>. We denote by =\>> the free formal structure generated by >, >> and >. In other words, each element \\> is a tree whose leafs are labeled by elements in >, whose unary nodes are labeled by >, and whose binary nodes are labeled by >>. For instance, if =\*z>*\*\>>, then the following tree is an element of >>: <\equation*> |*|\|\3*\>>||\*\>>> We will denote by > the size of >, the number of leafs plus the number of integral nodes of the tree >. We denote by \> the total size of >, when we also count multiplicative nodes. For instance, the size of the above example tree is and its total size . We denote by > the finite subset of > of leafs of >. Elements of > are called . It may sometimes be useful to assume the existence of a special integral node monomial of size . Each integral monomial \\> induces a natural element |^>\C[[\]]>. Indeed, this was already assumed if \\>. If =\*\> =\>, then we recursively set <\eqnarray*> *\|^>>|||^>*|^>>>| \|^>>|||^>>>>> We also recursively define a non-trivial support function > by <\eqnarray*> \>|||^>(\\\)>>| \*\>|| \* \>>| \>||\ \>supp \>>>> We let ]]> denote the (non-associative) representation algebra from example . Elements of ]]> are called and we call ]]> a with >. For each C[[\]]>, we denote \supp f>lf \>. <\remark> The multiplication on >]]> is not associative nor commutative. In the sequel of this paper, this will not be a problem, since integral transseries are mainly used for the purpose of representation. Nevertheless, it is possible to define an associative (and/or commutative) variant of >]]>. Let >> be the equivalence relation on > generated by all relations of the form *\)*\\\*(\*\)>. This relation is compatible with the representation mapping> as well as the size function. Assuming that \>, it follows that />> has the structure of a multiplicative monoid and />]]> has the structure of an associative representation algebra. The mapping :C[[\]]\C[[\]]> naturally factors through/>]]>. ]]>> The mapping :\\C[[\]];\\ \> naturally extends by strong linearity to ]]>. Indeed, given \\> there is at most one \\> with \supp \={ \}>. Similarly, the multiplication >> extends to a strongly bilinear mapping >:C[[\]]\C[[\]]>. Given C[[\]]>, we denote by \>> and >> the strongly linear operators on ]]> with <\eqnarray*> \ g>>||>| g>||>>> The operators >, >\>> and >>> (for monomials >) admit strongly linear left inverses |\>>, >\|\>>> and >|\>>> whose action on monomials is given by <\eqnarray*> |\> \>||>|\=||0fn||1ex|> \>>||>>>>>>>|>\|\>> \>||>|\=\*\>>||>>>>>>>|>|\>> \>||>|\=\*\>>||>>>>>>>>> Let C[[\]]> be such that f\1>. Then we claim that <\equation*> (1+f)=1-f+f+\=1-f+f*f-f*(f*f)+f*(f*(f*f))-\ is a well-define multiplicative inverse of modulo >>. Indeed, (1+f)1>\( f)>>. Moreover, given \\> and with \supp f>, we must have # \>. Consider an exponential transmonomial \\> with >\z>. Then <\equation*> (\*\\exp)>=\*\>\exp+1\\>\exp For arbitrary transmonomials \\> it follows that <\equation*> (exp z*\\exp)>\log\(exp z*\\exp)>\log\\ for a sufficiently large . For such an , we define the of > by <\equation*> ispan \=(exp\\\log) ([exp z*\\exp]>\log). We have <\equation*> supp \\{\\\:\\>>\ \>}. <\example> We have >=\>, =z> and . Notice that <\equation*> ispan \*(\\exp)=(ispan \)\exp. Assume now that \\>. For integral monomials \C[[\]]>>, we recursively define the of > by <\eqnarray*> >||>|*\>||> {span \,span \}>>| \>||> {span \,ispan \|^>>}>>>> We have <\equation*> \\{\\\:\\>\|^>>}. For C[[\]]>> such that \supp f>lf \> is finite (we say that has ), we define \supp f> span \>. <\example> We have >( \>*( \))=\>. A is a set > of subsets of > which is closed under arbitrary intersections and such that }\> for each \\>. The elements of > will be called . For each subset \\> there exists a smallest frame which contains > and we denote it by )>>. <\example> Assume that > is a monomial group and define the flatness relations as in remark . Then the set <\equation*> =>=\>>>,\\\>\*\. is a framework. Indeed, if )I>=(\*\)I>> is a family of elements in > with I>\\\>, then I>\=(I>\)*\> for any \I>\>. If > is only a monomial monoid which can be embedded in a monomial group >, then ={\\\:\\>}> is again a framework. A on > is a function > which associates a frame >\> to each integral monomial \\>, so that <\eqnarray*> >>||}\=\\\>>|*\>>||>*\>)>>>|\>>|>|\\>> \>>>>> In particular, \\\>> for all \\>. We call >> the frame for >. More generally, given a set > of integral monomials, we call <\equation*> \>=(\>:\\\)> the frame for >. Given a representation algebra ]]> of integral series with a framework function :\\> as above, we call ]]> a . <\example> Assume that \\>. Taking <\equation*> \>={\\\:\\>>\|^>>} for all \\>, we define a framework function on >. Given an integral series \[[\]]>, the number of integral monomials > with =n> is finite for each fixed size \>. Therefore, we may define the >\t*\>[t]> for by <\equation*> >\\\>>\|f>\|*t>. We say that is if >> is convergent. We will denote the set of combinatorially convergent series in [[\]]> by [[\]]>. <\proposition> The set [[\]]> is stable under >, > and >. <\proof> This follows immediately from the facts that for all \[[\]]>, we have <\eqnarray*> >>|>|>+>>>|>>|>|>*>>>| f|\>>||>>>>> Here \\> for ,\\\>[t]> if \\> for all \>. A family )I>> of elements in [[\]]> is said to be if >)I>> is a summable family of power series in >{{t}}>. In other words, I:>\0}> is finite for each \> and \>(I>>)*t\\>{{t}}>. The set [[\]]> is a strong >-module for this infinite summation operator. Consider a strongly linear mapping [[\]]\\[[\]]>. For each \>, let >=max\\,s>=n> (|\>)\\>\{+\}>. We call >=>*u=>*t*u> the for . Notice that >> is uniquely determined by the restriction of to >. We may also regard >> as a mapping on >\{\\}[[t]]> by setting > >=>*> t>. We have <\eqnarray*> >>|>|> >>>>> for all \[[\]]>. If >> maps >{{t}}> into itself, then maps [[\]]> into [[\]]>, and we say that is . This is the case if and only if *>)\>> is a summable family in >{{t}}> for each \0>. In particular, if >\\>{{t,u}}> and there exist constants ,\\0> with >=0> for all \*n-\>, then is uniformly strong. A uniformly strong mapping [[\]]\\[[\]]> is said to be a if f\f> for all \[[\]]>. In that case is said to be a rewriting of and we write L f>. If maps > into itself, then we call a . In particular, consider a mapping \\> such that there exist constants ,\\0> with \\>, L \= \> and >\\+\*s>> for all \\>. Then extends uniquely to a monomial rewriting. <\example> The mapping which recursively replaces multiplications *\> by multiplications *\> determines a monomial rewriting. Assume that is the constant field for the derivation on ]]>. Then for any C[[\]]> there exists a constant \C> with <\equation*> ( f)*( g)= f* g+ g* f+c. Let > be the subset of > of integral monomials of the form <\equation*> \* \* \*\* \ with ,\,\\\>. We recursively define a product >> on ld>]> by <\eqnarray*> \\>||*\>>|\(\* \)>||*\* \>>|*\)\\>||*\* \>>|* \)\(\* \)>||*\*( (\\ \)+ (\\ \)+c|^>,|^>>)>>>> for all ,\\\> and ,\\\> and extension by linearity. Here we understand that the products *\> are taken in >. We recursively define the mouldification \C[\]> of an integral monomial \\> by <\eqnarray*> >||(\\\)>>|*\>||)\(mld \)(\,\\\\\)>>| \>|| mld \(\\\)>>>> This definition extends to a strongly linear mapping ]]\C[[\]]>. For several purposes, it is more convenient to work with moulds in ]]> than general integral series in ]]>. However, the mapping generally destroys combinatorial convergence, is not a rewriting. The convergence can often be restored using the process of arborification , which corresponds more or less to inverting the mapping in a nice way. In this paper, we will show that most important operations can be carried out directly in ]]>, while preserving combinatorial convergence. Throughout this section, we assume that ]]=C[[\>]]> is a framed representation algebra of integral series with underlying monomial group > and framework function :\\>. A is a finite set > of formal , together with a of one of the following forms for each \>: <\description> \{\}>, with \\>; \\\\>, with ,\\>; \\*\>, with ,\\>; \ \>, with \>. The language symbols \> may regarded as subsets of > as follows. Consider the set of mapping :\\>, such that for all \> we have (\)\{\}>, (\)\\(\)\\(\)>, (\)\\(\)*\(\)>, resp. (\)\ \(\)>, if > is specified by , , resp. . Then S:\\\S>\(\)> is again in . We will regard \> as the subset S)(\)> of >. Subsets of this kind are called . <\example> For each finite subset > of >, the set >> generated by >, >> and > is a regular language. Notice that >> consists of the \\> with \\>. Inversely, given a regular language specification >, let \\> be the finite set monomials \\>, such that \{\}> for some \>. Then each \> is contained in >> and the set f> is finite for each C[[\]]>. Given a regular language specification >, we say that \> \>, and we write \\>, if \\\\,\\\\\,\\\*\,\\\*\> for some \>, or \ \>. The transitive closure of the direct dependency relation>> is denoted by >>>; we say that > >, if \>\>. The dependency relation>>> is reflexive and transitive, but not necessarily anti-symmetric, since distinct language symbols may mutually depend on each other. <\example> Reconsider the introductory equation (). In its integral form (), this equation gives rise to the regular language specification <\eqnarray*> >|>| \;>>|>|>|\\;>>|>|>|>};>>|>|>|*\,>>>> where we may take =\*z>*\*\>>, =z>*\> and the natural embedding of > into > for>. We will show later that all integral monomials which occur in the expansion () belong to >. <\remark> In practice, in order to specify a regular language, it will often be convenient to regroup non interdependent rules together. For instance, the language> from example > may simply be specified by \({\>}\\*\).> <\remark> Consider a regular language specification > and a language symbol\> such that \>\> for no \> with \{\}> for some >. Then =\> as a subset of >. A language specification which contains no symbols > of the above type is said to be . Let > be a regular language specification. An is a sequence <\equation> \\>\\>\\>\\>\, such that \> and for all {1,\,l}>, we have \>, \\> and either <\itemize> \\\\> or \\\\> and =1>. \\*\> or \\*\> and \ \>. \ \> and \supp>> >. If =\>, then we call () a in >. A cycle () is said to be if \{\,\,\}>. Notice that each two language symbols > and >> in a cycle mutually depends on each other. \ We say that > satisfies the , if *\*\\1> for every cycle(). In that case, we say that > is a and the elements of > are called . A grid-based subset of > is an arbitrary subset of a grid-based language. Series in ]]> with grid-based support are called . We denote by >> the representation algebra of such grid-based series. <\remark> In relation to remark it is often useful to consider a slightly more general notion of arcs by allowing sub-arcs \>\\>\> to be replaced by one-step arcs \*\*\>\> in the case when the languages ,\,\> are unique with the properties that \\\\\\\\> and \{\,\}> for all {p+1,\,q-1}>. <\example> The language specification from example is grid-based. Indeed, it suffices to verify the cycle condition for minimal cycles. Up to cyclic permutation, such minimal cycles are necessarily of the form <\equation*> \\>\\\\>\. It is easily verified that >\(> \>)> and \\>>\2*\>> for all . Consequently, \supp \z*log z*\> and \>>\2*\>>, whence *\\1>. If we set <\equation*> \\{\>}, then we notice that the cycle condition is no longer satisfied. <\example> Any grid-based subset of > is also a grid-based subset of >>. Let > be a regular language specification and define <\equation*> \={1}\\ \\>supp>> \\{\}\> \\\, Consider a \>-labeled tree with children ,\,U>. Assume that the roots of ,\,U> are labeled by ,\),(\,\),\,(\,\)>. We say that is a if this is recursively the case for ,\,U> and either <\itemize> \{\}>, and \ \>. \\\\> or \\\\> for some \>, and =1>. \\*\>, and =1>. \ \>, and \supp>>>. We denote by >> the set of all such derivation trees. Given \>>, we define \\>, \> and \\> as follows: <\itemize> > is the product of all > where ,\)> ranges over all labels of . > is obtained from by substituting each label ,\)> by >, >> or >, depending on whether \{\}>, \\*\> \ \>, and by eliminating all nodes ,\)> with \\\\>. =\>, where ,\)> is the label of the root of . <\example> For the language specification > from example , the tree <\equation*> )|,\)|)|(\2*\>,\)>>|5*z>,\)|)|(\2*\>,\)>>> is a derivation tree \>> for the triple ,\,\)> with =\8*z>*\4*\>>, =( \2*\>>)*( \2*\>>)> and =\>. <\proposition> For each triple ,\,\)> with \\\> and \ \>, there exists a \>> with =\>, =\> and =\>. <\proof> We recursively construct ,\,\>> as follows: <\itemize> If \{\}>, then ,\,\>> is reduced to its root labeled by ,\)>. If \\\\>, then we choose {1,2}> with \\>, and set <\eqnarray*> ,\,\>>||)|T,\,\>>>>>> If \\*\>, =\*\> and =\*\> with \ \> , then <\eqnarray*> ,\,\>>||)|T,\,\>|T,\,\>>>>>> If \ \>, = \> and =\*\> with \supp>> > and \ \>, then <\eqnarray*> ,\,\>>||,\)|T,\,\>>>>>> It is easily verified by recursion that =\>, =\> and =\>. If ,\,\>> is a derivation tree constructed as in the proof of the proposition, then we say that is a for the triple ,\,\)>. For instance, is a derivation tree for ,\,\)> in example . <\lemma> Consider a subtree of a derivation tree with respect to a grid-based language specification >. If =\>, then \\>. <\proof> The derivation tree is of the form <\equation> ,\)|U|\|,\)|U|\||,\)|U|\|S|\|U>>|-4.5fn|>|0cm||0cm||>>|\|U>>|-6fn|>|-2fn||2fn||>|\|U>> where the expanded subtrees are >,\,U>=S>. Denoting by ,\)> the label of the root of and =\>*\*\>>/\>>> for all {1,\,l}>, we have a cycle <\equation> \\>\\>\\>\\>\, since =\=\=\>. We conclude that =\*\*\*\\\>. Let > be a grid-based language specification. We say that a derivation tree \>> is , if it does not contain a subtree of the form () with =\>. Given \>, let > be the set of monomials \\> such that ,\)=(\,\)> for some cycle-free derivation tree . Clearly, > is finite. Now consider ,\,\=\> with \\\\> and \{\,\,\}>. For {1,\,l}>, we define the set \\>\\> by <\itemize> If \\\\> or \\\\>, then \\>=1>. If \\*\> or \\*\>, then \\>= \>. If \ \>, then \\>=supp>> >. Clearly, for every \\\\>,\,\\\\\>>, we have a cycle (), so <\equation*> \\\\\>=\\\>*\*\\\>\1. Let > be the finite union of all \\\\>>, where ,\,\> are as above. <\lemma> For every \\\>, we have <\equation*> \\( \)*\>. <\proof> Let \ \>. We will prove that \( \)*\>> by induction over the minimal size of a derivation tree ,\,\>> for ,\,\)>. This is clear if > is cycle-free. Otherwise, ,\,\>> admits a subtree of the form () with =\>. Modulo the replacement of by a subtree, we may assume without loss of generality that the > and are all cycle-free. By the definition of \\\\>>, we now have /\\\>. Now consider the derivation tree which is obtained from ,\,\>> when replacing by . By the induction hypothesis, we have \( \)*\>>. We conclude that =(\/\)*\\( \)*\>>. <\theorem> Consider the set >>> of integral series over a grid-based differential algebra >> and assume that > is grid-based on >>. Then all strong linear combinations over grid-based subsets of >> are summable. <\proof> Let > be a grid-based subset of >>, so that \\> for \> some grid-based language specification >. Let > and >> be as in the previous section and notice that > is grid-based. Now give \> the natural ordering ,\)\(\,\)\\\\\\=\> and order >> by Higman's imbrication ordering , with the additional requirement that the imbrication preserves roots. Then \ Kruskal's theorem implies that the set of \>-labeled trees is well-quasi-ordered for the opposite ordering of >>. We claim that the mapping <\eqnarray*> :\>>|>|>>||>|>>>> preserves the ordering >>. So assume that ,\,\>\T|~>,|~>,|~>>> and let us prove by induction over the size of ,\,\>> that \|~>>. Write <\eqnarray*> ,\,\>>||,\)|T,\,\>|\|T,\,\>>>>||~>,|~>,|~>>>|||~>,|~>)|T|~>,|~>,|~>>|\|T|~>>,|~>>,|~>>>>>>>> Since the imbrication of ,\,\>> into|~>,|~>,|~>>> preserves roots, we have <\itemize> ,\)\(|~>,|~>)>, so that |~>=\>, =p> and |~>=\> for all . Each |~>,|~>,\>> admits a subtree of the form |~>|~>,|~>|~>,\>> with ,\,\>\T|~>|~>,|~>|~>,\>>. Now the induction hypothesis implies that that \|~>|~>> for all . By lemma , we also have |~>|~>\|~>> for all . It follows that <\equation*> \=\*\*\*\\|~>*|~>*\*|~>=|~>. This completes the proof of our claim. Now let \> and consider a family >*|^>)\\>> with >\\>. Let be the set of triples ,\,\)> with \\> and \ \>. Then the family >*|^>>*\),\,\)\S>> refines >*|^>)\\>>. By proposition , each triple ,\,\)\S> admits a (distinct) derivation tree ,\,\>\\>>. By what precedes, it follows that >*|^>>*\),\,\)\S>> is a well-based family. From lemma , we conclude that >*|^>)\\>> is a grid-based family. Theorem implies in particular that \=\\> \> is grid-based for all\>. If \\>, then we denote |^>>=\ \>>. A truncation operator >> on >>> is said to be compatible with the grid-based structure, if for every grid-based language \\>>, there exists a grid-based language > \> so that >> maps >> into > \>>. Throughout this section, we assume that >=\>>> is a representation algebra of grid-based series with underlying monomial group \\> and framework function :\\>. <\proposition> The intersection of a grid-based and a regular language is a grid-based language. <\proof> Consider a grid-based and a regular language specification > |~>>. In view of remark , we may assume that each language symbol \> |~>\|~>> is specified by a rule of the form <\eqnarray*> >|>|\\\\\\\\\ \\\\ \{\,\,\}>>||~>>|>||~>\|~>\\\|~>>\|~>>\ |~>\\\ |~>>\{|~>,\,|~>>}>>>> Let >|>> |~>> be the regular language specification, whose symbols are formal intersections \|~>> with > and |~>> as above, and so that each \|~>> is specified by <\equation*> \\|~>\|~>>(\\|~>|~>>)\(\\|~>|~>>)
\|~>>(\\|~>|~>>)
\{\,\,\}\{|~>,\,|~>>}. Since any cycle \|~>\>\\>\\|~>> in >|>> |~>> induces a cycle \>\\>\> in >, we conclude that >|>> |~>>> is a regular language specification. <\proposition> The set difference between a grid-based and a regular language is a grid-based language. <\proof> Consider a grid-based and a regular language specification > |~>>, where each language symbol \> |~>\|~>> is specified by a rule of the form() (). Let >|> |~>> be the regular language specification, whose symbols are formal differences \\|~>> with > as in () and where |~>=|~>\\\|~>> is a finite union, where each |~>> is specified by <\equation*> |~>\|~>\|~>\\\|~>>\|~>>\ |~>\\\ |~>>\{|~>,\,|~>>}. Each formal symbol \\|~>> is specified by <\eqnarray*> \\|~>>|>|\\=\>\\|~>)\\>|~>|~>>
\\\|~>)\\>|~>|~>>
\>>|||\\(|~>\\\|~>>\\\|~>\\\|~>>)\>>|||,\,\}\{|~>,\,|~>>,\,|~>,\,|~>>},>>>> where > stands for the set of pairs |~>)> with {1,\,u}> and |~>\{1,\,}>. Since any cycle \|~>\>\\>\\|~>> in >|> |~>> induces a cycle \>\\>\> in >, we conclude that >|> |~>>> is a regular language specification. Consider \\>, \\>, \\>, and a relation > among >>, >>, >>, >>>, >>>, >>>, >>>>, >>>>, >>>>, >>, >> and >. Then we define <\eqnarray*> \\>|>|\\;>>|\\>|>|\\;>>|\\>|>||^>\\.>>>> These relations generalize to grid-based integral series \>>, by requiring that they hold uniformly for all monomials in a grid-based language \supp f>. More precisely, denoting by > the set of all grid-based languages, we define <\eqnarray*> \>|>|\\,supp f\\\(\\\\,\\\))>>|\>|>|\\,supp f\\\(\\\\,\\\))>>|\>|>|\\,supp f\\\(\\\\,\\\))>>>> Notice that these definitions indeed extend the case when is a monomial, since}> is a grid-based language for every \\>. We say that \>> is , if +\> for certain \>, \\> and \|^>>. In that case, we denote =\>. Given a subset > of > and \>>, we recall that >=\\>f>*\>. More generally, if > is a subset of >>, then we denote >={f>:f\\}>. These notations are particularly useful if > is one of the sets <\eqnarray*> \>||\\:\\\}>>|\>||\\:\\\}>>|\>||\\:\\\}>>>> Restrictions on the support combine in a natural way. For instance, we have <\equation*> \>\,\\>={f\\>:\\\,supp f\\\(\\\\,\\\\\\\)}, because of proposition . <\proposition> Let ,\\\> and \{>,>,>}>. Given \\> with \\>, we define <\equation*> T>\> \=>|\>\>>>||>>>>> Then >\>> extends by strong linearity into an operator >\>:\>\>\\>\>>. <\proof> Given \>\>>, there exists a grid-based language specification > and \> with \>> and \\>. Then the support of \supp f>f>*T>\> \> is included in >, so >\> f=g\\>> is well-defined. <\remark> It can be shown that one actually has >\>=\>\,\>\>>. Let >> be an algebra of grid-based integral series. A on> is a mapping >:\\\>> such that <\description> > |^>=|^>>>, for all \\>. >\\> for all \\> with |^>>\\>. >> is regular for all \\> with |^>>\\>. >\|^>>> for all \\> with |^>>\\>. >)>=\*\>> for all \\> and \\>. *\)>>=\>>> for all ,\\\> with |^>\|^>>. In that case, and in virtue of the next sections, we say that >> is a of grid-based series. We say that >> is finitely based if <\equation*> lcl \=\\lf (\>)\lf (lf (\>)>)\\ is finite for all finite \\>. Given \\>, we will also denote >=\>>. Assuming that |^>>\\>, let \>, \\> and \|^>> be such that >=c*\+\>. Then >> admits a natural inverse >> modulo >> given by <\equation*> v>=c1>*\1>*(1+c1>*\1>*\)1>. If > is a grid-based language with \\>, \|^>> and \|^>>, then =\2>*\*(\1>*\)>> is a grid-based language with >\{\1>}\\>, \|^>1>> and \|^>>. It follows that >> is also a regular grid-based series. In the sequel, we will denote >={\}\\> and >={\1>}\\>. If |^>>\\>>, then we set >=\>={1}> and >=u>1>>. If |^>>=0>, then we take >=\>. Assume now that =\>> for some finite set >, that =z>*\>> for some plane differential transbasis =(\,\,\)> of transmonomials, and that =|^>,\,\=|^>> for certain ,\,\\\>. In that case we say that the differential representation algebra >> is and the above notations may be extended to more general monomials \\>: given \\> with |^>=z>*\>*\*\>> and =\>*\*\>>, we let >=u>> and >=v>> (if \1>). Furthermore, given =\\\>, consider =\>\\\\>\{\>}>. Then for all =c*\+\> with |^>\\>, we have \\>, \|^>> and \|^>>. Similarly, with =\2>*\*(\1>*\)>> as above, we have >\{\1>}\\>, \|^>1>> and \|^>>. Setting >={\}\\> and >={\1>}\\>>, we may therefore assume that >\\>> and >\\>> for all \\> with |^>\\>. If =\>, then we take >=\>={1}>. Let us now define a strong derivation :\>\\>>. We first define the derivative of each monomial in >: <\eqnarray*> >||>)*\(\\\>)>>|*\)>||*\+\* \>>|>\)>||>>>> Clearly, \ |^>=|^>> for all \\>. <\proposition> The mapping :\\\>> extends to a strongly linear mapping :\>\\>>, which represents the derivation on >>. <\proof> Consider a grid-based language specification >. For each \>, we define a new language symbol \> by <\itemize> If \{\}>, then \\\>*\>. If \\\\>, then \\\ \\\ \>. If \\*\>, then \\(\ \)*\\\*(\ \)>. If \ \>, then \\\>. Clearly, if \>> with \>, then \\ \>>. Now consider a cycle \>\\>\> which involves one of the languages of the form \> with \>. Since none of the \> and none of the >> depend on \>, it follows that the cycle has the form \\>\\>\\>> for certain ,\,\\> and modulo remark . But then \>\\>\> is also a cycle, whence *\*\\1>. We conclude that the \> with \> are grid-based languages. Given \\\>, the above discussion shows that > belongs to the grid-based language \>. In order to prove that the mapping \\ \>> extends by strong linearity, we still need to show that for every \\ \> there exists only a finite number of \\> with \supp \>. Indeed, by induction over the size of >, it is easily seen that > is necessarily obtained from > through the replacement of a subtree > of > by \> or the replacement of a subtree of the form *\> with \supp \>> by >. Assume that =\>> is triangular, with =z>*\>>. <\proposition> There exist grid-based subsets >>, |\>>> and >> of [z>]>>> such that for all \> we have <\eqnarray*> f>|>|>* f>>| |\> f>|>||\>>* f>>| f>|>|>* f>>>> <\proof> It suffices to prove the support bounds for monomials >. If \ \>, then there exists an \ \> with \supp \\(supp[z]*\>> )*\>. Consequently, we may take >=supp[z]*\>> >. If \ |\> \>, then > is of the form = \> and \ \>. Consequently, \>\supp \\ \>, so we may take |\>>={\/\>:\\z>*\>}>. We notice that|\>>> is a finite set. Let us finally show that we may take >=\|\>>\ \>, where =\\>\>> is a finite union up to duplicates. We use induction over the size of >. If \\>>, then have \\( \>)*\\\>*\>. If =\*\>, then by the induction hypothesis (\*\)\(\>* \)* \\ \*(\>* \)=\>* \>. Finally, if = \>, then \= |\> \\\|\>>* \>. <\proposition> Let \\> be such that >\\\\>. Then \ \,\\>> is stable under differentiation. <\proof> Let > be a grid-based language specification with \\> and \\> for all \>. Given \\\>, let us prove by induction over the size of > that \\\,\\>>. If \{\}>, then |^>\\> implies \\\>*{\}\\\,\\>>. If =\*\>, then ,\,\,\\\\,\\>> implies =\*\+\*\\\\,\\>>. Finally, if = \>, then =\\\\,\\>>. <\proposition> Assume that >> maps > into >>. Then the set >> is stable under differentiation. <\proof> Given a finite subset of > of >, let <\equation*> \=1+t*\\>>|\> For all \\> with \\>, we claim that <\equation*> \|\>\#\*t-1>*\ Indeed, using induction over >, we have <\eqnarray*> \|\>>||>*\|\>=>|\>*t\\>>| (\*\)|\>>|>|*t-1>*\)*|\>+|\>(#\*t-1>*\)=(#\*\)*t*\-1>*\>>| ( \)|\>>|||\>=t \-1>\(# \)*t \-1>*\*>>>> By strong linearity, we conclude that <\equation*> f|\>\>*\ for all \>> with \>, whence f\\>>. We conclude by recalling that is finite for each \>>. Throughout this and the next section, we assume that >=\>>> is a triangular differential representation algebra of grid-based series with underlying monomial group =z>*\>>, framework function :\\> and logarithmic derivation >:\\\>>. The objective of this and the next section is to construct truncation operators >\>> on =\>> for all \{>,>,>}>, \\>> and \\>. In this section, we start with the construction of >\>> on >\>>, where <\eqnarray*> >||\,\>>\>>>|>||\,\>>\>>>>> We assume that=\> is fixed and perform the construction simultaneously for all possible values of\\>>. Given \\>\>>, we define >\> \>, >\> \> and >\> \> by induction over the size of >. We always take <\eqnarray*> >\> \>||>>> If \>\>, then we take <\eqnarray*> >\> \>||>|>\> \>||>>>> If \>\>, then it will be convenient to denote =T>\>> and =T>\>>. We distinguish the following cases: <\enumerate> [\\>]. We take <\eqnarray*> (\)>||>>|(\)>||>>> [=\*\>]. We take <\eqnarray*> (\)>||(\)*\(\)>>|(\)>||(\)*\(\)+\(\)*\>>>> [=\>]. If >\\>, then we set <\eqnarray*> (\)>|| \(\)>>|(\)>|| \(\)>>>> If >\\>, then we take <\eqnarray*> ||(v>)>>|(\)>||(\)>>|(\)>|| T>|^>>(\-(w*\( \)))>>||| [\(\)-w*\(\)-w* T>|^>>(\(\))]>>>> <\remark> The relation () needs some further explanations. We first observe that the definitions of >\> \>, >\> \> and >\> \> coincide with those from proposition in the case when \\\>>. This ensures that (v>)> is well-defined. We will show below (proposition ) that (\)\\>|^>,\\>>. From proposition , it follows that (\)\\\>>. This ensures that >|^>>(\(\))> is well-defined. Finally, it can be shown that *\( \)\>|^>>, which justifies the simplification <\equation*> T>|^>>(w*\( \))= w*\(\). Consider a grid-based language \\>\>>. Given a grid-based language specification> with \>, then we notice that > only depends on languages \> with \\>. Modulo removing all other languages, we may thus assume without loss of generality that \\> for all \>. In order to show that the definitions of >\> \>, >\> \> and >\> \> for monomials \\> extend by strong linearity to >>, we first have to specify regular languages >\> \>, >\> \> and >\> \> with respect to which >\> f>, >\> f> and >\> f> can be expanded for \>>. We proceed along similar lines as for the construction of >\> \>, >\> \> and >\> \>. Since |^>>\>\>, we take >\> \\\>. If |^>>\>\>, then we take <\eqnarray*> >\> \>|>|>>|>\> \>|>|>>>> If |^>>\>\>, then we abbreviate \=T>\> \>, \=T>\> \> and distinguish the following cases: <\enumerate> [\{\}>]. We take <\eqnarray*> (\)>|>|>>|(\)>|>|>>>> [\\\\>]. We take <\eqnarray*> (\)>|>|>\>(\)\T>\>(\)>>|(\)>|>|>\>(\)\T>\>(\)>>>> [\\*\>]. We take <\eqnarray*> (\)>|>|(\)*\(\)>>|(\)>|>|(\)*\(\)\\(\)*\>>>> [\ \>]. If >\\>, then we set <\eqnarray*> (\)>|>| \(\)>>|(\)>|>| \(\)>>>> If >\\>, then we take <\eqnarray*> >|>|(\>)>>|(\)>|>|*\(\)>>|(\)>|>| [\(\)\\*\(\)\\*T>|^>>>(\( \))]>>>> By induction over the size of >, it is straightforward to verify that (\)\\( \)>> and (\)\\( \)>> for all >. <\remark> If \\> for all \>, then case 4 with >\\> never occurs, and it is easily checked that (\)\\> and (\)\\> for all \>. We will show in proposition below that (\)\\>|^>,\\>>. It follows that > and >|^>>>(\( \))> are well-defined grid-based languages. <\proposition> For \> with \\>\>>, we have <\eqnarray*> >\> \>||>>|>\> \>|>|>\,\\>>>|>\> \>|>|>\>,>>>> Moreover, if \\>\,\\>>, then >\> \\\>\,\\>>. <\proof> The inclusions are clear if |^>>\>\>. So assume that |^>>\>\> and let \\ \>. Let us prove by induction over the minimal size of a derivation tree for ,\,\ \)> with \ \> that \>\> and \\>. We distinguish the following cases: <\description> \{\}>>We must have =\>. Now =|^>>\>\> and \\>. \\\\>>Let {1,2}> be such that \\ \>. Then we must have \\\>, whence |^>>=|^>>>. By the induction hypothesis, we get \>\> and \\>. \\*\>>We obtain =\*\> with \\ \> and \\ \>. By the induction hypothesis, we have \>|^>>>, \>|^>>> and ,\\\>. It follows that \>|^>>*|^>>=|^>>\>\> and =\*\\\>. \ \>>If |^>>\\>, then = \> with \\ \>. By the induction hypothesis, we have \>|^>>> and \\>. Since |^>>\\>, it follows that \\> and = \\> |^>>\>|^>>>. If |^>>\\>, then =\*\> with \\> and \\ \>. By the induction hypothesis, we get \>|^>>> and \\>. Since \\>w,\\>>, we also have \>w> and \\>. It follows that \>w*|^>>\>|^>>> and \\>. The other inclusions are proved in a similar way. <\proposition> Given \> and \{>,>,>}> with \\>\>>, we have <\eqnarray*> >\> \>>||>>|>\> \>>|>|>\(> \>)>>|>\> \>>|>|>>>>> <\proof> The inclusions are clear if |^>>\>\>. Assume therefore that |^>>\>\>. If \\>\>>, then also \\\>>, whence >\> \\\> and >\> \>\\>>. Otherwise, we must have >=(>>> \)>, since |^>>\\>\(>>> \)> and >\(>>\)>. We conclude by proposition . <\proposition> The languages >\> \>, >\> \> and >\> \> are grid-based. <\proof> For languages of the form >\> \=\> there is nothing to prove. The case when \\> for all \> has also been dealt with in remark . Consider a cycle \>\\>\> which involves a language of the form (\)>. Then none of the > can be in \{\}>, since none of the languages in \{\}> depend on (\)>. Consequently, the cycle is of the form <\equation*> \(\)\>\\>\(\), with =|^>>> for all . For all , let =|^>>> if (\)\\*\(\)> and =\> otherwise. Then, using proposition , <\equation*> \\>\\>\ is again a cycle with *\*\\\*\*\\1>. Let us next consider a cycle \>\\>\> which involves a language of the form (\)>. Then none of the > can be a language of the form >, (\)>, >|^>>>(\(\))> or >, with \>. Consequently, the cycle is of the form <\equation*> \(\)\>\\>\(\), with =|^>>> for all . For all with \\*\> or \\*\> and \ \(\)> or \ \>, let =|^>>\\>. For the other , let =\>. Then, using proposition, <\equation*> \\>\\>\ is again a cycle with *\*\\\*\*\\1>. <\proposition> >\>>, >\>> and >\>> extend to >> by strong linearity. <\proof> The proposition is clear for >\>>. For \\> with \>\>, we also have \\:\\supp T>\>(\)}=\> and \\:\\supp T>\>(\)}={\}>. Given \\> with \>\>, let <\eqnarray*> (\)>||\\:\\supp T>\>(\)}>>|(\)>||\\:\\supp T>\>(\)}>>>> We also define <\eqnarray*> (\)>||\\:\\\*\}>>|(\)>||\\:\\\*\}>>|(\)>||\\:\= \}>>|(\)>||\\:\\supp \ \}>>>> Let us prove by induction over the size of \\> that (\)> and (\)> are finite. Now <\eqnarray*> (\)>|>|}\\(\(\))*\(\(\))\ \(\(\))\ \(\(\))>>|(\)>|>|(\(\))*\(\(\))\\(\(\))*\(\)\>>||| \(\(\))\ \(\(\(\)))\ \(\(\(\(\))))>>>> By the induction hypothesis, the sets at the right hand sides are finite. <\proposition> The operators >\>>, >\>>, >\>> on >\>> are projections with <\eqnarray*> >\>>||>|>\>>||>\,\\>>>|>\>>||>\>,>>>> Also, the restriction of >\>> to >\,\\>> is a projection on >\,\\>>. <\proof> The operator >\>=0> is clearly a projection with >\>=0>. By construction, we also have >\> \=\> and >\> \=\> for \\>\,\\>> \\>\>>. Given \>> with \\>\,\\>>, it follows that >\> f=f\\>> and similarly for >\>>. We conclude by proposition . <\proposition> Let ,|^>\{>,>,>}> and |~>\>>\>. Then the operators >\>> and =T>|~>>> on >\>> satisfy \P=P\>. <\proof> The result is clear when |~>\>\> or |^>\>\>. Assume therefore that |^>\>\\>|~>>. If |~>\>>, then |~>>|~>> \=T|~>>|~>> T>\> \=0>. If |~>=\>, then |~>>|~>> \=\> and |~>>|~>> T>\> \=T>\> \>. Let us denote by > f> the flattened support of \> in />>>. By proposition, there exists sets ,\>>, |\>,\>> and ,\>> of >/>>> with <\eqnarray*> f>|>|>* f>>| |\> f>|>||\>>* f>>| f>|>|>* f>>>> <\proposition> There exist a grid-based set ,\>\1> such that the operators >\>> and >\>> on >\>> satisfy <\eqnarray*> > T>\> f>|>|> f>>|> T>\> f>|>|,\>*> f>>>> <\proof> It suffices to prove both bounds for monomials >. The bound () directly follows from the fact that >\> \\\>\>>. Taking <\equation*> \,\>={\\\,\>\\,\>*\,\>\\|\>,\>*\,\>:\\>1}>, we prove () by induction over the size of >. In the case when \>\>, we have >\> \=\> and we are done, so assume that \>\>. If \\>, then >\> \=\> and we are again done. If =\*\>, then <\equation*> \ \\(\,\>*> \)*(\,\>*> \)=\,\>*> \. Assume now that = \>. If |^>>>\>, then we denote =|^>\\>, so that > w=> w={|\>}> and |^>\\*|^>>. Let |\>\> \ \>. We distinguish three cases: <\enumerate> [|^>>>\> and |\>\> w*\ \>] Since > \ \={|^>>|\>}>, we have \>\*\|^>>\>\*\|^>>>. This shows that |\>\|\>*> \\\,\>*> \>, since |\>\> > and \>1>. [|^>>>\> and |\>\> w*T>|^>>((\ \))>] Since \)\\>, we have <\equation*> > T>|^>>((\ \))\> (\ \) It follows that |\>\|\>*|\>*> (\ \)> with |\>\\,\>> and \>\>. Since > \ \={|^>>|\>}={|^>>|\>/|\>}>, we also have |\>\|\>*|\>*> \> with |\>\\,\>> and \>\1>>. Hence |\>\*\|\>*> \\\,\>*> \>. [|\>\> \ \>] Let >, >, >, =\>, =\/\>, =\/\> and =\/\> be as in the following diagram: <\equation*> |\>\> \>|>||\>\> \ \>>||\>\\|\>,\>>|r+0cm||r+0cm||>\>|||\>\\,\>>|l+0cm||l+0cm||>>>||\>\> \>||\>\\,\>>>||\>\> \ \>>>>> with =\/\>> and \\1>*supp \>, so that \\\/\>>. If \\>, then *\\\/ \>*\ \/\>\1>, whence *\|\>\\,\>> and *\*\|\>\\,\>>. If \\>, then \\>, whence ,\\\> and *\|\>=1>. Again, we obtain *\*\|\>=|\>\\,\>>. <\proposition> Assuming that >> maps > into >, the >\>> with \{>,>,>}> map >\>> into itself. <\proof> Let \t*\>[t]> be such that \> and <\equation*> v>|\>\>|\>\\ for all \\> with |^>>\\>. We claim that for all \\>\>>, we have <\equation*> \|\>\|\>\\. Indeed, using induction over the size if >, we are always in one of the following cases: <\eqnarray*> \\{0,\}>|>| \|\>\|\>\|\>\\>>| \=(\ \)*(\ \)>|>| \|\>= \|\>* \|\>\(|\>\\)*(|\>\\)=|\>\\>>| \= \ \>|>| \|\>=t* \|\>\t*|\>\\\\*|\>\\=|\>\\>>| \=\ v>*\ \>|>| \|\>=\* \|\>\\*|\>\\=|\>\\>>>> By strong linearity it follows that f|\>\>\\> for all \>\>>. Using a similar induction it can be checked that <\equation*> \|\>\|\>\(2*\) for all \\> \,\\>>. Indeed, in the product case, we have <\equation*> (\*\)|\>\\>*(2*\)>+(2*\)>*t>\(2*\)*\>. We deduce that f|\>\>\(2*\)> for all \>\,\\>>. Setting =4*\*(\\(2*\))>, with> as in the proof of proposition , we finally claim that <\equation*> \|\>\\*[(|\>\\)\(2*\)] for all \\> \>>. Indeed, using induction, we have <\eqnarray*> (\*\)|\>>|>|>*\*[(\>)\(2*\)]+t>*\*[(\>)\(2*\)]>>||>|*[(\>*(\>)+\>*(\>))\(2*\)]>>|||*[(\*\>)\(2*\)]>>>> in the multiplicative case and <\eqnarray*> \|\>>|>| \|\>+ (v>*\ \)|\>\(2*\)>>||>|*[(\-1>)\(2*\)]+[t*\*(\>)]\(2*\)>>|||*[(\-1>)\(2*\)]+>*\*[(\>)\(2*\)]>>||>|*[(t>\\)\(2*\)]>>>> in the integral case. We conclude that >\> f\\>\>> for all \>\>>. Let \1> be a grid-based subset of >/>>> and \ \\>>. We will denote by ;\>=\;\>>> the set of all series \> for which there exists a grid-based language specification> with <\itemize> > \\|\>*\> and \>> for some \>. > \\|^>>|\>*\> for all \\>. Given \>>\> and \{>,>,>}>, let us now define the grid-based operator <\eqnarray*> >\>:\;\,\>*\>>|>|;\,\>*\>\\>\>>>>> We proceed by induction over <\equation*> p=p,\>=card {|\>\\,\>*\:\\>\\>\}. The case has been dealt with in the previous section. Assume therefore that 0>. Let |~>|\>> be the maximal element of ,\>*\*|\>)>|\>>>. Then >\>\\;\,\>*\>\\>\>\\|~>;\,\>*\>>. Moreover, |~>,\>\p>, so we already have constructed >\>> on |~>;\,\>*\>>. Given \\;\,\>*\>> we now define <\eqnarray*> >\> \*>||>\> \+T>\> T>\> \>>|>\> \*>||>\> T>\> \>>|>\> \*>||>\> T>\> \>>>> Similarly, given a grid-based language \\;\,\>*\>>, we define <\eqnarray*> >\> \*>|>|>\> \\T>\> T>\> \>>|>\> \*>|>|>\> T>\> \>>|>\> \*>|>|>\> T>\> \>>>> so that >\> \\T>\> \> for all \\>. Since >\> \\T>\> \\\|~>;\,\>*\>>, we notice that >\> T>\> \> and >\> T>\> \> are well-defined. We also notice that the definitions extend the previous definitions on |~>;\,\>*\>> if |^>\>\> |^>>\>\>, since >\>> and >\>> are respectively the zero and the identity operator on |~>;\,\>*\>>. By strong linearity, we thus obtain the desired operator >\>> on ;\,\>*\>>, which extends its previous definition on |~>;\,\>*\>>. Since any \> belongs to ;\>> for some > and >, it follows that >\>> is defined on >. <\proposition> Assuming that >> maps > into >, the >\>> with \{>,>,>}> map > into itself. <\proof> Assume that \\\;\,\>*\>>. Let us show by induction over ,\>> that >\> f\\>. We have already treated the case in proposition . In particular, >\> f,T>\> f\\\\|~>;\,\>*\>>, with |~>> as above. Now <\eqnarray*> >\> f>||>\> f+T>\> T>\> f>>|>\> f>||>\> T>\> f(\\{>,>})>>>> We conclude by the induction hypothesis. <\proposition> The operators >\>>, >\>> and >\>> on > are projections with <\eqnarray*> >\>>||>\,\\>>>|>\>>||>\,\\>>>|>\>>||>\>>>>> Furthermore, the restriction of >\>> to \>> is a projection on >\,\\>>. <\proof> Given \\;\>>, let us prove by induction over ,\>> that \\>\,\\>> implies >\> \=\>. If ,\>=0>, then we are done by proposition . Otherwise, we have either |^>\>\> or |^>\>\>. In the first case, we obtain >\> \=\> and >\> \=0>. In the second case, we get >\> \=0> and >\> T>\> \=\>, by induction. Similarly, \\>\,\\>> implies >\> \=\> and \\>\>> implies >\> \=\>. It follows that >\>>, >\>> and >\>> are the identity operators on >\,\\>>, >\,\\>> >\>>. Given a grid-based language \\;\>>, let us now prove by induction over ,\>> that >\> \\\>\,\\>>, >\> \\\>\,\\>>, >\> \\\>\>> and >\> \\\>\,\\>> whenever \\\>>. If ,\>=0>, then we are done by proposition . Otherwise, we have >\> \\\|~>;\>> (where |~>|\>> is the maximal element of ,\>*\*|\>)>|\>>>), so the induction hypothesis implies <\eqnarray*> >\> T>\> \>|>|>\,\\>>>|>\> \=T>\> T>\> \>|>|>\,\\>>>|>\> \=T>\> T>\> \>|>|>\>>>>> and >\> \=T>\> T>\> \\\>\,\\>> if \\\>>. Since \ >\> \\\>\,\\>\\>\,\\>>, we conclude that >\> \=T>\> \\T>\> T>\> \\\>\,\\>>. <\proposition> Let ,|~>\{>,>,>}> and |~>\>>\>. Then the operators >\>> and =T|~>>|~>>> on > satisfy \P=P\>. <\proof> Without loss of generality, we may assume that |~>\\>. We prove that \P=P\> on ;\>>> by induction over ,\>>. If , then we are done by proposition . So assume that 0>. Let >\>> if =>> and if \>>. Setting >\>>, we have Q>. The induction hypothesis combined with strong linearity implies <\equation> \P\Q=P\\Q Now we distinguish three cases: <\description> \>|~>>>If |~>\>>, then <\equation*> P\=\P=0. If |~>=>>, then we get <\equation*> P\=P=\P. \>|~>>>If |~>=>>, then <\equation*> P\=\P=0. If |~>=>>, then =R>, so that <\eqnarray*> \P>||R+\P\Q=R+P\\Q=R+P\R\Q=R>>|>||R+P\Q\R=R>>>> If |~>=>>, then =Q>, whence <\equation*> \P=Q\R+\P\Q=0+P\\Q=P\. \>|~>>>Let =T>\>> if |~>=>> and =0> if \>>, so that =+\Q>. Then <\eqnarray*> \P>||\R+\P\Q>>|||\R+\Q\R+\P\Q>>|||\R+\P\Q>>>> and similarly =R\+P\\Q>. Now and > commute, since we have either =R> or or =0>. From (), we conclude that \P=P\>. We finally have to extend >\>>, >\>> and >\>> from > to >. By induction, we may assume that we have done this for |~>=\>> with =k+1> and that propositions and below already hold for > and |~>> instead of and >. In particular, |~>>\>> is a projection of > on >. Now consider a monomial \\> which is not in >. Then we set <\eqnarray*> >\> \>|||~>>\> \+T>\> T|~>>\> \>>|>\> \>||>\> T|~>>\> \>>|>\> \>||>\> T|~>>\> \+T|~>>\> \>>>> Similarly, given a language \\> but \\>, we set <\eqnarray*> >\> \>|>||~>>\> \\T>\> T|~>>\> \>>|>\> \>|>|>\> T|~>>\> \>>|>\> \>|>|>\> T|~>>\> \\T|~>>\> \>>>> so that >\> \ \T>\> \> for each \\> and \{>,>,>}>. Notice that the defining relations remain valid if \\> or \\>, by the induction hypotheses. By strong linearity, the operators >\>>, >\>> and >\>> on > therefore extend to >. <\proposition> Assuming that >> maps > into >, the >\>> with \{>,>,>}> map > into itself. <\proof> If > is the largest element of >, then we are done by proposition . Otherwise, we use induction and assume that we have proved the assertion for all larger |~>\\>. Given \>, it follows that |~>>\> f,T|~>>\> f,T|~>>\> f\\>. Now <\eqnarray*> >\> f>||>\> T|~>>\> f>>|>\> f>||>\> T|~>>\> f+T|~>>\> f(\\{>,>})>>>> We conclude by proposition . <\proposition> The operators >\>>, >\>> and >\>> on > are projections with <\eqnarray*> >\>>||\\:\\>\\\\|^>/\}>>>|>\>>||>\,\\>>>|>\>>||\\:\\>\\\\\/|^>}>>>>> Furthermore, the restrictions of >\>> and >\>> to \>> are projections on >\,\\>> >\,\\>>. <\proof> If , then we are done by proposition . If n>, then the induction hypotheses at the beginning of this section imply that the above properties are already satisfied for the operators |~>>\>>, |~>>\>> and |~>>\>>. Assume now that \\> is such that \>\> and \|^>/\>. If \\>, then proposition implies >\> \=\>. Otherwise, the induction hypothesis implies |~>>\> \=\> and |~>>\> \=T|~>>\> T|~>>\> \=T|~>>\> T|~>>\> \\\|~>>\>\\|~>>\>={0}>. This shows that >\> \=T|~>>\> \+T>\> T|~>>\> \=\>. In a similar way, if \\> is such that \>\> and \|^>/\>, then >\> \=\>. Finally, if \\> is such that \>\> and \\>, then \\>, so >\> \=\>, by proposition . Given a grid-based language \\>, the induction hypothesis and proposition also imply <\eqnarray*> >\> \>|>|\\:\\|~>>\\\\|^>/\}\\>\,\\>={\\\:\\>\\\\|^>/\}>>|>\> \>|>|>\,\\>=\>\,\\>>>|>\> \>|>|\\:\\|~>>\\\\|^>/\}\\>\>={\\\:\\>\\\\|^>/\}>>>> Finally, if \\\>>, then we obtain <\eqnarray*> >\> \>|>||~>>\,\\>\\>\,\\>=\>\,\\>>>|>\> \>|>||~>>\,\\>\\>\,\\>=\>\,\\>>>>> This completes the proof. <\proposition> Let ,|~>\{>,>,>}>, ,|~>\\>> and =\,|~>=\>> with >. The the operators >\>>, =T|~>|~>>|~>>> on > satisfy \P=P\>. <\proof> If , then we are done by proposition . If n>, then the induction hypotheses at the beginning of this section imply that we have commutation when is replaced by . Notice that we do not necessarily have =k+1> contrary to before, but merely \k>. Let us first assume that \|~>>. Let >\>> and denote >\>> if \>> and otherwise. Then Q>, so the induction hypothesis implies <\eqnarray*> >||+P\Q\>>|||\R+P\\Q>>|\P>||\R+\P\Q>>>> Moreover, by proposition , and > commute on the image of . We conclude that and > commute everywhere. Assume now that |~>=\>. Let =T>|~>>> and denote =T|~>>|~>>> if |~>\>> and =0> otherwise. If |~>\>\>, then =Q>, =\Q=0> and the induction hypothesis implies <\eqnarray*> >||+P\Q\+P\\>>|||+P\\>>|||\R+\P\Q>>|||\P>>>> Assume now that |~>\>\>. We have already shown above that (or >) and (or > or or >) commute. We also have =\Q=0>. Consequently, <\eqnarray*> >||+P\Q\+R\\+P\Q\\>>|||+P\Q\+R\\>>|||\R+\P\Q+\\R>>|||\P>>>> This completes the proof. Let us now consider an extension |\>> of the transbasis > with a new element |\>> between > and |~>=\>. Likewise, assume that we have extensions |\>=z>*|\>>> of >, |\>> of > with :|\>\|\>> and |\>=|\>>> of >, together with a logarithmic derivation on |\>> which extends the one on >. Denote the truncation operators on |\>>> as constructed above by >>\>> for all \|\>>, \|\>>> and \{>,>,>}>. If \\> and \\>>, then we want to show that the restriction of >>\>> to >> coincides with >\>>. Denoting by > the canonical injection of >> into |\>>>, we thus have to show that >>\>\\=\\T>\>>>. In the cases when \\> or \\> and \|~>>, the definitions of >>\> \> and >\> \> clearly coincide. Assume therefore that =\>. If =>>, then <\eqnarray*> >>\>\\>||>>\>\>|\>>\>\>|~>>\>\\>>|||>>\>\>|\>>\>\\\T|~>>\>>>>> Now for \supp im T|~>>\>> we have \>>\> and \\>, whence \|\>>\> and \|\>>. It follows that >|\>>\> \=\> and >>\> \=T>\> \>, whence >>\>\\=\\T>\>>. If \>>, then <\eqnarray*> >>\>\\>||>|~>>\>+>|\>>\>\>|~>>\>+>>\>\>|\>>\>\>|~>>\>)\\>>|||\T|~>>\>+>|\>>\>\\\T|~>>\>+>>\>\>|\>>\>\\\T|~>>\>>>|||\T|~>>\>+\\T>\>\T|~>>\>>>|||\T>\>>>>> Indeed, in a similar way as above, we have <\equation*> >>\>\>|\>>\>\\\T|~>>\>=>>\>\\\T>\>=\\T>\>\T|~>>\>. Furthermore, for \supp im T|~>>\>> we have >|\>>\> \=0>, since \>>. In this section, we will construct the representation algebra >> of integral exponential transseries, with :\>\z>*\>. Using induction over \>, we first construct a differential representation algebra >=\>>> of grid-based integral series, with underlying monomial group>*\>, and such that <\description> For each \\>, there exists a ``privileged'' =|\>\\>> with =|^>>. For all ,\,f\\>>, there exists a triangular differential representation subalgebra >>\\>> of grid-based series with ,\,f\\>>>. In , we call > a for . We notice that the union of two triangular sets is again a triangular set. Given ,\\\> with \1>, we claim that the operators >\>> with \{>,>,>}> are naturally defined on >>. Indeed, given \>>, there exists a triangular set> for , |\>> and |\>>. In sections and , we have shown that >\> f> is a well-defined element of >>>. Moreover, because of section , the value of >\> f> does not depend on the choice of >. Taking >={1}>> and >=1>, the induction hypotheses and are clearly satisfied for . Assume that >> has been constructed and let <\equation*> \>>={f\\>: f\\>}. The set <\equation*> \=exp \>> is clearly a monomial group with >-powers and we have a natural mapping :\>\\>*\>> defined by <\eqnarray*> >f|^>>||>>>|*\ |^>>|||^>*|^>>>| \|^>>|||^>>>>> We define a logarithmic derivative on > as follows. Given =\ f>\\> with \\>, we may write =c*\+\> with \>>, \\> and \\>. Now we set <\equation*> \>\c*|\>+T>\,\>1> f. Since f\\>>, we notice that >\,\>1> f\(\>)\,\1,\\>>. We extend the mapping >:\\\> into a mapping >:\\\> as follows. If \\\\> is such that there exists an (\>>)> with =\ >>, then we arbitrarily take such an and set |\>=\ f>>. Otherwise, we simply take =\ \>>>. Let us prove , which will complete the induction. Given ,\,f\\>>, the set =lf(f)\\\lf(f)> is finite. By the induction hypothesis, there exists a triangular differential representation subalgebra >>\\>> of grid-based series with >\\>>>. Taking |~>=\*\>>, we then obtain a triangular differential representation subalgebra |~>>>\\>> of grid-based series with ,\,f\\|~>>>>. We clearly have >\\>\\>\\>. The set <\equation*> \>=\>\\>\\>\\ is called the set of exponential integral transseries. For \>>, the smallest with \>> is called the of . Setting =exp \>>>, the finiteness property implies that >=\>>> and >=\>\\>\\>. By induction over the exponential height , let us now construct a strongly linear mapping \exp:\>\\>> which maps integral monomials to integral monomials. So assume that or that 0> and that we already have mapping \exp:\>\\>>. Given a monomial \\>>, we recursively define \exp> by <\eqnarray*> f>\exp>|| f)\exp>(f=0\f\\>>)>>|*\)\exp>||\exp)*(\\exp)>>| \)\exp>|| (\ 1>*(f\exp))>>>> This definition has a natural analogue for language specifications: <\eqnarray*> f>}\exp>|| f)\exp>}>>|\\)\exp>||\exp\\\exp>>|*\)\exp>||\exp)*(\\exp)>>| \)\exp>|| (\ 1>*(\\exp))>>>> Hence, \exp> extends by strong linearity to >>. Now for each \>, the representation algebra <\equation*> \>\exp of >*\>\exp> with derivation = z>*\> is formally isomorphic to the representation algebra >> of >*\>> with derivation >. By what precedes, we may therefore embed each >\exp> into >\exp> (for instance, 1>\\>> is identified with )1> \)1> 1>*1>\\>\log>), so that <\equation*> \>\\>\log\\>\log\\ The set <\equation*> \>=\>\\>\log\\>\log\\ is called the set of integral transseries. Setting <\equation*> \=\\\\log\\\log\\, we have >=\>>>. <\proposition> Let \>>, ,\\\> and \{>,\,>}>. Then <\enumerate-alpha> There exists a \,\> \>> with => \>>. There exists an \,\ \>> with = \>>. <\proof> In the case when \>>, ,\\\>, \1> we may take > \> f>. Similarly, if f\\> and \\>, then we take > \> f>. The general case is reduced to one of the above cases modulo a sufficient number of upward shiftings. <\corollary> Each \>> with 0> admits a multiplicative inverse modulo >>. <\proof> Writing =c*\*(1+\)> with \\>*\> and \1>, we may take <\equation*> f1>=c1>*|\>1>*(1+\)1>, where \,\1>> is such that =\>. An integral transseries in >> is said to be if is combinatorially convergent as an integral series and if >> is recursively combinatorially convergent for every \lf(f)>. The inclusions <\eqnarray*> |>|lf g>>||>|lf g>>| f>||>>> together with proposition imply: <\proposition> The set >> is stable under >, > and >.> <\proposition> The set >> is stable under postcomposition with . <\proof> Given \>>, let us prove by induction over the exponential height of that exp\\>>. For each \lf f>, we have either and \exp=\=1>, or 0> and =\ g>>, where has exponential height > n-1>. In the second case, the induction hypothesis implies that \exp)>=\ 1>*(g\exp)\\>>. Since <\equation*> lf (f\exp)\(lf f)\exp\{\ 1>}, it follows that >\\>> for all \lf (f\exp)>. Furthermore, the postcomposition with send monomials \supp f> to monomials \exp\supp f\exp> with \exp\#\>. It follows that <\equation*> exp|\>\*>. This shows that exp\\>>. Proposition implies that >\exp\\>> and more generally <\equation*> \>\\>\log\\>\log\\. We call <\equation*> \>=\>\\>\log\\>\log\\ the set of combinatorially convergent integral transseries. We denote >, >, the images of >>, >>, under >. The following is an immediate consequence of proposition : <\proposition> The set >> is stable under >, > and >.> <\proposition> Given ,\,f\\>>, there exists a triangular set > with ,\,f\\>>> and such that >> maps > into >>. <\proof> We prove the proposition by induction over the maximal exponential height of ,\,f>. If , then the result is clear, so assume 0>. The set =lf(f)\\\lf(f)> is finite. By the induction hypothesis, there exists a triangular set > with >\\>>> and such that >> maps > into >>. Taking |~>=\*\>>, we have ,\,f\\|~>>>>. Let us show that >> maps |~>> into >>. So let \|~>> with |^>>\\>. Writing =c*\+\>, where =\ g>>, we have <\equation*> \>=c**|\>+T>\,\>1> g. By the construction of >>, we have |\>\\>>. Since \>>>, proposition also implies that >\,\>1> g\\>>>. <\proposition> Let ,\\\> and \{>,\,>}> with \1>. Then >\>> maps >> into itself. <\proof> Given \>>, let > be a triangular set with \>>> and such that >> maps > into >>. By proposition , we now have >\> f\\>>\\>>. In a similar way as proposition and its corollary, one may now prove: <\proposition> Let \>>, ,\\\> and \{>,\,>}>. Then <\enumerate-alpha> There exists a \,\> \>> with => \>>. There exists an \,\ \>> with = \>>. <\corollary> Each \>> with 0> admits a multiplicative inverse modulo >>. In this paper, we have laid the foundations for the formal calculus with integral transseries. We intend to further develop this theory in a forthcoming paper. Let us briefly mention a few points which still have to be investigated in more detail. First of all, from the foundational point of view, we have chosen to work with ``uniform'' arcs and cycles. It is also possible to consider ``individual'' arcs and cycles of the form <\equation*> (\,\)\>(\,\)\>\\>(\,\)\>(\,\), such that \\\> and for all {1,\,l}>, we have \\\>, \\> and either <\itemize> \\\\> or \\\\>, =\> and =1>. \\*\> or \\*\>, =\*\> =\*\> and \ \>. \ \>, = \> and \supp>> >. We expect that languages which verify the weaker ``individual'' cycle condition can always be rewritten into languages which verify the usual uniform cycle condition, using the technique of ``loop unrolling''. More generally, given an arbitrary regular language >, one may define its ``descending part'' >>: it consists of those integral monomials > such that any ``cycle in the derivation tree of >'' satisfies the individual cycle condition. Again, >> may be computed using the process of loop unrolling. Another application of loop unrolling in combination with truncation is to rewrite an arbitrary grid-based language specification > into an equivalent language specification |~>> modulo >>, such that for every \ \\|~>>, we have \\> for all ,\\\>>. In particular, in the cycle condition, this implies that (supp>> )=\(supp>> )> for all \\>. Another interesting topic from the foundational point of view is to systematically work with operators of either one of the forms <\eqnarray*> >:f>|>|1>* \*f>>|>:f>|>| \)>>1>*\1>* \*f>>>> instead of usual integration. These operators have the advantage of being closer to arborified moulds and may make it easier to develop the theory of accelero-summation. Secondly, operators of the form *J>> with \1> are naturally ``infinitesimal'' on suitable frames, and it should be possible to rewrite arbitrary grid-based languages as a tree whose leafs are languages which are constructed using products, infinitesimal operators and repetition. Finally, it remains to be shown that the set of integral transseries is stable under many other operations, such as composition and functional inversion (when defined), formal alien differentiation, the resolution of quasi-linear differential equations, and so on. Of course, the consideration of additional operators besides integration, such as infinite summation, is another interesting topic. <\bibliography|bib|alpha|all.bib> <\bib-list|[99]> J.Écalle and B.Vallet. The arborification-coarborification transform: analytic, combinatorial, and algebraic aspects. Technical Report 2004-30, Univ. Paris-Sud, 2004. J.vander Hoeven. . PhD thesis, École polytechnique, France, 1997. J.vander Hoeven. Complex transseries solutions to algebraic differential equations. Technical Report 2001-34, Univ. d'Orsay, 2001. J.vander Hoeven. Transseries and real differential algebra. Technical Report 2004-47, Université Paris-Sud, Orsay, France, 2004. Submitted to Springer-Verlag's series of Lecture Notes in Mathematics. <\initial> <\collection> <\references> <\collection> |?>> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > |\>|40>> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > |?>> |?>> > > > > > > > > > > > > > > > > > |||\|||>>>|16>> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > <\auxiliary> <\collection> <\associate|bib> vdH:osc EcVal04 vdH:osc vdH:osc vdH:osc vdH:osc vdH:osc vdH:phd EcVal04 vdH:ln <\associate|toc> |math-font-series||font-shape||1.Introduction> |.>>>>|> |math-font-series||font-shape||2.Complex transseries> |.>>>>|> |2.1.Construction of complex transseries |.>>>>|> > |2.2.Differentiation and integration |.>>>>|> > |2.3.Flatness relations |.>>>>|> > |2.4.Transbases |.>>>>|> > |math-font-series||font-shape||3.Truncation-closed representation modules> |.>>>>|> |3.1.Representation modules |.>>>>|> > |3.2.Truncation operators |.>>>>|> > |math-font-series||font-shape||4.Integral series> |.>>>>|> |4.1.Integral series |.>>>>|> > |4.2.Computations in |C[[\]]> |.>>>>|> > |4.3.The span of an integral series |.>>>>|> > |4.4.Frameworks |.>>>>|> > |4.5.Combinatorial convergence |.>>>>|> > |4.6.Mouldification |.>>>>|> > |math-font-series||font-shape||5.Grid-based integral series> |.>>>>|> |5.1.Regular languages |.>>>>|> > |5.2.Grid-based languages |.>>>>|> > |5.3.Derivation trees |.>>>>|> > |5.4.Summability of grid-based integral series |.>>>>|> > |math-font-series||font-shape||6.Differentiation> |.>>>>|> |6.1.Stability properties under boolean operations |.>>>>|> > |6.2.Uniform restrictions on the support |.>>>>|> > |6.3.Logarithmic derivatives |.>>>>|> > |6.4.Differentiation |.>>>>|> > |6.5.Support properties of differentiation |.>>>>|> > |6.6.Combinatorial convergence |.>>>>|> > |math-font-series||font-shape||7.First order expansions> |.>>>>|> |7.1.Expansion of monomials |.>>>>|> > |7.2.Expansion of the language specifications |.>>>>|> > |7.3.Frames for the expanded languages |.>>>>|> > |7.4.Extension by strong linearity |.>>>>|> > |7.5.Properties of the truncation operators |.>>>>|> > |7.6.Combinatorial convergence |.>>>>|> > |math-font-series||font-shape||8.Full expansions> |.>>>>|> |8.1.Higher order expansions |.>>>>|> > |8.2.Properties of higher order expansion |.>>>>|> > |8.3.Recursive expansions |.>>>>|> > |8.4.Properties of recursive expansion |.>>>>|> > |8.5.Extension of the transbasis |.>>>>|> > |math-font-series||font-shape||9.Integral transseries> |.>>>>|> |9.1.The set of exponential integral transseries |.>>>>|> > |9.2.The set of general integral transseries |.>>>>|> > |9.3.Combinatorial convergence |.>>>>|> > |math-font-series||font-shape||10.Conclusion> |.>>>>|> |math-font-series||font-shape||Bibliography> |.>>>>|>