%PARAM.2
\magnification=\magstep1
\def\firstpage{1}
\pageno=\firstpage
%FONTS.4
\font\huge=cmbx10 scaled\magstep2
\font\xbold=cmbx10 scaled\magstep1
\font\cbold=cmsy10 scaled\magstep1
\font\mbold=cmmi10 scaled\magstep1
\font\sub=cmbx10
\font\smallish=cmr8
\font\smallbf=cmbx7
\font\small=cmr7
\font\tiny=cmr5
\font\plg=cmtt10
\font\plgt=cmtt10 at 10truept
%
% from amssym.def
\font\tenmsb=msbm10
\font\sevenmsb=msbm7
\font\fivemsb=msbm5
\newfam\msbfam
\textfont\msbfam=\tenmsb
\scriptfont\msbfam=\sevenmsb
\scriptscriptfont\msbfam=\fivemsb
\def\Bbb#1{{\fam\msbfam\relax#1}}
%TITLES.4
\count5=0
\count6=1
\count7=1
\count8=1
\def\proof{\medskip\noindent{\bf Proof.\ }}
\def\qed{\hfill{\smallbf QED}\par\medskip}
\def\references{\bigskip\noindent\hbox{\bf References}\medskip}
\def\remark{\medskip\noindent{\bf Remark.\ }}
\def\nextremark{\smallskip\noindent$\circ$\hskip1.5em}
\def\firstremark{\bigskip\noindent{\bf Remarks.}\nextremark}
\def\abstract#1\par{{\smallish{\narrower\noindent {\bf Abstract.} #1 \par}}}
\def\equ(#1){\hskip-0.03em\csname e#1\endcsname}
\def\clm(#1){\csname c#1\endcsname}
\def\equation(#1){\eqno\tag(#1)}
%\def\equation(#1){\eqno\tag(#1) {\rm #1}}
\def\tag(#1){(\number\count5.
\number\count6)
\expandafter\xdef\csname e#1\endcsname{
(\number\count5.\number\count6)}
\global\advance\count6 by 1}
\def\claim #1(#2) #3\par{
\vskip.1in\medbreak\noindent
{\bf #1\ \number\count5.\number\count7.\ }{\sl #3}\par
\expandafter\xdef\csname c#2\endcsname{#1~\number\count5.\number\count7}
\global\advance\count7 by 1
\ifdim\lastskip<\medskipamount
\removelastskip\penalty55\medskip\fi}
\def\section#1\par{\vskip0pt plus.3\vsize\penalty-75
\vskip0pt plus -.3\vsize\bigskip\bigskip
\global\advance\count5 by 1
\message{#1}\leftline
{\xbold \number\count5.\ #1}
\count6=1
\count7=1
\count8=1
\nobreak\smallskip\noindent}
\def\subsection#1\par{\vskip0pt plus.2\vsize\penalty-75
\vskip0pt plus -.2\vsize\bigskip\bigskip
\message{#1}\leftline{\sub
\number\count5.\number\count8.\ #1}
\global\advance\count8 by 1
\nobreak\smallskip\noindent}
\def\proofof(#1){\medskip\noindent{\bf Proof of \csname c#1\endcsname.\ }}
%MACROS.17
\def\rightheadline{\hfil}
\def\leftheadline{\small\hfil HANS KOCH\hfil}
\headline={\ifnum\pageno=\firstpage\hfil\else
\ifodd\pageno{{\tiny\rightheadline}\number\pageno}
\else{\number\pageno\tiny\leftheadline}\fi\fi}
\footline={\ifnum\pageno=\firstpage\hss\tenrm\folio\hss\else\hss\fi}
%
\let\ov=\overline
\let\cl=\centerline
\let\wh=\widehat
\let\wt=\widetilde
\let\eps=\varepsilon
\let\sss=\scriptscriptstyle
%
% needs fonts.4 or later
\def\mean{{\Bbb E}}
\def\proj{{\Bbb P}}
\def\natural{{\Bbb N}}
\def\integer{{\Bbb Z}}
\def\rational{{\Bbb Q}}
\def\real{{\Bbb R}}
\def\complex{{\Bbb C}}
\def\torus{{\Bbb T}}
\def\iso{{\Bbb J}}
\def\Id{{\Bbb I}}
\def\id{{\rm I}}
\def\modulo{{\rm mod~}}
\def\std{{\rm std}}
\def\Im{{\rm Im~}}
%
\def\mapright#1{\smash{\mathop{\longrightarrow}\limits^{#1}}}
%
\def\half{{1\over 2}}
\def\third{{1\over 3}}
\def\quarter{{1\over 4}}
%
\def\AA{{\cal A}}
\def\BB{{\cal B}}
\def\CC{{\cal C}}
\def\DD{{\cal D}}
\def\EE{{\cal E}}
\def\FF{{\cal F}}
\def\GG{{\cal G}}
\def\HH{{\cal H}}
\def\II{{\cal I}}
\def\JJ{{\cal J}}
\def\KK{{\cal K}}
\def\LL{{\cal L}}
\def\MM{{\cal M}}
\def\NN{{\cal N}}
\def\OO{{\cal O}}
\def\PP{{\cal P}}
\def\QQ{{\cal Q}}
\def\RR{{\cal R}}
\def\SS{{\cal S}}
\def\TT{{\cal T}}
\def\UU{{\cal U}}
\def\VV{{\cal V}}
\def\WW{{\cal W}}
\def\XX{{\cal X}}
\def\YY{{\cal Y}}
\def\ZZ{{\cal Z}}
%DRAFT5.TEX
%\input param.2
%\input fonts.4
%\input titles.4
%\input macros.17
%
\def\iminus{I^{^-}\!}
\def\dminus{d^{^-}}
\def\iplus{I^{^+}\!}
\def\iplusminus{I^{^\pm}\!}
\def\Iminus{{\Bbb I}^{^-}\!}
\def\Iplus{{\Bbb I}^{^+}\!}
\def\Iplusminus{{\Bbb I}^{^\pm}\!}
\def\ssF{{\scriptscriptstyle F}}
\def\ssO{{\scriptscriptstyle 0}}
\def\ssH{{\scriptscriptstyle H}}
\def\ssHp{{\scriptscriptstyle H'}}
\def\ssHpp{{\scriptscriptstyle H''}}
\def\nablap{{\nabla_{\!p}}}
\def\nablaq{{\nabla_{\!q}}}
\def\BBB{{\Bbb B}}
\def\JJJ{{\Bbb J}}
\def\supabs{{\rm supabs}}
%
\def\rED{1}
\def\rKad{2}
\def\rSKad{3}
\def\rMcKi{4}
\def\rMcKii{5}
\def\rMEsc{6}
\def\rKSi{7}
\def\rGJSS{8}
\def\rWi{9}
\def\rKSii{10}
\def\rKMcK{11}
\def\rMaoH{12}
\def\rGMao{13}
\def\rWii{14}
\def\rACS{15}
\def\rMMS{16}
\def\rMcKiii{17}
\def\rCGM{18}
\def\rSti{19}
\def\rCGJii{20}
\def\rCGJK{21}
\def\rAKW{22}
\def\rKi{23}
\def\rCJBC{24}
\def\rCMcK]{25}
\def\rAK{26}
\def\rJLDi{27}
\def\rJLDii{28}
\def\rCJ{29}
\def\rCC{30}
\def\rKii{31}
\def\rKiii{32}
\def\rKSW{33}
\def\rAda{34}
\def\rGNAT{35}
\def\rPentium{36}
\def\rIEEE{37}
%
\def\rightheadline{\small\hfil
A RENORMALIZATION GROUP FIXED POINT\hfil}
%
\cl{{\xbold A Renormalization Group Fixed Point}}
\cl{{\xbold Associated with the Breakup of Golden Invariant Tori}}
%
\bigskip
\cl{Hans Koch}
\smallskip
\cl{Department of Mathematics, University of Texas at Austin}
\cl{Austin, TX 78712}
%
\footnote{}
{{\small This work was supported in part by the National Science Foundation
under Grants No. DMS-9705095 and DMS-0088935.}}
%
\bigskip
\abstract
We give a computer-assisted proof for the existence of
a renormalization group fixed point (Hamiltonian) with non-trivial scaling,
associated with the breakup of invariant tori
with rotation number equal to the golden mean.
\section Introduction and main results
Renormalization group methods for Hamiltonian flows
and related maps were introduced first in [\rED,\rKad],
as a tool for explaining the breakup of golden invariant tori.
Since then, these methods have been developed further
and extended to other systems [\rSKad--\rKii],
but one of the main problems has remained open:
The existence of a non-trivial renormalization group (RG) fixed point.
In this paper, we prove that such a fixed point exists.
Its connection with critical invariant tori
was discussed earlier in [\rKii].
The general form of our RG transformation $\RR$ can be described as follows.
Consider the matrix $T=\left[{0~1\atop 1~1}\right]$,
whose eigenvalues are the golden mean $\vartheta=\half+\half\sqrt{5}$,
and $-\vartheta^{-1}$.
This matrix defines a map on the torus $\torus^2$,
and it can be extended to a symplectic map $\TT$
on $\torus^2\times\real^2$, by setting $\TT(q,p)=\bigl(Tq,T^{-1}p\bigr)$.
If $H$ is a Hamiltonian function on $\torus^2\times\real^2$, then
$$
\RR(H)=H\circ\TT\quad (\modulo\GG)\,.
\equation(RRmodGG)
$$
Here, $\GG$ is a group (ideally) of transformations
that preserves rotation numbers.
This includes coordinate changes $H\mapsto H\circ U$,
with $U$ canonical and homotopic to the identity,
a scaling of of the action variables $H\mapsto\mu^{-1}H(.,\mu.)$,
and a scaling of the energy $H\mapsto\tau H-\epsilon$.
Thus, a specific RG transformation is obtained
by choosing a map $H\mapsto G_\ssH$ with values in $\GG$,
and defining $\RR(H)=G_\ssH(H\circ\TT)$.
The goal is to do this in such a way that $\RR$
defines a hyperbolic dynamical system some manifold
of ``normalized'' Hamiltonians,
which is contracting in all but a finite number of directions.
By contrast to other RG schemes in dynamical systems,
this seems possible only if we allow $\GG$ to be infinite dimensional.
This is one of the interesting and challenging aspect
of a renormalization group for Hamiltonians.
We will now define the notion of a ``resonant'' Hamiltonian,
and after introducing an appropriate function space,
the resonant subspace will serve
as our manifold of normalized Hamiltonians.
Consider the eigenvectors $\omega=(\vartheta^{-1},1)$
and $\Omega=(1,-\vartheta^{-1})$ of the matrix $T$,
associated with the eigenvalues
$\vartheta$ and $-\vartheta^{-1}$, respectively.
In what follows, a Hamiltonian is always a function
that admits a representation
$$
H(q,p)=\omega\cdot p
+\!\sum_{(\nu,k)\in I}H_{\nu,k}\cos(\nu\cdot q)(\Omega\cdot p)^k\,,
\equation(Hqp)
$$
where $I=\VV\times\natural$ and
$\VV=\{\nu\in\integer\times\natural:\nu_2>0 {\rm~or~}\nu_1\ge 0\}$.
We call $H$ {\it real} if the coefficients $H_{\nu,k}$ are all real.
Given a set $J\subseteq I$, denote by $\JJJ H$
the Hamiltonian obtained from $H$
by restricting the sum in \equ(Hqp) to the index set $J$.
In particular, consider the set
$$
\iplus=\bigl\{(\nu,k)\in I: |\omega\cdot\nu|\le\sigma|\Omega\cdot\nu|
{\rm ~or~ } |\omega\cdot\nu|<\kappa k\bigr\}\,,
\equation(iplusdef)
$$
and the corresponding projection $\Iplus$,
where $\sigma$ and $\kappa$ are fixed but arbitrary positive real numbers.
The Hamiltonian $\Iplus H$ will be called
the {\it resonant} part of $H$,
and $\Iminus H=H-\Iplus H$ the {\it non-resonant} part.
The (non)resonant part of a function
$$
F(q,p)=\!\sum_{(\nu,k)\in I}
\bigl[F_{\nu,k}\cos(\nu\cdot q)+F'_{\nu,k}\sin(\nu\cdot q)\bigr]
(\Omega\cdot p)^k
\equation(Fqp)
$$
is defined similarly.
In addition, if the coefficients $F'_{\nu,k}$ or $F_{\nu,k}$ are all zero,
we will call $F$ an {\it even} or {\it odd} function, respectively.
As mentioned above, ``normalizing'' a Hamiltonian
involves the elimination of its non-resonant part.
This will be done by means of a canonical change of variables.
A canonical transformations $U_\phi: (q,p)\mapsto (q+Q,p+P)$,
associated with a generating function $\phi$,
is defined implicitly by the equation
$$
\eqalign{
Q(q,p)&=\nablap\phi\bigl(q,p+P(q,p)\bigr)\,,\cr
P(q,p)&=-\nablaq\phi\bigl(q,p+P(q,p)\bigr)\,.\cr}
\equation(UphiDef)
$$
In what follows, a generating function
$\phi$ is always assumed to be an odd function of the form \equ(Fqp).
Notice that if $\phi$ is small, then
$H\circ U_\phi=H+\{H,\phi\}\,+$ ``higher order terms''.
We are now ready to give a formal definition
of our RG transformation $\RR$.
In what follows, two Hamiltonians that differ only by an additive constant
will be considered equivalent.
(We will do this by simply ignoring such constants.)
Let $\phi_0$ be a fixed generating function, to be chosen later.
Define $\TT_\mu(q,p)=\bigl(Tq,\mu T^{-1}p\bigr)$
and $\mu_\ssO=\vartheta^{-3}$.
Then we set
$$
\RR=\NN\circ\LL\circ\SS\,,
\equation(RRDef)
$$
where
$$
\eqalign{
(\SS H)(q,p)&=c_\ssH H\bigl(q,p/c_\ssH\bigr)\,,\cr
\LL H&=\tau_\ssH\mu_\ssO^{-1}H\circ\TT_{\mu_\ssO}\circ U_{\phi_0}\,,\cr
\NN(H)&=H\circ\UU_\ssH\,.\cr}
\equation(NNLLSSDef)
$$
Here, $c_\ssH=2H_{0,2}\,$, $\tau_\ssH=\vartheta$,
and $\UU_\ssH$ is a canonical transformation,
determined by solving the equation
$$
\Iminus\bigl(H\circ\UU_\ssH\bigr)=0\,.
\equation(Eliminate)
$$
If $c_\ssH$ is equal to zero,
or if \equ(Eliminate) cannot be solved
in the way described below, then $\RR(H)$ remains undefined.
Our choice $\tau_\ssH=\vartheta$ guarantees that
if $H$ is of the form \equ(Hqp), then so is $\LL H$,
i.e., the coefficient of $\omega\cdot p$ remains $1$.
The constant $c_\ssH$ is determined by the condition
$(\SS H)_{0,2}=1/2$.
Another $H$-dependent constant could be added to $\RR(H)$,
in order to guarantee e.g. that $(\RR(H))_{0,0}=0$.
These (somewhat arbitrary) normalization conditions ensure that
$\RR$ contracts along the orbits of scaling transformations.
Similarly, we expect the normalization map $\NN$
to make $\RR$ a contraction along the orbits
of coordinate changes $H\mapsto H\circ U_\phi\,$.
We will comment later on the corresponding choice of normal form
(resonant subspace).
Equation \equ(Eliminate) will be solved iteratively.
We now give a formal description of the first step.
Assume that $H=H_1+f_1$ is a small perturbation
of some resonant Hamiltonian $H_1\,$.
If we regard \equ(Eliminate) as an equation for the generating
function of $\UU_\ssH\,$,
then its first order approximation is
$$
\Iminus\bigl(f_1+\{H_1,\phi_1\}\bigr)=0\,.
\equation(Phi1)
$$
In order to get a unique solution, we also impose the condition
that $\phi_1$ be non-resonant.
Now define $H_2$ and $f_2$ to be the resonant and nonresonant part,
respectively, of $H\circ U_{\phi_1}\,$.
Having solved equation \equ(Eliminate) to first order in $f_1\,$,
we can expect $f_2$ to be much smaller than $f_1$.
Thus, we iterate the procedure,
and define $\UU_\ssH=U_{\phi_1}\circ U_{\phi_2}\circ\ldots$,
if the iteration converges.
The Hamiltonian $H_1$ that will be used in this procedure
is an approximate fixed point of $\RR$.
To be more precise,
we have determined numerically a resonant Hamiltonian $H_1\,$,
together with a generating function $\phi_0\,$,
in such a way that $\LL\SS H_1\approx H_1\,$.
In what follows,
we will limit the domain of $\RR$ to a small neighborhood of $H_1\,$,
and thus $\NN$ needs to be defined only near $H_1\,$.
This is why we can obtain $\UU_\ssH$ by perturbation theory.
Notice that the combination of $\NN$ with the other parts of $\RR$
involves a change of coordinates with
$U_{\phi_0}\circ U_{\phi_1}\circ U_{\phi_2}\circ\ldots$,
where all generating functions except $\phi_0$
depend on the argument of $\RR$.
The transformation $U_{\phi_0}$ can be viewed as a ``common factor'',
and we have chosen to incorporate this factor into the definition of $\LL$,
instead of making it part of $\UU_\ssH\,$.
For a RG analysis of near-integrable Hamiltonians [\rKi,\rAK],
this common factor is simply the identity.
\claim Definition(Spaces)
Given any vector $\rho=(\rho_1,\rho_2)$ with positive components,
and any $\alpha\ge 0$, define $\FF_{\rho,\alpha}$ to be
the (complex) Banach space of functions \equ(Fqp), for which the norm
$$
\|F\|_{\rho,\alpha}
=\!\sum_{(\nu,k)\in I}\bigl(|F_{\nu,k}|+|F'_{\nu,k}|\bigr)
e^{\alpha|\omega\cdot\nu|}\cosh(\rho_1\Omega\cdot\nu)\rho_2^k
\equation(RhoAlphaNorm)
$$
is finite. (We assume of course that $F'_{0,k}=0$ for all $k$.)
The odd an even subspaces of $\FF_{\rho,\alpha}$ will be denoted by
$\AA_{\rho,\alpha}$ and $\BB_{\rho,\alpha}\,$, respectively.
Furthermore, the affine space $H_0+\BB_{\rho,\alpha}\,$,
where $H_0(q,p)=\omega\cdot p$,
will be denoted by $\BB'_{\rho,\alpha}\,$.
In order to simplify notation,
we will drop the subscript $\alpha$, whenever $\alpha=0$.
If $\alpha>0$, then the functions in $\FF_{\rho,\alpha}$
are analytic on the complex domain $D_{\rho,\alpha}\,$,
defined by
$|\Im x|<\alpha$, $|\Im y|<\rho_1\,$, and $|z|<\rho_2\,$,
where
$$
x=\omega'\cdot q\,,\qquad
y=\Omega'\cdot q\,,\qquad
z=\Omega\cdot p\,,
\equation(xyzDef)
$$
and where $\omega'$ and $\Omega'$ are constant
multiples of $\omega$ and $\Omega$, respectively,
such that $\omega\cdot\omega'=\Omega\cdot\Omega'=1$.
The functions in $\FF_\rho$ are defined in
the complex domain $D_\rho\,$, characterized by
$\Im x=0$, $|\Im y|<\rho_1\,$, and $|z|<\rho_2\,$,
where they are continuous, and analytic in $y$ and $z$.
The main result of this paper is the following.
\claim Theorem(RRFix)
There exists an even real resonant Fourier-Taylor polynomial $h_1\,$,
an odd real Fourier-Taylor polynomial $\phi_0\,$,
and a choice of the parameters $\sigma,\kappa,\rho$,
such that $\RR$ defines a compact analytic map,
from some open neighborhood $B$ of $H_1=H_0+h_1$
in $\BB'_\rho\,$, to the resonant subspace of $\BB'_\rho\,$.
This map $\RR$ has a unique fixed point $H_\ast$ in $B$,
which is real, belongs to $\BB'_{\rho,\alpha}$ for some $\alpha>0$,
and is non-trivial, in the sense that $c_{\ssH_\ast}>1$.
Our proof of this theorem is computer-assisted.
As a by-product, we also obtain rigorous bounds
on the Fourier-Taylor coefficients of $H_\ast$,
and other quantities of interest.
For the normalization constant $c_{\ssH_\ast}\,$,
we obtain the bound $c_{\ssH_\ast}=1.024332969\ldots$,
which is consistent with the numerical results in [\rMcKi,\rAKW].
On a purely numerical level, the fixed point $H_\ast\,$,
and the corresponding scaling map
$\Lambda_\ast=\TT_{\mu_\ast}\circ U_{\phi_0}\circ\UU_{\LL H_\ast}\,$,
also satisfy a set of conditions that was shown in [\rKii]
to imply the existence of a ``critical'' invariant torus.
Here, $\mu_\ast=\mu_0/c_{\ssH_\ast}\,$.
We did not (yet) verify these conditions rigorously,
since they require bounds in different function spaces.
We note that the choice of the resonant projection $\Iplus$
is somewhat arbitrary, like other normalization conditions.
The properties of $\Iplusminus$ that play an important role
in our analysis are that $H\mapsto\Iplus(H\circ\TT_{\mu_\ssO})$
is analyticity improving, and that the condition \equ(Phi1)
defines a continuous linear map $f_1\mapsto\phi_1$
on the non-resonant subspace of $\BB_\rho\,$.
\clm(RRFix) is proved by converting the fixed point problem
for $\RR$, to a fixed point problem for
an approximate Newton map $\MM$ associated with $\RR$.
To be more precise, we choose an approximate inverse $M$
of $\Id-D\RR(H_1)$, and define
$$
\MM(h)=h+\RR(H_1+Mh)-(H_1+Mh)\,.
\equation(MMDef)
$$
The goal is then to show that $\MM$ is a contraction
on a small ball centered at zero in $\BB_\rho\,$.
This is a common strategy in computer-assisted proofs;
see e.g. [\rKSW] and references therein.
It usually involves explicit bounds on a
finite dimensional truncation of $\MM$,
and error bounds for the terms that were truncated.
In the case at hand, however,
working with a truncation of the full map $\MM$
turned out to be computationally prohibitive.
We solve this problem by using the fact that $\MM$
only needs to be estimated on a small open set.
More specifically, we approximate the most complex part of $\MM$,
which is the map $\NN$,
by a much simpler affine map $\NN_1\,$,
and then estimate the difference between the two.
Let $H_1$ be a fixed non-resonant Hamiltonian, and define
$$
\NN_1(H_1+f_1)=H_1+\Id^{+}\bigl(f_1+\{H_1,\phi_1\}\bigr)\,,
\equation(NN1Def)
$$
where $\phi_1$ is the solution of equation \equ(Phi1).
Then $\NN_1$ is an approximation of $\NN$,
in the sense that $\NN(H_1+f_1)-\NN_1(H_1+f_1)$
vanishes to first order in $f_1\,$.
The map $\NN_1$ can now be used to define an approximate
RG transformation
$$
\RR_1=\NN_1\circ\LL\circ\SS\,.
\equation(RR1Def)
$$
Notice that $\RR_1$ is nonlinear,
but only due to the trivial scaling transformation $\SS$.
In order to estimate the nonlinear term, let
$$
\wt\SS(H_1,f)=\SS(H_1+f)-\SS(H_1)-D\SS(H_1)f\,.
\equation(SStDef)
$$
Then, by using that $\NN_1$ is affine,
we can decompose $\RR_1$ as follows:
$$
\eqalign{
\RR_1(H_1+f)
&=\NN_1\bigl(\LL\SS(H_1)+\LL D\SS(H_1)f+\LL\wt\SS(H_1,f)\bigr)\cr
&=\RR_1(H_1)+D\RR_1(H_1)f+\wt\RR(H_1,f)\,,\cr}
\equation(R1Decomp)
$$
where
$$
\wt\RR(H_1,f)=D\NN_1(H_1)\LL\wt\SS(H_1,f)\,.
\equation(RRtDef)
$$
This leads to the following representation for the map $\MM$.
$$
\eqalign{
\MM(h)
&
=\bigl(\RR_1(H_1)-H_1\bigr)
+\bigl[\Id-\bigl(\Id-D\RR_1(H_1)\bigr)M\bigr]h\cr
&+\wt\RR(H_1,Mh)
+\bigl(\RR-\RR_1\bigr)(H_1+Mh)\,.\cr}
\equation(MMDecomp)
$$
The term in square brackets defines a linear operator on $\BB_\rho\,$,
which we will show to be of norm $K<1$.
Since the Hamiltonian $H_1$ is chosen to be
an approximate fixed point of $\RR$, and thus of $\RR_1\,$,
the term $\RR_1(H_1)-H_1$ in equation \equ(MMDecomp)
is small, say of norm $\eps>0$.
If $\MM$ is restricted to a ball $B$
of radius $R\eps$, centered at $h=0$, then formally,
the nonlinear (last two) terms on the right hand side of \equ(MMDecomp)
are of the oder $\OO(\eps^2)$.
Thus, if $(1-K)R>1$, and $\eps>0$ is sufficiently small,
we expect $\MM$ to map the ball $B$ into itself.
In order to prove that $\MM$ is a contraction,
we also need to estimate the derivatives of the nonlinear terms.
But by using analyticity, it suffices to estimate their norm,
on a slightly larger domain, say $2B$.
Formally, this yields a bound of the order $\OO(\eps)$.
What needs to be proved is that this bound is less than $1-K$.
The remaining part of this paper is organized as follows.
In the next two sections, we estimate the maps $\NN_1$ and $\RR_1\,$.
Section 4 describes the iterative solution
of equation \equ(Eliminate), which defines $\NN$.
The RG transformation $\RR$, and the contraction $\MM$,
are discussed in Section 5.
In particular, we show that \clm(RRFix) follows from a set of inequalities,
which are formulated in Theorem 5.2.
Section 6 contains an outline of our (computer-assisted) proof of Theorem 5.2.
The details of this proof are written in the programming language Ada95 [\rAda],
and can be found in Section.7 [\rKiii].
\section The transformation {\cbold N}$_1$
In this section, we discuss the map $\NN_1\,$,
and give some basic estimates for compositions
and derivatives of functions in $\FF_\rho\,$.
Here, and in what follows, $\rho$ is a fixed but arbitrary
domain parameter in $\real_{+}^2\,$.
If $L$ is a bounded linear operator on $\FF_\rho\,$,
then $\|L\|_\rho$ denotes the operator norm of $L$.
Define
$$
\eqalign{
\partial_x&=\omega\cdot\nablaq\,,\cr
\phantom{\DD_x}&\phantom{=1}\cr}
\qquad
\eqalign{
\partial_y&=\Omega\cdot\nablaq\,,\cr
\DD_y&=\partial_x^{-1}\partial_y\,,\cr}
\qquad
\eqalign{
\partial_z&=\Omega'\cdot\nablap\,,\cr
\DD_z&=\partial_x^{-1}\partial_z\,.\cr}
\equation(xyz)
$$
\claim Proposition(DDBounds)
$\DD_y\Iminus$ and $\DD_z\Iminus$
are bounded linear operators on $\FF_\rho\,$, with norms
$$
\bigl\|\DD_y\Iminus\bigr\|_\rho\le\sigma^{-1}\,,\qquad
\bigl\|\DD_z\Iminus\bigr\|_\rho\le(\kappa\rho_2)^{-1}\,.
\equation(DDBounds)
$$
\proof
Let $\psi=\cos(\nu\cdot Q)Z^k$ or $\psi=\sin(\nu\cdot Q)Z^k$,
with $(v,k)$ belonging to the complement of $\iplus$ in $I$.
Here, $Q(q,p)=q$, and $Z(q,p)=\Omega\cdot p$.
By using that $|\Omega\cdot\nu|/|\omega\cdot\nu|<\sigma^{-1}$
and $k/|\omega\cdot\nu|<\kappa^{-1}$, we immediately get the bounds
$\|\DD_2\psi\|_\rho\le\sigma^{-1}\|\psi\|_\rho$
and $\|\DD_2\psi\|_\rho\le(\kappa\rho_2)^{-1}\|\psi\|_\rho\,$.
These bounds extend by linearity to all of $\Iminus\FF_\rho\,$,
which proves the claim.
\qed
Next, we consider the map $\NN_1$ described in equation \equ(NN1Def).
Consider a function $h_1$ whose partial derivatives
$\partial_z h_1$ and $\partial_y h_1$ belong to $\FF_\rho\,$,
and define
$$
\DD(h_1)=\bigl[(\partial_z h_1)\DD_y-(\partial_y h_1)\DD_z\bigr]\Iminus\,.
\equation(AhDef)
$$
Let $H_1=H_0+h_1\,$, and assume that
$$
\|\DD(h_1)\|_\rho\le A<1\,.
\equation(DDhContracts)
$$
Then for every function $f_1\in\BB_\rho\,$,
the equation \equ(Phi1) has a solution given by
$$
\phi_1=\partial_x^{-1}\psi_1\,,\qquad
\psi_1=\bigl[\Id+\Iminus \DD(h_1)\bigr]^{-1}\Iminus f_1\,.
\equation(Psi1)
$$
Clearly, the function $\psi_1\in\Iminus\BB_\rho$
is uniquely determined by $f_1$ and satisfies the bound
$$
\|\psi_1\|_\rho\le(1-A)^{-1}\|f_1\|_\rho\,.
\equation(PsiBound)
$$
The map $\NN_1$ can now be written as follows:
$$
\NN_1(H_1,f_1)=H_1+\Iplus f_1-\Iplus \DD(h_1)\psi_1\,.
\equation(NN1Def)
$$
Here, we have re-defined $\NN_1$ as a function of two variables,
in order to emphasize the dependence on the choice of $H_1\,$.
Estimating $\NN_1$ requires a bounds on the last term
in equation \equ(NN1Def).
We will do this by using a numerical approximation $\psi\in\Iminus\BB_\rho$
for the function $\psi_1$ defined in \equ(Psi1).
Since
$$
\psi_1-\psi=\bigl[\Id+\Iminus \DD(h_1)\bigr]^{-1}
\bigl(\Iminus f_1-\Iminus[\Id+\DD(h_1)]\psi\bigr)\,,
\equation(PsiDiff)
$$
we have immediately the following
\claim Proposition(NN1Bound)
If $\psi$ is any non-resonant function in $\BB_\rho\,$, then
$$
\bigl\|\Iplus \DD(h_1)\psi_1-\Iplus \DD(h_1)\psi\bigr\|_\rho
\le{A\over 1-A}\bigl\|\Iminus f_1
-\Iminus[\Id+\DD(h_1)]\psi\bigr\|_\rho\,.
\equation(NN1Bound)
$$
This inequality shows in particular (setting $\psi=0$)
that $f\mapsto\NN_1(H_1,f)$
is a continuous linear operator on $\BB_\rho\,$.
We conclude this section with a bound on $\DD(h)$,
and some other basic estimates that will be used later.
Define
$$
\Gamma(s)=\Gamma(s,0,0),\qquad
\Gamma(s,t,v)=\sup_{u\ge v}{\cosh(su)\over\cosh(u)}
e^{(1-s-t)u}\,,\qquad s,t,v\ge 0\,.
\equation(GammaDef)
$$
\claim Proposition(Basic)
Consider functions $f,G\in\FF_\rho$ and $h\in\FF_{\rho'}\,$,
and the change of variables
$U(q,p)=(q+f(q,p)\Omega,G(q,p)\Omega')$.
Then
\item{$(a)$}
$\|fG\|_\rho\le\|f\|_\rho\|G\|_\rho\,$.
%
\item{$(b)$}
$\|h\circ U\|_\rho\le\Gamma(\rho'_1/\rho_1)\|h\|_{\rho'}\,$,\ \ if
$\rho'_1\ge\rho_1+\|f\|_\rho$ and $\rho'_2\ge\|g\|_\rho\,$.
%
\item{$(c)$}
$\|\DD(h)\|_\rho\le s_0^{-1}\Gamma(\rho'_1/\rho_1)\|h\|_{\rho'}\,$,\ \ if
$\rho'_1\ge\rho_1+s_0/(\kappa\rho_2)$ and
$\rho'_2\ge\rho_2+s_0/\sigma$ and $s_0>0$.
%
\item{$(d)$}
$\|\DD(h)\|_\rho\le\sigma^{-1}\|\partial_z h\|_\rho
+(\kappa\rho_2)^{-1}\|\partial_y h\|_\rho\,$,\ \ if
$\rho'_1\ge\rho_1$ and $\rho'_2\ge\rho_2\,$.
%
\item{$(e)$}
$\|\partial_y h\|_\rho\le(e\delta_1)^{-1}
\Gamma(\rho_1/\rho'_1)\|h\|_{\rho'}\,$,\ \ if
$\rho'_1=\rho_1+\delta_1>\rho_1$ and $\rho'_2\ge\rho_2\,$.
%
\item{$(f)$}
$\|\partial_z h\|_\rho\le\delta_2^{-1}\|h\|_{\rho'}\,$,\ \ if
$\rho'_1\ge\rho_1$ and $\rho'_2=\rho_2+\delta_2>\rho_2\,$.
\proof
The first and last bounds are straightforward to check.
In order to prove $(b)$, consider first the case
$h=\cos(\nu\cdot Q)Z^k$,
where $Q(q,p)=q$ and $Z(q,p)=\Omega\cdot p$. Then
$$
\eqalign{
\|h\circ U\|_\rho
&=\bigl\|\bigl[\cos(\nu\cdot Q)\cos(\nu\cdot\Omega f)
-\sin(\nu\cdot Q)\sin(\nu\cdot\Omega f)\bigr]g^k\bigr\|_\rho\cr
&\le\cosh(\rho_1\Omega\cdot\nu)
\bigl[\cosh\bigl(\|\nu\cdot\Omega f\|_\rho\bigr)
+\sinh\bigl(\|\nu\cdot\Omega f\|_\rho\bigr)\bigr]\|g\|_\rho^k\cr
&\le{\cosh(\rho_1\Omega\cdot\nu)\over\cosh(\rho'_1\Omega\cdot\nu)}
e^{|\Omega\cdot\nu|\|f\|_\rho}
\cosh(\rho'_1\Omega\cdot\nu)\bigl(\rho'_2\bigr)^k\cr
&\le\Gamma(\rho_1/\rho'_1)\|h\|_{\rho'}\,,\cr}
\equation(BasicB)
$$
and an analogous bound holds for $h=\sin(\nu\cdot Q)Z^k$.
Since we are dealing with weighted $\ell^1$ spaces,
the claim $(b)$ now follows by taking linear combinations and limits.
The bound $(c)$ is obtained from \clm(DDBounds) and $(b)$,
by taking a general non-resonant $\psi$
in the unit ball of $\BB_\rho\,$,
and estimating the derivative in
$$
\bigl\|\DD(h_1)\psi\bigr\|_\rho
=\left\|{d\over ds}
h\bigl(Q+s[\DD_z\psi]\Omega,
[Z-s\DD_y\psi]\Omega'\bigr)\Bigm|_{s=0}\right\|_\rho\,,
\equation(BasicC)
$$
using Cauchy's formula with contour $|s|=s_0$.
The inequality $(d)$ follows immediately from \clm(DDBounds) and $(a)$.
In order to prove $(e)$, consider again $h=\cos(\nu\cdot Q)Z^k$.
By using that
$|\Omega\cdot\nu|\le(e\delta_1)^{-1}\exp(\delta_1|\Omega\cdot\nu|)$,
we obtain the bound
$$
\eqalign{
\|\partial_y h\|_\rho&=\|(\Omega\cdot\nu)\sin(\nu\cdot Q)Z^k\|_\rho
=|\Omega\cdot\nu|\cosh(\rho_1\Omega\cdot\nu)\rho_2^k\cr
&\le{\cosh(\rho_1\Omega\cdot\nu)\over\cosh(\rho'_1\Omega\cdot\nu)}
|\Omega\cdot\nu| \|h\|_{\rho'}
\le(e\delta_1)^{-1}\Gamma(\rho_1/\rho'_1)\|h\|_{\rho'}\,.\cr}
\equation(DerBoundsQ)
$$
Similarly for $h=\sin(\nu\cdot Q)Z^k$.
The claim $(e)$ now follows by taking linear combinations and limits.
\qed
These bounds will typically be used for $\rho'$ close to $\rho$.
In order to give an idea of the size of $\Gamma(s)$
in such cases, we note that for $0~~\rho$.
One of the ingredients of $\RR_1$ is a canonical change
of variables $H\mapsto H\circ U_{\phi_0}\,$,
determined via equation \equ(UphiDef)
from its generating function $\phi_0\,$.
We assume that $\phi_0(q,p)$ is odd,
and that the first partial derivatives of $\psi_0\,$,
including $\psi_0=\partial_x\phi_0\,$,
belong to $\FF_{\rho'}\,$,
for $\rho'$ sufficiently large
(explicit conditions will be given below).
The second equation in \equ(UphiDef)
yields the following equation for $g=\Omega\cdot P$.
$$
g(q,p)=-[\DD_y\psi_0]\bigl(q,p+g(q,p)\Omega'\bigr)\,.
\equation(KKFix1)
$$
We note that the argument $p+g(q,p)\Omega'$ above could be replaced
by $G(q,p)\Omega'$ with $G(q,p)=\Omega\cdot p+g(q,p)$.
Thus, \clm(Basic).b applies to compositions of this type.
In order to solve equation \equ(KKFix1),
we first determine an approximate solution $g_0\in\BB_{\rho''}\,$,
and then estimate the error.
To this end, define
$$
a=\bigl\|[\partial_z\DD_y\psi_0](.,.+g_0\Omega')\bigr\|_{\rho''}\,,
\quad
\eps=\bigl\|[\DD_y\psi_0](.,.+g_0\Omega')+g_0\bigr\|_{\rho''}\,,
\equation(KKFix2)
$$
and if $a<1$, choose a real number $b$ such that
$$
b\ge\bigl\|\bigl[\partial_z^2\DD_y\psi_0\bigr]
(.,.+g\Omega')\bigr\|_{\rho''}
{\rm ~~~whenever~~~} \|g-g_0\|_{\rho''}\le 2\eps/(1-a)\,.
\equation(KKFix3)
$$
\claim Proposition(KKFix0)
If $a<1$ and $4b\eps\le(1-a)^2$, then the equation \equ(KKFix1)
has a unique solution in $g\in\BB_{\rho''}$
within a distance $r=2\eps/(1-a)$ of $g_0\,$,
assuming that $\DD_y\psi_0$ and $\DD_z\psi_0$
belong to $\AA_{\rho'}\,$,
with $\rho'_1=\rho''_1$ and $\rho'_2>\rho''_2+\|g_0\|_{\rho''}+r$.
\proof
$G$ solves equation \equ(KKFix1) if and only if
$h=g-g_0$ is a fixed point of the map $\KK$,
defined by
$$
\KK(h)=h_0+K(h)h\,,\qquad
K(h)=-\int\limits_0^1
[\partial_z\DD_y\psi_0]\bigl(.,.+(g_0+sh)\Omega'\bigr) ds\,,
\equation(KKFix4)
$$
where $h_0=-[\DD_y\psi_0](.,.+g_0\Omega')-g_0\,$.
Denote by $B$ the closed ball of radius $r$ in $\BB_{\rho''}\,$,
centered at the origin.
By the mean value theorem,
$$
\|K(h)-K(h')\|_{\rho''}\le{b\over 2}\|h-h'\|_{\rho''}\,,
\equation(KKFix5)
$$
whenever $h,h'\in B$, and by taking $h'=0$,
we obtain the bound $\|K(h)\|_{\rho''}\le a+{b\over 2}\|h\|_{\rho''}\,$.
Thus, if $h$ and $h'$ belong to $B$, then
$$
\eqalign{
\|\KK(h)-\KK(h')\|_{\rho''}&=\|[K(h)-K(h')]h+K(h')[h-h']\|_{\rho''}\cr
&\le{b\over 2}\|h-h'\|_{\rho''}\|h\|_{\rho''}
+\left(a+{b\over 2}\|h'\|_{\rho''}\right)\|h-h'\|_{\rho''}\cr
&\le(a+br)\|h-h'\|_{\rho''}
\le{a+1\over 2}\|h-h'\|_{\rho''}\,.\cr}
\equation(KKFix6)
$$
By taking again $h'=0$, we find that $\|\KK(h)\|_{\rho''}\le r$.
Thus, $\KK$ is a contraction on $B$,
and the assertion follows.
For reference later on, we note that the fixed point $h\in B$
of $\KK$ satisfies the equation $h=h_0/(1-K(h))$.
This leads to the bound
$$
\|h\|_{\rho''}\le\eps\bigl\|1/\bigl(1-K(h)\bigr)\bigr\|_{\rho''}\,.
\equation(gBound)
$$
\qed
In what follows, we assume that equation \equ(KKFix1)
has a solution $g\in\BB_{\rho''}\,$.
The canonical transformation $U_{\phi_0}$ can now be written
explicitly as
$$
U_{\phi_0}(q,p)
=\Bigl(q+[\DD_z\psi_0]\bigl(q,p+g(q,p)\Omega'\bigr)\Omega,\,
p+g(q,p)\Omega'+\gamma(q,p)\omega'\Bigr)\,,
\equation(Uphi0)
$$
with $\gamma(q,p)=-\psi_0(q,p+g(q,p)\Omega')$.
As a result, we have the following expression
for the linear transformation $\LL$ defined in \equ(NNLLSSDef).
Let $G(q,p)=\Omega\cdot p+g(q,p)$. Then
$$
(\LL H)(q,p)
=\omega\cdot p-\psi_0\bigl(q,G(q,p)\Omega'\bigr)+(Lh)(q,p)\,,
\equation(LLH)
$$
where $h=H-H_0$ and
$$
(Lh)(q,p)
=\vartheta^4h\bigl(Tq-\vartheta^{-1}[\DD_z\psi_0](q,G(q,p)\Omega')\Omega,
-\vartheta^{-2}G(q,p)\Omega'\bigr)\,.
\equation(LhDef)
$$
Define
$$
b_2=\|G\|_{\rho''}\,,\qquad
b_1=\|\DD_z\psi_0\|_{(\rho''_1,b_2)}\,,
\equation(bDef)
$$
assuming that $\DD_z\psi_0$ belongs to $\AA_{(\rho''_1,b_2)}\,$.
\claim Proposition(LBound)
Let $h\in\BB_{\rho'}$ with
$\rho'_1>\vartheta^{-1}(\rho''_1+b_1)$ and $\rho_2'=\vartheta^{-2}b_2\,$.
Then $Lh$ belongs to $\BB_{\rho''}\,$,
and if the Fourier-Taylor series \equ(Fqp) of $h$
only includes frequencies $\nu$
satisfying a bound $|\Omega\cdot\nu|\ge\lambda\ge 0$, then
$$
\|Lh\|_{\rho''}\le\vartheta^4\Gamma\bigl(
\rho''_1/\rho'_1,1-(\rho''_1+b_1)/(\vartheta\rho'_1),\lambda/\rho'_1\bigr)
\|h\|_{\rho'}\,.
\equation(LhBound)
$$
\proof
Consider first $h=\cos(\nu\cdot Q)Z^k$,
where $Q(q,p)=q$ and $Z(q,p)=\Omega\cdot p$.
Define $f(q,p)=[\DD_z\psi_0](q,G(q,p)\Omega')$.
This function $f$ belongs to $\AA_{\rho''}$ and is bounded in norm by $b_1\,$,
as \clm(Basic).b shows.
Thus, we have the bound
$$
\eqalign{
\|Lh\|_{\rho''}
&=\Bigl\|\vartheta^4\bigl[\cos\bigl((T\nu)\cdot Q\bigr)
\cos\bigl(\vartheta^{-1}(\Omega\cdot\nu)f\bigr)\cr
&\phantom{xxxx}+\sin\bigl((T\nu)\cdot Q\bigr)
\sin\bigl(\vartheta^{-1}(\Omega\cdot\nu)f\bigr)\bigr]
\bigl(\vartheta^{-2}G\bigr)^k\Bigr\|_{\rho''}\cr
&\le\vartheta^4\cosh\bigl({\rho''}_1\vartheta^{-1}\Omega\cdot\nu\bigr)
e^{\vartheta^{-1}|\Omega\cdot\nu|\|f\|_{\rho''}}
\bigl(\vartheta^{-2}\|G\|_{\rho''}\bigr)^k\cr
&\le\vartheta^4\|h\|_{\rho'}
{\cosh(\rho''_1\vartheta^{-1}\Omega\cdot\nu)\over\cosh(\rho'_1\Omega\cdot\nu)}
e^{\vartheta^{-1}|\Omega\cdot\nu|b_1}\,,\cr
}
$$
which implies \equ(LhBound).
The generalization to arbitrary $h\in\BB_{\rho'}$
follows by taking linear combinations and limits.
\qed
Our next goal is to define $\RR_1$ as the composition
$$
\RR_1:\
\BB'_\rho\ \mapright{\SS}\
\BB'_{\rho'}\ \mapright{\LL}\
\BB'_{\rho''}\ \mapright{\NN_1}\
\BB'_{\rho''}\,,
\equation(SSLLNN1)
$$
with some additional restriction on the domain.
Here, $\rho'=(\rho_1,\vartheta^{-2}b_2)$.
By combining \clm(LBound) and \clm(NN1Bound),
we obtain immediately the following
\claim Corollary(RR1Domain)
Let $\rho''>\rho>0$.
Denote by $B$ the set of all functions $H\in\BB'_\rho$
satisfying
$$
2|H_{0,2}|\rho_2>\vartheta^{-2}b_2\,.
\equation(cHCondition)
$$
Assume that $b_1<\vartheta\rho_1-\rho''_1\,$,
and that $H_1=H_0+h_1$ is a Hamiltonian in $B$
for which $\|\DD(h_1)\|_{\rho''}$ is finite, and less than $1$.
Then $\RR_1=\NN_1\circ\LL\circ\SS$ is well defined
and analytic as a map from $B$ to $\BB'_{\rho''}\,$.
The analyticity of $\RR_1$ follows from
the analyticity of the map $\SS$,
together with the fact that $\NN_1$ and $\LL$ are affine
and continuous on the spaces indicated in \equ(SSLLNN1).
We note that $\RR_1(H)$ is always resonant.
The following fact shows that, as a consequence,
$\RR_1$ is analyticity improving, and thus also compact,
when considered as a map from $\BB'_\rho$ to itself.
\claim Proposition(Trivial)
If $\rho^\ast=(\rho_1+\alpha\sigma,e^{\alpha\kappa}\rho_2)$
with $\alpha\ge 0$, then $\Iplus\FF_{\rho^\ast}$
is contained in $F_{\rho,\alpha}\,$.
This proposition follows from a simple but important property
of the projection $\Iplus$:
Under the given assumption,
$$
e^{\alpha|\omega\cdot\nu|}\
\cosh(\rho_1\Omega\cdot\nu)\rho_2^k
\le\Gamma(\rho_1/\rho^\ast_1)\cosh(\rho^\ast_1\Omega\cdot\nu)
\bigl(\rho'_2\bigr)^k\,,\qquad
(\nu,k)\in\iplus\,.
\equation(RhoAlphaFact)
$$
\section The transformation {\cbold N}
As mentioned in the introduction,
the transformation $\UU_\ssH$ is defined as a composition
$$
\UU_\ssH=U_{\phi_1}\circ U_{\phi_2}\circ U_{\phi_3}\circ\ldots\,,
\equation(UPhiProd)
$$
where $U_{\phi_1}$ is determined in such as way that
$H\mapsto H\circ U_{\phi_1}$ eliminates the
leading non-resonant part of $H=H_1+f_1\,$,
and the other canonical transformations $U_{\phi_k}$
are obtained by iterating the same procedure.
The precise definition of $\phi_1$ is given by equation \equ(Psi1).
\claim Proposition(KKFix1)
Let $\rho'=(\rho_1,\rho_2+\delta_2)$ with $\delta_2>0$.
Let $\psi_1$ be a non-resonant function in $\BB_{\rho'}$
which satisfies
$$
(\sigma\delta_2)^{-1}\|\psi_1\|_{\rho'}\le\tau<1/2\,.
\equation(KKFix7)
$$
Then the equation \equ(KKFix1), with $\psi_0=\psi_1\,$,
has a unique solution $g$ in the ball $B$
of radius $\delta_2/2$ in $\BB_\rho\,$, centered at the origin, and
$$
\|g\|_\rho\le\|\DD_y\psi_1\|_{\rho'}
\le\sigma^{-1}\|\psi_1\|_{\rho'}\,.
\equation(KKFix8)
$$
\proof
Let $r=(\rho_1,\rho_2+\delta_2/2)$.
Denote by $\KK$ the map that assigns to $g\in B$
the function on the right hand side of \equ(KKFix1),
with $\psi_0=\psi_1\,$.
Then the bound \equ(DDBounds) and \clm(Basic) imply that
$$
\eqalign{
\|\KK(g)\|_\rho
&\le\|\DD_y\psi_1\|_{\rho'}
\le\sigma^{-1}\|\psi_1\|_{\rho'}<\delta_2/2\,,\cr
\|\KK(g)-\KK(g')\|_\rho
&\le\|\partial_z\DD_y\psi_1\|_r\|g-g'\|_\rho
\le 2\tau\|g-g'\|_\rho\,,\cr}
\equation(KKFix9)
$$
for any functions $g,g'\in B$.
This shows that $\KK$ is a contraction on $B$,
and thus has a unique fixed point in $B$.
The bound \equ(KKFix8) follows from the first part
of \equ(KKFix9).
\qed
\claim Proposition(UphiBounds)
Let $\rho'=(\rho_1+\delta_1,\rho_2+\delta_2)$
with $\delta_1\ge(\kappa\rho'_2)^{-1}\sigma\delta_2>0$.
Let $h_1$, $f_1$, and $\psi_1$ be functions in $\BB_{\rho'}\,$,
and define $H_1=H_0+h_1\,$.
If $\psi_1$ is non-resonant and satisfies \equ(KKFix7), then
$$
\eqalign{
\bigl\|f_1\circ U_{\phi_1}-f_1\bigr\|_\rho
&\le{(\sigma\delta_2)^{-1}\over 1-\tau}
\Gamma\bigl(\rho_1/\rho'_1\bigr)
\|f_1\|_{\rho'}\|\psi_1\|_{\rho'}\,,\cr
\bigl\|H_1\circ U_{\phi_1}-H_1-\{H_1,\phi_1\}\bigr\|_\rho
&\le{(\sigma\delta_2)^{-2}\over 1-\tau}
\Bigl(\sigma\delta_2
+\Gamma\bigl(\rho_1/\rho'_1\bigr)\|h_1\|_{\rho'}\Bigr)
\|\psi_1\|_{\rho'}^2\,.\cr}
\equation(UphiBounds)
$$
\proof
The case $\psi_1=0$ is trivial.
Assume now that $\psi_1\not=0$, and consider the family of functions
$$
F(s)(q,p)
=f_1\bigl(q+s[\DD_z\psi_0]\bigl(q,p+g(q,p)\Omega'\bigr)\Omega,\,
p+sg(q,p)\Omega'\bigr)\,,
$$
where $g$ is the solution of \equ(KKFix1) described in \clm(KKFix1).
Let $10$ component-wise,
and that
$$
\|f_n\|_{\rho'}\le C_n\,,\quad
\|H_n-H_0\|_{\rho'}\le B_n\,,\quad
\|\DD(H_n-H_0)\|_{\rho'}\le A_n<1\,.
\equation(ABC)
$$
Implicit in this assumption is that $f_n\,$, $h_n=H_n-H_0\,$,
and $\partial_z h_n$ belong to $\BB_{\rho'}\,$,
and that $\partial_y h_n$ belong to $\AA_{\rho'}\,$.
This will not always be mentioned.
Our goal is to obtain analogous bounds, in $\BB_\rho\,$,
for the functions
$$
H_{n+1}=\Iplus\bigl[(H_n+f_n)\circ U_{\phi_n}\bigr]\,,\qquad
f_{n+1}=\Iminus\bigl[(H_n+f_n)\circ U_{\phi_n}\bigr]\,,
\equation(NStepDef)
$$
where $\phi_n$ is the generating function given
by the analogue of equation \equ(Psi1),
where all indices $1$ have been replaced by $n$.
To this end, define
$$
\tau_n(x)={C_n\over\sigma x(1-A_n)}\,,\quad
K_n(x)={(2-A_n)\sigma x+B_n\over
\sigma^2\bigl(1-\tau_n(x)\bigr)(1-A_n)^2}
\Gamma\bigl(\rho_1/\rho'_1\bigr)\,,
\equation(TauK)
$$
for $0m$, the functions $H_n-H_0$ and $f_n$
belong to $\BB_{\rho^{(n)}}$ and satisfy the bounds
$$
\|f_n\|_{\rho^{(n)}}\le C_n\le 4^{-n+m}C_m\,,\qquad
\|H_n-H_m\|_{\rho^{(n)}}\le B_n-B_m\le{13\over 3}\;C_m\,.
\equation(Cn)
$$
\proof
We proceed by induction, using \clm(CBABounds)
with the parameters \equ(CBADomain0).
In fact, we will weaken the bounds \equ(CBABounds) slightly,
by substituting $\rho^\ast_2$ for $\rho'_2$
in the definition of the parameter $d$.
Let now $i\ge m$ be fixed, and consider $m\le n\le i$.
Assume that the first bound in \equ(Cn) holds,
together with the inequalities
$$
\|H_n-H_0\|_{\rho^{(n)}}\le B_n\le{1\over 6}\,,\qquad
\|\DD(H_n-H_0)\|_{\rho^{(n)}}\le A_n\le{3\over 4}\,.
\equation(ABn)
$$
Define $d_n=2^{-n+m}d_m$.
From the assumptions \equ(ABm) and \equ(Cm), it follows e.g.
that $d_m<1/6$ and $C_m0$, we define a sequence of triples $(A_n,B_n,C_n)$,
using equation \equ(CBABounds), with $k=0$ for $n=1$,
and $k=1$ otherwise.
\claim Corollary(NNDiffBound)
If $\|f_1\|_{\rho^{(1)}}\le C_1\,$, and $C_m$ satisfies
the second inequality in \equ(Cm), then the limit
$$
\NN(H_1+f_1)=\lim_{n\to\infty}H_n
\equation(NNLimit)
$$
exists in $\BB_{\rho^\ast}$ and satisfies the bound
$$
\|\NN(H_1+f_1)-\NN_1(H_1,f_1)\|_{\rho^\ast}
\le C_2+\sum_{n=2}^{m-1}\Delta B_n +{13\over 3}C_m\,.
\equation(NNDiffBound)
$$
\proof
The inequality \equ(NNDiffBound) follows from the identity
$$
\NN(H_1+f_1)-\NN_1(H_1,f_1)=\Iplus R(H_1,f_1)
+\sum_{n=2}^\infty\bigl(H_{n+1}-H_n\bigr)\,,
\equation(NNDiff)
$$
using \clm(IterN), and the bound \equ(RBound).
\qed
At this point, we take equation \equ(NNLimit)
as our definition of the map $\NN$.
Some properties of $\NN$ are summarized in the
\claim Lemma(NNProp)
Assume that $C_1>0$ is sufficiently small, such that
$C_m$ satisfies the second inequality in \equ(Cm).
Consider an open ball $B$ in $\BB_{\rho^{(1)}}$
of radius less than $C_1\,$, centered at $H_1\,$.
Then $\NN$ is well defined and analytic,
as a map from $B$ to $\Iplus \BB_{\rho^\ast}\,$.
For every Hamiltonian $H$ in $B$,
the equation \equ(UPhiProd) defines a map $\UU_\ssH$
from $D_{\rho^\ast}$ to $D_{\rho^{(1)}}\,$, and we have
$$
\NN(H)=H\circ\UU_\ssH\,.
\equation(NNeqHoUU)
$$
If $H_1$ and $H\in B$ belong to $\BB_{\rho^{(1)},\eps}\,$,
for some $\eps>0$, then there exists $\alpha>0$, such that
$\UU_\ssH$ extends to an analytic canonical transformation
from $D_{\rho^\ast,\alpha}$
to $D_{\rho^{(1)},\alpha}\,$.
\proof
The analyticity of $\NN$ follows from the uniform convergence
of our iteration schemes.
The convergence of the infinite composition \equ(UPhiProd),
uniformly on compact subsets of $D_{\rho^\ast}\,$,
can be proved as in [\rAK].
This yields a map
$\UU_\ssH: D_{\rho^\ast}\to D_{\rho^{(1)}}\,$,
which satisfies equation \equ(NNeqHoUU).
At this point, it is useful to note that
we could have chosen any fixed $\alpha\ge 0$
in the definition of (the norm in) the spaces $\FF_{\rho}\,$,
without affecting any of the estimates in this section.
The only change, when increasing $\alpha$,
is that the results apply to fewer Hamiltonians.
Assume now that $H_1$ belongs to $\BB_{\rho^{(1)},\eps}\,$,
for some $\eps>0$.
Then we can find $\alpha>0$,
such that the bounds \equ(AB1) remain satisfied,
if $\|.\|_{\rho^{(1)}}$ is replaced by $\|.\|_{\rho^{(1)},\alpha}\,$,
and such that $B$ is contained in an open ball in $\BB_{\rho,\alpha}$
of radius less than $C_1\,$, centered at $H_1\,$.
For a Hamiltonian $H$ in this ball,
we now obtain convergence of \equ(UPhiProd)
on compact subsets of $D_{\rho^\ast,\alpha}\,$,
which preserves analyticity.
\qed
\section The transformations {\cbold R} and {\cbold M}
The transformation $\MM$ will be estimated
by using the decomposition \equ(MMDecomp).
Controlling the affine part (first two terms)
is relatively straightforward, albeit tedious,
using the estimates from Section 3
and the formula for $D\SS(H_1)$ given below.
What remains to be discussed are the nonlinear (last two) terms
in the decomposition \equ(MMDecomp) of $\MM$.
We start by considering the normalization transformations $\SS$,
defined by equation \equ(NNLLSSDef).
In what follows, the approximate RG fixed point $H_1$
is always assumed to be a Fourier-Taylor polynomial.
This is not really necessary, but it is sufficient
and simplifies the discussion.
Given $H_1=H_0+h_1\,$, let $c=2(h_1)_{0,2}\,$.
If $f$ is any function of $q$ and $p$, define
$$
\wh f=\SS_c f\,,\qquad
(\SS_\lambda f)(q,p)=\lambda f(q,p/\lambda)\,,\qquad
\lambda\in\complex\setminus\{0\}\,.
\equation(SScDef)
$$
Then the derivative of $\SS$ at $H_1\,$,
and the nonlinear part \equ(SStDef) of $\SS$,
can be written as
$$
\eqalign{
D\SS(H_1)f
&=\wh f+\epsilon\bigl(\wh{H_1}-Z\partial_z\wh{H_1}\bigr)\,,\cr
\wt\SS(H_1,f)
&=\bigl[\SS_{1+\epsilon}\wh{H_1}-\wh{H_1}
-\epsilon\bigl(\wh{H_1}-Z\partial_z\wh{H_1}\bigr)\bigr]
+\bigl(\SS_{1+\epsilon}\wh f-\wh f\ \bigr)\,,\cr}
\equation(DSS)
$$
where $\epsilon=2\wh f_{0,2}$ and $Z(q,p)=\Omega\cdot p$.
Due to our assumption on $H_1\,$,
the derivative $D\SS(H_1)$ is bounded as a linear operator
from $\BB_\rho$ to $\BB_{\hat\rho}\,$,
for $\hat\rho=(\rho_1,c\rho_2)$.
Furthermore, the term in square brackets in equation \equ(DSS)
can be controlled by an explicit computation.
The following proposition can be used to estimate
the remaining part of $\wt\SS(H_1,f)$.
\claim Proposition(SScBound)
Assume $\rho'_1=\hat\rho_1$ and $\rho'_2<\hat\rho_2\,$.
If $\wh f$ belongs to $\BB_{\hat\rho}$
and $|\epsilon|$ is less than $\epsilon_0=1-\rho'_2/\hat\rho_2\,$, then
$$
\bigl\|\SS_{1+\epsilon}\wh f-\wh f\;\bigr\|_{\rho'}
\le|\epsilon|\left(1+{1\over\epsilon_0-|\epsilon|}\right)
\bigl\|\wh f\,\bigr\|_{\hat\rho}\,.
\equation(SScBound1)
$$
\proof
If we define $\wh f_\lambda(q,p)=\wh f(q,p/\lambda)$, then
$$
\bigl\|\wh f_{1+\epsilon}-\wh f\;\bigr\|_{\rho'}
\le\Biggl\|{1\over 2\pi i}\oint\limits_{|\lambda|=\lambda_0}\!\!
{\epsilon\over\lambda(\lambda-\epsilon)}
\wh f_\lambda\, d\lambda\Biggr\|_{\rho'}
\le{|\epsilon|\over\epsilon_0-|\epsilon|}\bigl\|\wh f\,\bigr\|_{\hat\rho}\,,
\equation(ScB2)
$$
and by adding to this
$\bigl\|\epsilon\wh f_{1+\epsilon}\bigr\|_{\rho'}
\le|\epsilon|\bigl\|\wh f\,\bigr\|_\rho\,$,
the bound \equ(SScBound1) follows.
\qed
What remains to be done is to put all the pieces together.
By using that $\SS=\SS\circ\SS_c\,$,
we define $\RR$ to be the following composition of maps:
$$
\RR:\
\BB'_\rho\ \mapright{\SS_c}\
\BB'_{\hat\rho}\ \mapright{\SS}\
\BB'_{\rho'}\ \mapright{\LL}\
\BB'_{\rho''}\ \mapright{\NN}\
\BB'_{\rho^\ast}\,,
\equation(SSLLNN)
$$
with some additional restriction on its domain.
To be more precise about the domain, let us fix $\rho''>\rho^\ast>\rho$.
Assume that the function $\psi_0$ defining
the canonical transformation $U_{\phi_0}$
satisfies the conditions given in Section 3,
so that $\LL$ is a well defined and continuous map
between the spaces indicated in \equ(SSLLNN).
Here, $\hat\rho=(\rho_1,c\rho_2)$
and $\rho'=(\rho_1,\vartheta^{-2}b_2)$,
with $b_2$ the constant defined by equation \equ(bDef).
In order to benefit from \clm(SScBound),
we restrict $\RR$ to Hamiltonians $H=H_1+f$ for which
$$
2\bigl|\wh f_{0,2}\bigr|<1-\vartheta^{-2}b_2/(c\rho_2)\,,
\equation(SSDomain)
$$
assuming that this inequality holds for $f=0$.
Additional choices, and conditions,
are involved in the definition of $\NN$,
as described in Section 4.
This includes the domain parameter $\rho^{(1)}$,
which we take to be $\rho''$,
and the bounds \equ(AB1) on the Hamiltonian $H_1\,$.
For the purpose of this section,
the domain $D_\RR$ of $\RR$ is now defined as the set of all Hamiltonians
$H=H_1+f$ in $\BB'_\rho$ that satisfy the condition \equ(SSDomain),
and are mapped into the domain of $\NN$ by $\LL\circ\SS$.
This in turn defines the domain of the map $\MM$,
given by equation \equ(MMDef),
as the inverse image of $D_\RR$ under $h\mapsto H_1+Mh$.
Here, $M$ is a fixed linear isomorphism of $\BB_\rho\,$,
chosen to be an approximate inverse of $\Id-D\RR_1(H_1)$.
Denote by $B(r)$ the open ball of radius $r$ in $\BB_\rho\,$,
centered at the origin.
Given $r>0$ such that $B(2r)$ is contained in the domain of $\MM$,
we can use \clm(SScBound),
together with \clm(LBound) (case $\lambda=0$)
and \clm(NN1Bound) (case $\psi=0$),
to determine positive constants $K_1$ and $K_2$,
such that
$$
\bigl\|\wt\RR(H_1,Mh)\bigr\|_{\rho^\ast}\le K_n\,,\qquad
h\in B(nr)\,,\quad
n=1,2\,,
\equation(KKDef)
$$
where $\wt\RR$ is the nonlinear part of $\RR_1\,$,
defined by equation \equ(RRtDef).
Similarly for the last term in the representation \equ(MMDecomp),
which involves the difference
$$
\RR-\RR_1=\bigl(\NN-\NN_1)\circ\LL\circ\SS\,.
\equation(RRDiff)
$$
By using \clm(LBound) (case $\lambda=0$)
and the bound \equ(NNDiffBound) on $\NN-\NN_1\,$,
we can determine constants $K'_1$ and $K'_2$,
such that
$$
\bigl\|\bigl(\RR-\RR_1\bigr)(H_1+Mh)\bigr\|_{\rho^\ast}
\le K'_n\,,\qquad
h\in B(nr)\,,\quad
n=1,2\,.
\equation(KKpDef)
$$
\claim Theorem(MMFix)
There exists an odd real Fourier-Taylor polynomial $\psi_0\,$,
an even real resonant Fourier-Taylor polynomial $h_1\,$,
an invertible bounded linear operator $M$ on $\BB_\rho\,$,
a set of parameters as described after \equ(SSLLNN),
and a positive real number $r$,
such that $B(2r)$ is contained in the domain of $\MM$.
Let $H_1=H_0+h_1$ and
$$
\eps=\|\RR_1(H_1)-H_1\|_{\rho^\ast}\,,\qquad
K=\bigl\|\Id-\bigl(\Id-D\RR_1(H_1)\bigr)M\bigr\|_\rho\,.
\equation(epsK)
$$
Then there are positive constants
$K_1$, $K_2$, $K'_1$, and $K'_2$, satisfying
$$
\eps+Kr+K_1+K'_10$,
and that $\RR$ is compact.
As mentioned earlier, \clm(MMFix) implies the existence
of a unique fixed point for $\MM$ in the closure of $B(r)$.
In fact, since the first inequality in \equ(KKpBound) is strict,
this fixed point $h$ lies in $B(r)$.
The corresponding Hamiltonian $H=H_1+Mh$
is clearly a fixed point of $\RR$.
It satisfies $c_\ssH>1$ by \clm(MMFix),
and given that $M$ is invertible,
$\RR$ has no other fixed point in $B$.
This concludes the proof of \clm(RRFix).
\qed
\section Outline of the proof of \clm(MMFix)
The proof of \clm(MMFix) is based on a discretization
of the problem,
made possible by the compactness property of $\RR$,
and by the fact that only strict inequalities need to be proved.
We will describe here an algorithm that can be (and has been)
used to implement this discretization,
and to give rigorous estimates on the discretization errors.
This description only covers the main ideas and choices;
for details, the reader is referred to the source code
of our computer program [\rKiii].
In order to simplify notation,
we will from now on ignore the component $\omega\cdot p$
of the action variable $p$.
This does not represent a restriction,
since a function $f$ in $\FF_\rho$
only depend on the component $z=\Omega\cdot p$.
Similarly, if $f$ does not depend on the variable $q$ or $z$,
we will write $f(z)$ or $f(q)$, respectively,
in place of $f(q,z)$.
\subsection Standard sets
Estimates on a real number usually take the form
of upper and lower bounds, i.e., intervals.
In order to mechanize the process,
we will limit such estimates to intervals $[c-r,c+r]$
whose center $c$ and radius $r\ge 0$ belong to a finite set
of real numbers that are ``representable'' on a computer,
in a standard IEEE floating point format (described later).
The collection of all these intervals,
also referred to as ``standard sets'' for $\real$,
will be denoted by $\std(\real)$.
Objects in other spaces will be estimated similarly,
by locating them in standard sets for those spaces.
We start by defining the standard sets for $\BB_\rho\,$.
This involves the the choice of four positive integers $d'\le d$ and $\ell\dminus_\nu$
in \equ(Taylor2) are set to zero.
Two other operators that enter the definition of $\NN_1$ and $\NN$
are $\DD_y$ and $\DD_z\,$.
If applied to a Fourier-Taylor polynomial ($\psi_0$),
they can be bounded component-wise, which is trivial.
In all other cases, the argument of $\DD_y$ or $\DD_z$
is a non-resonant function,
and we can use \clm(DDBounds) to estimate the non-polynomial parts
in the representations \equ(Taylor1) and \equ(Taylor2).
For a bound on $(h_1,f_1)\mapsto\NN_1(H_0+h_1,f_1)-H_0-h_1\,$,
which involves solving the linear equation \equ(Psi1),
we apply the same strategy as for other inverses:
Starting with the centers of the given standard sets
(for $h_1$ a set of polynomials),
we first compute a numerical approximation $\psi$
for the function $\psi_1$ defined in \equ(Psi1),
then use the bounds discussed above to estimate $\Iplus\DD(h_1)\psi$,
and then add to the result a ball determined by \clm(NN1Bound).
Finally, consider the map
$(h_1,f_1)\mapsto\NN(H_0+h_1+f_1)-\NN_1(H_0+h_1,f_1)$.
Our bound on this map is restricted to polynomial standard sets
\equ(stdBB1) for $h_1\,$, and to balls centered at zero for $f_1\,$.
As a first step, we determine (strict) upper bounds
$C_1$, $B_1$, and $A_1$ (using \clm(Basic).d),
on the norms $\|f_1\|_{\rho''}$, $\|h_1\|_{\rho''}$,
and $\|\DD(h_1)\|_{\rho''}$, respectively.
After that, it suffices to estimate the triples
$(A_n,B_n,C_n)$, defined by equation \equ(CBABounds),
for $n=2,3,\ldots,m$,
and to verify that they satisfy the conditions
of \clm(CBABounds) and \clm(IterN).
Then the desired bound is given by equation \equ(NNDiffBound).
In our implementation of this bound,
we use $m=5$ and try out $6$ different choices
(of relative distances)
for each of the domain parameters $\rho^{(2)},\ldots,\rho^{(5)}$,
in order to optimize the final estimate.
For the interpolation parameter $s$ in \equ(CBABounds), we use
$$
s=\bigl[2K_n(0)(1-A_n)A_n^{-k}d^{-2}C_n\bigr]^{1/3}\,,
\equation(sChoice)
$$
which is roughly the value that minimizes $\Delta A_n\,$.
\subsection The contraction $\MM$
The only basic ingredients of $\MM$ that we have not yet discussed
are the normalization map $\SS$, and the linear operator $M$.
The map $\SS$, its derivative, and the second order Taylor remainder $\wt S$,
are straightforward to bound, using equation \equ(DSS) and \clm(SScBound).
This leaves us with the operator $M$, which appears in three of the terms
in the decomposition \equ(MMDecomp) of $\MM$.
Our approximate inverse $M$ of $\Id-D\RR(H_1)$
is of the form $\Id-W$, for an operator $W$
whose matrix elements $W_{j,i}$
(with respect to the canonical basis for $\BB_\rho$)
are non-zero only if $j$ and $i$ belong to
both $\iplus$ and $V_\ell\times\{0,1,\ldots,d-1\}$.
Although $W$ is just a finite matrix,
there is no good general bound on such an operator,
within the collection of standard sets \equ(stdBB).
This is the reason why we apply $M$ before any other step
(in the definition of $\MM$),
when we still have maximal control of its input.
We also use the maps $\SS$ and $\TT_{\mu_\ssO}$ as early as possible,
for the following reasons.
Any error in the $(0,2)$ coefficient of a function
propagates to almost all other coefficients under the action of $\SS$.
And the composition with $\TT_{\mu_\ssO}$ contracts
resonant terms $\cos(\nu\cdot Q)Z^k$ with large $\nu$ or $k$,
so that if we loose track of some of these terms,
we also loose contraction.
Ideally, a bound on a contraction like $\MM$
needs to be defined only on balls.
In our case, this can be done for the last two terms
in the decomposition \equ(MMDecomp),
since they involve no significant cancellations.
In fact, a partial bound on $M$ suffices for these terms,
in the form of a bound on the map
$h\mapsto(\|Mh\|_\rho,(Mh)_{0,2})$.
This requires only an estimate of the partial norms
$$
\|\JJJ M\|_\rho\
=\sup_{i\in I}\sum_{j\in J}|M_{j,i}|w_j/w_{i}\,,\qquad
w_{(\nu,k)}=\cosh(\rho_1\Omega\cdot\nu)\rho_2^k\,,
\equation(MNorms)
$$
for $J=I$, and for $J=\{(0,2)\}$.
For simplicity, we integrate these estimates
directly into a bound on the combined map
$h\mapsto\SS(H_0+Mh)-H_0$ and its derivative.
Bounds on the maps represented by the last two terms in \equ(MMDecomp),
are now obtained by composing bounds that have already been discussed,
using the representations \equ(RRtDef) and \equ(RRDiff).
Similarly for the first term in equation \equ(MMDecomp).
What we still need is an estimate on the norm of
$$
M'=\Id-\bigl(\Id-D\RR_1(H_1)\bigr)M=W+D\RR_1(H_1)M\,,
\equation(MprimeDef)
$$
as a linear operator on $\BB_\rho\,$.
First, we note that if this norm is less than $1$,
then $M$ is invertible, as claimed in \clm(MMFix).
This can be seen as follows.
Let $J$ be a finite subset of $I$ such that $\JJJ W\JJJ=W$.
If the norm of $M'$ is less than $1$,
then the kernel of $M$ has to be trivial.
This implies that $\JJJ M\JJJ$ is invertible on $\JJJ\BB_\rho\,$.
Thus, $M$ is invertible on $\BB_\rho\,$.
The operator norm of $M'$ is given by the equation
$$
\|M'\|_\rho=\sup_{i\in\iplus}\|M'G_i\|_\rho\,,\qquad
G_{(\nu,k)}(q,z)=w_{(\nu,k)}^{-1}\cos(\nu\cdot q)z^k\,.
\equation(MprimeNorm)
$$
In order to estimate this norm,
we first choose a finite number of standard sets $\HH_n$
whose union contains all of the basis vectors $G_i$ for $\BB_\rho\,$.
Then we apply a bound on $h\mapsto\|M'h\|_\rho$ to each of them,
and take the maximum.
Among the standard sets used are all singletons $\{G_i\}$,
with $i$ belonging to both $\iplus$ and $V_\ell\times\{0,1,\ldots,d-1\}$.
This part of our bound relies heavily on cancellations,
which are due to the fact that
$M$ is an approximate inverse of $\Id-D\RR_1(H_1)$.
In addition, we consider the standard sets
$C(V_\ell^c\times\{k\})$, $C(V_\ell^c\times\{d',d'+1,\ldots\})$,
and $C(\{\nu\}\times\{d,d+1,\ldots\})$,
for all $k\in\{0,1,\ldots d'-1\}$ and $\nu\in V_\ell\,$,
where $C=[-1,1]$.
When restricted to these sets, $M$ coincides with $D\RR_1(H_1)$.
Here, the contraction does not come from cancellations,
but from the composition with $\TT_{\mu_\ssO}\,$.
\subsection Organization of programs: Packages and data types
The bounds described in the previous four subsections
have been implemented in the programming language Ada95 [\rAda].
Most of our code is contained in a collection Ada95 ``packages'',
which encapsulate groups of related procedures and data,
and make their functionality available through a well defined interface.
The main packages and data types are organized in layers,
with each layer providing the main building blocks for the next.
At the lowest level we have a package named {\tt Reps},
defining the set of representable real numbers,
in the form of a data type {\tt Rep}.
Depending on {\tt Reps} are two children packages,
{\tt Reps.Ops} and {\tt Reps.IO},
which provide some elementary functions (not used for bounds)
and input/output procedures, respectively, for the type {\tt Rep}.
The next level contains a package named {\tt Intervals},
which defines the data type {\tt Interval},
and a few simple operations that do not involve rounding.
This data type represents real intervals,
as well as ``generalized intervals'' \equ(Interval).
An {\tt Interval} has two components of type {\tt Rep},
specifying a center and a radius.
However, this information is ``private'' to the package {\tt Intervals}
and its children {\tt Intervals.Ops} and {\tt Intervals.IO}.
These three packages provide the basic bounds (and input/output)
on the level of intervals and balls, and specifications on how to use them,
but no information about how data is represented.
The same strategy is followed at higher levels.
We note that our bound on the sum of two (generalized) intervals
is implemented as a binary operator ``{\tt +}'',
with left and right argument of type {\tt Interval}.
Similarly for other elementary arithmetic operations.
For purely numerical computations
(recall that several of our bounds require approximate solutions),
we use three packages named
{\tt Numerics}, {\tt Numerics.Ops} and {\tt Numerics.IO}.
Their public part is the same as that of {\tt Intervals} and its children,
except that the private type {\tt Interval} is replaced
by a public type {\tt Numeric}, derived from {\tt Rep}.
This allows e.g. other packages to work with a ``generic type''
{\tt Scalar}, which can be instantiated later to either {\tt Interval}
(for rigorous bounds) or {\tt Numeric} (for numerical computations).
In fact, all of our higher level packages are generic in this sense.
The third level packages {\tt Taylors}, {\tt Taylors.Ops} and {\tt Taylors.IO},
implement bounds involving the standard sets $\PP(\CC)=\PP(\CC,\VV)$,
represented by a private type {\tt Taylor}.
They take as argument (package parameter) a data type named {\tt Scalar},
to be used for the components {\tt P.C(K)} and {\tt P.E}
of a record {\tt P} of type {\tt Taylor},
which represent the coefficients $C_k$ and $E$
of the standard set $\PP(\CC)$.
Unless specified otherwise, we will assume now
that {\tt Scalar} is chosen to be {\tt Interval}.
For efficiency, some of our bounds return standard sets
that have $C_k=\{0\}$ for all $k$ larger than a specified cutoff {\tt D},
and this ``cutoff'' is stored in a designated component {\tt P.D}
of the result {\tt P}.
We also allow the special value {\tt P.D=-1},
but only if {\tt P} is identically zero.
It should be noted that the type {\tt Taylor}
does not carry any information about domains.
This information has to be provided by the user,
as arguments to the bounds (procedures or functions) that depend on domains.
We also note that standard set $\PP(\CC,V)$
can be associated with pairs $(\PP(\CC),V)$.
Similarly, the balls $C(J)$ can be associated with pairs $(C,J)$.
At the levels discussed so far, we only keep track of,
and estimate, the first component of these pairs.
Level four consists of the packages {\tt Fouriers},
{\tt Fouriers.Ops}, and {\tt Fouriers.IO}.
The package parameters include the length {\tt Lmax}
and width {\tt Wmax} of a rectangle in frequency space.
For the purpose of the work discussed here,
this rectangle is always the square $V_\ell\,$.
The remaining parameters correspond to those used in {\tt Taylors}.
The bounds at this level are still mostly general purpose,
involving the standard sets for $\BB_\rho$ and $\AA_\rho\,$,
represented by a (private) data type {\tt Fourier}.
A variable {\tt F} of type {\tt Fourier} has several components,
including two arrays {\tt F.C} and {\tt F.E},
whose elements represent the coefficients $\PP(\CC_\nu,\{0\})$
and $\PP(\CC_n,V_n^c)$, respectively, in the equation \equ(stdBB),
as well as a parity component {\tt F.J},
whose value ($0$ or $1$) indicates whether {\tt F} is even or odd.
The domain parameter $\rho$ is stored in a component {\tt F.R}.
Finally, a Boolean component {\tt F.P} specifies whether or not {\tt F}
represents a set \equ(stdBB1) of Fourier-Taylor polynomials,
as opposed to a general standard set \equ(stdBB).
Since this representation is ``private'', the packages at this level
also provide facilities for accessing this information.
A few types and functions,
that are independent of the choice of {\tt Scalar},
are defined in separate package called {\tt Fouriers\_Init}.
We note that {\tt Fouriers.Ops} includes two procedures
(versions of {\tt Comp3} and {\tt CompOmegaTmu0})
that process simultaneously an entire array of standard sets.
These procedures implement bounds on the composition operator
``$\circ_z$'', and on the combination of ``$\circ_y$''
with the map $h\mapsto h\circ\TT_{\mu_\ssO}\,$.
The bound on ``$\circ_y$'' is extremely computation intensive,
but most of the estimates are independent of the input data.
Thus, we carry out several bounds in parallel, whenever possible.
This is used e.g. for the standard sets $\HH_n$
mentioned after equation \equ(MprimeNorm).
In addition, some purely numeric procedures
(generating error messages, if used with type {\tt Interval}),
that are more renormalization group specific,
have been included in {\tt Fouriers.Ops}, for reasons of efficiency.
In order to facilitate the use of numeric procedures
inside an otherwise generic package,
we added a generic child {\tt Numerics.Ops.Fou}
to the package {\tt Numerics.Ops}, which uses
a {\tt Numeric} instantiation of the packages {\tt Fouriers} and {\tt Fouriers.Ops},
and makes some of their entities available under different names.
In particular, the {\tt Numeric} version of the type {\tt Fourier}
is renamed to {\tt Polynom}.
The next level consists of a single generic package called {\tt RG\_Ops}.
It takes the same package parameters as {\tt Fouriers},
and two additional parameters {\tt Sigma} and {\tt Kappa},
which specify the values of $\sigma$ and $\kappa$
defining the projections $\Iplusminus$.
For ``historical'' reasons, the generic version of {\tt Fourier}
is renamed to {\tt Hamilton}.
The bounds given in {\tt RG\_Ops} are mostly the ones
described in Subsections 6.4 and 6.5.
But we also include bounds on inverses, described in Subsection 6.3,
which are based on approximate solutions.
These approximate solutions are computed by using
the {\tt Polynom} procedures from {\tt Numerics.Ops.Fou}.
There are four auxiliary packages
that have not yet been mentioned:
{\tt Lin}, {\tt Lin.Ops}, {\tt Lin.IO}, and {\tt Messages}.
The first three of them define a data type {\tt Sparse},
which is used to represent the matrix $W$,
and they implement some trivial procedures for handling such matrices.
The package {\tt Messages} is used by various program parts
to display messages or prompt for input.
\subsection Main programs
In order to prove \clm(MMFix),
we need to estimate the constants $K_1,K_2,K_1',K_2',\eps,K$,
and then verify that the inequalities \equ(KKpBound) hold.
We have split this task into several main programs (procedures),
some of which can be run independently from others,
e.g. on different machines, in order to reduce computation time.
Since all the necessary bounds have been implemented
in the abovementioned packages,
the main programs do little else than defining parameters,
reading data, calling procedures from {\tt RG\_Ops},
and displaying results or writing intermediate results to disk
(in hexadecimal ASCII format).
The input to these programs are the two Fourier-Taylor polynomials
$h_1$ and $\psi_0\,$, and the matrix $W$.
The function $\psi_0$ defines the canonical transformation
$U_{\phi_0}\,$, via the solution $g$ of equation \equ(KKFix1).
Since the function $g$ is needed repeatedly,
our first step is to determine a standard set containing $g$,
and to save it for all other programs to use.
This is done in the program {\tt Run\_UpsiAux}.
We also save standard sets containing
$\partial_y\psi_0, \partial_z\psi_0\,$, and $\DD_z\psi_0\,$,
for reasons that are explained below.
The next four programs can be run independently of each other.
{\tt Run\_RG1} estimates the norm $\|\RR_1(H_1)-H_1\|_{\rho^\ast}\,$.
Two other programs, {\tt Run\_TildeR} and {\tt Run\_RminusR1},
are used to obtain the upper bounds $K_n$ and $K_n'\,$,
respectively, in the inequalities \equ(KKDef) and \equ(KKpDef).
These bounds are needed for $n=1$ and $n=2$.
{\tt Run\_TildeR} prompts for the value of $n$,
and has to be run separately (possibly in parallel) for each value,
while {\tt Run\_RminusR1} automatically covers both cases.
All of the programs mentioned so far,
as well as the program {\tt RGAux} described below,
use the ``degrees'' $\ell=40$ and $d=16$.
Much of our strategy of proof has been motivated by the fact
that bounding the derivative of our RG transformation
in the ``traditional'' way (for computer-assisted proofs)
would be computationally prohibitive with current technology.
This includes the use of the approximate RG transformation $\RR_1$
(which is much easier to differentiate than $\RR$),
and measures for achieving the desired accuracy
with the relatively low degrees $\ell=40$ and $d=16$.
(This influenced many choices,
including the order of the maps in the definition of $\RR$).
Still, it was necessary to lower the degrees even further,
in the programs that estimate the operator norm of $M'$,
despite the parallelization of our bounds for compositions.
Thus, we need to convert (enlarge) the standard sets \equ(stdBB1)
for $\psi_0$ and other polynomials,
to standards sets \equ(stdBB) with a lower value of $\ell$ and $d$,
before they can be used by these programs.
However, a set of polynomials is no longer recognized as such
after the conversion, and even if this information were preserved,
it would not help to get accurate bounds on derivatives or coefficients.
In order to minimize such effects,
we carry out some of these bounds beforehand, at $\ell=40$ and $d=16$,
and convert the results afterwards.
To be more precise, we save the results
(as mentioned in the description of {\tt Run\_UpsiAux})
and convert them later with a program called {\tt LowerQDegs}.
Such an estimate is carried out by running the program {\tt RGAux},
which determines (and then saves) a standard set
containing the image of the function $f(q,z)=z^2$,
under the derivative of $R=\LL\circ\SS$ at $H_1\,$.
The result is used later to estimate functions $DR(H_1)MG_i\,$,
as part of our bound on the norm \equ(MprimeNorm) of the operator $M'$.
More specifically, we decompose $MG_i$ into a sum $f_i+c_if$,
such that the $(0,2)$ coefficient of $f_i$ is zero.
Given a standard set containing $DR(H_1)f$,
it now suffices to estimate $DR(H_1)f_i\,$.
This can be done accurately at low degrees,
since $D\LL(H_1)$ acts trivially on $f_i\,$.
Our estimate on the norm of $M'$ is organized in the two
programs {\tt MM1Norm\_W} and {\tt MM1Norm\_noW}.
Among the standard sets $\HH_n$ described after equation \equ(MprimeNorm),
{\tt MM1Norm\_W} considers those with frequencies $\nu$ outside $V_\ell\,$,
as well as all singletons $\{G_i\}$
for which at least one matrix element $W_{j,i}$ is non-zero.
This makes a total of $759$ standard sets.
Whenever possible, {\tt MM1Norm\_W} processes $20$ of them in parallel.
In addition, {\tt MM1Norm\_W} prompts for, and can be restricted to,
a subrange of standard sets to be processed,
so that the task can be distributed among several machines.
The program {\tt MM1Norm\_noW} covers those standard sets $\HH_n$
that are not considered by {\tt MM1Norm\_W}.
The parameters used in the proof of \clm(MMFix) are
$\sigma\approx 0.85001$, $\kappa\approx\sigma/0.4$,
$\rho\approx(0.85,0.15)$,
$\rho^\ast=({\tt Up}(\rho_1),{\tt Up}(\rho_2))$,
$\rho''\approx(0.9,0.165)$, and $r\approx 3*10^{-12}$,
where ${\tt Up}(\rho_i)$ is the successor of $\rho_i$
in the set of representable numbers.
The precise value of $r$, in standard base $16$ notation,
is 3.4C6CC8389BE334C8*10$^{{\rm -A}}$.
The precise value of the other parameters can be found
in Section.7 [\rKiii].
We developed our programs with the public version
3.13p of the GNAT compiler [\rGNAT].
As our type {\tt Rep} of ``representable numbers'',
we chose GNAT's floating point type {\tt Long\_Long\_Float}.
On the architecture used (Intel Pentium class PC),
this type maps directly to the 80-bit ``extended real'' format [\rPentium]
used by the floating point unit (FPU),
which implements the IEEE ``double extended'' precision format,
and complies with the
IEEE Standard for Binary Floating-Point Arithmetic [\rIEEE].
In particular, it is possible to specify that
the four elementary operations never return a number
that is less than the true result.
As described in Subsection 6.2, this suffices for our purpose.
Thus, we put the FPU in ``round up'' mode,
for the duration of all of our programs:
When the package {\tt Intervals.Ops} is elaborated,
a procedure {\tt Round\_Up}
sets the binary FPU control word to {\tt 0000101101100000}.
This one (assembly) instruction is machine dependent,
and needs to be changed before running our programs on different hardware.
It also un-masks all exceptions, besides rounding,
and thus excludes de-normalized numbers (and infinite values)
from $\std(\real)$.
There are certainly other good choices for $\std(\real)$.
It should be noted that the quality of our bounds
is not determined on the level of representable numbers or intervals.
What is far more important (besides the general strategy of proof)
is the control of the discretization errors
that arise from estimating objects in infinite dimensions
by a finite number of inequalities.
Our programs were compiled (at optimization level {\tt O3})
and run on various PC's, using the GNU/Linux operating system.
The estimated running time for a single 1GHz Pentium class PC
is around 4 months.
All programs terminated without signaling any errors, implying e.g.
that the ball $B(2r)$ is contained in the domain of $\MM$.
The resulting upper bounds on the norms
in \equ(KKDef), \equ(KKpDef), and \equ(epsK) are
$K_1<7.0*10^{-18}$,
$K_2<2.8*10^{-17}$,
$K'_1<4.2*10^{-14}$,
$K'_2<1.7*10^{-13}$,
$\eps<9.0*10^{-15}$, $K<0.84$,
and it is straightforward to check
that these constants satisfy the inequalities \equ(KKpBound).
Furthermore, we find that $c_\ssH=1.024332969\ldots$
for every Hamiltonian $H$ in $H_0+MB(r)$.
This completes the proof of \clm(MMFix).
\bigskip\noindent{\bf Acknowledgments}\hfill\break
The author would like to thank P.~Wittwer and M.~Zou
for many helpful discussions and suggestions,
and the Department of Theoretical Physics at the
University of Geneva for its hospitality,
while part of this work was carried out.
\references
\font\ninerm=cmr9
\font\nineit=cmti9
\font\ninebf=cmbx9
\font\ninett=cmtt9
\def\rm{\ninerm}
\def\it{\nineit}
\def\bf{\ninebf}
\def\tt{\ninett}
\baselineskip=11pt
\rm
\item{[\rED]} D.F.~Escande and F.~Doveil,
{\it Renormalisation Method for Computing the
Thr\-eshold of the Large Scale
Stochastic Instability in Two Degree of Freedom Hamiltonian Systems,}
J.~Stat. Phys.~{\bf 26} (1981), 257--284.
\item{[\rKad]} L.P.~Kadanoff,
{\it Scaling for a Critical Kolmogorov--Arnold--Moser Trajectory,}
Phys.~Rev.~Lett. {\bf 47} (1981), 1641--1643.
\item{[\rSKad]} S.J.~Shenker and L.P.~Kadanoff,
{\it Critical Behavior of a KAM Surface. I. Empirical Results,}
J.~Stat.~Phys. {\bf 27} (1982), 631--656.
\item{[\rMcKi]} R.S.~MacKay,
{\it Renormalisation in Area Preserving Maps,}
Thesis, Prin\-ce\-ton (1982).
World Scientific, London (1993).
\item{[\rMcKii]} R.S.~MacKay, {\it
Renormalisation Approach to Invariant Circles in Area--Preserving Maps,}
Physica D {\bf 7} (1983), 283--300.
\item{[\rMEsc]} A.~Mehr and D.F.~Escande,
{\it Destruction of KAM Tori in Hamiltonian Systems:
Link with the Destabilization of Nearby Cycles
and Calculation of Residues,}
Physica D {\bf 13} (1984), 302--338.
\item{[\rKSi]} K.~Khanin, Ya.G.~Sinai, {\it
The Renormalization Group Method and KAM Theory.}
In ``Nonlinear Phenomena in Plasma Physics and Hydrodynamics'',
R.Z.~Sagdeev (ed), Mir (1986), 93--118.
\item{[\rGJSS]} J.M.~Greene, H.~Johannesson, B.~Schaub and H.~Suhl,
{\it Scaling Anomaly at the Critical Transition
of an Incommensurate Structure,}
Phys.~Rev.~A {\bf 36} (1987), 5858--5861.
\item{[\rWi]} J.~Wilbrink,
{\it New Fixed Point of the Renormalization Operator for Invariant Circles,}
Phys. Lett. A {\bf 131} (1988), 251--255.
\item{[\rKSii]} K.~Khanin, Ya.G.~Sinai, {\it
Renormalization Group Methods in the Theory of Dynamical Systems.}
Int.~J.~Mod.~Phys.~B {\bf 2} (1988), 147--165.
\item{[\rKMcK]} J.A.~Ketoja and R.S.~MacKay,
{\it Fractal Boundary for the Existence of Invariant Circles
for Area--Preserving Maps:
Observations and Renormalisation Explanation,}
Physica D {\bf 35} (1989), 318--334.
\item{[\rMaoH]} J.~M. Mao and R.~H.~G. Helleman, {\it
Existence of KAM Tori for Four--Dimensional
Volume Preserving Maps.}
Nuovo Cimento B {\bf 104} (1989), 177--182.
\item{[\rGMao]} J.M.~Greene and J.~Mao,
{\it Higher--Order Fixed Points of the Renormalization Operator
for Invariant Circles,}
Nonlinearity {\bf 3} (1990), 69--78.
\item{[\rWii]} J.~Wilbrink,
{\it New Fixed Point of the Renormalisation Operator
Associated with the Recurrence of Invariant Circles
in Generic Hamiltonian Maps,}
Nonlinearity {\bf 3} (1990), 567--584.
\item{[\rACS]} R.~Artuso, G.~Casati, D.L.~Shepelyansky, {\it
Breakdown of Universality in Renormalization Dynamics
for Critical Invariant Torus.}
Europhys.~Lett. {\bf 15} (1991), 381--386.
\item{[\rMMS]} R.S.~MacKay, J.D.~Meiss, and J.~Stark,
{\it An Approximate Renormalization for the Break-up
of Invariant Tori with Three Frequencies,}
Phys.~Lett.~A {\bf 190} (1994), 417--424.
\item{[\rMcKiii]} R.S.~MacKay, {\it
Three Topics in Hamiltonian Dynamics.}
Preprint U. Warwick (1994).\hfil\break
Also in: ``Dynamical Systems and Chaos'', Vol.2,
Y.~Aizawa, S.~Saito, K.~Shiraiwa (eds),
World Scientific, London (1995).
\item{[\rCGM]} J.~del~Castillo-Negrete, J.~M.~Greene, P.~Morrison,
{\it Area Preserving Non--Twist Maps:
Periodic Orbits and Transition to Chaos.}
Physica D {\bf 91} (1996), 1--23.
\item{[\rSti]} A.~Stirnemann,
{\it Towards an Existence Proof of MacKay's Fixed Point,}
Comm.~Math.~Phys. {\bf 188} (1997), 723--735.
\item{[\rCGJii]} M.~Govin, C.~Chandre, H.R.~Jauslin, {\it
KAM--Renormalization Group Approach to the Breakup
of Invariant Tori in Hamiltonian Systems.}
Phys.~Rev.~E {\bf 57}, 1536--1543 (1998).
\item{[\rCGJK]} C.~Chandre, M.~Govin, H.R.~Jauslin, and H.~Koch,
{\it Universality for the Breakup of Invariant Tori in Hamiltonian Flows,}
Phys.~Rev.~E {\bf 57} (1998), 6612--6617.
\item{[\rAKW]} J.J.~Abad, H.~Koch, and P.~Wittwer,
{\it A Renormalization Group for Hamiltonians: Numerical Results,}
Nonlinearity {\bf 11} (1998), 1185--1194.
\item{[\rKi]} H.~Koch,
{\it A Renormalization Group for Hamiltonians,
with Applications to KAM Tori,}
Erg.~Theor.~Dyn.~Syst. {\bf 19} (1999), 1--47.
\item{[\rCJBC]} C.~Chandre, H.~R.~Jauslin, G.~Benfatto, A.~Celletti,
{\it An Approximate Renormalization--Group Transformation for Hamiltonian
Systems with Three Degrees of Freedom,}
Phys.~Rev.~E {\bf 60} (1999), 5412--5421
\item{[\rCMcK]} C.~Chandre and R.S.~MacKay,
{\it Approximate Renormalization with Co\-dimension--One Fixed Point
for The Break-up of some Three--Frequency Tori,}
Phys. Lett.~A {\bf 275} (2000), 394--400.
\item{[\rAK]} J.J.~Abad and H.~Koch,
{\it Renormalization and Periodic Orbits for Hamiltonian Flows,}
Commun.~Math.~Phys. {\bf 212} (2000), 371--394.
\item{[\rJLDi]} J.~Lopes Dias, {\it
Renormalisation of Flows on the Multidimensional Torus
Close to a KT Frequency Vector,}
Nonlinearity {\bf 15} (2002), 647--664.
\item{[\rJLDii]} J.~Lopes Dias, {\it
Renormalisation Scheme for Vector Fields on T$\,^2$
with a Diophantine Frequency,}
Nonlinearity {\bf 15} (2002), 665--679.
\item{[\rCJ]} C.~Chandre and H.R.~Jauslin,
{\it Renormalization--Group Analysis for the Transition to Chaos
in Hamiltonian Systems,}
to appear in Phys.~Rep. (2002)
\item{[\rCC]} C.~Chandre,
{\it Renormalization for Cubic Frequency Invariant Tori
in Hamiltonian Systems with Two Degrees of Freedom,}
to appear in Discrete Contin.~Dynam.~Systems B (2002).
\item{[\rKii]} H.~Koch,
{\it On the Renormalization of Hamiltonian Flows,
and Critical Invariant Tori,}
preprint {\tt mp\_arc 01-191}, to appear in
Discrete Contin.~Dynam.~Systems A (2002).
\item{[\rKiii]} The preprint {\tt mp\_arc 02-175} of this paper
includes the source code for the programs used in our proof of \clm(MMFix).
See also {\tt ftp://ftp.ma.utexas.edu/pub/papers/koch/kam-fixpt/}.
\item{[\rKSW]} H.~Koch, A.~Schenkel and P.~Wittwer,
{\it Computer--Assisted Proofs in Analysis and Programming in Logic:
A Case Study,}
SIAM Rev. {\bf 38} (1996), 565--604.
\item{[\rAda]} S.T.~Taft and R.A.~Duff (eds),
{\it Ada 95 Reference Manual: Language and Standard Libraries,
International Standard ISO/IEC 8652:1995(E)},
Lecture Notes in Computer Science {\bf 1246} (1997).
See also {\tt http://www.adahome.com/rm95/}.
\item{[\rGNAT]} Ada Core Technologies, 73 Fifth Avenue, New York, NY 10003, USA.
\hfil\break
See also {\tt ftp://cs.nyu.edu/pub/gnat}.
\item{[\rPentium]} Intel Corp.,
{\it Intel Architecture Software Developer's Manual,
Volume 1: Basic Architecture,}
{\tt http://developer.intel.com/design/pentiumii/manuals/243190.htm}.
\item{[\rIEEE]} The Institute of Electrical and Electronics Engineers, Inc.,
{\it IEEE Standard for Binary Float\-ing--Point Arithmetic,}
ANSI/IEEE Std 754--1985.
\bye
~~