Content-Type: multipart/mixed; boundary="-------------0904231235233" This is a multi-part message in MIME format. ---------------0904231235233 Content-Type: text/plain; name="09-67.comments" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="09-67.comments" AMS-Code: 37E40 E-mail: gianni.arioli@polimi.it, koch@math.utexas.edu For possible updates and a formatted program listing, see ftp://ftp.ma.utexas.edu/pub/papers/koch/maps-fixpt/ ---------------0904231235233 Content-Type: text/plain; name="09-67.keywords" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="09-67.keywords" area preserving maps, commuting pairs, quasi periodic, golden mean, invariant circle, breakup, critical, universal, renormalization group, MacKay, fixed point, generating function, computer assisted ---------------0904231235233 Content-Type: application/x-tex; name="MapsRG1.tex" Content-Transfer-Encoding: 7bit Content-Disposition: inline; filename="MapsRG1.tex" %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% including smallfonts.tex %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %smallfonts.tex % \newskip\ttglue % \font\fiverm=cmr5 \font\fivei=cmmi5 \font\fivesy=cmsy5 \font\fivebf=cmbx5 \font\sixrm=cmr6 \font\sixi=cmmi6 \font\sixsy=cmsy6 \font\sixbf=cmbx6 \font\sevenrm=cmr7 \font\eightrm=cmr8 \font\eighti=cmmi8 \font\eightsy=cmsy8 \font\eightit=cmti8 \font\eightsl=cmsl8 \font\eighttt=cmtt8 \font\eightbf=cmbx8 \font\ninerm=cmr9 \font\ninei=cmmi9 \font\ninesy=cmsy9 \font\nineit=cmti9 \font\ninesl=cmsl9 \font\ninett=cmtt9 \font\ninebf=cmbx9 % \font\twelverm=cmr12 \font\twelvei=cmmi12 \font\twelvesy=cmsy12 \font\twelveit=cmti12 \font\twelvesl=cmsl12 \font\twelvett=cmtt12 \font\twelvebf=cmbx12 %% EIGHT POINT FONT FAMILY \def\eightpoint{\def\rm{\fam0\eightrm} \textfont0=\eightrm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm \textfont1=\eighti \scriptfont1=\sixi \scriptscriptfont1=\fivei \textfont2=\eightsy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex \textfont\itfam=\eightit \def\it{\fam\itfam\eightit} \textfont\slfam=\eightsl \def\sl{\fam\slfam\eightsl} \textfont\ttfam=\eighttt \def\tt{\fam\ttfam\eighttt} \textfont\bffam=\eightbf \scriptfont\bffam=\sixbf \scriptscriptfont\bffam=\fivebf \def\bf{\fam\bffam\eightbf} \tt \ttglue=.5em plus.25em minus.15em \normalbaselineskip=9pt \setbox\strutbox=\hbox{\vrule height7pt depth2pt width0pt} \let\sc=\sixrm \let\big=\eightbig \normalbaselines\rm} \def\eightbig#1{{\hbox{$\textfont0=\ninerm\textfont2=\ninesy \left#1\vbox to6.5pt{}\right.$}}} %% NINE POINT FONT FAMILY \def\ninepoint{\def\rm{\fam0\ninerm} \textfont0=\ninerm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm \textfont1=\ninei \scriptfont1=\sixi \scriptscriptfont1=\fivei \textfont2=\ninesy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex \textfont\itfam=\nineit \def\it{\fam\itfam\nineit} \textfont\slfam=\ninesl \def\sl{\fam\slfam\ninesl} \textfont\ttfam=\ninett \def\tt{\fam\ttfam\ninett} \textfont\bffam=\ninebf \scriptfont\bffam=\sixbf \scriptscriptfont\bffam=\fivebf \def\bf{\fam\bffam\ninebf} \tt \ttglue=.5em plus.25em minus.15em \normalbaselineskip=11pt \setbox\strutbox=\hbox{\vrule height8pt depth3pt width0pt} \let\sc=\sevenrm \let\big=\ninebig \normalbaselines\rm} \def\ninebig#1{{\hbox{$\textfont0=\tenrm\textfont2=\tensy \left#1\vbox to7.25pt{}\right.$}}} %% TWELVE POINT FONT FAMILY --- not really small \def\twelvepoint{\def\rm{\fam0\twelverm} \textfont0=\twelverm \scriptfont0=\eightrm \scriptscriptfont0=\sixrm \textfont1=\twelvei \scriptfont1=\eighti \scriptscriptfont1=\sixi \textfont2=\twelvesy \scriptfont2=\eightsy \scriptscriptfont2=\sixsy \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex \textfont\itfam=\twelveit \def\it{\fam\itfam\twelveit} \textfont\slfam=\twelvesl \def\sl{\fam\slfam\twelvesl} \textfont\ttfam=\twelvett \def\tt{\fam\ttfam\twelvett} \textfont\bffam=\twelvebf \scriptfont\bffam=\eightbf \scriptscriptfont\bffam=\sixbf \def\bf{\fam\bffam\twelvebf} \tt \ttglue=.5em plus.25em minus.15em \normalbaselineskip=11pt \setbox\strutbox=\hbox{\vrule height8pt depth3pt width0pt} \let\sc=\sevenrm \let\big=\twelvebig \normalbaselines\rm} \def\twelvebig#1{{\hbox{$\textfont0=\tenrm\textfont2=\tensy \left#1\vbox to7.25pt{}\right.$}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% end of smallfonts.tex %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% including param.2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %param.2 \magnification=\magstep1 \def\firstpage{1} \pageno=\firstpage %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% end of param.2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% including fonts.5b %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %fonts.5b \font\fiverm=cmr5 \font\sevenrm=cmr7 \font\sevenbf=cmbx7 \font\eightrm=cmr8 \font\eightbf=cmbx8 \font\ninerm=cmr9 \font\ninebf=cmbx9 \font\tenbf=cmbx10 \font\magtenbf=cmbx10 scaled\magstep1 \font\magtensy=cmsy10 scaled\magstep1 \font\magtenib=cmmib10 scaled\magstep1 \font\magmagtenbf=cmbx10 scaled\magstep2 % \font\eightmsb=msbm8 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% end of fonts.5b %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% including symbols.1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % symbols.1 % % just concatenated amssym.def version 2.2 and amssym.tex version 2.2b % and commented out stuff: lines now beginning with %# % % use with fonts.5b instead of fonts.5 % %%% ==================================================================== %%% @TeX-file{ %%% filename = "amssym.def", %%% version = "2.2", %%% date = "22-Dec-1994", %%% time = "10:14:01 EST", %%% checksum = "28096 117 438 4924", %%% author = "American Mathematical Society", %%% copyright = "Copyright (C) 1994 American Mathematical Society, %%% all rights reserved. Copying of this file is %%% authorized only if either: %%% (1) you make absolutely no changes to your copy, %%% including name; OR %%% (2) if you do make changes, you first rename it %%% to some other name.", %%% address = "American Mathematical Society, %%% Technical Support, %%% Electronic Products and Services, %%% P. O. Box 6248, %%% Providence, RI 02940, %%% USA", %%% telephone = "401-455-4080 or (in the USA and Canada) %%% 800-321-4AMS (321-4267)", %%% FAX = "401-331-3842", %%% email = "tech-support@math.ams.org (Internet)", %%% codetable = "ISO/ASCII", %%% keywords = "amsfonts, msam, msbm, math symbols", %%% supported = "yes", %%% abstract = "This is part of the AMSFonts distribution, %%% It is the plain TeX source file for the %%% AMSFonts user's guide.", %%% docstring = "The checksum field above contains a CRC-16 %%% checksum as the first value, followed by the %%% equivalent of the standard UNIX wc (word %%% count) utility output of lines, words, and %%% characters. This is produced by Robert %%% Solovay's checksum utility.", %%% } %%% ==================================================================== %#\expandafter\ifx\csname amssym.def\endcsname\relax \else\endinput\fi % % Store the catcode of the @ in the csname so that it can be restored later. %#\expandafter\edef\csname amssym.def\endcsname{% %# \catcode`\noexpand\@=\the\catcode`\@\space} % Set the catcode to 11 for use in private control sequence names. \catcode`\@=11 % % Include all definitions related to the fonts msam, msbm and eufm, so that % when this file is used by itself, the results with respect to those fonts % are equivalent to what they would have been using AMS-TeX. % Most symbols in fonts msam and msbm are defined using \newsymbol; % however, a few symbols that replace composites defined in plain must be % defined with \mathchardef. \def\undefine#1{\let#1\undefined} \def\newsymbol#1#2#3#4#5{\let\next@\relax \ifnum#2=\@ne\let\next@\msafam@\else \ifnum#2=\tw@\let\next@\msbfam@\fi\fi \mathchardef#1="#3\next@#4#5} \def\mathhexbox@#1#2#3{\relax \ifmmode\mathpalette{}{\m@th\mathchar"#1#2#3}% \else\leavevmode\hbox{$\m@th\mathchar"#1#2#3$}\fi} \def\hexnumber@#1{\ifcase#1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or 8\or 9\or A\or B\or C\or D\or E\or F\fi} \font\tenmsa=msam10 \font\sevenmsa=msam7 \font\fivemsa=msam5 \newfam\msafam \textfont\msafam=\tenmsa \scriptfont\msafam=\sevenmsa \scriptscriptfont\msafam=\fivemsa \edef\msafam@{\hexnumber@\msafam} \mathchardef\dabar@"0\msafam@39 \def\dashrightarrow{\mathrel{\dabar@\dabar@\mathchar"0\msafam@4B}} \def\dashleftarrow{\mathrel{\mathchar"0\msafam@4C\dabar@\dabar@}} \let\dasharrow\dashrightarrow \def\ulcorner{\delimiter"4\msafam@70\msafam@70 } \def\urcorner{\delimiter"5\msafam@71\msafam@71 } \def\llcorner{\delimiter"4\msafam@78\msafam@78 } \def\lrcorner{\delimiter"5\msafam@79\msafam@79 } % Note that there should not be a final space after the digits for a % \mathhexbox@. \def\yen{{\mathhexbox@\msafam@55}} \def\checkmark{{\mathhexbox@\msafam@58}} \def\circledR{{\mathhexbox@\msafam@72}} \def\maltese{{\mathhexbox@\msafam@7A}} \font\tenmsb=msbm10 \font\sevenmsb=msbm7 \font\fivemsb=msbm5 \newfam\msbfam \textfont\msbfam=\tenmsb \scriptfont\msbfam=\sevenmsb \scriptscriptfont\msbfam=\fivemsb \edef\msbfam@{\hexnumber@\msbfam} \def\Bbb#1{{\fam\msbfam\relax#1}} \def\widehat#1{\setbox\z@\hbox{$\m@th#1$}% \ifdim\wd\z@>\tw@ em\mathaccent"0\msbfam@5B{#1}% \else\mathaccent"0362{#1}\fi} \def\widetilde#1{\setbox\z@\hbox{$\m@th#1$}% \ifdim\wd\z@>\tw@ em\mathaccent"0\msbfam@5D{#1}% \else\mathaccent"0365{#1}\fi} \font\teneufm=eufm10 \font\seveneufm=eufm7 \font\fiveeufm=eufm5 \newfam\eufmfam \textfont\eufmfam=\teneufm \scriptfont\eufmfam=\seveneufm \scriptscriptfont\eufmfam=\fiveeufm \def\frak#1{{\fam\eufmfam\relax#1}} \let\goth\frak % Restore the catcode value for @ that was previously saved. %#\csname amssym.def\endcsname %#\endinput %%% ==================================================================== %%% @TeX-file{ %%% filename = "amssym.tex", %%% version = "2.2b", %%% date = "26 February 1997", %%% time = "13:14:29 EST", %%% checksum = "61515 286 903 9155", %%% author = "American Mathematical Society", %%% copyright = "Copyright (C) 1997 American Mathematical Society, %%% all rights reserved. Copying of this file is %%% authorized only if either: %%% (1) you make absolutely no changes to your copy, %%% including name; OR %%% (2) if you do make changes, you first rename it %%% to some other name.", %%% address = "American Mathematical Society, %%% Technical Support, %%% Electronic Products and Services, %%% P. O. Box 6248, %%% Providence, RI 02940, %%% USA", %%% telephone = "401-455-4080 or (in the USA and Canada) %%% 800-321-4AMS (321-4267)", %%% FAX = "401-331-3842", %%% email = "tech-support@ams.org (Internet)", %%% codetable = "ISO/ASCII", %%% keywords = "amsfonts, msam, msbm, math symbols", %%% supported = "yes", %%% abstract = "This is part of the AMSFonts distribution. %%% It contains the plain TeX source file for loading %%% the AMS extra symbols and Euler fraktur fonts.", %%% docstring = "The checksum field above contains a CRC-16 checksum %%% as the first value, followed by the equivalent of %%% the standard UNIX wc (word count) utility output %%% of lines, words, and characters. This is produced %%% by Robert Solovay's checksum utility.", %%% } %%% ==================================================================== %% Save the current value of the @-sign catcode so that it can %% be restored afterwards. This allows us to call amssym.tex %% either within an AMS-TeX document style file or by itself, in %% addition to providing a means of testing whether the file has %% been previously loaded. We want to avoid inputting this file %% twice because when AMSTeX is being used \newsymbol will give an %% error message if used to define a control sequence name that is %% already defined. %% %% If the csname is not equal to \relax, we assume this file has %% already been loaded and \endinput immediately. %#\expandafter\ifx\csname pre amssym.tex at\endcsname\relax \else\endinput\fi %% Otherwise we store the catcode of the @ in the csname. %#\expandafter\chardef\csname pre amssym.tex at\endcsname=\the\catcode`\@ %% Set the catcode to 11 for use in private control sequence names. \catcode`\@=11 %% Load amssym.def if necessary: If \newsymbol is undefined, do nothing %% and the following \input statement will be executed; otherwise %% change \input to a temporary no-op. %#\ifx\undefined\newsymbol \else \begingroup\def\input#1 {\endgroup}\fi %#\input amssym.def \relax %% Most symbols in fonts msam and msbm are defined using \newsymbol. A few %% that are delimiters or otherwise require special treatment have already %% been defined as soon as the fonts were loaded. Finally, a few symbols %% that replace composites defined in plain must be undefined first. \newsymbol\boxdot 1200 \newsymbol\boxplus 1201 \newsymbol\boxtimes 1202 \newsymbol\square 1003 \newsymbol\blacksquare 1004 \newsymbol\centerdot 1205 \newsymbol\lozenge 1006 \newsymbol\blacklozenge 1007 \newsymbol\circlearrowright 1308 \newsymbol\circlearrowleft 1309 \undefine\rightleftharpoons \newsymbol\rightleftharpoons 130A \newsymbol\leftrightharpoons 130B \newsymbol\boxminus 120C \newsymbol\Vdash 130D \newsymbol\Vvdash 130E \newsymbol\vDash 130F \newsymbol\twoheadrightarrow 1310 \newsymbol\twoheadleftarrow 1311 \newsymbol\leftleftarrows 1312 \newsymbol\rightrightarrows 1313 \newsymbol\upuparrows 1314 \newsymbol\downdownarrows 1315 \newsymbol\upharpoonright 1316 \let\restriction\upharpoonright \newsymbol\downharpoonright 1317 \newsymbol\upharpoonleft 1318 \newsymbol\downharpoonleft 1319 \newsymbol\rightarrowtail 131A \newsymbol\leftarrowtail 131B \newsymbol\leftrightarrows 131C \newsymbol\rightleftarrows 131D \newsymbol\Lsh 131E \newsymbol\Rsh 131F \newsymbol\rightsquigarrow 1320 \newsymbol\leftrightsquigarrow 1321 \newsymbol\looparrowleft 1322 \newsymbol\looparrowright 1323 \newsymbol\circeq 1324 \newsymbol\succsim 1325 \newsymbol\gtrsim 1326 \newsymbol\gtrapprox 1327 \newsymbol\multimap 1328 \newsymbol\therefore 1329 \newsymbol\because 132A \newsymbol\doteqdot 132B \let\Doteq\doteqdot \newsymbol\triangleq 132C \newsymbol\precsim 132D \newsymbol\lesssim 132E \newsymbol\lessapprox 132F \newsymbol\eqslantless 1330 \newsymbol\eqslantgtr 1331 \newsymbol\curlyeqprec 1332 \newsymbol\curlyeqsucc 1333 \newsymbol\preccurlyeq 1334 \newsymbol\leqq 1335 \newsymbol\leqslant 1336 \newsymbol\lessgtr 1337 \newsymbol\backprime 1038 \newsymbol\risingdotseq 133A \newsymbol\fallingdotseq 133B \newsymbol\succcurlyeq 133C \newsymbol\geqq 133D \newsymbol\geqslant 133E \newsymbol\gtrless 133F \newsymbol\sqsubset 1340 \newsymbol\sqsupset 1341 \newsymbol\vartriangleright 1342 \newsymbol\vartriangleleft 1343 \newsymbol\trianglerighteq 1344 \newsymbol\trianglelefteq 1345 \newsymbol\bigstar 1046 \newsymbol\between 1347 \newsymbol\blacktriangledown 1048 \newsymbol\blacktriangleright 1349 \newsymbol\blacktriangleleft 134A \newsymbol\vartriangle 134D \newsymbol\blacktriangle 104E \newsymbol\triangledown 104F \newsymbol\eqcirc 1350 \newsymbol\lesseqgtr 1351 \newsymbol\gtreqless 1352 \newsymbol\lesseqqgtr 1353 \newsymbol\gtreqqless 1354 \newsymbol\Rrightarrow 1356 \newsymbol\Lleftarrow 1357 \newsymbol\veebar 1259 \newsymbol\barwedge 125A \newsymbol\doublebarwedge 125B \undefine\angle \newsymbol\angle 105C \newsymbol\measuredangle 105D \newsymbol\sphericalangle 105E \newsymbol\varpropto 135F \newsymbol\smallsmile 1360 \newsymbol\smallfrown 1361 \newsymbol\Subset 1362 \newsymbol\Supset 1363 \newsymbol\Cup 1264 \let\doublecup\Cup \newsymbol\Cap 1265 \let\doublecap\Cap \newsymbol\curlywedge 1266 \newsymbol\curlyvee 1267 \newsymbol\leftthreetimes 1268 \newsymbol\rightthreetimes 1269 \newsymbol\subseteqq 136A \newsymbol\supseteqq 136B \newsymbol\bumpeq 136C \newsymbol\Bumpeq 136D \newsymbol\lll 136E \let\llless\lll \newsymbol\ggg 136F \let\gggtr\ggg \newsymbol\circledS 1073 \newsymbol\pitchfork 1374 \newsymbol\dotplus 1275 \newsymbol\backsim 1376 \newsymbol\backsimeq 1377 \newsymbol\complement 107B \newsymbol\intercal 127C \newsymbol\circledcirc 127D \newsymbol\circledast 127E \newsymbol\circleddash 127F \newsymbol\lvertneqq 2300 \newsymbol\gvertneqq 2301 \newsymbol\nleq 2302 \newsymbol\ngeq 2303 \newsymbol\nless 2304 \newsymbol\ngtr 2305 \newsymbol\nprec 2306 \newsymbol\nsucc 2307 \newsymbol\lneqq 2308 \newsymbol\gneqq 2309 \newsymbol\nleqslant 230A \newsymbol\ngeqslant 230B \newsymbol\lneq 230C \newsymbol\gneq 230D \newsymbol\npreceq 230E \newsymbol\nsucceq 230F \newsymbol\precnsim 2310 \newsymbol\succnsim 2311 \newsymbol\lnsim 2312 \newsymbol\gnsim 2313 \newsymbol\nleqq 2314 \newsymbol\ngeqq 2315 \newsymbol\precneqq 2316 \newsymbol\succneqq 2317 \newsymbol\precnapprox 2318 \newsymbol\succnapprox 2319 \newsymbol\lnapprox 231A \newsymbol\gnapprox 231B \newsymbol\nsim 231C \newsymbol\ncong 231D \newsymbol\diagup 201E \newsymbol\diagdown 201F \newsymbol\varsubsetneq 2320 \newsymbol\varsupsetneq 2321 \newsymbol\nsubseteqq 2322 \newsymbol\nsupseteqq 2323 \newsymbol\subsetneqq 2324 \newsymbol\supsetneqq 2325 \newsymbol\varsubsetneqq 2326 \newsymbol\varsupsetneqq 2327 \newsymbol\subsetneq 2328 \newsymbol\supsetneq 2329 \newsymbol\nsubseteq 232A \newsymbol\nsupseteq 232B \newsymbol\nparallel 232C \newsymbol\nmid 232D \newsymbol\nshortmid 232E \newsymbol\nshortparallel 232F \newsymbol\nvdash 2330 \newsymbol\nVdash 2331 \newsymbol\nvDash 2332 \newsymbol\nVDash 2333 \newsymbol\ntrianglerighteq 2334 \newsymbol\ntrianglelefteq 2335 \newsymbol\ntriangleleft 2336 \newsymbol\ntriangleright 2337 \newsymbol\nleftarrow 2338 \newsymbol\nrightarrow 2339 \newsymbol\nLeftarrow 233A \newsymbol\nRightarrow 233B \newsymbol\nLeftrightarrow 233C \newsymbol\nleftrightarrow 233D \newsymbol\divideontimes 223E \newsymbol\varnothing 203F \newsymbol\nexists 2040 \newsymbol\Finv 2060 \newsymbol\Game 2061 \newsymbol\mho 2066 \newsymbol\eth 2067 \newsymbol\eqsim 2368 \newsymbol\beth 2069 \newsymbol\gimel 206A \newsymbol\daleth 206B \newsymbol\lessdot 236C \newsymbol\gtrdot 236D \newsymbol\ltimes 226E \newsymbol\rtimes 226F \newsymbol\shortmid 2370 \newsymbol\shortparallel 2371 \newsymbol\smallsetminus 2272 \newsymbol\thicksim 2373 \newsymbol\thickapprox 2374 \newsymbol\approxeq 2375 \newsymbol\succapprox 2376 \newsymbol\precapprox 2377 \newsymbol\curvearrowleft 2378 \newsymbol\curvearrowright 2379 \newsymbol\digamma 207A \newsymbol\varkappa 207B \newsymbol\Bbbk 207C \newsymbol\hslash 207D \undefine\hbar \newsymbol\hbar 207E \newsymbol\backepsilon 237F % Restore the catcode value for @ that was previously saved. %#\catcode`\@=\csname pre amssym.tex at\endcsname %\endinput %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% end of symbols.1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% including titles.6c %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %titles.6c % requires fonts.5 or higher and smallfonts.tex \count5=0 \count6=1 \count7=1 \count8=1 \count9=1 \def\proof{\medskip\noindent{\bf Proof.\ }} \def\qed{\hfill{\sevenbf QED}\par\medskip} \def\references{\bigskip\noindent\hbox{\bf References}\medskip} \def\remark{\medskip\noindent{\bf Remark.\ }} \def\nextremark #1\par{\item{$\circ$} #1} \def\firstremark #1\par{\bigskip\noindent{\bf Remarks.} \smallskip\nextremark #1\par} \def\abstract#1\par{{\baselineskip=10pt \eightpoint\narrower\noindent{\eightbf 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.1\vsize\penalty-40 \vskip0pt plus -.1\vsize\bigskip\bigskip \global\advance\count5 by 1 \message{#1}\leftline {\magtenbf \number\count5.\ #1} \count6=1 \count7=1 \count8=1 \nobreak\smallskip\noindent} \def\subsection#1\par{\vskip0pt plus.05\vsize\penalty-20 \vskip0pt plus -.05\vsize\medskip\medskip \message{#1}\leftline{\tenbf \number\count5.\number\count8.\ #1} \global\advance\count8 by 1 \nobreak\smallskip\noindent} \def\addref#1{\expandafter\xdef\csname r#1\endcsname{\number\count9} \global\advance\count9 by 1} \def\proofof(#1){\medskip\noindent{\bf Proof of \csname c#1\endcsname.\ }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% end of titles.6c %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% including macros.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %macros.18 % requires fonts.5 or later \def\rightheadline{\hfil} \def\leftheadline{\sevenrm\hfil HANS KOCH\hfil} \headline={\ifnum\pageno=\firstpage\hfil\else \ifodd\pageno{{\fiverm\rightheadline}\number\pageno} \else{\number\pageno\fiverm\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 % \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\tr{{\rm tr}} \def\modulo{{\rm mod~}} \def\std{{\rm std}} \def\Re{{\rm Re\hskip 0.15em}} \def\Im{{\rm Im\hskip 0.15em}} \def\defeq{\mathrel{\mathop=^{\rm def}}} % \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}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% end of macros.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % mapsrg1.tex % %\input smallfonts.tex %\input param.2 %\input fonts.5b %\input symbols.1 %\input titles.6c %\input macros.18 % \font\tenib=cmmib10 \def\bme{{\hbox{\tenib e}}} \def\bmx{{\hbox{\tenib x}}} \def\bmy{{\hbox{\tenib y}}} \def\bms{{\hbox{\tenib s}}} \def\bmt{{\hbox{\tenib t}}} \def\bmu{{\hbox{\tenib u}}} \def\bmv{{\hbox{\tenib v}}} % \def\bue{{\hbox{\teneufm e}}} \def\bux{{\hbox{\teneufm x}}} \def\buy{{\hbox{\teneufm y}}} \def\bus{{\hbox{\teneufm s}}} \def\but{{\hbox{\teneufm t}}} \def\buu{{\hbox{\teneufm u}}} \def\buv{{\hbox{\teneufm v}}} % \font\bigeufm=eufm9 scaled\magstep1 \def\buF{{\hbox{\bigeufm F}}} \def\buN{{\hbox{\bigeufm N}}} \def\buR{{\hbox{\bigeufm R}}} \def\buS{{\hbox{\bigeufm S}}} % \def\reflect{{\Bbb S}} \def\BbbL{{\Bbb L}} \def\AUV{\AA^\diamond} \def\AXY{\AA} % \def\thalf{{\textstyle{1\over 2}}} \def\tlamhalf{{\textstyle{\lambda\over 2}}} \def\vec#1#2{\left(\matrix{#1\cr#2}\right)} \def\vek#1#2#3{\left(\matrix{#1\cr#2\cr#3}\right)} % \def\loongrightarrow{\relbar\joinrel\longrightarrow} \def\looongrightarrow{\relbar\joinrel\loongrightarrow} \def\loongmapsto{\mapstochar\loongrightarrow} \def\looongmapsto{\mapstochar\looongrightarrow} % \def\xlongmapsto{\mathop{\longmapsto}\limits} \def\xloongmapsto{\mathop{\loongmapsto}\limits} \def\xlooongmapsto{\mathop{\looongmapsto}\limits} % \def\ssf{{\sss f}} \def\ssg{{\sss g}} \def\ssh{{\sss h}} \def\ssE{{\sss E}} \def\ssF{{\sss F}} \def\ssG{{\sss G}} \def\ssP{{\sss P}} \def\ssR{{\sss R}} \def\ssT{{\sss T}} \def\ssZ{{\sss Z}} \def\ssFG{{\sss FG}} \def\ssGF{{\sss GF}} \def\ssPP{{\sss\PP}} % \def\Rminus{R_{_{-}}} \def\Rplus{R_{_{+}}} \def\Rplusminus{R_{_\pm}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \addref{KadanoffEION} \addref{MacKayEITW} \addref{FeigenbaumKadanoffShenkerEITW} \addref{MacKayEITH} % \addref{StirnemannNITH} \addref{StirnemannNISE} % \addref{EscandeDoveilEION} \addref{MehrEscandeEIFO} % \addref{ChandreJauslinZETW} \addref{KochZEEI} % \addref{KochZETW} \addref{KochZEFO} \addref{KochZENI} \addref{ArioliKochZENI} % \addref{IEEE} \addref{Ada} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\leftheadline{\sevenrm\hfil GIANNI ARIOLI and HANS KOCH\hfil} \def\rightheadline{\sevenrm\hfil Critical fixed point for area-preserving maps\hfil} %% \cl{{\magtenbf The critical renormalization fixed point}} \cl{{\magtenbf for commuting pairs of area-preserving maps}} \bigskip \cl{Gianni Arioli \footnote{$^1$} {{\sevenrm Dipartimento di Matematica, Politecnico di Milano, Piazza Leonardo da Vinci 32, 20133 Milano.}} and Hans Koch \footnote{$^2$} {{\sevenrm Department of Mathematics, University of Texas at Austin, Austin, TX 78712}} } \bigskip \abstract We prove the existence of the critical fixed point $(F,G)$ for MacKay's renormalization operator for pairs of maps of the plane. The maps $F$ and $G$ commute, are area-preserving, reversible, real analytic, and they satisfy a twist condition. \section Introduction %%%%%%%%%%%%%%%%%%%%%%%% We consider the fixed point problem for the following operator $\buR$, acting on pairs of area-preserving maps $\PP=(F,G)$ of the plane: $$ \buR(\PP)=(\wt F,\wt G)\,,\qquad \wt F=\Lambda^{-1}G\Lambda\,,\qquad \wt G=\Lambda^{-1}FG\Lambda\,. \equation(RRFG) $$ Here, $\Lambda$ is a linear scaling $(x,z)\mapsto(\lambda x,\mu z)$, depending on $\PP$, with $\lambda$ and $\mu$ defined by the condition $\wt G(0,0)=(-1,-1)$. Our main result is the following. \claim Theorem(MapFix) The transformation $\buR$ has a fixed point $(F,G)$, with associated scalings $$ \lambda=-0.7067956691\ldots\,,\qquad \mu=-0.3260633966\ldots\,. \equation(LaMuBound) $$ The maps $F$ and $G$ are area-preserving, real analytic, and nonlinear. In addition, they satisfy the following, on non-empty open subsets of their domains. $G$ is reversible with respect to the involution $S(x,z)=(-x,z)$, in the sense that $SGS=G^{-1}$. The same holds for $F$. Furthermore, $F$ and $G$ commute. Our proof of this theorem is computer-assisted. \medskip\noindent This fixed point problem has a rather long history [\rKadanoffEION--\rStirnemannNISE]. The fixed point described in \clm(MapFix), is known as the ``critical'' fixed point of $\buR$. Its existence was conjectured in [\rMacKayEITW], based on a numerical investigations; and some rigorous partial results were obtained in [\rStirnemannNISE]. A related fixed point problem for Hamiltonians was solved recently in [\rKochZEFO,\rKochZENI]. The motivation behind these studies is to describe the breakup of golden invariant circles in one-parameter families of maps, such as the standard family $$ (x,z)\mapsto (x+w,w)\,,\qquad w=z-\beta\sin(2\pi x)\,. \equation(StdMap) $$ For $\beta=0$, the map \equ(StdMap) has a smooth invariant circles, including one (at $z=\vartheta$) whose rotation number is the inverse of the golden mean $\vartheta=\half\sqrt{5}+\half$. By KAM theory, the same holds for small $\beta>0$. The golden circle is observed to persist as $\beta$ is increased, up to some value $\beta_\infty$, where it starts to break up. The transition is characterized by several numerical quantities that are universal, in the sense that the exact same values are observed in a large class of one-parameter families of cylinder maps $\beta\mapsto G_\beta\,$. In particular, the critical map in the family (the map $G_\beta$ for $\beta=\beta_\infty$) has a non-smooth golden invariant circle. This circle, and the entire orbit structure nearby, is invariant under a scaling $\Lambda={\rm diag}(\lambda,\mu)$, with $\lambda$ and $\mu$ being the values \equ(LaMuBound). The maps \equ(StdMap) commute with integer translations $\FF_n(x,z)=(x+n,z)$, so they define maps on the cylinder $\torus\times\real$. In a more general situation, the cylinder can be $\real^2/\FF$, where $\FF$ is a $\integer$-action on $\real^2$, generated by some diffeomorphism $\FF_1\,$. A map on this cylinder can be described by a map $G:\real^2\to\real^2$ that commutes with $\FF_1\,$. If we think of $\FF_1$ as a full rotation of the cylinder, then the equation for a periodic point $(x,z)$ of $G$, with rotation number ${p\over q}$, is $G^q(x,z)=\FF_p(x,z)$. We refer to such a point as being ${p\over q}$-periodic for the pair $(F,G)$, where $F$ is the inverse of $\FF_1\,$. Then a ${p\over q}$-periodic point for $(F,G)$ is just a fixed point for $F^pG^q$. At the same time it is a ${q-p\over p}$-periodic point for $(G,FG)$, since $F^pG^q=G^{q-p}(FG)^p$. Now consider the continued fraction approximants $r_1={1\over 2}$, $r_2={2\over 3}$, $r_3={3\over 5}$, $r_4={5\over 8}$, $\ldots$ for the inverse golden mean $\vartheta^{-1}$, and let $n>1$. Then a $r_n$-periodic point for $(F,G)$ is a $r_{n-1}$-periodic point for $(G,FG)$. Furthermore, taking $n\to\infty$ yields an analogous statement about quasiperiodic points with rotation number $\vartheta^{-1}$. Coming back to the scaling properties of critical cylinder maps, one observation is the following: After a suitable change of coordinates, a sequence of $r_n$-periodic points $(x_n,z_n)$ accumulates at the origin (lying on the golden circle), with asymptotic ratios $x_{n+1}/x_n\to\lambda$ and $z_{n+1}/z_n\to\mu$. This motivates a rescaling of the map $(F,G)\mapsto(G,FG)$, as in \equ(RRFG), and it suggests that, under iteration of $\buR$, a critical area-preserving cylinder map converges to the critical fixed point. In this ``renormalization picture'', the value $\beta_\infty$ marks the point where a family $\beta\mapsto\PP_\beta$ crosses the (codimension $1$) stable manifold of the fixed point. Another universal quantity that can be observed in such families is a value $\delta\approx 1.62795$. It describes the geometric accumulation, at $\beta_\infty\,$, of bifurcation points $\beta_n$ involving $r_n$-periodic orbits. This number $\delta$ is expected to be the expanding eigenvalue of the derivative $D\buR$ at the fixed point. Estimates on $\delta$ require a study of this derivative, which we have not done here; but it could be the subject for future work. Notice that $\buR$ preserves the commuting property of pairs. However, the constraint $FG=GF$ is highly impractical to work with. Thus, we drop it for the time being. Another problem is reversibility: it is not preserved by $\buR$. What does preserve reversibility are ``palindromic'' compositions like $GFG$. Thus, we start by considering the transformation $$ \buN(G)=\Lambda^{-1}FG_1\Lambda\,,\qquad G_1=\Lambda^{-1}FG\Lambda\,,\qquad F=\Lambda^{-1}G\Lambda\,. \equation(NNG) $$ Here, $\lambda$ and $\mu$ are defined by the equation $G(-\lambda,-\mu)=(-\lambda^2,-\mu^2)$. This guarantees that the normalization condition $G(0,0)=(-1,-1)$ is satisfied again by $\buN(G)$, as well as by $G_1\,$. Clearly, if $G$ is a fixed point for $\buN$, satisfying $G_1=G$, then the corresponding pair $(F,G)$ is a fixed point of $\buR$. Interestingly, the property $G_1=G$ holds almost automatically: Let $G$ be a reversible fixed point of $\buN$. Then, using that $\Lambda^{-1}G=F\Lambda^{-1}$, we find that $J=G_1^{-1}G$ satisfies $$ J=(\Lambda^{-1}G^{-1}F^{-1}\Lambda)(\Lambda^{-2}GFG\Lambda^2) =\Lambda^{-1}G^{-1}\Lambda^{-1}FG\Lambda^2 =\Lambda^{-1}J^{-1}\Lambda\,. \equation(JProp) $$ In addition, $J$ leaves the origin invariant. Assuming $J$ is analytic near the origin, a simple power series argument, using that $|\mu|$ is not an integer power of $|\lambda|$, shows that the conjugacy \equ(JProp) implies $J=\pm\id$. By proving that $J$ is analytic and different from $-\id$, we can conclude that $G_1=G$. Hence the pair $(F,G)$ is a fixed point of $\buR$. In addition, the identity $G_1=G$ implies that $G_1$ is reversible, which in turn implies that $F$ and $G$ commute. The complete argument is a bit more involved, since the domains of these maps need to be considered. Another constraint is that the map $G$ has to preserve area. We deal with this in the usual way, by representing $G$ in terms of a generating function $g$, $$ G(x,z)=(y,w)\,,\qquad z=-g_1(x,y)\,,\quad w=g_2(x,y)\,, \equation(Gfromg) $$ where $g_j=\partial_j g$. In other words, the fixed point problem $\buN(G)=G$ is translated into a fixed point problem $\NN(g)=g$. After solving the latter, and verifying that $g_{1,2}>1$ on the relevant domain, we obtain the desired fixed point of $\buN$ by solving equation \equ(Gfromg). The twist property $g_{1,2}>0$ guarantees that the solution is unique. Furthermore, since the one-form $wdy-zdx$ is the differential of $g$, and thus closed, the resulting map $G$ is area-preserving. For simplicity, we reconstruct $G$ and define $F$ on domains that are (each) a union of two overlapping rectangles, satisfying $$ \Lambda\ov{D_\ssG}\subset D_\ssG\,,\qquad \Lambda\ov{D_\ssF}\subset D_\ssG\,,\qquad G\Lambda\ov{D_\ssG}\subset D_\ssF\,. \equation(extension) $$ Except for the closures, these are the minimal conditions for $\buR(\PP)$ to be defined on the domain of $\PP$, regardless of the order in which $F$ and $G$ are composed. In [\rStirnemannNITH], a fixed point of $\buR$ that satisfies \equ(extension) is said to have the {\it extension property}. When combined with additional properties, it is possible to prove a number of interesting facts about cylinder maps that are attracted to such a fixed point under iteration of $\buR$. This includes the existence of a golden invariant circle. For further details we refer to [\rStirnemannNITH]. We did not attempt to verify any of these additional properties, but our computer programs should be well suited for such (and other) investigations. A related fixed point problem was considered in [\rStirnemannNISE], namely $F=\Lambda^{-3}GFG\Lambda^3$ and $G=\Lambda^{-3}GFGFG\Lambda^3$. This is a palindromic modification of the equation $\buR^3(\PP)=\PP$. It was proved in [\rStirnemannNISE] that the corresponding fixed point equation for a reduced generating function (corresponding our $g_1$) has a solution; and the bounds obtained for $\lambda$ and $\mu$ are compatible with \equ(LaMuBound). What was left open is the question of whether the corresponding maps $F$ and $G$ commute (which would yield a fixed point or period $3$ for $\buR$, assuming that $F$ and $G$ have proper domains), and whether they are area-preserving. As indicated earlier, there are analogues of the transformation \equ(RRFG), that act on Hamiltonians. An overview of the work in this area, which goes back to [\rEscandeDoveilEION, \rMehrEscandeEIFO], can be found in [\rChandreJauslinZETW, \rKochZEEI]. One such transformation, that preserves analyticity, was proved to have a critical fixed point [\rKochZEFO], with a non-smooth invariant torus [\rKochZENI]. Naturally, the scaling constants for Hamiltonians agree with \equ(RRFG). As one would expect, there is a connection between $\buR$ and its Hamiltonian analogue. However, this connection [\rKochZETW] is purely formal, and a direct analysis of $\buR$ seemed more promising (and interesting) than trying to make this connection rigorous. One problem with $\buR$ has always been the need to work with commuting pairs; but our argument following \equ(JProp) shows that this issue is less serious than it seems. It should be possible to extend our methods to obtain results on the derivative of $\buR$ at the critical fixed point. An analogous analysis for Hamiltonians seems currently out of reach, due to the complexity of the transformation involved. Our results on the transformation $\NN$ for generating functions, and on a related contraction $\MM$, can be found in Sections 4 and 5, respectively. The relevant function spaces, and some basic estimates, are given in Section 3. In Section 6, we discuss an implicit equation that arises in the definition of $\NN$. A description of our computer-assisted proof can be found in Section 7. We start by defining the transformation $\NN$. \section Generating functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The transformation $\NN$ for generating functions is formally $\NN=\Psi^{-1}\buN\Psi$, where $\Psi$ is the map that assigns an area-preserving map $G$ to a generating function $g$, via equation \equ(Gfromg). Our aim here is to give an explicit but formal description of $\NN$, and of its derivative. We start with some simple facts about generating functions and use the opportunity to introduce some notation. As can be verified using \equ(Gfromg), the generating function $f\star g$ for a composed map $FG$ is given by $$ (f\star g)(x,y) =g(x,\VV)+f(\VV,y)\,, \equation(fog) $$ with the ``midpoint'' $\VV=\VV(x,y)$ determined by the equation $$ {d\over d\VV}\bigl[g(x,\VV)+f(\VV,y)\bigr]=0\,. \equation(midpoint) $$ A conjugacy $F=\Lambda^{-1}G\Lambda$ by a scaling $\Lambda={\rm diag}(\lambda,\mu)$ translates into $$ f=(\lambda\mu)^{-1}g\circ\ell\,,\qquad \ell(x,y)=(\lambda x,\lambda y)\,. \equation(gscale) $$ For the generating function $g^{-1}$ of the inverse map $G^{-1}$ we get $g^{-1}(x,y)=-g(y,x)$. {}From this, one sees that the generating function $\reflect g$ for $SG^{-1}S$ is given by $$ (\reflect g)(x,y)=g(-y,-x)\,. \equation(SSg) $$ A function $g$ that is invariant under $\reflect$ will be called {\it symmetric}. Now we consider the generating function analogue of each step in the definition of $$ \buN(G)=\Lambda^{-2}GFG\Lambda^2\,,\qquad F=\Lambda^{-1}G\Lambda\,. \equation(NNGAgain) $$ We assume that $G$ is reversible and satisfies the normalization $G(0,0)=(-1,-1)$. Thus, the corresponding generating function has to be symmetric and satisfy $$ g_1(0,-1)=0\,\qquad g_2(0,-1)=-1\,. \equation(gNormalize) $$ The generating function $f$ of $F$ is given by \equ(gscale), once we have determined the scaling constants $\lambda$ and $\mu$. We would like $\lambda$ and $\mu$ to yield the sequence $$ (0,0)\xloongmapsto^{\Lambda^2} (0,0)\xlongmapsto^G (-1,-1)\xlongmapsto^F (-\lambda,-\mu)\xlongmapsto^G (-\lambda^2,-\mu^2)\xloongmapsto^{\Lambda^{-2}} (-1,-1)\,, \equation(NormalChain) $$ so that $\buN(G)$ is again properly normalized. Notice that the map $G_1=\Lambda^{-1}FG\Lambda$ then satisfies $G_1(0,0)=(-1,-1)$ as well. The first and last condition (arrow) in \equ(NormalChain) hold for any choice of $\lambda$ and $\mu$. The second is just the normalization of $G$, and the third follows from the fourth by the definition of $F$. So we determine $\lambda$ and $\mu$ by the fourth condition, or equivalently, by the equation $$ g_1(-\lambda,-\lambda^2)=\mu\,,\qquad g_2(-\lambda,-\lambda^2)=-\mu^2\,. \equation(LambdaMuCond) $$ Next, consider the composed map $\wh H=GFG$. Applying the identity \equ(fog) twice, we see that the generating function $\wh h$ of $\wh H$ is given by $$ \wh h(x,y)=g(x,\VV)+f(\VV,\WW)+g(\WW,y)\,, \equation(gfgfun) $$ with $\VV=\VV(x,y)$ and $\WW=\WW(x,y)$ making the right hand side of \equ(gfgfun) stationary: $$ g_2(x,\VV)+f_1(\VV,\WW)=0\,,\qquad f_2(\VV,\WW)+g_1(\WW,y)=0\,. \equation(GFGMid) $$ A simple calculation, using that both $f$ and $g$ are symmetric, shows that the second equality in \equ(GFGMid) follows from the first, if $\WW=-\reflect \VV$. This identity also ensures that $\wh h$ is symmetric. Thus, it suffices to solve $$ g_2(x,\VV)+f_1\bigl(\VV,-\reflect \VV)=0\,. \equation(GFGMid) $$ Once this equation is solved, and $\wh h$ is defined via \equ(gfgfun), the remaining step $\wt G=\Lambda^{-2}\wh H\Lambda^2$ translates to $$ \wt g(x,y)=(\lambda\mu)^{-2}\wh h(\lambda^2 x,\lambda^2 y)\,. \equation(gRenorm) $$ Here, we have used \equ(gscale) again. Given that $\wt G=\buN(G)$, the map $g\mapsto\wt g$ is the desired transformation $\NN$. We will also need to estimate the derivative of $\NN$, so let us now compute $\wt g'=D\NN(g)g'$. This is easier than one might think. We assume that both $g$ and $g'$ are symmetric. Using the symmetry of $g$, the equation \equ(LambdaMuCond) for $\lambda$ can be written as $K(g,\lambda)=0$, where $$ K(g,\lambda)=g_1(\lambda^2,\lambda) -g_2(\lambda^2,\lambda)^2\,. \equation(KgLambda) $$ Setting $DK(g,\lambda)(g',\lambda')=0$ and solving for $\lambda'$, we find that $$ \lambda'= -\bigl(2\lambda g_{1,1}+g_{1,2} -2g_2[2\lambda g_{2,1}+g_{2,2}]\bigr)^{-1} \bigl[g'_1-2g_2g'_2]\,, \equation(DgToLambda) $$ where all functions are being evaluated at $(\lambda^2,\lambda)$. Since $\mu=-g_2(\lambda^2,\lambda)$, the corresponding variation of $\mu$ is $$ \mu'=-g'_2-[2\lambda g_{2,1}+g_{2,2}]\lambda'\,. \equation(DLambdaToMu) $$ Then the variation of $f=(\lambda\mu)^{-1}g\circ\ell$ is given by $$ f'=(\lambda\mu)^{-1}g'\circ\ell -(\lambda'/\lambda+\mu'/\mu)f +(\lambda'/\lambda)\DD f\,, \equation(DgTof) $$ where $\DD$ denotes the generator of dilations, $(\DD f)(x,y)=xf_1(x,y)+yf_2(x,y)$. The variation $\wh h'$ of the function $\wh h$ in the composition \equ(gfgfun) is simply $$ \wh h'(x,y)=g'(x,\VV)+f'(\VV,\WW)+g'(\WW,y)\,, \equation(gfgfunVar) $$ since the right hand side of \equ(gfgfun) is stationary with respect to variations of $\VV$ and $\WW$. The last step in the definition of $\NN$ is the scaling $\wt g=(\lambda\mu)^{-2}\wh h\circ\ell^2$. Its variation is analogous to \equ(DgTof), so the function $\wt g'=D\NN(g)g'$ is given by $$ \wt g'=(\lambda\mu)^{-2}\wh h'\circ\ell^2 -2(\lambda'/\lambda+\mu'/\mu)\wt g +2(\lambda'/\lambda)\DD\wt g\,. \equation(DTTg) $$ Notice that the basic steps involved in the construction of $\NN(g)$ and $D\NN(g)g'$ are derivatives, composition of functions, and the solution of implicit equations. \section Function spaces %%%%%%%%%%%%%%%%%%%%%%%%%%% In order to control the steps described in the last section, we first need to choose appropriate domains and function spaces. Since we need good approximations for analytic functions, our preference is to use Taylor series, and domains that are disks (in each variable). The equation \equ(SSg) shows that the generating function $g$ for a reversible map $G$ is an even function of $x+y$. Thus, it is natural to change variables to $$ t=x+y\,,\qquad s=x-y\,. \equation(xytots) $$ However, using a domain of the type $|t-t_0|<\rho_t$ for the variable $t$ poses problems. Expanding about $t_0=0$ is essentially useless, even numerically. And using a disk about $t_0\not=0$ is not a workable option, since we need a reasonable subspace of even functions. Here, and in what follows, we call a function {\it even} if it is an even function of $t$. A possible way out is to write our functions as $P+tQ$, with $P$ and $Q$ even; then expand $P$ and $Q$ in powers of $u=t^2-t_0^2$ and $v=s-s_0\,$. But it turns out that the resulting domains are too borderline for a successful analysis of $\NN$. What improves the situation drastically is a choice of variables of the form $$ u=\bigl[t^2-t_0^2\bigr]+b[s-s_0]\,,\qquad v=s-s_0\,, \equation(tstouv) $$ with $b$ substantially different from $0$. Specific values for the parameters $t_0$, $s_0$, and $b$ will be given later. The corresponding function spaces are chosen as follows. Given a pair of positive real numbers $\rho=(\rho_u,\rho_v)$, denote by $D_\rho$ the set of points $(u,v)\in\complex^2$ such that $|u|<\rho_u$ and $|v|<\rho_v\,$. Define $\AUV_\rho$ to be the space of all all analytic functions $P: D_\rho\to\complex$, that extend continuously to the boundary of $D_\rho\,$, equipped with the norm $$ \|P\|_\rho=\sum_{m,n}|P_{m,n}|\rho_u^m\rho_v^n\,,\qquad P(u,v)=\sum_{m,n}P_{m,n}u^mv^n\,. \equation(AANorm) $$ Clearly, $\AUV_\rho$ is a Banach algebra, that is, $\|PQ\|_\rho\le\|P\|_\rho\|Q\|_\rho\,$. If $\AA$ is any complex Banach algebra with unit, then for $U,V\in\AA$ we define $P(U,V)=\sum_{m,n}P_{m,n}U^mV^n$, provided that the series converges in $\AA$. Before extending the above to include non-even functions, we give here the bound that is used (in our programs) to estimate the various derivatives that appear in the construction of $\NN(g)$ and $D\NN(g)g'$. Given positive real numbers $\sigma<\tau$, and a non-negative integer $k$, define $$ W_k(\sigma,\tau)=\max_{m\ge k}\,W_{k,m}(\sigma,\tau)\,,\qquad W_{k,m}(\sigma,\tau) ={m!\over (m-k)!}\left({\sigma\over\tau}\right)^m \sigma^{-k}\,. \equation(normfacs) $$ \claim Proposition(DerBound) Let $r=(r_u,r_v)$, with $00$, denote by $B_r(h)$ the closed ball in $\AXY_\varrho^e$ of radius $r$, centered at $h$. \claim Lemma(MMFix) There exists a normalized real polynomial $g_0\in\AXY_\varrho^e\,$, a bounded linear operator $M$ on $\AXY_\varrho$ as described above, as well as real numbers $r>0$ and $R\ge\|M\|_\varrho r$, such that the following holds. The transformation $\NN$ is well defined, bounded, and analytic, as a map from $B_\ssR(g_0)$ to $\AXY_\rho\,$, with $\rho_u={17\over 16}\varrho_u$ and $\rho_v={17\over 16}\varrho_v\,$. For the corresponding map $\MM$, $$ \|\MM(g_0)\|_\varrho\le\eps\,,\qquad \|D\MM(\gamma)\|_\varrho\le\kappa\,, \equation(ContrBounds) $$ with $\eps,\kappa>0$ satisfying $\eps+\kappa r0$. Assume that the following holds, for all $\nu\in\AXY_\rho$ of norm $r$ or less. The functions $A_\nu$, $B_\nu$, $R^{-1}$ belong to $\AXY_\rho$ and satisfy a bound $$ \|R^{-1}\|_\rho \bigl(\|A_0\|_\rho+\|B_0\|_\rho\bigr) \bigl(\|A_\nu-A_0\|_\rho+\|B_\nu-B_0\|_\rho\bigr)\le\kappa\,, \equation(VCompZeroTwo) $$ with $\kappa<1$. Furthermore, $$ \bigl\|D\KK(\VV)^{-1}\KK(\VV)\bigr\|_\rho\le\eps<(1-\kappa)r\,. \equation(VCompZeroOne) $$ Then the equation $\KK(\VV+\nu)=0$ has a unique solution $\nu_\ast\in\AXY_\rho$ of norm $\le r$. \proof Define $$ \CC(\nu)=\nu-D\KK(\VV)^{-1}\KK(\VV+\nu)\,. \equation(VCompZeroThree) $$ Notice that $\|\CC(0)\|_\rho\le\eps$ by the assumption \equ(VCompZeroOne). We also have $$ \eqalign{ D\CC(\nu)&=\id-D\KK(\VV)^{-1}D\KK(\VV+\nu)\cr &=-D\KK(\VV)^{-1}\bigl[D\KK(\VV+\nu)-D\KK(\VV)\bigr]\cr &=-R^{-1}\bigl[(\reflect A_0)-B_0\reflect\bigr] \bigl[(A_v-A_0)+(B_v-B_0)\reflect\bigr]\,,\cr} \equation(VCompZeroFour) $$ so the inequality \equ(VCompZeroTwo) implies that $\|D\CC(\nu)\|\le\kappa$ on the ball $\|\nu\|_\rho\le r$. The assertion now follows from the contraction mapping principle. \qed When solving the midpoint equation \equ(GFGMid), we start with a function $g$ belonging to $\AXY_\varrho^e\,$, and a function $f$ belonging to another space of this type. In order to verify the hypotheses of \clm(VCompZero), we first have to estimate the derivatives $\phi=f_1$ and $\psi=g_2\,$, as as well as the first partial derivatives of $\phi$ and $\psi$. This can be done by using \clm(DerBound). Then we can use \clm(BBalg) to estimate the functions $A_\nu$ and $B_\nu\,$. The inverse $1/R$ is estimated by using the contraction $\xi\mapsto(\XX+2\xi)[{\bf 1}-R\XX]-R\xi^2$, whose fixed point $\xi_\ast$ is the difference between the true inverse and an approximate inverse $\XX$. Combining steps and using the chain rule, we see that the function $\CC(\nu)$ in \equ(VCompZeroThree) depends analytically on the pair $(f,g)$, on any open domain where the necessary norm inequalities are satisfied. By uniform convergence, the analytic dependence carries over to the solution $\nu_\ast\,$. The last argument is based on the fact that the fixed point for the contraction $\CC$ can be obtained by iteration, yielding a sequence that converges (geometrically or better) in norm. The same arguments apply to the fixed point problem $\MM(\gamma)=\gamma$. Our constructive definition of $\MM$ yields either an empty domain (unsatisfied norm inequalities), or else an analytic map. \section Organization of the programs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% What remains to be proved is \clm(MMFix), including \equ(LaMuBound), the domain and range properties described in \clm(NNProp), and a simple bound on $DJ(0,0)$. These are all inequalities. The goal is to reduce inequalities like $\|D\MM(\gamma)\|_\varrho\le\kappa$ into several simpler ones, and to continue this reduction, until the inequalities that need to be checked are completely trivial. The computer is used not only to check these trivial inequalities, but also to generate them, using the propositions from this paper, or more basic facts, or definitions. The basic techniques used in our proof are not new. Thus, we will limit our description to the main structure, and to some novel aspects. The precise definitions, and all other details of the proof, can be found in the source code of our programs. (They are written in the programming language Ada95 [\rAda].) The programs should be organized well enough to be readable without much knowledge of programming. Since more complex structures are defined in terms of simpler ones, we will start with a description of the lowest level. One of the issues at this level is rounding. To avoid a possible misunderstanding, we would like to stress that the control of roundoff errors is a rather trivial aspect of this type of proofs. The main difficulty is to control objects in infinite dimensions, namely our spaces $\AXY_\rho\,$, with a finite amount of information. This requires keeping track of what is relevant at each step of the proof, and discarding unnecessary information. In what follows, words in {\tt this font} will denote entities (data types, procedures, packages, $\ldots$) in our programs. As mentioned earlier, implicit equations are first ``solved'' numerically, and then we prove that there exists a true solution nearby. Thus, most procedures are designed to be run either in numeric or rigorous mode, depending on whether the generic type {\tt Scalar} is instantiated with {\tt Numeric} or {\tt Ball}, respectively. Modes are switched withing the program as needed. In numeric mode, the floating point unit is instructed to round to the nearest {\tt Rep} (representable number, in our case $80$ bit [\rIEEE]), while in rigorous mode, we put the unit into round-up mode. This guarantees e.g. that {\tt R1+R2} returns an upper bound on the true sum of {\tt R1} and {\tt R2}. A lower bound can be obtained from {\tt -(-R1-R2)}. This allows for rigorous interval arithmetics. Our ``intervals'' are in fact special cases of balls $\BB(c,r,b)=(c+r\,\UU){\bf 1}+b\,{\bf U}$ in a commutative Banach algebra $\AA$ with unit ${\bf 1}$, where $c$ and $r,b\ge 0$ are representable real numbers, $\UU$ is the unit ball in $\real$ or $\complex$, and ${\bf U}$ is the unit ball in $\AA$. The corresponding data type {\tt Ball} is a record {\tt S=(S.C,S.R,S.B)} with components of type {\tt Rep}. Using controlled rounding as described above, it is easy to implement an operation {\tt S1+S2} that returns a {\tt Ball S}, with the property that $\BB({\tt S})$ contains all sums $s_1+s_2\,$, with $s_1\in \BB({\tt S1})$ and $s_2\in \BB({\tt S2})$. Such low level operations are defined in the Ada package {\tt Balls}. In what follows, we identify a data type like {\tt Ball} with the collection of all representable sets $\BB({\tt S})$ based on this type. These sets $\BB({\tt S})$ are sufficient when working with $\AA=\real$ or $\AA=\complex$. Consider now the space $\AA=\AUV_\rho\,$. In this case, $\BB({\tt S})$ represents a neighborhood of the constant function $(u,v)\mapsto{\tt S.C}$. More elaborate subsets of $\AUV_\rho$ are represented by a type {\tt Taylor2}, consisting of a pair {\tt T=(T.R,T.C)}, where {\tt T.R} is a pair of numbers of type {\tt Radius} (non-negative {\tt Rep}), representing the domain parameter $\rho$, and where {\tt T.C} is a two-dimensional {\tt array(0..PDeg,0..PDeg)} with components {\tt T.C(M,N)} of type {\tt Ball}. The pair {\tt T} represents the set $\BB({\tt T})=\sum\BB({\tt T.C(M,N)}) {\bf u}^{\sss M}{\bf v}^{\sss N}$. This sum ranges over nonnegative integers {\tt M} and {\tt N}, with {\tt M+N} not exceeding {\tt PDeg}. Clearly, we can define a {\tt Taylor2}-sum {\tt T1+T2} with with the desired property (analogous to the one described above for balls), in terms of {\tt Ball}-sums {\tt T1.C(M,N)+T2.C(M,N)}. This and other bounds on operations involving functions in $\AUV_\rho$ are defined in the package {\tt Taylors2}. For the quadratic functions $\bmu$ and $\bmv$ defined in Section 3, we use a data type {\tt Args}, given by a record {\tt A=(A.T0,A.S0,A.B,A.A)} with components of type {\tt Rep}. The first three components describe the parameters $t_0$, $s_0$, and $b$. The component {\tt A.A} is the coefficient $a$ in a more general version $a[t^2-t_0^2]+[s-s_0]$ of our function $\bmv$, but we only use $a=0$ here. Some basic operations involving such quadratic functions, and changes of variables, are defined in the packages {\tt MiniFuns} and {\tt MiniFuns.Ops}. Our standard sets in the space $\AXY_\rho$ are defined by a type {\tt Fun}, consisting of a quadruplet {\tt F=(F.A,F.E,F.P,F.Q)}, where {\tt F.P} and {\tt F.Q} are of type {\tt Taylor2}. The component {\tt F.E} is a {\tt Boolean} parameter; if {\tt True}, then the set represented by {\tt F} is $\BB({\tt F})=\BB({\tt F.P})+\bmt \BB({\tt F.Q})$, with $\BB({\tt F.P})$ and $\BB({\tt F.Q})$ as described above, except for a change of variables $u=\bmu(x,y)$ and $v=\bmv(x,y)$ defined by the {\tt Args}-type argument {\tt F.A} of {\tt F}. We refer to such a {\tt Fun} as being of ``even'' type. If {\tt F.E} is {\tt False}, then the {\tt Ball}-type components {\tt F.P.C(M,N)} and {\tt F.Q.C(M,N)} use $\AXY_\rho$ as algebra, and not just the even subspace $\AXY_\rho^e\,$. So the functions in the corresponding sets $\BB({\tt F.P})$ and $\BB({\tt F.Q})$ need not be even. This ``general'' version of {\tt Fun} appears naturally when composing with a function in $\AXY_\rho\,$. For such compositions, we use \clm(BBalg) to estimate the errors. The even type is more convenient for estimating derivatives, since we can use \clm(DerBound) directly, via the chain rule. Thus, once the midpoint equation \equ(GFGMid) is solved, and we have a ``general'' {\tt Fun} for the function $\wh h$ defined in \equ(gfgfunVar), we convert this set to even type. The basic operations involving sets in $\AXY_\rho$ are defined in the package {\tt Funs2}. We recall that \equ(GFGMid) is solved by first computing a numerical approximation for the functions $\VV$. This is done by the procedure {\tt Funs2.Num.NumCompZero}. Then {\tt RG.MidPoint} verifies that this approximate solution satisfies the hypotheses of \clm(VCompZero). This yields an upper bound $r$ on the norm of the error, so it suffices to add a ball of radius $r$ to the approximate solution, to obtain a {\tt Fun}-type set that contains the true midpoint function $\VV$. The above discussion should make clear that we can constructively define a map {\tt Renorm}, from {\tt Fun} to ${\tt Fun}\cup\{{\tt Error}\}$, with the following property: If $g\in \BB({\tt G1})$, and if {\tt Renorm} yields a set {\tt G2}, then $\NN(g)\in \BB({\tt G2})$. In the context of computer-assisted proofs, such a set-map is called a ``bound'' on the map $\NN$. Bounds on maps like $\NN$ and $\MM$ are defined in the package {\tt RG}. They use bounds on more basic maps, defined in {\tt Funs2}, which in turn use bounds defined in {\tt Taylors2}, etc. If a domain {\tt Error} occurs along the way (meaning that some condition could not be verified), then the program is simply halted. Our bound on $\MM$ is named {\tt Contract}. One of the steps in the proof of \clm(MMFix) is to verify that $\|\MM(0)\|_\varrho\le\eps$. This is done simply by applying {\tt Contract} to the set $\{0\}$, and then evaluating the {\tt Norm} of the resulting set of functions, which yields a set of numbers named {\tt Eps}. The maximum {\tt Sup(Eps)} defines our choice of $\eps$ in \clm(MMFix). Then $r$ is determined in such a way that $\eps+\kappa r