Valuation theory of exponential Hardy fields. I (Q1395393)

Let \(T\) be a theory of a polynomially bounded o-minimal expansion \({\mathcal P}\) of the ordered field of reals. Let \({\mathcal F}_T\) be the set of all o-definable functions of \({\mathcal P}\). It is assumed that \(T\) defines the restricted exponential and logarithmic functions. Denote by \(T(\exp)\) the theory of the expansion \(({\mathcal P},\exp),\) where \(\exp\) is the unrestricted real exponential function. Any model \({\mathcal R}\) of \(T(\exp)\) which contains \(({\mathbb R},+,\cdot,<,{\mathcal F}_T,\exp)\) is taken as a substructure. The Hardy field of \({\mathcal R},\) denoted by \(H({\mathcal R}),\) is the set of germs at \(\infty\) of unary \({\mathcal R}\)-definable functions \(f:{\mathcal R}\rightarrow {\mathcal R}.\) Then \(H({\mathcal R})\) is an ordered differential field. Let \(x\in H({\mathcal R})\) be the germ of the identity function. \(H({\mathcal R})\) is equal to the closure of its subfield \({\mathcal R}(x)\) under \({\mathcal F}_T\), exp and log. The valuation theoretical structure of this closure is analyzed. It is said that an infinitely increasing unary function \(f\) on \({\mathcal R}\) has level \(s\in {\mathbb Z}\) if there is \(N\in {\mathbb N}\) such that \(\log_{N+s}\circ f\) is asymptotic to \(\log_{N}\) on \({\mathcal R}.\) If every \({\mathcal R}\)-definable ultimately strictly increasing and unbounded unary function on \({\mathcal R}\) has a level then \({\mathcal R}\) is said to be levelled. It is proved that every definable function on \({\mathcal R}\) has a level, and this level is determined explicitly. Denote by \({\mathbb R}_{\text{an,powers}}\) the expansion of the ordered field of real numbers by the set \({\mathcal F}_{\text{an}}\) of restricted analytic functions and the power function \(P_r.\) It is proved that \(H({\mathbb R}_{\text{an,powers}})\) is maximal among the Hardy subfields of \(H({\mathbb R}_{\text{an},\exp})\) associated with polynomially bounded reducts of \({\mathbb R}_{\text{an},\exp}.\)