1Introduction

1.1The quest of a universal framework for asymptotic calculus

In order to get our hands on a complex mathematical expression, we first need to simplify it as much as possible. This can often be achieved by eliminating parts that are asymptotically negligible. For instance, when studying the expression for large values of , we may compute the approximations , , and then . Such approximations rely on our ability to determine and compare asymptotic rates of growth.

Is it possible to develop a universal framework for this kind of asymptotic simplification? This sounds like a difficult problem in general, especially for multivariate functions or functions with an irregular growth like . On the other hand, the problem might become tractable for univariate functions in a neighborhood of infinity , provided that is constructed using a limited number of well-behaved primitives.

An important first step towards a systematic asymptotic calculus of this kind was made by Hardy in [20, 21], based on earlier ideas by du Bois-Reymond [14, 15, 16]. We say that is an -function if it is constructed from and the real numbers using the field operations, exponentiation, and logarithms. Given two non-zero germs of -functions , at infinity, Hardy proved that exactly one of the relations , , or holds, where

Hardy also observed [20, p. 22] that “The only scales of infinity that are of any practical importance in analysis are those which may be constructed by means of the logarithmic and exponential functions.” In other words, Hardy suggested that the framework of -functions not only allows for the development of a systematic asymptotic calculus, but that this framework is also sufficient for all “practical” purposes.

Hardy went on [20, chapter V] with the examination of possible counterexamples, through the exploration of pathological functions whose asymptotic behavior does not conform to any logarithmico-exponential scale. Here he made a distinction between irregular asymptotic behavior (such as oscillating functions) and regular asymptotic behavior that yet cannot be described in terms of -functions. Basic examples of the second type were already constructed by du Bois-Reymond and Hardy [20, chapter II]. For instance, let for and let for each . Then grows faster than any -function.

In order to formalize the concept of “regular” growth at infinity, we focus on classes of (germs of) functions that are stable under common calculus operations such as addition, multiplication, differentiation, and composition. The class of -functions indeed satisfies these conditions, but it is interesting to investigate whether there exist larger classes of functions with similar properties.

Two particular settings that have received a lot of attention are Hardy fields (i.e. fields of germs of real continuously differentiable functions at infinity that are closed under differentiation [7]) and germs of definable functions in -minimal structures [10]. Each of these settings excludes oscillatory behavior in a strong sense. For instance, although the function does not oscillate for large values of , its second derivative does, so the germ of this function at infinity does not belong to a Hardy field.

With a more precise definition of regularity at hand, one may re-examine the existence of regular functions whose asymptotic growth falls outside any scale of -functions. For instance, the function from above is not even continuous and thereby not sufficiently regular. Nevertheless, it was shown by Kneser [28] that the functional equation

(1.1)

has a real analytic solution on . This provides us with a more natural candidate for a regular function that grows faster than any -function. Indeed, it was shown by Boshernitzan [6] that Kneser's solution belongs to a Hardy field. The functional inverse of frequently occurs in the complexity analysis of recursive algorithms that use exponential size reductions. For instance, the fastest known algorithm [22] for multiplying two polynomials of degree in runs in time . This shows that Hardy's framework of -functions is insufficient, even for practical purposes.

Another example of a regular function that is not asymptotic to any -function is the functional inverse of . This fact was actually raised as a question by Hardy and only proved in [23] and [13]. More explicit examples of such functions, like , were given in [23]. It turns out that the class of -functions lacks several important closure properties (e.g. functional inversion and integration), which makes it unsuitable as a universal framework for asymptotic calculus.

The class of transseries forms a better candidate for such a universal framework. A transseries is a formal object that is constructed from (with ) and the real numbers, using exponentiation, logarithms, and infinite sums. One example of a transseries is

Depending on conditions satisfied by their supports, there are different types of transseries. The first constructions of fields of transseries are due to Dahn and Göring [9] and Écalle [17]. More general constructions were proposed subsequently by van der Hoeven and his student Schmeling [23, 29].

Transseries form a natural “infinitary” extension of the concept of an -function. The transseries are closed under integration and functional inversion [23, 13]. They also satisfy a differential intermediate value property [26, Chapter 9]. However, transseries are only defined formally, so their analytic meaning is not necessarily obvious. One technique for associating an analytic meaning to certain divergent transseries is accelero-summation [17], a generalization of Borel summation [5]. An alternative technique is based on differential algebra and model theory [27, 1]. In this paper, we focus on formal asymptotic computations, without worrying about analytic counterparts.

Despite the excellent closure properties of transseries for the resolution of differential equations, the functional equation (1.1) still does not have a transseries solution. In order to establish a universal formal framework for asymptotic calculus, we therefore need to incorporate extremely fast growing functions such as , as well as formal solutions , , etc. to the following equations:

			(1.2)
			(1.3)

The fast growing functions , , are called hyperexponentials. Their functional inverses , , are called hyperlogarithms and they grow extremely slowly. The first construction of a field of generalized transseries that is closed under and for all was accomplished in [29]. Here we understand that and .

The hyperlogarithms , , etc. obviously satisfy the functional equations

In addition, we have a simple formula for their derivatives

(1.4)

where and

for all and . The formula (1.4) is eligible for generalization to arbitrary ordinals . Taking , we note that the function does not satisfy any functional equation. Yet any truly universal formal framework for asymptotic calculus should accommodate functions such as for the simple reason that it is possible to construct models with good properties in which they exist. For instance, by [6], there exist Hardy fields with infinitely large functions that grow more slowly than for all .

The construction of the field of logarithmic hyperseries in [12] was the first step towards the incorporation of hyperlogarithms with arbitrary . The field is the smallest non-trivial field of generalized power series over that is closed under all hyperlogarithms and infinite real power products. It turns out that is a proper class and that is closed under differentiation, integration, and composition.

The main purpose of the present paper is the construction of a field of general hyperseries that is also closed under the functional inverse of for every ordinal . Our construction strongly relies on properties of the field of logarithmic hyperseries. Intuitively speaking, the reason is that the derivative of can be expressed as the composition of a logarithmic hyperseries with :

and similarly for all higher derivatives. One key aspect of our approach is therefore to construct increasingly large fields of hyperseries simultaneously with compositions

where denotes the class of positive infinitely large elements of .

The main result of this paper is the construction of a field of hyperseries that is closed under all hyperlogarithms and all hyperexponentials . Does this end our quest for a universal formal framework for asymptotic calculus? Not quite yet. First of all, it remains to be shown that is closed under all common calculus operations, such as differentiation and composition. Secondly, the field does not contain any solution to the functional equation

Fortunately, it is possible to construct fields of transseries with “nested” solutions

to such equations [29, Section 2.5]. Something similar is possible for hyperseries; although this is beyond the scope of the present paper, we introduce the fundamental concepts that we expect to use for this generalization.

One may also wonder whether there exist natural models for hyperexponential functions and hyperseries. We already noted that Kneser constructed a real analytic solution of the equation (1.1). Schmeling also constructed real analytic solutions , , of (1.2), (1.3), etc. Écalle introduced a systematic technique for the construction of quasi-analytic solutions to these and more general iteration equations [17]. In general, it seems unlikely that there exist any “privileged” regular solutions at infinity.

Another interesting model for hyperexponentiation is Conway's field of surreal numbers [8]. The field is a non-standard extension of the field which contains the class of ordinal numbers. The arithmetic operations are defined in a surprisingly “simple” way, using transfinite induction. Nevertheless, the field has a remarkably rich structure; e.g. it is real-closed. The exponential function on the reals has been extended to by Gonshor [18] and this extension preserves the first order properties of [11].

A “simplest” surreal solution to (1.1) with good properties has been constructed in [3]. This solution is only defined on , but in view of our previous remarks on real solutions of (1.1), is interesting to note that we may indeed consider it as “the” privileged solution on . Constructing each hyperlogarithm and hyperexponential on surreal numbers involves overcoming many technical difficulties. Our results from this paper reduce this to the simpler task of defining partial hyperlogarithms on , which satisfy a short list of axioms.

We finally note that Berarducci and Mantova also defined a derivation with respect to on [4]. This derivation again has good model theoretic properties [2]. However, although the derivation satisfies for all , it was pointed out in [1] that it does not satisfy for all , for “reasonable” definitions of . Indeed, for the definition of from [3], we have .

Stated differently, the hyperexponential structure on reveals that is not the ultimate derivation on with respect to that we might hope for. One major motivation behind the work in this paper is precisely the construction of a better derivation on , as well as a composition. The plan, which has been detailed in [1], is to construct an isomorphism between and a suitable field of hyperseries with a natural derivation and composition with respect to . The present paper can be regarded as one important step in this direction.

1.2Strategy and outline of the main results

In order to construct a field of hyperseries that is closed under all hyperexponentials and all hyperlogarithms , we follow the common approach of starting with an arbitrary field of hyperseries and then closing it off via a transfinite sequence of extensions.

Now closing off under hyperlogarithms turns out to be much easier than closing off under hyperexponentiation. For this reason, and following [23, 29, 12], it is actually convenient to do this once and for all and only work with fields of hyperseries that are already closed under all hyperlogarithms. In particular, the smallest field of hyperseries of this type with an element is the field of logarithmic hyperseries from [12], where for all .

The next step is to work out the technical definition of a “field of hyperseries” that will be suitable for the hyperexponential extension process. Quite naturally, such a field should be a Hahn field of generalized power series, where is a totally ordered monomial group: see Subsection 2.2 for basic definitions and reminders. For reasons mentioned in the previous subsection, we also require the existence of a composition law , where . For each , this allows us to define a function by setting for .

We say that is a hyperserial field if the composition satisfies a list of natural axioms such as associativity and restricted Taylor expansions; see Section 6 for the full list of axioms. The only non-obvious axiom for traditional fields of transseries states that a transseries is a monomial if and only if (i.e. the support of only contains infinitely large elements). The only non-obvious axiom HF7 for hyperserial fields is a generalization of this axiom: if , then we require that the support of satisfies for any -atomic element . Here is said to be -atomic if is a monomial for all .

Our definition of hyperserial fields is similar to the definition of fields of transseries from [24, 29], with a few differences. The old definition includes an additional axiom of well-nestedness T4 which is important for the definition of derivations and compositions, but which is not required for the purposes of the present paper. Of course, our current presentation is based on the composition law . Finally, we use a slightly different technical notion of confluence. We say that is confluent if, for all ordinals and all , there exist a -atomic element and with . We refer to Remark 3.6 for a discussion of the differences with the definition from [29].

Given an ordinal , it turns out that the hyperlogarithm is entirely determined by its restriction to the set of -atomic elements. The field together with these restricted hyperlogarithms is called the hyperserial skeleton of . The fact that the logarithm can be recovered from its restriction to is a well-known fact. Indeed, we first recover on , since and for all . For all , , and infinitesimal , we then have

Hyperserial skeletons can also be defined in an abstract manner, i.e. without knowledge of a hyperserial field of which it is the skeleton. Precise definitions will be given in Section 3; for now it suffices to know that an abstract hyperserial skeleton is a field of generalized power series together with partially defined functions that satisfy suitable axioms. The first key result of this paper is the construction of an exact correspondence between abstract hyperserial skeletons and hyperserial fields. This correspondence preserves confluence for a suitable analogue of the confluence axiom for hyperserial skeletons.

Sections 4 and 5 contain the core of this construction. In Section 4, we first show how to extend the partial functions of a confluent hyperserial skeleton to all of . In Section 5, we prove that any confluent hyperserial skeleton can be endowed with a well-behaved composition law . In Section 6, we complete our construction of a correspondence between hyperserial skeletons and hyperserial fields. More precisely, we prove:

Theorem 1.1. If is a confluent hyperserial skeleton, then there is a unique function such that is a confluent hyperserial field with

Theorem 1.2. Let be a hyperserial field of force . Then the skeleton of is a hyperserial skeleton. Moreover, if is confluent, then so is its skeleton and coincides with the unique composition from Theorem 1.1.

Sections 7 and 8 are devoted to the closure of a confluent hyperserial field under hyperexponentiation. In view of Theorem 1.1, it suffices to operate on the level of hyperserial skeletons instead of hyperserial fields. In Section 7, we investigate when the hyperexponential of an element in already exists in . This gives us a criterion under which the extended hyperlogarithms are bijective. In Section 8, we prove our main theorem that every confluent hyperserial skeleton has a minimal extension whose extended hyperlogarithm functions are bijective:

Theorem 1.3. Let be a confluent hyperserial skeleton. Then has a confluent extension such that the function

is bijective for each ordinal . Moreover, if is another confluent extension and if the extended function is bijective for each , then there is a unique embedding of into over .

Corollary. There exists a minimal hyperserial extension of that is closed under for all ordinals .

2Preliminaries

2.1Set-theoretic notations and conventions

We work in von Neumann-Gdel-Bernays set theory with Global Choice (NBG), which is a conservative extension of ZFC. In this set theory, all proper classes are in bijective correspondence with the class of all ordinal numbers. We will sometimes write for elements that are either ordinals or equal to the class of ordinals. In that case, we write instead of . We make the convention that . If is a successor ordinal, then we define to be the unique ordinal with . If is a limit ordinal, then we define .

Recall that every ordinal has a unique Cantor normal form

where , and with . The ordinals are called the exponents of the Cantor normal form and the integers its coefficients. We write (resp. ) if each exponent of the Cantor normal form of satisfies (resp. ). We also define to be the unique ordinal with and with for some . Note that if and only if .

2.2Fields of well-based series

Well-based series.

Let be a linearly ordered abelian group (which may be a proper class). We let denote the class of functions whose support

is a well-based set, i.e. a set which is well-ordered for the reverse order .

We regard elements of as well-based series where for each . By [19], the class is a field for the operations

Note that each sum has finite support. We say that is a field of well-based series and that is the monomial group of . An element is called a monomial.

An increasing union of fields of well-based series is not, in general, a field of well-based series. However, this is always true if the union is indexed over :

Lemma 2.1. Let be a family of linearly ordered abelian groups such that whenever . Set for each , so for . Set . Then

Proof. Set . Clearly, , so it remains to show the other inclusion. Let . For each , let be the least with . Set

Then .

If , then we define

to be the dominant monomial of . We give the structure of a totally ordered field by setting

We define the asymptotic relations , , , and on by

The monomial group is naturally embedded in as an ordered group and

for all non-zero .

For and , we set . We say that a series is a truncation of , denoted , if there is with . We have if and only if (which holds vacuously when ). We finally define

Series in are called infinitesimal and series in are called positive infinite. Each can be decomposed uniquely as , where , , and is infinitesimal.

Well-based families.

If is a family in 𝕋, then we say that is well-based if

• is a well-based set, and

• is finite for all .

Then we may define the sum of as the series

If and are families, then we define their product as the family . By [25, Proposition 3.3], if and are well-based, then so is their product, and we have

We will frequently use the following facts regarding families for and .

Lemma 2.2. Consider a field of well-based series .

Let be another field of well-based series. If is -linear, then we say that is strongly linear if for every well-based family in 𝕋, the family in is well-based, and

If is a function, then we say that it is well-based if for any well-based family in , the family in is well-based. Then extends uniquely into a strongly linear map [25, Proposition 3.5]. Moreover, is strictly increasing whenever is strictly increasing and it is a ring morphism whenever for all [25, Corollary 3.8]. In particular, if for all and is strictly increasing, then is well-based. Hence:

Proposition 2.3.

Let and be totally ordered by and consider an order-preserving map . Then there is a unique strongly linear function that extends . Moreover, if is a group morphism, then is an ordered field embedding.

If extends (so extends ), then the operator support of a function is the set . If is a well-based set, then is well-based; see [12, Lemma 2.9].

Definition 2.4. We define a function to be relatively well-based if

is well-based.

Proposition 2.5. Let be relatively well-based. Assume that and that is strictly increasing. Then is well-based and its strongly linear extension is injective.

Proof. Given a well-based subset , we have to show that is a well-based family. We have

so is a well-based subset of . For any , the set of pairs with forms a finite antichain. Since any with induces such a pair , it follows that the set of all such is also finite. This completes the proof that is well-based. To see that is injective, let and take with . The assumption that is strictly increasing gives , whence .

Real powers.

We say that has real powers, if it comes with a real power operation such that is a multiplicative ordered -vector space, i.e. an ordered -vector space with multiplication and real powering in the roles of addition and scalar multiplication. Any real power operation on extends to as follows: for , we set

(2.1)

and for where , , and , we set .

Proposition 2.6. For and we have

Proof. For , the first two relations follow from basic power series manipulations; see [25, Corollary 16]. The extension to the general case when is straightforward and left to the reader.

Assume now that and . Since , it suffices to show that . Write where , , and . Since , we have , so either , or and , or and . If , then , so . If and , then and . If and , then , so .

Thus, the extended real power operation gives the structure of a multiplicative ordered -vector space. Accordingly, we say that has real powers.

Power series operations.

and elements , we say that is defined at if the family is well-based.

Lemma 2.7. Suppose that is uncountable and let be a power series which is defined on . If , then for some .

Proof. We prove this by induction on . If , then set and write . Suppose that and let be the set of with . Fix and let be such that for all . Since , there exists an index with . Then , whence

In particular, is countable, whereas is uncountable, so .

Now suppose that and write . Assume that . By the induction hypothesis, we can find and such that . Fix such elements and let be the set of such that . By the special case when , we see that . Thus, for some .

2.3Logarithmic hyperseries

A central object in our work is the field of logarithmic hyperseries of [12], equipped with its natural derivation and composition . We briefly recall its definition and some of its properties.

Logarithmic hyperseries.

For each ordinal , there is an element which we call the -th iterated hyperlogarithm. Intuitively speaking, we have , , , ..., , , etc. Let be an ordinal of the form . We write for the monomial group of all formal products with . The group is naturally ordered by setting if for some with for all . We also have a real power operation on given by setting for . This operation extends to all of as described in the previous subsection.

We call the field of logarithmic hyperseries of strength . If are ordinals with , then we let denote the interval and we let denote the subgroup

As in [12], we write , and

We will sometimes write and . We have natural inclusions , which give natural inclusions .

Derivation on .

The field is equipped with a strongly linear derivation . Given and a logarithmic hypermonomial , we define the derivation of by

where . Note that . For and , we sometimes write . Equipped with its derivation, the field is an -field with small derivation, so for , we have

Moreover, is well-based, which implies the following variant of [12, Lemma 2.13]:

Lemma 2.8. Let , let be a field of well-based series, and let be a strongly linear field embedding. For and with , the family is well-based. Moreover, the map is a strongly linear field embedding.

Proof. Since is well-based and is a strongly linear field embedding, the set is well-based. Thus is well-based and , since . Let . For each , we have

Since is well-based and , it follows that is well-based and that the map is well-defined and strongly linear. For all , we also have

which shows that preserves multiplication.

Composition on .

In addition to its derivation, the field comes equipped with a composition law which is unique to satisfy:

• For , the map is a strongly linear field embedding. As a consequence this map preserves the relations and [12, Lemma 6.6].

• For and , we have [12, Proposition 7.14].

• For and , we have [12, Corollary 7.5].

• For and , we have and [12, Section 1.4].

• For ordinals , we have [12, Corollary 5.11].

• For any successor ordinal , we have [12, Lemma 5.8].

• The constant term of vanishes if is a limit ordinal [12, Lemma 5.8].

• For and with , the family is well-based, and

  [12, Proposition 8.1]

The uniqueness follows from [12, Theorem 1.3]. By [12, Proposition 7.8], the derivation also satisfies the chain rule: for all and , we have

As we will see, the field equipped with the composition is hyperserial.

For , the unique composition from above restricts to a composition . For , the map defined by is a strongly linear field embedding with image by [12, Lemma 5.13]. Accordingly, for , we let denote the unique series in with . Note that for all and that, more generally, for and . For and we have

(2.2)

where is the derivation on (see [12, Section 5.1]). Let . Then is strongly linear and , so, by [12, Lemma 2.2],

(2.3)

In particular,

(2.4)

Lemma 2.9. For each , each , and each , we have .

Proof. Since is closed under taking derivatives and the derivation preserves infinitesimals, it suffices to prove the lemma for . We have , so

Since and , this yields . Since as well, we have . Since the map maps onto , we conclude that .

3Hyperserial skeletons

3.1Domain of definition

We let be an ordered field of well-based series with real powers. Let be an ordinal with . Given a structure where are partial functions on , we consider the following axioms for :

Suppose satisfies all axioms DD for . We set for all and we extend this notation to the case when , by setting

(3.1)

For , we call the class of -atomic elements. Note that for all . We let be the identity function with and, for with Cantor normal form , we define . Here we understand that whenever , , and so on until .

Proposition 3.1. For with , we have

Proof. Given and , let us first show by induction on that is defined and in . This holds for by definition. Let and assume that the assertion holds strictly below . If , then . Assume and let , and be such that . We have so by definition. In particular , so our inductive hypothesis on applied to gives that is a monomial.

Given such that and for all , let us next show by induction that . This is clear if . Let be such that the statement holds strictly below . If is a successor, then for and , we have so for all , whence . Assume now that is a limit and let . Then for all , so the induction hypothesis yields . We again conclude that .

3.2Axioms for the hyperlogarithms

Let be an ordered field of well-based series with real powers, let , and let be partial functions on which satisfy the axioms DD for all . We consider the following axioms, where is an ordinal with .

We define a logarithm as follows:

(3.2)

Then is an ordered -vector subspace of . For with , we consider the following axiom:

Remark 3.2. The axiom P allows us to define the infinite product for to be the unique monomial with , hence the name. Note that the axiom is a consequence of FE₀: if FE₀ holds, then for and , we have .

Definition 3.3. Let . A hyperserial skeleton of force is a structure where is an ordered field of well-based series with real powers and are partial functions on which satisfy DD, FE, A, M, and R for all , as well as P for all with .

Note that a hyperserial skeleton of force 0 is just a field of well-based series with real powers and that is a hyperserial skeleton of force if and only if is a hyperserial skeleton of force for each ordinal . We will often write to denote a hyperserial skeleton (of force ), where it is implied that for , the term refers to the -th hyperlogarithm on .

Definition 3.4. Let and be hyperserial skeletons of force . We say that a function is an embedding of force if it is a strongly linear strictly increasing ring morphism with for each such that

and such that

If is an embedding of force , then we say that is an extension of of force .

3.3Confluence

In this subsection, let be a hyperserial skeleton of force and let with . We inductively define the notion of -confluence in conjunction with functions and the classes , as follows:

Definition 3.5. The field is said to be -confluent if is non-trivial. The function maps each to its dominant monomial . For each , we set

Let with , let , and suppose is -confluent for all .

If each class contains an -atomic element, then we say that is -confluent. We will see that each class contains at most one -atomic element, which we denote by .

Remark 3.6. We note that -confluence is somewhat stronger than the similar notion of -confluence from [29], due to the extra requirement that we have maps .

Lemma 3.7. Let with and suppose is -confluent. Then the function is well-defined. Moreover, we have for all and .

Proof. We prove this by induction on , noticing that the case is trivial. Assume that this is the case for all ordinals and let . To see that is well-defined, let with . We need to show .

Assume that is a successor. Take with Since is -atomic for each and since is well-defined by our induction hypothesis, we have for each . It follows by induction on that for each and, likewise, for each , so . As both and are monomials, we have . The axiom implies that is injective and thus .

Assume now that is a limit and take with . Since is -atomic and since is well-defined by our induction hypothesis, we have . Likewise, , so . As both and are monomials, we have . Since is injective by , we conclude that .

As to our second assertion, consider and with . If is a successor, then the inductive hypothesis implies , so and . If is a limit, then , so and .

Corollary 3.8. Let with . If is -confluent, then for all .

Proposition 3.9. Let with . If is -confluent for all , then the class is convex for each . Moreover, if is -confluent, then is non-decreasing.

Proof. We prove this by induction on . Let . It is clear that is convex and that is increasing. Let and assume that the result holds for all . By the monotonicity axioms, each function is strictly increasing on (when , one also needs to use FE₀ to see that for ). As the composition of non-decreasing functions is non-decreasing, the function is non-decreasing for each and each . We deduce that is non-decreasing and that the classes are convex.

If is -confluent for all , then the proposition implies that the classes with form a partition of into convex subclasses. If is also -confluent, then we have the following explicit decomposition for all :

Definition 3.10. is said to be confluent if it is -confluent for each with . An extension/embedding of force is confluent if is confluent.

Note that if , then 𝕋 is confluent if and only if it is -confluent.

3.4The case of logarithmic hyperseries

Let be an ordinal and set . The goal of this section is to check that is a confluent hyperserial skeleton of force . This is immediate for , so we assume that .

Definition 3.11. Let and for , let . Given , set

We will show that is a hyperserial skeleton by checking that the axioms are satisfied. We begin with the domain of definition axioms.

Lemma 3.12. satisfies DD and , for all .

Proof. We prove this by induction on . The case when is immediate. For , consider an infinite monomial . We have , which is a monomial if and only for some . Conversely, for each we have . Now let and suppose that the lemma holds for all non-zero ordinals less than . Assume that is a limit. We have , whence

Assume now that is a successor. If , then where , and we clearly have for all , whence . Conversely, let . Then where . If is a limit, then , whence and . If is a successor, then for some and some , so

Since , we see that

Since , we must have , so .

For and , note that . Note also that the notions of -atomicity and -atomicity coincide in whenever is a limit with . This will not be the case in general.

Proposition 3.13. The field satisfies P for all .

Proof. Let and let . By Remark 3.2, we may assume . We have for some . Let be a sequence of real numbers. We have

This sum coincides with where .

Proposition 3.14. The field satisfies R, A, and M, for all .

Proof. Let and let . We have for some . Write where , , and if is a limit. We claim . If is a successor, then since , we have

If is a limit, then , so

Now we move on to verification of R, A, and M. The only elements in are and possibly 1 (if ), so for all and , which proves R. For , we have

so A holds as well.

As to M, take with . We have for some with . Write where , , and if is a limit. The argument above gives . If , then and if , then and . In either case, M is satisfied.

Recall that for and , we write for the real exponent of in . Given , we define to be the least ordinal with ; see also [12, p. 23].

Proposition 3.15. is -confluent. More precisely, for and , we have

(3.3)

Proof. We first note that is -confluent as is not trivial. We proceed by induction on . Take . If , then we have where is -atomic, so and is -confluent. It remains to note that .

Now suppose that and assume that is -confluent and satisfies (3.3) for all . Suppose is a successor, so . Write with and with if is a limit. We have , so

and .

Now suppose is a limit, so there is with . By hypothesis, we have that and so

Again, this yields .

Theorem 3.16. is a confluent hyperserial skeleton of force .

Proof. Using the identity

for , the field is easily seen to satisfy FE₀, A₀, M₀, and R₀. Moreover, satisfies FE for all by [12, Lemma 5.6]. Using Propositions 3.13, 3.14 and 3.15, we conclude that is a confluent hyperserial skeleton of force .

Corollary 3.17. is a confluent hyperserial skeleton of force .

4Extending the partial functions

Let . The purpose of the next two sections is to prove the following theorem:

Theorem 4.1. Let be a confluent hyperserial skeleton of force . There is a unique function satisfying:

We claim that it suffices to prove the theorem in the case when . The case when can then be proved as follows: let be a confluent hyperserial skeleton of force On. Then for every , there exists a unique composition that satisfies C1, C2, C3, and C4. For , the composition extends , by uniqueness. For any and , we have for some , so we may define and this definition does not depend on . It is straightforward to check that this defines the unique composition which satisfies C1, C2, C3, and C4.

Throughout this section, we fix an ordinal and a hyperserial skeleton of force . We fix also such that is -confluent and we set . We assume that Theorem 4.1 holds for , so we have a unique composition satisfying , , , and . For and , we write . In light of Lemma 2.9, the expression makes sense for each . Our main goal is to prove the following result:

Proposition 4.2. There is an extension of to such that for all , , and with , we have

We will also prove that satisfies the extension of FE to (Proposition 4.13), that has Taylor expansions around every point (Proposition 4.15) and that it is strictly increasing on (Lemma 4.17).

Our extension will heavily depend on Taylor series expansions, so it is convenient to introduce some notation for that. Let be such that for all . Let and with . By Lemma 2.8 with , in place of , and , we have that the family is well-based. We define

4.1Extending the logarithm

Here . For , we define

and

Note that and . By [25, Corollary 16], we have

(4.1)

(4.2)

(4.3)

Proposition 4.3. There is a unique extension of into an ordered group embedding

with

For , writing for , , and , we have

Proof. The uniqueness and the fact that is a morphism are proven in [29, Example 2.1.3 and Lemma 2.1.4]. To see that is order-preserving, we need only check that for all . If , then and we have . If and , then we have , since . If , we have , so .

For , we often write in place of . For , we define to be the unique element of with . If , then we sometimes use instead of .

Proposition 4.4. For , we have .

Proof. Let , where , , and . If , then , so . If , then . If , then , since , , and . Thus

If , then and . Hence and . If , then is negative and infinite, so .

Remark 4.5. Proposition 4.4 proves that satisfies the properties of transseries fields in [29, Definition 2.2.1] except possibly for the axiom .

Proposition 4.6. For , and , we have .

Proof. First, note that for all : if , then this is just axiom FE₀; if , then ; if , then . Now, writing with , , and , we have

			(by (4.3))
			(by ())

			(by (4.3))
			(by (4.1))

Proposition 4.7. For and with , the family is well-based, with

Proof. For and , we have and . For , we have

So the family is well-based with . The proposition follows, as

4.2Extending the hyperlogarithms

Assume now that . Let us revisit the notion of confluence.

Lemma 4.8. Let and suppose that for some . Then for all with .

Proof. We first show that . Take and such that . We have

where . Set , so . We have

where . Thus, .

Now, fix with and set . By and , we have

Lemma 2.9 in conjunction with the fact that gives us that , so .

Proposition 4.9. For all , we have

Proof. We fix . Since , we know by Lemma 4.8 that it is enough to show that We proceed by induction on . If , then and

An easy induction on yields for each , whence the result.

Now suppose that . If is a successor, then for each there is some with . By our inductive assumption applied to , we have that for some . By Lemma 4.8, we have and an easy induction on gives us that . Thus, we have that for some . Likewise, for some . By replacing and with and invoking Lemma 4.8, we may assume that . Since , we have . On the other hand, given , if for some , then take some with . By Lemma 4.8, we have , so .

If is a limit, then for each there is with . By our inductive assumption applied to , we have that for some , so by Lemma 4.8. Thus and likewise, for some . By replacing and with and invoking Lemma 4.8, we may assume that . Since , we have . On the other hand, given , if for some , then take some with . By Lemma 4.8, we have , so .

Proposition 4.9 in conjunction with Lemma 4.8 gives us the following corollary:

Corollary 4.10. For each there is such that

for all . Moreover, if for some and some , then .

Definition 4.11. Let and let with . We define

As discussed at the beginning of the section, the series exists in by Lemmas 2.8 and 2.9. To prove Proposition 4.2 all that remains is to show:

Lemma 4.12. The above definition does not depend on the choice of .

Proof. Let , , be as in Definition 4.11 and suppose that for some . Set . We need to show that

Without loss of generality, we may assume that . Now

Since , this yields . Let

considered as formal power series and in Then

so it suffices to show that . For each , we have

so for all , and we conclude that by Lemma 2.7.

We end this section with various extensions of the validity of Taylor series expansions and a proof that is strictly increasing on .

Proposition 4.13. Assume is a successor. For , we have .

Proof. By Corollary 4.10, there is some such that . We may write

Note that is -atomic, so . For we have

so for all . It follows that

			(by Definition 4.11)
			(by FE)
			(by Definition 4.11)

This concludes the proof.

Lemma 4.14. For all , , and , we have

Proof. By applying to for , we have

Arguing as in the proof of Lemma 4.12, it is enough to show that

as power series in . Let . We have

Therefore,

Since , we are done by Lemma 2.7.

Proposition 4.15. For and with , we have

Proof. Let with . Set . By Lemmas 2.8 and 2.9, the series exists in . We claim that . As by , it suffices to show that

as power series in . But this follows from Lemma 2.7, by noting that the equality holds when evaluated at any element of .

Now set and let , so . By definition of and the above claim, we have

Using , it follows that

By Lemma 4.14, we conclude that

where the last equality follows from the definition of .

Lemma 4.16. Let , let , and let with

Then where .

Proof. Set , so . We have

where the first and third equalities follow from the definition of and where the second equality holds by Lemma 4.14.

Lemma 4.17. The function is strictly increasing on .

Proof. By induction on , we may assume that is strictly increasing on for all (the case follows from Proposition 4.3). As a composition of strictly increasing functions is strictly increasing, the function is strictly increasing on for all . Given , let us show that . We start with the case when and take with and . Then is infinitesimal and positive by our induction hypothesis. By Lemma 4.16, we have

Since , we have , so .

Now we turn to the case when . Set and and take an ordinal with

Set , so

Repeated applications of (2.4) with in place of gives , so and

Since , we have so . Thus, . All together, this shows that . Likewise, we have . By the monotonicity axiom M, we have , so .

5Compositions on confluent hyperserial skeletons

Throughout this section, stands for a fixed ordinal and for a fixed confluent hyperserial skeleton of force . We let . Our aim is to construct a well-behaved external composition that satisfies C1, C2, C3, and C4 from Theorem 4.1. We will also prove that the mapping has relatively well-based support for all . Throughout the section, we make the inductive assumption that Theorem 4.1 holds for all and that the mapping has relatively well-based support for all and .

5.1The case when

Here is a -confluent hyperserial skeleton of force . The field is the field of well-based series of real powers of the variable , with real coefficients.

Lemma 5.1. If is well-based, then is well-based for all .

Proof. Let with , and . Note that . Since and are both well-based, we are done.

Given and , the family is well-based by the above lemma, so we may define

One easily verifies that this composition satisfies and . We next prove

Proposition 5.2. Let , , and . We have .

Proof. Write where , , and . We have , so . We also have

Since by , we only need to show that . Now for some , so

by Proposition 2.6.

Corollary 5.3. Let , , and . We have .

Proof. We have

where the second equality follows from Proposition 5.2 and the third follows from strong linearity of composition with .

Proposition 5.4. For , and with , we have .

Proof. We first handle the case when , where . We have , so

For , we also have , so . Therefore,

Now, Lemma 2.8 gives that the the map is well-based and strongly linear, so for a general , we have

The above results show that satisfies , and . To complete the proof of Theorem 4.1 for , it remains to show uniqueness.

Proposition 5.5. The function is unique to satisfy , , , and

Proof. Let be a composition satisfying conditions , , , and Write , where , , and . By strong linearity, it suffices to verify that for any monomial in . Given , the condition implies

We have , so

We have by and by , so . Likewise, , so

5.2C1 and C2 for

For the remainder of this section, we assume that . By the results in Section 4, we have a well-defined extension of to all of for each . Indeed, for and , take with with (so if is a limit). Then we may set .

Given and , we have by that , so we set . Clearly, the map is an embedding of monomial groups which preserves real powers, and by , this embedding is order-preserving as well. For , we set . By Proposition 2.3, we have:

Lemma 5.6. The map is a strongly linear ordered field embedding.

By Lemma 2.8 with , the series exists in for any .

Lemma 5.7. Let , , and . We have

Proof. If is a limit ordinal, then the lemma follows from for any ordinal with , so we may assume that is a successor. We prove the lemma by induction on . The lemma is immediate when , so suppose and take and with . Our induction hypothesis yields

Note that and . We claim that

When , this just follows from . When , this is Proposition 4.7 with in place of and in place of . When , this is Definition 4.11 with in place of and in place of . Since and , it remains to show that . Now as series in . Indeed, for , we have

We conclude by Lemma 2.7.

Lemma 5.6 shows that C1 holds if . In the general situation when , our next goal is to show that the family is well-based. For the remainder of this subsection, we fix . By -confluence and Corollary 4.10, take and such that for all . If is a successor, we can arrange that . Set , set , and set .

Lemma 5.8. Let and let . If is a successor or , then the expression is defined and equal to .

Proof. Suppose is a successor ordinal, so . Then , so is defined. As the maps and are strongly linear, we may assume that is a monomial . Since for , we have

Now suppose that is a limit and that for some . By increasing , we may assume that , so . Then and give

Lemma 5.9. There is a well-based family from such that

for each with .

Proof. Fix with . We first claim that

If is a limit, then take with . Then , so gives

and gives , thereby proving the claim. If is a successor, then take with . By Lemma 5.7 and the fact that , we have

Having proved our claim, let be given and set . Lemma 2.9 yields , whence . If is a limit, then , where is as above. So in both the successor and limit cases, we may apply Lemma 5.8 with in place of to get

This gives

It remains to show that the family is well-based. Since is a well-based family in and is strongly linear, the family is well-based. Since is well-based and infinitesimal, the family is well-based. We conclude that the family is well-based.

Proposition 5.10. Let be a sequence of real numbers. Then the family is well-based and the series lies in .

Proof. We will show the following:

1. For each , the family is well-based and

   

2. The family is well-based and

   

The proposition follows from (a) and (b), since the union of finitely many well-based families is well-based and is closed under finite sums.

To see why (a) holds, let and note that

Since is well-based, gives that is well-based. We have

Set . We claim that . If , then and

If , then gives

As for (b), let . By Lemma 5.9, there exists a well-based family from such that

The families and are well-based by Lemma 5.6 and the fact that . Since the family is also well-based, it follows that is again well-based. In particular,

is well-based. Now

Since and are infinitesimal for all , we may write

where By (4.1), we have . Furthermore, P implies

We conclude that .

Let . In light of Proposition 5.10, we define

We note that the map is an embedding of ordered multiplicative groups for each .

Our next objective is to show that the map extends by strong linearity to a map which satisfies C1 and C2. For this, we will show that is a relatively well-based mapping, by using a similar “gluing” technique as for Proposition 5.10. Recall that our second induction hypothesis from the beginning of this section stipulated that the mapping is relatively well-based for all and .

Proposition 5.11. Let be the map . Then is relatively well-based.

Proof. Let be the restriction of to and for , let be the restriction of to . Since

it suffices to show that each and are relatively well-based. For the , fix . Our induction hypothesis implies that the map is relatively well-based. By Lemma 5.8 with in place of , we have

It follows that is also relatively well-based with .

Now for . Let . By Lemma 5.9, we have a well-based family from such that

Exponentiating both sides, we obtain

so . The set

is well-based, infinitesimal and does not depend on . Since

for all , we conclude that is well-based.

We already noted that the map from Proposition 5.11 is an order-preserving multiplicative embedding. By Proposition 2.5, it follows that is well-based, so it extends uniquely into an order-preserving and strongly linear embedding . Taking for all , this proves C1. By construction, we also have C2. Note that extends the unique composition of Theorem 4.1 for .

5.3Properties C3 and C4 and uniqueness for

Proposition 5.12. For and , we have .

Proof. As in Proposition 5.2, it suffices to prove that holds for each . For such , we have

By Proposition 4.6, we also have . By injectivity of the logarithm, we conclude that .

Lemma 5.13. For all and all , we have .

Proof. First, we note that for , we have

where the last equality uses the definition of . Now, let and write with , , and . Then and

Here we used the facts that and that composition with commutes with powers and infinite sums.

Proposition 5.14. The function satisfies C3, i.e. for all , , and we have .

Proof. We will show by induction on that for all , all , and all . If , then this follows from Proposition 5.12 and strong linearity.

Let , let and be fixed, and assume that the proposition holds whenever for some . By strong linearity, it suffices to prove that for all . Lemma 5.13 gives

Using the injectivity of and strong linearity, we may thus reduce to the case when for . Our induction hypothesis takes care of the case when is a limit ordinal or when , so we may assume that , where . By the inductive definitions of and , we may further reduce to the case when . Lemma 5.13 takes care of the case , so we may assume that . In summary, we thus need to show that , where .

Set . We claim that . We have , where , , and if is a limit ordinal. As , we have

This gives

where the first equality in the second line follows from Proposition 4.13.

Having proved our claim, let us now show that . Take with , and . We have

As and for all , by Lemma 2.9, our induction hypothesis applied to gives

for . Along with C1, we thus have

Using also our claim that , we obtain

It remains to show that . Now

so and . We may thus apply Lemma 4.16 to and , to conclude that .

Proposition 5.15. For , and with , we have

Proof. Since holds for , we need only consider the case when is a successor and . We prove the result by induction on . By Proposition 4.7 (when ) or Proposition 4.15 (when ), we have . Assume that and write with . We have

Since , the induction hypothesis yields

Since , it remains to show that . It is enough to show that as power series in . This follows from Lemma 2.7, since

for all .

Proposition 5.16. The function satisfies C4, i.e. for all , all and all with , we have

Proof. Fix and with . Let be the map given by

We need to show that for all . By Lemma 2.8, the map is strongly linear, so it suffices to show that for all . Since is injective, it is enough to show that . Now by Lemma 5.13 and by [12, Lemma 8.3]. By Proposition 5.15 and strong linearity, we have

We conclude that .

To conclude our proof of Theorem 4.1, we prove the uniqueness of .

Proposition 5.17. The function is unique to satisfy C1, C2, C3, and C4.

Proof. Let be a composition satisfying conditions C1, C2, C3, and C4 and let . We first show that . Write , with , , and . By C4, we have

For , we have , so C2 gives

Thus, it remains to show that . Using C2, C3, and the identity , we see that

Likewise .

Now we turn to the task of showing that for . We make the inductive assumption that for and , we have (if , this is Proposition 5.5). By strong linearity, it suffices to verify that for any monomial . As and likewise for , it suffices to show this only for . Given , we have by C3 that

Thus, it suffices to show that for all . By our induction hypothesis, we only need to handle the case that is a successor and . If , then by Proposition 4.9, there is an ordinal with . Our inductive hypothesis and Lemma 2.9 yield

			(for )

Thus,

			(by C4)

Now suppose and assume by induction that for all . Take with . Then C3 and our inductive assumption gives

This concludes the proof.

6Hyperserial fields

We are now in a position to prove Theorems 1.1 and 1.2. Let be a field of well-based series, let , and let be a function. For and , we define as follows: set , set if , and set if . For with , we define to be the class of series with for all . We say that is a hyperserial field of force if the following axioms are satisfied:

HF1

is a strongly -linear ordered field embedding for all .

HF2

for all , , and .

HF3

for all , , and with .

HF4

for all ordinals , , and all with .

HF5

The map described above is a real power operation on .

HF6

for all .

HF7

for all and

for all , , and .

Axioms HF6 and HF7 only make sense when , so they are assumed to hold trivially when . We say that is confluent if and if for all with and all , there exist and with

For the remainder of this section, we fix a hyperserial field of force . For each , we define the function . The skeleton of is defined to be the structure equipped with the real power operation on given by HF5. The main purpose of this section is to prove the following refinement of Theorem 1.2.

Theorem 6.1. The skeleton of is a hyperserial skeleton. Moreover, if is confluent, then so is its skeleton and coincides with the unique composition from Theorem 4.1.

When , then the skeleton of is just the field itself with the real power operation on . Clearly, this is a hyperserial skeleton, as there are no axioms to verify. Moreover, it is 0-confluent so long as is, so Theorem 6.1 follows from Proposition 5.5, since clearly satisfies , , , and . Therefore, we may assume that . We will verify the various hyperserial skeleton axioms over the next few lemmas, beginning with the Domain of Definition axioms:

Lemma 6.2. The skeleton satisfies the axioms DD for all .

Proof. By definition, is the class of with . Since by HF5, the axiom DD holds. Let us fix and let us assume that holds for all . If is a limit, then

Suppose is a successor. The inclusion holds by definition, so we show the other inclusion. Let and let . Take and with . Then , so , by our inductive assumption. Repeated applications of HF2 give . Since is arbitrary, this gives .

Now for the functional equations, asymptotics, regularity, and monotonicity axioms:

Lemma 6.3. The skeleton satisfies the axioms FE, A, and R for all .

Proof. Given and , we have

			(by HF2 and HF1)
			(by HF6)

so FE₀ holds. Let be a successor ordinal and let , so is defined and lies in . The axiom HF2 implies

so FE holds as well. The asymptotics axiom A₀ follows from the relation in and HF1. Likewise, A follows from the fact that for all . By HF1, we note that the sets and are mutually cofinal for each . The regularity axioms R for therefore follow from HF7.

Lemma 6.4. The skeleton satisfies the axioms M for all .

Proof. The axiom M₀ follows from the fact that . For , let and take with . We need to show

We first consider the case that for some with . Then HF4 gives us that . By (2.4), we have , where and . Since , we have

Since , we have , so . The axiom HF4 gives , so . Thus,

Now we handle the case that for all with . We claim that the sets

are mutually cofinal. Let be given and take with and . Then by assumption, so and HF4 gives . This proves the cofinality claim. Now, HF7 gives and likewise, . Thus,

In particular, , as desired.

Before proving the infinite powers axioms, we need a lemma:

Lemma 6.5. Let with , , and . Then

where is as defined in Subsection 4.1.

Proof. Set , so and . The axiom HF3 gives

We have by HF2, and . Hence

Given , we have , so for , we have

Thus, .

Lemma 6.6. The skeleton satisfies the axioms P for all with .

Proof. let with , let and let be a sequence of real numbers. We need to show that , where for and where . Set . We may assume that and, by negating each if need be, we further assume that . Hence is defined. The axioms HF1 and HF2 give

so it remains to show that . For each , we have . This gives . Take and with . Lemma 6.5 gives

The axiom HF7 gives . If , then , so . If , we have . As we have established that , it follows that and . Thus , as desired.

This shows that is a hyperserial skeleton of force . Now we turn to confluence. First, we need a lemma:

Lemma 6.7. Let and let . If , then and for all with . In particular, for all with .

Proof. The proof is essentially the same as the proof of Lemma 4.8. Take and with . By Lemma 6.5, we have

so . Set , so . Again, Lemma 6.5 gives

so . Now set and fix with . We have

Since , we have .

Lemma 6.8. Suppose is confluent. Then is confluent as well.

Proof. The skeleton is -confluent since is non-trivial. Let with and assume that is -confluent for all . We also make the inductive assumption that for and , we have for some . Let and take and with . We will show that . We first handle the case that is a successor. Take with . Lemma 6.7 gives . By assumption, we have for some , so , again by Lemma 6.7. Induction on gives for all , so

and . The case that is a limit is similar, though this time we take with and use that

to see that . Since was arbitrary, this gives that is -confluent.

Proof of Theorem 6.1. Lemmas 6.2, 6.3, 6.4, and 6.6 show that of is a hyperserial skeleton. The composition clearly satisfies C1, C2, C3, and C4. If is confluent, then is confluent by Lemma 6.8 and Proposition 5.17 implies that coincides with the unique composition from Theorem 4.1.

Given a confluent hyperserial skeleton of force , it is clear that the unique composition in Theorem 4.1 satisfies all of the hyperserial field axioms except for possibly HF4. In the course of our inductive proof in Sections 7 and 8, we will prove the following lemma (Lemma 7.5):

Lemma 6.9. Let be a confluent hyperserial skeleton of force and let be the composition law established in Theorem 4.1. Then the function is strictly increasing for all ordinals .

Thus, the unique composition in Theorem 4.1 satisfies HF4 as well. The proof of Lemma 7.5 will not rely on any of the results from this section. This gives us the following refinement of Theorem 1.1:

Theorem 6.10. If is a confluent hyperserial skeleton of force , then there is a unique function such that is a confluent hyperserial field of force with skeleton .

7Hyperexponentiation

Our goal for Sections 7 and 8 is to prove Theorem 1.3. We will actually prove a “relative” version of the theorem, for which we first need a few more definitions. Given a confluent hyperserial skeleton of force , we let be the composition from Theorem 4.1. For each , we let be the map given by .

Definition 7.1. Let be a confluent hyperserial skeleton of force and let . We say that has force if for each , the function is bijective.

Note that if has force , then is bijective for all .

Remark 7.2. Every confluent hyperserial skeleton of force is a confluent hyperserial skeleton of force . Given a set-sized field of transseries , we recall that the exponential function cannot be total [23, Proposition 2.2]. Thus, any confluent hyperserial skeleton of force with is necessarily a proper class.

Remark 7.3. Let be a hyperserial skeleton of force . Then is hyperserial of force if and only if is hyperserial of force for all . Similarly, is hyperserial of force if and only if is hyperserial of force for all .

We can now state the relative version of Theorem 1.3 that we are after:

Theorem 7.4. Let be a confluent hyperserial skeleton of force and let . Then has a confluent extension of force with the following property: if is another confluent hyperserial skeleton of force and if is an embedding of force , then there is a unique embedding of force that extends .

Theorem 1.3 follows from Theorem 7.4 by taking . Throughout Section 7 and Subsections 8.1, 8.2, 8.3, and 8.4, we fix a confluent hyperserial skeleton of force and an ordinal , and we make the induction hypothesis that Theorem 7.4 holds for . Note that this holds trivially if . Our main objective is to show that Theorem 7.4 still holds for instead of .

For this, we have to show how to define missing hyperexponentials of the form with . In this section, we start by giving a formula for hyperexponentials that are already defined in . In the next section, we show how to adjoin the missing hyperexponentials to .

Before we continue, let us fix some notation. Let

Given , we set

Note that and that . Given , we set

and we view , , and as functions from to . We define and analogously.

Given , we say that is defined if . If is of force , then is defined for all and . Lemma 4.17 tells us that is strictly increasing; in particular, it is injective. We let be its functional inverse, which is again strictly increasing. We may also consider as a partially defined function on .

Our induction hypothesis, that exists, has the following consequence:

Lemma 7.5. For , the function is strictly increasing on .

Proof. Let with . By our inductive assumption, and both exist in . As and are strictly increasing on and , we have and

7.1Local inversion of the hyperlogarithms

In this subsection, we study the range of the functions for and give a formula for their partial functional inverses. We fix and set . We also fix . For , we define series inductively by

Intuitively speaking, behaves like , whereas the sum behaves like for , and thereby provides a functional inverse of on a neighborhood of .

Proposition 7.6. Let with . Then the family is well-based and for .

Proof. Consider the derivative on . We claim that for all . This is clear for . Assuming that the claim holds for a given , we have

In light of this claim, we have . Recall that has well-based operator support as an operator on , so

Consider the strongly linear map

and set

so is well-based and . For , we have , so for , there exist with

This gives us

and it follows that

As , we have , so we deduce that is well-based and that for .

For our next result, we need a combinatorial lemma for power series over a differential field. Let be a differential field. Then the ring is naturally equipped with two derivations:

We also have a composition given by

for . This composition cooperates with our derivations as follows:

Lemma 7.7. Let and . Write and assume that we have

for each and , where . Then .

Proof. The last two assumptions give us the following identities

			(7.1)
			(7.2)

We claim that . Indeed, we have

			(by (7.1))
			(by (7.2))
			(since )

Write . The identity yields for each . Since , we conclude that and for .

Lemma 7.8. Let with . Then

(7.3)

Proof. We have

Consider the formal power series

Writing , we have

Thus, it suffices to show that .

Let and . Then by factoring out from the inner sum and reindexing, we have

Note that the sequence satisfies the identities:

Since , the sequence satisfies the identities

Setting , we have

Using Lemma 7.7, we conclude that .

Proposition 7.9. The map is a bijection from to .

Proof. Let and let . We have , so

Since , we have

so . This gives .

Conversely, given , Lemma 7.8 yields . Let us show by induction on that . We have . Assuming that , we have

We have

so . This gives

It follows that for each , so . Since , we conclude that .

7.2Truncated series

Definition 7.10. We say that a series is -truncated if it is purely infinite, i.e. if . For , we say that is -truncated if for all and all . Let denote the class of -truncated series in .

In Subsection 3.3, we showed for that the class can be partitioned into convex subclasses , each of which contains a unique -atomic element . In this section, we describe a different partition of into convex subclasses, each of which will contain a unique -truncated series . We will then show that is bijective provided that . This was done in [29] for , but we provide a short proof below. First, for , set , so is 1-truncated and . We also set .

Proposition 7.11. [29, Proposition 2.3.8] For , we have if and only if . Thus, the function is bijective if and only if .

Proof. Let and let , and with . We have , since . Thus, we have if and only if , since is an additive subgroup of .

As a related fact for later use, we also note the following:

Lemma 7.12. For , we have . Thus, if and only if . Moreover, is a bijection between and for each .

Proof. Given , write , where , , and . We have

R₀ and M₀ give that and, as is a subgroup of , it follows that . Thus, is 1-truncated. If , then and if , then , so . Thus, , as desired. The fact that if and only if follows from this and the fact that is injective. Now assume that and let . Then

so . By Proposition 7.11, .

For the remainder of this subsection, we assume that .

Lemma 7.13. We have . If is a successor, then .

Proof. For and , we have and so . Assume now that is a successor and let and . Again, . Take with . Then for all and , we have

so .

Lemma 7.14. Let and let . Then is -truncated if and only if for all .

Proof. We have for all since the series is infinite. Let and let . By Lemma 7.5, the function is strictly increasing, so we have if and only if , hence the result.

By Lemma 7.14 and R, the series is -truncated for all . The axiom R₀ also gives that is -truncated for .

Lemma 7.15. Let with and let . Then .

Proof. Take with . Then Lemma 7.5 gives , so it is enough to prove that . For this, we may show that in . As the map is order-preserving, it is enough to show that

This follows from Lemma 7.5 and the fact that .

Definition 7.16. For , we define

Proposition 7.17. The classes form a partition of into convex subclasses.

Proof. Let . The convexity of follows immediately from the definition of and Lemma 7.5. Let . We claim that , from which it follows by symmetry that . This clearly holds if , so assume that .

We first show that . Let and let with for some . Given with , we have , whence . Therefore,

by Lemma 7.5, so for all such .

If is a successor, take with . Then and since , we have

If is a limit, take with , so that . Let us show that . Suppose for contradiction that . By (2.4), we have

Since , we have , so

Therefore,

This means that : a contradiction since .

Now let and let us show . This is clear if or if , so we assume that , , and are pairwise distinct. By our claim, we have and , so take with and . Note that

thus, . Lemmas 7.5 and 7.15 yield

If , then by definition. If , then , so by our claim.

Proposition 7.18. Let . Then the class contains exactly one -truncated element.

Proof. Let us first show that contains a -truncated element. Suppose that itself is not -truncated, let be greatest such that for some . Setting , we have , so by Lemma 7.15. Our assumption on therefore yields , whence .

We claim that is -truncated. Fix . By definition of , we have for all . Since , Lemma 7.15 gives for all , so . By definition, this means that for all . Since , we have , by Lemma 7.15. Thus, , as claimed.

Now let be -truncated series with . We need to show that . Take with . For , we have since is -truncated. Therefore,

so by Lemma 7.15. Thus . Since , we deduce , so . We also have , so the same argument gives and we conclude that .

For , we define to be the unique -truncated series in . Note that this definition extends the previous definition of . It follows from the proof of Proposition 7.18 that for all and that

Proposition 7.19. For we have

Proof. We have if and only if for some . Since for each , this is in turn equivalent to by Lemma 7.5 . Thus, if and only if for some , and it remains to show that for some if and only if for some . This follows from the fact that if , then , so .

Proposition 7.20. For each we have .

Proof. Let . Then there is with . Thus, and so by Proposition 7.9. Therefore, by Proposition 7.19.

Corollary 7.21. We have on . Thus, for , we have if and only if .

Proof. Let . Then by Proposition 7.20 and is -truncated by R and Lemma 7.14. Thus . The fact that if and only if follows from this and the fact that is injective.

Proposition 7.22. Assume that is a confluent hyperserial skeleton of force . Then for all . In particular, if is defined for , then is defined on .

Proof. We prove this by induction on . Let . By Proposition 7.20, we need only prove that . Let . By Proposition 7.19, there is a with . By Proposition 7.9, there is a with . Since is hyperserial of force , the hyperexponential is defined and

Finally, since , Lemma 4.8 and Proposition 4.9 imply .

Corollary 7.23. Assume that is a confluent hyperserial skeleton of force . Then we have whenever one of the sides is defined.

Corollary 7.24. The following are equivalent:

Proof. The equivalence between ) and ) follows from Proposition 7.22 and the fact that we have

for all . The equivalence between ) and ) follows directly from Proposition 7.22. The equivalence between ) and ) follows from Corollary 7.21.

7.3Useful properties of truncation

Throughout this subsection, we let and we set and . Given , it will be convenient to introduce the following notations:

Lemma 7.25. Let , , and . We have

Proof. We claim that if , then and

Assuming that , we have

whence . Now

so . Since , we have , so Lemma 7.5 gives

as desired. Composing with gives that if , then and

From which it follows that .

Corollary 7.26. Let with . Then .

Proof. We have . Let with . We have , so

by Lemma 7.5. Since by Lemma 7.25 and is convex, we are done.

Lemma 7.27. For each and each , we have

Proof. Take with . Since , we have by Lemma 7.5. This gives

Thus, . Likewise, since , we have

so . Lemma 7.5 gives , so we have

By Lemma 7.25, both and are elements of . Since is convex, this means that it also contains and .

We have the following useful consequence:

Corollary 7.28. Let be such that for some . Then

Proof. Take with . Then

We have by Lemma 7.27 and we have by Lemma 7.25, so . Likewise, . Since is convex, this yields . Since by Lemma 7.27, we conclude that .

Corollary 7.29. Let with . Then and .

Proof. As is strictly increasing, we have , which gives . We first claim that . If , then Corollary 7.28 gives that , so we may focus on the case when . Suppose towards contradiction that and that for some . Then

Since , we have , so . Since , we have

so by Proposition 7.19, a contradiction.

From our claim, we get . This yields , as . Take with . Lemma 7.25 gives

so since is convex and is strictly increasing.

8Hyperexponential extensions

In this section, is a confluent hyperserial skeleton of force and . Given we consider a class of -truncated series without -hyperexponentials in and show how to extend into a minimal confluent hyperserial skeleton of force that contains for all series . Most of the work in the case has already been done in [29], but Subsection 8.1 contains a self-contained treatment for our setting. For the construction of in Subsections 8.1, 8.2, 8.3, and 8.4, we recall that we made the induction hypothesis that Theorem 7.4 holds for . After the construction of , we conclude this section with the proofs of Theorems 7.4 and 1.3.