### Model completeness and o-minimality of \R_an

Notes on the Denef-(van Den Dries) quantifier elimination for \R_an and its 
consequences.

Jan Denef and Lou van den Dries "p-adic and real subanalytic sets"
Annals of Mathematics 1998.

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

## Analytic functions

# Formal power series

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

F (- R[[\X]]
F = \sum_{\nu (- \N^n} a_\nu \X^\nu
where \X^\nu := X_1^{\nu_1}*...*X_n^{\nu_n}.

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

For R a ring, R^* := { x (- R : \exists y (- R. x*y=1 } = units.
Lemma: For F (- R[[\X]], F (- R[[\X]]^* iff F(0) (- R^*.
Proof:
    By induction, suffices to show when \X=X is a single variable.

    If F*G = 1 then F(0)*G(0)=1.
    
    If F = \sum a_iX^i
    If a_0*b_0=1, then define recursively for n>=0
    b_{n+1} := -a_0^{-1}(a_1*b_n + a_2*b_{n-1} + ... a_{n+1}*b_0).
    Then \sum_{0<=i<=n+1} a_ib_{n+1-i} = 0,
    so (\sum a_iX^i)*(\sum b_iX^i) = 1.

# Convergent power series

F (- \R[[\X]]
dom(\sum a_\nu\X^\nu)
    := int( { \x (- \R^n : \sum a_\nu\x^\nu converges } )
     = int( { \x : { a_\nu\x^\nu : \nu } is bounded )

e.g. dom( \sum_\nu X^\nuY^\nu ) = { XY < 1 }

\R<\X> := { F : 0 (- dom(F) }

Fact:
    \R<\X> is a subring of \R[[\X]].

F (- \R<\X> defines a function ~F : dom(F) --> \R.

Fact:
    ~F=0 iff F=0.
    ~F (- C^\infty(dom(F)).

f : U --> \R is _analytic_ at \b (- U
if f(\X-\b) = ~F(\X) on U_\b, some \b (- U_\b (=_op U and some F (- \R<\X>.

Fact:
    ~F is analytic at every b (- dom(F).
Proof[Idea of proof]:
    show the Taylor series at b,
        \sum_\nu 1/((\sum\nu)!) \~{D_1^{\nu_1}...D_n^{\nu_n} F}(b) X^\nu
    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].

Fact:
    if f is analytic at b and g is analytic at f(b),
    then (g \circ f) is analytic at b.

Corollary:
    \R<\X>^* = \R[[\X]]^* \cap \R<\X>
Proof:
    Suppose F (- \R<\X> has non-zero constant term;
    WTS F is invertible in \R<\X>.
    Multiplying F by a constant, WMA F(0)=1.
    So say F = 1-G where G (- \R[[\X]] with G(0)=0.
    Let H(X) := \sum X^i (- \R<X>.
    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 (- \R<\X> by the Fact.

# Weierstrass Preparation

Say F (- \R[[\X,Y]] is _regular_ in Y
if some term aY^p with a/=0 occurs in the power series F,
i.e. if F(0,Y) /= 0.

Fact[Weierstrass Preparation Theorem]:
    If F (- \R<\X,Y> is regular in Y,
    then exists Q (- \R<\X>^* and L (- \R<\X>[Y],
    such that F = Q*L.
    
# Denef-vanDenDries Preparation

Fact:
    \R<\X> is Noetherian; that is, any ideal is finitely generated.

Fact:
    The embedding \R<\X> <= \R[[X]] is faithfully flat.

I omit the definition of faithful flatness, because in fact we need only the 
following consequence.
Corollary:
    If f_i,f (- \R<\X>
    and the linear equation f_1*x_1 + ... f_n*x_n = f
    has a solution in \R[[\X]],
    then it already has a solution in \R<\X>.

Wilkie names the following application of these facts the "Denef-vanDenDries 
Preparation Theorem". So let us use that name too.

Theorem:
    If F (- \R<\X,\Y>
    then F(\X,\Y) = \sum_{|\nu| < d} a_\nu(\X) * \Y^\nu * u_\nu(\X,\Y)
    for some d (- \N, a_\nu (- \R<\X>, u_\nu (- \R<\X,\Y>^*.
Proof:
    By induction on the length of \Y.
    So suppose for \R<\X,\Y>; we prove it for \R<\X,\Y,Z>.
    Let F = \sum a_iZ^i (- \R<\X,\Y,Z>, a_i (- \R<\X,\Y>.
    \R<\X,\Y> is Noetherian, so there exist d (- \N and b_{i,j} (- \R<\X,\Y>
    such that a_{d+i} = \sum_{j<d} b_{i,j} a_j.
    So F = \sum_{i<d} a_iZ^i + \sum_{j>=0} \sum_{i<d} b_{i,j}a_jZ^{d+j}
        = \sum_{i<d} a_iZ^i + Z^d \sum_{i<d} a_i \sum_{j>=0} b_{i,j}Z^j
        = \sum_{i<d} (a_iZ^i)(1 + Z^{d-i} \sum_{j>=0} b_{i,j}Z^j)
        = \sum_{i<d} a_iZ^iu_i
    Now apply the inductive hypothesis to the a_i.

## \R_an

||\x|| := max_i |x_i|
B_<r := { \x (- \R^n : ||\x|| < r }
B_<=r := { \x (- \R^n : ||\x|| <= r }

For r>0,
\R{\X}_r := { F (- \R[[\X]] : B_<=r (= dom(F) },
so \R<\X> = \cap_{r (- \R_{>0}} \R{\X}_r.

If F (- \R{\X}_r,
~F|_r(\x) := { ~F(\x) if \x (- B_<r
             { 0      else
"restricted analytic function".

Say (r,F) is _acceptable_ if r (- \R_{>0} and F (- \R{X}_r.

\R_an := { \R; +,-,*,<, (a)_{a (- \R}, (~F|_r)_{(r,F) acceptable} }
structure in language L_an.

L_an^D := L_an \cup {D}
\R_an^D := expansion of \R_an interpreting D by
    D(x,y) := { x/y if y!=0
              { 0   if y=0

Theorem[Denef-(van den Dries)]:
    T_an^D := Th(\R_an^D) has QE.

Corollary:
    T_an := Th(\R_an) is model complete.
Proof:
    Any qf L_an^D formula is equivalent to an existential L_an formula.
    
    For example, if t_1,t_2 are terms, then 
        \phi(D(t_1(x),t_2(x)))
        <=> \exists z. ( \phi(z) /\
            ( (t_2(x) = 0 /\ z=0) \/ (t_2(x) != 0 /\ z*t_2(x) = t_1(x)) ) ).

Remark:
    Model completeness of \R_an was previously proven (expressed in different
    but equivalent terms) by Gabrielov in the 1960s
    ("theorem of the complement" for subanalytic sets).

    // Y (= \R^n is _semi-analytic_
    // if every b (- \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 (= B_<=r is qf-definable in \R_an iff semi-analytic.
    //
    // Z (= \R^n is _sub-analytic_
    // if every b (- \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 (= B_<=r is existentially definable in \R_an iff
    // sub-analytic.
    //
    // Theorem[Gabrielov, 1960s]: if Z is sub-analytic, so is \R^n \\ Z.
    //
    // Exercise: This is *equivalent* to model completeness of \R_an.


# o-minimality of \R_an

Lemma 1:
    Suppose 0 /= F (- \R<X>.
    Then F = X^m*G for some unique m (- \N and G (- F[[X]]^*,
    and dom(G) = dom(F),
    and for some \epsilon>0,
    ~F has constant non-zero sign on (0,\epsilon).
Proof:
    Existence and uniqueness of m,G is immediate from the description of 
    F[[X]]^*.
    For dom(G) = dom(X^m*G):
    given x (- \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 ~G is continuous, so ~G and hence ~F
    has constant non-zero sign on some (0,\epsilon).

Lemma 2:
    Let t(x) be an L_an^D-term in 1 variable.
    Exists \epsilon > 0 s.t.
    t(x) = 0 on (0,\epsilon)
    or t(x) = (x^m*~F(x)) on (0,\epsilon)
    for some m (- \Z and F (- \R[[X]]^* \cap \R{X}_\epsilon.
    In particular, t(x) has constant sign on (0,\epsilon).
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}*~F_i(x) on (0,\epsilon_i)
    with F_i (- \R[[X]]^* \cap \R{X}_{\epsilon_i}.
    Say m_1 <= m_2.
    then t_1(x)+t_2(x) = x^{m_1}*(~F_1(x) + x^{m_2-m_1}*~F_2(x));
    but by Lemma 1, F_1(X) + X^{m_2-m_1}*F_2(X) = X^k*G(X) say,
    and then t_1(x)+t_2(x) = x^{m_1+k}*~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) = ~F|_r(t_1(x),...,t_n(x))
    Pick common \epsilon for the t_i.
    If t_i = 0 on (0,\epsilon), replace F with F(x_1,...,0,...,x_n).
    So WMA t_i(x) = f_i(x) on (0,\epsilon),
    where f_i(x) = x_i^{m_i}*~F_i(x)
    for some F_i (- \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 1.
    If any such sign is not positive, again F = 0 so done.
    Else, |f_i(0)| <= r, so (f_1(0),...,f_n(0)) (- B_{<=r} (= \dom(F).
    Then f(x) := ~F(f_1(x),...,f_n(x)) is analytic at 0,
    so done by Lemma 1.

Corollary of QE:
    T_an is o-minimal.
Proof:
    Any qf formula in \R_an^D is equivalent to a boolean combination of
    { t(x) > 0 } for t an L_an^D-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 2 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 (- [a,b],
    by Lemma 2 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].


## Proof of QE

# QE criterion

Fact:
    T has QE iff:
    if M_1,M_2 |= T are \omega-saturated
    with a common f.g. substructure A,
    and if b (- M_1,
    then there exists an embedding <Ab>^{M_1} (-> M_2 extending id_A.

So let M_1,M_2 |= T_an^D be \omega-saturated
with a common f.g. substructure K,
and b (- M_1.
Note K <= M_1 is a subfield and \R_an^D is a substructure of K.

Lemma:
    If there exists an embedding <Kb>^{M_1} (-> M_2' >~ M_2 extending id_K,
    then there exists an embedding <Kb>^{M_1} (-> M_2 extending id_K.
Proof:
    Say b |-> b' (- M_2'. Then realise \tp(b'/K) in M_2 by \omega-saturation.

So we may freely replace M_2 with an elementary extension.

# I: local -> global

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

Remark: for \alpha != 0, \st(\alpha) = \infty iff 1/\alpha (- \mu.

Remark:
    If \a (- \mu^n and F (- \R<\X>,
    then ~F|_r(\a) is independent of the choice of r.
    We write ~F(\a) for the common value.

Definition:
    e : \mu(M_1) )= A --> \mu(M_2)
    is a partial T_an-\mu-embedding
    if ~F(\a) > 0 iff ~F(e(\a)) > 0
    for \a (- A^{<\omega} and F (- \R<\X>.

Lemma:
    If e : <Kb> \cap \mu(M_1) --> \mu(M_2) is a partial T_an-\mu-embedding,
    then e extends to an L_an^D-embedding e' : <Kb> (-> M_2.
Proof:
    e'(\alpha) := { \st(alpha) + e(\alpha - \st(\alpha))  if \st(alpha) (- \R
                  { 1/e(1/\alpha)  if \st(\alpha) = \infty

    Claim:
        e' is an ordered field embedding.
    Proof: 
        First we show that e' is order-preserving.
        STS e is order-preserving.
        Consider F := X-Y (- \R{X,Y}_1.
        T_an |= \forall x,y. ( |x|<1 /\ |y|<1 -> ~F|_1(x,y) = x-y ),
        so for \eta,\eta' (- <Kb>\cap\mu,
        \eta > \eta'
            <=> ~F(\eta,\eta') > 0
            <=> ~F(e(\eta),e(\eta')) > 0
            <=> e(\eta) > e(\eta').

        Now if f(X,Y),g(X,Y) (- \R[X,Y]
        and \eta,\eta',\eta'' (- <Kb>\cap\mu
        and g(\eta,\eta') != 0
        and \eta'' = f(\eta,\eta')/g(\eta,\eta'),
        then by considering F := Z*g(X,Y)-f(X,Y),
        e(\eta'') = f(e(\eta),e(\eta'))/g(e(\eta),e(\eta')).

        Preservation by e' of +,* follows.

        e.g. suppose \eta,\eta' (- <Kb>\cap\mu,
        we claim e'(1/\eta + 1/\eta') = e'(1/\eta)+e'(1/\eta').
        Let s := \st((1/\eta + 1/\eta')) (- \R \cup {\infty}.

        If s=\infty, then
            \eta'' := 1/(1/\eta + 1/\eta') (- <Kb>\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
            e'(1/\eta + 1/\eta') = 1/e(\eta'')
                = 1/(1/(1/e(\eta) + 1/e(\eta')))
                = e'(1/\eta) + e'(1/\eta').

        If s (- \R, then
            \eta''' := (1/\eta + 1/\eta') - s (- <Kb>\cap\mu.
        Then
            e'(1/\eta + 1/\eta') = s+e(\eta''')
                = s+((1/e(\eta) + 1/e(\eta'))-s)
                = e'(1/\eta) + e'(1/\eta').

        Similarly for the other cases (e.g. e'((s+\eta)*(1/\eta'))).

        // Is this really the neatest proof?
        // Wilkie just says it's "easy to see"...

    It remains to see that for acceptable (r,F),
    and \alphabar (- <Kb>^n,
    e'(~F|_r(\alphabar)) = ~F|_r(e'(\alphabar)).

    If ||\alphabar|| >= r then also ||e'(\alphabar)|| >= r,
    so the equality is clear.
    Else, \s := \st(\alphabar) (- \dom(F),
    so ~F is analytic at \s.
    Let s' := ~F(\s),
    and say (\epsilon,G) is acceptable s.t.
    ~F (- \R{\X}_{r+\epsilon} and
    ~G(\x) = ~F(\s+\x) - s' for \x (- B_{<\epsilon}
    Then T_an^D |= \forall \x.
        (||\x|| < \epsilon ->
            ~G|_\epsilon(\x) = ~F|_{r+\epsilon}(\s+\x) - s').
    So
    ~F|_r(e'(\alphabar))
        = s' + ~F|_{r+\epsilon}(\s+e(\etabar)) - s'
        = s' + ~G(e(\etabar))
        = s' + e(~G(\etabar))  (considering Y-G(X))
        = s' + e(~F|_{r+\epsilon}(\s+\etabar) - s')
        = e'(~F|_{r+\epsilon}(\alphabar))
        = e'(~F|_r(\alphabar))  (since ||\alphabar|| < r)
    as required.
    
# II: local 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:

Lemma:
    Let m,n (- \N,
    \X = (X_1,...,X_m),
    \Y = (Y_1,...,Y_n),
    and S a finite subset \R<\X,\Y>,
    and \c (- K^m,
    and \b (- \mu^n.

    Then exists \b' (- \mu(M_2)
    s.t. for F (- S,
    M_1 |= ~F(\c,\b) > 0 <=> M_2 |= ~F(\c,\b') > 0
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 /= 0.

    By Denef-vanDenDries Preparation,
    F(\X,\Y) = \sum_{|\nu| < d} a_\nu(\X) * \Y^\nu * u_\nu(\X,\Y)
    for some d (- \N, a_\nu (- \R<\X>, u_\nu (- \R<\X,\Y>^*.

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

    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 (- \R<\X,\Z,\Y>, and
    ~F(\c,\y) = M * ~G(\c,\k,\y) for \y (- \mu^n.

    Define \Lambda : \mu^n --> \mu^n; \y |->
        (y_1+y_n^{d^{n-1}}, y_2+y_n^{d^{n-2}},..., y_{n-1}+y_n^d, y_n).

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

    Let H(\X,\Z,\Y) := G(\X,\Z,\Lambda(\Y)) (- \R<\X,\Z,\Y>
    (considering \Lambda as a tuple of (polynomial) formal power series).

    Claim:
        H is regular in Y_n.
    Proof:
        H(0,0,0,Y_n)
          = \sum_{|\nu| < d} s_\nu * \Lambda(0,Y_n) * u_\nu(0,0,Y_n)
          = \sum_{|\nu| < d} s_\nu * Y_n^{\sum \nu_i d^{n-i}} * u_\nu(0,0,Y_n)
        These exponents are distinct for distinct \nu, and ordered according 
        to the lexicographic order on the \nu.
        So \nu lexicographically minimal s.t. s_\nu /= 0, which exists since 
        s_{\nu_0}=1, witnesses regularity of H.

    So by Weierstrass preparation,
        ~F(\c,\Lambda(\y)) = M * ~Q(\c,\k,\y) * ~L(\c,\k,\y)
    where Q (- \R<\X,\Z,\Y>^* and L (- \R<\X,\Z,\Y_{<n}>[Y_n],
    where \Y_{<n} := (Y_1,...,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
    
    By QE for RCF,
    for \epsilon (- \R_{>0},
    \exists y_n (- (-\epsilon,\epsilon). \sum_{i=0}^p w_iy_n^i > 0
    is equivalent to a qf ordered ring formula \psi_\epsilon(w_i).
    By the inductive hypothesis (using that \R<\X,\Z,\Y'> is a ring),
    exists \b''_\epsilon in \mu(M_2)^{n-1} s.t.
    |= \psi_\epsilon(~L_i(\c,\k,\b''_\epsilon))

    So by \omega-saturation,
    exists \b'' in \mu(M_2)^n s.t.
    ~L(\c,\k,\b'') > 0.
    Hence ~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 (- S,
    proceed as above (so using the same \Lambda for all F),
    and apply RCF QE to the corresponding conjunction of inequalities.