% AUTOGENERATED FILE; you probably want to edit the .tex.in file, not this.
\input{preamble-article}
\pagestyle{headings}
\usepackage{amssymb,amsmath,enumerate,amsthm,url}
\usepackage[all,cmtip]{xy}
\usepackage{graphicx}
\providecommand{\Dashv}{\mathrel{\text{\reflectbox{$\vDash$}}}}
\bibliographystyle{alpha}
\begin{document}
\providecommand{\an}{\operatorname{an}}
\providecommand{\id}{\operatorname{id}}
\providecommand{\dom}{\operatorname{dom}}
\providecommand{\st}{\operatorname{st}}
\providecommand{\sign}{\operatorname{sign}}
\newcommand{\X}{{\overline{X}}}
\newcommand{\Y}{{\overline{Y}}}
\renewcommand{\Z}{{\overline{Z}}}
\newcommand{\w}{{\overline{w}}}
\newcommand{\x}{{\overline{x}}}
\newcommand{\y}{{\overline{y}}}
\newcommand{\z}{{\overline{z}}}
\renewcommand{\a}{{\overline{a}}}
\renewcommand{\b}{{\overline{b}}}
\renewcommand{\c}{{\overline{c}}}
\newcommand{\s}{{\overline{s}}}
\renewcommand{\k}{{\overline{k}}}

\newcommand{\Ran}{\R_{\an}}
\newcommand{\Lan}{L_{\an}}
\newcommand{\Tan}{T_{\an}}
\newcommand{\RanD}{\R_{\an}^D}
\newcommand{\LanD}{L_{\an}^D}
\newcommand{\TanD}{T_{\an}^D}
\providecommand{\alphabar}{\overline{\alpha}}
\providecommand{\etabar}{\overline{\eta}}
\renewcommand{\int}{\operatorname{int}}

\title{Model completeness and o-minimality of $\Ran$}
\maketitle

Notes on the Denef - van den Dries quantifier elimination for $\Ran$ and its 
consequences, written for a pair of seminars in Muenster, January 2018.

These notes are based in large part on some lecture notes by Alex Wilkie on 
the topic, currently available at:
\url{http://www.logique.jussieu.fr/modnet/Publications/Introductory\%20Notes\%20and\%20surveys/Wilkie.pdf}

A reader who has stumbled upon these notes and has not read Wilkie's notes 
should stop reading now and seek out Wilkie's notes instead. In these notes I 
attempt to spell out the odd thing left implicit in Wilkie's notes, but 
essentially these notes cover a proper subset of the material covered in 
Wilkie's notes, skip over many details handled nicely there, and indubitably 
add errors and imprecisions of their own.

\section{Analytic functions}

\subsection{Formal power series}

For $R$ a ring,
\[ R[[X]] := \{ \sum_{i \in \N} a_iX^i : a_i \in R \} \]
\[ R[[\X]] = R[[X_1,\ldots ,X_n]] = (\ldots ((R[[X_1]])[[X_2]])\ldots )[[X_n]] \]

If $F \in R[[\X]]$, we can write
\[ F = \sum_{\nu \in \N^n} a_\nu \X^\nu \]
where $\X^\nu := X_1^{\nu_1}\ldots X_n^{\nu_n}$.

$|\nu| := \max_i \nu_i$.

$F(0) :=$ constant term of $F = a_0$

For $R$ a ring, $R^* := \{ x \in R : \exists y \in R.\; xy=1 \} =$ multiplicative 
group of units.
\begin{lemma}
    For $F \in R[[\X]]$, $F \in R[[\X]]^*$ iff $F(0) \in R^*$.
\end{lemma}
\begin{proof}
    By induction, suffices to show when $\X=X$ is a single variable.

    If $FG = 1$ then $F(0)G(0)=1$.
    
    If $F = \sum a_iX^i$
    If $a_0b_0=1$, then define recursively for $n\geq 0$
    \[ b_{n+1} := -a_0^{-1}(a_1b_n + a_2b_{n-1} + \ldots  a_{n+1}b_0) .\]
    Then $\sum_{0\leq i\leq n+1} a_ib_{n+1-i} = 0$,
    so $(\sum a_iX^i)(\sum b_iX^i) = 1$.
\end{proof}

\subsection{Convergent power series}

For $F \in \R[[\X]]$, define
\begin{align*} \dom(\sum a_\nu\X^\nu)
  &:= \int( \{ \x \in \R^n : \sum a_\nu\x^\nu \mbox{ converges } \} ) \\
    & = \int( \{ \x : \{ a_\nu\x^\nu : \nu \} \mbox{ is bounded } \} ) \end{align*}

e.g.\ $\dom( \sum_\nu X^\nu Y^\nu ) = \{ (x,y) : xy < 1 \}$.

Let $\R\left<{\X}\right> := \{ F : 0 \in \dom(F) \}$.

\begin{fact}
    $\R\left<{\X}\right>$ is a subring of $\R[[\X]]$.
\end{fact}

Now $F = \sum a_\nu \X^\nu \in \R\left<{\X}\right>$ defines a function $\widetilde {F} : \dom(F) \rightarrow  
\R$; $\widetilde {F}(\x) := \sum a_\nu \x^\nu$.

\begin{fact}
    $\widetilde {F}=0$ iff $F=0$.
    $\widetilde {F} \in C^\infty(\dom(F))$.
\end{fact}

Say $f : U \rightarrow  \R$ is {\bf analytic} at $\b \in U$
if $f(\X-\b) = \widetilde {F}(\X)$ on $U_\b$, some $\b \in U_\b \subseteq _{\operatorname{op}} U$ and some $F \in 
\R\left<{\X}\right>$.

\begin{fact}
    $\widetilde {F}$ is analytic at every $b \in \dom(F)$.
\end{fact}
\begin{proof}[Idea of proof]
    show the Taylor series at $b$,
    \[ \sum_\nu 1/((\sum\nu)!) \widetilde {D^{\nu}F}(b) X^\nu \]
    where $D^{\nu} = D_1^{\nu_1}\ldots D_n^{\nu_n}$ where $D_i = d/dX_i$ is formal 
    derivation,
    converges near $b$.
    See [Krantz-Park "A primer of Real Analytic Functions" Proposition 2.2.7].
\end{proof}

\begin{fact}
    if $f$ is analytic at $b$ and $g$ is analytic at $f(b)$,
    then $(g \circ f)$ is analytic at $b$.
\end{fact}

\begin{corollary}
    \[ \R\left<{\X}\right>^* = \R[[\X]]^* \cap \R\left<{\X}\right> \]
\end{corollary}
\begin{proof}
    Suppose $F \in \R\left<{\X}\right>$ has non-zero constant term;
    WTS $F$ is invertible in $\R\left<{\X}\right>$.
    Multiplying $F$ by a constant, WMA $F(0)=1$.
    So say $F = 1-G$ where $G \in \R[[\X]]$ with $G(0)=0$.
    Let $H(X) := \sum X^i \in \R\left<{X}\right>$.
    Then $(1-X)H(X) = 1$,
    so $F(H\circ G) = F(\X)(H(G(\X)) = (1+G(\X))(H(G(\X))) = 1$
    and $H \circ G \in \R\left<{\X}\right>$ by the Fact.
\end{proof}

\subsection{Weierstrass Preparation}

Say $F \in \R[[\X,Y]]$ is {\bf regular} in $Y$
if some term $aY^p$ with $p\geq 0$ and $a\neq 0$ occurs in the power series $F$,
i.e.\ if ``$F(0,Y) \neq  0$''.

\begin{fact}[Weierstrass Preparation Theorem]
    If $F \in \R\left<{\X,Y}\right>$ is regular in $Y$,
    then exists $Q \in \R\left<{\X,Y}\right>^*$ and $L \in \R\left<{\X}\right>[Y]$,
    such that $F = QL$.
\end{fact}
    
\subsection{Denef - van den Dries Preparation}

\begin{fact}
    $\R\left<{\X}\right>$ is Noetherian; that is, any ideal is finitely generated.
\end{fact}

\begin{fact}
    The embedding $\R\left<{\X}\right> \leq  \R[[X]]$ is faithfully flat.
\end{fact}

I omit the definition of faithful flatness, because in fact we need only the 
following consequence.
\begin{fact} \label{cor:fflatlinear}
    If $F_i$,$F \in \R\left<{\X}\right>$
    and the linear equation $F_1x_1 + \ldots  F_nx_n = F$
    has a solution in $\R[[\X]]$,
    then it already has a solution in $\R\left<{\X}\right>$.
\end{fact}

\begin{corollary} \label{cor:fflatlinearUnit}
    If $F_i$,$F \in \R\left<{\X}\right>$
    and the linear equation $F_1x_1 + \ldots  F_nx_n = F$
    has a solution in $\R[[\X]]^*$,
    then it already has a solution in $\R\left<{\X}\right>^*$.
\end{corollary}
\begin{proof}
    Say $U_i \in \R[[\X]]^*$ is a solution.
    Then $\sum_i (F_i)(U_i(0) + \sum_j x_i^j X_j) = F$
    has a solution in $\R[[\X]]$,
    hence in $\R\left<{\X}\right>$.
    So since $U_i(0) \neq  0$,
    the original equation has a solution in $\R\left<{\X}\right>^*$.
\end{proof}

The following consequence of these facts is what we will need in the QE proof; 
I follow Wilkie in naming it as follows.

\begin{theorem}[Denef - van den Dries Preparation Theorem]
    If $F \in \R\left<{\X,\Y}\right>$
    then $F(\X,\Y) = \sum_{|\nu| < d} a_\nu(\X) \Y^\nu u_\nu(\X,\Y)$
    for some $d \in \N$, $a_\nu \in \R\left<{\X}\right>$, $u_\nu \in \R\left<{\X,\Y}\right>^*$.
\end{theorem}
\begin{proof}
    By induction on the length of $\Y$.
    So suppose for $\R\left<{\X,\Y}\right>$; we prove it for $\R\left<{\X,\Y,Z}\right>$.
    Let $F = \sum_{i \in \N} a_iZ^i \in \R\left<{\X,\Y,Z}\right>$, $a_i \in \R\left<{\X,\Y 
   }\right>$.
    $\R\left<{\X,\Y}\right>$ is Noetherian, so there exist $d \in \N$ and $b_{i,j} \in \R\left<{\X,\Y}\right>$
    such that $a_{d+i} = \sum_{i<d} b_{i,j} a_i$.
    So
    \begin{align*} F &= \sum_{i<d} a_iZ^i + \sum_{j\geq 0} \sum_{i<d} b_{i,j}a_iZ^{d+j} \\
    &= \sum_{i<d} a_iZ^i + \sum_{i<d} a_i Z^i Z^{d-i} \sum_{j\geq 0} b_{i,j}Z^j 
    \\
        &= \sum_{i<d} (a_iZ^i)(1 + Z^{d-i} \sum_{j\geq 0} b_{i,j}Z^j) \\
        &= \sum_{i<d} a_iZ^iu_i \end{align*}

    Here we have $u_i \in \R[[\X,\Y,Z]]^*$, and then by 
    Corollary~\ref{cor:fflatlinearUnit},
    we can find such $u_i \in \R\left<{\X,\Y,Z}\right>^*$.

    Now apply the inductive hypothesis to the $a_i$.
\end{proof}

\section{$\Ran$}

\[ \|\x\| := max_i |x_i| \]
\[ B_{<r} := \{ \x \in \R^n : \|\x\| < r \} \]
\[ B_{\leq r} := \{ \x \in \R^n : \|\x\| \leq  r \} \]

For $r>0$,
\[ \R\{\X\}_r := \{ F \in \R[[\X]] : B_{\leq r} \subseteq  \dom(F) \} ,\]
so $\R\left<{\X}\right> = \cap_{r \in \R_{>0}} \R\{\X\}_r$.

If $F \in \R\{\X\}_r$,
\[ \widetilde {F}\negmedspace\restriction_r(\x) := \begin{cases}
            \widetilde {F}(\x)  & \mbox{if } \x \in B_{<r} \\
             0      & \mbox{else }
             \end{cases} \]
"restricted analytic function".

Say $(r,F)$ is {\bf acceptable} if $r \in \R_{>0}$ and $F \in \R\{X\}_r$.

\[ \Ran := \{ \R; +,-,\cdot,<, (a)_{a \in \R}, (\widetilde {F}\negmedspace\restriction_r)_{(r,F) acceptable} \} \]
structure in language $\Lan$.

Let $\LanD := \Lan \cup \{D\}$, and $\RanD :=$ expansion of $\Ran$ 
interpreting $D$ by
    \[ D(x,y) := \begin{cases}
            x/y &\mbox{if } y\neq 0 \\
            0   &\mbox{if } y=0 \end{cases} \]

\begin{theorem}[Denef - van den Dries]
    $\TanD := Th(\RanD)$ has QE.
\end{theorem}

\begin{corollary}
    $\Tan := Th(\Ran)$ is model complete.
\end{corollary}
\begin{proof}
    Any qf $\LanD$-formula is equivalent to an existential $\Lan$-formula.
    
    For example, if $t_1,t_2$ are terms, then
    \[ \phi(D(t_1(x),t_2(x)))
        \Leftrightarrow  \exists z.\; ( \phi(z) \wedge
            ( (t_2(x) = 0 \wedge z=0) \vee (t_2(x) \neq  0 \wedge z\cdot t_2(x) = t_1(x)) ) 
            ). \]
\end{proof}

\begin{remark}
    Model completeness of $\Ran$ was previously proven (expressed in different
    but equivalent terms) by Gabrielov in the 1960s
    ("theorem of the complement" for subanalytic sets).

    %% Y \subseteq  \R^n is \underline{semi-analytic}
    %% if every b \in \R^n has an open neighbourhood U_b such that
    %% U_b \cap Y is a boolean combination of sets
    %% { f(x) > 0 } with f analytic at b.
    %% 
    %% Exercise: Y \subseteq  B_\leq r is qf-definable in \Ran iff semi-analytic.
    %%
    %% Z \subseteq  \R^n is \underline{sub-analytic}
    %% if every b \in \R^n has an open neighbourhood U_b such that
    %% U_b \cap Z is the image under a co-ordinate projection
    %% of a bounded semi-analytic set.
    %%
    %% Exercise: Y \subseteq  B_\leq r is existentially definable in \Ran iff
    %% sub-analytic.
    %%
    %% Theorem[Gabrielov, 1960s]: if Z is sub-analytic, so is \R^n \setminus Z.
    %%
    %% Exercise: This is *equivalent* to model completeness of \Ran.
\end{remark}


\subsection{o-minimality of $\Ran$}

\begin{lemma} \label{lem:omin1}
    Suppose $0 \neq  F \in \R\left<{X}\right>$.
    Then $F = X^mG$ for some unique $m \in \N$ and $G \in F[[X]]^*$,
    and $\dom(G) = \dom(F)$,
    and for some $\epsilon>0$,
    $\widetilde {F}$ has constant non-zero sign on $(0,\epsilon)$.
\end{lemma}
\begin{proof}
    Existence and uniqueness of $m$,$G$ is immediate from the description of 
    $F[[X]]^*$.
    For $\dom(G) = \dom(X^mG)$:
    given $x \in \R$, $\{ a_ix^i \}$ is bounded iff $\{ a_ix^{m+i} = 
    x^m(a_ix^i) \}$ is.

    Now $G$ has non-zero constant term and $\widetilde {G}$ is continuous, so $\widetilde {G}$ and hence $\widetilde {F}$
    has constant non-zero sign on some $(0,\epsilon)$.
\end{proof}

\begin{lemma} \label{lem:omin2}
    Let $t(x)$ be an $\LanD$-term in 1 variable.
    Exists $\epsilon > 0$ s.t.
    $t(x) = 0$ on $(0,\epsilon)$
    or $t(x) = (x^m\widetilde {F}(x))$ on $(0,\epsilon)$
    for some $m \in \Z$ and $F \in \R[[X]]^* \cap \R\{X\}_\epsilon$.
    In particular, $t(x)$ has constant sign on $(0,\epsilon)$.
\end{lemma}
\begin{proof}
    By induction on terms.
    Obvious for $t(x)=x$ or $t(x)=b$.

    Suppose $t(x) = t_1(x)+t_2(x)$ and $t_i(x)$ are as required.
    If either $t_i(x) = 0$ on $(0,\epsilon_i)$, this is clear.
    Else, say $t_i(x) = x^{m_i}\widetilde {F}_i(x)$ on $(0,\epsilon_i)$
    with $F_i \in \R[[X]]^* \cap \R\{X\}_{\epsilon_i}$.
    Say $m_1 \leq  m_2$.
    then $t_1(x)+t_2(x) = x^{m_1}(\widetilde {F}_1(x) + x^{m_2-m_1}\widetilde {F}_2(x))$;
    but by Lemma~\ref{lem:omin1}, $F_1(X) + X^{m_2-m_1}F_2(X) = X^kG(X)$ say,
    and then $t_1(x)+t_2(x) = x^{m_1+k}\widetilde {G}(x)$ is as required
    with $\epsilon := \min_i \epsilon_i$.
    
    Similarly for $-$.
    Similarly for $*$ and $D$, since the product or ratio of two units is a unit.
    
    Finally, suppose $(F,r)$ is acceptable and
    $t(x) = \widetilde {F}\negmedspace\restriction_r(t_1(x),\ldots ,t_n(x))$
    Pick common $\epsilon$ for the $t_i$.
    If $t_i = 0$ on $(0,\epsilon)$, replace $F$ with $F(x_1,\ldots ,0,\ldots ,x_n)$.
    So WMA $t_i(x) = f_i(x)$ on $(0,\epsilon)$,
    where $f_i(x) = x_i^{m_i}\widetilde {F}_i(x)$
    for some $F_i \in \R[[X]]^* \cap \R\{X\}_\epsilon$.
    If any $m_i < 0$, then $t(x) = 0$ near 0 so done.
    Reducing $\epsilon$ further, WMA $r - |f_i(x)|$ has constant sign on
    $(0,\epsilon)$ by Lemma~\ref{lem:omin1}.
    If any such sign is not positive, again $F = 0$ so done.
    Else, $|f_i(0)| \leq  r$, so $(f_1(0),\ldots ,f_n(0)) \in B_{\leq r} \subseteq  \dom(F)$.
    Then $f(x) := \widetilde {F}(f_1(x),\ldots ,f_n(x))$ is analytic at 0,
    so done by Lemma~\ref{lem:omin1}.
\end{proof}

\begin{corollary}[Corollary of QE]
    $\Tan$ is o-minimal.
\end{corollary}
\begin{proof}
    Any qf formula in $\RanD$ is equivalent to a boolean combination of
    $\{ t(x) > 0 \}$ for $t$ an $\LanD$-term in one variable,
    so STS for any such $t$ there is a partition of $\R$ into finitely many
    points and intervals such that $\sign(t(x))$ is constant on each.

    Applying Lemma~\ref{lem:omin2} to $t(D(1,x))$ and $t( -D(1,x) )$,
    $t(x)$ has constant sign on some $(-\infty,a)$ and $(b,\infty)$.
    Then for $c \in [a,b]$,
    by Lemma~\ref{lem:omin2} applied to $t(x - c)$ and $t(x - (-c))$,
    for some $\epsilon > 0$,
    $t(x)$ has constant sign on $(c - \epsilon,c)$, $\{c\}$, and 
    $(c,c+\epsilon)$.
    
    We conclude by compactness of $[a,b]$.
\end{proof}


\section{Proof of QE}

\subsection{QE criterion}

\begin{fact}
    $T$ has QE iff:
    if $M_1,M_2 \vDash  T$ are $\omega$-saturated
    with a common f.g. substructure $A$,
    and if $b \in M_1$,
    then there exists an embedding $\left<{Ab}\right>^{M_1} \ensuremath{\lhook\joinrel\relbar\joinrel\rightarrow} M_2$ extending $\id_A$.
\end{fact}

So let $M_1,M_2 \vDash  \TanD$ be $\omega$-saturated
with a common f.g. substructure $K$,
and $b \in M_1$.
Note $K \leq  M_1$ is a subfield and $\RanD$ is a substructure of $K$.

\begin{lemma}
    If there exists an embedding $\left<{Kb}\right>^{M_1} \ensuremath{\lhook\joinrel\relbar\joinrel\rightarrow} M_2' \succ  M_2$ extending 
    $\id_K$,
    then there exists an embedding $\left<{Kb}\right>^{M_1} \ensuremath{\lhook\joinrel\relbar\joinrel\rightarrow} M_2$ extending $\id_K$.
\end{lemma}
\begin{proof}
    Say $b \mapsto  b' \in M_2'$. Then realise $\tp(b'/K)$ in $M_2$ by $\omega$-saturation.
\end{proof}

So we may freely replace $M_2$ with an elementary extension.

\subsection{I: local $\rightarrow $ global}

For $M \vDash  \Tan$,
let $\mu(M) := \{ \eta \in M : |\eta| < r \mbox{ for all } r \in \R_{>0} \}$.
For $\alpha \in M$, there is at most one $s \in \R$ s.t. $\alpha \in s+\mu(M)$.
Let $\st(\alpha) := s$ if such $s$ exists, else $\st(\alpha) := \infty$.

\begin{remark}
    for $\alpha \neq  0$, $\st(\alpha) = \infty$ iff $1 / \alpha \in \mu$.
\end{remark}

\begin{remark}
    If $\a \in \mu^n$ and $F \in \R\left<{\X}\right>$,
    then $\widetilde {F}\negmedspace\restriction_r(\a)$ is independent of the choice of $r$.
    We write $\widetilde {F}(\a)$ for the common value.
    Note $\widetilde {F}(\a) \in \mu$, by continuity.
\end{remark}

\begin{definition}
    If $A \subseteq  \mu(M_1)$,
    a map $e : A \rightarrow  \mu(M_2)$
    is a {\bf partial $\Tan$-$\mu$-embedding}
    if for $\a \in A^{<\omega}$ and $F \in \R\left<{\X}\right>$,
    \[ \widetilde {F}(\a) > 0 \Leftrightarrow  \widetilde {F}(e(\a)) > 0 .\]
\end{definition}

\begin{lemma}
    Any partial $\Tan$-$\mu$-embedding
    $e : \left<{Kb}\right> \cap \mu(M_1) \rightarrow  \mu(M_2)$
    extends to an $\LanD$-embedding $e' : \left<{Kb}\right> \ensuremath{\lhook\joinrel\relbar\joinrel\rightarrow} M_2$.
\end{lemma}
\begin{proof}
    \[ e'(\alpha) := \begin{cases}
        \st(\alpha) + e(\alpha - \st(\alpha))  &\mbox{if } \st(\alpha) \in \R 
        \\
        1/e(1 / \alpha)  &\mbox{if } \st(\alpha) = \infty
        \end{cases} \]

    \begin{claim}
        $e'$ is an ordered field embedding.
    \end{claim}
    Proof: 
        First we show that $e'$ is order-preserving.
        STS $e$ is order-preserving.
        Consider $F := X-Y \in \R\{X,Y\}_1$.
        \[ \Tan \vDash  \forall x,y.\; ( |x|<1 \wedge |y|<1 \rightarrow  \widetilde {F}\negmedspace\restriction_1(x,y) = x-y ), \]
        so for $\eta,\eta' \in \left<{Kb}\right>\cap\mu$,
        \begin{align*} \eta &> \eta' \\
            &\Leftrightarrow  \widetilde {F}(\eta,\eta') > 0 \\
            &\Leftrightarrow  \widetilde {F}(e(\eta),e(\eta')) > 0 \\
            &\Leftrightarrow  e(\eta) > e(\eta'). \end{align*}

        Now if $f(X,Y),g(X,Y) \in \R[X,Y]$
        and $\eta,\eta',\eta'' \in \left<{Kb}\right>\cap\mu$
        and $g(\eta,\eta') \neq  0$
        and $\eta'' = f(\eta,\eta')/g(\eta,\eta')$,
        then by considering $F := Zg(X,Y)-f(X,Y)$,
        $e(\eta'') = f(e(\eta),e(\eta'))/g(e(\eta),e(\eta'))$.

        Preservation by $e'$ of $+,*$ follows.

        For example, suppose $\eta,\eta' \in \left<{Kb}\right>\cap\mu$,
        we claim $e'(1 / \eta + 1 / \eta') = e'(1 / \eta)+e'(1 / \eta')$.
        Let $s := \st((1 / \eta + 1 / \eta')) \in \R \cup {\infty}$.

        If $s=\infty$, then
            \[ \eta'' := 1/(1 / \eta + 1 / \eta') \in \left<{Kb}\right>\cap\mu .\]
        Then by the above applied to the rational function $1/(1/X+1/Y)$,
            \[ e(\eta'') = 1/(1/e(\eta)+1/e(\eta')). \]
        So
            \begin{align*} e'(1 / \eta + 1 / \eta') &= 1/e(\eta'') \\
                &= 1/(1/(1/e(\eta) + 1/e(\eta'))) \\
                &= e'(1 / \eta) + e'(1 / \eta'). \end{align*}

        If $s \in \R$, then
            \[ \eta''' := (1 / \eta + 1 / \eta') - s \in \left<{Kb}\right>\cap\mu. \]
        Then
            \begin{align*} e'(1 / \eta + 1 / \eta') &= s+e(\eta''') \\
                &= s+((1/e(\eta) + 1/e(\eta'))-s) \\
                &= e'(1 / \eta) + e'(1 / \eta'). \end{align*}

        The other cases (e.g.\ $e'((s+\eta)(1 / \eta'))$) can be handled 
        similarly.

        % Is this really the neatest proof?
        % Wilkie just says it's "easy to see"\ldots 
\end{proof}

    It remains to see that for acceptable $(r,F)$,
    and $\alphabar \in \left<{Kb}\right>^n$,
    $e'(\widetilde {F}\negmedspace\restriction_r(\alphabar)) = \widetilde {F}\negmedspace\restriction_r(e'(\alphabar))$.

    If $\|\alphabar\| \geq  r$ then also $\|e'(\alphabar)\| \geq  r$,
    so the equality is clear.
    Else, $\s := \st(\alphabar) \in \dom(F)$,
    so $\widetilde {F}$ is analytic at $\s$.
    Let $s' := \widetilde {F}(\s)$,
    and say $(\epsilon,G)$ is acceptable s.t.
    $\widetilde {F} \in \R\{\X\}_{r+\epsilon}$ and
    $\widetilde {G}(\x) = \widetilde {F}(\s+\x) - s'$ for $\x \in \R^n$, $\|\x\|<\epsilon$.
    Then \[ \TanD \vDash  \forall \x.\;
        (\|\x\| < \epsilon \rightarrow 
            \widetilde {G}\negmedspace\restriction_\epsilon(\x) = \widetilde {F}\negmedspace\restriction_{r+\epsilon}(\s+\x) - s'). \]
    So
    \begin{align*} \widetilde {F}\negmedspace\restriction_r(e'(\alphabar))
        &= s' + \widetilde {F}\negmedspace\restriction_{r+\epsilon}(\s+e(\etabar)) - s' \mbox{ (where $\etabar := 
        \alphabar - \s$) } \\
        &= s' + \widetilde {G}(e(\etabar)) \\
        &= s' + e(\widetilde {G}(\etabar))  \mbox{ (considering $Y-G(X)$) } \\
        &= s' + e(\widetilde {F}\negmedspace\restriction_{r+\epsilon}(\s+\etabar) - s') \\
        &= e'(\widetilde {F}\negmedspace\restriction_{r+\epsilon}(\alphabar)) \\
        &= e'(\widetilde {F}\negmedspace\restriction_r(\alphabar))  \mbox{ (since $\|\alphabar\| < r$) } \end{align*}
    as required.

    
\subsection{II: finding a $\Tan$-$\mu$-embedding}

It remains to show that such an $e$ exists.

Since we may replace $M_2$ by an elementary extension, it suffices to show that 
the corresponding (long) type over $K\cap\mu$ is consistent, as follows:

\begin{lemma}
    Let $m$,$n \in \N$,
    $\X = (X_1,\ldots ,X_m)$,
    $\Y = (Y_1,\ldots ,Y_n)$,
    and $S \subseteq  \R\left<{\X,\Y}\right>$ finite,
    and $\c \in (K\cap\mu)^m$,
    and $\b \in \mu(M_1)^n$.

    Then exists $\b' \in \mu(M_2)^n$
    s.t. for $F \in S$,
    \[ M_1 \vDash  \widetilde {F}(\c,\b) > 0 \Leftrightarrow  M_2 \vDash  \widetilde {F}(\c,\b') > 0 .\]
\end{lemma}
\begin{proof}
    By induction on $n$, the $n=0$ case being trivial.

    First we show how to handle a single $F$.
    So suppose $S = \{F\}$.
    WMA $F \neq  0$.

    By Denef - van den Dries Preparation,
    \[ F(\X,\Y) = \sum_{|\nu| < d} a_\nu(\X) \Y^\nu u_\nu(\X,\Y) \]
    for some $d \in \N$, $a_\nu \in \R\left<{\X}\right>$, $u_\nu \in \R\left<{\X,\Y}\right>^*$.

    Let $\nu_0$ s.t. $M := |a_{\nu_0}(\c)| \geq  |a_\nu(\c)| \forall \nu$.
    Define
        \[ s_\nu := \st(a_\nu(\c)/M) \in \R \]
        \[ k_\nu := a_\nu(\c)/M - s_\nu \in K \]

    (Remark: here it is crucial that $K$ is a $\LanD$-substructure, and hence 
    a subfield, rather than merely a $\Lan$-substructure.)

    Let $\Z = (Z_\nu)_{|\nu| < d}$, and define
    \[ G(\X,\Z,\Y) := \sum_{|\nu| < d} (Z_\nu + s_\nu) \Y^\nu u_\nu(\X,\Y). \]

    Then $G \in \R\left<{\X,\Z,\Y}\right>$, and
    $\widetilde {F}(\c,\y) = M \widetilde {G}(\c,\k,\y)$ for $\y \in \mu^n$.

    Define $\Lambda : \mu^n \rightarrow  \mu^n$;
    \[ \y \mapsto 
        (y_1+y_n^{d^{n-1}}, y_2+y_n^{d^{n-2}},\ldots , y_{n-1}+y_n^d, y_n). \]

    % Then \Lambda is a bijection, with inverse
    % \Omega : \mu^n \rightarrow  \mu^n; \y \mapsto 
    %  (y_1-y_n^{d^{n-1}}, y_2-y_n^{d^{n-2}},\ldots , y_{n-1}-y_n^d, y_n).

    Let $H(\X,\Z,\Y) := G(\X,\Z,\Lambda(\Y)) \in \R\left<{\X,\Z,\Y}\right>$
    (considering $\Lambda$ as a tuple of (polynomial) formal power series).

    \begin{claim}
        $H$ is regular in $Y_n$.
    \end{claim}
    \begin{proof}
        \begin{align*} H(0,0,0,Y_n)
          &= \sum_{|\nu| < d} s_\nu \Lambda(0,Y_n)^\nu u_\nu(0,\Lambda(0,Y_n)) 
          \\
          &= \sum_{|\nu| < d} s_\nu Y_n^{\sum \nu_i d^{n-i}} u_\nu(0,\Lambda(0,Y_n)) \end{align*}
        Now for $\nu$ with $|\nu| < d$,
        the exponents $\sum \nu_i d^{n-i}$ are distinct for distinct $\nu$, 
        and are ordered according to the lexicographic order on the $\nu$.
        So taking $\nu$ lexicographically minimal s.t. $s_\nu \neq  0$, which 
        exists since $s_{\nu_0}=1$, witnesses regularity of $H$.
    \end{proof}

    So by Weierstrass preparation,
        \[ \widetilde {F}(\c,\Lambda(\y)) = M \widetilde {G}(\c,\k,\y) = M \widetilde {Q}(\c,\k,\y) \widetilde {L}(\c,\k,\y) 
        \]
    where $Q \in \R\left<{\X,\Z,\Y}\right>^*$ and $L \in \R\left<{\X,\Z,\Y_{<n}}\right>[Y_n]$,
    where $\Y_{<n} := (Y_1,\ldots ,Y_{n-1})$.
    WLOG $Q(0) > 0$.

    Say $L(\X,\Z,\Y) = \sum_{i=0}^p L_i(\X,\Z,\Y_{<n})Y_n^i$
    with $L_i \in \R\left<{\X,\Z,\Y_{<n}}\right>$.
    
    By QE for RCF,
    for $\epsilon \in \R_{>0}$,
    \[ \exists y_n \in (-\epsilon,\epsilon). \sum_{i=0}^p w_iy_n^i > 0 \]
    is equivalent modulo RCF to a qf ordered ring formula $\psi_\epsilon(\w)$, 
    which is a boolean combination of atomic formulae $f(\w)>0$ where $f$ is a 
    polynomial over $\mathbb{Z}$.
    So by the inductive hypothesis, and since $\R\left<{\X,\Z,\Y_{<n}}\right>$ is a 
    ring,
    there exists $\b''_\epsilon$ in $\mu(M_2)^{n-1}$ s.t.
    \[ \vDash  \psi_\epsilon(\widetilde {L}_i(\c,\k,\b''_\epsilon)) \]

    So by $\omega$-saturation,
    exists $\b''$ in $\mu(M_2)^n$ s.t.
    $\widetilde {L}(\c,\k,\b'') > 0$.
    Hence $\widetilde {F}(\c,\Lambda(\b'')) > 0$,
    so $\b' := \Lambda(\b'')$ is as required.

    For general finite $S$,
    we may take a $d$ common to all $F \in S$,
    proceed as above (so using the same $\Lambda$ for all $F$),
    and apply RCF QE to the corresponding conjunction of inequalities.
\end{proof}
\end{document}
