4. Proof of monotonicity

Fix $x$, $y$ as in the assumptions. Let $\gamma\in\mathbb{J}$. We shall prove the conclusion by induction on $\mathrm{ER}(\gamma)$.

When $\gamma$ is $\log^{\circ n}(T)$ for some $n$, both conclusions hold because $\log^{\circ n}$ is concave: $0<\frac{\log^{\circ n}(a)-\log^{\circ n}(b)}{a-b}\leq(\log^{\circ n})^{\prime}(b)$ for any $b$ in its domain and $a>b$, and so also for $x>y>\mathbb{R}$. The conclusion is trivial for $\gamma=0$.

Now assume $\mathrm{ER}(\gamma)>0$ and let $re^{\delta}$ be the leading term of $\gamma$. Recall that $\delta\in\mathbb{J}^{>0}$ and that $\mathrm{ER}(\delta)<\mathrm{ER}(\gamma)$. By Proposition 3.2, we have

which we rewrite as

Recall moreover that since $\gamma\sim re^{\delta}$ and $\gamma\not\asymp 1$, we have $\gamma^{\prime}\sim re^{\delta}\delta^{\prime}$, so in particular $\gamma^{\prime}\circ y\sim re^{\delta\circ y}(\delta^{\prime}\circ y)$.

We distinguish two cases. If $\delta\circ x-\delta\circ y\prec 1$, then we can use the Taylor expansion of $\exp$ to check that

where the second inequality follows from the inductive hypothesis (1). Therefore,

Both conclusions follow trivially.

Now suppose that $\delta\circ x-\delta\circ y\succeq 1$. Note in particular that $\gamma\circ x-\gamma\circ y\succ 1$, because $e^{\delta\circ y}\succ 1$ and $e^{\delta\circ x-\delta\circ y}-1\succeq 1$, so we only need to prove conclusion (2). By inductive hypothesis (2), $(\delta^{\prime}\circ y)(x-y)\succeq 1$, which with $e^{\delta\circ y}\succ 1$ yields (2):

Write

If $\gamma\circ x-\gamma\circ y\prec 1$, then using Lemma 4.1(1)

Otherwise, $e^{\gamma\circ x-\gamma\circ y}\not\sim 1$, and since $\gamma\circ x<\gamma\circ y$ by Proposition 3.1 applied to $-\gamma$, we have $e^{\gamma\circ x-\gamma\circ y}\preceq 1$, thus

where the last inequality follows from Lemma 4.1(2). ∎

Let $x,y\in\mathbb{U}$ with $x>y>\mathbb{R}$ and $f\in\mathbb{R}\langle\!\langle T\rangle\!\rangle$. Trivially, when $f^{\prime}=0$, we have $f=r\in\mathbb{R}$, so $r\circ x=r\circ y=r$, as desired. We now assume that $f^{\prime}>0$, and we want to prove $f\circ x>f\circ y$. The case $f^{\prime}<0$ will follow trivially by replacing $f$ with $-f$.

Case $f=T+\varepsilon$ with $\varepsilon\prec T$. Note that in this case $f^{\prime}\sim 1$, so $f^{\prime}>0$. We claim that $\varepsilon\circ x-\varepsilon\circ y\prec x-y$, and so $f\circ x-f\circ y\sim x-y$, which clearly implies $f\circ x>f\circ y$.

Suppose that $e^{\gamma}$ is a monomial in the support of $\varepsilon$. We claim that $e^{\gamma\circ x}-e^{\gamma\circ y}\prec x-y$. This is trivial for $\gamma=0$, and an immediate consequence of Proposition 3.2 for $\gamma>0$. For $\gamma<0$, we have $1\succ(e^{\gamma})^{\prime}$, so $1\succ(e^{\gamma})^{\prime}\circ y$, hence by Corollary 4.2

Taking the sum over all terms in $\varepsilon$, we find that $\varepsilon\circ x-\varepsilon\circ y\prec x-y$.

Case $f>\mathbb{R}$. Recall that $\mathbb{R}\langle\!\langle T\rangle\!\rangle$ is confluent, because for any $g\in\mathbb{R}\langle\!\langle T\rangle\!\rangle^{>\mathbb{R}}$, the leading monomials along the sequence $(\log^{\circ n}(g):n\in\mathbb{N})$ must have decreasing exponential rank, until one reaches $\log^{\circ k}(T)$ for some $k$. Pick $n\in\mathbb{N}$ such that $\log^{\circ n}(T)\circ f=\log^{\circ n}(f)=\log^{\circ k}(T)+\varepsilon$ for some $k\in\mathbb{N}$ and some $\varepsilon\prec\log^{\circ k}(T)$. Note that

where $\overline{\varepsilon}=\varepsilon\circ\exp^{\circ k}(T)\prec\log^{\circ k}(T)\circ\exp^{\circ k}(T)=T$. By the previous case, the function $x\mapsto x+(\overline{\varepsilon}\circ x)$ is strictly increasing. Since the functions $\log$ and $\exp$ are also strictly increasing on $\mathbb{U}^{>\mathbb{R}}$, then so is the function $x\mapsto f\circ x$.

Case $f\not>\mathbb{R}$. Since by assumption $f^{\prime}>0$, we cannot have $f<\mathbb{R}$, so there must be some $r\in\mathbb{R}$ such that $f-r\prec 1$, and moreover $f-r<0$. It follows that $g=-\frac{1}{f-r}>\mathbb{R}$. By the previous case, the function $x\mapsto g\circ x$ is strictly increasing, thus so is the function

Up to replacing $f$ with $-f$, we may assume that $f^{\prime}>0$. Since $f\not\asymp 1$, we have $f^{\prime}\succ g^{\prime}$, thus $f^{\prime}-rg^{\prime}=(f-rg)^{\prime}>0$ for every $r\in\mathbb{R}$. By Theorem A,

Moreover, $f\circ x-f\circ y>0$, and the conclusion follows. ∎

Apply Corollary 4.3 to $f$ and $f-g\prec f$. ∎

Fix $f\in\mathbb{R}\langle\!\langle T\rangle\!\rangle$, $x,y\in\mathbb{U}^{>\mathbb{R}}$, $w\in\mathbb{U}$ such that $f\circ x\leq w\leq f\circ y$. Note that the case $f\in\mathbb{R}$ is trivial, so assume $f\notin\mathbb{R}$. There is $z\in\mathbb{U}^{>\mathbb{R}}$ such that $f\circ z=w$: when $f>\mathbb{R}$, just take $z=f^{\mathrm{inv}}\circ w$, where $f^{\mathrm{inv}}\in\mathbb{R}\langle\!\langle T\rangle\!\rangle^{>\mathbb{R}}$ is the compositional inverse of $f$ ([6]); otherwise, replace $f$ with $\pm\frac{1}{f-r}>\mathbb{R}$ just as in the proof of Theorem A, and reduce to $f>\mathbb{R}$. By Theorem A, $z$ has to be between $x$ and $y$. ∎