Constant power maps on Hardy fields and transseries
Let $\mathbb{T}$ be the differential field of logarithmic-exponential transseries. We consider the expansion of $\mathbb{T}$ by the binary map that sends a positive transseries $f$ and a real number $r$ to the transseries $f^r$, together with a constant symbol for the real number $\mathrm{e}$. Building on recent work of Aschenbrenner, van den Dries, and van der Hoeven, we show that this expansion is model complete, and we give an axiomatization of its theory that is effective relative to the theory of the real exponential field. We show that maximal Hardy fields, equipped with the same map $(f,r)\mapsto f^r$, enjoy the same theory as $\mathbb{T}$, and we use this to establish a transfer theorem between Hardy fields and transseries.